Stefan pushed to branch master at Stefan / Typer
Commits: db00a5fa by Stefan Monnier at 2016-11-11T15:59:22-05:00 Drop the `trace` arg in lparse
* src/REPL.ml (repl): Remove `%elabtrace`.
* src/debug_util.ml (main.lexps): Don't print elabtrace.
* src/eval.ml (eval_debug_info): Just use elexp rather than pexporlexp. (append_eval_trace, root_string, print_eval_result): Adjust accordingly.
* src/lparse.ml (root_string, _global_lexp_trace): Remove. (debug_message): Don't print "root string" any more. (infer): Rename from _lexp_p_infer. Drop `trace` arg. (infer_type): Rename from lexp_type_infer. (check): Rename from _lexp_p_check. Drop `trace' arg. (infer_and_check): Rename from lexp_p_infer_and_check. (check_case): Rename from lexp_case. (infer_call): Rename from lexp_call. (lexp_parse_inductive): Check that field types are indeed types. (lexp_p_decls): Rename from _lexp_decls. (lexp_decls_toplevel, print_lexp_trace, lexp_p_check, lexp_p_infer): Remove. (lexp_parse_all): Rename from _lexp_parse_all.
* src/opslexp.ml (pexporlexp): Remove type. (pol_string, pol_name): Remove.
- - - - -
6 changed files:
- src/REPL.ml - src/debug_util.ml - src/eval.ml - src/lparse.ml - src/opslexp.ml - tests/eval_test.ml
Changes:
===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -218,7 +218,6 @@ let rec repl i clxp rctx = | "%quit" | "%q" -> () | "%help" | "%h" -> (print_string _help_msg; repl clxp rctx) | "%calltrace" | "%ct" -> (print_eval_trace None; repl clxp rctx) - | "%elabtrace" | "%et" -> (print_lexp_trace None; repl clxp rctx) | "%typertrace" | "%tt" -> (print_typer_trace None; repl clxp rctx)
(* command with arguments *)
===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -392,7 +392,6 @@ let main () = let lexps, nctx = try lexp_p_decls pexps octx with e -> print_string reset; - print_lexp_trace None; raise e in print_string reset;
===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -46,7 +46,7 @@ open Printf (* IO Monad *) module OL = Opslexp
-type eval_debug_info = OL.pexporlexp list * elexp list +type eval_debug_info = elexp list * elexp list
let dloc = dummy_location let _global_eval_trace = ref ([], []) @@ -56,7 +56,7 @@ let _builtin_lookup = ref SMap.empty
let append_eval_trace trace (expr : elexp) = let (a, b) = trace in - let r = (OL.Elexp expr)::a, b in + let r = expr::a, b in _global_eval_trace := r; r
let append_typer_trace trace (expr : elexp) = @@ -95,7 +95,7 @@ let root_string () = let a, _ = !_global_eval_trace in match List.rev a with | [] -> "" - | e::_ -> OL.pol_string e + | e::_ -> elexp_string e
let debug_message error_type type_name type_string loc expr message = debug_messages error_type loc @@ -572,10 +572,7 @@ and print_trace title trace default = (* Print the trace*) print_string (Fmt.make_title title); print_string (Fmt.make_sep '-'); - let _ = List.iteri (fun i expr -> - match expr with - | OL.Pexp p -> lexp_trace i p - | OL.Elexp e -> elexp_trace i e) trace in + let _ = List.iteri elexp_trace trace in print_string (Fmt.make_sep '=')
and print_eval_trace trace =
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -64,7 +64,6 @@ let dltype = type0 let dloc = dummy_location
let _global_lexp_ctx = ref make_elab_context -let _global_lexp_trace = ref [] let _parsing_internals = ref false let btl_folder = ref "./btl/"
@@ -72,17 +71,11 @@ let warning = msg_warning "LPARSE" let error = msg_error "LPARSE" let fatal = msg_fatal "LPARSE"
-let root_string () = - match !_global_lexp_trace with - | [] -> "" - | e::_ -> OL.pol_string e - (* Print Lexp name followed by the lexp in itself, finally throw an exception *) let debug_message error_type type_name type_string loc expr message = debug_messages error_type loc message [ (type_name expr) ^ ": " ^ (type_string expr); - "Root: " ^ (root_string ()); ]
let lexp_fatal = debug_message fatal lexp_name lexp_string @@ -95,6 +88,10 @@ let value_fatal = debug_message fatal value_name value_string (* :-( *) let global_substitution = ref (empty_meta_subst, [])
+(* The prefix `elab_check_` is used for functions which do internal checking + * (i.e. errors signalled here correspond to internal errors rather than + * to errors in the user's code). *) + 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 @@ -181,20 +178,22 @@ let ctx_define_rec (ctx: elab_context) decls = * Type Inference * --------------------- *) (* Parsing a Pexp into an Lexp is really "elaboration", i.e. it needs to - * infer the types and perform macro-expansion. For won't really - * do any of that, but we can already start structuring it accordingly. + * infer the types and perform macro-expansion. * * More specifically, we do it with 2 mutually recursive functions: - * one takes a Pexp along with its expected type and return an Lexp - * of that type (hopefully), whereas the other takes a Pexp and - * infers its type (which it returns along with the Lexp). + * - `check` takes a Pexp along with its expected type and return an Lexp + * of that type (hopefully) + * - `infer` takes a Pexp and infers its type (which it returns along with + * the Lexp). * This is the idea of "bidirectional type checking", which minimizes - * the amount of "guessing" and/or annotations. Basically guessing/annotations - * is only needed at those few places where the code is not fully-normalized, - * which in normal programs is only in "let" definitions. - * So the rule of thumbs are: - * - use lexp_p_infer for destructors, and use lexp_p_check for constructors. - * - use lexp_p_check whenever you can. + * the amount of "guessing" and/or annotations. Since we infer types anyway + * it doesn't really reduce the amount of type annotations for us, but it + * reduces the amount of inference and checking, i.e. it reduces the number of + * metavars we create/instantiate/dereference as well as the number of call to + * the unification algorithm. + * Basically guessing/annotations is only needed at those few places where the + * code is not fully-normalized, which in normal programs is only in "let" + * definitions. *)
@@ -211,16 +210,13 @@ let newMetalevel () =
let newMetatype () = newMetavar (newMetalevel ())
-let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = +let rec infer (p : pexp) (ctx : elab_context): lexp * ltype =
- let trace = ((OL.Pexp p)::trace) in let tloc = pexp_location p in - let lexp_infer p ctx = _lexp_p_infer p ctx trace in
(* Save current trace in a global variable. If an error occur, we will be able to retrieve the most recent trace and context. *) _global_lexp_ctx := ctx; - _global_lexp_trace := trace;
match p with (* Block/String/Integer/Float. *) @@ -236,12 +232,12 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = (* Symbol i.e identifier. *) | Pvar (loc, name) -> (try - let idx = (senv_lookup name ctx) in - let lxp = (make_var name idx loc) in + let idx = senv_lookup name ctx in + let lxp = make_var name idx loc in
(* Search type. *) let ltp = env_lookup_type ctx ((loc, name), idx) in - lxp, ltp (* Return Macro[22] *) + lxp, ltp
with Not_found -> (pexp_error loc p ("The variable: `" ^ name ^ "` was not declared"); @@ -250,18 +246,18 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype =
(* Let, Variable declaration + local scope. *) | Plet (loc, decls, body) - -> let declss, nctx = _lexp_decls decls ctx trace in - let bdy, ltp = lexp_infer body nctx in + -> let declss, nctx = lexp_p_decls decls ctx in + let bdy, ltp = infer body nctx in let s = List.fold_left (OL.lexp_defs_subst loc) S.identity declss in - (lexp_let_decls declss bdy nctx trace), + (lexp_let_decls declss bdy nctx), mkSusp ltp s
(* ------------------------------------------------------------------ *) | Parrow (kind, ovar, tp, loc, expr) - -> let ltp = lexp_type_infer tp ctx ovar trace in + -> let ltp = infer_type tp ctx ovar in let nctx = ectx_extend ctx ovar Variable ltp in
- let lxp = lexp_type_infer expr nctx None trace in + let lxp = infer_type expr nctx None in
let v = mkArrow(kind, ovar, ltp, tloc, lxp) in v, type0 @@ -271,7 +267,7 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = (* (arg_kind * pvar * pexp option) list *) let formal = List.map (fun (kind, var, opxp) -> let ltp, _ = match opxp with - | Some pxp -> _lexp_p_infer pxp !nctx trace + | Some pxp -> infer pxp !nctx | None -> dltype, dltype in
nctx := env_extend !nctx var Variable ltp; @@ -286,25 +282,24 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = * (not always type0). *) type0 (List.rev formal) in
- let map_ctor = lexp_parse_inductive ctors nctx trace in + let map_ctor = lexp_parse_inductive ctors nctx in let v = mkInductive(tloc, label, formal, map_ctor) in v, ltp
(* This case can be inferred. *) | Plambda (kind, var, Some ptype, body) - -> let ltp, lasort = lexp_infer ptype ctx in - elab_check_sort ctx lasort (Some var) ltp; + -> let ltp = infer_type ptype ctx (Some var) in
let nctx = env_extend ctx var Variable ltp in - let lbody, lbtp = lexp_infer body nctx in + let lbody, lbtp = infer body nctx in
let lambda_type = mkArrow (kind, Some var, ltp, tloc, lbtp) in mkLambda(kind, var, ltp, lbody), lambda_type
- | Pcall (fname, _args) -> lexp_call fname _args ctx trace + | Pcall (fname, args) -> infer_call fname args ctx
| Pcons(t, sym) - -> let idt, _ = lexp_infer t ctx in + -> let idt, _ = infer t ctx in let (loc, cname) = sym in let meta_ctx, _ = !global_substitution in
@@ -351,34 +346,33 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = mkCons(idt, sym), cons_type
| Phastype (_, pxp, ptp) - -> let ltp = lexp_type_infer ptp ctx None trace in - (_lexp_p_check pxp ltp ctx trace), ltp + -> let ltp = infer_type ptp ctx None in + (check pxp ltp ctx, ltp)
| (Plambda _ | Pcase _ | Pmetavar _) -> let t = newMetatype () in - let lxp = _lexp_p_check p t ctx trace in + let lxp = check p t ctx in (lxp, t)
-and lexp_type_infer pexp ectx var trace = - let t, s = _lexp_p_infer pexp ectx trace in +and infer_type pexp ectx var = + (* We could also use lexp_check with an argument of the form + * Sort (?s), but in most cases the metavar would be allocated + * unnecessarily. *) + let t, s = infer pexp ectx in elab_check_sort ectx s var t; t
-and lexp_let_decls declss (body: lexp) ctx i = +and lexp_let_decls declss (body: lexp) ctx = List.fold_right (fun decls lxp -> mkLet (dloc, decls, lxp)) declss body
-and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = +and check (p : pexp) (t : ltype) (ctx : elab_context): lexp =
- let trace = ((OL.Pexp p)::trace) in let tloc = pexp_location p in - let lexp_infer p ctx = _lexp_p_infer p ctx trace in - let lexp_check p ltp ctx = _lexp_p_check p ltp ctx trace in
(* Safe current trace in a global variable. If an error occur, we will be able to retrieve the most recent trace and context *) _global_lexp_ctx := ctx; - _global_lexp_trace := trace;
let unify_with_arrow lxp kind var aty subst = let body = newMetatype () in @@ -406,9 +400,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = (* Check argument type annotation, if any. *) let def_arg_type = match def_arg_type with | Some def_arg_type - -> let def_arg_type, lasort = lexp_infer def_arg_type ctx in - elab_check_sort ctx lasort (Some var) def_arg_type; - Some def_arg_type + -> Some (infer_type def_arg_type ctx (Some var)) | _ -> None in
(* Read var type from the provided type *) @@ -427,7 +419,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = | lxp -> unify_with_arrow lxp kind var def_arg_type subst in
let nctx = env_extend ctx var Variable given_arg_type in - let lbody = lexp_check body given_body_type nctx in + let lbody = check body given_body_type nctx in mkLambda (kind, var, given_arg_type, lbody)
in @@ -437,17 +429,17 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = -> infer_lambda_body kind var def_arg_type body subst
| Pcase (loc, target, branches) - -> lexp_case t (loc, target, branches) ctx trace + -> check_case t (loc, target, branches) ctx
(* FIXME: Handle *macro* pcalls here! *) (* | Pcall (fname, _args) -> *)
| Pmetavar _ -> newMetavar t
- | _ -> lexp_p_infer_and_check p ctx t trace + | _ -> infer_and_check p ctx t
-and lexp_p_infer_and_check pexp ctx t i = - let (e, inferred_t) = _lexp_p_infer pexp ctx i in +and infer_and_check pexp ctx t = + let (e, inferred_t) = infer pexp ctx in let subst, _ = !global_substitution in (match Unif.unify inferred_t t (ectx_to_lctx ctx) subst with | None @@ -464,12 +456,10 @@ and lexp_p_infer_and_check pexp ctx t i = e
(* Lexp.case can sometimes be inferred, but we prefer to always check. *) -and lexp_case rtype (loc, target, ppatterns) ctx i = +and check_case rtype (loc, target, ppatterns) ctx = (* FIXME: check if case is exhaustive *) (* Helpers *)
- let lexp_infer p ctx = _lexp_p_infer p ctx i in - let pat_string p = sexp_string (pexp_u_pat p) in
let uniqueness_warn pat = @@ -481,7 +471,7 @@ and lexp_case rtype (loc, target, ppatterns) ctx i = if SMap.mem name map then uniqueness_warn pat in
(* get target and its type *) - let tlxp, tltp = lexp_infer target ctx in + let tlxp, tltp = infer target ctx in let meta_ctx, _ = !global_substitution in (* FIXME: We need to be careful with whnf: while the output is equivalent * to the input, it's not necessarily as readable. So try to reuse the @@ -507,12 +497,12 @@ and lexp_case rtype (loc, target, ppatterns) ctx i = let nctx = ctx_extend ctx v Variable tltp in let rtype' = mkSusp rtype (S.shift (M.length (ectx_to_lctx nctx) - M.length (ectx_to_lctx ctx))) in - let lexp = _lexp_p_check pexp rtype' nctx i in + let lexp = check pexp rtype' nctx in lbranches, Some (v, lexp) in
let add_branch pctor pargs = let loc = pexp_location pctor in - let lctor, _ = _lexp_p_infer pctor ctx i in + let lctor, _ = 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)) @@ -559,7 +549,7 @@ and lexp_case rtype (loc, target, ppatterns) ctx i = let rtype' = mkSusp rtype (S.shift (M.length (ectx_to_lctx nctx) - M.length (ectx_to_lctx ctx))) in - let lexp = _lexp_p_check pexp rtype' nctx i in + let lexp = check pexp rtype' nctx in SMap.add cons_name (loc, fargs, lexp) lbranches, dflt | _ -> lexp_error loc lctor "Not a constructor"; lbranches, dflt @@ -584,21 +574,18 @@ and lexp_case rtype (loc, target, ppatterns) ctx i =
mkCase (loc, tlxp, rtype, lpattern, dflt)
-(* Identify Call Type and return processed call *) -and lexp_call (func: pexp) (sargs: sexp list) ctx i = +(* Identify Call Type and return processed call. *) +and infer_call (func: pexp) (sargs: sexp list) ctx = let loc = pexp_location func in let meta_ctx, _ = !global_substitution in
- let lexp_infer p ctx = _lexp_p_infer p ctx i in - let lexp_check p ltp ctx = _lexp_p_check p ltp ctx i in - (* Vanilla : sqr is inferred and (lambda x -> x * x) is returned * Macro : sqr is returned * Constructor : a constructor is returned * Anonymous : lambda *)
(* retrieve function's body (sqr 3) sqr is a Pvar() *) - let body, ltp = lexp_infer func ctx in + let body, ltp = infer func ctx in let ltp = nosusp ltp in
let rec handle_fun_args largs sargs pending ltp = @@ -608,7 +595,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = when SMap.mem aname' pending -> let sarg = SMap.find aname' pending in let parg = pexp_parse sarg in - let larg = lexp_check parg arg_type ctx in + let larg = check parg arg_type ctx in handle_fun_args ((ak, larg) :: largs) sargs (SMap.remove aname' pending) (L.mkSusp ret_type (S.substitute larg)) @@ -629,7 +616,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = when (aname = aname' || aname = "_") (* Explicit-implicit argument. *) -> let parg = pexp_parse sarg in - let larg = lexp_check parg arg_type ctx in + let larg = check parg arg_type ctx in handle_fun_args ((ak, larg) :: largs) sargs pending (L.mkSusp ret_type (S.substitute larg))
@@ -647,7 +634,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i =
| sarg :: sargs, Arrow (Aexplicit, _, arg_type, _, ret_type) -> let parg = pexp_parse sarg in - let larg = _lexp_p_check parg arg_type ctx i in + let larg = check parg arg_type ctx in handle_fun_args ((Aexplicit, larg) :: largs) sargs pending (L.mkSusp ret_type (S.substitute larg)) | sarg :: sargs, Arrow (kind, _, arg_type, _, ret_type) @@ -674,7 +661,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i =
| true, [String (_, str); stp] -> let ptp = pexp_parse stp in - let ltp, _ = lexp_infer ptp ctx in + let ltp, _ = infer ptp ctx in Builtin((loc, str), ltp), ltp
| true, _ -> error loc "Wrong Usage of `Built-in`"; @@ -689,7 +676,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = mkCall (body, List.rev largs), ret_type in
let handle_macro_call () = - let sxp = match lexp_expand_macro body sargs ctx i with + let sxp = match lexp_expand_macro body sargs ctx with | Vsexp(sxp) -> sxp (* Those are sexp converted by the eval function *) | Vint(i) -> Integer(dloc, i) @@ -699,7 +686,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = value_fatal loc v "Macro_ expects `(List Sexp) -> Sexp`" in
let pxp = pexp_parse sxp in - lexp_infer pxp ctx in + infer pxp ctx in
(* This is the builtin Macro type *) let macro_type, macro_disp = match get_predef_option "Macro" ctx with @@ -715,7 +702,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = match macro with | Pvar(l, name) when is_builtin_macro name -> let pargs = List.map pexp_parse sargs in - let largs = _lexp_parse_all pargs ctx i in + let largs = lexp_parse_all pargs ctx in (get_macro_impl loc name) loc largs ctx ltp
(* true macro *) @@ -725,8 +712,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = | _ -> handle_funcall ()
(* Parse inductive type definition. *) -and lexp_parse_inductive ctors ctx i = - let lexp_parse p ctx = _lexp_p_infer p ctx i in +and lexp_parse_inductive ctors ctx =
let make_args (args:(arg_kind * pvar option * pexp) list) ctx : (arg_kind * vdef option * ltype) list = @@ -736,7 +722,7 @@ and lexp_parse_inductive ctors ctx i = | hd::tl -> begin match hd with | (kind, var, exp) -> - let lxp, _ = lexp_parse exp ctx in + let lxp = infer_type exp ctx var in let nctx = ectx_extend ctx var Variable dltype in loop tl ((kind, var, lxp)::acc) nctx end in @@ -749,24 +735,25 @@ and lexp_parse_inductive ctors ctx i =
(* Macro declaration handling, return a list of declarations * to be processed *) -and lexp_expand_macro macro_funct sargs ctx trace - = lexp_expand_macro_ macro_funct sargs ctx trace "expand_macro_" +and lexp_expand_macro macro_funct sargs ctx + = lexp_expand_macro_ macro_funct sargs ctx "expand_macro_"
-and lexp_expand_dmacro macro_funct sargs ctx trace - = lexp_expand_macro_ macro_funct sargs ctx trace "expand_dmacro_" +and lexp_expand_dmacro macro_funct sargs ctx + = lexp_expand_macro_ macro_funct sargs ctx "expand_dmacro_"
-and lexp_expand_macro_ macro_funct sargs ctx trace expand_fun = +and lexp_expand_macro_ macro_funct sargs ctx expand_fun =
(* Build the function to be called *) let macro_expand = get_predef expand_fun ctx in - let args = [(Aexplicit, macro_funct); (Aexplicit, (olist2tlist_lexp sargs ctx))] in + let args = [(Aexplicit, macro_funct); + (Aexplicit, (olist2tlist_lexp sargs ctx))] in
let macro = mkCall (macro_expand, args) in let emacro = OL.erase_type macro in let rctx = from_lctx ctx in
(* eval macro *) - let vxp = try _eval emacro rctx (trace, []) + let vxp = try _eval emacro rctx ([], []) with e -> print_eval_trace None; raise e in (* Return results *) (* Vint/Vstring/Vfloat might need to be converted to sexp *) @@ -792,7 +779,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = | Var((_, "add-attribute"), _) ->( (* Builtin macro *) let pargs = List.map pexp_parse sargs in - let largs = _lexp_parse_all pargs ctx [] in + let largs = lexp_parse_all pargs ctx in
(* extract info *) let var, att, fn = match largs with @@ -806,7 +793,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = [], ctx)
| _ ->( - let ret = lexp_expand_dmacro body sargs ctx [] in + let ret = lexp_expand_dmacro body sargs ctx in
(* convert typer list to ocaml *) let decls = tlist2olist [] ret in @@ -822,9 +809,6 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = with e -> fatal loc ("Macro `" ^ mname ^ "`not found")
-(* Parse let declaration *) -and lexp_p_decls decls ctx = _lexp_decls decls ctx [] - and lexp_check_decls (ectx : elab_context) (* External context. *) (nctx : elab_context) (* Context with type declarations. *) (defs : (vdef * pexp * ltype) list) @@ -833,7 +817,7 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) (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) + IntMap.add i (v, check pexp adjusted_ltp nctx, ltp) map) defs IntMap.empty in let decls = List.rev (List.map (fun (_, d) -> d) (IntMap.bindings declmap)) in @@ -857,7 +841,7 @@ and lexp_decls_1 [], [], nctx
| Ptype ((l, vname) as v, ptp) :: pdecls - -> let (ltp, lsort) = _lexp_p_infer ptp nctx [] in + -> let ltp = infer_type ptp nctx (Some v) in if SMap.mem vname pending_decls then (error l ("Variable `" ^ vname ^ "` declared twice!"); lexp_decls_1 pdecls ectx nctx pending_decls pending_defs) @@ -865,17 +849,16 @@ and lexp_decls_1 pending_defs then (error l ("Variable `" ^ vname ^ "` already defined!"); lexp_decls_1 pdecls ectx nctx pending_decls pending_defs) - else (elab_check_sort nctx lsort (Some v) ltp; - lexp_decls_1 pdecls ectx - (env_extend nctx v ForwardRef ltp) - (SMap.add vname (l, ltp) pending_decls) - pending_defs) + else 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 + let (lexp, ltp) = 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, @@ -914,29 +897,23 @@ and lexp_decls_1 else fatal l "Context changed in already changed context")
-and _lexp_decls pdecls ctx i: ((vdef * lexp * ltype) list list * elab_context) = +and lexp_p_decls pdecls ctx: ((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 + let declss, nnctx = lexp_p_decls pdecls nctx in decls :: declss, nnctx
-and lexp_decls_toplevel decls ctx = - _lexp_decls decls ctx [] - -and _lexp_parse_all (p: pexp list) (ctx: elab_context) i : lexp list = +and lexp_parse_all (p: pexp list) (ctx: elab_context) : lexp list =
let rec loop (plst: pexp list) ctx (acc: lexp list) = match plst with | [] -> (List.rev acc) - | pe :: plst -> let lxp, _ = _lexp_p_infer pe ctx i in + | pe :: plst -> let lxp, _ = infer pe ctx in (loop plst ctx (lxp::acc)) in
(loop p ctx [])
-and print_lexp_trace (trace : (OL.pexporlexp list) option) = - print_trace " ELAB TRACE " trace !_global_lexp_trace - (* Only print var info *) and lexp_print_var_info ctx = let ((m, _), env, _) = ctx in @@ -955,16 +932,6 @@ and lexp_print_var_info ctx = print_string "\n") done
-(* Those call reinitialize the calltrace *) -let lexp_parse_all p ctx = _lexp_parse_all p ctx [] - -let lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context): lexp = - _lexp_p_check p t ctx [] - -let lexp_p_infer (p : pexp) (ctx : elab_context): lexp * ltype = - _lexp_p_infer p ctx [] - - (* Default context with builtin types * --------------------------------------------------------- *)
===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -526,18 +526,3 @@ and clean_map cases =
SMap.mapi (fun key (l, args, expr) -> (l, (clean_arg_list args), (erase_type expr))) cases - - -(* Custom type to make trace uniform between lparse and eval *) -type pexporlexp = - | Pexp of P.pexp - | Elexp of E.elexp - - -let pol_string xp = match xp with - | Pexp p -> P.pexp_string p - | Elexp e -> E.elexp_string e - -let pol_name xp = match xp with - | Pexp p -> P.pexp_name p - | Elexp e -> E.elexp_name e
===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -251,8 +251,7 @@ let _ = test_eval_eqv_named "my_list = cons 1 (cons 2 (cons 3 - (cons 4 (nil %%(a := Int) - ))))" + (cons 4 nil)))"
"length my_list; head my_list;
View it on GitLab: https://gitlab.com/monnier/typer/commit/db00a5fa51a7dad8e4ef72d85de0bb4c6952...
Afficher les réponses par date