aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/tac2core.ml233
-rw-r--r--src/tac2core.mli2
-rw-r--r--src/tac2entries.ml8
-rw-r--r--src/tac2expr.mli3
-rw-r--r--src/tac2interp.ml46
-rw-r--r--src/tac2interp.mli8
-rw-r--r--src/tac2stdlib.ml221
-rw-r--r--src/tac2tactics.ml48
-rw-r--r--src/tac2tactics.mli22
9 files changed, 313 insertions, 278 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 7f136b48ae..4a35442b04 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -100,9 +100,14 @@ let err_matchfailure bt =
(** Helper functions *)
-let thaw bt f = f bt [v_unit]
+let thaw f = f [v_unit]
-let throw bt e = Proofview.tclLIFT (Proofview.NonLogical.raise (e bt))
+let throw e =
+ Tac2interp.get_backtrace >>= fun bt ->
+ Proofview.tclLIFT (Proofview.NonLogical.raise (e bt))
+
+let fail e =
+ Tac2interp.get_backtrace >>= fun bt -> Proofview.tclZERO (e bt)
let set_bt bt e = match e with
| Tac2interp.LtacError (kn, args, _) -> Tac2interp.LtacError (kn, args, bt)
@@ -117,13 +122,13 @@ let wrap f =
let wrap_unit f =
return () >>= fun () -> f (); return v_unit
-let assert_focussed bt =
+let assert_focussed =
Proofview.Goal.goals >>= fun gls ->
match gls with
| [_] -> Proofview.tclUNIT ()
- | [] | _ :: _ :: _ -> throw bt err_notfocussed
+ | [] | _ :: _ :: _ -> throw err_notfocussed
-let pf_apply bt f =
+let pf_apply f =
Proofview.Goal.goals >>= function
| [] ->
Proofview.tclENV >>= fun env ->
@@ -133,103 +138,103 @@ let pf_apply bt f =
gl >>= fun gl ->
f (Proofview.Goal.env gl) (Tacmach.New.project gl)
| _ :: _ :: _ ->
- throw bt err_notfocussed
+ throw err_notfocussed
(** Primitives *)
-let define0 name f = Tac2env.define_primitive (pname name) begin fun bt arg -> match arg with
-| [_] -> f bt
+let define0 name f = Tac2env.define_primitive (pname name) begin fun arg -> match arg with
+| [_] -> f
| _ -> assert false
end
-let define1 name r0 f = Tac2env.define_primitive (pname name) begin fun bt arg -> match arg with
-| [x] -> f bt (r0.Value.r_to x)
+let define1 name r0 f = Tac2env.define_primitive (pname name) begin fun arg -> match arg with
+| [x] -> f (r0.Value.r_to x)
| _ -> assert false
end
-let define2 name r0 r1 f = Tac2env.define_primitive (pname name) begin fun bt arg -> match arg with
-| [x; y] -> f bt (r0.Value.r_to x) (r1.Value.r_to y)
+let define2 name r0 r1 f = Tac2env.define_primitive (pname name) begin fun arg -> match arg with
+| [x; y] -> f (r0.Value.r_to x) (r1.Value.r_to y)
| _ -> assert false
end
-let define3 name r0 r1 r2 f = Tac2env.define_primitive (pname name) begin fun bt arg -> match arg with
-| [x; y; z] -> f bt (r0.Value.r_to x) (r1.Value.r_to y) (r2.Value.r_to z)
+let define3 name r0 r1 r2 f = Tac2env.define_primitive (pname name) begin fun arg -> match arg with
+| [x; y; z] -> f (r0.Value.r_to x) (r1.Value.r_to y) (r2.Value.r_to z)
| _ -> assert false
end
(** Printing *)
-let () = define1 "print" pp begin fun _ pp ->
+let () = define1 "print" pp begin fun pp ->
wrap_unit (fun () -> Feedback.msg_notice pp)
end
-let () = define1 "message_of_int" int begin fun _ n ->
+let () = define1 "message_of_int" int begin fun n ->
return (Value.of_pp (Pp.int n))
end
-let () = define1 "message_of_string" string begin fun _ s ->
+let () = define1 "message_of_string" string begin fun s ->
return (Value.of_pp (str (Bytes.to_string s)))
end
-let () = define1 "message_of_constr" constr begin fun bt c ->
- pf_apply bt begin fun env sigma ->
+let () = define1 "message_of_constr" constr begin fun c ->
+ pf_apply begin fun env sigma ->
let pp = Printer.pr_econstr_env env sigma c in
return (Value.of_pp pp)
end
end
-let () = define1 "message_of_ident" ident begin fun _ c ->
+let () = define1 "message_of_ident" ident begin fun c ->
let pp = Id.print c in
return (Value.of_pp pp)
end
-let () = define2 "message_concat" pp pp begin fun _ m1 m2 ->
+let () = define2 "message_concat" pp pp begin fun m1 m2 ->
return (Value.of_pp (Pp.app m1 m2))
end
(** Array *)
-let () = define2 "array_make" int valexpr begin fun bt n x ->
- if n < 0 || n > Sys.max_array_length then throw bt err_outofbounds
+let () = define2 "array_make" int valexpr begin fun n x ->
+ if n < 0 || n > Sys.max_array_length then throw err_outofbounds
else wrap (fun () -> ValBlk (0, Array.make n x))
end
-let () = define1 "array_length" block begin fun _ v ->
+let () = define1 "array_length" block begin fun v ->
return (ValInt (Array.length v))
end
-let () = define3 "array_set" block int valexpr begin fun bt v n x ->
- if n < 0 || n >= Array.length v then throw bt err_outofbounds
+let () = define3 "array_set" block int valexpr begin fun v n x ->
+ if n < 0 || n >= Array.length v then throw err_outofbounds
else wrap_unit (fun () -> v.(n) <- x)
end
-let () = define2 "array_get" block int begin fun bt v n ->
- if n < 0 || n >= Array.length v then throw bt err_outofbounds
+let () = define2 "array_get" block int begin fun v n ->
+ if n < 0 || n >= Array.length v then throw err_outofbounds
else wrap (fun () -> v.(n))
end
(** Ident *)
-let () = define2 "ident_equal" ident ident begin fun _ id1 id2 ->
+let () = define2 "ident_equal" ident ident begin fun id1 id2 ->
return (Value.of_bool (Id.equal id1 id2))
end
-let () = define1 "ident_to_string" ident begin fun _ id ->
+let () = define1 "ident_to_string" ident begin fun id ->
return (Value.of_string (Id.to_string id))
end
-let () = define1 "ident_of_string" string begin fun _ s ->
+let () = define1 "ident_of_string" string begin fun s ->
let id = try Some (Id.of_string s) with _ -> None in
return (Value.of_option Value.of_ident id)
end
(** Int *)
-let () = define2 "int_equal" int int begin fun _ m n ->
+let () = define2 "int_equal" int int begin fun m n ->
return (Value.of_bool (m == n))
end
-let binop n f = define2 n int int begin fun _ m n ->
+let binop n f = define2 n int int begin fun m n ->
return (Value.of_int (f m n))
end
@@ -238,52 +243,52 @@ let () = binop "int_add" (+)
let () = binop "int_sub" (-)
let () = binop "int_mul" ( * )
-let () = define1 "int_neg" int begin fun _ m ->
+let () = define1 "int_neg" int begin fun m ->
return (Value.of_int (~- m))
end
(** String *)
-let () = define2 "string_make" int char begin fun bt n c ->
- if n < 0 || n > Sys.max_string_length then throw bt err_outofbounds
+let () = define2 "string_make" int char begin fun n c ->
+ if n < 0 || n > Sys.max_string_length then throw err_outofbounds
else wrap (fun () -> Value.of_string (Bytes.make n c))
end
-let () = define1 "string_length" string begin fun _ s ->
+let () = define1 "string_length" string begin fun s ->
return (Value.of_int (Bytes.length s))
end
-let () = define3 "string_set" string int char begin fun bt s n c ->
- if n < 0 || n >= Bytes.length s then throw bt err_outofbounds
+let () = define3 "string_set" string int char begin fun s n c ->
+ if n < 0 || n >= Bytes.length s then throw err_outofbounds
else wrap_unit (fun () -> Bytes.set s n c)
end
-let () = define2 "string_get" string int begin fun bt s n ->
- if n < 0 || n >= Bytes.length s then throw bt err_outofbounds
+let () = define2 "string_get" string int begin fun s n ->
+ if n < 0 || n >= Bytes.length s then throw err_outofbounds
else wrap (fun () -> Value.of_char (Bytes.get s n))
end
(** Terms *)
(** constr -> constr *)
-let () = define1 "constr_type" constr begin fun bt c ->
+let () = define1 "constr_type" constr begin fun c ->
let get_type env sigma =
Proofview.V82.wrap_exceptions begin fun () ->
let (sigma, t) = Typing.type_of env sigma c in
let t = Value.of_constr t in
Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT t
end in
- pf_apply bt get_type
+ pf_apply get_type
end
(** constr -> constr *)
-let () = define2 "constr_equal" constr constr begin fun _ c1 c2 ->
+let () = define2 "constr_equal" constr constr begin fun c1 c2 ->
Proofview.tclEVARMAP >>= fun sigma ->
let b = EConstr.eq_constr sigma c1 c2 in
Proofview.tclUNIT (Value.of_bool b)
end
-let () = define1 "constr_kind" constr begin fun _ c ->
+let () = define1 "constr_kind" constr begin fun c ->
let open Constr in
Proofview.tclEVARMAP >>= fun sigma ->
return begin match EConstr.kind sigma c with
@@ -377,7 +382,7 @@ let () = define1 "constr_kind" constr begin fun _ c ->
end
end
-let () = define1 "constr_make" valexpr begin fun _ knd ->
+let () = define1 "constr_make" valexpr begin fun knd ->
let open Constr in
let c = match knd with
| ValBlk (0, [|n|]) ->
@@ -457,8 +462,8 @@ let () = define1 "constr_make" valexpr begin fun _ knd ->
return (Value.of_constr c)
end
-let () = define1 "constr_check" constr begin fun bt c ->
- pf_apply bt begin fun env sigma ->
+let () = define1 "constr_check" constr begin fun c ->
+ pf_apply begin fun env sigma ->
try
let (sigma, _) = Typing.type_of env sigma c in
Proofview.Unsafe.tclEVARS sigma >>= fun () ->
@@ -469,26 +474,26 @@ let () = define1 "constr_check" constr begin fun bt c ->
end
end
-let () = define3 "constr_substnl" (list constr) int constr begin fun _ subst k c ->
+let () = define3 "constr_substnl" (list constr) int constr begin fun subst k c ->
let ans = EConstr.Vars.substnl subst k c in
return (Value.of_constr ans)
end
-let () = define3 "constr_closenl" (list ident) int constr begin fun _ ids k c ->
+let () = define3 "constr_closenl" (list ident) int constr begin fun ids k c ->
let ans = EConstr.Vars.substn_vars k ids c in
return (Value.of_constr ans)
end
(** Patterns *)
-let () = define2 "pattern_matches" pattern constr begin fun bt pat c ->
- pf_apply bt begin fun env sigma ->
+let () = define2 "pattern_matches" pattern constr begin fun pat c ->
+ pf_apply begin fun env sigma ->
let ans =
try Some (Constr_matching.matches env sigma pat c)
with Constr_matching.PatternMatchingFailure -> None
in
begin match ans with
- | None -> Proofview.tclZERO (err_matchfailure bt)
+ | None -> fail err_matchfailure
| Some ans ->
let ans = Id.Map.bindings ans in
let of_pair (id, c) = Value.of_tuple [| Value.of_ident id; Value.of_constr c |] in
@@ -497,30 +502,30 @@ let () = define2 "pattern_matches" pattern constr begin fun bt pat c ->
end
end
-let () = define2 "pattern_matches_subterm" pattern constr begin fun bt pat c ->
+let () = define2 "pattern_matches_subterm" pattern constr begin fun pat c ->
let open Constr_matching in
let rec of_ans s = match IStream.peek s with
- | IStream.Nil -> Proofview.tclZERO (err_matchfailure bt)
+ | IStream.Nil -> fail err_matchfailure
| IStream.Cons ({ m_sub = (_, sub); m_ctx }, s) ->
let ans = Id.Map.bindings sub in
let of_pair (id, c) = Value.of_tuple [| Value.of_ident id; Value.of_constr c |] in
let ans = Value.of_tuple [| Value.of_constr m_ctx; Value.of_list of_pair ans |] in
Proofview.tclOR (return ans) (fun _ -> of_ans s)
in
- pf_apply bt begin fun env sigma ->
+ pf_apply begin fun env sigma ->
let ans = Constr_matching.match_appsubterm env sigma pat c in
of_ans ans
end
end
-let () = define2 "pattern_matches_vect" pattern constr begin fun bt pat c ->
- pf_apply bt begin fun env sigma ->
+let () = define2 "pattern_matches_vect" pattern constr begin fun pat c ->
+ pf_apply begin fun env sigma ->
let ans =
try Some (Constr_matching.matches env sigma pat c)
with Constr_matching.PatternMatchingFailure -> None
in
begin match ans with
- | None -> Proofview.tclZERO (err_matchfailure bt)
+ | None -> fail err_matchfailure
| Some ans ->
let ans = Id.Map.bindings ans in
let ans = Array.map_of_list snd ans in
@@ -529,23 +534,23 @@ let () = define2 "pattern_matches_vect" pattern constr begin fun bt pat c ->
end
end
-let () = define2 "pattern_matches_subterm_vect" pattern constr begin fun bt pat c ->
+let () = define2 "pattern_matches_subterm_vect" pattern constr begin fun pat c ->
let open Constr_matching in
let rec of_ans s = match IStream.peek s with
- | IStream.Nil -> Proofview.tclZERO (err_matchfailure bt)
+ | IStream.Nil -> fail err_matchfailure
| IStream.Cons ({ m_sub = (_, sub); m_ctx }, s) ->
let ans = Id.Map.bindings sub in
let ans = Array.map_of_list snd ans in
let ans = Value.of_tuple [| Value.of_constr m_ctx; Value.of_array Value.of_constr ans |] in
Proofview.tclOR (return ans) (fun _ -> of_ans s)
in
- pf_apply bt begin fun env sigma ->
+ pf_apply begin fun env sigma ->
let ans = Constr_matching.match_appsubterm env sigma pat c in
of_ans ans
end
end
-let () = define2 "pattern_instantiate" constr constr begin fun _ ctx c ->
+let () = define2 "pattern_instantiate" constr constr begin fun ctx c ->
let ctx = EConstr.Unsafe.to_constr ctx in
let c = EConstr.Unsafe.to_constr c in
let ans = Termops.subst_meta [Constr_matching.special_meta, c] ctx in
@@ -554,7 +559,8 @@ end
(** Error *)
-let () = define1 "throw" exn begin fun bt (e, info) ->
+let () = define1 "throw" exn begin fun (e, info) ->
+ Tac2interp.get_backtrace >>= fun bt ->
let e = set_bt bt e in
Proofview.tclLIFT (Proofview.NonLogical.raise ~info e)
end
@@ -562,48 +568,50 @@ end
(** Control *)
(** exn -> 'a *)
-let () = define1 "zero" exn begin fun bt (e, info) ->
+let () = define1 "zero" exn begin fun (e, info) ->
+ Tac2interp.get_backtrace >>= fun bt ->
let e = set_bt bt e in
Proofview.tclZERO ~info e
end
(** (unit -> 'a) -> (exn -> 'a) -> 'a *)
-let () = define2 "plus" closure closure begin fun bt x k ->
- Proofview.tclOR (thaw bt x) (fun e -> k bt [Value.of_exn e])
+let () = define2 "plus" closure closure begin fun x k ->
+ Proofview.tclOR (thaw x) (fun e -> k [Value.of_exn e])
end
(** (unit -> 'a) -> 'a *)
-let () = define1 "once" closure begin fun bt f ->
- Proofview.tclONCE (thaw bt f)
+let () = define1 "once" closure begin fun f ->
+ Proofview.tclONCE (thaw f)
end
(** (unit -> unit) list -> unit *)
-let () = define1 "dispatch" (list closure) begin fun bt l ->
- let l = List.map (fun f -> Proofview.tclIGNORE (thaw bt f)) l in
+let () = define1 "dispatch" (list closure) begin fun l ->
+ let l = List.map (fun f -> Proofview.tclIGNORE (thaw f)) l in
Proofview.tclDISPATCH l >>= fun () -> return v_unit
end
(** (unit -> unit) list -> (unit -> unit) -> (unit -> unit) list -> unit *)
-let () = define3 "extend" (list closure) closure (list closure) begin fun bt lft tac rgt ->
- let lft = List.map (fun f -> Proofview.tclIGNORE (thaw bt f)) lft in
- let tac = Proofview.tclIGNORE (thaw bt tac) in
- let rgt = List.map (fun f -> Proofview.tclIGNORE (thaw bt f)) rgt in
+let () = define3 "extend" (list closure) closure (list closure) begin fun lft tac rgt ->
+ let lft = List.map (fun f -> Proofview.tclIGNORE (thaw f)) lft in
+ let tac = Proofview.tclIGNORE (thaw tac) in
+ let rgt = List.map (fun f -> Proofview.tclIGNORE (thaw f)) rgt in
Proofview.tclEXTEND lft tac rgt >>= fun () -> return v_unit
end
(** (unit -> unit) -> unit *)
-let () = define1 "enter" closure begin fun bt f ->
- let f = Proofview.tclIGNORE (thaw bt f) in
+let () = define1 "enter" closure begin fun f ->
+ let f = Proofview.tclIGNORE (thaw f) in
Proofview.tclINDEPENDENT f >>= fun () -> return v_unit
end
(** (unit -> 'a) -> ('a * ('exn -> 'a)) result *)
-let () = define1 "case" closure begin fun bt f ->
- Proofview.tclCASE (thaw bt f) >>= begin function
+let () = define1 "case" closure begin fun f ->
+ Proofview.tclCASE (thaw f) >>= begin function
| Proofview.Next (x, k) ->
- let k bt = function
+ let k = function
| [e] ->
let (e, info) = Value.to_exn e in
+ Tac2interp.get_backtrace >>= fun bt ->
let e = set_bt bt e in
k (e, info)
| _ -> assert false
@@ -614,31 +622,31 @@ let () = define1 "case" closure begin fun bt f ->
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)
+let () = define3 "focus" int int closure begin fun i j tac ->
+ Proofview.tclFOCUS i j (thaw tac)
end
(** unit -> unit *)
-let () = define0 "shelve" begin fun _ ->
+let () = define0 "shelve" begin
Proofview.shelve >>= fun () -> return v_unit
end
(** unit -> unit *)
-let () = define0 "shelve_unifiable" begin fun _ ->
+let () = define0 "shelve_unifiable" begin
Proofview.shelve_unifiable >>= fun () -> return v_unit
end
-let () = define1 "new_goal" int begin fun bt ev ->
+let () = define1 "new_goal" int begin fun ev ->
let ev = Evar.unsafe_of_int ev in
Proofview.tclEVARMAP >>= fun sigma ->
if Evd.mem sigma ev then
Proofview.Unsafe.tclNEWGOALS [ev] <*> Proofview.tclUNIT v_unit
- else throw bt err_notfound
+ else throw err_notfound
end
(** unit -> constr *)
-let () = define0 "goal" begin fun bt ->
- assert_focussed bt >>= fun () ->
+let () = define0 "goal" begin
+ assert_focussed >>= fun () ->
Proofview.Goal.enter_one begin fun gl ->
let concl = Tacmach.New.pf_nf_concl gl in
return (Value.of_constr concl)
@@ -646,8 +654,8 @@ let () = define0 "goal" begin fun bt ->
end
(** ident -> constr *)
-let () = define1 "hyp" ident begin fun bt id ->
- pf_apply bt begin fun env _ ->
+let () = define1 "hyp" ident begin fun id ->
+ pf_apply begin fun env _ ->
let mem = try ignore (Environ.lookup_named id env); true with Not_found -> false in
if mem then return (Value.of_constr (EConstr.mkVar id))
else Tacticals.New.tclZEROMSG
@@ -655,8 +663,8 @@ let () = define1 "hyp" ident begin fun bt id ->
end
end
-let () = define0 "hyps" begin fun bt ->
- pf_apply bt begin fun env _ ->
+let () = define0 "hyps" begin
+ pf_apply begin fun env _ ->
let open Context.Named.Declaration in
let hyps = List.rev (Environ.named_context env) in
let map = function
@@ -673,52 +681,52 @@ let () = define0 "hyps" begin fun bt ->
end
(** (unit -> constr) -> unit *)
-let () = define1 "refine" closure begin fun bt c ->
- let c = thaw bt c >>= fun c -> Proofview.tclUNIT ((), Value.to_constr c) in
+let () = define1 "refine" closure begin fun c ->
+ let c = thaw c >>= fun c -> Proofview.tclUNIT ((), Value.to_constr c) in
Proofview.Goal.enter begin fun gl ->
let gl = Proofview.Goal.assume gl in
Refine.generic_refine ~typecheck:true c gl
end >>= fun () -> return v_unit
end
-let () = define2 "with_holes" closure closure begin fun bt x f ->
+let () = define2 "with_holes" closure closure begin fun x f ->
Proofview.tclEVARMAP >>= fun sigma0 ->
- thaw bt x >>= fun ans ->
+ thaw x >>= fun ans ->
Proofview.tclEVARMAP >>= fun sigma ->
Proofview.Unsafe.tclEVARS sigma0 >>= fun () ->
- Tacticals.New.tclWITHHOLES false (f bt [ans]) sigma
+ Tacticals.New.tclWITHHOLES false (f [ans]) sigma
end
-let () = define1 "progress" closure begin fun bt f ->
- Proofview.tclPROGRESS (thaw bt f)
+let () = define1 "progress" closure begin fun f ->
+ Proofview.tclPROGRESS (thaw f)
end
-let () = define2 "abstract" (option ident) closure begin fun bt id f ->
- Tactics.tclABSTRACT id (Proofview.tclIGNORE (thaw bt f)) >>= fun () ->
+let () = define2 "abstract" (option ident) closure begin fun id f ->
+ Tactics.tclABSTRACT id (Proofview.tclIGNORE (thaw f)) >>= fun () ->
return v_unit
end
-let () = define2 "time" (option string) closure begin fun bt s f ->
- Proofview.tclTIME s (thaw bt f)
+let () = define2 "time" (option string) closure begin fun s f ->
+ Proofview.tclTIME s (thaw f)
end
-let () = define0 "check_interrupt" begin fun bt ->
+let () = define0 "check_interrupt" begin
Proofview.tclCHECKINTERRUPT >>= fun () -> return v_unit
end
(** Fresh *)
-let () = define2 "fresh_free_union" (repr_ext val_free) (repr_ext val_free) begin fun _ set1 set2 ->
+let () = define2 "fresh_free_union" (repr_ext val_free) (repr_ext val_free) begin fun set1 set2 ->
let ans = Id.Set.union set1 set2 in
return (Value.of_ext Value.val_free ans)
end
-let () = define1 "fresh_free_of_ids" (list ident) begin fun _ ids ->
+let () = define1 "fresh_free_of_ids" (list ident) begin fun ids ->
let free = List.fold_right Id.Set.add ids Id.Set.empty in
return (Value.of_ext Value.val_free free)
end
-let () = define1 "fresh_free_of_constr" constr begin fun _ c ->
+let () = define1 "fresh_free_of_constr" constr begin fun c ->
Proofview.tclEVARMAP >>= fun sigma ->
let rec fold accu c = match EConstr.kind sigma c with
| Constr.Var id -> Id.Set.add id accu
@@ -728,7 +736,7 @@ let () = define1 "fresh_free_of_constr" constr begin fun _ c ->
return (Value.of_ext Value.val_free ans)
end
-let () = define2 "fresh_fresh" (repr_ext val_free) ident begin fun _ avoid id ->
+let () = define2 "fresh_fresh" (repr_ext val_free) ident begin fun avoid id ->
let nid = Namegen.next_ident_away_from id (fun id -> Id.Set.mem id avoid) in
return (Value.of_ident nid)
end
@@ -769,9 +777,8 @@ let intern_constr self ist c =
let interp_constr flags ist c =
let open Pretyping in
- let bt = ist.env_bkt in
let ist = to_lvar ist in
- pf_apply bt begin fun env sigma ->
+ pf_apply begin fun env sigma ->
Proofview.V82.wrap_exceptions begin fun () ->
let (sigma, c) = understand_ltac flags env sigma ist WithoutTypeConstraint c in
let c = ValExt (Value.val_constr, c) in
@@ -865,7 +872,7 @@ let () =
GlbVal tac, gtypref t_unit
in
let interp ist tac =
- let ist = { ist with env_ist = Id.Map.empty } in
+ let ist = { env_ist = Id.Map.empty } in
let lfun = Tac2interp.set_env ist Id.Map.empty in
let ist = Ltac_plugin.Tacinterp.default_ist () in
(** FUCK YOU API *)
@@ -911,8 +918,8 @@ let () =
(** FUCK YOU API *)
let idtac = (Obj.magic idtac : Geninterp.Val.t) in
let interp ist tac =
- let ist = Tac2interp.get_env ist.Geninterp.lfun in
- let ist = { ist with env_ist = Id.Map.empty } in
+(* let ist = Tac2interp.get_env ist.Geninterp.lfun in *)
+ let ist = { env_ist = Id.Map.empty } in
Tac2interp.interp ist tac >>= fun _ ->
Ftactic.return idtac
in
diff --git a/src/tac2core.mli b/src/tac2core.mli
index b5800a7172..9fae65bb3e 100644
--- a/src/tac2core.mli
+++ b/src/tac2core.mli
@@ -27,4 +27,4 @@ val c_false : ltac_constructor
end
-val pf_apply : backtrace -> (Environ.env -> Evd.evar_map -> 'a Proofview.tactic) -> 'a Proofview.tactic
+val pf_apply : (Environ.env -> Evd.evar_map -> 'a Proofview.tactic) -> 'a Proofview.tactic
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 97e1fe8e8e..eed7eb6def 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -748,14 +748,12 @@ let register_struct ?local str = match str with
(** Toplevel exception *)
-let print_ltac2_backtrace = ref false
-
let _ = Goptions.declare_bool_option {
Goptions.optdepr = false;
Goptions.optname = "print Ltac2 backtrace";
Goptions.optkey = ["Ltac2"; "Backtrace"];
- Goptions.optread = (fun () -> !print_ltac2_backtrace);
- Goptions.optwrite = (fun b -> print_ltac2_backtrace := b);
+ Goptions.optread = (fun () -> !Tac2interp.print_ltac2_backtrace);
+ Goptions.optwrite = (fun b -> Tac2interp.print_ltac2_backtrace := b);
}
let pr_frame = function
@@ -773,7 +771,7 @@ let () = register_handler begin function
| Tac2interp.LtacError (kn, _, bt) ->
let c = Tac2print.pr_constructor kn in (** FIXME *)
let bt =
- if !print_ltac2_backtrace then
+ if !Tac2interp.print_ltac2_backtrace then
fnl () ++ str "Backtrace:" ++ fnl () ++ prlist_with_sep fnl pr_frame bt
else
mt ()
diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index 1b4a704b11..77e2cfef0e 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -201,9 +201,8 @@ type valexpr =
| ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr
(** Arbitrary data *)
-and ml_tactic = backtrace -> valexpr list -> valexpr Proofview.tactic
+and ml_tactic = valexpr list -> valexpr Proofview.tactic
type environment = {
env_ist : valexpr Id.Map.t;
- env_bkt : backtrace;
}
diff --git a/src/tac2interp.ml b/src/tac2interp.ml
index 08cebc0af0..f37b4f8e9c 100644
--- a/src/tac2interp.ml
+++ b/src/tac2interp.ml
@@ -16,9 +16,34 @@ open Tac2expr
exception LtacError = Tac2ffi.LtacError
+let backtrace : backtrace Evd.Store.field = Evd.Store.field ()
+
+let print_ltac2_backtrace = ref false
+
+let get_backtrace =
+ Proofview.tclEVARMAP >>= fun sigma ->
+ match Evd.Store.get (Evd.get_extra_data sigma) backtrace with
+ | None -> Proofview.tclUNIT []
+ | Some bt -> Proofview.tclUNIT bt
+
+let set_backtrace bt =
+ Proofview.tclEVARMAP >>= fun sigma ->
+ let store = Evd.get_extra_data sigma in
+ let store = Evd.Store.set store backtrace bt in
+ let sigma = Evd.set_extra_data store sigma in
+ Proofview.Unsafe.tclEVARS sigma
+
+let with_frame frame tac =
+ if !print_ltac2_backtrace then
+ get_backtrace >>= fun bt ->
+ set_backtrace (frame :: bt) >>= fun () ->
+ tac >>= fun ans ->
+ set_backtrace bt >>= fun () ->
+ Proofview.tclUNIT ans
+ else tac
+
let empty_environment = {
env_ist = Id.Map.empty;
- env_bkt = [];
}
type closure = {
@@ -34,7 +59,7 @@ type closure = {
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 }
+| Name id -> { env_ist = Id.Map.add id v ist.env_ist }
let get_var ist id =
try Id.Map.find id ist.env_ist with Not_found ->
@@ -63,7 +88,7 @@ let rec interp (ist : environment) = function
| GTacApp (f, args) ->
interp ist f >>= fun f ->
Proofview.Monad.List.map (fun e -> interp ist e) args >>= fun args ->
- Tac2ffi.to_closure f ist.env_bkt args
+ Tac2ffi.to_closure f args
| GTacLet (false, el, e) ->
let fold accu (na, e) =
interp ist e >>= fun e ->
@@ -82,7 +107,7 @@ let rec interp (ist : environment) = function
let fixs = List.map map el in
let fold accu (na, _, cls) = match na with
| Anonymous -> accu
- | Name id -> { ist with env_ist = Id.Map.add id cls accu.env_ist }
+ | Name id -> { 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 *)
@@ -108,25 +133,24 @@ let rec interp (ist : environment) = function
return (ValOpn (kn, Array.of_list el))
| GTacPrm (ml, el) ->
Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el ->
- Tac2env.interp_primitive ml (FrPrim ml :: ist.env_bkt) el
+ with_frame (FrPrim ml) (Tac2env.interp_primitive ml el)
| GTacExt (tag, e) ->
let tpe = Tac2env.interp_ml_object tag in
- let ist = { ist with env_bkt = FrExtn (tag, e) :: ist.env_bkt } in
- tpe.Tac2env.ml_interp ist e
+ with_frame (FrExtn (tag, e)) (tpe.Tac2env.ml_interp ist e)
-and interp_app f = (); fun bt args -> match f with
+and interp_app f = (); fun 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
+ | [], [] -> with_frame (FrLtac kn) (interp ist e)
| [], _ :: _ ->
- interp ist e >>= fun f -> Tac2ffi.to_closure f bt args
+ with_frame (FrLtac kn) (interp ist e) >>= fun f -> Tac2ffi.to_closure f args
| _ :: _, [] ->
let cls = { clos_ref = kn; clos_env = ist.env_ist; clos_var = ids; clos_exp = e } in
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
+ push { env_ist = ist } ids args
and interp_case ist e cse0 cse1 = match e with
| ValInt n -> interp ist cse0.(n)
diff --git a/src/tac2interp.mli b/src/tac2interp.mli
index 48af59b178..1003e9f1eb 100644
--- a/src/tac2interp.mli
+++ b/src/tac2interp.mli
@@ -24,3 +24,11 @@ val set_env : environment -> Glob_term.unbound_ltac_var_map -> Glob_term.unbound
exception LtacError of KerName.t * valexpr array * backtrace
(** Ltac2-defined exceptions seen from OCaml side *)
+
+(** {5 Backtrace} *)
+
+val get_backtrace : backtrace Proofview.tactic
+
+val with_frame : frame -> 'a Proofview.tactic -> 'a Proofview.tactic
+
+val print_ltac2_backtrace : bool ref
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 14ad8695ca..28bcd6a1cf 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 = (Value.to_closure f) bt [v_unit]
+let thaw f = Value.to_closure f [v_unit]
let to_pair f g = function
| ValBlk (0, [| x; y |]) -> (f x, g y)
@@ -126,8 +126,7 @@ and to_intro_patterns il =
let to_destruction_arg = function
| ValBlk (0, [| c |]) ->
- (** FIXME: lost backtrace *)
- let c = thaw [] c >>= fun c -> return (to_constr_with_bindings c) in
+ let c = thaw c >>= fun c -> return (to_constr_with_bindings c) in
None, ElimOnConstr c
| ValBlk (1, [| id |]) -> None, ElimOnIdent (Loc.tag (Value.to_ident id))
| ValBlk (2, [| n |]) -> None, ElimOnAnonHyp (Value.to_int n)
@@ -155,7 +154,7 @@ let to_rewriting = function
let orient = Value.to_option Value.to_bool orient in
let repeat = to_multi repeat in
(** FIXME: lost backtrace *)
- let c = thaw [] c >>= fun c -> return (to_constr_with_bindings c) in
+ let c = thaw c >>= fun c -> return (to_constr_with_bindings c) in
(orient, repeat, c)
| _ -> assert false
@@ -190,59 +189,59 @@ let pname s = { mltac_plugin = "ltac2"; mltac_tactic = s }
let lift tac = tac <*> return v_unit
let define_prim0 name tac =
- let tac bt arg = match arg with
+ let tac arg = match arg with
| [_] -> lift tac
| _ -> assert false
in
Tac2env.define_primitive (pname name) tac
let define_prim1 name tac =
- let tac bt arg = match arg with
- | [x] -> lift (tac bt x)
+ let tac arg = match arg with
+ | [x] -> lift (tac x)
| _ -> assert false
in
Tac2env.define_primitive (pname name) tac
let define_prim2 name tac =
- let tac bt arg = match arg with
- | [x; y] -> lift (tac bt x y)
+ let tac arg = match arg with
+ | [x; y] -> lift (tac x y)
| _ -> assert false
in
Tac2env.define_primitive (pname name) tac
let define_prim3 name tac =
- let tac bt arg = match arg with
- | [x; y; z] -> lift (tac bt x y z)
+ let tac arg = match arg with
+ | [x; y; z] -> lift (tac x y z)
| _ -> assert false
in
Tac2env.define_primitive (pname name) tac
let define_prim4 name tac =
- let tac bt arg = match arg with
- | [x; y; z; u] -> lift (tac bt x y z u)
+ let tac arg = match arg with
+ | [x; y; z; u] -> lift (tac x y z u)
| _ -> assert false
in
Tac2env.define_primitive (pname name) tac
let define_prim5 name tac =
- let tac bt arg = match arg with
- | [x; y; z; u; v] -> lift (tac bt x y z u v)
+ let tac arg = match arg with
+ | [x; y; z; u; v] -> lift (tac x y z u v)
| _ -> assert false
in
Tac2env.define_primitive (pname name) tac
(** Tactics from Tacexpr *)
-let () = define_prim2 "tac_intros" begin fun _ ev ipat ->
+let () = define_prim2 "tac_intros" begin fun ev ipat ->
let ev = Value.to_bool ev in
let ipat = to_intro_patterns ipat in
Tactics.intros_patterns ev ipat
end
-let () = define_prim4 "tac_apply" begin fun bt adv ev cb ipat ->
+let () = define_prim4 "tac_apply" begin fun adv ev cb ipat ->
let adv = Value.to_bool adv in
let ev = Value.to_bool ev in
- let map_cb c = thaw bt c >>= fun c -> return (to_constr_with_bindings c) in
+ let map_cb c = thaw c >>= fun c -> return (to_constr_with_bindings c) in
let cb = Value.to_list map_cb cb in
let map p = Value.to_option (fun p -> Loc.tag (to_intro_pattern p)) p in
let map_ipat p = to_pair Value.to_ident map p in
@@ -250,20 +249,20 @@ let () = define_prim4 "tac_apply" begin fun bt adv ev cb ipat ->
Tac2tactics.apply adv ev cb ipat
end
-let () = define_prim3 "tac_elim" begin fun _ ev c copt ->
+let () = define_prim3 "tac_elim" begin fun ev c copt ->
let ev = Value.to_bool ev in
let c = to_constr_with_bindings c in
let copt = Value.to_option to_constr_with_bindings copt in
Tactics.elim ev None c copt
end
-let () = define_prim2 "tac_case" begin fun _ ev c ->
+let () = define_prim2 "tac_case" begin fun ev c ->
let ev = Value.to_bool ev in
let c = to_constr_with_bindings c in
Tactics.general_case_analysis ev None c
end
-let () = define_prim1 "tac_generalize" begin fun _ cl ->
+let () = define_prim1 "tac_generalize" begin fun cl ->
let cast = function
| ValBlk (0, [| c; occs; na |]) ->
((to_occurrences Value.to_int occs, Value.to_constr c), to_name na)
@@ -273,113 +272,113 @@ let () = define_prim1 "tac_generalize" begin fun _ cl ->
Tactics.new_generalize_gen cl
end
-let () = define_prim3 "tac_assert" begin fun bt c tac ipat ->
+let () = define_prim3 "tac_assert" begin fun c tac ipat ->
let c = Value.to_constr c in
- let of_tac t = Proofview.tclIGNORE (thaw bt t) in
+ let of_tac t = Proofview.tclIGNORE (thaw t) in
let tac = Value.to_option (fun t -> Value.to_option of_tac t) tac in
let ipat = Value.to_option (fun ipat -> Loc.tag (to_intro_pattern ipat)) ipat in
Tactics.forward true tac ipat c
end
-let () = define_prim3 "tac_enough" begin fun bt c tac ipat ->
+let () = define_prim3 "tac_enough" begin fun c tac ipat ->
let c = Value.to_constr c in
- let of_tac t = Proofview.tclIGNORE (thaw bt t) in
+ let of_tac t = Proofview.tclIGNORE (thaw t) in
let tac = Value.to_option (fun t -> Value.to_option of_tac t) tac in
let ipat = Value.to_option (fun ipat -> Loc.tag (to_intro_pattern ipat)) ipat in
Tactics.forward false tac ipat c
end
-let () = define_prim2 "tac_pose" begin fun _ idopt c ->
+let () = define_prim2 "tac_pose" begin fun idopt c ->
let na = to_name idopt in
let c = Value.to_constr c in
Tactics.letin_tac None na c None Locusops.nowhere
end
-let () = define_prim4 "tac_set" begin fun bt ev idopt c cl ->
+let () = define_prim4 "tac_set" begin fun ev idopt c cl ->
let ev = Value.to_bool ev in
let na = to_name idopt in
let cl = to_clause cl in
Proofview.tclEVARMAP >>= fun sigma ->
- thaw bt c >>= fun c ->
+ thaw c >>= fun c ->
let c = Value.to_constr c in
Tactics.letin_pat_tac ev None na (sigma, c) cl
end
-let () = define_prim3 "tac_destruct" begin fun _ ev ic using ->
+let () = define_prim3 "tac_destruct" begin fun ev ic using ->
let ev = Value.to_bool ev in
let ic = Value.to_list to_induction_clause ic in
let using = Value.to_option to_constr_with_bindings using in
Tac2tactics.induction_destruct false ev ic using
end
-let () = define_prim3 "tac_induction" begin fun _ ev ic using ->
+let () = define_prim3 "tac_induction" begin fun ev ic using ->
let ev = Value.to_bool ev in
let ic = Value.to_list to_induction_clause ic in
let using = Value.to_option to_constr_with_bindings using in
Tac2tactics.induction_destruct true ev ic using
end
-let () = define_prim1 "tac_red" begin fun _ cl ->
+let () = define_prim1 "tac_red" begin fun cl ->
let cl = to_clause cl in
Tactics.reduce (Red false) cl
end
-let () = define_prim1 "tac_hnf" begin fun _ cl ->
+let () = define_prim1 "tac_hnf" begin fun cl ->
let cl = to_clause cl in
Tactics.reduce Hnf cl
end
-let () = define_prim3 "tac_simpl" begin fun _ flags where cl ->
+let () = define_prim3 "tac_simpl" begin fun flags where cl ->
let flags = to_red_flag flags in
let where = Value.to_option to_pattern_with_occs where in
let cl = to_clause cl in
Tac2tactics.simpl flags where cl
end
-let () = define_prim2 "tac_cbv" begin fun _ flags cl ->
+let () = define_prim2 "tac_cbv" begin fun flags cl ->
let flags = to_red_flag flags in
let cl = to_clause cl in
Tac2tactics.cbv flags cl
end
-let () = define_prim2 "tac_cbn" begin fun _ flags cl ->
+let () = define_prim2 "tac_cbn" begin fun flags cl ->
let flags = to_red_flag flags in
let cl = to_clause cl in
Tac2tactics.cbn flags cl
end
-let () = define_prim2 "tac_lazy" begin fun _ flags cl ->
+let () = define_prim2 "tac_lazy" begin fun flags cl ->
let flags = to_red_flag flags in
let cl = to_clause cl in
Tac2tactics.lazy_ flags cl
end
-let () = define_prim2 "tac_unfold" begin fun _ refs cl ->
+let () = define_prim2 "tac_unfold" begin fun refs cl ->
let map v = to_pair Value.to_reference (fun occ -> to_occurrences to_int_or_var occ) v in
let refs = Value.to_list map refs in
let cl = to_clause cl in
Tac2tactics.unfold refs cl
end
-let () = define_prim2 "tac_fold" begin fun _ args cl ->
+let () = define_prim2 "tac_fold" begin fun args cl ->
let args = Value.to_list Value.to_constr args in
let cl = to_clause cl in
Tactics.reduce (Fold args) cl
end
-let () = define_prim2 "tac_pattern" begin fun _ where cl ->
+let () = define_prim2 "tac_pattern" begin fun where cl ->
let where = Value.to_list to_constr_with_occs where in
let cl = to_clause cl in
Tactics.reduce (Pattern where) cl
end
-let () = define_prim2 "tac_vm" begin fun _ where cl ->
+let () = define_prim2 "tac_vm" begin fun where cl ->
let where = Value.to_option to_pattern_with_occs where in
let cl = to_clause cl in
Tac2tactics.vm where cl
end
-let () = define_prim2 "tac_native" begin fun _ where cl ->
+let () = define_prim2 "tac_native" begin fun where cl ->
let where = Value.to_option to_pattern_with_occs where in
let cl = to_clause cl in
Tac2tactics.native where cl
@@ -388,102 +387,102 @@ end
(** Reduction functions *)
let define_red1 name tac =
- let tac bt arg = match arg with
- | [x] -> tac bt x >>= fun c -> Proofview.tclUNIT (Value.of_constr c)
+ let tac arg = match arg with
+ | [x] -> tac x >>= fun c -> Proofview.tclUNIT (Value.of_constr c)
| _ -> assert false
in
Tac2env.define_primitive (pname name) tac
let define_red2 name tac =
- let tac bt arg = match arg with
- | [x; y] -> tac bt x y >>= fun c -> Proofview.tclUNIT (Value.of_constr c)
+ let tac arg = match arg with
+ | [x; y] -> tac x y >>= fun c -> Proofview.tclUNIT (Value.of_constr c)
| _ -> assert false
in
Tac2env.define_primitive (pname name) tac
let define_red3 name tac =
- let tac bt arg = match arg with
- | [x; y; z] -> tac bt x y z >>= fun c -> Proofview.tclUNIT (Value.of_constr c)
+ let tac arg = match arg with
+ | [x; y; z] -> tac x y z >>= fun c -> Proofview.tclUNIT (Value.of_constr c)
| _ -> assert false
in
Tac2env.define_primitive (pname name) tac
-let () = define_red1 "eval_red" begin fun bt c ->
+let () = define_red1 "eval_red" begin fun c ->
let c = Value.to_constr c in
- Tac2tactics.eval_red bt c
+ Tac2tactics.eval_red c
end
-let () = define_red1 "eval_hnf" begin fun bt c ->
+let () = define_red1 "eval_hnf" begin fun c ->
let c = Value.to_constr c in
- Tac2tactics.eval_hnf bt c
+ Tac2tactics.eval_hnf c
end
-let () = define_red3 "eval_simpl" begin fun bt flags where c ->
+let () = define_red3 "eval_simpl" begin fun flags where c ->
let flags = to_red_flag flags in
let where = Value.to_option to_pattern_with_occs where in
let c = Value.to_constr c in
- Tac2tactics.eval_simpl bt flags where c
+ Tac2tactics.eval_simpl flags where c
end
-let () = define_red2 "eval_cbv" begin fun bt flags c ->
+let () = define_red2 "eval_cbv" begin fun flags c ->
let flags = to_red_flag flags in
let c = Value.to_constr c in
- Tac2tactics.eval_cbv bt flags c
+ Tac2tactics.eval_cbv flags c
end
-let () = define_red2 "eval_cbn" begin fun bt flags c ->
+let () = define_red2 "eval_cbn" begin fun flags c ->
let flags = to_red_flag flags in
let c = Value.to_constr c in
- Tac2tactics.eval_cbn bt flags c
+ Tac2tactics.eval_cbn flags c
end
-let () = define_red2 "eval_lazy" begin fun bt flags c ->
+let () = define_red2 "eval_lazy" begin fun flags c ->
let flags = to_red_flag flags in
let c = Value.to_constr c in
- Tac2tactics.eval_lazy bt flags c
+ Tac2tactics.eval_lazy flags c
end
-let () = define_red2 "eval_unfold" begin fun bt refs c ->
+let () = define_red2 "eval_unfold" begin fun refs c ->
let map v = to_pair Value.to_reference (fun occ -> to_occurrences to_int_or_var occ) v in
let refs = Value.to_list map refs in
let c = Value.to_constr c in
- Tac2tactics.eval_unfold bt refs c
+ Tac2tactics.eval_unfold refs c
end
-let () = define_red2 "eval_fold" begin fun bt args c ->
+let () = define_red2 "eval_fold" begin fun args c ->
let args = Value.to_list Value.to_constr args in
let c = Value.to_constr c in
- Tac2tactics.eval_fold bt args c
+ Tac2tactics.eval_fold args c
end
-let () = define_red2 "eval_pattern" begin fun bt where c ->
+let () = define_red2 "eval_pattern" begin fun where c ->
let where = Value.to_list (fun p -> to_pair Value.to_constr (fun occ -> to_occurrences to_int_or_var occ) p) where in
let c = Value.to_constr c in
- Tac2tactics.eval_pattern bt where c
+ Tac2tactics.eval_pattern where c
end
-let () = define_red2 "eval_vm" begin fun bt where c ->
+let () = define_red2 "eval_vm" begin fun where c ->
let where = Value.to_option to_pattern_with_occs where in
let c = Value.to_constr c in
- Tac2tactics.eval_vm bt where c
+ Tac2tactics.eval_vm where c
end
-let () = define_red2 "eval_native" begin fun bt where c ->
+let () = define_red2 "eval_native" begin fun where c ->
let where = Value.to_option to_pattern_with_occs where in
let c = Value.to_constr c in
- Tac2tactics.eval_native bt where c
+ Tac2tactics.eval_native where c
end
-let () = define_prim4 "tac_rewrite" begin fun bt ev rw cl by ->
+let () = define_prim4 "tac_rewrite" begin fun ev rw cl by ->
let ev = Value.to_bool ev in
let rw = Value.to_list to_rewriting rw in
let cl = to_clause cl in
- let to_tac t = Proofview.tclIGNORE (thaw bt t) in
+ let to_tac t = Proofview.tclIGNORE (thaw t) in
let by = Value.to_option to_tac by in
Tac2tactics.rewrite ev rw cl by
end
-let () = define_prim4 "tac_inversion" begin fun bt knd arg pat ids ->
+let () = define_prim4 "tac_inversion" begin fun knd arg pat ids ->
let knd = to_inversion_kind knd in
let arg = to_destruction_arg arg in
let pat = Value.to_option (fun ipat -> Loc.tag (to_intro_pattern ipat)) pat in
@@ -495,13 +494,13 @@ end
let () = define_prim0 "tac_reflexivity" Tactics.intros_reflexivity
-let () = define_prim2 "tac_move" begin fun _ id mv ->
+let () = define_prim2 "tac_move" begin fun id mv ->
let id = Value.to_ident id in
let mv = to_move_location mv in
Tactics.move_hyp id mv
end
-let () = define_prim2 "tac_intro" begin fun _ id mv ->
+let () = define_prim2 "tac_intro" begin fun id mv ->
let id = Value.to_option Value.to_ident id in
let mv = Value.to_option to_move_location mv in
let mv = Option.default MoveLast mv in
@@ -518,69 +517,69 @@ END
let () = define_prim0 "tac_assumption" Tactics.assumption
-let () = define_prim1 "tac_transitivity" begin fun _ c ->
+let () = define_prim1 "tac_transitivity" begin fun c ->
let c = Value.to_constr c in
Tactics.intros_transitivity (Some c)
end
let () = define_prim0 "tac_etransitivity" (Tactics.intros_transitivity None)
-let () = define_prim1 "tac_cut" begin fun _ c ->
+let () = define_prim1 "tac_cut" begin fun c ->
let c = Value.to_constr c in
Tactics.cut c
end
-let () = define_prim2 "tac_left" begin fun _ ev bnd ->
+let () = define_prim2 "tac_left" begin fun ev bnd ->
let ev = Value.to_bool ev in
let bnd = to_bindings bnd in
Tactics.left_with_bindings ev bnd
end
-let () = define_prim2 "tac_right" begin fun _ ev bnd ->
+let () = define_prim2 "tac_right" begin fun ev bnd ->
let ev = Value.to_bool ev in
let bnd = to_bindings bnd in
Tactics.right_with_bindings ev bnd
end
-let () = define_prim1 "tac_introsuntil" begin fun _ h ->
+let () = define_prim1 "tac_introsuntil" begin fun h ->
Tactics.intros_until (to_qhyp h)
end
-let () = define_prim1 "tac_exactnocheck" begin fun _ c ->
+let () = define_prim1 "tac_exactnocheck" begin fun c ->
Tactics.exact_no_check (Value.to_constr c)
end
-let () = define_prim1 "tac_vmcastnocheck" begin fun _ c ->
+let () = define_prim1 "tac_vmcastnocheck" begin fun c ->
Tactics.vm_cast_no_check (Value.to_constr c)
end
-let () = define_prim1 "tac_nativecastnocheck" begin fun _ c ->
+let () = define_prim1 "tac_nativecastnocheck" begin fun c ->
Tactics.native_cast_no_check (Value.to_constr c)
end
-let () = define_prim1 "tac_constructor" begin fun _ ev ->
+let () = define_prim1 "tac_constructor" begin fun ev ->
let ev = Value.to_bool ev in
Tactics.any_constructor ev None
end
-let () = define_prim3 "tac_constructorn" begin fun _ ev n bnd ->
+let () = define_prim3 "tac_constructorn" begin fun ev n bnd ->
let ev = Value.to_bool ev in
let n = Value.to_int n in
let bnd = to_bindings bnd in
Tactics.constructor_tac ev None n bnd
end
-let () = define_prim1 "tac_symmetry" begin fun _ cl ->
+let () = define_prim1 "tac_symmetry" begin fun cl ->
let cl = to_clause cl in
Tactics.intros_symmetry cl
end
-let () = define_prim2 "tac_split" begin fun _ ev bnd ->
+let () = define_prim2 "tac_split" begin fun ev bnd ->
let ev = Value.to_bool ev in
let bnd = to_bindings bnd in
Tactics.split_with_bindings ev [bnd]
end
-let () = define_prim1 "tac_rename" begin fun _ ids ->
+let () = define_prim1 "tac_rename" begin fun ids ->
let map c = match Value.to_tuple c with
| [|x; y|] -> (Value.to_ident x, Value.to_ident y)
| _ -> assert false
@@ -589,72 +588,72 @@ let () = define_prim1 "tac_rename" begin fun _ ids ->
Tactics.rename_hyp ids
end
-let () = define_prim1 "tac_revert" begin fun _ ids ->
+let () = define_prim1 "tac_revert" begin fun ids ->
let ids = Value.to_list Value.to_ident ids in
Tactics.revert ids
end
let () = define_prim0 "tac_admit" Proofview.give_up
-let () = define_prim2 "tac_fix" begin fun _ idopt n ->
+let () = define_prim2 "tac_fix" begin fun idopt n ->
let idopt = Value.to_option Value.to_ident idopt in
let n = Value.to_int n in
Tactics.fix idopt n
end
-let () = define_prim1 "tac_cofix" begin fun _ idopt ->
+let () = define_prim1 "tac_cofix" begin fun idopt ->
let idopt = Value.to_option Value.to_ident idopt in
Tactics.cofix idopt
end
-let () = define_prim1 "tac_clear" begin fun _ ids ->
+let () = define_prim1 "tac_clear" begin fun ids ->
let ids = Value.to_list Value.to_ident ids in
Tactics.clear ids
end
-let () = define_prim1 "tac_keep" begin fun _ ids ->
+let () = define_prim1 "tac_keep" begin fun ids ->
let ids = Value.to_list Value.to_ident ids in
Tactics.keep ids
end
-let () = define_prim1 "tac_clearbody" begin fun _ ids ->
+let () = define_prim1 "tac_clearbody" begin fun ids ->
let ids = Value.to_list Value.to_ident ids in
Tactics.clear_body ids
end
(** Tactics from extratactics *)
-let () = define_prim2 "tac_discriminate" begin fun _ ev arg ->
+let () = define_prim2 "tac_discriminate" begin fun ev arg ->
let ev = Value.to_bool ev in
let arg = Value.to_option to_destruction_arg arg in
Tac2tactics.discriminate ev arg
end
-let () = define_prim3 "tac_injection" begin fun _ ev ipat arg ->
+let () = define_prim3 "tac_injection" begin fun ev ipat arg ->
let ev = Value.to_bool ev in
let ipat = Value.to_option to_intro_patterns ipat in
let arg = Value.to_option to_destruction_arg arg in
Tac2tactics.injection ev ipat arg
end
-let () = define_prim1 "tac_absurd" begin fun _ c ->
+let () = define_prim1 "tac_absurd" begin fun c ->
Contradiction.absurd (Value.to_constr c)
end
-let () = define_prim1 "tac_contradiction" begin fun _ c ->
+let () = define_prim1 "tac_contradiction" begin fun c ->
let c = Value.to_option to_constr_with_bindings c in
Contradiction.contradiction c
end
-let () = define_prim4 "tac_autorewrite" begin fun bt all by ids cl ->
+let () = define_prim4 "tac_autorewrite" begin fun all by ids cl ->
let all = Value.to_bool all in
- let by = Value.to_option (fun tac -> Proofview.tclIGNORE (thaw bt tac)) by in
+ let by = Value.to_option (fun tac -> Proofview.tclIGNORE (thaw tac)) by in
let ids = Value.to_list Value.to_ident ids in
let cl = to_clause cl in
Tac2tactics.autorewrite ~all by ids cl
end
-let () = define_prim1 "tac_subst" begin fun _ ids ->
+let () = define_prim1 "tac_subst" begin fun ids ->
let ids = Value.to_list Value.to_ident ids in
Equality.subst ids
end
@@ -663,43 +662,43 @@ let () = define_prim0 "tac_substall" (return () >>= fun () -> Equality.subst_all
(** Auto *)
-let () = define_prim3 "tac_trivial" begin fun bt dbg lems dbs ->
+let () = define_prim3 "tac_trivial" begin fun dbg lems dbs ->
let dbg = to_debug dbg in
- let map c = thaw bt c >>= fun c -> return (Value.to_constr c) in
+ let map c = thaw c >>= fun c -> return (Value.to_constr c) in
let lems = Value.to_list map lems in
let dbs = Value.to_option (fun l -> Value.to_list Value.to_ident l) dbs in
Tac2tactics.trivial dbg lems dbs
end
-let () = define_prim5 "tac_eauto" begin fun bt dbg n p lems dbs ->
+let () = define_prim5 "tac_eauto" begin fun dbg n p lems dbs ->
let dbg = to_debug dbg in
let n = Value.to_option Value.to_int n in
let p = Value.to_option Value.to_int p in
- let map c = thaw bt c >>= fun c -> return (Value.to_constr c) in
+ let map c = thaw c >>= fun c -> return (Value.to_constr c) in
let lems = Value.to_list map lems in
let dbs = Value.to_option (fun l -> Value.to_list Value.to_ident l) dbs in
Tac2tactics.eauto dbg n p lems dbs
end
-let () = define_prim4 "tac_auto" begin fun bt dbg n lems dbs ->
+let () = define_prim4 "tac_auto" begin fun dbg n lems dbs ->
let dbg = to_debug dbg in
let n = Value.to_option Value.to_int n in
- let map c = thaw bt c >>= fun c -> return (Value.to_constr c) in
+ let map c = thaw c >>= fun c -> return (Value.to_constr c) in
let lems = Value.to_list map lems in
let dbs = Value.to_option (fun l -> Value.to_list Value.to_ident l) dbs in
Tac2tactics.auto dbg n lems dbs
end
-let () = define_prim4 "tac_newauto" begin fun bt dbg n lems dbs ->
+let () = define_prim4 "tac_newauto" begin fun dbg n lems dbs ->
let dbg = to_debug dbg in
let n = Value.to_option Value.to_int n in
- let map c = thaw bt c >>= fun c -> return (Value.to_constr c) in
+ let map c = thaw c >>= fun c -> return (Value.to_constr c) in
let lems = Value.to_list map lems in
let dbs = Value.to_option (fun l -> Value.to_list Value.to_ident l) dbs in
Tac2tactics.new_auto dbg n lems dbs
end
-let () = define_prim3 "tac_typeclasses_eauto" begin fun bt str n dbs ->
+let () = define_prim3 "tac_typeclasses_eauto" begin fun str n dbs ->
let str = Value.to_option to_strategy str in
let n = Value.to_option Value.to_int n in
let dbs = Value.to_option (fun l -> Value.to_list Value.to_ident l) dbs in
@@ -708,8 +707,8 @@ end
(** Firstorder *)
-let () = define_prim3 "tac_firstorder" begin fun bt tac refs ids ->
- let tac = Value.to_option (fun t -> Proofview.tclIGNORE (thaw bt t)) tac in
+let () = define_prim3 "tac_firstorder" begin fun tac refs ids ->
+ let tac = Value.to_option (fun t -> Proofview.tclIGNORE (thaw t)) tac in
let refs = Value.to_list Value.to_reference refs in
let ids = Value.to_list Value.to_ident ids in
Tac2tactics.firstorder tac refs ids
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index dacbb898d3..aa2ee4711a 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -122,62 +122,62 @@ let native where cl =
let where = Option.map map_pattern_with_occs where in
Tactics.reduce (CbvNative where) cl
-let eval_fun bt red c =
- Tac2core.pf_apply bt begin fun env sigma ->
+let eval_fun red c =
+ Tac2core.pf_apply begin fun env sigma ->
let (redfun, _) = Redexpr.reduction_of_red_expr env red in
let (sigma, ans) = redfun env sigma c in
Proofview.Unsafe.tclEVARS sigma >>= fun () ->
Proofview.tclUNIT ans
end
-let eval_red bt c =
- eval_fun bt (Red false) c
+let eval_red c =
+ eval_fun (Red false) c
-let eval_hnf bt c =
- eval_fun bt Hnf c
+let eval_hnf c =
+ eval_fun Hnf c
-let eval_simpl bt flags where c =
+let eval_simpl flags where c =
let where = Option.map map_pattern_with_occs where in
Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
let flags = { flags with rConst } in
- eval_fun bt (Simpl (flags, where)) c
+ eval_fun (Simpl (flags, where)) c
-let eval_cbv bt flags c =
+let eval_cbv flags c =
Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
let flags = { flags with rConst } in
- eval_fun bt (Cbv flags) c
+ eval_fun (Cbv flags) c
-let eval_cbn bt flags c =
+let eval_cbn flags c =
Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
let flags = { flags with rConst } in
- eval_fun bt (Cbn flags) c
+ eval_fun (Cbn flags) c
-let eval_lazy bt flags c =
+let eval_lazy flags c =
Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
let flags = { flags with rConst } in
- eval_fun bt (Lazy flags) c
+ eval_fun (Lazy flags) c
-let eval_unfold bt occs c =
+let eval_unfold occs c =
let map (gr, occ) =
get_evaluable_reference gr >>= fun gr -> Proofview.tclUNIT (occ, gr)
in
Proofview.Monad.List.map map occs >>= fun occs ->
- eval_fun bt (Unfold occs) c
+ eval_fun (Unfold occs) c
-let eval_fold bt cl c =
- eval_fun bt (Fold cl) c
+let eval_fold cl c =
+ eval_fun (Fold cl) c
-let eval_pattern bt where c =
+let eval_pattern where c =
let where = List.map (fun (pat, occ) -> (occ, pat)) where in
- eval_fun bt (Pattern where) c
+ eval_fun (Pattern where) c
-let eval_vm bt where c =
+let eval_vm where c =
let where = Option.map map_pattern_with_occs where in
- eval_fun bt (CbvVm where) c
+ eval_fun (CbvVm where) c
-let eval_native bt where c =
+let eval_native where c =
let where = Option.map map_pattern_with_occs where in
- eval_fun bt (CbvNative where) c
+ eval_fun (CbvNative where) c
let on_destruction_arg tac ev arg =
Proofview.Goal.enter begin fun gl ->
diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli
index 841e8fe762..f6825d84aa 100644
--- a/src/tac2tactics.mli
+++ b/src/tac2tactics.mli
@@ -56,28 +56,28 @@ val vm : (Pattern.constr_pattern * occurrences_expr) option -> clause -> unit ta
val native : (Pattern.constr_pattern * occurrences_expr) option -> clause -> unit tactic
-val eval_red : backtrace -> constr -> constr tactic
+val eval_red : constr -> constr tactic
-val eval_hnf : backtrace -> constr -> constr tactic
+val eval_hnf : constr -> constr tactic
-val eval_simpl : backtrace -> global_reference glob_red_flag ->
+val eval_simpl : global_reference glob_red_flag ->
(Pattern.constr_pattern * occurrences_expr) option -> constr -> constr tactic
-val eval_cbv : backtrace -> global_reference glob_red_flag -> constr -> constr tactic
+val eval_cbv : global_reference glob_red_flag -> constr -> constr tactic
-val eval_cbn : backtrace -> global_reference glob_red_flag -> constr -> constr tactic
+val eval_cbn : global_reference glob_red_flag -> constr -> constr tactic
-val eval_lazy : backtrace -> global_reference glob_red_flag -> constr -> constr tactic
+val eval_lazy : global_reference glob_red_flag -> constr -> constr tactic
-val eval_unfold : backtrace -> (global_reference * occurrences_expr) list -> constr -> constr tactic
+val eval_unfold : (global_reference * occurrences_expr) list -> constr -> constr tactic
-val eval_fold : backtrace -> constr list -> constr -> constr tactic
+val eval_fold : constr list -> constr -> constr tactic
-val eval_pattern : backtrace -> (EConstr.t * occurrences_expr) list -> constr -> constr tactic
+val eval_pattern : (EConstr.t * occurrences_expr) list -> constr -> constr tactic
-val eval_vm : backtrace -> (Pattern.constr_pattern * occurrences_expr) option -> constr -> constr tactic
+val eval_vm : (Pattern.constr_pattern * occurrences_expr) option -> constr -> constr tactic
-val eval_native : backtrace -> (Pattern.constr_pattern * occurrences_expr) option -> constr -> constr tactic
+val eval_native : (Pattern.constr_pattern * occurrences_expr) option -> constr -> constr tactic
val discriminate : evars_flag -> destruction_arg option -> unit tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 00:43:23 +0000