Commit b434a9a8 authored by Sylvain Dailler's avatar Sylvain Dailler

Naming proposition for expl of transformations with arguments #191

This puts explanations on goals generated by some transformations with
arguments. Ideally, no goals should be without explanations.
parent 64b9237d
......@@ -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 ->
......
......@@ -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]].
......
......@@ -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
......
......@@ -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,
......
......@@ -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
......@@ -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
......@@ -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
......
......@@ -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 ->
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment