Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit d5a8547d authored by Sylvain Dailler's avatar Sylvain Dailler

subst x can be used when x appears alone in 2 equalities.

destruct_alg_subst x also substitute x when x is an lsymbol
parent 43211b86
......@@ -303,32 +303,37 @@ let unfold unf hl =
This function returns None if not found, Some (None, t1, t2) with t1 being
to_subst and t2 being term to substitute to if the equality found it a symbol
definition. If equality found is a a decl then it is returned:
Some (Some pr, t1, t2) *)
Some (Some pr, t1, t2).
If the lsymbol to substitute appear in 2 equalities, only the first one is
used. *)
let find_eq (to_subst: Term.lsymbol list) =
fold (fun d acc ->
fold (fun d (acc, used) ->
match d.d_node with
| Dprop (k, pr, t) when k != Pgoal ->
let acc = (match t.t_node with
let acc, used = (match t.t_node with
| Tapp (ls, [t1; t2]) when ls_equal ls ps_equ ->
(* Allow to rewrite from the right *)
begin
match t1.t_node, t2.t_node with
| Tapp (ls, []), _ when List.exists (ls_equal ls) to_subst ->
Some (Some pr, t1, t2) :: acc
| _, Tapp (ls, []) when List.exists (ls_equal ls) to_subst ->
Some (Some pr, t2, t1) :: acc
| _ -> acc
| Tapp (ls, []), _ when List.exists (ls_equal ls) to_subst &&
not (List.exists (ls_equal ls) used) ->
Some (Some pr, t1, t2) :: acc, ls :: used
| _, Tapp (ls, []) when List.exists (ls_equal ls) to_subst &&
not (List.exists (ls_equal ls) used) ->
Some (Some pr, t2, t1) :: acc, ls :: used
| _ -> acc, used
end
| _ -> acc) in
acc
| Dlogic [(ls, ld)] when List.exists (ls_equal ls) to_subst ->
| _ -> acc, used) in
acc, used
| Dlogic [(ls, ld)] when List.exists (ls_equal ls) to_subst &&
not (List.exists (ls_equal ls) used) ->
(* Function without arguments *)
let vl, e = open_ls_defn ld in
if vl = [] then
Some (None, t_app_infer ls [], e) :: acc
Some (None, t_app_infer ls [], e) :: acc, ls :: used
else
acc
| _ -> acc) []
acc, used
| _ -> acc, used) ([],[])
(* This found any equality which at one side contains a single lsymbol and is
local. It gives same output as found_eq. *)
......@@ -419,7 +424,7 @@ let subst_eq found_eq =
| Dtype _ | Ddata _ | Dparam _ -> [d]) None
end
let subst_eq_list found_eq_list =
let subst_eq_list (found_eq_list, _) =
List.fold_left (fun acc_tr found_eq ->
Trans.compose (subst_eq found_eq) acc_tr) Trans.identity found_eq_list
......
......@@ -17,6 +17,11 @@ open Generic_arg_trans_utils
(** This file contains transformations with arguments that eliminates logic
connectors (instantiate, destruct, destruct_alg). *)
let is_lsymbol t =
match t.t_node with
| Tapp (_, []) -> true
| _ -> false
let create_constant ty =
let fresh_name = Ident.id_fresh "x" in
let ls = create_lsymbol fresh_name [] (Some ty) in
......@@ -58,11 +63,12 @@ let rec compounds_of acc (t: term) =
new goal per constructor of the type and introduce corresponding
variables. It also introduce the equality between the term and
its destruction in the context.
When replace is set to true, a susbtitution is done when x is an lsymbol.
*)
let destruct_alg (x: term) : Task.task Trans.tlist =
let destruct_alg replace (x: term) : Task.task Trans.tlist =
let ty = x.t_ty in
(* We list all the constants used in x so that we know the first place in the
task where we can introduce hypothesis about the destruction of x. *)
task where we can introduce hypothesis about the destruction of x. *)
let ls_of_x = ref (compounds_of Term.Sls.empty x) in
let defined = ref false in
let r = ref [] in
......@@ -73,7 +79,7 @@ task where we can introduce hypothesis about the destruction of x. *)
match ty.Ty.ty_node with
| Ty.Tyvar _ -> raise (Cannot_infer_type "destruct")
| Ty.Tyapp (ts, _) ->
Trans.decl_l (fun d ->
let trans = Trans.decl_l (fun d ->
match d.d_node with
(* TODO not necessary to check this first: this can be optimized *)
| _ when (not !defined) && Term.Sls.is_empty !ls_of_x ->
......@@ -109,6 +115,11 @@ task where we can introduce hypothesis about the destruction of x. *)
| Dprop (Pgoal, _, _) ->
[[d]]
| _ -> [[d]]) None
in
if replace && is_lsymbol x then
Trans.compose_l trans (Trans.singleton (Apply.subst [x]))
else
trans
end
(* Destruct the head term of an hypothesis if it is either
......@@ -213,4 +224,7 @@ let () = wrap_and_register ~desc:"destruct <name> destructs the head constructor
"destruct" (Tprsymbol Ttrans_l) destruct
let () = wrap_and_register ~desc:"destruct <name> destructs as an algebraic type"
"destruct_alg" (Tterm Ttrans_l) destruct_alg
"destruct_alg" (Tterm Ttrans_l) (destruct_alg false)
let () = wrap_and_register ~desc:"destruct <name> destructs as an algebraic type and substitute the definition if an lsymbol was provided"
"destruct_alg_subst" (Tterm Ttrans_l) (destruct_alg true)
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