Stefan pushed to branch unification at Stefan / Typer

Commits: e134b211 by Stefan Monnier at 2016-10-04T21:04:33-04:00 * src/eval.ml (from_lctx): Rewrite to obey the db_offset

* src/debruijn.ml (lexp_ctx_cons): Tighten the check.

* src/env.ml (value_type): Use runtime_env. (runtime_env): Drop the extra two integers. (env_cell): Make the var's name immutable. (get_rte_variable, get_rte_size, add_rte_variable, print_rte_ctx): Adjust accordingly. (set_rte_variable): Adjust and make return type be unit. (get_rte_size, is_free_var, rte_shift): Remove.

* src/myers.ml (fold_left, fold_right, map, iteri): New functions.

* tests/env_test.ml: Don't use the return value of set_rte_variable.

- - - - - 1a68cffc by Stefan Monnier at 2016-10-05T12:42:41-04:00 * src/lparse.ml (_lexp_decls): Rewrite to fix scoping issues

* src/lparse.ml (elab_check_sort, elab_check_proper_type): New functions. (elab_check_def, ctx_define_rec._): Use them to check that the types are proper types. (lexp_detect_recursive, _lexp_rec_decl): Remove. (lexp_check_decls, lexp_decls_1): New functions. (_lexp_decls): Use them instead.

* src/opslexp.ml (check) <Arrow>: Fix incorrect context for target.

* src/util.ml (IntMap): New module.

* src/debug_util.ml (lexp_detect_recursive): Move from lparse.ml.

- - - - - 0bec5cff by Stefan Monnier at 2016-10-05T15:09:46-04:00 Merge branch 'trunk' into unification

- - - - -

9 changed files:

- src/debruijn.ml - src/debug_util.ml - src/env.ml - src/eval.ml - src/lparse.ml - src/myers.ml - src/opslexp.ml - src/util.ml - tests/env_test.ml

Changes:

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -109,7 +109,12 @@ let lexp_ctx_cons (ctx : lexp_context) offset d v t = assert (offset >= 0 && (ctx = M.nil || let (previous_offset, _, _, _) = M.car ctx in - previous_offset >= 0 && previous_offset <= 1 + offset)); + previous_offset >= 0 (* General constraint. *) + (* Either `ctx` is self-standing (doesn't depend on us), + * or it depends on us (and maybe other bindings to come), in + * which case we have to depend on the exact same bindings. *) + && (previous_offset <= 1 + || previous_offset = 1 + offset))); M.cons (offset, d, v, t) ctx

let lctx_extend (ctx : lexp_context) (def: vdef) (v: varbind) (t: lexp) =

===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -215,6 +215,82 @@ let format_source () = ) else (List.iter (fun str -> print_string str; print_string "\n") result;)

+let lexp_detect_recursive pdecls = + (* Pack mutually recursive declarations *) + (* mutually recursive def must use forward declarations *) + + let decls = ref [] in + let pending = ref [] in + let merged = ref [] in + + List.iter (fun expr -> + match expr with + | Pexpr((l, s), pxp) ->( + let was_forward = (List.exists + (fun (Ldecl((_, p), _, _)) -> p = s) !pending) in + + let is_empty = (List.length !pending) = 0 in + let is_one = (List.length !pending) = 1 in + + (* This is a standard declaration: not forwarded *) + if (was_forward = false) && is_empty then( + decls := [Ldecl((l, s), Some pxp, None)]::!decls; + ) + (* This is an annotated expression + * or the last element of a mutually rec definition *) + else if (was_forward && is_one) then ( + + (* we know that names match already *) + let ptp = (match (!pending) with + | Ldecl(_, _, ptp)::[] -> ptp + (* we already checked that len(pending) == 1*) + | Ldecl(_, _, ptp)::_ -> lexp_fatal l "Unreachable" + | [] -> lexp_fatal l "Unreachable" + | Lmcall _ :: _ -> lexp_fatal l "Unreachable") in + + (* add declaration to merged decl *) + merged := Ldecl((l, s), Some pxp, ptp)::(!merged); + + (* append decls *) + decls := (List.rev !merged)::!decls; + + (* Reset State *) + pending := []; + merged := []; + ) + (* This is a mutually recursive definition *) + else ( + (* get pending element and remove it from the list *) + let elem, lst = List.partition + (fun (Ldecl((_, n), _, _)) -> n = s) !pending in + + let _ = (match elem with + (* nothing to merge *) + | [] -> + merged := Ldecl((l, s), Some pxp, None)::!merged; + + (* append new element to merged list *) + | Ldecl((l, s), _, Some ptp)::[] -> + merged := Ldecl((l, s), Some pxp, (Some ptp))::!merged; + + (* s should be unique *) + | _ -> lexp_error l "declaration must be unique") in + + (* element is not pending anymore *) + pending := lst; + )) + + | Ptype((l, s), ptp) -> + pending := Ldecl((l, s), None, Some ptp)::!pending + + (* macro will be handled later *) + | Pmcall(a, sargs) -> + decls := [Lmcall(a, sargs)]::!decls; + + ) pdecls; + + (List.rev !decls) + let main () = parse_args ();

===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -55,13 +55,17 @@ type value_type = | Vcons of symbol * value_type list | Vbuiltin of string | Vfloat of float - | Closure of string * elexp * (((string option * value_type) ref M.myers) * (int * int)) + | Closure of string * elexp * runtime_env | Vsexp of sexp (* Values passed to macros. *) (* Unable to eval during macro expansion, only throw if the value is used *) | Vdummy | Vin of in_channel | Vout of out_channel | Vcommand of (unit -> value_type) + (* Runtime Environ *) + and env_cell = (string option * (value_type ref)) + and runtime_env = env_cell M.myers +

let rec value_equal a b = @@ -138,26 +142,16 @@ let value_name v = | Vout _ -> "Vout" | Vcommand _ -> "Vcommand"

-(* Runtime Environ *) -type env_cell = (string option * value_type) ref -type runtime_env = (env_cell M.myers) * (int * int) - -let make_runtime_ctx = (M.nil, (0, 0)) - -let get_rte_size (ctx: runtime_env): int = let (l, _) = ctx in M.length l +let make_runtime_ctx = M.nil

-let is_free_var idx ctx = - let (l, (osize, _)) = ctx in - let tsize = (get_rte_size ctx) - osize in - if idx > tsize then true else false +let get_rte_size (ctx: runtime_env): int = M.length ctx

let get_rte_variable (name: string option) (idx: int) - (ctx: runtime_env): value_type = - let (l, _) = ctx in + (ctx: runtime_env): value_type = try ( - let ref_cell = (M.nth idx l) in - let (tn, x) = !ref_cell in - match (tn, name) with + let (defname, ref_cell) = (M.nth idx ctx) in + let x = !ref_cell in + match (defname, name) with | (Some n1, Some n2) -> ( if n1 = n2 then x @@ -183,36 +177,21 @@ let get_rte_variable (name: string option) (idx: int) env_error dloc ("Variable lookup failure. Var: "" ^ n ^ "" idx: " ^ (str_idx idx))

-let rte_shift vref ctx = - let (_, (osize, _)) = ctx in (* number of variable declared outside *) - let csize = get_rte_size ctx in (* current size *) - let offset = csize - osize in - Debug_fun.do_debug (fun () -> - prerr_endline (">>> offset " ^ (string_of_int offset) ^ " (" ^ (string_of_int csize)^ " - " ^ (string_of_int osize) ^ ")"); ()); - let ((loc, name), idx) = vref in - (* check if variable is free *) - let offset = if idx > offset then offset else 0 in - (* shift idx *) - idx + offset - -let add_rte_variable name (x: value_type) (ctx: runtime_env): runtime_env = - let (l, b) = ctx in - let lst = (M.cons (ref (name, x)) l) in - (lst, b) +let add_rte_variable name (x: value_type) (ctx: runtime_env) + : runtime_env = + let valcell = ref x in + M.cons (name, valcell) ctx

-let set_rte_variable idx name (lxp: value_type) ctx = - let (l, _) = ctx in - let ref_cell = (M.nth idx l) in - let (n, _) = !ref_cell in +let set_rte_variable idx name (v: value_type) (ctx : runtime_env) = + let (n, ref_cell) = (M.nth idx ctx) in

- match (n, name) with - | Some n1, Some n2 -> - if (n1 != n2) then - env_error dloc ("Variable's Name must Match: " ^ n1 ^ " vs " ^ n2) - else( - ref_cell := (name, lxp); ctx) + (match (n, name) with + | Some n1, Some n2 -> + if (n1 != n2) then + env_error dloc ("Variable's Name must Match: " ^ n1 ^ " vs " ^ n2) + | _ -> ());

- | _ -> ref_cell := (name, lxp); ctx + ref_cell := v

(* This function is used when we enter a new scope *) @@ -273,14 +252,14 @@ let print_myers_list l print_fun = print_string (make_sep '=')

let print_rte_ctx (ctx: runtime_env) = - let (l, b) = ctx in - print_myers_list l - (fun x -> - let (n, g) = !x in - let _ = + print_myers_list + ctx + (fun (n, vref) -> + let g = !vref in + let _ = match n with - | Some m -> lalign_print_string m 12; print_string " | " - | None -> print_string (make_line ' ' 12); print_string " | " in + | Some m -> lalign_print_string m 12; print_string " | " + | None -> print_string (make_line ' ' 12); print_string " | " in

- value_print g; print_string "\n") + value_print g; print_string "\n")

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -64,7 +64,7 @@ let _builtin_lookup = ref SMap.empty

(* This is an internal definition * 'i' is the recursion depth used to print the call trace *) -let rec _eval lxp ctx i: (value_type) = +let rec _eval lxp (ctx : Env.runtime_env) i: (value_type) = Debug_fun.do_debug (fun () -> prerr_endline ("[StackTrace] ------------------------------------------"); prerr_endline ("[StackTrace] let rec _eval lxp ctx i"); @@ -129,7 +129,6 @@ and eval_var ctx lxp v = ()); Debug_fun.do_debug (fun () -> prerr_endline ("index not shifted " ^ (string_of_int idx)); - prerr_endline ("index shifted " ^ (string_of_int (rte_shift v ctx))); prerr_endline ("ctx size " ^ (string_of_int (get_rte_size ctx))); () ); @@ -226,9 +225,9 @@ and _eval_decls (decls: (vdef * elexp) list) add_rte_variable (Some name) Vdummy ctx) ctx decls in

List.iteri (fun idx ((_, name), lxp) -> - let lxp = _eval lxp nctx (i + 1) in + let v = _eval lxp nctx (i + 1) in let offset = n - idx in - ignore (set_rte_variable offset (Some name) lxp nctx)) decls; + ignore (set_rte_variable offset (Some name) v nctx)) decls;

nctx and eval_decls_toplevel (decls: (vdef * elexp) list list) ctx = @@ -408,34 +407,44 @@ let eval_all lxps rctx silent = List.map (fun g -> evalfun g rctx) lxps

-let maybe s = match s with Some v -> v | _ -> "" - -(* build a rctx from a lctx, rm is used to ignore the last 'rm' elements *) -let from_lctx (ctx: elab_context) rm: runtime_env = - let ((n, _), env, _) = ctx in - let n = n - 1 in - let rctx = ref make_runtime_ctx in - - (* FIXME: Why not use Myers.map (Myers.nthcdr) ? *) - for i = 0 to (n - rm) do - let name, exp = match (Myers.nth (n - i) env) with - | (_, Some (_, name), LetDef exp, _) -> Some name, Some exp - | (_, Some (_, name), _, _) -> Some name, None - | _ -> None, None in - - let vxp = match exp with - | Some lxp -> - let octx = add_rte_variable name Vdummy (!rctx) in - let lxp = (OL.erase_type lxp) in - (try (eval lxp octx) - with e -> elexp_print lxp; - print_string "\n"; raise e) - - (* Happen once *) - | None -> eval_warning dloc ("Unable to eval expr: " ^ (maybe name)); - Vdummy in - - rctx := add_rte_variable name vxp (!rctx) - done; - - !rctx +let varname s = match s with Some (_, v) -> v | _ -> "<anon>" + +(* build a rctx from a lctx. *) +let from_lctx (ctx: elab_context): runtime_env = + let (_, lctx, _) = ctx in + let rctx : runtime_env + = M.map (fun (_, oname, _, _) + -> (match (oname : symbol option) with + | Some (_, name) -> Some name + | _ -> None), + ref Vdummy) + lctx in + + (* Then fill each slot in turn. *) + let _, evals + = M.fold_left + (fun (i, evals) (o, oname, def, _) + -> match def with + | LetDef lxp + -> (let elxp = OL.erase_type lxp in + let (_, valcell) = M.nth i rctx in + let octx = M.nthcdr (i - o + 1) rctx in + (i + 1, (valcell, elxp, octx) :: evals)) + | _ + (* FIXME: We should stop right here if this variable is + * actually used (e.g. if this type's variable is ∀t.t). *) + -> eval_warning dloc ("No definition to compute the value of `" + ^ varname oname ^ "`"); + (i + 1, evals)) + (0, []) lctx in + (* The evaluations have to be done "from the end of the list". *) + List.iter (fun (valcell, elxp, octx) + -> try valcell := eval elxp octx + with e -> (* print_lexp_ctx (ectx_to_lctx ctx); *) + print_string "eval-in-from_lctx failed on: "; + (* lexp_print lxp; print_string "\nerased to: "; *) + elexp_print elxp; + print_string "\n"; raise e) + evals; + + rctx

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -77,33 +77,54 @@ type mdecl = | Ldecl of symbol * pexp option * pexp option | Lmcall of symbol * sexp list

-let elab_check_def (ctx : lexp_context) var lxp ltype = - if OL.conv_p ltype (OL.check ctx lxp) then - () (* FIXME: Check ltype as well! *) + +let elab_check_sort (ctx : elab_context) lsort (l, name) ltp = + match OL.lexp_whnf lsort (ectx_to_lctx ctx) VMap.empty with + | Sort (_, _) -> () (* All clear! *) + | _ -> lexp_error l ("Type of `" ^ name ^ "` is not a proper type: " + ^ lexp_to_str ltp) + +let elab_check_proper_type (ctx : elab_context) ltp v = + try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) v ltp + with e -> print_string ("Exception while checking type `" + ^ lexp_to_str ltp ^ "` of var `" ^ + (let (_, name) = v in name) ^"`\n"); + print_lexp_ctx (ectx_to_lctx ctx); + raise e + +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 + elab_check_proper_type ctx ltype var else (print_string "¡¡ctx_define error!!\n"; lexp_print lxp; print_string " !: "; lexp_print ltype; print_string "\nbecause\n"; - lexp_print (OL.check ctx lxp); + lexp_print (OL.check lctx lxp); print_string " != "; lexp_print ltype; print_string "\n"; lexp_fatal (let (l,_) = var in l) "TC error")

let ctx_define (ctx: elab_context) var lxp ltype = - elab_check_def (ectx_to_lctx ctx) var lxp ltype; + elab_check_def ctx var lxp ltype; env_extend ctx var (LetDef lxp) ltype

let ctx_define_rec (ctx: elab_context) decls = let nctx = ectx_extend_rec ctx decls in + let _ = List.fold_left (fun n (var, lxp, ltp) + -> elab_check_proper_type + nctx (push_susp ltp (S.shift n)) var; + 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 nlctx = ectx_to_lctx nctx in * let _ = List.fold_left (fun n (var, lxp, ltp) - * -> elab_check_def nlctx var lxp + * -> elab_check_def nctx var lxp * (push_susp ltp (S.shift n)); * n - 1) * (List.length decls) @@ -560,7 +581,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = let args = [(Aexplicit, body); (Aexplicit, (olist2tlist_lexp sargs ctx))] in let macro = Call(macro_expand, args) in let emacro = OL.erase_type macro in - let rctx = (from_lctx ctx 0) in + let rctx = from_lctx ctx in

_global_eval_trace := [];

@@ -787,7 +808,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = let arg = olist2tlist_lexp sargs ctx in let lxp = Call(lxp, [(Aexplicit, arg)]) in let elexp = OL.erase_type lxp in - let rctx = (from_lctx ctx 0) in + let rctx = from_lctx ctx in

(* get a list of declaration *) let decls = eval elexp rctx in @@ -810,154 +831,94 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = (* Parse let declaration *) and lexp_p_decls decls ctx = _lexp_decls decls ctx 0

-and lexp_detect_recursive pdecls = - (* Pack mutually recursive declarations *) - (* mutually recursive def must use forward declarations *) - - let decls = ref [] in - let pending = ref [] in - let merged = ref [] in - - List.iter (fun expr -> - match expr with - | Pexpr((l, s), pxp) ->( - let was_forward = (List.exists - (fun (Ldecl((_, p), _, _)) -> p = s) !pending) in - - let is_empty = (List.length !pending) = 0 in - let is_one = (List.length !pending) = 1 in - - (* This is a standard declaration: not forwarded *) - if (was_forward = false) && is_empty then( - decls := [Ldecl((l, s), Some pxp, None)]::!decls; - ) - (* This is an annotated expression - * or the last element of a mutually rec definition *) - else if (was_forward && is_one) then ( - - (* we know that names match already *) - let ptp = (match (!pending) with - | Ldecl(_, _, ptp)::[] -> ptp - (* we already checked that len(pending) == 1*) - | Ldecl(_, _, ptp)::_ -> lexp_fatal l "Unreachable" - | [] -> lexp_fatal l "Unreachable" - | Lmcall _ :: _ -> lexp_fatal l "Unreachable") in - - (* add declaration to merged decl *) - merged := Ldecl((l, s), Some pxp, ptp)::(!merged); - - (* append decls *) - decls := (List.rev !merged)::!decls; - - (* Reset State *) - pending := []; - merged := []; - ) - (* This is a mutually recursive definition *) - else ( - (* get pending element and remove it from the list *) - let elem, lst = List.partition - (fun (Ldecl((_, n), _, _)) -> n = s) !pending in - - let _ = (match elem with - (* nothing to merge *) - | [] -> - merged := Ldecl((l, s), Some pxp, None)::!merged; - - (* append new element to merged list *) - | Ldecl((l, s), _, Some ptp)::[] -> - merged := Ldecl((l, s), Some pxp, (Some ptp))::!merged; - - (* s should be unique *) - | _ -> lexp_error l "declaration must be unique") in - - (* element is not pending anymore *) - pending := lst; - )) - - | Ptype((l, s), ptp) -> - pending := Ldecl((l, s), None, Some ptp)::!pending - - (* macro will be handled later *) - | Pmcall(a, sargs) -> - decls := [Lmcall(a, sargs)]::!decls; - - ) pdecls; - - (List.rev !decls) - - -and _lexp_decls decls ctx i: ((vdef * lexp * ltype) list list * elab_context) = - (* detect mutually recursive def and merge definition *) - let decls = lexp_detect_recursive decls in - let all = ref [] in - - let ctx = List.fold_left (fun ctx decl -> - match decl with - (* Special case *) - | [Lmcall ((l, s), sargs)] -> - (* get pexp decls *) - let pdecls, ctx = lexp_decls_macro (l, s) sargs ctx in - let decls, ctx = _lexp_decls pdecls ctx i in - all := (List.append (List.rev decls) !all); - ctx - - | _ -> - let d, ctx = _lexp_rec_decl decl ctx i in - all := d::!all; - ctx) ctx decls in - - (List.rev !all), ctx - -and _lexp_rec_decl decls ctx i = - (* parse a group of mutually recursive definitions - * i.e let decl parsing *) - - (* to compute recursive offset *) - let lst = ref [] in - - (* add all elements to the environment *) - let tctx = List.fold_left (fun vctx decl -> - match decl with - | Ldecl((l, s), _, None) -> - env_extend vctx (l, s) ForwardRef dltype - - | Ldecl((l, s), _, Some ptp) -> - let ltp, _ = lexp_p_infer ptp vctx in - env_extend vctx (l, s) ForwardRef ltp - - | Lmcall _ -> - lexp_fatal dloc "use lexp_decl_macro to parse macro decls") ctx decls in - - (* ectx_extend_rec (ctx: elab_context) (defs: (vdef * lexp * ltype) list) *) - let i = ref (1 + List.length decls) in - let ctx = List.fold_left (fun vctx decl -> - i := !i - 1; - match decl with - (* +1 because we allow each definition to be recursive *) - (* lexp infer *) - | Ldecl ((l, s), Some pxp, None) -> - let lxp, ltp = lexp_p_infer pxp tctx in - lst := ((l, s), lxp, ltp)::!lst; - (env_extend_rec (!i) vctx (l, s) (LetDef lxp) ltp) - - (* lexp check *) - | Ldecl ((l, s), Some pxp, Some ptp) -> - let ltp, _ = lexp_p_infer ptp tctx in - let lxp = lexp_p_check pxp ltp tctx in - lst := ((l, s), lxp, ltp)::!lst; - (env_extend_rec (!i) vctx (l, s) (LetDef lxp) ltp) - - (* macros *) - | Lmcall (a, sargs) -> - lexp_fatal dloc "use lexp_decl_macro to parse macro decls" - - (* unused arg *) - | Ldecl ((l, s), None, _) -> - lexp_error l ("Variable "" ^ s ^ "" is unused!"); - vctx) ctx decls in - - (List.rev !lst), ctx +and lexp_check_decls (ectx : elab_context) (* External context. *) + (nctx : elab_context) (* Context with type declarations. *) + (defs : (vdef * pexp * ltype) list) + : (vdef * lexp * ltype) list * elab_context = + let declmap = List.fold_right + (fun ((_, vname) as v, pexp, ltp) map -> + let i = senv_lookup vname nctx in + let adjusted_ltp = push_susp ltp (S.shift (i + 1)) in + IntMap.add i (v, lexp_p_check pexp adjusted_ltp nctx, ltp) + map) + defs IntMap.empty in + let decls = List.rev (List.map (fun (_, d) -> d) (IntMap.bindings declmap)) in + decls, ctx_define_rec ectx decls + + +and lexp_decls_1 + (pdecls : pdecl list) + (ectx : elab_context) (* External ctx. *) + (nctx : elab_context) (* New context. *) + (pending_decls : (location * ltype) SMap.t) (* Pending type decls. *) + (pending_defs : (vdef * pexp * ltype) list) (* Pending definitions. *) + : (vdef * lexp * ltype) list * pdecl list * elab_context = + match pdecls with + | [] -> (if not (SMap.is_empty pending_decls) then + let (s, (l, _)) = SMap.choose pending_decls in + lexp_error l ("Variable `" ^ s ^ "` declared but not defined!") + else + assert (pending_defs == [])); + [], [], nctx + + | Ptype ((l, vname) as v, ptp) :: pdecls + -> let (ltp, lsort) = lexp_p_infer ptp nctx in + if SMap.mem vname pending_decls then + (lexp_error l ("Variable `" ^ vname ^ "` declared twice!"); + lexp_decls_1 pdecls ectx nctx pending_decls pending_defs) + else if List.exists (fun ((_, vname'), _, _) -> vname = vname') + pending_defs then + (lexp_error l ("Variable `" ^ vname ^ "` already defined!"); + lexp_decls_1 pdecls ectx nctx pending_decls pending_defs) + else (elab_check_sort nctx lsort v ltp; + lexp_decls_1 pdecls ectx + (env_extend nctx v ForwardRef ltp) + (SMap.add vname (l, ltp) pending_decls) + pending_defs) + + | Pexpr ((l, vname) as v, pexp) :: pdecls + when SMap.is_empty pending_decls + -> assert (pending_defs == []); + assert (ectx == nctx); + let (lexp, ltp) = lexp_p_infer pexp nctx in + (* Lexp decls are always recursive, so we have to shift by 1 to account + * for the extra var (ourselves). *) + [(v, push_susp lexp (S.shift 1), ltp)], pdecls, + env_extend nctx v (LetDef lexp) ltp + + | Pexpr ((l, vname) as v, pexp) :: pdecls + -> (try let (_, ltp) = SMap.find vname pending_decls in + let pending_decls = SMap.remove vname pending_decls in + let pending_defs = ((v, pexp, ltp) :: pending_defs) in + if SMap.is_empty pending_decls then + let decls, nctx = lexp_check_decls ectx nctx pending_defs in + decls, pdecls, nctx + else + lexp_decls_1 pdecls ectx nctx pending_decls pending_defs + + with Not_found -> + lexp_error l ("`" ^ vname ^ "` defined but not declared!"); + lexp_decls_1 pdecls ectx nctx pending_decls pending_defs) + + | Pmcall ((l, _) as v, sargs) :: pdecls + -> let pdecls', nctx' = lexp_decls_macro v sargs nctx in + if nctx = nctx' then + (* Plain macro expansion! *) + lexp_decls_1 (List.append pdecls' pdecls) ectx nctx + pending_decls pending_defs + else if ectx = nctx then + (assert (SMap.is_empty pending_decls); + assert (pending_defs = []); + lexp_decls_1 (List.append pdecls' pdecls) ectx nctx' + pending_decls pending_defs) + else lexp_fatal l "Context changed in already changed context" + + +and _lexp_decls pdecls ctx i: ((vdef * lexp * ltype) list list * elab_context) = + if pdecls = [] then [], ctx else + let decls, pdecls, nctx = lexp_decls_1 pdecls ctx ctx SMap.empty [] in + let declss, nnctx = _lexp_decls pdecls nctx i in + decls :: declss, nnctx

and lexp_decls_toplevel decls ctx = _lexp_decls decls ctx 1

===================================== src/myers.ml ===================================== --- a/src/myers.ml +++ b/src/myers.ml @@ -112,3 +112,15 @@ let rec findcdr p l = | Mcons (x, _, _, _) when p x -> last | Mcons (_, l1, _, l2) -> findcdr2 (Some l) l1 l2 in findcdr1 None l + +let rec fold_left f i l = match l with + | Mnil -> i + | Mcons (x, l, _, _) -> fold_left f (f i x) l + +let rec fold_right f l i = match l with + | Mnil -> i + | Mcons (x, l, _, _) -> f x (fold_right f l i) + +let map f l = fold_right (fun x l' -> cons (f x) l') l nil + +let iteri f l = fold_left (fun i x -> f i x; i + 1) 0 l

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -257,8 +257,9 @@ let rec check ctx e = check new_ctx e | Arrow (ak, v, t1, l, t2) -> (let k1 = check ctx t1 in - let k2 = check (DB.lexp_ctx_cons ctx 0 v Variable t1) t2 in - match k1, k2 with + let nctx = DB.lexp_ctx_cons ctx 0 v Variable t1 in + let k2 = check nctx t2 in + match lexp_whnf k1 ctx VMap.empty, lexp_whnf k2 nctx VMap.empty with | (Sort (_, s1), Sort (_, s2)) -> if ak == P.Aerasable && impredicative_erase then k2 else Sort (l, sort_compose l s1 s2)

===================================== src/util.ml ===================================== --- a/src/util.ml +++ b/src/util.ml @@ -1,4 +1,4 @@ -(* util.ml --- Misc definitions for Typer. +(* util.ml --- Misc definitions for Typer. -*- coding: utf-8 -*-

Copyright (C) 2011-2013, 2016 Free Software Foundation, Inc.

@@ -22,6 +22,8 @@ this program. If not, see http://www.gnu.org/licenses/. *)

module SMap = Map.Make (struct type t = string let compare = String.compare end) +module IntMap + = Map.Make (struct type t = int let compare = compare end)

type charpos = int type bytepos = int @@ -70,8 +72,8 @@ let typer_unreachable s = raise (Unreachable_error s) * | [X] Fatal SECTION [ln 12, cl 12: FILE.typer] * | >> typer_dump = something; * | >> - * | >> My Error message is on multiple line - * | >> multiple line + * | >> My Error message is on multiple line + * | >> multiple line * | ------------------------------------------------ *)

===================================== tests/env_test.ml ===================================== --- a/tests/env_test.ml +++ b/tests/env_test.ml @@ -61,9 +61,11 @@ let _ = (add_test "ENV" "Set Variables" (fun () ->

print_rte_ctx rctx;

- let rctx, _ = List.fold_left (fun (ctx, idx) (n, _, v) -> - ((set_rte_variable idx n (Vdummy) ctx), idx - 1)) - (rctx, n) var in + let rctx, _ = List.fold_left + (fun (ctx, idx) (n, _, v) -> + (set_rte_variable idx n (Vdummy) ctx); + (ctx, idx - 1)) + (rctx, n) var in

print_rte_ctx rctx;

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