diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2ffi.ml | 1 | ||||
| -rw-r--r-- | src/tac2ffi.mli | 1 | ||||
| -rw-r--r-- | src/tac2stdlib.ml | 4 | ||||
| -rw-r--r-- | src/tac2tactics.ml | 7 | ||||
| -rw-r--r-- | src/tac2types.mli | 6 |
5 files changed, 14 insertions, 5 deletions
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml index 7960d4d45f..923a29e5c5 100644 --- a/src/tac2ffi.ml +++ b/src/tac2ffi.ml @@ -329,6 +329,7 @@ let reference = { type ('a, 'b) fun1 = closure let fun1 (r0 : 'a repr) (r1 : 'b repr) : ('a, 'b) fun1 repr = closure +let to_fun1 r0 r1 f = to_closure f let rec apply : type a. a arity -> a -> valexpr list -> valexpr Proofview.tactic = fun arity f args -> match args, arity with diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli index 36743f3346..cb6d5a1e49 100644 --- a/src/tac2ffi.mli +++ b/src/tac2ffi.mli @@ -143,6 +143,7 @@ type ('a, 'b) fun1 val app_fun1 : ('a, 'b) fun1 -> 'a repr -> 'b repr -> 'a -> 'b Proofview.tactic +val to_fun1 : 'a repr -> 'b repr -> valexpr -> ('a, 'b) fun1 val fun1 : 'a repr -> 'b repr -> ('a, 'b) fun1 repr val valexpr : valexpr repr diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml index 4bcbe69b07..2828bbc53f 100644 --- a/src/tac2stdlib.ml +++ b/src/tac2stdlib.ml @@ -108,7 +108,7 @@ and to_intro_pattern_action = function let map ipat = to_intro_pattern ipat in IntroInjection (Value.to_list map inj) | ValBlk (2, [| c; ipat |]) -> - let c = thaw c >>= fun c -> return (Value.to_constr c) in + let c = Value.to_fun1 Value.unit Value.constr c in IntroApplyOn (c, to_intro_pattern ipat) | ValBlk (3, [| b |]) -> IntroRewrite (Value.to_bool b) | _ -> assert false @@ -143,7 +143,7 @@ let to_induction_clause v = match Value.to_tuple v with let to_assertion v = match Value.to_block v with | (0, [| ipat; t; tac |]) -> - let to_tac t = Proofview.tclIGNORE (thaw t) in + let to_tac t = Value.to_fun1 Value.unit Value.unit t in let ipat = Value.to_option to_intro_pattern ipat in let t = Value.to_constr t in let tac = Value.to_option to_tac tac in diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml index b55bd5c1b8..0b25ebb378 100644 --- a/src/tac2tactics.ml +++ b/src/tac2tactics.ml @@ -17,6 +17,7 @@ open Proofview open Proofview.Notations let return = Proofview.tclUNIT +let thaw r f = Tac2ffi.app_fun1 f Tac2ffi.unit r () let tactic_infer_flags with_evar = { Pretyping.use_typeclasses = true; @@ -31,6 +32,9 @@ let delayed_of_tactic tac env sigma = let c, pv, _, _ = Proofview.apply env tac pv in (sigma, c) +let delayed_of_thunk r tac env sigma = + delayed_of_tactic (thaw r tac) env sigma + let mk_bindings = function | ImplicitBindings l -> Misctypes.ImplicitBindings l | ExplicitBindings l -> @@ -55,7 +59,7 @@ and mk_intro_pattern_action = function | IntroOrAndPattern ipat -> Misctypes.IntroOrAndPattern (mk_or_and_intro_pattern ipat) | IntroInjection ipats -> Misctypes.IntroInjection (List.map mk_intro_pattern ipats) | IntroApplyOn (c, ipat) -> - let c = Loc.tag @@ delayed_of_tactic c in + let c = Loc.tag @@ delayed_of_thunk Tac2ffi.constr c in Misctypes.IntroApplyOn (c, mk_intro_pattern ipat) | IntroRewrite b -> Misctypes.IntroRewrite b @@ -172,6 +176,7 @@ let assert_ = function Tactics.forward true None (Some ipat) c | AssertType (ipat, c, tac) -> let ipat = Option.map mk_intro_pattern ipat in + let tac = Option.map (fun tac -> thaw Tac2ffi.unit tac) tac in Tactics.forward true (Some tac) ipat c let letin_pat_tac ev ipat na c cl = diff --git a/src/tac2types.mli b/src/tac2types.mli index 1cacbefc88..a7b0ceed6e 100644 --- a/src/tac2types.mli +++ b/src/tac2types.mli @@ -15,6 +15,8 @@ open Proofview type evars_flag = bool type advanced_flag = bool +type 'a thunk = (unit, 'a) Tac2ffi.fun1 + type quantified_hypothesis = Misctypes.quantified_hypothesis = | AnonHyp of int | NamedHyp of Id.t @@ -47,7 +49,7 @@ and intro_pattern_action = | IntroWildcard | IntroOrAndPattern of or_and_intro_pattern | IntroInjection of intro_pattern list -| IntroApplyOn of EConstr.t tactic * intro_pattern +| IntroApplyOn of EConstr.t thunk * intro_pattern | IntroRewrite of bool and or_and_intro_pattern = | IntroOrPattern of intro_pattern list list @@ -86,5 +88,5 @@ type rewriting = constr_with_bindings tactic type assertion = -| AssertType of intro_pattern option * constr * unit tactic option +| AssertType of intro_pattern option * constr * unit thunk option | AssertValue of Id.t * constr |