Commit 0ac9d709 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Nwe versions of transformations subst and subst_all

parent beebe3f0
......@@ -9,22 +9,34 @@ goal g2: forall x. p x -> forall _y:int. x = 42 -> q x
goal g1: forall x. p x -> forall y. x = f y -> q x
end
constant x : int
module More
axiom h1 : p x
use import int.Int
function f int : int
constant y:int
goal g3: forall x:int.
forall z. z = x+1 ->
forall y. y = z ->
x = f y -> y = f y + 1
axiom h2: x = f y
end
goal g: q x
module Other
use import int.Int
goal g3: forall x:int.
forall z. z = x+1 ->
forall y. y = z ->
x = f y -> y = f y + 1
predicate p int
constant x : int
axiom H1 : p x
constant y : int = 3
axiom H2 : x = y+1
goal g : x*y = 0
end
\ No newline at end of file
......@@ -34,17 +34,17 @@
<transf name="remove" arg1="h1,h2">
<goal name="g3.0">
<transf name="case" arg1="x=0">
<goal name="g3.0.0" expl="true case">
<goal name="g3.0.0">
</goal>
<goal name="g3.0.1" expl="false case">
<goal name="g3.0.1">
</goal>
</transf>
<transf name="introduce_premises" >
<goal name="g3.0.0">
<transf name="induction" arg1="x" arg2="from" arg3="42">
<goal name="g3.0.0.0" expl="base case">
<goal name="g3.0.0.0">
</goal>
<goal name="g3.0.0.1" expl="recursive case">
<goal name="g3.0.0.1">
</goal>
</transf>
</goal>
......@@ -57,5 +57,21 @@
</transf>
</goal>
</theory>
<theory name="More">
<goal name="g3">
</goal>
</theory>
<theory name="Other">
<goal name="g">
<transf name="subst" arg1="x">
<goal name="g.0">
</goal>
</transf>
<transf name="subst_all" >
<goal name="g.0">
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
......@@ -226,7 +226,11 @@ let get_exception_message ses id e =
Pp.sprintf "Error in transformation %s during inclusion of following declarations:\n%a" s
(Pp.print_list (fun fmt () -> Format.fprintf fmt "\n") (print_tdecl ses id)) ld,
Loc.dummy_position, ""
| Generic_arg_trans_utils.Arg_trans_term (s, t1, t2) ->
| Generic_arg_trans_utils.Arg_trans_term (s, t) ->
Pp.sprintf "Error in transformation %s during with term:\n %a : %a " s
(print_term ses id) t (print_opt_type ses id) t.Term.t_ty,
Loc.dummy_position, ""
| Generic_arg_trans_utils.Arg_trans_term2 (s, t1, t2) ->
Pp.sprintf "Error in transformation %s during unification of following two terms:\n %a : %a \n %a : %a" s
(print_term ses id) t1 (print_opt_type ses id) t1.Term.t_ty
(print_term ses id) t2 (print_opt_type ses id) t2.Term.t_ty,
......
......@@ -90,7 +90,7 @@ let with_terms ~trans_name subst_ty subst lv withed_terms =
| Reduction_engine.NoMatch (Some (t1, t2)) ->
Debug.dprintf debug_matching "Term %a and %a can not be matched. Failure in matching@."
Pretty.print_term t1 Pretty.print_term t2;
raise (Arg_trans_term (trans_name, t1, t2))
raise (Arg_trans_term2 (trans_name, t1, t2))
| Reduction_engine.NoMatchpat (Some (p1, p2)) ->
Debug.dprintf debug_matching "Term %a and %a can not be matched. Failure in matching@."
Pretty.print_pat p1 Pretty.print_pat p2;
......@@ -112,7 +112,7 @@ let with_terms ~trans_name subst_ty subst lv withed_terms =
if Term.t_equal_nt_nl y z then
Some y
else
raise (Arg_trans_term (trans_name ^ ": ", y, z)))
raise (Arg_trans_term2 (trans_name ^ ": ", y, z)))
subst new_subst
in
subst_ty, subst
......@@ -132,7 +132,7 @@ let matching_with_terms ~trans_name slv lv left_term right_term withed_terms =
Debug.dprintf debug_matching
"Term %a and %a can not be matched. Failure in matching@."
Pretty.print_term t1 Pretty.print_term t2;
raise (Arg_trans_term (trans_name, t1, t2))
raise (Arg_trans_term2 (trans_name, t1, t2))
| Reduction_engine.NoMatchpat (Some (p1, p2)) ->
Debug.dprintf debug_matching
"Term %a and %a can not be matched. Failure in matching@."
......@@ -174,7 +174,7 @@ let apply pr withed_terms : Task.task Trans.tlist = Trans.store (fun task ->
List.map (fun ng -> Task.add_decl task
(create_prop_decl Pgoal (create_prsymbol (gen_ident "G")) ng)) nlp
else
raise (Arg_trans_term ("apply", inst_nt, g)))
raise (Arg_trans_term2 ("apply", inst_nt, g)))
let replace rev f1 f2 t =
match rev with
......@@ -320,7 +320,7 @@ let detect_prop_list pr k hl =
*)
let replace t1 t2 hl =
if not (Ty.ty_equal (t_type t1) (t_type t2)) then
raise (Arg_trans_term ("replace", t1, t2))
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
......
......@@ -15,7 +15,8 @@ open Theory
exception Arg_trans of string
exception Arg_trans_decl of (string * tdecl list)
exception Arg_trans_term of (string * term * term)
exception Arg_trans_term of (string * term)
exception Arg_trans_term2 of (string * term * term)
exception Arg_trans_pattern of (string * pattern * pattern)
exception Arg_trans_type of (string * Ty.ty * Ty.ty)
exception Arg_bad_hypothesis of (string * term)
......
......@@ -13,7 +13,8 @@ open Term
exception Arg_trans of string
exception Arg_trans_decl of (string * Theory.tdecl list)
exception Arg_trans_term of (string * term * term)
exception Arg_trans_term of (string * term)
exception Arg_trans_term2 of (string * term * term)
exception Arg_trans_pattern of (string * pattern * pattern)
exception Arg_trans_type of (string * Ty.ty * Ty.ty)
exception Arg_bad_hypothesis of (string * term)
......
......@@ -11,12 +11,169 @@
open Term
open Decl
open Theory
open Generic_arg_trans_utils
open Args_wrapper
(* transformations "subst" and "subst_all" *)
let debug_subst = Debug.register_flag "subst" ~desc:"debug transformations subst and subst_all"
let rec subst_in_term sigma t =
match t.t_node with
| Tapp(ls,[]) ->
begin
try Mls.find ls sigma
with Not_found -> t
end
| _ -> t_map (subst_in_term sigma) t
let subst_in_def sigma ls (d:ls_defn) =
let (vl,t) = open_ls_defn d in
make_ls_defn ls vl (subst_in_term sigma t)
(* [apply_subst prs sigma] is a transformation that operates on each decls.
for each decl:
- if d is a prop whose prsymbol belongs to prs, then it is removed
- if d is a declaration of a constant symbol in the domain of sigma
then it is removed
- otherwise d is rewritten using the substitution sigma
in [sigma], the right hand sides must not contain any symbols
appearing in the left-hand-side
*)
let apply_subst ((prs,sigma) : (Spr.t * term Mls.t)) : Task.task Trans.trans =
Trans.decl
(fun d ->
match d.d_node with
| Dprop(_k,pr,_t) when Spr.mem pr prs -> []
| Dprop(k,pr,t) -> [create_prop_decl k pr (subst_in_term sigma t)]
| Dparam ls -> if Mls.mem ls sigma then [] else [d]
| Dlogic ld ->
let ld' =
List.fold_right
(fun (ls,ld) acc ->
if Mls.mem ls sigma then acc
else (subst_in_def sigma ls ld)::acc)
ld
[]
in
begin
match ld' with
| [] -> []
| _ -> [create_logic_decl ld']
end
| Dind ((is: ind_sign), (ind_list: ind_decl list)) ->
let ind_list =
List.map (fun ((ls: lsymbol), (idl: (prsymbol * term) list)) ->
let idl = List.map (fun (pr, t) -> (pr, subst_in_term sigma t)) idl in
(ls, idl)) ind_list
in
[create_ind_decl is ind_list]
| Dtype _ | Ddata _ -> [d])
None
let rec occurs_in_term ls t =
match t.t_node with
| Tapp(ls',[]) when ls_equal ls' ls -> true
| _ -> t_any (occurs_in_term ls) t
(* [find_equalities filter t] searches in task [t] for equalities of
the form constant = term or term = constant, where constant does
not occur in the term. That function returns first the set of
prsymbols for the equalities found, and second a map from the
lsymbols of the constant to the associated term. That map is
normalized in the sense that the terms on the right are fully
substituted, for example if the equalities "x=t" and "y=x+u" are
found, then the map contains "x -> t" and "y ->t+u". The [filter]
function applys a generic filter to the constants that can be taken
into consideration. if several equalities occur for the same
constant, the first one is considered.
*)
let find_equalities filter =
Trans.fold_decl
(fun d ((prs,sigma) as acc) ->
match d.d_node with
| Dprop (Pgoal, _, _) -> acc
| Dprop (_, pr, t) ->
begin
match t.t_node with
| Tapp (ls, [t1; t2]) when ls_equal ls ps_equ ->
begin
try match t1.t_node with
| Tapp (ls, []) when
filter ls &&
not (Mls.mem ls sigma) ->
let t2' = subst_in_term sigma t2 in
if occurs_in_term ls t2' then raise Exit
else
let () = Debug.dprintf debug_subst "selected: %a -> %a@."
Pretty.print_ls ls Pretty.print_term t2' in
(Spr.add pr prs, Mls.add ls t2' sigma)
| _ -> raise Exit
with Exit ->
match t2.t_node with
| Tapp (ls, []) when
filter ls &&
not (Mls.mem ls sigma) ->
let t1' = subst_in_term sigma t1 in
if occurs_in_term ls t1' then acc
else
let () = Debug.dprintf debug_subst "selected: %a -> %a@."
Pretty.print_ls ls Pretty.print_term t1' in
(Spr.add pr prs, Mls.add ls t1' sigma)
| _ -> acc
end
| _ -> acc
end
| Dlogic ld ->
List.fold_left
(fun ((prs,sigma) as acc) (ls,ld) ->
if filter ls then
let vl, t = open_ls_defn ld in
if vl = [] && not (occurs_in_term ls t) then
let t = subst_in_term sigma t in
(prs, Mls.add ls t sigma)
else acc
else acc)
acc
ld
| Ddata _ | Dtype _ | Dparam _ | Dind _ -> acc)
(Spr.empty, Mls.empty)
let subst_all =
Trans.bind (find_equalities (fun _ -> true)) apply_subst
let () =
wrap_and_register ~desc:"substitutes with all equalities between a constant and a term"
"subst_all"
(Ttrans) subst_all
let subst tl =
let to_subst =
List.fold_left
(fun acc t ->
match t.t_node with
| Tapp (ls, []) -> Sls.add ls acc
| _ -> raise (Arg_trans "subst: %a is not a constant")) Sls.empty tl
in
Trans.bind (find_equalities (fun ls -> Sls.mem ls to_subst)) apply_subst
let () =
wrap_and_register ~desc:"substitutes with all equalities involving one of the given constants"
"subst"
(Ttermlist Ttrans) subst
(*
(* This found any equality which at one side contains a single lsymbol and is
local. It gives same output as found_eq. *)
let find_eq2 is_local_decl =
......@@ -144,12 +301,14 @@ let () =
"subst_all"
(Ttrans) subst_all
*)
(*********)
(* Subst *)
(*********)
(*
(* Creation of as structure that associates the replacement of terms as a
function of the
*)
......@@ -305,3 +464,4 @@ let subst args = Trans.bind (find args) readd_decls
let () = wrap_and_register ~desc:"remove a literal using an equality on it"
"subst"
(Ttermlist Ttrans) subst
*)
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