Using higher-order representation for closures.

11 files changed, 83 insertions, 85 deletions

diff --git a/src/tac2core.ml b/src/tac2core.ml
index 2f349e32af..603ddeecfd 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -100,7 +100,7 @@ let err_matchfailure bt =
 
 (** Helper functions *)
 
-let thaw bt f = Tac2interp.interp_app bt f [v_unit]
+let thaw bt f = f bt [v_unit]
 
 let throw bt e = Proofview.tclLIFT (Proofview.NonLogical.raise (e bt))
 
@@ -569,7 +569,7 @@ end
 
 (** (unit -> 'a) -> (exn -> 'a) -> 'a *)
 let () = define2 "plus" closure closure begin fun bt x k ->
-  Proofview.tclOR (thaw bt x) (fun e -> Tac2interp.interp_app bt k [Value.of_exn e])
+  Proofview.tclOR (thaw bt x) (fun e -> k bt [Value.of_exn e])
 end
 
 (** (unit -> 'a) -> 'a *)
@@ -597,31 +597,22 @@ let () = define1 "enter" closure begin fun bt f ->
   Proofview.tclINDEPENDENT f >>= fun () -> return v_unit
 end
 
-let k_var = Id.of_string "k"
-let e_var = Id.of_string "e"
-let prm_apply_kont_h = pname "apply_kont"
-
 (** (unit -> 'a) -> ('a * ('exn -> 'a)) result *)
 let () = define1 "case" closure begin fun bt f ->
   Proofview.tclCASE (thaw bt f) >>= begin function
   | Proofview.Next (x, k) ->
-    let k = {
-      clos_ref = None;
-      clos_env = Id.Map.singleton k_var (Value.of_ext Value.val_kont k);
-      clos_var = [Name e_var];
-      clos_exp = GTacPrm (prm_apply_kont_h, [GTacVar k_var; GTacVar e_var]);
-    } in
-    return (ValBlk (0, [| Value.of_tuple [| x; ValCls k |] |]))
+    let k bt = function
+    | [e] ->
+      let (e, info) = Value.to_exn e in
+      let e = set_bt bt e in
+      k (e, info)
+    | _ -> assert false
+    in
+    return (ValBlk (0, [| Value.of_tuple [| x; Value.of_closure k |] |]))
   | Proofview.Fail e -> return (ValBlk (1, [| Value.of_exn e |]))
   end
 end
 
-(** 'a kont -> exn -> 'a *)
-let () = define2 "apply_kont" (repr_ext val_kont) exn begin fun bt k (e, info) ->
-  let e = set_bt bt e in
-  k (e, info)
-end
-
 (** int -> int -> (unit -> 'a) -> 'a *)
 let () = define3 "focus" int int closure begin fun bt i j tac ->
   Proofview.tclFOCUS i j (thaw bt tac)
@@ -695,7 +686,7 @@ let () = define2 "with_holes" closure closure begin fun bt x f ->
   thaw bt x >>= fun ans ->
   Proofview.tclEVARMAP >>= fun sigma ->
   Proofview.Unsafe.tclEVARS sigma0 >>= fun () ->
-  Tacticals.New.tclWITHHOLES false (Tac2interp.interp_app bt f [ans]) sigma
+  Tacticals.New.tclWITHHOLES false (f bt [ans]) sigma
 end
 
 let () = define1 "progress" closure begin fun bt f ->
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 9fd03ff5aa..97e1fe8e8e 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -686,7 +686,7 @@ type redefinition = {
 
 let perform_redefinition (_, redef) =
   let kn = redef.redef_kn in
-  let data, _ = Tac2env.interp_global kn in
+  let data = Tac2env.interp_global kn in
   let data = { data with Tac2env.gdata_expr = redef.redef_body } in
   Tac2env.define_global kn data
 
@@ -715,7 +715,7 @@ let register_redefinition ?(local = false) (loc, qid) e =
   | TacAlias _ ->
     user_err ?loc (str "Cannot redefine syntactic abbreviations")
   in
-  let (data, _) = Tac2env.interp_global kn in
+  let data = Tac2env.interp_global kn in
   let () =
     if not (data.Tac2env.gdata_mutable) then
       user_err ?loc (str "The tactic " ++ pr_qualid qid ++ str " is not declared as mutable")
@@ -800,7 +800,7 @@ let print_ltac ref =
     in
     match kn with
     | TacConstant kn ->
-      let data, _ = Tac2env.interp_global kn in
+      let data = Tac2env.interp_global kn in
       let e = data.Tac2env.gdata_expr in
       let (_, t) = data.Tac2env.gdata_type in
       let name = int_name () in
diff --git a/src/tac2env.ml b/src/tac2env.ml
index c04eaf7b0c..ef2b44afb9 100644
--- a/src/tac2env.ml
+++ b/src/tac2env.ml
@@ -52,33 +52,13 @@ let empty_state = {
 
 let ltac_state = Summary.ref empty_state ~name:"ltac2-state"
 
-(** Get a dynamic value from syntactical value *)
-let rec eval_pure kn = function
-| GTacAtm (AtmInt n) -> ValInt n
-| GTacRef kn ->
-  let { gdata_expr = e } =
-    try KNmap.find kn ltac_state.contents.ltac_tactics
-    with Not_found -> assert false
-  in
-  eval_pure (Some kn) e
-| GTacFun (na, e) ->
-  ValCls { clos_ref = kn; clos_env = Id.Map.empty; clos_var = na; clos_exp = e }
-| GTacCst (_, n, []) -> ValInt n
-| GTacCst (_, n, el) -> ValBlk (n, Array.map_of_list eval_unnamed el)
-| GTacOpn (kn, el) -> ValOpn (kn, Array.map_of_list eval_unnamed el)
-| GTacAtm (AtmStr _) | GTacLet _ | GTacVar _ | GTacSet _
-| GTacApp _ | GTacCse _ | GTacPrj _ | GTacPrm _ | GTacExt _ | GTacWth _ ->
-  anomaly (Pp.str "Term is not a syntactical value")
-
-and eval_unnamed e = eval_pure None e
-
 let define_global kn e =
   let state = !ltac_state in
   ltac_state := { state with ltac_tactics = KNmap.add kn e state.ltac_tactics }
 
 let interp_global kn =
   let data = KNmap.find kn ltac_state.contents.ltac_tactics in
-  (data, eval_pure (Some kn) data.gdata_expr)
+  data
 
 let define_constructor kn t =
   let state = !ltac_state in
diff --git a/src/tac2env.mli b/src/tac2env.mli
index e40958e1a0..49c9910a44 100644
--- a/src/tac2env.mli
+++ b/src/tac2env.mli
@@ -24,7 +24,7 @@ type global_data = {
 }
 
 val define_global : ltac_constant -> global_data -> unit
-val interp_global : ltac_constant -> global_data * valexpr
+val interp_global : ltac_constant -> global_data
 
 (** {5 Toplevel definition of types} *)
 
diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index 36c3fbbe59..1b4a704b11 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -180,6 +180,13 @@ type strexpr =
 
 type tag = int
 
+type frame =
+| FrLtac of ltac_constant option
+| FrPrim of ml_tactic_name
+| FrExtn : ('a, 'b) Tac2dyn.Arg.tag * 'b -> frame
+
+type backtrace = frame list
+
 type valexpr =
 | ValInt of int
   (** Immediate integers *)
@@ -187,32 +194,14 @@ type valexpr =
   (** Structured blocks *)
 | ValStr of Bytes.t
   (** Strings *)
-| ValCls of closure
+| ValCls of ml_tactic
   (** Closures *)
 | ValOpn of KerName.t * valexpr array
   (** Open constructors *)
 | ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr
   (** Arbitrary data *)
 
-and closure = {
-  mutable clos_env : valexpr Id.Map.t;
-  (** Mutable so that we can implement recursive functions imperatively *)
-  clos_var : Name.t list;
-  (** Bound variables *)
-  clos_exp : glb_tacexpr;
-  (** Body *)
-  clos_ref : ltac_constant option;
-  (** Global constant from which the closure originates *)
-}
-
-type frame =
-| FrLtac of ltac_constant option
-| FrPrim of ml_tactic_name
-| FrExtn : ('a, 'b) Tac2dyn.Arg.tag * 'b -> frame
-
-type backtrace = frame list
-
-type ml_tactic = backtrace -> valexpr list -> valexpr Proofview.tactic
+and ml_tactic = backtrace -> valexpr list -> valexpr Proofview.tactic
 
 type environment = {
   env_ist : valexpr Id.Map.t;
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index 3e3dd362f7..fb97177c4d 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -34,8 +34,6 @@ let val_constructor = Val.create "constructor"
 let val_projection = Val.create "projection"
 let val_case = Val.create "case"
 let val_univ = Val.create "universe"
-let val_kont : (Exninfo.iexn -> valexpr Proofview.tactic) Val.tag =
-  Val.create "kont"
 let val_free : Names.Id.Set.t Val.tag = Val.create "free"
 
 let extract_val (type a) (type b) (tag : a Val.tag) (tag' : b Val.tag) (v : b) : a =
diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
index 1789a8932f..dfc87f7db3 100644
--- a/src/tac2ffi.mli
+++ b/src/tac2ffi.mli
@@ -60,9 +60,9 @@ val of_ident : Id.t -> valexpr
 val to_ident : valexpr -> Id.t
 val ident : Id.t repr
 
-val of_closure : closure -> valexpr
-val to_closure : valexpr -> closure
-val closure : closure repr
+val of_closure : ml_tactic -> valexpr
+val to_closure : valexpr -> ml_tactic
+val closure : ml_tactic repr
 
 val block : valexpr array repr
 
@@ -113,7 +113,6 @@ val val_constructor : constructor Val.tag
 val val_projection : Projection.t Val.tag
 val val_case : Constr.case_info Val.tag
 val val_univ : Univ.universe_level Val.tag
-val val_kont : (Exninfo.iexn -> valexpr Proofview.tactic) Val.tag
 val val_free : Id.Set.t Val.tag
 
 val val_exn : Exninfo.iexn Tac2dyn.Val.tag
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index d1a3e13cdb..2dcd8b8da3 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -654,7 +654,7 @@ let rec intern_rec env (loc, e) = match e with
     let sch = Id.Map.find id env.env_var in
     (GTacVar id, fresh_mix_type_scheme env sch)
   | ArgArg (TacConstant kn) ->
-    let { Tac2env.gdata_type = sch }, _ =
+    let { Tac2env.gdata_type = sch } =
       try Tac2env.interp_global kn
       with Not_found ->
         CErrors.anomaly (str "Missing hardwired primitive " ++ KerName.print kn)
diff --git a/src/tac2interp.ml b/src/tac2interp.ml
index 6bee5a0794..08cebc0af0 100644
--- a/src/tac2interp.ml
+++ b/src/tac2interp.ml
@@ -21,6 +21,17 @@ let empty_environment = {
   env_bkt = [];
 }
 
+type closure = {
+  mutable clos_env : valexpr Id.Map.t;
+  (** Mutable so that we can implement recursive functions imperatively *)
+  clos_var : Name.t list;
+  (** Bound variables *)
+  clos_exp : glb_tacexpr;
+  (** Body *)
+  clos_ref : ltac_constant option;
+  (** Global constant from which the closure originates *)
+}
+
 let push_name ist id v = match id with
 | Anonymous -> ist
 | Name id -> { ist with env_ist = Id.Map.add id v ist.env_ist }
@@ -30,7 +41,10 @@ let get_var ist id =
     anomaly (str "Unbound variable " ++ Id.print id)
 
 let get_ref ist kn =
-  try snd (Tac2env.interp_global kn) with Not_found ->
+  try
+    let data = Tac2env.interp_global kn in
+    data.Tac2env.gdata_expr
+  with Not_found ->
     anomaly (str "Unbound reference" ++ KerName.print kn)
 
 let return = Proofview.tclUNIT
@@ -39,14 +53,17 @@ let rec interp (ist : environment) = function
 | GTacAtm (AtmInt n) -> return (ValInt n)
 | GTacAtm (AtmStr s) -> return (ValStr (Bytes.of_string s))
 | GTacVar id -> return (get_var ist id)
-| GTacRef qid -> return (get_ref ist qid)
+| GTacRef kn ->
+  let data = get_ref ist kn in
+  return (eval_pure (Some kn) data)
 | GTacFun (ids, e) ->
   let cls = { clos_ref = None; clos_env = ist.env_ist; clos_var = ids; clos_exp = e } in
-  return (ValCls cls)
+  let f = interp_app cls in
+  return (ValCls f)
 | GTacApp (f, args) ->
   interp ist f >>= fun f ->
   Proofview.Monad.List.map (fun e -> interp ist e) args >>= fun args ->
-  interp_app ist.env_bkt (Tac2ffi.to_closure f) args
+  Tac2ffi.to_closure f ist.env_bkt args
 | GTacLet (false, el, e) ->
   let fold accu (na, e) =
     interp ist e >>= fun e ->
@@ -58,17 +75,18 @@ let rec interp (ist : environment) = function
   let map (na, e) = match e with
   | GTacFun (ids, e) ->
     let cls = { clos_ref = None; clos_env = ist.env_ist; clos_var = ids; clos_exp = e } in
-    na, cls
+    let f = ValCls (interp_app cls) in
+    na, cls, f
   | _ -> anomaly (str "Ill-formed recursive function")
   in
   let fixs = List.map map el in
-  let fold accu (na, cls) = match na with
+  let fold accu (na, _, cls) = match na with
   | Anonymous -> accu
-  | Name id -> { ist with env_ist = Id.Map.add id (ValCls cls) accu.env_ist }
+  | Name id -> { ist with env_ist = Id.Map.add id cls accu.env_ist }
   in
   let ist = List.fold_left fold ist fixs in
   (** Hack to make a cycle imperatively in the environment *)
-  let iter (_, e) = e.clos_env <- ist.env_ist in
+  let iter (_, e, _) = e.clos_env <- ist.env_ist in
   let () = List.iter iter fixs in
   interp ist e
 | GTacCst (_, n, []) -> return (ValInt n)
@@ -96,15 +114,16 @@ let rec interp (ist : environment) = function
   let ist = { ist with env_bkt = FrExtn (tag, e) :: ist.env_bkt } in
   tpe.Tac2env.ml_interp ist e
 
-and interp_app bt f args = match f with
+and interp_app f = (); fun bt args -> match f with
 | { clos_env = ist; clos_var = ids; clos_exp = e; clos_ref = kn } ->
   let rec push ist ids args = match ids, args with
   | [], [] -> interp ist e
   | [], _ :: _ ->
-    interp ist e >>= fun f -> interp_app bt (Tac2ffi.to_closure f) args
+    interp ist e >>= fun f -> Tac2ffi.to_closure f bt args
   | _ :: _, [] ->
     let cls = { clos_ref = kn; clos_env = ist.env_ist; clos_var = ids; clos_exp = e } in
-    return (ValCls cls)
+    let f = interp_app cls in
+    return (ValCls f)
   | id :: ids, arg :: args -> push (push_name ist id arg) ids args
   in
   push { env_ist = ist; env_bkt = FrLtac kn :: bt } ids args
@@ -147,6 +166,28 @@ and interp_set ist e p r = match e with
 | ValInt _ | ValExt _ | ValStr _ | ValCls _ | ValOpn _ ->
   anomaly (str "Unexpected value shape")
 
+and eval_pure kn = function
+| GTacAtm (AtmInt n) -> ValInt n
+| GTacRef kn ->
+  let { Tac2env.gdata_expr = e } =
+    try Tac2env.interp_global kn
+    with Not_found -> assert false
+  in
+  eval_pure (Some kn) e
+| GTacFun (na, e) ->
+  let cls = { clos_ref = kn; clos_env = Id.Map.empty; clos_var = na; clos_exp = e } in
+  let f = interp_app cls in
+  ValCls f
+| GTacCst (_, n, []) -> ValInt n
+| GTacCst (_, n, el) -> ValBlk (n, Array.map_of_list eval_unnamed el)
+| GTacOpn (kn, el) -> ValOpn (kn, Array.map_of_list eval_unnamed el)
+| GTacAtm (AtmStr _) | GTacLet _ | GTacVar _ | GTacSet _
+| GTacApp _ | GTacCse _ | GTacPrj _ | GTacPrm _ | GTacExt _ | GTacWth _ ->
+  anomaly (Pp.str "Term is not a syntactical value")
+
+and eval_unnamed e = eval_pure None e
+
+
 (** Cross-boundary hacks. *)
 
 open Geninterp
diff --git a/src/tac2interp.mli b/src/tac2interp.mli
index ca263b2c4b..48af59b178 100644
--- a/src/tac2interp.mli
+++ b/src/tac2interp.mli
@@ -13,7 +13,7 @@ val empty_environment : environment
 
 val interp : environment -> glb_tacexpr -> valexpr Proofview.tactic
 
-val interp_app : backtrace -> closure -> valexpr list -> valexpr Proofview.tactic
+(* val interp_app : closure -> ml_tactic *)
 
 (** {5 Cross-boundary encodings} *)
 
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 79af41b7d0..14ad8695ca 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -18,7 +18,7 @@ module Value = Tac2ffi
 
 let return x = Proofview.tclUNIT x
 let v_unit = Value.of_unit ()
-let thaw bt f = Tac2interp.interp_app bt (Value.to_closure f) [v_unit]
+let thaw bt f = (Value.to_closure f) bt [v_unit]
 
 let to_pair f g = function
 | ValBlk (0, [| x; y |]) -> (f x, g y)