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

@@ -23,3 +23,5 @@ _tags
 .merlin
 gmon.out
 ocamlprof.dump
+emacs/*-autoloads.el
+emacs/*-pkg.el

src/REPL.ml

@@ -269,20 +269,20 @@ 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 ");
     print_string _welcome_msg;
     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 ()

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)

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(

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 -> "<undefined!>"
     | 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 =

src/eval.ml

@@ -612,43 +612,70 @@ let eval_all lxps rctx silent =
 
 let varname s = match s with Some (_, v) -> v | _ -> "<anon>"
 
-(* 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)

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
  * --------------------------------------------------------- *)

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 =