Hide definition of tacvalue in tacinterp

Author: SkySkimmer

plugins/ltac/pptactic.ml

@@ -1400,24 +1400,13 @@ let () =
   register_basic_print0 Stdarg.wit_pre_ident str str str;
   register_basic_print0 Stdarg.wit_string qstring qstring qstring
 
-let pr_tacvalue env = function
-  | VFun (a,_,loc,ids,l,tac) ->
-    let open Pp in
-    let tac = if List.is_empty l then tac else CAst.make ?loc @@ Tacexpr.TacFun (l,tac) in
-    let pr_env env =
-      if Id.Map.is_empty ids then mt ()
-      else
-        cut () ++ str "where" ++
-        Id.Map.fold (fun id c pp ->
-            cut () ++ Id.print id ++ str " := " ++ pr_value ltop c ++ pp)
-          ids (mt ())
-    in
-    v 0 (hov 0 (pr_glob_tactic env tac) ++ pr_env env)
-  | VRec _ -> str "<tactic closure>"
+let pr_tacvalue_ref = ref (fun _ _ : Pp.t -> assert false)
+
+let pr_tacvalue env v = !pr_tacvalue_ref env v
 
 let () =
   let printer env sigma _ _ prtac = prtac env sigma in
-  let top_print env sigma _ _ _ _ = pr_tacvalue env in
+  let top_print env sigma _ _ _ _ v = pr_tacvalue env v in
   declare_extra_genarg_pprule_with_level wit_tactic printer printer top_print
   ltop (LevelLe 0)
 
@@ -1451,3 +1440,7 @@ let () =
   in
   Gentactic.register_print wit_ltac (printer pr_raw_tactic_level)
     (printer (fun env _sigma n x -> pr_glob_tactic_level env n x))
+
+module Internal = struct
+  let pr_tacvalue_ref = pr_tacvalue_ref
+end

plugins/ltac/pptactic.mli

@@ -165,3 +165,7 @@ val make_constr_printer : (env -> Evd.evar_map -> entry_relative_level -> 'a ->
   'a Genprint.top_printer
 
 val ssr_loaded : unit -> bool
+
+module Internal : sig
+  val pr_tacvalue_ref : (env -> Tacarg.tacvalue -> Pp.t) ref
+end

plugins/ltac/tacarg.ml

@@ -13,7 +13,6 @@
 open Genarg
 open Geninterp
 open Tacexpr
-open Names
 
 let make0 ?dyn name =
   let wit = Genarg.make0 name in
@@ -28,17 +27,8 @@ let wit_open_constr_with_bindings = make0 "open_constr_with_bindings"
 let wit_bindings = make0 "bindings"
 let wit_quantified_hypothesis = wit_quant_hyp
 
-
-(** Abstract application, to print ltac functions *)
-type appl =
-  | UnnamedAppl (** For generic applications: nothing is printed *)
-  | GlbAppl of (Names.KerName.t * Geninterp.Val.t list) list
-       (** For calls to global constants, some may alias other. *)
-
-type tacvalue =
-  | VFun of appl * ltac_trace * Loc.t option * Geninterp.Val.t Id.Map.t *
-      Name.t list * glob_tactic_expr
-  | VRec of Geninterp.Val.t Id.Map.t ref * glob_tactic_expr
+(* we can put ocaml closures (through geninterp vals) in tacvalues so no need to be marshallable *)
+type tacvalue = ..
 
 let wit_tactic : (raw_tactic_expr, glob_tactic_expr, tacvalue) genarg_type =
   make0 "tactic"
@@ -49,3 +39,18 @@ let wit_ltac = Gentactic.make "ltac"
 
 let wit_destruction_arg =
   make0 "destruction_arg"
+
+module Internal = struct
+  let defined_tacvalue = ref false
+
+  let define_tacvalue (type a) () =
+    assert (not !defined_tacvalue);
+    defined_tacvalue := true;
+    let module M = (struct type tacvalue += V of a end) in
+    let of_v x = M.V x in
+    let to_v = function
+      | M.V x -> x
+      | _ -> assert false
+    in
+    of_v, to_v
+end

plugins/ltac/tacarg.mli

@@ -14,7 +14,6 @@ open Constrexpr
 open Genintern
 open Tactypes
 open Tacexpr
-open Names
 
 (** Tactic related witnesses, could also live in tactics/ if other users *)
 
@@ -43,16 +42,7 @@ val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
 
 (** Generic arguments based on Ltac. *)
 
-(** Abstract application, to print ltac functions *)
-type appl =
-  | UnnamedAppl (** For generic applications: nothing is printed *)
-  | GlbAppl of (Names.KerName.t * Geninterp.Val.t list) list
-       (** For calls to global constants, some may alias other. *)
-
-type tacvalue =
-  | VFun of appl * ltac_trace * Loc.t option * Geninterp.Val.t Id.Map.t *
-      Name.t list * glob_tactic_expr
-  | VRec of Geninterp.Val.t Id.Map.t ref * glob_tactic_expr
+type tacvalue
 
 val wit_tactic : (raw_tactic_expr, glob_tactic_expr, tacvalue) genarg_type
 
@@ -68,3 +58,8 @@ val wit_destruction_arg :
    glob_constr_and_expr with_bindings Tactics.destruction_arg,
    delayed_open_constr_with_bindings Tactics.destruction_arg) genarg_type
 
+module Internal : sig
+
+  val define_tacvalue : unit -> ('a -> tacvalue) * (tacvalue -> 'a)
+
+end

plugins/ltac/tacinterp.ml

@@ -42,6 +42,17 @@ open Ltac_pretype
 
 module TacStore = Tacenv.TacStore
 
+(** Abstract application, to print ltac functions *)
+type appl =
+  | UnnamedAppl (** For generic applications: nothing is printed *)
+  | GlbAppl of (Names.KerName.t * Geninterp.Val.t list) list
+       (** For calls to global constants, some may alias other. *)
+
+type tacvalue_v =
+  | VFun of appl * ltac_trace * Loc.t option * Geninterp.Val.t Id.Map.t *
+      Name.t list * glob_tactic_expr
+  | VRec of Geninterp.Val.t Id.Map.t ref * glob_tactic_expr
+
 (* Signature for interpretation: val_interp and interpretation functions *)
 type interp_sign = Tacenv.interp_sign =
   { lfun : Geninterp.Val.t Id.Map.t
@@ -138,6 +149,30 @@ let combine_appl appl1 appl2 =
 let of_tacvalue = Value.of_tacvalue
 let to_tacvalue = Value.to_tacvalue
 
+let (of_tacvalue_v : tacvalue_v -> tacvalue), to_tacvalue_v = Tacarg.Internal.define_tacvalue ()
+
+let pr_tacvalue env v = match to_tacvalue_v v with
+  | VFun (a,_,loc,ids,l,tac) ->
+    let open Pp in
+    let tac = if List.is_empty l then tac else CAst.make ?loc @@ Tacexpr.TacFun (l,tac) in
+    let pr_env env =
+      if Id.Map.is_empty ids then mt ()
+      else
+        cut () ++ str "where" ++
+        Id.Map.fold (fun id c pp ->
+            cut () ++ Id.print id ++ str " := " ++ Pptactic.pr_value Pptactic.ltop c ++ pp)
+          ids (mt ())
+    in
+    v 0 (hov 0 (Pptactic.pr_glob_tactic env tac) ++ pr_env env)
+  | VRec _ -> str "<tactic closure>"
+
+let () =
+  Pptactic.Internal.pr_tacvalue_ref := fun env v ->
+    pr_tacvalue env v
+
+let to_tacvalue_val v = Option.map to_tacvalue_v @@ to_tacvalue v
+let of_tacvalue_val v = of_tacvalue @@ of_tacvalue_v v
+
 (* Debug reference *)
 let debug = ref DebugOff
 
@@ -154,9 +189,9 @@ let is_traced () =
 
 (** More naming applications *)
 let name_vfun appl vle =
-  match to_tacvalue vle with
+  match to_tacvalue_val vle with
   | Some (VFun (appl0,trace,loc,lfun,vars,t)) ->
-    of_tacvalue (VFun (combine_appl appl0 appl,trace,loc,lfun,vars,t))
+    of_tacvalue_val (VFun (combine_appl appl0 appl,trace,loc,lfun,vars,t))
   | Some (VRec _) | None -> vle
 
 let f_avoid_ids : Id.Set.t TacStore.field = TacStore.field "f_avoid_ids"
@@ -261,7 +296,7 @@ let pr_closure env ist body =
 let pr_inspect env expr result =
   let pp_expr = Pptactic.pr_glob_tactic env expr in
   let pp_result =
-    match to_tacvalue result with
+    match to_tacvalue_val result with
     | Some (VFun (_, _, _, ist, ul, b)) ->
       let body = if List.is_empty ul then b else CAst.make (TacFun (ul, b)) in
       str "a closure with body " ++ fnl() ++ pr_closure env ist body
@@ -286,7 +321,7 @@ let push_trace call ist =
   else [],[]
 
 let propagate_trace ist loc id v =
-  match to_tacvalue v with
+  match to_tacvalue_val v with
   | None ->  Proofview.tclUNIT v
   | Some tacv ->
     match tacv with
@@ -299,21 +334,21 @@ let propagate_trace ist loc id v =
       let t = if List.is_empty it then b else CAst.make (TacFun (it,b)) in
       let trace = push_trace(loc,LtacVarCall (kn,id,t)) ist in
       let ans = VFun (appl,trace,loc,lfun,it,b) in
-      Proofview.tclUNIT (of_tacvalue ans)
+      Proofview.tclUNIT (of_tacvalue_val ans)
     | VRec _ ->  Proofview.tclUNIT v
 
 let append_trace trace v =
-  match to_tacvalue v with
-  | Some (VFun (appl,trace',loc,lfun,it,b)) -> of_tacvalue (VFun (appl,trace',loc,lfun,it,b))
+  match to_tacvalue_val v with
+  | Some (VFun (appl,trace',loc,lfun,it,b)) -> of_tacvalue_val (VFun (appl,trace',loc,lfun,it,b))
   | _ -> v
 
 (* Dynamically check that an argument is a tactic *)
 let coerce_to_tactic loc id v =
   let fail () = user_err ?loc
     (str "Variable " ++ Id.print id ++ str " should be bound to a tactic.")
   in
-  match to_tacvalue v with
-  | Some (VFun (appl,trace,_,lfun,it,b)) -> of_tacvalue (VFun (appl,trace,loc,lfun,it,b))
+  match to_tacvalue_val v with
+  | Some (VFun (appl,trace,_,lfun,it,b)) -> of_tacvalue_val (VFun (appl,trace,loc,lfun,it,b))
   | _ -> fail ()
 
 let intro_pattern_of_ident id = CAst.make @@ IntroNaming (IntroIdentifier id)
@@ -1151,15 +1186,15 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti
   let value_interp ist =
   match tac2 with
   | TacFun (it, body) ->
-    Ftactic.return (of_tacvalue (VFun (UnnamedAppl, extract_trace ist, extract_loc ist, ist.lfun, it, body)))
+    Ftactic.return (of_tacvalue_val (VFun (UnnamedAppl, extract_trace ist, extract_loc ist, ist.lfun, it, body)))
   | TacLetIn (true,l,u) -> interp_letrec ist l u
   | TacLetIn (false,l,u) -> interp_letin ist l u
   | TacMatchGoal (lz,lr,lmr) -> interp_match_goal ist lz lr lmr
   | TacMatch (lz,c,lmr) -> interp_match ist lz c lmr
   | TacArg v -> interp_tacarg ist v
   | _ ->
     (* Delayed evaluation *)
-    Ftactic.return (of_tacvalue (VFun (UnnamedAppl, extract_trace ist, extract_loc ist, ist.lfun, [], tac)))
+    Ftactic.return (of_tacvalue_val (VFun (UnnamedAppl, extract_trace ist, extract_loc ist, ist.lfun, [], tac)))
   in
   let open Ftactic in
   Control.check_for_interrupt ();
@@ -1305,7 +1340,7 @@ and eval_tactic_ist ist tac : unit Proofview.tactic =
       Ftactic.run args tac
 
 and force_vrec ist v : Val.t Ftactic.t =
-  match to_tacvalue v with
+  match to_tacvalue_val v with
   | Some (VRec (lfun,body)) -> val_interp {ist with lfun = !lfun} body
   | _ -> Ftactic.return v
 
@@ -1385,7 +1420,7 @@ and interp_tacarg ist arg : Val.t Ftactic.t =
 and interp_app loc ist fv largs : Val.t Ftactic.t =
   Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
   let (>>=) = Ftactic.bind in
-  match to_tacvalue fv with
+  match to_tacvalue_val fv with
   | None | Some (VRec _) -> Tacticals.tclZEROMSG (str "Illegal tactic application.")
   (* if var=[] and body has been delayed by val_interp, then body
       is not a tactic that expects arguments.
@@ -1432,7 +1467,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
       end <*>
       if List.is_empty lval then Ftactic.return v else interp_app loc ist v lval
     else
-      Ftactic.return (of_tacvalue (VFun(push_appl appl largs,trace,loc,newlfun,lvar,body)))
+      Ftactic.return (of_tacvalue_val (VFun(push_appl appl largs,trace,loc,newlfun,lvar,body)))
   | Some (VFun(appl,trace,_,olfun,[],body)) ->
     let extra_args = List.length largs in
     let info = Exninfo.reify () in
@@ -1454,7 +1489,7 @@ and tactic_of_value ist vle =
     let info = Exninfo.reify () in
     Tacticals.tclZEROMSG ~info (str "Expression does not evaluate to a tactic (got a " ++ str name ++ str ").")
 
-and tactic_of_tacvalue ist = function
+and tactic_of_tacvalue ist v = match to_tacvalue_v v with
   | VFun (appl,trace,loc,lfun,[],t) ->
     Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
     let ist = {
@@ -1506,7 +1541,7 @@ and interp_letrec ist llc u =
   Proofview.tclUNIT () >>= fun () -> (* delay for the effects of [lref], just in case. *)
   let lref = ref ist.lfun in
   let fold accu ({v=na}, b) =
-    let v = of_tacvalue (VRec (lref, CAst.make (TacArg b))) in
+    let v = of_tacvalue_val (VRec (lref, CAst.make (TacArg b))) in
     Name.fold_right (fun id -> Id.Map.add id v) na accu
   in
   let lfun = List.fold_left fold ist.lfun llc in
@@ -1536,7 +1571,7 @@ and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } =
   let lfun = extend_values_with_bindings subst (lctxt +++ hyp_subst +++ ist.lfun) in
   let ist = { ist with lfun } in
   val_interp ist lhs >>= fun v ->
-  match to_tacvalue v with
+  match to_tacvalue_val v with
   | Some (VFun (appl,trace,loc,lfun,[],t)) ->
       let ist =
         { lfun = lfun
@@ -1547,7 +1582,7 @@ and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } =
       let dummy = VFun (appl, extract_trace ist, loc, Id.Map.empty, [],
         CAst.make (TacId [])) in
       let (stack, _) = trace in
-      catch_error_tac stack (tac <*> Ftactic.return (of_tacvalue dummy))
+      catch_error_tac stack (tac <*> Ftactic.return (of_tacvalue_val dummy))
   | _ -> Ftactic.return v
 
 
@@ -2000,7 +2035,7 @@ module Value = struct
   include Taccoerce.Value
 
   let closure ist tac =
-    VFun (UnnamedAppl, extract_trace ist, None, ist.lfun, [], tac)
+    of_tacvalue_v @@ VFun (UnnamedAppl, extract_trace ist, None, ist.lfun, [], tac)
 
   let of_closure ist tac =
     let closure = closure ist tac in