Commit 10306ad1 authored by Sylvain Dailler's avatar Sylvain Dailler

Fix induction_arg_ty_lex by adding attribute induction on variable

parent 0dd92f60
......@@ -24,6 +24,7 @@ Transformations
(previously ignored):x:
* Fix crash of eliminate_unknown_types
* Giving too many arguments to a transformation do not display a popup anymore
* Fix behavior of induction_arg_ty_lex (now equivalent to induction_ty_lex)
Counterexamples
* Improved display of counterexamples in Task view
......
......@@ -70,13 +70,14 @@ let is_good_type t ty =
| _ -> false
(* Reverts a declaration d to a goal g *)
let revert g d : Term.term =
let revert ?tr g d : Term.term =
match d.d_node with
| Dtype _ -> raise (Arg_trans "revert: cannot revert type")
| Ddata _ -> raise (Arg_trans "revert: cannot revert type")
| Dparam ls ->
(try
let new_ident = Ident.id_fresh ls.ls_name.Ident.id_string in
let attrs = Opt.map2 (fun tr ls -> tr ls) tr (Some ls) in
let new_ident = Ident.id_fresh ?attrs ls.ls_name.Ident.id_string in
let new_var = Term.create_vsymbol new_ident (Opt.get ls.Term.ls_value) in
let g = t_replace (t_app_infer ls []) (t_var new_var) g in
t_forall_close [new_var] [] g
......@@ -103,8 +104,8 @@ let fold_map f init =
(* Takes a list of prop l and a goal g and reverts the list
of prop to the goal g *)
let revert_list (l: decl list) g =
List.fold_left revert g l
let revert_list ?tr (l: decl list) g =
List.fold_left (revert ?tr) g l
(* Go through a term and collect constants *)
let add_ls_term s t =
......@@ -150,30 +151,30 @@ let depends dep d =
(* TODO Do a transformation as a fold that reverts automatically dependencies
but that could be used elsewhere instead of all those adhoc functions. *)
let revert_tr prlist lslist =
let revert_tr ?tr prlist lslist =
fold_map (fun d ((acc, dep), task) ->
match d.d_node with
| Dparam ls when (depends dep d ||
List.exists (fun ls1 -> ls_equal ls ls1) lslist) ->
| Dparam ls when
depends dep d || List.exists (fun ls1 -> ls_equal ls ls1) lslist ->
((d :: acc, Sls.add ls dep), task)
| Dprop (k, pr1, _) when k != Pgoal
| Dprop (k, pr1, _) when
k != Pgoal
&& (depends dep d || List.exists (fun pr -> pr_equal pr pr1) prlist)
->
((d :: acc, dep), task)
| Dprop (k, pr1, g) when k = Pgoal ->
begin
match acc with
begin match acc with
| [] ->
raise (Arg_trans "prsymbol not found")
| drevlist ->
let new_goal = Decl.create_prop_decl k pr1 (revert_list drevlist g) in
(([], Sls.empty), Task.add_decl task new_goal)
end
let new_goal = Decl.create_prop_decl k pr1 (revert_list ?tr drevlist g) in
(([], Sls.empty), Task.add_decl task new_goal)
end
| _ -> ((acc, dep), Task.add_decl task d)
)
([], Sls.empty)
let revert_tr_symbol symbol_list =
let revert_tr_symbol ?tr symbol_list =
(* Order does not matter *)
let rec convert_list pr_acc ls_acc symbollist =
......@@ -185,7 +186,7 @@ let revert_tr_symbol symbol_list =
raise (Arg_trans "Tysymbol should not appear here. Please report")
in
let (prlist, lslist) = convert_list [] [] symbol_list in
revert_tr prlist lslist
revert_tr ?tr prlist lslist
(* s is a set of variables, g is a term. If d contains one of the elements of s
then all variables of d are added to s and the declaration is prepended to g.
......@@ -308,4 +309,4 @@ let () = wrap_and_register
let () = wrap_and_register
~desc:"revert <list> puts list back in the goal."
"revert"
(Tlist Ttrans) revert_tr_symbol
(Tlist Ttrans) (revert_tr_symbol ?tr:None)
......@@ -9,4 +9,10 @@
(* *)
(********************************************************************)
val revert_tr_symbol: Args_wrapper.symbol list -> Task.task Trans.trans
(* [tr] gives a function that gives a set of attributes to the fresh elements
generated during the revert. It allows in particular to add [@induction] for
induction_ty_lex.
*)
val revert_tr_symbol:
?tr:(Term.lsymbol -> Ident.Sattr.t) ->
Args_wrapper.symbol list -> Task.task Trans.trans
......@@ -348,7 +348,14 @@ let () =
~desc:"Generate@ induction@ hypotheses@ for@ goals@ over@ algebraic@ types."
let induction_on_hyp ls =
Trans.compose (Ind_itp.revert_tr_symbol [Tslsymbol ls])
(* We add the induction attribute on the reverted symbol *)
let tr = Some
(fun s -> (* Add induction attribute *only* on ls *)
if ls_equal s ls then
Ident.Sattr.singleton (create_attribute "induction")
else Ident.Sattr.empty)
in
Trans.compose (Ind_itp.revert_tr_symbol ?tr [Tslsymbol ls])
(Trans.store induction_ty_lex)
let () = wrap_and_register
......
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