Stefan pushed to branch unification at Stefan / Typer

Commits: 4e504963 by Stefan Monnier at 2016-07-28T12:42:23-04:00 Tweak use of substitutions and unsusp

* src/inverse_subst.ml (mkFinalShift): Remove; use S.shift instead. (toIr): Use S.mkShift. (flattenIr.flattenCons): Remove unused `offset' arg. Simplify.

* src/lexp.ml (subst): Newtype. (mkSusp): Also apply eagerly to Metavar. (push_susp): Rename from unsusp. (nosusp): Rename from ususp_all. (_lexp_to_str): Use push_susp.

* src/unification.ml (unify.tmp): Use nosusp. (_unify_susp): Remove.

* tests/inverse_test.ml: Use S.shift/cons and friends.

- - - - -

8 changed files:

- src/elexp.ml - src/inverse_subst.ml - src/lexp.ml - src/lparse.ml - src/subst.ml - src/typecheck.ml - src/unification.ml - tests/inverse_test.ml

Changes:

===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -86,7 +86,7 @@ let rec erase_type (lxp: L.lexp): elexp = Case(l, (erase_type target), (clean_map cases), (clean_maybe default))

- | L.Susp(l, s) -> erase_type (L.unsusp l s) + | L.Susp(l, s) -> erase_type (L.push_susp l s)

(* To be thrown out *) | L.Arrow _ -> Type

===================================== src/inverse_subst.ml ===================================== --- a/src/inverse_subst.ml +++ b/src/inverse_subst.ml @@ -12,28 +12,27 @@ type inter_subst = lexp list (* Intermediate between "tree"-like substitution an

let dummy_var = Var((dummy_location, "DummyVar"), -1)

-(** Make a Shift with Identity as "inner" substitution. - Returns Identity if the Shift offset is lower or equal to 0 -*) -let mkFinalShift (value: int): lexp S.subst = - if value > 0 - then S.Shift (S.Identity, value) - else S.Identity - -(** Transform a subst into a more linear 'intermdiate representation': +(** Transform a subst into a more linear 'intermediate representation':

- - a1.↑^{x1}(a2.↑^{x2}(a3.↑^{x3}id)) -> a1.(↑^{x1}a2).(↑^{x2}a3).↑^{x3}id + - a₁ · ↑n₁ (a₂ · ↑n₂ (a₃ · ↑n₃ id)) + ⇒ a₁' · a₂' · a₃' · ↑n₃ id

or in ocaml-ish representation :

- - S.Cons(var, S.Shift(..., offset)) -> S.Cons(var, S.Shift(S.Identity, offset))::...::Identity + - S.Cons(var, S.Shift(..., offset)) + ⇒ S.Cons(var, S.Shift(S.Identity, offset))::...::Identity *) let toIr (s: lexp S.subst) : inter_subst = - let rec toIr s last_offset = + let rec toIr s total_offset = match s with - | S.Shift (s_1, offset) -> toIr s_1 (last_offset + offset) - | S.Cons(Var _ as v, s_1) -> Susp(v, (S.mkShift S.Identity last_offset))::(toIr s_1 last_offset) - | S.Identity -> [Susp(dummy_var, (S.mkShift S.Identity last_offset ))] + | S.Shift (s_1, offset) -> toIr s_1 (total_offset + offset) + (* FIXME: A Cons with something else than a Var is not an error. + * It might mean that we can't invert this substitution, but that's + * no justification for "assert false". *) + | S.Cons(Var _ as v, s_1) + (* FIXME: Why not L.mkSusp? *) + -> Susp (v, S.shift total_offset)::(toIr s_1 total_offset) + | S.Identity -> [Susp (dummy_var, S.shift total_offset)] | _ -> assert false in toIr s 0

@@ -46,15 +45,14 @@ let toIr (s: lexp S.subst) : inter_subst = - <code>S.Cons(var, S.Shift(S.Identity, offset))::...::Identity -> S.Cons(var, S.Cons(...S.Shift(S.Identity, x1+x2+x3...)))</code> *) let flattenIr (s: inter_subst): lexp S.subst option = - let rec flattenCons s offset = + let rec flattenCons s = match s with - | Susp (_, S.Shift (S.Identity, o))::[] -> Some (S.Shift(S.Identity, o + offset)) - | Susp (_, S.Identity)::[] -> Some (mkFinalShift offset) - | susp::tail -> (match flattenCons tail offset with - | Some (s1) -> Some (S.Cons (unsusp_all susp, s1)) + | Susp (_dummy_var, s)::[] -> Some s + | susp::tail -> (match flattenCons tail with + | Some (s1) -> Some (S.cons (nosusp susp) s1) | None -> None) | _ -> None - in flattenCons s 0 + in flattenCons s

(** Flatten a "tree"-like substitution:

@@ -156,9 +154,9 @@ let to_list (s: lexp S.subst) : (((int * int) list) * int) = let rec to_cons (lst: (int * int) list) (shift: int) : lexp S.subst option = match lst with | (_, i)::tail -> (match (to_cons tail shift) with - | Some s -> Some (S.Cons (mkVar i, s)) + | Some s -> Some (S.cons (mkVar i) s) | None -> None) - | [] -> Some (mkFinalShift shift) + | [] -> Some (S.shift shift)

(** Compute the inverse, if there is one, of the substitution.

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -53,13 +53,14 @@ type label = symbol (* Pour la propagation des types bidirectionnelle, tout va dans `infer`, * sauf Lambda et Case qui vont dans `check`. Je crois. *) type ltype = lexp + and subst = lexp S.subst and lexp = | Imm of sexp (* Used for strings, ... *) | SortLevel of sort_level | Sort of U.location * sort | Builtin of vdef * ltype | Var of vref - | Susp of lexp * lexp S.subst (* Lazy explicit substitution: e[σ]. *) + | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) | Let of U.location * (vdef * lexp * ltype) list * lexp | Arrow of arg_kind * vdef option * ltype * U.location * lexp @@ -74,7 +75,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 * (lexp S.subst) * vdef (*idx * S.subst * (name * location)*) + | Metavar of int * subst * vdef (* (* For logical metavars, there's no substitution. *) * | Metavar of (U.location * string) * metakind * metavar ref * and metavar = @@ -110,9 +111,13 @@ type varbind =

let rec mkSusp e s = if S.identity_p s then e else + (* We apply the substitution eagerly to some terms. + * There's no deep technical rason for that: + * it just seemed like a good idea to do it eagerly when it's easy. *) match e with | Susp (e, s') -> mkSusp e (scompose s' s) - | Var (l,v) -> slookup s l v (* Apply the substitution eagerly. *) + | Var (l,v) -> slookup s l v + | Metavar (vn, s', vd) -> Metavar (vn, scompose s' s, vd) | _ -> Susp (e, s) and scompose s1 s2 = S.compose mkSusp s1 s2 and slookup s l v = S.lookup (fun l i -> Var (l, i)) @@ -272,16 +277,13 @@ let rec lexp_location e = let vdummy = (U.dummy_location, "dummy") let maybev mv = match mv with None -> vdummy | Some v -> v

-let rec unsusp e s = (* Push a suspension one level down. *) +let rec push_susp e s = (* Push a suspension one level down. *) match e with | Imm _ -> e | SortLevel _ -> e | Sort (l, Stype e) -> Sort (l, Stype (mkSusp e s)) | Sort (l, _) -> e | Builtin _ -> e - | Var ((l,_) as lv,v) -> U.msg_error "SUSP" l "¡Susp(Var)!"; slookup s lv v - | Susp (e,s') -> U.msg_error "SUSP" (lexp_location e) "¡Susp(Susp)!"; - mkSusp e (scompose s' s) | Let (l, defs, e) -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in let (_,ndefs) = L.fold_left (fun (s,ndefs) (v, def, ty) @@ -322,11 +324,19 @@ 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.compose (mkSusp) s s'), vdef_) + (* Susp should never appear around Var/Susp/Metavar because mkSusp + * pushes the subst into them eagerly. IOW if there's a Susp(Var..) + * or Susp(Metavar..) it's because some chunk of code should use mkSusp + * rather than Susp. *) + | Susp (e,s') -> U.msg_error "SUSP" (lexp_location e) "¡Susp(Susp)!"; + push_susp e (scompose s' s) + | (Var _ | Metavar _) + -> U.msg_error "SUSP" (lexp_location e) "¡Susp((meta)var)!"; + push_susp (mkSusp e s) S.identity

-let unsusp_all e = +let nosusp e = (* Return `e` without `Susp`. *) match e with - | Susp(e, s) -> unsusp e s + | Susp(e, s) -> push_susp e s | _ -> e

let lexp_to_string e = @@ -670,7 +680,7 @@ and _lexp_to_str ctx exp = | Float (_, s) -> tval (string_of_float s) | e -> sexp_to_str e)

- | Susp _ -> _lexp_to_str ctx (unsusp_all exp) + | Susp (e, s) -> _lexp_to_str ctx (push_susp e s)

| Var ((loc, name), idx) -> name ^ (index idx) ;

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -241,7 +241,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = let inductive_type = Var((loc, type_name), idx) in

(* Get constructor args *) - let formal, args = match unsusp_all idt with + let formal, args = match nosusp idt with | Inductive(_, _, formal, ctor_def) -> ( try formal, (SMap.find cname ctor_def) with Not_found -> @@ -297,7 +297,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = (* This case cannot be inferred *) | Plambda (kind, var, None, body) ->( (* Read var type from the provided type *) - let ltp, lbtp = match unsusp_all t with + let ltp, lbtp = match nosusp t with | Arrow(kind, _, ltp, _, lbtp) -> ltp, lbtp | _ -> lexp_error tloc "Type does not match"; dltype, dltype in

@@ -402,7 +402,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =

(* consume Arrows and args together *) let rec get_return_type name i ltp args = - match (unsusp_all ltp), args with + match (nosusp ltp), args with | _, [] -> ltp | Arrow(_, _, _, _, ltp), hd::tl -> (get_return_type name (i + 1) ltp tl) | _, _ -> lexp_warning loc @@ -416,7 +416,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =

(* retrieve function's body *) let body, ltp = _lexp_p_infer fun_name ctx (i + 1) in - let ltp = unsusp_all ltp in + let ltp = nosusp ltp in

let handle_named_call (loc, name) = (* Process Arguments *) @@ -428,7 +428,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = let idx = senv_lookup name ctx in let vf = (make_var name idx loc) in

- match unsusp_all (env_lookup_expr ctx ((loc, name), idx)) with + match nosusp (env_lookup_expr ctx ((loc, name), idx)) with | Builtin((_, "Built-in"), _) ->( (* ------ SPECIAL ------ *) match !_parsing_internals, largs with @@ -476,7 +476,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = lexp_fatal loc (name ^ " was found but " ^ (string_of_int idx) ^ " is not a correct index.") in

- let lxp = match unsusp_all lxp with + let lxp = match nosusp lxp with | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct | _ -> print_string "\n"; @@ -555,7 +555,7 @@ and lexp_read_pattern pattern exp target ctx: | Ppatvar ((loc, name) as var) ->( try( let idx = senv_lookup name ctx in - match unsusp_all (env_lookup_expr ctx ((loc, name), idx)) with + match nosusp (env_lookup_expr ctx ((loc, name), idx)) with (* We are matching a constructor *) | Cons _ -> (name, loc, []), ctx

@@ -641,7 +641,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * lexp_context) = " is not a correct index.") in

(* get stored function *) - let lxp = match unsusp_all lxp with + let lxp = match nosusp lxp with | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct | _ -> print_string "\n"; print_string (lexp_to_string lxp); print_string "\n";

===================================== src/subst.ml ===================================== --- a/src/subst.ml +++ b/src/subst.ml @@ -21,6 +21,28 @@ this program. If not, see http://www.gnu.org/licenses/. *)

module U = Util

+(* Implementation of the subsitution calculus. + * + * As a general rule, try not to use the constructors of the `subst' + * datatype, but use the following entry points instead. + * Constructor functions: + * - S.identity + * - S.cons + * - S.mkShift + * - S.shift + * - S.compose + * - S.substitute + * - S.sink + * Destructor functions: + * - S.identity_p + * - S.lookup + * + * This implementation is generic (i.e. can be with various datatypes + * implementing the associated lambda-calculus), which is the reason for + * the added complexity of arguments like `mkVar` and `mkShift` to `S.lookup`. + * So in general, you'll want to use Lexp.scompose and Lexp.slookup + * for those functions. + *)

(* Suspensions definitions. * @@ -236,6 +258,7 @@ let shift (m:db_offset) = mkShift Identity m (* The trivial substitution which doesn't do anything. *) let identity = Identity

+(* Test if a substitution is trivial. The "_p" stands for "predicate". *) let identity_p s = match s with | Identity -> true | _ -> false

(* Compose two substitutions. This implements the merging rules.

===================================== src/typecheck.ml ===================================== --- a/src/typecheck.ml +++ b/src/typecheck.ml @@ -110,7 +110,7 @@ let lookup_type ctx vref = let lookup_value ctx vref = let (_, i) = vref in match Myers.nth i ctx with - | (o, _, LetDef v, _) -> Some (unsusp v (S.shift (i + 1 - o))) + | (o, _, LetDef v, _) -> Some (push_susp v (S.shift (i + 1 - o))) | _ -> None

let assert_type e t t' = @@ -151,7 +151,7 @@ let rec check ctx e = | Builtin (_, t) -> t (* FIXME: Check recursive references. *) | Var v -> lookup_type ctx v - | Susp (e, s) -> check ctx (unsusp e s) + | Susp (e, s) -> check ctx (push_susp e s) | Let (_, defs, e) -> let tmp_ctx = L.fold_left (fun ctx (v, e, t)

===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -81,11 +81,11 @@ let zip_fold list1 list2 f = The metavar unifyer is the end rule, it can't call unify with it's parameter (changing their order) *) let rec unify (l: lexp) (r: lexp) (subst: substitution) : return_type = - let tmp = match (l, r) with + let tmp = match (nosusp l, nosusp r) with | (_, Metavar _) -> _unify_metavar r l subst | (_, Call _) -> _unify_call r l subst | (_, Case _) -> _unify_case r l subst - | (_, Susp _) -> _unify_susp r l subst + | (_, Susp _) -> assert false | (_, Let _) -> _unify_let r l subst | (Imm _, _) -> _unify_imm l r subst | (Cons _, _) -> _unify_cons l r subst @@ -96,7 +96,7 @@ let rec unify (l: lexp) (r: lexp) (subst: substitution) : return_type = | (Lambda _, _) -> _unify_lambda l r subst | (Metavar _, _) -> _unify_metavar l r subst | (Call _, _) -> _unify_call l r subst - | (Susp _, _) -> _unify_susp l r subst + | (Susp _, _) -> assert false | (Case _, _) -> _unify_case l r subst | (Inductive _, _) -> _unfiy_induct l r subst | (Sort _, _) -> _unify_sort l r subst @@ -271,13 +271,6 @@ and _unify_call (call: lexp) (lxp: lexp) (subst: substitution) : return_type = | None -> Debug_fun.debug_print_unify "_unify_call" call lxp " -> unification failed"; tmp | Some _ -> Debug_fun.debug_print_unify "_unify_call" call lxp " -> unification success"; tmp

-(** Apply unsusp to the Susp and unify the result with the lexp -*) -and _unify_susp (susp_: lexp) (lxp: lexp) (subst: substitution) : return_type = - match susp_ with - | Susp _ -> unify (unsusp_all susp_) lxp subst - | _ -> None - (** Unify a Case with a lexp - Case, Case -> try to unify - Case, _ -> Constraint

===================================== tests/inverse_test.ml ===================================== --- a/tests/inverse_test.ml +++ b/tests/inverse_test.ml @@ -21,13 +21,13 @@ open Fmt_lexp open Debug_fun

let mkShift2 shift subst = - S.Shift (subst, shift) + S.mkShift subst shift

let rec mkTestSubst lst = match lst with - | (var, shift)::tail -> S.Cons (mkVar var, - mkShift2 shift (mkTestSubst tail)) - | [] -> S.Identity + | (var, shift)::tail -> S.cons (mkVar var) + (mkShift2 shift (mkTestSubst tail)) + | [] -> S.identity

type result_type = | Ok @@ -42,10 +42,10 @@ let input = ((mkTestSubst ((0, 3)::(2, 2)::(4, 5)::[])), Ok):: ((mkTestSubst ((0, 3)::(1, 2)::(4, 5)::[])), Ok):: ((mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(5, 5)::[])), TransfoFail):: - ((S.Cons (mkVar 1, S.Shift(S.Identity, 3))), Ok):: - ((S.Cons (mkVar 1, S.Cons (mkVar 3, S.Identity))), TransfoFail):: - ((S.Shift (S.Shift (S.Identity, 3), 4)), Ok):: - ((S.Shift (S.Cons (mkVar 1, S.Identity), 5)), TransfoFail):: + ((S.cons (mkVar 1) (S.shift 3)), Ok):: + ((S.cons (mkVar 1) (S.cons (mkVar 3) (S.identity))), TransfoFail):: + ((S.mkShift (S.shift 3) 4), Ok):: + ((S.mkShift (S.cons (mkVar 1) (S.identity)) 5), TransfoFail):: ((mkTestSubst ((4, 0)::(2, 2)::(3, 5)::[])), Ok):: ((mkTestSubst ((1, 2)::(5, 1)::(3, 5)::[])), Ok):: ((mkTestSubst ((1, 2)::(5, 2)::(3, 5)::[])), InverseFail):: @@ -59,10 +59,7 @@ let is_identity s = | S.Shift(S.Identity, shift) -> (acc = shift) | S.Identity -> true | _ -> false - in match s with - | S.Shift(S.Identity, _) -> true - | S.Identity -> true - | _ -> is_identity s 0 + in is_identity s 0

let generateRandInput shiftMax numberOfTest = Random.self_init (); @@ -184,8 +181,8 @@ let _ = generate_tests "TRANSFORMATION" (fun (subst, b) -> match flatten subst, b with | Some(s), Ok -> ((subst, (s)), true) | Some(s), InverseFail -> ((subst, (s)), true) - | None, TransfoFail -> ((subst, S.Identity), true) + | None, TransfoFail -> ((subst, S.identity), true) | Some (s), _ -> ((subst, s), false) - | None, _ -> ((subst, S.Identity), false)) + | None, _ -> ((subst, S.identity), false))

let _ = run_all ()

View it on GitLab: https://gitlab.com/monnier/typer/commit/4e5049638ef74bcaa83598d6a10ca91dfe0d...