Stefan pushed to branch master at Stefan / Typer

Commits: cf67844d by Stefan Monnier at 2019-09-13T21:06:03Z First tweak to try and handle parameterized inductives

* src/elab.ml (check_case.add_branch): Try and handle parameterized constructors. (elab_check_def): Slightly improve message.

* src/unification.ml (unify_inductive): New function. (unify'): Use it.

- - - - -

3 changed files:

- src/elab.ml - src/lexp.ml - src/unification.ml

Changes:

===================================== src/elab.ml ===================================== @@ -171,7 +171,8 @@ let elab_check_def (ctx : elab_context) var lxp ltype = elab_check_proper_type ctx ltype var else (EV.debug_messages fatal loc "Type check error: ¡¡ctx_define error!!" [ - lexp_string lxp ^ " !: " ^ lexp_string ltype; + (match var with (_, Some n) -> n | _ -> "<anon>") + ^ " = " ^ lexp_string lxp ^ " !: " ^ lexp_string ltype; " because"; lexp_string ltype' ^ " != " ^ lexp_string ltype])

@@ -650,7 +651,15 @@ and check_case rtype (loc, target, ppatterns) ctx = let add_branch pctor pargs = let loc = sexp_location pctor in let lctor, ct = infer pctor ctx in - match OL.lexp_whnf lctor (ectx_to_lctx ctx) with + let rec inst_args ctx e = match OL.lexp_whnf e (ectx_to_lctx ctx) with + | Lambda (Aerasable, v, t, body) + -> let arg = newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx) + v t in + let nctx = ctx_extend ctx v Variable t in + let body = inst_args nctx body in + mkSusp body (S.substitute arg) + | e -> e in + match nosusp (inst_args ctx lctor) with | Cons (it', (_, cons_name)) -> let _ = match Unif.unify it' it (ectx_to_lctx ctx) with | (None | Some (_::_)) @@ -676,7 +685,7 @@ and check_case rtype (loc, target, ppatterns) ctx = pargs (* Pattern arguments. *) cargs (* Constructor arguments. *) pe (* Pending explicit pattern args. *) - acc = (* Accumulated reult. *) + acc = (* Accumulated result. *) match (pargs, cargs) with | (_, []) when not (SMap.is_empty pe) -> let pending = SMap.bindings pe in

===================================== src/lexp.ml ===================================== @@ -281,8 +281,7 @@ let rec sunshift n = else (assert (n >= 0); S.cons impossible (sunshift (n - 1)))

-let _ = assert (S.identity (* Sanity check! *) - = scompose (S.shift 5) (sunshift 5)) +let _ = assert (S.identity_p (scompose (S.shift 5) (sunshift 5)))

(* The quick test below seemed to indicate that about 50% of the "sink"s * are applied on top of another "sink" and hence cound be combined into

===================================== src/unification.ml ===================================== @@ -1,6 +1,6 @@ (* unification.ml --- Unification of Lexp terms

-Copyright (C) 2016-2018 Free Software Foundation, Inc. +Copyright (C) 2016-2019 Free Software Foundation, Inc.

Author: Vincent Bonnevalle tiv.crb@gmail.com

@@ -132,14 +132,16 @@ let rec unify (e1: lexp) (e2: lexp) and unify' (e1: lexp) (e2: lexp) (ctx : DB.lexp_context) (vs : OL.set_plexp) : return_type = + if e1 == e2 then Some [] else let e1' = OL.lexp_whnf e1 ctx in let e2' = OL.lexp_whnf e2 ctx in - let changed = not (e1 == e1' && e2 == e2') in + if e1' == e2' then Some [] else + let changed = true (* not (e1 == e1' && e2 == e2') *) in if changed && OL.set_member_p vs e1' e2' then Some [] else let vs' = if changed then OL.set_add vs e1' e2' else vs in match (e1', e2') with | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _) - | (Var _, Var _) | (Inductive _, Inductive _)) + | (Var _, Var _)) -> if OL.conv_p ctx e1' e2' then Some [] else None | (l, (Metavar (idx, s, _) as r)) -> unify_metavar ctx idx s r l | ((Metavar (idx, s, _) as l), r) -> unify_metavar ctx idx s l r @@ -152,7 +154,17 @@ and unify' (e1: lexp) (e2: lexp) (* | (Inductive _ as l, r) -> unify_induct l r subst *) | (Sort _ as l, r) -> unify_sort l r ctx vs' | (SortLevel _ as l, r) -> unify_sortlvl l r ctx vs' - | _ -> Some (if OL.conv_p ctx e1' e2' then [] else [(e1, e2)]) + | (Inductive (_loc1, label1, args1, consts1), + Inductive (_loc2, label2, args2, consts2)) + -> (* print_string ("Unifying inductives " + * ^ snd label1 + * ^ " and " + * ^ snd label2 + * ^ "\n"); *) + unify_inductive ctx vs' args1 args2 consts1 consts2 + | _ -> Some (if OL.conv_p ctx e1' e2' then [] + else ((* print_string "Unification failure on default\n"; *) + [(e1, e2)]))

(********************************* Type specific unify *******************************)

@@ -401,6 +413,26 @@ and is_same arglist arglist2 = * | None -> test e subst) * ) None lst *)

+and unify_inductive ctx vs args1 args2 consts1 consts2 = + let unif_formals ctx vs args1 args2 + = if not (List.length args1 == List.length args2) then (ctx, vs, None) else + List.fold_left (fun (ctx, vs, residue) ((ak1, v1, t1), (ak2, v2, t2)) + -> (DB.lexp_ctx_cons ctx v1 Variable t1, + OL.set_shift vs, + if not (ak1 == ak2) then None + else unify_and (unify' t1 t2 ctx vs) residue)) + (ctx, vs, Some []) + (List.combine args1 args2) in + let (ctx, vs, residue) = unif_formals ctx vs args1 args2 in + if not (SMap.cardinal consts1 == SMap.cardinal consts2) then None else + SMap.fold (fun cname args1 residue + -> match SMap.find cname consts2 with + | args2 -> let (_ctx, _vs, residue') + = unif_formals ctx vs args1 args2 in + unify_and residue' residue + | exception Not_found -> None) + consts1 residue + (** unify the SMap of list in Inductive *) (* and unify_induct_sub_list l1 l2 subst = * let test l1 l2 subst =

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