From 42923f807f4630241c5b95024c8f25ef2e74af0e Mon Sep 17 00:00:00 2001 From: Stefan Monnier Date: Mon, 5 Dec 2016 20:52:17 -0500 Subject: [PATCH] Only evaluate closed expressions in from_lctx * src/debruijn.ml (set_singleton, set_union): New functions. * src/env.ml (value_type): Add `Vundefined`. (print_rte_ctx): Drop hardcoded magic number. * src/eval.ml (from_lctx): Rewrite. (roname, ctx_memo, closed_dbset_p, closed_p): New functions. (from_ectx): New function to replace the old misnamed from_lctx. * src/lparse.ml (default_ectx): Rename from default_lctx. * src/opslexp.ml (mv_set): New type. (list_union, mv_set_empty, mv_set_add, mv_set_union, fv_memo) (fv_empty, fv_union, fv_sink, fv_hoist, fv): New functions. * tests/macro_test.ml ("macros base"): Move macro call to within a function, to test the handling of variables in the context. * .gitignore: Add patterns for ELPA files. --- .gitignore | 2 + src/REPL.ml | 6 +-- src/debruijn.ml | 10 ++++ src/debug_util.ml | 4 +- src/env.ml | 6 ++- src/eval.ml | 107 +++++++++++++++++++++++++++---------------- src/lparse.ml | 16 +++---- src/opslexp.ml | 95 ++++++++++++++++++++++++++++++++++++++ tests/eval_test.ml | 12 ++--- tests/lparse_test.ml | 4 +- tests/macro_test.ml | 12 ++--- tests/unify_test.ml | 4 +- 12 files changed, 206 insertions(+), 72 deletions(-) diff --git a/.gitignore b/.gitignore index f64cd77..906b4c4 100644 --- a/.gitignore +++ b/.gitignore @@ -23,3 +23,5 @@ _tags .merlin gmon.out ocamlprof.dump +emacs/*-autoloads.el +emacs/*-pkg.el diff --git a/src/REPL.ml b/src/REPL.ml index 410ebc7..192097a 100644 --- a/src/REPL.ml +++ b/src/REPL.ml @@ -269,7 +269,7 @@ let parse_args () = let main () = parse_args (); - let lctx = default_lctx in + let ectx = default_ectx in let rctx = default_rctx in print_string (make_title " TYPER REPL "); @@ -277,12 +277,12 @@ let main () = print_string (make_sep '-'); flush stdout; - let (i, lctx, rctx) = readfiles (!arg_files) (1, lctx, rctx) true in + let (i, ectx, rctx) = readfiles (!arg_files) (1, ectx, rctx) true in flush stdout; (* Initiate REPL. This will allow us to inspect interpreted code *) - repl i lctx rctx + repl i ectx rctx let _ = main () diff --git a/src/debruijn.ml b/src/debruijn.ml index 0accc55..b190d55 100644 --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -327,6 +327,8 @@ let set_mem i (o, m) = VMap.mem (i - o) m let set_set i (o, m) = (o, VMap.add (i - o) () m) let set_reset i (o, m) = (o, VMap.remove (i - o) m) +let set_singleton i = (0, VMap.singleton i ()) + (* Adjust a set for use in a deeper scope with `o` additional bindings. *) let set_sink o (o', m) = (o + o', m) @@ -336,3 +338,11 @@ let set_hoist o (o', m) = let (_, _, newm) = VMap.split (-1 - newo) m in (newo, newm) +let set_union (o1, m1) (o2, m2) : set = + if o1 = o2 then + (o1, VMap.merge (fun k _ _ -> Some ()) m1 m2) + else + let o = o2 - o1 in + (o1, VMap.fold (fun i2 () m1 + -> VMap.add (i2 + o) () m1) + m2 m1) diff --git a/src/debug_util.ml b/src/debug_util.ml index 3b90a45..0d1a630 100644 --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -196,7 +196,7 @@ let format_source () = let toks = lex default_stt pretoks in let nodes = sexp_parse_all_to_list default_grammar toks (Some ";") in let pexps = pexp_decls_all nodes in - let ctx = default_lctx in + let ctx = default_ectx in let lexps, _ = lexp_p_decls pexps ctx in print_string (make_sep '-'); print_string "\n"; @@ -354,7 +354,7 @@ let main () = debug_pexp_decls pexps; print_string "\n")); (* get lexp *) - let octx = default_lctx in + let octx = default_ectx in (* Debug declarations merging *) (if (get_p_option "merge-debug") then( diff --git a/src/env.ml b/src/env.ml index 9c3b8df..e6f00d1 100644 --- a/src/env.ml +++ b/src/env.ml @@ -55,6 +55,7 @@ type value_type = | 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 *) + | Vundefined | Vdummy | Vin of in_channel | Vout of out_channel @@ -109,6 +110,7 @@ let value_name v = | Vsexp _ -> "Vsexp" | Vcons _ -> "Vcons" | Vfloat _ -> "Vfloat" + | Vundefined -> "Vundefined" | Vdummy -> "Vdummy" | Vstring _ -> "Vstring" | Closure _ -> "Closure" @@ -120,6 +122,7 @@ let rec value_string v = | Vin _ -> "in_channel" | Vout _ -> "out_channe;" | Vdummy -> "dummy" + | Vundefined -> "" | Vcommand _ -> "command" | Vstring s -> "\"" ^ s ^ "\"" | Vbuiltin s -> s @@ -212,8 +215,7 @@ let print_rte_ctx_n (ctx: runtime_env) start = (* Only print user defined variables *) let print_rte_ctx ctx = - (* FIXME: harcoded -3, runtime_env has 3 variables missing *) - print_rte_ctx_n ctx (!L.builtin_size - 3) + print_rte_ctx_n ctx (!L.builtin_size) (* Dump the whole context *) let dump_rte_ctx ctx = diff --git a/src/eval.ml b/src/eval.ml index 77e83bf..89e0549 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -612,43 +612,70 @@ let eval_all lxps rctx silent = let varname s = match s with Some (_, v) -> v | _ -> "" -(* build a rctx from a lctx. *) -(* FIXME: `eval` with a disabled runIO, and then memoize, memoize, ... *) -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). *) - -> 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 +let roname loname = (match (loname : symbol option) with + | Some (_, name) -> Some name + | _ -> None) + +module CMap + (* Memoization table. FIXME: Ideally the keys should be "weak", but + * I haven't found any such functionality in OCaml's libs. *) + = Hashtbl.Make + (struct type t = lexp_context let hash = Hashtbl.hash let equal = (==) end) +let ctx_memo = CMap.create 1000 + +let closed_dbset_p rctx ((o, vm) : DB.set) = + VMap.for_all (fun i () -> let (_, rc) = Myers.nth (i + o) rctx in + match !rc with Vundefined -> false | _ -> true) + vm + +let closed_p rctx (fvs, mvs) = + closed_dbset_p rctx fvs + (* FIXME: Handle metavars! *) + && VMap.is_empty mvs + +let rec from_lctx (lctx: lexp_context): runtime_env = + (* FIXME: `eval` with a disabled runIO. *) + let from_lctx' (lctx: lexp_context): runtime_env = + match lctx with + | Myers.Mnil -> Myers.nil + | Myers.Mcons ((0, loname, def, _), lctx, _, _) + -> let rctx = from_lctx lctx in + Myers.cons (roname loname, + ref (match def with + | LetDef e + when closed_p rctx (OL.fv e) + -> eval (OL.erase_type e) rctx + | _ -> Vundefined)) + rctx + | Myers.Mcons ((1, loname, LetDef e, _), lctx, _, _) + -> let rec getdefs i lctx rdefs fvs = + match lctx with + | Myers.Mcons ((o, loname, LetDef e, _), lctx, _, _) + when o = i + -> getdefs (i + 1) lctx ((loname, e) :: rdefs) + (OL.fv_union fvs (OL.fv e)) + | _ -> (lctx, rdefs, fvs) in + let (lctx, rdefs, fvs) = getdefs 2 lctx [(loname, e)] OL.fv_empty in + let rctx = from_lctx lctx in + let (nrctx, evs) + = List.fold_left (fun (rctx, evs) (loname, e) + -> let rc = ref Vundefined in + (Myers.cons (roname loname, rc) rctx, + (e, rc)::evs)) + (rctx, []) rdefs in + let _ = + if closed_p rctx (OL.fv_hoist (List.length rdefs) fvs) then + List.iter (fun (e, rc) -> rc := eval (OL.erase_type e) nrctx) evs + else () in + nrctx + | _ -> U.internal_error "Unexpected lexp_context shape!" + in + try CMap.find ctx_memo lctx + with Not_found + -> let r = from_lctx' lctx in + CMap.add ctx_memo lctx r; + r + +(* build a rctx from a ectx. *) +let from_ectx (ctx: elab_context): runtime_env = + from_lctx (ectx_to_lctx ctx) diff --git a/src/lparse.ml b/src/lparse.ml index 59ce353..a531902 100644 --- a/src/lparse.ml +++ b/src/lparse.ml @@ -32,7 +32,6 @@ open Util open Fmt -open Myers open Prelexer open Lexer @@ -53,7 +52,6 @@ module Unif = Unification module OL = Opslexp module EL = Elexp -module SU = Subst (* Shortcut => Create a Var *) let make_var name index loc = @@ -681,13 +679,13 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = let rec handle_fun_args largs sargs pending ltp = let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) meta_ctx in match sargs, ltp' with - | _, Arrow (ak, Some (_, aname'), arg_type, _, ret_type) - when SMap.mem aname' pending - -> let sarg = SMap.find aname' pending in + | _, Arrow (ak, Some (_, aname), arg_type, _, ret_type) + when SMap.mem aname pending + -> let sarg = SMap.find aname pending in let parg = pexp_parse sarg in let larg = check parg arg_type ctx in handle_fun_args ((ak, larg) :: largs) sargs - (SMap.remove aname' pending) + (SMap.remove aname pending) (L.mkSusp ret_type (S.substitute larg)) | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs, @@ -833,7 +831,7 @@ and lexp_expand_macro_ macro_funct sargs ctx expand_fun : value_type = (* FIXME: Don't `mkCall + eval` but use eval_call instead! *) let macro = mkCall (macro_expand, args) in let emacro = OL.erase_type macro in - let rctx = EV.from_lctx ctx in + let rctx = EV.from_ectx ctx in (* eval macro *) let vxp = try EV._eval emacro rctx ([], []) @@ -1145,7 +1143,7 @@ let dynamic_bind r v body = with e -> r := old; raise e (* Make lxp context with built-in types *) -let default_lctx +let default_ectx = let _ = register_special_forms () in (* Empty context *) let lctx = make_elab_context in @@ -1184,7 +1182,7 @@ let default_lctx lctx in lctx -let default_rctx = EV.from_lctx default_lctx +let default_rctx = EV.from_ectx default_ectx (* String Parsing * --------------------------------------------------------- *) diff --git a/src/opslexp.ml b/src/opslexp.ml index ecfa387..5a4b306 100644 --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -594,6 +594,101 @@ let rec check' meta_ctx erased ctx e = let check meta_ctx = check' meta_ctx DB.set_empty +(** Compute the set of free (meta)variables. **) + +let rec list_union l1 l2 = match l1 with + | [] -> l2 + | (x::l1) -> list_union l1 (if List.mem x l2 then l2 else (x::l2)) + +type mv_set = subst list VMap.t +let mv_set_empty = VMap.empty +let mv_set_add ms m s + = let ss = try VMap.find m ms with Not_found -> [] in + if List.mem s ss then ms + else VMap.add m (s::ss) ms +let mv_set_union : mv_set -> mv_set -> mv_set + = VMap.merge (fun m oss1 oss2 + -> match (oss1, oss2) with + | (None, _) -> oss2 + | (_, None) -> oss1 + | (Some ss1, Some ss2) + -> Some (list_union ss1 ss2)) + +module LMap + (* Memoization table. FIXME: Ideally the keys should be "weak", but + * I haven't found any such functionality in OCaml's libs. *) + = Hashtbl.Make + (struct type t = lexp let hash = Hashtbl.hash let equal = (==) end) +let fv_memo = LMap.create 1000 + +let fv_empty = (DB.set_empty, mv_set_empty) +let fv_union (fv1, mv1) (fv2, mv2) + = (DB.set_union fv1 fv2, mv_set_union mv1 mv2) +let fv_sink n (fvs, mvs) = (DB.set_sink n fvs, mvs) +let fv_hoist n (fvs, mvs) = (DB.set_hoist n fvs, mvs) + +let rec fv (e : lexp) : (DB.set * mv_set) = + let fv' e = match e with + | Imm _ -> fv_empty + | SortLevel SLz -> fv_empty + | SortLevel (SLsucc e) -> fv e + | SortLevel (SLlub (e1, e2)) -> fv_union (fv e1) (fv e2) + | Sort (_, Stype e) -> fv e + | Sort (_, (StypeOmega | StypeLevel)) -> fv_empty + | Builtin _ -> fv_empty + | Var (_, i) -> (DB.set_singleton i, mv_set_empty) + | Susp (e, s) -> fv (push_susp e s) + | Let (_, defs, e) + -> let len = List.length defs in + let (s, _) + = List.fold_left (fun (s, o) (_, e, t) + -> (fv_union s (fv_union (fv_sink o (fv t)) + (fv e)), + o - 1)) + (fv e, len) defs in + fv_hoist len s + | Arrow (_, _, t1, _, t2) -> fv_union (fv t1) (fv_hoist 1 (fv t2)) + | Lambda (_, _, t, e) -> fv_union (fv t) (fv_hoist 1 (fv e)) + | Call (f, args) + -> List.fold_left (fun s (_, arg) + -> fv_union s (fv arg)) + (fv f) args + | Inductive (_, _, args, cases) + -> let alen = List.length args in + let s + = List.fold_left (fun s (_, _, t) + -> fv_sink 1 (fv_union s (fv t))) + fv_empty args in + let s + = SMap.fold + (fun _ fields s + -> fv_union + s + (fv_hoist (List.length fields) + (List.fold_left (fun s (_, _, t) + -> fv_sink 1 (fv_union s (fv t))) + fv_empty fields))) + cases s in + fv_hoist alen s + | Cons (t, _) -> fv t + | Case (_, e, t, cases, def) + -> let s = fv_union (fv e) (fv t) in + let s = match def with + | None -> s + | Some (_, e) -> fv_union s (fv_hoist 1 (fv e)) in + SMap.fold (fun _ (_, fields, e) s + -> fv_union s (fv_hoist (List.length fields) (fv e))) + cases s + | Metavar (m, s, _, t) + -> let (fvs, mvs) = fv t in + (fvs, mv_set_add mvs m s) + in + try LMap.find fv_memo e + with Not_found + -> let r = fv' e in + LMap.add fv_memo e r; + r + (*********** Type erasure, before evaluation. *****************) let rec erase_type (lxp: L.lexp): E.elexp = diff --git a/tests/eval_test.ml b/tests/eval_test.ml index 1138848..e4dce40 100644 --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -38,7 +38,7 @@ open Builtin open Env (* default environment *) -let lctx = default_lctx +let ectx = default_ectx let rctx = default_rctx (* Params: @@ -48,10 +48,10 @@ let rctx = default_rctx *) let test_eval_eqv_named name decl run res = add_test "EVAL" name (fun () -> - let rctx, lctx = eval_decl_str decl lctx rctx in + let rctx, ectx = eval_decl_str decl ectx rctx in - let erun = eval_expr_str run lctx rctx in (* evaluated run expr *) - let eres = eval_expr_str res lctx rctx in (* evaluated res expr *) + let erun = eval_expr_str run ectx rctx in (* evaluated run expr *) + let eres = eval_expr_str res ectx rctx in (* evaluated res expr *) if value_eq_list erun eres then success () @@ -288,12 +288,12 @@ let _ = (add_test "EVAL" "Monads" (fun () -> (lambda f -> write f \"Hello2\"); " in - let rctx, lctx = eval_decl_str dcode lctx rctx in + let rctx, ectx = eval_decl_str dcode ectx rctx in let rcode = "run-io c 2" in (* Eval defined lambda *) - let ret = eval_expr_str rcode lctx rctx in + let ret = eval_expr_str rcode ectx rctx in match ret with | [v] -> success () | _ -> failure () diff --git a/tests/lparse_test.ml b/tests/lparse_test.ml index 12bb858..a946b3a 100644 --- a/tests/lparse_test.ml +++ b/tests/lparse_test.ml @@ -60,7 +60,7 @@ let generate_lexp_from_str str = (List.map (fun (_, lxp, _) -> lxp)) (List.flatten lst)) - (lexp_decl_str str default_lctx)) + (lexp_decl_str str default_ectx)) let _ = generate_tests "TYPECHECK" @@ -68,7 +68,7 @@ let _ = generate_tests (fun x -> List.map lexp_string x) (fun x -> (x, true)) -let lctx = default_lctx +let lctx = default_ectx (* let _ = (add_test "TYPECHEK_LEXP" "lexp_print" (fun () -> * * let dcode = " diff --git a/tests/macro_test.ml b/tests/macro_test.ml index 0b822fa..d09c2bf 100644 --- a/tests/macro_test.ml +++ b/tests/macro_test.ml @@ -39,7 +39,7 @@ open Env (* default environment *) -let lctx = default_lctx +let ectx = default_ectx let rctx = default_rctx let _ = (add_test "MACROS" "macros base" (fun () -> @@ -57,11 +57,11 @@ let _ = (add_test "MACROS" "macros base" (fun () -> sqr = Macro_ my_fun; " in - let rctx, lctx = eval_decl_str dcode lctx rctx in + let rctx, ectx = eval_decl_str dcode ectx rctx in - let ecode = "(sqr 3);" in + let ecode = "(lambda (x : Int) -> sqr 3) 5;" in - let ret = eval_expr_str ecode lctx rctx in + let ret = eval_expr_str ecode ectx rctx in match ret with | [Vint(r)] -> expect_equal_int r (3 * 3) @@ -81,11 +81,11 @@ let _ = (add_test "MACROS" "macros decls" (fun () -> my-decls Nat;" in - let rctx, lctx = eval_decl_str dcode lctx rctx in + let rctx, ectx = eval_decl_str dcode ectx rctx in let ecode = "a; b;" in - let ret = eval_expr_str ecode lctx rctx in + let ret = eval_expr_str ecode ectx rctx in match ret with | [Vint(a); Vint(b)] -> diff --git a/tests/unify_test.ml b/tests/unify_test.ml index fb63e16..a962d05 100644 --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -100,14 +100,14 @@ let generate_ltype_from_str str = (List.map (fun (_, _, ltype) -> ltype)) (List.flatten lst)) - (lexp_decl_str str default_lctx)) + (lexp_decl_str str default_ectx)) let generate_lexp_from_str str = List.hd ((fun (lst, _) -> (List.map (fun (_, lxp, _) -> lxp)) (List.flatten lst)) - (lexp_decl_str str default_lctx)) + (lexp_decl_str str default_ectx)) let input_induct = generate_lexp_from_str str_induct let input_int_4 = generate_lexp_from_str str_int_4