BONNEVALLE Vincent pushed to branch unification at Stefan / Typer

Commits: 9652bc5e by n3f4s at 2016-07-04T21:54:46+02:00 add lexp S.subst to Metavar

- - - - - 96a7856a by n3f4s at 2016-07-04T21:55:54+02:00 change expected result of test for Lambda * Lambda

- - - - - 05aea4ec by n3f4s at 2016-07-04T21:57:05+02:00 add Metavar in unsusp

- - - - - e2e37a5c by n3f4s at 2016-07-06T16:04:59+02:00 add beginning of index substitution in _unify_meta

- - - - -

4 changed files:

- src/fmt_lexp.ml - src/lexp.ml - src/unification.ml - tests/unify_test.ml

Changes:

===================================== src/fmt_lexp.ml ===================================== --- a/src/fmt_lexp.ml +++ b/src/fmt_lexp.ml @@ -22,7 +22,7 @@ let rec string_of_lxp lxp = | Var ((_, name), idx) -> "Var(" ^ name ^ ", #" ^(string_of_int idx) ^ ")" | Arrow (_, _, a, _, b) -> "Arrow(" ^ (string_of_lxp a) ^ " => " ^ (string_of_lxp b) ^ ")" | Lambda (_,(_, name), dcl, body) -> "Lambda(" ^ name ^ ": " ^ (string_of_lxp dcl) ^ " => (" ^ (string_of_lxp body) ^ "))" - | Metavar (value, (_, name)) -> "Metavar(" ^ (string_of_int value) ^ ", " ^ name ^ ")" + | Metavar (value, _, (_, name)) -> "Metavar(" ^ (string_of_int value) ^ ", " ^ name ^ ")" | Call (_) -> "Call(...)" | Inductive _ -> ("Inductive") ^ "(...)" | Sort _ -> ("Sort") ^ "(...)" @@ -43,7 +43,7 @@ let colored_string_of_lxp lxp lcol vcol = | Arrow (_, _, a, _, b) -> (lcol "Arrow(") ^ (vcol (string_of_lxp a)) ^ " => " ^ (vcol (string_of_lxp b)) ^ ")" | Lambda (_,(_, name), dcl, body) -> (lcol "Lambda") ^ "(" ^ (vcol name) ^ " : " ^ (vcol (string_of_lxp dcl)) ^ " => (" ^ (vcol (string_of_lxp body)) ^ "))" - | Metavar (value, (_, name)) -> (lcol "Metavar" ) ^ "(" ^ (vcol (string_of_int value)) ^ ", " ^ (vcol name) ^ ")" + | Metavar (value, _, (_, name)) -> (lcol "Metavar" ) ^ "(" ^ (vcol (string_of_int value)) ^ ", " ^ (vcol name) ^ ")" | Call (_) -> (lcol "Call(...)" ) | Case _ -> (lcol "Case") ^ "(...)" | Inductive _ -> (lcol "Inductive") ^ "(...)"

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -74,7 +74,7 @@ type ltype = lexp * ltype (* The type of the return value of all branches *) * (U.location * (arg_kind * vdef option) list * lexp) SMap.t * lexp option (* Default. *) - | Metavar of int * vdef (*idx * (name * location)*) + | Metavar of int * (lexp S.subst) * vdef (*idx * S.subst * (name * location)*) (* (* For logical metavars, there's no substitution. *) * | Metavar of (U.location * string) * metakind * metavar ref * and metavar = @@ -322,6 +322,7 @@ let rec unsusp e s = (* Push a suspension one level down. *) match default with | None -> default | Some e -> Some (mkSusp e s)) + | Metavar (idx, s', vdef_) -> Metavar(idx, s, vdef_)

let unsusp_all e = match e with

===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -35,7 +35,7 @@ let associate (meta: int) (lxp: lexp) (subst: substitution) *) let find_or_none (value: lexp) (map: substitution) : lexp option = match value with - | Metavar (idx, _) -> (if VMap.mem idx map + | Metavar (idx, _, _) -> (if VMap.mem idx map then Some (VMap.find idx map) else None) | _ -> None @@ -230,15 +230,22 @@ and _unify_lambda (lambda: lexp) (lxp: lexp) (subst: substitution) : return_type * metavar , lexp -> OK *) and _unify_metavar (meta: lexp) (lxp: lexp) (subst: substitution) : return_type = + (** s:S.subst -> l:lexp -> s':S.subst where l[s][s'] = l *) + let rec inverse subst = Some S.Identity + in let find_or_unify metavar value lxp s = match find_or_none metavar s with - | None -> Some ((associate value lxp s, [])) | Some (lxp_) -> unify lxp_ lxp s + | None -> (match metavar with + | Metavar (_, subst_, _) -> (match inverse subst_ with + | Some s' -> Some (associate value (unsusp lxp s') s, []) + | None -> None) + | _ -> None) in match (meta, lxp) with - | (Metavar (val1, _), Metavar (val2, _)) when val1 = val2 -> + | (Metavar (val1, s1, _), Metavar (val2, s2, _)) when val1 = val2 -> Some ((subst, [])) - | (Metavar (v, _), _) -> find_or_unify meta v lxp subst + | (Metavar (v, s1, _), _) -> find_or_unify meta v lxp subst | (_, _) -> None

(** Unify a Call (call) and a lexp (lxp) @@ -326,7 +333,7 @@ and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) (subst: substitution) : return_ty match sortlvl, lxp with | (SortLevel s, SortLevel s2) -> (match s, s2 with | SLn i, SLn j when i = j -> Some (subst, []) - | SLsucc l1, SLsucc l2 -> unify l1 l2 subst (* Is SLsucc some kind of linked list ? *) + | SLsucc l1, SLsucc l2 -> unify l1 l2 subst | _, _ -> None) | _, _ -> None

===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -112,7 +112,7 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) = Lambda ((Aexplicit), (Util.dummy_location, "L2"), Var((Util.dummy_location, "z"), 4), - Imm (Integer (Util.dummy_location, 3))), Unification ) (* Should unify with index shift *) + Imm (Integer (Util.dummy_location, 3))), Nothing )

::(input_induct , input_induct , Equivalent) ::(input_int_4 , input_int_4 , Equivalent) @@ -160,6 +160,7 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) = ::(input_arrow3 , input_arrow , Constraint) (* of the var inside the arrow *) ::(input_arrow2 , input_arrow , Equivalent) ::(input_arrow3 , input_arrow3 , Equivalent) + ::(Metavar (0, S.Identity, (Util.dummy_location, "M")), Var ((Util.dummy_location, "x"), 3), Unification)

::[]

View it on GitLab: https://gitlab.com/monnier/typer/compare/8a0ad87e19e240c9d9341baafb845746f8f...