Stefan pushed to branch unification at Stefan / Typer

Commits: cf261607 by Stefan Monnier at 2016-10-29T20:18:55-04:00 * src/opslexp.ml (lexp_defs_subst): Fix definition

* src/lparse.ml (elab_check_sort): Improve error message. (elab_check_def): Use better location in error message. (build_var): Remove. (_lexp_p_infer): Improve error message.

- - - - - aaad384e by Stefan Monnier at 2016-11-01T13:12:13-04:00 Merge branch 'trunk' into unification

- - - - -

3 changed files:

- src/lparse.ml - src/opslexp.ml - tests/eval_test.ml

Changes:

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -99,13 +99,14 @@ let elab_check_sort (ctx : elab_context) lsort var ltp = let meta_ctx, _ = !global_substitution in match OL.lexp_whnf lsort (ectx_to_lctx ctx) meta_ctx with | Sort (_, _) -> () (* All clear! *) - | _ -> match var with + | _ -> let typestr = lexp_string ltp ^ " : " ^ lexp_string lsort in + match var with | None -> lexp_error (lexp_location ltp) ltp - ("`" ^ lexp_string ltp ^ "` is not a proper type") + ("`" ^ typestr ^ "` is not a proper type") | Some (l, name) -> lexp_error l ltp ("Type of `" ^ name ^ "` is not a proper type: " - ^ lexp_string 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 @@ -124,7 +125,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype =

let ltype' = try OL.check lctx lxp with e -> - lexp_error dloc lxp "Error while type-checking"; + lexp_error loc lxp "Error while type-checking"; 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 @@ -197,10 +198,6 @@ let ctx_define_rec (ctx: elab_context) decls = *)

-let build_var name ctx = - let type0_idx = senv_lookup name ctx in - Var((dloc, name), type0_idx) - let mkMetavar t = let meta = Unif.create_metavar () in let name = "__metavar" (* ^ (string_of_int meta) *) in @@ -333,7 +330,9 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = ("Constructor "" ^ cname ^ "" does not exist"); [], [])

- | lxp -> lexp_error loc lxp "Not an Inductive Type"; [], [] in + | lxp -> lexp_error loc lxp ("`" ^ lexp_string idt + ^ "` is not an inductive type"); + [], [] in

(* Build Arrow type. *) let target = if formal = [] then

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -114,10 +114,25 @@ and conv_p' (s1:lexp S.subst) (s2:lexp S.subst) e1 e2 : bool = and conv_p e1 e2 = conv_p' S.identity S.identity e1 e2

(* Extend a substitution S with a (mutually recursive) set - * of definitions DEFS. *) -let lexp_defs_subst l s defs = - List.fold_left (fun s (_, lexp, _) -> S.cons (Let (l, defs, lexp)) s) - s defs + * of definitions DEFS. + * This is rather tricky. E.g. for + * + * (x₁ = e1; x₂ = e₂) + * + * Where x₁ will be DeBuijn #1 and x₂ will be DeBruijn #0, + * we want a substitution of the form + * + * (let x₂ = e₂ in e₂) · (let x₁ = e₁; x₂ = e₂ in e₁) · Id + * + * Because we want #2 in both e₂ and e₁ to refer to the nearest variable in + * the surrouding context, but the substitution for #0 (defined here as + * `let x₂ = e₂ in e₂`) will be interpreted in the remaining context, + * which already provides "x₁". + *) +let rec lexp_defs_subst l s defs = match defs with + | [] -> s + | (_, lexp, _) :: defs' + -> lexp_defs_subst l (S.cons (Let (l, defs, lexp)) s) defs'

(* Reduce to weak head normal form. * WHNF implies:

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -91,6 +91,16 @@ let _ = test_eval_eqv_named x = let a = 1; b = 2 in I in (case x | I => c) : Int;" (* == *) "3"

+let _ = test_eval_eqv_named + "Let3" + + "c = 3; e = 1; f = 2; d = 4;" + + "let TrueProp : Type; I : TrueProp; + TrueProp = inductive_ TrueProp I; I = inductive-cons TrueProp I; + x = let a = 1; b = 2 in I + in (case x | I => c) : Int;" (* == *) "3" + (* Lambda * ------------------------ *)

View it on GitLab: https://gitlab.com/monnier/typer/compare/f4010f969534693155443e22588514b8152...