diff --git a/src/transform/apply.ml b/src/transform/apply.ml
index ebab341784c914da3ac43375513ab70a6828b826..9b8ef0086c380934913e1f892b6237b4eb1e9210 100644
--- a/src/transform/apply.ml
+++ b/src/transform/apply.ml
@@ -25,6 +25,19 @@ open Generic_arg_trans_utils
let debug_matching = Debug.register_info_flag "print_match"
~desc:"Print@ terms@ that@ were@ not@ successfully@ matched@ by@ ITP@ tactic@ apply."
+(* One only need to change the following parameter values to change the
+ explanation given to *new* goals introduced by transformation of this file.
+*)
+
+(* Subgoals generated by using [apply] *)
+let apply_subgoals = "apply premises"
+
+(* Subgoals generated by using [rewrite] *)
+let rewrite_subgoals = "rewrite premises"
+
+(* Equality hypothesis generated by using [replace] *)
+let replace_hypothesis = "equality hypothesis"
+
(* Do as intros: introduce all premises of hypothesis pr and return a triple
(goal, list_premises, binded variables) *)
let intros f =
@@ -162,8 +175,10 @@ let apply pr withed_terms : Task.task Trans.tlist = Trans.store (fun task ->
let inst_nt = t_ty_subst subst_ty subst nt in
if (Term.t_equal_nt_na inst_nt g) then
let nlp = List.map (t_ty_subst subst_ty subst) lp in
- List.map (fun ng -> Task.add_decl task
- (create_prop_decl Pgoal (create_prsymbol (gen_ident "G")) ng)) nlp
+ List.map (fun ng ->
+ let pr = create_prsymbol (gen_ident "G") in
+ Task.add_decl task
+ (create_goal ~expl:apply_subgoals pr ng)) nlp
else
raise (Arg_trans_term2 ("apply", inst_nt, g)))
@@ -268,7 +283,7 @@ let rewrite_in rev with_terms h h1 =
p = Paxiom) ->
[d]
| Dprop (Pgoal, _, _) ->
- [create_prop_decl Pgoal (Decl.create_prsymbol (gen_ident "G")) e]
+ [create_goal ~expl:rewrite_subgoals (Decl.create_prsymbol (gen_ident "G")) e]
| _ -> [d] )
None) lp in
Trans.par (trans_rewriting :: list_par) in
@@ -335,7 +350,7 @@ let rewrite_list opt rev with_terms hl h1 =
p = Paxiom) ->
[d]
| Dprop (Pgoal, _, _) ->
- [create_prop_decl Pgoal (Decl.create_prsymbol (gen_ident "G")) e]
+ [create_goal ~expl:rewrite_subgoals (Decl.create_prsymbol (gen_ident "G")) e]
| _ -> [d] )
None) lp in
Trans.par (trans_rewriting :: list_par) in
@@ -387,8 +402,10 @@ let replace t1 t2 hl =
raise (Arg_trans_term2 ("replace", t1, t2))
else
(* Create a new goal for equality of the two terms *)
- let g = Decl.create_prop_decl Decl.Pgoal (create_prsymbol (gen_ident "G")) (t_app_infer ps_equ [t1; t2]) in
- let ng = Trans.goal (fun _ _ -> [g]) in
+ let pr_goal = create_prsymbol (gen_ident "G") in
+ let eq_goal_term = t_app_infer ps_equ [t1; t2] in
+ let ng = create_goal ~expl:replace_hypothesis pr_goal eq_goal_term in
+ let ng = Trans.goal (fun _ _ -> [ng]) in
let g = Trans.decl (fun d ->
match d.d_node with
| Dprop (p, pr, t) when detect_prop_list pr p hl ->
diff --git a/src/transform/case.ml b/src/transform/case.ml
index 0025d2494e2659ab3371f91f6bad7f8ac227a874..af5c3cbcfb7c6bf9e115371905ad72daddb759e2 100644
--- a/src/transform/case.ml
+++ b/src/transform/case.ml
@@ -19,6 +19,20 @@ open Generic_arg_trans_utils
(** This file contains transformation with arguments that acts directly on a
logic connector for intro (case, or_intro, intros, exists) *)
+(** Explanations *)
+
+(* Explanation for [left]/[right] *)
+let left_case_expl = "left case"
+let right_case_expl = "right case"
+
+(* Explanation for [case] *)
+let true_case_expl = "true case"
+let false_case_expl = "false case"
+
+(* Add an explanation attribute to a goal *)
+let create_goal_trans ~expl =
+ Trans.goal (fun pr g -> [create_goal ~expl pr g])
+
(* From task [delta |- G] and term t, build the tasks:
[delta, t] |- G] and [delta, not t | - G] *)
let case t name =
@@ -29,13 +43,11 @@ let case t name =
in
let h = Decl.create_prsymbol (gen_ident name) in
let hnot = Decl.create_prsymbol (gen_ident name) in
- let attr_true = create_attribute "expl:true case" in
- let attr_false = create_attribute "expl:false case" in
let t_not_decl = Decl.create_prop_decl Decl.Paxiom hnot (Term.t_not t) in
let t_decl = Decl.create_prop_decl Decl.Paxiom h t in
- let left_trans = Trans.compose (add_goal_attr_trans attr_true)
+ let left_trans = Trans.compose (create_goal_trans ~expl:true_case_expl)
(Trans.add_decls [t_decl]) in
- let right_trans = Trans.compose (add_goal_attr_trans attr_false)
+ let right_trans = Trans.compose (create_goal_trans ~expl:false_case_expl)
(Trans.add_decls [t_not_decl]) in
Trans.par [left_trans; right_trans]
@@ -47,9 +59,9 @@ let or_intro (left: bool) : Task.task Trans.trans =
match t.t_node with
| Tbinop (Tor, t1, t2) ->
if left then
- [create_prop_decl Pgoal pr t1]
+ [create_goal ~expl:left_case_expl pr t1]
else
- [create_prop_decl Pgoal pr t2]
+ [create_goal ~expl:right_case_expl pr t2]
| _ -> [d]
end
| _ -> [d]) None
@@ -58,7 +70,7 @@ let exists_aux g x =
let t = subst_exist g x in
let pr_goal = create_prsymbol (gen_ident "G") in
let new_goal = Decl.create_prop_decl Decl.Pgoal pr_goal t in
- [new_goal]
+ [new_goal]
(* From task [delta |- exists x. G] and term t, build
the task [delta |- G[x -> t]].
diff --git a/src/transform/cut.ml b/src/transform/cut.ml
index 86070dd8225123d8cf96f648a9f9c864022989fd..349b975f70309c0185d67b69c094875d1a58ca4a 100644
--- a/src/transform/cut.ml
+++ b/src/transform/cut.ml
@@ -18,6 +18,9 @@ open Args_wrapper
(** This file contains transformations with arguments that adds/removes
declarations from the context *)
+(* Explanation for assert and cut *)
+let assert_expl = "asserted formula"
+
(* From task [delta |- G] , build the tasks [delta, t | - G] and [delta] |- t] *)
let cut t name =
let name =
@@ -26,7 +29,7 @@ let cut t name =
| None -> "h"
in
let h = Decl.create_prsymbol (gen_ident name) in
- let g_t = Decl.create_prop_decl Decl.Pgoal h t in
+ let g_t = create_goal ~expl:assert_expl h t in
let h_t = Decl.create_prop_decl Decl.Paxiom h t in
let goal_cut = Trans.goal (fun _ _ -> [g_t]) in
let goal = Trans.add_decls [h_t] in
@@ -41,7 +44,7 @@ let assert_tac t name =
| None -> "h"
in
let h = Decl.create_prsymbol (gen_ident name) in
- let g_t = Decl.create_prop_decl Decl.Pgoal h t in
+ let g_t = create_goal ~expl:assert_expl h t in
let h_t = Decl.create_prop_decl Decl.Paxiom h t in
let goal_cut = Trans.goal (fun _ _ -> [g_t]) in
let goal = Trans.add_decls [h_t] in
diff --git a/src/transform/destruct.ml b/src/transform/destruct.ml
index 104be778fadc7b110f287e13634920958d2aa652..e807559b1a71ea64b1d45dc100c63203d035968a 100644
--- a/src/transform/destruct.ml
+++ b/src/transform/destruct.ml
@@ -17,6 +17,11 @@ open Generic_arg_trans_utils
(** This file contains transformations with arguments that eliminates logic
connectors (instantiate, destruct, destruct_alg). *)
+(** Explanation *)
+
+(* Explanation for destruct premises *)
+let destruct_expl = "destruct premise"
+
let is_lsymbol t =
match t.t_node with
| Tapp (_, []) -> true
@@ -192,11 +197,11 @@ let destruct pr : Task.task Trans.tlist =
(* Destruct case for an implication. The first goal should be new_decl,
the second one is unchanged. *)
| first_task :: second_task :: [] ->
- let new_goal =
- create_prop_decl Pgoal (create_prsymbol (gen_ident "G")) new_decl in
- let first_goal = Task.add_decl first_task new_goal in
- let second_goal = Task.add_tdecl second_task goal in
- first_goal :: second_goal :: []
+ let pr = create_prsymbol (gen_ident "G") in
+ let new_goal = create_goal ~expl:destruct_expl pr new_decl in
+ let first_goal = Task.add_decl first_task new_goal in
+ let second_goal = Task.add_tdecl second_task goal in
+ first_goal :: second_goal :: []
| _ -> assert false)
(* from task [delta, name:forall x.A |- G,
diff --git a/src/transform/generic_arg_trans_utils.ml b/src/transform/generic_arg_trans_utils.ml
index 3ca998e79f56f6bb2d1741c6747d766a9a7f6123..62e22c39de76ad7a8901e9b0a9e1e739050fc5bb 100644
--- a/src/transform/generic_arg_trans_utils.ml
+++ b/src/transform/generic_arg_trans_utils.ml
@@ -155,11 +155,6 @@ let sort =
Trans.bind get_local sort
-(* Add an attribute to a goal (useful to add an expl for example) *)
-let add_goal_attr_trans attr =
- Trans.goal (fun pr g -> [create_prop_decl Pgoal pr (t_attr_add attr g)])
-
-
(****************************)
(* Substitution of terms *)
(****************************)
@@ -183,3 +178,13 @@ let replace_tdecl (subst: term_subst) (td: tdecl) =
| Decl d ->
create_decl (replace_decl subst d)
| _ -> td
+
+
+(************************)
+(* Explanation handling *)
+(************************)
+
+let create_goal ~expl pr t =
+ let expl = Ident.create_attribute ("expl:" ^ expl) in
+ let t = Term.t_attr_add expl t in
+ create_prop_decl Pgoal pr t
diff --git a/src/transform/generic_arg_trans_utils.mli b/src/transform/generic_arg_trans_utils.mli
index 98a6de28683066c2483312c83abfb388f817a2fa..377d17f6bc90cf48ee531eed2605d3ff1bc94e21 100644
--- a/src/transform/generic_arg_trans_utils.mli
+++ b/src/transform/generic_arg_trans_utils.mli
@@ -47,13 +47,9 @@ val get_local_task: Task.task -> Decl.decl list
definitions defined before axioms *)
val sort: Task.task Trans.trans
-(* Add an attribute to a goal (useful to add an expl for example) *)
-val add_goal_attr_trans: Ident.attribute -> Task.task Trans.trans
-
-
-(****************************)
-(* Substitution of terms *)
-(****************************)
+(*************************)
+(* Substitution of terms *)
+(*************************)
type term_subst = term Mterm.t
@@ -62,3 +58,13 @@ val replace_subst: term_subst -> Term.term -> Term.term
val replace_decl: term_subst -> Decl.decl -> Decl.decl
val replace_tdecl: term_subst -> Theory.tdecl -> Theory.tdecl
+
+(************************)
+(* Explanation handling *)
+(************************)
+
+(* This function creates a goal with an explanation. The term on which this is
+ applied should not contain any explanation itself (otherwise both would
+ appear in the ide).
+*)
+val create_goal: expl:string -> Decl.prsymbol -> Term.term -> Decl.decl
diff --git a/src/transform/ind_itp.ml b/src/transform/ind_itp.ml
index b5bdba14a3e69d84051ebfaa018f36aa11b5e00b..9357f9aff7b089ee2eb6d2c1d6a9650434992617 100644
--- a/src/transform/ind_itp.ml
+++ b/src/transform/ind_itp.ml
@@ -16,6 +16,14 @@ open Args_wrapper
(** This file contains the transformation with arguments 'induction on integer' *)
+(** Explanation *)
+
+(* Explanation for induction base goal of induction tactic *)
+let base_case_expl = "base case"
+
+(* Explanation for recursive case *)
+let rec_case_expl = "recursive case"
+
(* Documentation of induction:
@@ -228,8 +236,7 @@ let induction x bound env =
let init_trans = Trans.decl (fun d -> match d.d_node with
| Dprop (Pgoal, pr, t) ->
let nt = Term.t_app_infer le_int [x; bound] in
- let attr_base = Ident.create_attribute "expl:base case" in
- let d = create_prop_decl Pgoal pr (t_attr_add attr_base t) in
+ let d = create_goal ~expl:base_case_expl pr t in
let pr_init =
create_prop_decl Paxiom (Decl.create_prsymbol (gen_ident "Init")) nt in
[pr_init; d]
@@ -261,8 +268,7 @@ let induction x bound env =
create_prop_decl Paxiom (Decl.create_prsymbol (gen_ident "Init")) x_gt_bound_t in
let rec_pr = create_prsymbol (gen_ident "Hrec") in
let hrec = create_prop_decl Paxiom rec_pr t_delta' in
- let attr_rec = Ident.create_attribute "expl:recursive case" in
- let d = create_prop_decl Pgoal pr (t_attr_add attr_rec t) in
+ let d = create_goal ~expl:rec_case_expl pr t in
[x_gt_bound; hrec; d]
| Dprop (_p, _pr, _t) ->
if !x_is_passed then
diff --git a/src/transform/subst.ml b/src/transform/subst.ml
index 90e78c98eeaaa0003aae164779b9769a63a1d8a8..c294864a3ff534e916a6cc94aa2437ca65f94b3b 100644
--- a/src/transform/subst.ml
+++ b/src/transform/subst.ml
@@ -93,7 +93,7 @@ let apply_subst ((prs,sigma) : (Spr.t * term Mls.t)) (tdl:Theory.tdecl list) : T
| [] ->
let d = create_prop_decl Pgoal pr (subst_in_term sigma t) in
let td = Theory.create_decl d in
-Task.add_tdecl tuc td
+ Task.add_tdecl tuc td
| _ -> raise (Arg_trans "apply_subst failed")
end
| Dprop(_k,pr,_t) when Spr.mem pr prs ->