Commit f91bc030 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Split variable detection out of Tree.reify.

This commit also splits Reify.reify_full into two functions.
parent b65d4c4e
......@@ -82,17 +82,15 @@ Definition eval_goal (g : gol) (x : R) :=
Ltac massage_goal :=
let aux a x t :=
match reify a (@nil R) with
| (?a, @nil R) => change (eval_goal (t a) x)
end in
let a := reify a (@nil R) in
(change (eval_goal (t a) x)) in
match goal with
| |- (Rabs ?x <= ?v)%R => aux v x (Gabsle true)
| |- (?u <= ?x)%R => aux u x (Gge true)
| |- (?x <= ?v)%R => aux v x (Gle true)
| |- (?u <= ?x <= ?v)%R =>
match reify u (@nil R) with
| (?u, @nil R) => aux v x (Glele u)
end
let u := reify u (@nil R) in
aux v x (Glele u)
| |- (?u < ?x)%R => aux u x Ggt
| |- (?x > ?u)%R => aux u x Ggt
| |- (?x < ?v)%R => aux v x Glt
......@@ -103,17 +101,14 @@ Ltac massage_goal :=
Ltac find_hyps_aux x known cont :=
let aux H u t :=
match reify u (@nil R) with
| (?u, @nil R) =>
let k := constr:(cons (t u) known) in
revert H ;
find_hyps_aux x k cont
end in
let u := reify u (@nil R) in
let k := constr:(cons (t u) known) in
revert H ;
find_hyps_aux x k cont in
match goal with
| H : (?u <= x <= ?v)%R |- _ =>
match reify u (@nil R) with
| (?u', @nil R) => aux H v (Hlele u')
end
let u := reify u (@nil R) in
aux H v (Hlele u)
| H : (?u <= x)%R |- _ => aux H u (Hge true)
| H : (x >= ?u)%R |- _ => aux H u (Hge false)
| H : (x <= ?v)%R |- _ => aux H v (Hle true)
......@@ -146,47 +141,39 @@ Ltac find_hyps vars :=
change (eval_hyps k vars g) ;
clear in
find_hyps_aux2 vars cont
end ;
match goal with
| |- eval_hyps ?hyps' _ _ =>
let hyps := fresh "__hyps" in
set (hyps := hyps')
end.
Ltac reify_partial y vars :=
let expr' := reify y vars in
let expr := fresh "__expr" in
set (expr := expr') ;
change y with (eval expr vars) ;
generalize (extract_correct expr vars) ;
let decomp := eval lazy in (extract expr (length vars)) in
change (extract expr (length vars)) with decomp ;
cbv iota beta ;
match decomp with
| Eprog ?prog' ?consts' =>
let prog := fresh "__prog" in
set (prog := prog') ;
let consts := fresh "__consts" in
set (consts := consts')
end.
Ltac reify_full vars0 :=
(* version without the noise due to let-ins and manual reduction:
match goal with
| |- eval_goal ?g ?y =>
match reify y vars0 with
| (?prog, ?vars) =>
change (eval_goal g (eval prog vars)) ;
rewrite <- (extract_correct prog vars) ;
find_hyps vars
end
end *)
match goal with
| |- eval_goal ?g' ?y =>
let vars := get_vars y vars0 in
let g := fresh "__goal" in
set (g := g') ;
match reify y vars0 with
| (?expr', ?vars) =>
let expr := fresh "__expr" in
set (expr := expr') ;
change (eval_goal g (eval expr vars)) ;
generalize (extract_correct expr vars) ;
let decomp := eval vm_compute in (extract expr (length vars)) in
change (extract expr (length vars)) with decomp ;
cbv iota ;
match decomp with
| Eprog ?prog' ?consts' =>
let prog := fresh "__prog" in
set (prog := prog') ;
let consts := fresh "__consts" in
set (consts := consts')
end ;
apply eq_ind ;
find_hyps vars
end
end ;
match goal with
| |- eval_hyps ?hyps' _ _ =>
let hyps := fresh "__hyps" in
set (hyps := hyps')
reify_partial y vars ;
apply eq_ind ;
find_hyps vars
end.
Module Bnd (I : IntervalOps).
......
......@@ -73,31 +73,71 @@ Fixpoint eval (e : expr) (l : list R) :=
end.
Ltac list_add a l :=
let rec aux a l n :=
let rec aux l :=
match l with
| nil => constr:((n, cons a l))
| cons a _ => constr:((n, l))
| cons ?x ?l =>
match aux a l (S n) with
| (?n, ?l) => constr:((n, cons x l))
end
| nil => constr:(cons a l)
| cons a _ => l
| cons ?x ?l => let l := aux l in constr:(cons x l)
end in
aux a l O.
aux l.
Ltac reify t l :=
Ltac list_find a l :=
let rec aux l n :=
match l with
| nil => false
| cons a _ => n
| cons _ ?l => aux l (S n)
end in
aux l O.
Ltac get_vars t l :=
let rec aux t l :=
let aux_u a := aux a l in
let aux_b a b :=
let l := aux a l in
aux b l in
lazymatch t with
| Ropp ?a => aux_u a
| Rabs ?a => aux_u a
| Rinv ?a => aux_u a
| Rsqr ?a => aux_u a
| Rmult ?a ?a => aux_u a
| sqrt ?a => aux_u a
| cos ?a => aux_u a
| sin ?a => aux_u a
| tan ?a => aux_u a
| atan ?a => aux_u a
| exp ?a => aux_u a
| ln ?a => aux_u a
| powerRZ ?a ?b => aux_u a
| pow ?a ?b => aux_u a
| Rplus ?a ?b => aux_b a b
| Rminus ?a ?b => aux_b a b
| Rplus ?a (Ropp ?b) => aux_b a b
| Rmult ?a ?b => aux_b a b
| Rdiv ?a ?b => aux_b a b
| Rmult ?a (Rinv ?b) => aux_b a b
| Rnearbyint ?a ?b => aux_u b
| IZR (Raux.Ztrunc ?a) => aux_u a
| IZR (Raux.Zfloor ?a) => aux_u a
| IZR (Raux.Zceil ?a) => aux_u a
| IZR (Round_NE.ZnearestE ?a) => aux_u a
| PI => l
| IZR ?n => l
| _ => list_add t l
end in
aux t l.
Ltac reify t l :=
let rec aux t :=
let aux_u o a :=
match aux a l with
| (?u, ?l) => constr:((Eunary o u, l))
end in
let u := aux a in
constr:(Eunary o u) in
let aux_b o a b :=
match aux b l with
| (?v, ?l) =>
match aux a l with
| (?u, ?l) => constr:((Ebinary o u v, l))
end
end in
match t with
let u := aux a in
let v := aux b in
constr:(Ebinary o u v) in
lazymatch t with
| Ropp ?a => aux_u Neg a
| Rabs ?a => aux_u Abs a
| Rinv ?a => aux_u Inv a
......@@ -123,14 +163,13 @@ Ltac reify t l :=
| IZR (Raux.Zfloor ?a) => aux_u (Nearbyint rnd_DN) a
| IZR (Raux.Zceil ?a) => aux_u (Nearbyint rnd_UP) a
| IZR (Round_NE.ZnearestE ?a) => aux_u (Nearbyint rnd_NE) a
| PI => constr:((Econst_pi, l))
| IZR ?n => constr:((Eint n, l))
| PI => constr:(Econst_pi)
| IZR ?n => constr:(Eint n)
| _ =>
match list_add t l with
| (?n, ?l) => constr:((Evar n, l))
end
let n := list_find t l in
constr:(Evar n)
end in
aux t l.
aux t.
Module Bnd (I : IntervalOps).
......
......@@ -1419,6 +1419,18 @@ Inductive expr :=
| Eunary : unary_op -> expr -> expr
| Ebinary : binary_op -> expr -> expr -> expr.
Ltac list_add a l :=
let rec aux a l n :=
match l with
| nil => constr:((n, cons a l))
| cons a _ => constr:((n, l))
| cons ?x ?l =>
match aux a l (S n) with
| (?n, ?l) => constr:((n, cons x l))
end
end in
aux a l O.
Ltac reify t l :=
let rec aux t l :=
match get_float t with
......@@ -1473,21 +1485,12 @@ Ltac reify t l :=
end in
aux t l.
Ltac list_find1 a l :=
let rec aux l n :=
match l with
| nil => false
| cons a _ => n
| cons _ ?l => aux l (S n)
end in
aux l O.
Ltac get_non_constants t :=
let rec aux t l :=
match t with
| Econst _ => l
| _ =>
match list_find1 t l with
match list_find t l with
| false =>
let m :=
match t with
......
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