Stefan pushed to branch unification at Stefan / Typer
Commits: 794c962d by Stefan Monnier at 2016-11-08T23:16:18-05:00 * src/opslexp.ml (check): Add `meta_ctx` argument
- - - - -
3 changed files:
- src/debug_util.ml - src/lparse.ml - src/opslexp.ml
Changes:
===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -423,8 +423,9 @@ let main () =
let cctx = lctx_to_cctx ctx in (* run type check *) - List.iter (fun (_, lxp, _) -> - let _ = OL.check cctx lxp in ()) flexps; + List.iter (fun (_, lxp, _) + -> let _ = OL.check VMap.empty cctx lxp in ()) + flexps;
print_string (" " ^ (make_line '-' 76)); print_string "\n";));
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -109,7 +109,8 @@ let elab_check_sort (ctx : elab_context) lsort var ltp = ^ typestr)
let elab_check_proper_type (ctx : elab_context) ltp var = - try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) var ltp + let meta_ctx, _ = !global_substitution in + try elab_check_sort ctx (OL.check meta_ctx (ectx_to_lctx ctx) ltp) var ltp with e -> print_string "Exception while checking type `"; lexp_print ltp; (match var with @@ -123,19 +124,19 @@ let elab_check_def (ctx : elab_context) var lxp ltype = let lctx = ectx_to_lctx ctx in let loc = lexp_location lxp in
- let ltype' = try OL.check lctx lxp + let meta_ctx, _ = !global_substitution in + let ltype' = try OL.check meta_ctx lctx lxp with e -> lexp_error loc lxp "Error while type-checking"; print_lexp_ctx (ectx_to_lctx ctx); raise e in - let meta_ctx, _ = !global_substitution in if OL.conv_p meta_ctx (ectx_to_lctx ctx) ltype ltype' then elab_check_proper_type ctx ltype (Some var) else (debug_messages fatal loc "Type check error: ¡¡ctx_define error!!" [ (lexp_string lxp) ^ "!: " ^ (lexp_string ltype); " because"; - (lexp_string (OL.check lctx lxp)) ^ "!= " ^ (lexp_string ltype);]) + (lexp_string (OL.check meta_ctx lctx lxp)) ^ "!= " ^ (lexp_string ltype);])
let ctx_extend (ctx: elab_context) (var : vdef option) def ltype = elab_check_proper_type ctx ltype var;
===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -271,9 +271,8 @@ let sort_compose l s1 s2 = StypeOmega)
(* "check ctx e" should return τ when "Δ ⊢ e : τ" *) -let rec check ctx e = - (* let mustfind = assert_type e t in *) - let meta_ctx = VMap.empty in +let rec check meta_ctx ctx e = + let check = check meta_ctx in match e with | Imm (Float (_, _)) -> B.type_float | Imm (Integer (_, _)) -> B.type_int
View it on GitLab: https://gitlab.com/monnier/typer/commit/794c962d5996740e2641e9151d2abbc3e57f...