Alice de Berny pushed to branch alice at Stefan / Typer
Commits: a7682e1c by irradiee at 2020-06-02T12:15:18-04:00 split lexp_whnf in 2 fun
- - - - -
4 changed files:
- src/elab.ml - src/eval.ml - src/opslexp.ml - src/unification.ml
Changes:
===================================== src/elab.ml ===================================== @@ -121,13 +121,12 @@ let sform_default_ectx = ref empty_elab_context * to errors in the user's code). *)
let elab_check_sort (ctx : elab_context) lsort var ltp = - let lp = lexp_lexp' (try OL.lexp_whnf lsort (ectx_to_lctx ctx) + match (try OL.lexp'_whnf lsort (ectx_to_lctx ctx) with e -> info ~print_action:(fun _ -> lexp_print lsort; print_newline ()) ~loc:(lexp_location lsort) "Exception during whnf of sort:"; - raise e) in - match lp with + raise e) with | Sort (_, _) -> () (* All clear! *) | _ -> let typestr = lexp_string ltp ^ " : " ^ lexp_string lsort in match var with @@ -579,8 +578,7 @@ and infer (p : sexp) (ctx : elab_context): lexp * ltype =
and elab_special_form ctx f args ot = let loc = lexp_location f in - let lp = lexp_lexp' (OL.lexp_whnf f (ectx_to_lctx ctx)) in - match lp with + match (OL.lexp'_whnf f (ectx_to_lctx ctx)) with | Builtin ((_, name), _, _) -> (* Special form. *) (get_special_form name) ctx loc args ot @@ -628,8 +626,7 @@ and get_implicit_arg ctx loc oname t = (* Build the list of implicit arguments to instantiate. *) and instantiate_implicit e t ctx = let rec instantiate t args = - let lp = lexp_lexp' (OL.lexp_whnf t (ectx_to_lctx ctx)) in - match lp with + match OL.lexp'_whnf t (ectx_to_lctx ctx) with | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) -> let arg = get_implicit_arg ctx (lexp_location e) v t1 in instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) @@ -641,8 +638,7 @@ and infer_type pexp ectx var = * Sort (?s), but in most cases the metavar would be allocated * unnecessarily. *) let t, s = infer pexp ectx in - (let lp = lexp_lexp' (OL.lexp_whnf s (ectx_to_lctx ectx)) in - match lp with + (match OL.lexp'_whnf s (ectx_to_lctx ectx) with | Sort (_, _) -> () (* All clear! *) (* FIXME: We could automatically coerce Type levels to Sorts, so we * could write `(a : TypeLevel) -> a -> a` instead of @@ -705,8 +701,7 @@ and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = * do lots of other things. *) and check_inferred ctx e inferred_t t = let (e, inferred_t) = - let lp = lexp_lexp' (OL.lexp_whnf t (ectx_to_lctx ctx)) in - match lp with + match OL.lexp'_whnf t (ectx_to_lctx ctx) with | Arrow ((Aerasable | Aimplicit), _, _, _, _) -> (e, inferred_t) | _ -> instantiate_implicit e inferred_t ctx in @@ -757,8 +752,7 @@ and check_case rtype (loc, target, ppatterns) ctx = | [] -> () in (cs, args) | None - -> let lp = lexp_lexp' (OL.lexp_whnf it' (ectx_to_lctx ctx)) in - match lp with + -> match OL.lexp'_whnf it' (ectx_to_lctx ctx) with | Inductive (_, _, fargs, constructors) -> let (s, targs) = List.fold_left (fun (s, targs) (ak, name, t) @@ -774,14 +768,12 @@ and check_case rtype (loc, target, ppatterns) ctx = it_cs_as := Some (it', cs, args); (cs, args) | _ -> let call_split e = - let lp = lexp_lexp' (OL.lexp_whnf e (ectx_to_lctx ctx)) in - match lp with + match OL.lexp'_whnf e (ectx_to_lctx ctx) with | Call (f, args) -> (f, args) | _ -> (e,[]) in let (it, targs) = call_split tltp in let constructors = - let lp = lexp_lexp' (OL.lexp_whnf it (ectx_to_lctx ctx)) in - match lp with + match OL.lexp'_whnf it (ectx_to_lctx ctx) with | Inductive (_, _, fargs, constructors) -> assert (List.length fargs = List.length targs); constructors @@ -806,17 +798,16 @@ and check_case rtype (loc, target, ppatterns) ctx = let loc = sexp_location pctor in let lctor, ct = infer pctor ctx in let rec inst_args ctx e = - let lp = OL.lexp_whnf e (ectx_to_lctx ctx) in - match lexp_lexp' lp with + let lxp = OL.lexp_whnf e (ectx_to_lctx ctx) in + match lexp_lexp' lxp 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 -> lp in - let lp = lexp_lexp' (nosusp (inst_args ctx lctor)) in - match lp with + | e -> lxp in + match lexp_lexp' (nosusp (inst_args ctx lctor)) with | Cons (it', (_, cons_name)) -> let _ = check_uniqueness pat cons_name lbranches in let (constructors, targs) = get_cs_as it' lctor in @@ -1018,7 +1009,7 @@ and lexp_parse_inductive ctors ctx = -> hc (Arrow (Aerasable, vname, t, l, e))) altacc in - if altacc' == altacc + if lexp_lexp' altacc' == lexp_lexp' altacc then acc (* No generalization! *) else (* Convert the Lexp back into a list of fields. *) @@ -1365,8 +1356,7 @@ and sform_add_attribute ctx loc (sargs : sexp list) ot = | _ -> fatal ~loc "add-attribute expects 3 arguments (table; var; attr)" in
let map, attr_type = - let lp = lexp_lexp' (OL.lexp_whnf table (ectx_to_lctx ctx)) in - match lp with + match OL.lexp'_whnf table (ectx_to_lctx ctx) with | Builtin (_, attr_type, Some map) -> map, attr_type | _ -> fatal ~loc "add-attribute expects a table as first argument" in
@@ -1383,8 +1373,7 @@ and get_attribute ctx loc largs = | _ -> fatal ~loc "get-attribute expects 2 arguments (table; var)" in
let map = - let lp = lexp_lexp' (OL.lexp_whnf table (ectx_to_lctx ctx)) in - match lp with + match OL.lexp'_whnf table (ectx_to_lctx ctx) with | Builtin (_, attr_type, Some map) -> map | _ -> fatal ~loc "get-attribute expects a table as first argument" in
===================================== src/eval.ml ===================================== @@ -738,9 +738,8 @@ let constructor_p name ectx = (* Use `lexp_whnf` so that `name` can be indirectly * defined as a constructor * (e.g. as in `let foo = cons in case foo x xs | ...` *) - let lwhnf = lexp_lexp' (OL.lexp_whnf (mkVar ((dummy_location, Some name), idx)) - (ectx_to_lctx ectx)) in - match lwhnf with + match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) + (ectx_to_lctx ectx) with | Cons _ -> true (* It's indeed a constructor! *) | _ -> false with Senv_Lookup_Fail _ -> false @@ -754,9 +753,8 @@ let erasable_p name nth ectx = else false | _ -> false in try let idx = senv_lookup name ectx in - let lwhnf = lexp_lexp' (OL.lexp_whnf (mkVar ((dummy_location, Some name), idx)) - (ectx_to_lctx ectx)) in - match lwhnf with + match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) + (ectx_to_lctx ectx) with | Cons ((Var v, _), _) -> ( match (env_lookup_expr ectx v) with | Some (Inductive (_, _, _, ctors), _) -> is_erasable ctors @@ -775,9 +773,8 @@ let erasable_p2 t name ectx = args) | _ -> false in try let idx = senv_lookup t ectx in - let lwhnf = lexp_lexp' (OL.lexp_whnf (mkVar ((dummy_location, Some t), idx)) - (ectx_to_lctx ectx)) in - match lwhnf with + match OL.lexp'_whnf (mkVar ((dummy_location, Some t), idx)) + (ectx_to_lctx ectx) with | Cons ((Var v, _), _) -> ( match (env_lookup_expr ectx v) with | Some (Inductive (_, _, _, ctors), _) -> is_erasable ctors @@ -794,9 +791,8 @@ let nth_ctor_arg name nth ectx = | exception (Failure _) -> "_" ) | _ -> "_" in try let idx = senv_lookup name ectx in - let lwhnf = lexp_lexp' (OL.lexp_whnf (mkVar ((dummy_location, Some name), idx)) - (ectx_to_lctx ectx)) in - match lwhnf with + match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) + (ectx_to_lctx ectx) with | Cons ((Var v, _), _) -> ( match (env_lookup_expr ectx v) with | Some (Inductive (_, _, _, ctors), _) -> find_nth ctors @@ -816,9 +812,8 @@ let ctor_arg_pos name arg ectx = | Some n -> n ) | _ -> (-1) in try let idx = senv_lookup name ectx in - let lwhnf = lexp_lexp' (OL.lexp_whnf (mkVar ((dummy_location, Some name), idx)) - (ectx_to_lctx ectx)) in - match lwhnf with + match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) + (ectx_to_lctx ectx) with | Cons ((Var v, _), _) -> ( match (env_lookup_expr ectx v) with | Some (Inductive (_, _, _, ctors), _) -> find_arg ctors
===================================== src/opslexp.ml ===================================== @@ -132,8 +132,9 @@ let lexp_close lctx e = * but only on *types*. If you must use it on code, be sure to use its * return value as little as possible since WHNF will inherently introduce * call-by-name behavior. *) -let lexp_whnf e (ctx : DB.lexp_context) : lexp = - let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = + +let lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = +let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = let le' = lexp_lexp' e in match le' with | Var v -> (match lookup_value ctx v with @@ -141,38 +142,38 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp = (* We can do this blindly even for recursive definitions! * IOW the risk of inf-looping should only show up when doing * things like full normalization (e.g. lexp_conv_p). *) - | Some e' -> lexp_whnf e' ctx) - | Susp (e, s) -> lexp_whnf (push_susp e s) ctx - | Call (e, []) -> lexp_whnf e ctx + | Some e' -> lexp_whnf_aux e' ctx) + | Susp (e, s) -> lexp_whnf_aux (push_susp e s) ctx + | Call (e, []) -> lexp_whnf_aux e ctx | Call (f, (((_, arg)::args) as xs)) -> - (let lwhnf' = lexp_lexp' (lexp_whnf f ctx) in + (let lwhnf' = lexp_lexp' (lexp_whnf_aux f ctx) in match lwhnf' with | Lambda (_, _, _, body) -> (* Here we apply whnf to the arg eagerly to kind of stay closer * to the idea of call-by-value, although in this context * we can't really make sure we always reduce the arg to a value. *) - lexp_whnf (mkCall (push_susp body (S.substitute (lexp_whnf arg ctx)), + lexp_whnf_aux (mkCall (push_susp body (S.substitute (lexp_whnf_aux arg ctx)), args)) ctx | Call (f', xs1) -> mkCall (f', List.append xs1 xs) | _ -> e) (* Keep `e`, assuming it's more readable! *) | Case (l, e, rt, branches, default) -> - let e' = lexp_whnf e ctx in + let e' = lexp_whnf_aux e ctx in let reduce name aargs = try let (_, _, branch) = SMap.find name branches in let (subst, _) = List.fold_left (fun (s,d) (_, arg) -> - (S.cons (L.mkSusp (lexp_whnf arg ctx) (S.shift d)) s, + (S.cons (L.mkSusp (lexp_whnf_aux arg ctx) (S.shift d)) s, d + 1)) (S.identity, 0) aargs in - lexp_whnf (push_susp branch subst) ctx + lexp_whnf_aux (push_susp branch subst) ctx with Not_found -> match default with | Some (v,default) - -> lexp_whnf (push_susp default (S.substitute e')) ctx + -> lexp_whnf_aux (push_susp default (S.substitute e')) ctx | _ -> Log.log_error ~section:"WHNF" ~loc:l ("Unhandled constructor " ^ name ^ "in case expression"); @@ -181,25 +182,30 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp = match e'' with | Cons (_, (_, name)) -> reduce name [] | Call (f, aargs) -> - (let lwhnf = lexp_lexp' (lexp_whnf f ctx) in + (let lwhnf = lexp_lexp' (lexp_whnf_aux f ctx) in match lwhnf with | Cons (_, (_, name)) -> reduce name aargs | _ -> mkCase (l, e, rt, branches, default)) | _ -> mkCase (l, e, rt, branches, default)) | Metavar (idx, s, _) -> (match metavar_lookup idx with - | MVal e -> lexp_whnf (push_susp e s) ctx + | MVal e -> lexp_whnf_aux (push_susp e s) ctx | _ -> e)
(* FIXME: I'd really prefer to use "native" recursive substitutions, using * ideally a trick similar to the db_offsets in lexp_context! *) | Let (l, defs, body) - -> lexp_whnf (push_susp body (lexp_defs_subst l S.identity defs)) ctx + -> lexp_whnf_aux (push_susp body (lexp_defs_subst l S.identity defs)) ctx
| elem -> e
- in lexp_whnf e ctx + in lexp_whnf_aux e ctx
+let lexp'_whnf e (ctx : DB.lexp_context) : lexp' = + lexp_lexp' (lexp_whnf_aux e ctx) + +let lexp_whnf e (ctx : DB.lexp_context) : lexp = + lexp_whnf_aux e ctx
(** A very naive implementation of sets of pairs of lexps. *) type set_plexp = (lexp * lexp) list @@ -260,8 +266,8 @@ let level_leq (c1, m1) (c2, m2) = let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let e1' = lexp_whnf e1 ctx in let e2' = lexp_whnf e2 ctx in - let e1''= lexp_lexp' e1' in - let e2'' = lexp_lexp' e2' in + let e1'' = lexp'_whnf e1 ctx in + let e2'' = lexp'_whnf e2 ctx in e1'' == e2'' || let changed = not (lexp_lexp' e1 == e1'' && lexp_lexp' e2 == e2'') in if changed && set_member_p vs e1' e2' then true else @@ -325,7 +331,7 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = (set_shift vs) args1 args2 | _,_ -> false in - l1 == l2 && conv_args ctx vs' args1 args2 + lexp_lexp' l1 == lexp_lexp' l2 && conv_args ctx vs' args1 args2 | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> l1 = l2 && conv_p t1 t2 (* I'm not sure to understand how to compare two Metavar * * Should I do a `lookup`? Or is it that simple: *) @@ -334,7 +340,7 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | (_, _) -> false
let conv_p (ctx : DB.lexp_context) e1 e2 - = if e1 == e2 then true + = if lexp_lexp' e1 == lexp_lexp' e2 then true else conv_p' ctx set_empty e1 e2
(********* Testing if a lexp is properly typed *********) @@ -363,8 +369,8 @@ type sort_compose_result let sort_compose ctx1 ctx2 l ak k1 k2 = (* BEWARE! Technically `k2` can refer to `v`, but this should only happen * if `v` is a TypeLevel. *) - let lwhnf1 = lexp_lexp' (lexp_whnf k1 ctx1) in - let lwhnf2 = lexp_lexp' (lexp_whnf k2 ctx2) in + let lwhnf1 = lexp'_whnf k1 ctx1 in + let lwhnf2 = lexp'_whnf k2 ctx2 in match (lwhnf1, lwhnf2) with | (Sort (_, s1), Sort (_, s2)) -> (match s1, s2 with @@ -443,8 +449,7 @@ let rec check'' erased ctx e = (* Log.internal_error "Type mismatch" *)) in let check_type erased ctx t = let s = check erased ctx t in - (let lwhnf = lexp_lexp' (lexp_whnf s ctx) in - match lwhnf with + (match lexp'_whnf s ctx with | Sort _ -> () | _ -> error_tc ~loc:(lexp_location t) ("Not a proper type: " ^ lexp_string t)); @@ -542,8 +547,7 @@ let rec check'' erased ctx e = (fun ft (ak,arg) -> let at = check (if ak = P.Aerasable then DB.set_empty else erased) ctx arg in - let lwhnf = lexp_lexp' (lexp_whnf ft ctx) in - match lwhnf with + match lexp'_whnf ft ctx with | Arrow (ak', v, t1, l, t2) -> if not (ak == ak') then (error_tc ~loc:(lexp_location arg) @@ -612,8 +616,7 @@ let rec check'' erased ctx e = | _ -> (e,[]) in let etype = lexp_whnf (check erased ctx e) ctx in let it, aargs = call_split etype in - (let lwhnf = lexp_lexp' (lexp_whnf it ctx) in - match lwhnf, aargs with + (match lexp'_whnf it ctx, aargs with | Inductive (_, _, fargs, constructors), aargs -> let rec mksubst s fargs aargs = match fargs, aargs with @@ -662,8 +665,7 @@ let rec check'' erased ctx e = | _,_ -> error_tc ~loc:l "Case on a non-inductive type!"); ret | Cons (t, (l, name)) - -> (let lwhnf = lexp_lexp' (lexp_whnf t ctx) in - match lwhnf with + -> (match lexp'_whnf t ctx with | Inductive (l, _, fargs, constructors) -> (try let fieldtypes = SMap.find name constructors in @@ -860,8 +862,7 @@ let rec get_type ctx e = -> let ft = get_type ctx f in List.fold_left (fun ft (ak,arg) - -> let lwhnf = lexp_lexp' (lexp_whnf ft ctx) in - match lwhnf with + -> match lexp'_whnf ft ctx with | Arrow (ak', v, t1, l, t2) -> mkSusp t2 (S.substitute arg) | _ -> ft) @@ -877,8 +878,7 @@ let rec get_type ctx e = let (level, _, _) = List.fold_left (fun (level, ictx, n) (ak, v, t) -> - ((let lwhnf = lexp_lexp' (lexp_whnf (get_type ictx t) ictx) in - match lwhnf with + ((match lexp'_whnf (get_type ictx t) ictx with | Sort (_, Stype _) when ak == P.Aerasable && impredicative_erase -> level @@ -902,8 +902,7 @@ let rec get_type ctx e = tct | Case (l, e, ret, branches, default) -> ret | Cons (t, (l, name)) - -> (let lwhnf = lexp_lexp' (lexp_whnf t ctx) in - match lwhnf with + -> (match lexp'_whnf t ctx with | Inductive (l, _, fargs, constructors) -> (try let fieldtypes = SMap.find name constructors in
===================================== src/unification.ml ===================================== @@ -184,15 +184,15 @@ 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 [] else + if lexp_lexp' e1 == lexp_lexp' e2 then [] else let e1' = OL.lexp_whnf e1 ctx in let e2' = OL.lexp_whnf e2 ctx in - if e1' == e2' then [] else + let e1'' = lexp_lexp' e1' in + let e2'' = lexp_lexp' e2' in + if e1'' == e2'' then [] else let changed = true (* not (e1 == e1' && e2 == e2') *) in if changed && OL.set_member_p vs e1' e2' then [] else let vs' = if changed then OL.set_add vs e1' e2' else vs in - let e1'' = lexp_lexp' e1' in - let e2'' = lexp_lexp' e2' in match (e1'', e2'') with | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _) | (Var _, Var _))
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/a7682e1c73354e184e9129f4e13368fcba...