Stefan pushed to branch master at Stefan / Typer
Commits: 49630b31 by Stefan Monnier at 2016-12-01T22:52:36-05:00 * src/lexp.ml (sort_level): Add SLlub
* src/opslexp.ml (level_canon, level_leq): New functions. (mkSLlub): New function, to replace sort_level_max. (sort_compose): Use it. Add ctx args. (check'): Use it as well.
* tests/eval_test.ml ("Partial Application"): Use negation to make sure the args are passed in the right order.
- - - - -
4 changed files:
- src/eval.ml - src/lexp.ml - src/opslexp.ml - tests/eval_test.ml
Changes:
===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -588,6 +588,7 @@ let eval_all lxps rctx silent = let varname s = match s with Some (_, v) -> v | _ -> "<anon>"
(* build a rctx from a lctx. *) +(* FIXME: `eval` with a disabled runIO, and then memoize, memoize, ... *) let from_lctx (ctx: elab_context): runtime_env = let (_, lctx) = ctx in let rctx : runtime_env
===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -114,6 +114,7 @@ type ltype = lexp and sort_level = | SLz | SLsucc of lexp + | SLlub of lexp * lexp
type varbind = | Variable @@ -184,6 +185,7 @@ let rec lexp_location e = match e with | Sort (l,_) -> l | SortLevel (SLsucc e) -> lexp_location e + | SortLevel (SLlub (e, _)) -> lexp_location e | SortLevel SLz -> U.dummy_location | Imm s -> sexp_location s | Var ((l,_),_) -> l @@ -210,6 +212,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) | Imm _ -> e | SortLevel (SLz) -> e | SortLevel (SLsucc e') -> mkSortLevel (SLsucc (mkSusp e' s)) + | SortLevel (SLlub (e1, e2)) -> mkSortLevel (SLlub (mkSusp e1 s, mkSusp e2 s)) | Sort (l, Stype e) -> mkSort (l, Stype (mkSusp e s)) | Sort (l, _) -> e | Builtin _ -> e @@ -275,6 +278,7 @@ let clean meta_ctx e = | Imm _ -> e | SortLevel (SLz) -> e | SortLevel (SLsucc e) -> mkSortLevel (SLsucc (clean s e)) + | SortLevel (SLlub (e1, e2)) -> mkSortLevel (SLlub (clean s e1, clean s e2)) | Sort (l, Stype e) -> mkSort (l, Stype (clean s e)) | Sort (l, _) -> e | Builtin _ -> e @@ -423,6 +427,9 @@ let rec lexp_unparse lxp = | SortLevel (SLsucc l) -> Pcall (Pbuiltin (lexp_location l, "TypeLevel.succ"), [pexp_unparse (lexp_unparse l)]) + | SortLevel (SLlub (l1, l2)) + -> Pcall (Pbuiltin (lexp_location l1, "TypeLevel.∪"), + [pexp_unparse (lexp_unparse l1); pexp_unparse (lexp_unparse l2)]) | Sort (l, StypeOmega) -> Pbuiltin (l, "Type_ω") | Sort (l, StypeLevel) -> Pbuiltin (l, "Type_ℓ") | Sort (l, Stype sl) @@ -665,6 +672,8 @@ and _lexp_to_str ctx exp =
| SortLevel (SLz) -> "##TypeLevel.z" | SortLevel (SLsucc e) -> "(##TypeLevel.succ " ^ lexp_string e ^ ")" + | SortLevel (SLlub (e1, e2)) + -> "(##TypeLevel.∪ " ^ lexp_string e1 ^ " " ^ lexp_string e1 ^ ")"
and lexp_str_ctor ctx ctors = SMap.fold (fun key value str @@ -707,6 +716,8 @@ let rec eq meta_ctx e1 e2 = | (Imm s1, Imm s2) -> s1 = s2 | (SortLevel SLz, SortLevel SLz) -> true | (SortLevel (SLsucc e1), SortLevel (SLsucc e2)) -> eq e1 e2 + | (SortLevel (SLlub (e11, e21)), SortLevel (SLlub (e12, e22))) + -> eq e11 e12 && eq e21 e22 | (Sort (_, StypeOmega), Sort (_, StypeOmega)) -> true | (Sort (_, StypeLevel), Sort (_, StypeLevel)) -> true | (Sort (_, Stype e1), Sort (_, Stype e2)) -> eq e1 e2
===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -283,21 +283,46 @@ let conv_p meta_ctx (ctx : DB.lexp_context) e1 e2
(********* Testing if a lexp is properly typed *********)
-let rec sort_level_max l1 l2 = match nosusp l1, nosusp l2 with - | SortLevel SLz, l2 -> l2 - | l1, SortLevel SLz -> l1 - | SortLevel (SLsucc l1), SortLevel (SLsucc l2) - -> mkSortLevel (SLsucc (sort_level_max l1 l2)) - | _, _ (* FIXME: This requires s.th. like `SLmax of lexp * lexp`! *) - -> U.msg_error "TC" (lexp_location l1) - ("Can't compute the max of levels `" - ^ lexp_string l1 ^ "` and `" - ^ lexp_string l2 ^ "`"); - mkSortLevel SLz - -let sort_compose l s1 s2 = +(* Turn e into its canonical representation, which is basically the set + * of vars it references along with the number of `succ` applied to them. + * `c` is the maximum "constant" level that occurs in `e` + * and `m` maps variable indices to the maxmimum depth at which they were + * found. *) +let level_canon e = + let rec canon e d ((c,m) as acc) = match e with + | SortLevel SLz -> if c < d then (d, m) else acc + | SortLevel (SLsucc e) -> canon e (d + 1) acc + | SortLevel (SLlub (e1, e2)) -> canon e1 d (canon e2 d acc) + | Var (_, i) -> let o = try VMap.find i m with Not_found -> -1 in + if o < d then (c, VMap.add i d m) else acc + | Metavar (i, _, _, _) + -> let o = try VMap.find (- i) m with Not_found -> -1 in + if o < d then (c, VMap.add (- i) d m) else acc + | _ -> (max_int, m) + in canon e 0 (0,VMap.empty) + +let level_leq (c1, m1) (c2, m2) = + c1 <= c2 + && c1 != max_int + && VMap.for_all (fun i d -> try d <= VMap.find i m2 with Not_found -> false) + m1 + +let rec mkSLlub meta_ctx ctx e1 e2 = + match (lexp_whnf e1 ctx meta_ctx, lexp_whnf e2 ctx meta_ctx) with + | (SortLevel SLz, e2) -> e2 + | (e1, SortLevel SLz) -> e1 + | (SortLevel (SLsucc e1), SortLevel (SLsucc e2)) + -> mkSortLevel (SLsucc (mkSLlub meta_ctx ctx e1 e2)) + | (e1', e2') + -> let ce1 = level_canon (L.clean meta_ctx e1') in + let ce2 = level_canon (L.clean meta_ctx e2') in + if level_leq ce1 ce2 then e1 + else if level_leq ce2 ce1 then e2 + else mkSortLevel (SLlub (e1, e2)) + +let sort_compose meta_ctx ctx l s1 s2 = match s1, s2 with - | (Stype l1, Stype l2) -> Stype (sort_level_max l1 l2) + | (Stype l1, Stype l2) -> Stype (mkSLlub meta_ctx ctx l1 l2) | ( (StypeLevel, Stype _) | (StypeLevel, StypeOmega) | (Stype _, StypeOmega)) @@ -339,16 +364,24 @@ let rec check' meta_ctx erased ctx e = | SortLevel SLz -> DB.type_level | SortLevel (SLsucc e) -> let t = check erased ctx e in + (* FIXME: Actually, we should probably have a special function to check + * that `e` is a level, so as to avoid `case` and other funny things. *) assert_type ctx e t DB.type_level; DB.type_level + | SortLevel (SLlub (e1, e2)) + -> let t1 = check erased ctx e1 in + assert_type ctx e1 t1 DB.type_level; + let t2 = check erased ctx e2 in + assert_type ctx e2 t2 DB.type_level; + DB.type_level | Sort (l, Stype e) -> let t = check erased ctx e in assert_type ctx e t DB.type_level; mkSort (l, Stype (mkSortLevel (SLsucc e))) | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) - -> (U.msg_error "TC" (lexp_location e) "Reached unreachable sort!"; - (* U.internal_error "Reached unreachable sort!"; *) + -> ((* U.msg_error "TC" (lexp_location e) "Reached unreachable sort!"; + * U.internal_error "Reached unreachable sort!"; *) DB.sort_omega) | Builtin (_, t, _) -> let _ = check_type DB.set_empty Myers.nil t in @@ -391,7 +424,7 @@ let rec check' meta_ctx erased ctx e = (* FIXME: fix scoping of `k2` and `s2`. *) -> if ak == P.Aerasable && impredicative_erase && s1 != StypeLevel then k2 - else mkSort (l, sort_compose l s1 s2) + else mkSort (l, sort_compose meta_ctx ctx l s1 s2) | (Sort (_, _), _) -> (U.msg_error "TC" (lexp_location t2) "Not a proper type"; mkSort (l, StypeOmega)) @@ -444,14 +477,14 @@ let rec check' meta_ctx erased ctx e = -> level | Sort (_, Stype level') (* FIXME: scoping of level vars! *) - -> sort_level_max level level' + -> mkSLlub meta_ctx ctx level level' | tt -> U.msg_error "TC" (lexp_location t) ("Field type " ^ lexp_string t ^ " is not a Type! (" ^ lexp_string tt ^")"); - (* DB.print_lexp_ctx ctx; - * U.internal_error "Oops"; *) + DB.print_lexp_ctx ctx; + (* U.internal_error "Oops"; *) level), DB.lctx_extend ctx v Variable t) (level, ctx)
===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -231,11 +231,11 @@ let _ = test_eval_eqv_named add = lambda x y -> (x + y);
inc1 = add 1; - inc2 = _+_ 2;" + inc2 = _-_ 5;"
"inc1 1; inc2 2; inc1 3;"
- "2; 4; 4" + "2; 3; 4"
(* * Lists
View it on GitLab: https://gitlab.com/monnier/typer/commit/49630b311b12ec5e6b3f411297e7f7817e05...
Afficher les réponses par date