Commit 0f71f965 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Optional arguments of tactics can be prlist

Optional arguments for induction, unfold and replace.
parent 2ca61f15
......@@ -219,8 +219,26 @@ let find_target_prop h : prsymbol trans =
let rewrite rev h h1 = Trans.bind (find_target_prop h1) (rewrite_in (not rev) h)
(* Replace occurences of t1 with t2 in h *)
let replace t1 t2 h =
(* This function is used to detect when we found the hypothesis/goal we want
to replace/unfold into. *)
let detect_prop pr k h =
match h with
| None -> k = Pgoal
| Some h -> Ident.id_equal pr.pr_name h.pr_name && (k = Paxiom || k = Pgoal)
let detect_prop_list pr k hl =
match hl with
| None -> k = Pgoal
| Some [] -> (* Should not be able to parse the empty list *)
raise (Arg_trans "replace")
| Some hl ->
((List.exists (fun h -> Ident.id_equal pr.pr_name h.pr_name) hl)
&& (k = Paxiom || k = Pgoal))
(* Replace occurences of t1 with t2 in h. When h is None, the default is to
replace in the goal.
*)
let replace t1 t2 hl =
if not (Ty.ty_equal (t_type t1) (t_type t2)) then
raise (Arg_trans_term ("replace", t1, t2))
else
......@@ -229,11 +247,12 @@ let replace t1 t2 h =
let ng = Trans.goal (fun _ _ -> [g]) in
let g = Trans.decl (fun d ->
match d.d_node with
| Dprop (p, pr, t) when (Ident.id_equal pr.pr_name h.pr_name && (p = Paxiom || p = Pgoal)) ->
| Dprop (p, pr, t) when detect_prop_list pr p hl ->
[create_prop_decl p pr (replace true t1 t2 t)]
| _ -> [d]) None in
Trans.par [g; ng]
let t_replace_app unf ls_defn t =
let (vl, tls) = ls_defn in
match t.t_node with
......@@ -247,7 +266,7 @@ let t_replace_app unf ls_defn t =
let rec t_ls_replace ls ls_defn t =
t_replace_app ls ls_defn (t_map (t_ls_replace ls ls_defn) t)
let unfold unf h =
let unfold unf hl =
let r = ref None in
Trans.decl
(fun d ->
......@@ -256,7 +275,7 @@ let unfold unf h =
| Dlogic [(ls, ls_defn)] when ls_equal ls unf ->
r := Some (open_ls_defn ls_defn);
[d]
| Dprop (k, pr, t) when pr_equal h pr ->
| Dprop (k, pr, t) when detect_prop_list pr k hl ->
begin
match !r with
| None -> [d]
......@@ -431,14 +450,14 @@ let () = wrap_and_register ~desc:"sort declarations"
"sort"
(Ttrans) sort
let () = wrap_and_register ~desc:"unfold ls pr: unfold logic symbol ls in hypothesis pr. Experimental." (* TODO *)
let () = wrap_and_register ~desc:"unfold ls [in] pr: unfold logic symbol ls in list of hypothesis pr. The argument in is optional: by default unfold in the goal." (* TODO *)
"unfold"
(Tlsymbol (Tprsymbol Ttrans)) unfold
(Tlsymbol (Topt ("in", Tprlist Ttrans))) unfold
let () = wrap_and_register
~desc:"replace <term1> <term2> <name> replaces occcurences of term1 by term2 in prop name"
~desc:"replace <term1> <term2> [in] <name list> replaces occcurences of term1 by term2 in prop name. If no list is given, replace in the goal."
"replace"
(Tterm (Tterm (Tprsymbol Ttrans_l))) replace
(Tterm (Tterm (Topt ("in", Tprlist Ttrans_l)))) replace
let _ = wrap_and_register
~desc:"rewrite [<-] <name> [in] <name2> rewrites equality defined in name into name2" "rewrite"
......
......@@ -475,6 +475,15 @@ let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.en
| Tstring t' ->
let arg = Some s' in
wrap_to_store t' (f arg) tail env tables task
| Tprlist t' ->
let pr_list = parse_list_qualid s' in
let pr_list =
List.map (fun id ->
try find_pr id tables with
| Not_found -> raise (Arg_qid_not_found id))
pr_list in
let arg = Some pr_list in
wrap_to_store t' (f arg) tail env tables task
| _ -> raise (Arg_expected (string_of_trans_typ t', s'))
end
| Topt (_, t'), _ ->
......
......@@ -59,6 +59,12 @@ let induction x bound env =
let plus_int = Theory.ns_find_ls th.Theory.th_export ["infix +"] in
let one_int =
Term.t_const (Number.ConstInt (Number.int_const_dec "1")) Ty.ty_int in
(* bound is optional and set to 0 if not given *)
let bound =
match bound with
| None -> Term.t_const (Number.ConstInt (Number.int_const_dec "0")) Ty.ty_int
| Some bound -> bound
in
if (not (is_good_type x Ty.ty_int) || not (is_good_type bound Ty.ty_int)) then
raise (Arg_trans "induction")
......@@ -122,6 +128,6 @@ let induction x bound env =
Trans.par [le_bound; ge_bound]
let () = wrap_and_register
~desc:"induction <term1> <term2> performs induction on int term1 from int term2"
~desc:"induction <term1> [from] <term2> performs induction on int term1 from int term2. term2 is optional and default to 0."
"induction"
(Tterm (Tterm Tenvtrans_l)) induction
(Tterm (Topt ("from", Tterm Tenvtrans_l))) induction
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