Stefan pushed to branch master at Stefan / Typer
Commits: 916549b4 by Stefan Monnier at 2016-12-06T23:19:43-05:00 Infer the inductive type of pattern constructors
* src/lparse.ml (check_case.add_branch): Unify rather than test inductive type of the pattern. (infer_call): Use get_type.
* src/opslexp.ml (get_type): New function.
* tests/eval_test.ml ("Generic-typed case"): New test.
* tests/macro_test.ml: Remove redundant explicit type args.
- - - - -
4 changed files:
- src/lparse.ml - src/opslexp.ml - tests/eval_test.ml - tests/macro_test.ml
Changes:
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -559,15 +559,17 @@ and check_case rtype (loc, target, ppatterns) ctx =
let add_branch pctor pargs = let loc = pexp_location pctor in - let lctor, _ = infer pctor ctx in + let lctor, ct = infer pctor ctx in let meta_ctx, _ = !global_substitution in match OL.lexp_whnf lctor (ectx_to_lctx ctx) meta_ctx with | Cons (it', (_, cons_name)) - -> let _ = if OL.conv_p meta_ctx (ectx_to_lctx ctx) it' it then () - else lexp_error loc lctor - ("Expected pattern of type `" - ^ lexp_string it ^ "` but got `" - ^ lexp_string it' ^ "`") in + -> let _ = match Unif.unify it' it (ectx_to_lctx ctx) meta_ctx with + | (None | Some (_, _::_)) + -> lexp_error loc lctor + ("Expected pattern of type `" + ^ lexp_string it ^ "` but got `" + ^ lexp_string it' ^ "`") + | Some subst -> global_substitution := subst in let _ = check_uniqueness pat cons_name lbranches in let cargs = try SMap.find cons_name constructors @@ -641,6 +643,8 @@ and check_case rtype (loc, target, ppatterns) ctx = let lexp = check pexp rtype' nctx in SMap.add cons_name (loc, fargs, lexp) lbranches, dflt + (* FIXME: is `ct` is Special-Form or Macro, pass pargs to it + * and try again with the result. *) | _ -> lexp_error loc lctor "Not a constructor"; lbranches, dflt in
@@ -778,9 +782,7 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = * expensive: a complexity of O(N²) for t₁ → t₂ ... → tₙ. *) let e = (get_special_form loc name) ctx loc sargs in let meta_ctx, _ = !global_substitution in - (* FIXME: We don't actually need to typecheck `e`, we just need - * to find its type. *) - (e, OL.check meta_ctx (ectx_to_lctx ctx) e) + (e, OL.get_type meta_ctx (ectx_to_lctx ctx) e)
| _ -> lexp_error loc body ("Unknown special-form: " ^ lexp_string body);
===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -689,6 +689,115 @@ let rec fv (e : lexp) : (DB.set * mv_set) = LMap.add fv_memo e r; r
+(** Finding the type of a expression. **) +(* This should never signal any warning/error. *) + +let rec get_type meta_ctx ctx e = + let get_type = get_type meta_ctx in + match e with + | Imm (Float (_, _)) -> DB.type_float + | Imm (Integer (_, _)) -> DB.type_int + | Imm (String (_, _)) -> DB.type_string + | Imm (Epsilon | Block (_, _, _) | Symbol _ | Node (_, _)) -> DB.type_int + | Builtin (_, t, _) -> t + | SortLevel _ -> DB.type_level + | Sort (l, Stype e) -> mkSort (l, Stype (mkSortLevel (SLsucc e))) + | Sort (_, StypeLevel) -> DB.sort_omega + | Sort (_, StypeOmega) -> DB.sort_omega + | Var (((_, name), idx) as v) -> lookup_type ctx v + | Susp (e, s) -> get_type ctx (push_susp e s) + | Let (l, defs, e) + -> let nctx = DB.lctx_extend_rec ctx defs in + mkSusp (get_type nctx e) (lexp_defs_subst l S.identity defs) + | Arrow (ak, v, t1, l, t2) + (* FIXME: Use `check` here but silencing errors? *) + -> (let k1 = get_type ctx t1 in + let nctx = DB.lexp_ctx_cons ctx 0 v Variable t1 in + (* BEWARE! `k2` can refer to `v`, but this should only happen + * if `v` is a TypeLevel, and in that case sort_compose + * should ignore `k2` and return TypeOmega anyway. *) + let k2 = get_type nctx t2 in + let k2 = mkSusp k2 (S.substitute impossible) in + match lexp_whnf k1 ctx meta_ctx, lexp_whnf k2 ctx meta_ctx with + | (Sort (_, s1), Sort (_, s2)) + -> if ak == P.Aerasable && impredicative_erase && s1 != StypeLevel + then k2 + else mkSort (l, sort_compose meta_ctx ctx l s1 s2) + | _ -> DB.type0) + | Lambda (ak, ((l,_) as v), t, e) + -> (mkArrow (ak, Some v, t, l, + get_type (DB.lctx_extend ctx (Some v) Variable t) + e)) + | Call (f, args) + -> let ft = get_type ctx f in + List.fold_left + (fun ft (ak,arg) + -> match lexp_whnf ft ctx meta_ctx with + | Arrow (ak', v, t1, l, t2) + -> mkSusp t2 (S.substitute arg) + | _ -> ft) + ft args + | Inductive (l, label, args, cases) + (* FIXME: Use `check` here but silencing errors? *) + -> let rec arg_loop args ctx = + match args with + | [] + -> let level + = SMap.fold + (fun _ case level -> + let level, _ = + List.fold_left + (fun (level, ctx) (ak, v, t) -> + (match lexp_whnf (get_type ctx t) + ctx meta_ctx with + | Sort (_, Stype _) + when ak == P.Aerasable && impredicative_erase + -> level + | Sort (_, Stype level') + (* FIXME: scoping of level vars! *) + -> mkSLlub meta_ctx ctx level level' + | tt -> level), + DB.lctx_extend ctx v Variable t) + (level, ctx) + case in + level) + cases (mkSortLevel SLz) in + mkSort (l, Stype level) + | (ak, v, t)::args + -> mkArrow (ak, Some v, t, lexp_location t, + arg_loop args (DB.lctx_extend ctx (Some v) Variable t)) in + let tct = arg_loop args ctx in + tct + | Case (l, e, ret, branches, default) -> ret + | Cons (t, (l, name)) + -> (match lexp_whnf t ctx meta_ctx with + | Inductive (l, _, fargs, constructors) + -> (try + let fieldtypes = SMap.find name constructors in + let rec indtype fargs start_index = + match fargs with + | [] -> [] + | (ak, vd, _)::fargs -> (ak, Var (vd, start_index)) + :: indtype fargs (start_index - 1) in + let rec fieldargs ftypes = + match ftypes with + | [] -> let nargs = List.length fieldtypes + List.length fargs in + mkCall (mkSusp t (S.shift nargs), + indtype fargs (nargs - 1)) + | (ak, vd, ftype) :: ftypes + -> mkArrow (ak, vd, ftype, lexp_location ftype, + fieldargs ftypes) in + let rec buildtype fargs = + match fargs with + | [] -> fieldargs fieldtypes + | (ak, ((l,_) as vd), atype) :: fargs + -> mkArrow (P.Aerasable, Some vd, atype, l, + buildtype fargs) in + buildtype fargs + with Not_found -> DB.type_int) + | _ -> DB.type_int) + | Metavar (idx, s, _, t) -> t + (*********** Type erasure, before evaluation. *****************)
let rec erase_type (lxp: L.lexp): E.elexp =
===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -365,6 +365,20 @@ let _ = test_eval_eqv_named "f Eq_refl 3" "3"
+let _ = test_eval_eqv_named + "Generic-typed case" + + "P = (a : Type) ≡> a -> Not (Not a); + p : P; + p = lambda a ≡> lambda x notx -> notx x; + tP : Decidable P; + tP = (datacons Decidable true) (prop := P) (p := p);" + + "case tP + | (datacons ? true) (p := _) => 3 + | (datacons ? false) (p := _) => 4;" + "3;" + (* run all tests *) let _ = run_all ()
===================================== tests/macro_test.ml ===================================== --- a/tests/macro_test.ml +++ b/tests/macro_test.ml @@ -51,8 +51,7 @@ let _ = (add_test "MACROS" "macros base" (fun () -> | cons hd tl => hd | nil => symbol_ "x") : Sexp in (node_ (symbol_ "_*_") - (cons (a := Sexp) hd - (cons (a := Sexp) hd (nil (a := Sexp))))); + (cons hd (cons hd nil)));
sqr = Macro_ my_fun; " in @@ -72,10 +71,10 @@ let _ = (add_test "MACROS" "macros base" (fun () -> let _ = (add_test "MACROS" "macros decls" (fun () -> let dcode = " decls-impl = lambda (x : List Sexp) -> - cons(a := Sexp) (node_ (symbol_ "_=_") - (cons(a := Sexp) (symbol_ "a") (cons(a := Sexp) (integer_ 1) (nil(a := Sexp))))) - (cons(a := Sexp) (node_ (symbol_ "_=_") - (cons(a := Sexp) (symbol_ "b") (cons(a := Sexp) (integer_ 2) (nil(a := Sexp))))) (nil(a := Sexp))); + cons (node_ (symbol_ "_=_") + (cons (symbol_ "a") (cons (integer_ 1) nil))) + (cons (node_ (symbol_ "_=_") + (cons (symbol_ "b") (cons (integer_ 2) nil))) nil);
my-decls = DMacro_ decls-impl;
View it on GitLab: https://gitlab.com/monnier/typer/commit/916549b4223a216e5974e9be66a5cba1effe...
Afficher les réponses par date