Stefan pushed to branch master at Stefan / Typer

Commits: 53c41e25 by Stefan Monnier at 2016-10-05T23:16:26-04:00 Fix some context and whnf handling in `check`.

* src/debruijn.ml (lctx_extend): Change vdef arg to be an option.

* src/lparse.ml (lexp_decls_1): Fix inf-loop on structural equality. (elab_check_def): Add debug output. Don't call conv_p. (ctx_define_rec): Do check that it's properly typed.

* src/opslexp.ml (check) <Let>, <Lambda>, <Case>: Call lexp_whnf. (check) <Inductive>: Fix context computation for fields.

- - - - -

3 changed files:

- src/debruijn.ml - src/lparse.ml - src/opslexp.ml

Changes:

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -117,8 +117,8 @@ let lexp_ctx_cons (ctx : lexp_context) offset d v t = || previous_offset = 1 + offset))); M.cons (offset, d, v, t) ctx

-let lctx_extend (ctx : lexp_context) (def: vdef) (v: varbind) (t: lexp) = - lexp_ctx_cons ctx 0 (Some def) v t +let lctx_extend (ctx : lexp_context) (def: vdef option) (v: varbind) (t: lexp) = + lexp_ctx_cons ctx 0 def v t

let env_extend_rec r (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) = let (loc, name) = def in

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -98,7 +98,16 @@ let elab_check_proper_type (ctx : elab_context) ltp v =

let elab_check_def (ctx : elab_context) var lxp ltype = let lctx = ectx_to_lctx ctx in - if OL.conv_p ltype (OL.check lctx lxp) then + let ltype' = try OL.check lctx lxp + with e -> + print_string "Error while type-checking:\n"; + lexp_print lxp; + print_string "\nIn context:\n"; + print_lexp_ctx (ectx_to_lctx ctx); + raise e in + (* FIXME: conv_p fails too often, e.g. it fails to see that `Type` is + * convertible to `Type_0`, because it doesn't have access to lctx. *) + if true (* OL.conv_p ltype ltype' *) then elab_check_proper_type ctx ltype var else (print_string "¡¡ctx_define error!!\n"; @@ -124,15 +133,12 @@ let ctx_define_rec (ctx: elab_context) decls = n - 1) (List.length decls) decls in - (* FIXME: conv_p fails too often, e.g. it fails to see that `Type` is - * convertible to `Type_0`, because it doesn't have access to lctx. - * - * let _ = List.fold_left (fun n (var, lxp, ltp) - * -> elab_check_def nctx var lxp - * (push_susp ltp (S.shift n)); - * n - 1) - * (List.length decls) - * decls in *) + let _ = List.fold_left (fun n (var, lxp, ltp) + -> elab_check_def nctx var lxp + (push_susp ltp (S.shift n)); + n - 1) + (List.length decls) + decls in nctx

(* The main job of lexp (currently) is to determine variable name (index)

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -181,7 +181,9 @@ let rec lexp_whnf e (ctx : DB.lexp_context) = match e with

let assert_type e t t' = - if conv_p t t' then () + (* FIXME: conv_p is not up to the task yet: it needs to take the ctx + * into account! *) + if true (* conv_p t t' *) then () else U.msg_error "TC" (lexp_location e) "Type mismatch"; ()

let rec sort_level_max l1 l2 = match nosusp l1, nosusp l2 with @@ -232,11 +234,11 @@ let rec check ctx e = | Let (_, defs, e) -> let tmp_ctx = List.fold_left (fun ctx (v, e, t) - -> (match check ctx t with + -> (match lexp_whnf (check ctx t) ctx with | Sort (_, Stype _) -> () | _ -> (U.msg_error "TC" (lexp_location t) "Def type is not a type!"; ())); - DB.lctx_extend ctx v ForwardRef t) + DB.lctx_extend ctx (Some v) ForwardRef t) ctx defs in let _ = List.fold_left (fun n (v, e, t) -> assert_type e (push_susp t (S.shift n)) @@ -260,14 +262,14 @@ let rec check ctx e = "Not a proper type"; Sort (l, StypeOmega))) | Lambda (ak, ((l,_) as v), t, e) - -> ((match check ctx t with + -> ((match lexp_whnf (check ctx t) ctx with | Sort _ -> () | _ -> (U.msg_error "TC" (lexp_location t) "Formal arg type is not a type!"; ())); Arrow (ak, Some v, t, l, (* FIXME: If ak is Aerasable, make sure the var only appears * in type annotations. *) - check (DB.lctx_extend ctx v Variable t) e)) + check (DB.lctx_extend ctx (Some v) Variable t) e)) | Call (f, args) -> let ft = check ctx f in List.fold_left (fun ft (ak,arg) @@ -292,28 +294,31 @@ let rec check ctx e = -> let level = SMap.fold (fun _ case level -> - List.fold_left - (fun level (ak, _, t) -> - if ak == P.Aerasable && impredicative_erase - then level - else match lexp_whnf (check ctx t) ctx with - | Sort (_, Stype level') - (* FIXME: scoping of level vars! *) - -> sort_level_max level level' - | tt -> U.msg_error "TC" (lexp_location t) - ("Field type " - ^ lexp_to_str t - ^ " is not a Type! (" - ^ lexp_to_str tt ^")"); - DB.print_lexp_ctx ctx; - SortLevel SLz) - level - case) + let level, _ = + List.fold_left + (fun (level, ctx) (ak, v, t) -> + (if ak == P.Aerasable && impredicative_erase + then level + else match lexp_whnf (check ctx t) ctx with + | Sort (_, Stype level') + (* FIXME: scoping of level vars! *) + -> sort_level_max level level' + | tt -> U.msg_error "TC" (lexp_location t) + ("Field type " + ^ lexp_to_str t + ^ " is not a Type! (" + ^ lexp_to_str tt ^")"); + DB.print_lexp_ctx ctx; + SortLevel SLz), + DB.lctx_extend ctx v Variable t) + (level, ctx) + case in + level) cases (SortLevel SLz) in Sort (l, Stype level) | (ak, v, t)::args -> Arrow (ak, Some v, t, lexp_location t, - arg_loop args (DB.lctx_extend ctx v Variable t)) in + arg_loop args (DB.lctx_extend ctx (Some v) Variable t)) in let tct = arg_loop args ctx in tct | Case (l, e, it, ret, branches, default) @@ -321,7 +326,7 @@ let rec check ctx e = match e with | Call (f, args) -> let (f',args') = call_split f in (f', args' @ args) | _ -> (e,[]) in - (match call_split (check ctx e) with + (match call_split (lexp_whnf (check ctx e) ctx) with | Inductive (_, _, fargs, constructors), aargs -> let rec mksubst s fargs aargs = match fargs, aargs with

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