mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
1413 lines
56 KiB
Plaintext
1413 lines
56 KiB
Plaintext
|
|
module Types
|
|
|
|
use Functions.Func
|
|
(*use import Assoc.Types as AS
|
|
use import Assoc.Logic as AS
|
|
use import Assoc.Impl as AS*)
|
|
use import BacktrackArray.Types as BA
|
|
use import BacktrackArray.Logic as BA
|
|
use import BacktrackArray.Impl as BA
|
|
use Firstorder_symbol_spec.Spec
|
|
use Firstorder_symbol_impl.Types
|
|
use Firstorder_symbol_impl.Logic
|
|
use Firstorder_symbol_impl.Impl
|
|
use Firstorder_term_spec.Spec
|
|
use Firstorder_term_impl.Types
|
|
use Firstorder_term_impl.Logic
|
|
use Firstorder_term_impl.Impl
|
|
|
|
type sdata = PConflict nlimpl_fo_term_list nlimpl_fo_term_list
|
|
| Assign nlimpl_fo_term
|
|
|
|
type subst = BA.t sdata
|
|
type timesubst = BA.timestamp sdata
|
|
|
|
type unifier_subst = {
|
|
ghost unifier_base_model : int -> (fo_term int int) ;
|
|
ghost unifier : int -> (fo_term int int) ;
|
|
}
|
|
|
|
type unification_return = {
|
|
ghost final_unifier : unifier_subst ;
|
|
ghost unifier_factor : int -> (fo_term int int) ;
|
|
}
|
|
|
|
(*type unify_return = {
|
|
ghost factor : int -> (fo_term int int);
|
|
}*)
|
|
|
|
end
|
|
|
|
module Logic
|
|
|
|
use int.Int
|
|
use Functions.Func
|
|
use option.Option
|
|
use import BacktrackArray.Types as BA
|
|
use import BacktrackArray.Logic as BA
|
|
use import BacktrackArray.Impl as BA
|
|
use list.List
|
|
use Firstorder_symbol_spec.Spec
|
|
use Firstorder_symbol_impl.Types
|
|
use Firstorder_symbol_impl.Logic
|
|
use Firstorder_symbol_impl.Impl
|
|
use Firstorder_term_spec.Spec
|
|
use Firstorder_term_impl.Types
|
|
use Firstorder_term_impl.Logic
|
|
use Firstorder_term_impl.Impl
|
|
use Types
|
|
|
|
constant sdata_inv : sdata -> bool
|
|
axiom sdata_inv_def : forall x:sdata.
|
|
sdata_inv x <-> match x with
|
|
| PConflict l1 l2 -> nlimpl_fo_term_list_ok l1 /\
|
|
nlimpl_fo_term_list_ok l2 /\ (forall x:int.
|
|
is_fo_term_free_var_in_fo_term_list x
|
|
l1.model_fo_term_list_field -> x >= 0) /\
|
|
(forall x:int. is_fo_term_free_var_in_fo_term_list x
|
|
l2.model_fo_term_list_field -> x >= 0)
|
|
| Assign l -> nlimpl_fo_term_ok l /\
|
|
(forall x:int. is_fo_term_free_var_in_fo_term x
|
|
l.model_fo_term_field -> x >= 0)
|
|
end
|
|
|
|
function smodel (l:timesubst) : int -> (fo_term int int)
|
|
axiom smodel_def : forall l:timesubst,x:int.
|
|
smodel l x = match table l x with
|
|
| Nil -> Var_fo_term x
|
|
| Cons (PConflict _ _) _ -> Var_fo_term x
|
|
| Cons (Assign u) _ -> u.model_fo_term_field
|
|
end
|
|
|
|
predicate unassigned (l:timesubst) (x:int) = match table l x with
|
|
| Cons (Assign _) _ -> false
|
|
| _ -> true
|
|
end
|
|
|
|
let lemma smodel_depend_only_model (l1 l2:timesubst) : unit
|
|
requires { l1.table = l2.table }
|
|
ensures { smodel l1 = smodel l2 }
|
|
=
|
|
assert { extensionalEqual (smodel l1) (smodel l2) }
|
|
|
|
function sc (s1:'b -> (fo_term 'ls 'b)) (s2:'b -> (fo_term 'ls 'b)) :
|
|
'b -> (fo_term 'ls 'b) =
|
|
subst_compose_fo_term s1 subst_id_symbol s2
|
|
|
|
function st (t:fo_term 'ls 'b) (s:'b -> (fo_term 'ls 'b)) : fo_term 'ls 'b =
|
|
subst_fo_term t subst_id_symbol s
|
|
|
|
function stl (t:fo_term_list 'ls 'b)
|
|
(s:'b -> (fo_term 'ls 'b)) : fo_term_list 'ls 'b =
|
|
subst_fo_term_list t subst_id_symbol s
|
|
|
|
(*
|
|
(* power relation. *)
|
|
|
|
inductive power_rel (s:'b -> (fo_term 'ls 'b)) (n:int)
|
|
(sr:'b -> (fo_term 'ls 'b)) =
|
|
| Power0 : forall s:'b -> (fo_term 'ls 'b).
|
|
power_rel s 0 subst_id_fo_term
|
|
| Powern : forall s:'b -> (fo_term 'ls 'b),n:int,
|
|
sr:'b -> (fo_term 'ls 'b).
|
|
n >= 0 /\ power_rel s n sr ->
|
|
power_rel s (n+1) (sc s sr)
|
|
|
|
let rec lemma power_rel_det (s:'b -> (fo_term 'ls 'b)) (n:int) : unit
|
|
ensures { forall sr1 sr2:'b -> (fo_term 'ls 'b).
|
|
power_rel s n sr1 /\ power_rel s n sr2 -> sr1 = sr2 }
|
|
variant { n }
|
|
=
|
|
if n > 0
|
|
then power_rel_det s (n-1)
|
|
|
|
let rec lemma power_rel_additive (s:'b -> (fo_term 'ls 'b)) (n m:int)
|
|
(srm:'b -> (fo_term 'ls 'b)) : unit
|
|
ensures { forall srn:'b -> (fo_term 'ls 'b).
|
|
power_rel s n srn /\ power_rel s m srm ->
|
|
power_rel s (n+m) (sc srn srm) }
|
|
variant { n }
|
|
=
|
|
if n > 0
|
|
then power_rel_additive s (n-1) m srm
|
|
|
|
let rec ghost power (s:'b -> (fo_term 'ls 'b)) (n:int) :
|
|
'b -> (fo_term 'ls 'b)
|
|
requires { n >= 0 }
|
|
ensures { power_rel s n result }
|
|
variant { n }
|
|
=
|
|
if n = 0
|
|
then subst_id_fo_term
|
|
else sc s (power s (n-1))
|
|
|
|
let rec lemma power_fixed_point (s:'b -> (fo_term 'ls 'b)) (n:int)
|
|
(x:'b) : unit
|
|
requires { s x = Var_fo_term x }
|
|
ensures { forall srn:'b -> (fo_term 'ls 'b).
|
|
power_rel s n srn -> srn x = Var_fo_term x }
|
|
variant { n }
|
|
=
|
|
if n > 0
|
|
then power_fixed_point s (n-1) x
|
|
*)
|
|
|
|
(* In other words : unifier is the idempotent limit reached by power
|
|
iteration of the model of unifier_base, which is unifier_base_model,
|
|
and iteration is an exponent reaching the fixed point. *)
|
|
|
|
predicate unifier_subst_ok (rho:subst) (u:unifier_subst) =
|
|
smodel (BA.current_timestamp rho) = u.unifier_base_model /\
|
|
(forall x:int. eval u.unifier_base_model x = Var_fo_term x ->
|
|
unassigned (BA.current_timestamp rho) x) /\
|
|
(*power_rel u.unifier_base_model u.iteration u.unifier /\
|
|
u.iteration > 0 /\*)
|
|
(* Replace *) (forall x:int. eval u.unifier_base_model x = Var_fo_term x ->
|
|
eval u.unifier x = Var_fo_term x) /\
|
|
sc u.unifier_base_model u.unifier = u.unifier /\
|
|
sc u.unifier u.unifier_base_model = u.unifier /\
|
|
sc u.unifier u.unifier = u.unifier /\
|
|
BA.correct rho /\
|
|
rho.inv = sdata_inv
|
|
|
|
(*let rec lemma size_term_increase (t:fo_term int int) (x:int)
|
|
(s:int -> (fo_term int int)) : unit
|
|
ensures { is_fo_term_free_var_in_fo_term x t ->
|
|
size_fo_term (subst_fo_term t subst_id_symbol s)
|
|
>= size_fo_term t + size_fo_term (s x) -
|
|
size_fo_term (Var_fo_term x:fo_term int int) }
|
|
ensures { size_fo_term (subst_fo_term t subst_id_symbol s) >=
|
|
size_fo_term t }
|
|
variant { size_fo_term t }
|
|
=
|
|
match t with
|
|
| Var_fo_term _ -> ()
|
|
| App _ l -> size_list_increase l x s
|
|
end
|
|
|
|
with lemma size_list_increase (t:fo_term_list int int) (x:int)
|
|
(s:int -> (fo_term int int)) : unit
|
|
ensures { is_fo_term_free_var_in_fo_term_list x t ->
|
|
size_fo_term_list (subst_fo_term_list t subst_id_symbol s)
|
|
>= size_fo_term_list t + size_fo_term (s x) -
|
|
size_fo_term (Var_fo_term x:fo_term int int) }
|
|
ensures { size_fo_term_list (subst_fo_term_list t subst_id_symbol s)
|
|
>= size_fo_term_list t }
|
|
variant { size_fo_term_list t }
|
|
=
|
|
match t with
|
|
| FONil -> ()
|
|
| FOCons u q -> size_term_increase u x s ;
|
|
size_list_increase q x s
|
|
end*)
|
|
|
|
end
|
|
|
|
module Impl
|
|
|
|
use int.Int
|
|
use Functions.Func
|
|
use option.Option
|
|
use import BacktrackArray.Types as BA
|
|
use import BacktrackArray.Logic as BA
|
|
use import BacktrackArray.Impl as BA
|
|
use list.List
|
|
use Firstorder_symbol_spec.Spec
|
|
use Firstorder_symbol_impl.Types
|
|
use Firstorder_symbol_impl.Logic
|
|
use Firstorder_symbol_impl.Impl
|
|
use Firstorder_term_spec.Spec
|
|
use Firstorder_term_impl.Types
|
|
use Firstorder_term_impl.Logic
|
|
use Firstorder_term_impl.Impl
|
|
use Types
|
|
use Logic
|
|
use ref.Ref
|
|
use list.Mem
|
|
|
|
exception UnificationFailure
|
|
|
|
(* Utility for a frequent reasoning that
|
|
allow to decrease variant. *)
|
|
(*let ghost checkit (rhob:subst) (rho:unifier_subst) (x:int) (*(it:int)*) : unit
|
|
(*requires { it >= 0 }
|
|
requires { forall sp:int -> (fo_term int int).
|
|
let tm = Var_fo_term x in
|
|
power_rel rho.unifier_base_model it sp ->
|
|
st tm sp = st tm rho.unifier }*)
|
|
requires { unifier_subst_ok rhob rho }
|
|
requires { match table (BA.current_timestamp rhob) x with
|
|
| Cons (Assign _) _ -> true
|
|
| _ -> false
|
|
end }
|
|
(*ensures { it >= 1 }*)
|
|
ensures { forall sp:int -> (fo_term int int).
|
|
let tm = eval rho.unifier_base_model x in
|
|
power_rel rho.unifier_base_model (it-1) sp ->
|
|
st tm sp = st tm rho.unifier }
|
|
=
|
|
let rho0 = rho.unifier in
|
|
let tm = (Var_fo_term x:fo_term int int) in
|
|
assert { (it = 0 -> tm = st tm subst_id_fo_term
|
|
= st tm rho0 && tm = st tm (sc rho0 rho.unifier_base_model)
|
|
= st tm rho.unifier_base_model &&
|
|
eval rho.unifier_base_model x = Var_fo_term x &&
|
|
match table (BA.current_timestamp rhob) x with
|
|
| Cons (Assign _) _ -> false
|
|
| _ -> true
|
|
end) && it <> 0 } ;
|
|
assert { forall sp:int -> (fo_term int int).
|
|
let rho0 = rho.unifier_base_model in
|
|
let rhoi = rho.unifier in
|
|
let tm = rho0 x in
|
|
let mx = Var_fo_term x in
|
|
power_rel rho0 (it-1) sp ->
|
|
power_rel rho0 it (sc rho0 sp) &&
|
|
st tm sp = st mx (sc rho0 sp) = st mx rhoi =
|
|
st mx (sc rho0 rhoi) = st tm rhoi && st tm sp = st tm rhoi }*)
|
|
|
|
let ghost bottomvar (rhob:subst) (ghost rho:unifier_subst) (x:int) : unit
|
|
requires { unifier_subst_ok rhob rho }
|
|
requires { unassigned (BA.current_timestamp rhob) x }
|
|
ensures { let tm = Var_fo_term x in
|
|
tm = st tm rho.unifier_base_model /\
|
|
tm = st tm rho.unifier }
|
|
=
|
|
assert { eval rho.unifier_base_model x = Var_fo_term x } ;
|
|
assert { eval rho.unifier x = Var_fo_term x }
|
|
|
|
(* Check presence of a variable inside the fully substituted term. *)
|
|
let rec check_unified_free_var (x:int) (t:nlimpl_fo_term)
|
|
(rhob:subst) (ghost rho:unifier_subst)
|
|
(*(ghost it:int)*) : unit
|
|
requires { unifier_subst_ok rhob rho }
|
|
requires { nlimpl_fo_term_ok t }
|
|
(* Variant requirement. *)
|
|
(*requires { forall sp:int -> (fo_term int int).
|
|
let tm = t.model_fo_term_field in
|
|
power_rel rho.unifier_base_model it sp ->
|
|
st tm sp = st tm rho.unifier }*)
|
|
(*requires { it >= 0 }*)
|
|
requires { forall y:int. is_fo_term_free_var_in_fo_term y
|
|
t.model_fo_term_field -> y >= 0 }
|
|
diverges (* variant { 0 } *)
|
|
(* variant { it , size_fo_term t.model_fo_term_field } *)
|
|
ensures { not(is_fo_term_free_var_in_fo_term x
|
|
(st t.model_fo_term_field rho.unifier)) }
|
|
raises { UnificationFailure (*->
|
|
is_fo_term_free_var_in_fo_term x (st t.model_fo_term_field rho.unifier)*) }
|
|
=
|
|
let tm = t.model_fo_term_field in
|
|
let rho0 = rho.unifier in
|
|
match destruct_fo_term t with
|
|
| NLCVar_fo_term y -> assert { tm = Var_fo_term y } ;
|
|
assert { (y < 0 -> table (BA.current_timestamp rhob) y = Nil
|
|
&& eval rho.unifier_base_model y = Var_fo_term y
|
|
&& eval rho.unifier y = Var_fo_term y
|
|
&& st tm rho.unifier = Var_fo_term y
|
|
&& is_fo_term_free_var_in_fo_term y (st tm rho.unifier)) && y >= 0 } ;
|
|
let by' = BA.get rhob y in
|
|
match by' with
|
|
| Nil -> bottomvar rhob rho y ;
|
|
if x = y
|
|
then raise UnificationFailure
|
|
| Cons (PConflict _ _) _ -> bottomvar rhob rho y ;
|
|
if x = y
|
|
then raise UnificationFailure
|
|
| Cons (Assign t2) _ -> assert { sdata_inv (Assign t2) } ;
|
|
let t2m = t2.model_fo_term_field in
|
|
assert { st tm rho0 = eval rho0 y = st t2m rho0 } ;
|
|
(*checkit rhob rho y it ;*)
|
|
check_unified_free_var x t2 rhob rho (*(it-1)*)
|
|
end
|
|
| NLC_App f l -> let fm = f.model_symbol_field in
|
|
let lm = l.model_fo_term_list_field in
|
|
assert { tm = App fm lm } ;
|
|
assert { forall s:int -> (fo_term int int).
|
|
st tm s = App fm (stl lm s) } ;
|
|
check_unified_free_var_list x l rhob rho (*it*)
|
|
end
|
|
|
|
with check_unified_free_var_list (x:int) (t:nlimpl_fo_term_list)
|
|
(rhob:subst) (ghost rho:unifier_subst) (*(ghost it:int)*) : unit
|
|
requires { nlimpl_fo_term_list_ok t }
|
|
requires { unifier_subst_ok rhob rho }
|
|
(* Variant requirement. *)
|
|
(*requires { forall sp:int -> (fo_term int int).
|
|
let tm = t.model_fo_term_list_field in
|
|
power_rel rho.unifier_base_model it sp ->
|
|
stl tm sp = stl tm rho.unifier }*)
|
|
(*requires { it >= 0 }*)
|
|
requires { forall y:int. is_fo_term_free_var_in_fo_term_list y
|
|
t.model_fo_term_list_field -> y >= 0 }
|
|
diverges (* variant { 0 } *)
|
|
(*variant { it , size_fo_term_list t.model_fo_term_list_field }*)
|
|
ensures { not(is_fo_term_free_var_in_fo_term_list x
|
|
(stl t.model_fo_term_list_field rho.unifier)) }
|
|
raises { UnificationFailure (*->
|
|
is_fo_term_free_var_in_fo_term_list x
|
|
(stl t.model_fo_term_list_field rho.unifier)*) }
|
|
=
|
|
let tm = t.model_fo_term_list_field in
|
|
let rho0 = rho.unifier in
|
|
match destruct_fo_term_list t with
|
|
| NLC_FONil -> ()
|
|
| NLC_FOCons u q -> let um = u.model_fo_term_field in
|
|
let qm = q.model_fo_term_list_field in
|
|
assert { tm = FOCons um qm } ;
|
|
assert { forall s:int -> (fo_term int int).
|
|
stl tm s = FOCons (st um s) (stl qm s) } ;
|
|
check_unified_free_var x u rhob rho (*it*) ;
|
|
check_unified_free_var_list x q rhob rho (*it*)
|
|
end
|
|
|
|
(*
|
|
(* to prevent : 1) expanding of t0 as a record,
|
|
2) inlining of nlimpl_fo_term *)
|
|
predicate ugly_hack (rho:table int nlimpl_fo_term) =
|
|
forall x:int, t0:nlimpl_fo_term.
|
|
AS.model rho x = Some t0 -> nlimpl_fo_term_ok t0
|
|
*)
|
|
|
|
(* Unification core routine : set a variable to some equation. *)
|
|
|
|
let assign (z:int) (t:nlimpl_fo_term) (lv:ref (list int)) (rhob:subst)
|
|
(ghost rho:unifier_subst) (ghost lp:int -> bool)
|
|
(*(ghost fv s:S.set int)*) : unification_return
|
|
|
|
(* Invariant requirements. *)
|
|
requires { z >= 0 }
|
|
requires { nlimpl_fo_term_ok t }
|
|
requires { unifier_subst_ok rhob rho }
|
|
|
|
|
|
(* Essential requirement : the variable is not yet assigned. *)
|
|
requires { unassigned (current_timestamp rhob) z }
|
|
(* Essential requirement given the structure invariants :
|
|
do not assign a variable to itself. *)
|
|
requires { st t.model_fo_term_field rho.unifier <> Var_fo_term z }
|
|
|
|
requires { forall y:int. is_fo_term_free_var_in_fo_term y
|
|
t.model_fo_term_field -> y >= 0 }
|
|
|
|
requires { forall x:int. mem x !lv ->
|
|
lp x /\ x >= 0 }
|
|
requires { forall x:int. unassigned (current_timestamp rhob) x -> lp x }
|
|
ensures { forall x:int. mem x !lv ->
|
|
lp x /\ x >= 0 }
|
|
ensures { forall x:int. unassigned (current_timestamp rhob) x -> lp x }
|
|
|
|
(* Invariant ensures. *)
|
|
ensures { unifier_subst_ok rhob result.final_unifier }
|
|
ensures { precede (old rhob) rhob }
|
|
|
|
(* Unifier properties. *)
|
|
ensures { sc rho.unifier result.unifier_factor =
|
|
result.final_unifier.unifier }
|
|
ensures { forall s:int -> (fo_term int int).
|
|
let s' = sc rho.unifier s in
|
|
s' z = st t.model_fo_term_field s' ->
|
|
s' = sc result.final_unifier.unifier s }
|
|
ensures { let s0 = result.final_unifier.unifier in
|
|
s0 z = st t.model_fo_term_field s0 }
|
|
ensures { let s0 = result.final_unifier.unifier in
|
|
let s1 = rho.unifier_base_model in
|
|
sc s0 s1 = s0 = sc s1 s0 }
|
|
ensures { let s0 = result.final_unifier.unifier in
|
|
let s1 = rho.unifier in
|
|
sc s0 s1 = s0 = sc s1 s0 }
|
|
|
|
diverges
|
|
(* Variant post-conditions. *)
|
|
(*ensures { cardinal result.unassigned_set < cardinal s }
|
|
ensures { forall x:int.
|
|
mem x fv /\ AS.model result.final_unifier.unifier_base x = None ->
|
|
mem x result.unassigned_set }
|
|
ensures { forall x y:int.
|
|
mem x fv /\
|
|
is_fo_term_free_var_in_fo_term y (
|
|
eval result.final_unifier.unifier_base_model x)
|
|
-> mem y fv }*)
|
|
raises { UnificationFailure -> precede (old rhob) rhob /\
|
|
correct rhob
|
|
(*-> forall s:int -> (fo_term int int).
|
|
let s' = sc rho.unifier s in
|
|
s' z <> st t.model_fo_term_field s'*) }
|
|
=
|
|
label Init in
|
|
assert { forall s1 s2 s3:int -> (fo_term int int).
|
|
sc s1 (sc s2 s3) = sc (sc s1 s2) s3 } ;
|
|
assert { forall t0:fo_term int int,s1 s2:int -> (fo_term int int).
|
|
st (st t0 s1) s2 = st t0 (sc s1 s2) } ;
|
|
let tm = t.model_fo_term_field in
|
|
let rho0 = rho.unifier_base_model in
|
|
let rhoi = rho.unifier in
|
|
let ghost stm = st tm rhoi in
|
|
(*let n0 = rho.iteration in*)
|
|
bottomvar rhob rho z;
|
|
assert { rho0 z = Var_fo_term z } ;
|
|
assert { rhoi z = Var_fo_term z } ;
|
|
(*assert { forall s:int -> (fo_term int int).
|
|
is_fo_term_free_var_in_fo_term z stm ->
|
|
match stm with
|
|
| Var_fo_term _ -> false
|
|
| _ -> size_fo_term (st stm s) > size_fo_term (s z) end &&
|
|
size_fo_term (st tm (sc rhoi s)) > size_fo_term (s z) &&
|
|
s z = sc rhoi s z && st tm (sc rhoi s) <> sc rhoi s z } ;*)
|
|
check_unified_free_var z t rhob rho (*rho.iteration*) ;
|
|
let ghost uf = subst_id_fo_term[z <- stm] in
|
|
let ghost rhoi' = sc rhoi uf in
|
|
let ghost rho0' = rho0[z <- tm] in
|
|
BA.add z (Assign t) rhob ;
|
|
lv := Cons z !lv;
|
|
(*let n1 = 2 * n0 + 1 in*)
|
|
assert { let rho' = current_timestamp (rhob at Init) in
|
|
let rho'' = current_timestamp rhob in
|
|
(forall x:int.
|
|
(x <> z -> table rho'' x = table rho' x &&
|
|
(smodel rho'' x = smodel rho' x = rho0 x = rho0' x)) /\
|
|
(x = z -> (smodel rho'' x = t.model_fo_term_field = rho0' x))) &&
|
|
extensionalEqual (smodel rho'') rho0' &&
|
|
smodel rho'' = rho0' } ;
|
|
let ghost rho0'' = rho0[z <- stm] in
|
|
assert { (forall x:int.
|
|
(x <> z -> uf x = Var_fo_term x && rho0'' x = rho0 x = sc uf rho0 x) /\
|
|
(x = z -> rho0'' x = stm = st stm rho0 = sc uf rho0 x)) &&
|
|
extensionalEqual rho0'' (sc uf rho0) && rho0'' = sc uf rho0 } ;
|
|
free_var_equivalence_of_subst_fo_term stm subst_id_symbol
|
|
subst_id_symbol rho0 rho0' ;
|
|
assert { (forall x:int.
|
|
(x <> z -> uf x = Var_fo_term x &&
|
|
rho0'' x = rho0 x = rho0' x = sc uf rho0' x) /\
|
|
(x = z -> rho0'' x = stm = st stm rho0 = st stm rho0' = sc uf rho0 x)) &&
|
|
extensionalEqual rho0'' (sc uf rho0') && rho0'' = sc uf rho0' } ;
|
|
(*assert { forall r:int -> (fo_term int int).
|
|
power_rel r 0 subst_id_fo_term /\ sc r subst_id_fo_term = r &&
|
|
power_rel r 1 r } ;*)
|
|
(*let rec ghost aux0 (m:int) (sp1 sp2:int -> (fo_term int int)) : unit
|
|
requires { m >= 0 }
|
|
requires { power_rel rho0 m sp1 /\ power_rel rho0'' m sp2 }
|
|
variant { m }
|
|
ensures { sc sp2 uf = sc sp1 uf }
|
|
ensures { sc rhoi sp1 = rhoi }
|
|
ensures { sc sp1 rhoi = rhoi }
|
|
=
|
|
if m <> 0
|
|
then ( let sp1' = power rho0 (m-1) in
|
|
let sp2' = power rho0'' (m-1) in
|
|
aux0 (m-1) sp1' sp2' ;
|
|
free_var_equivalence_of_subst_fo_term stm subst_id_symbol
|
|
subst_id_symbol subst_id_fo_term uf ;
|
|
assert { power_rel rho0 1 rho0 &&
|
|
power_rel rho0'' 1 rho0'' &&
|
|
(power_rel rho0 m (sc rho0 sp1') /\
|
|
power_rel rho0 m (sc sp1' rho0)) &&
|
|
power_rel rho0'' m (sc rho0'' sp2') &&
|
|
sc sp1' rho0 = sp1 = sc rho0 sp1' && sp2 = sc rho0'' sp2'} ;
|
|
assert { sc rhoi sp1 = sc rhoi sp1' = rhoi = sc sp1' rhoi = sc sp1 rhoi
|
|
&& st stm sp1 = st tm (sc rhoi sp1) = st tm rhoi = stm } ;
|
|
assert {
|
|
sc sp2 uf = sc rho0'' (sc sp2' uf) = sc (sc uf rho0) (sc sp1' uf)
|
|
= sc uf (sc sp1 uf) &&
|
|
(forall x:int. x <> z ->
|
|
sc uf (sc sp1 uf) x = sc sp1 uf x) &&
|
|
(sc uf (sc sp1 uf) z = st stm (sc sp1 uf) = st stm uf = stm
|
|
= uf z = sc sp1 uf z)
|
|
&& extensionalEqual (sc uf (sc sp1 uf)) (sc sp1 uf)
|
|
&& sc sp2 uf = sc sp1 uf })
|
|
else assert { sp1 = subst_id_fo_term }
|
|
in*)
|
|
(*
|
|
let rec ghost aux1 (m:int) (sp1 sp2:int -> (fo_term int int)) : unit
|
|
requires { m >= 0 }
|
|
requires { power_rel rho0 m sp1 }
|
|
requires { power_rel rho0' m sp2 }
|
|
variant { m }
|
|
ensures { st tm sp1 = st tm sp2 }
|
|
=
|
|
if m <> 0
|
|
then (
|
|
let sp1' = power rho0 (m-1) in
|
|
let sp2' = power rho0' (m-1) in
|
|
assert { power_rel rho0 1 rho0 &&
|
|
power_rel rho0 m (sc sp1' rho0) &&
|
|
sp1 = sc sp1' rho0 } ;
|
|
assert { power_rel rho0' 1 rho0' &&
|
|
power_rel rho0' m (sc sp2' rho0') &&
|
|
sc sp2' rho0' = sp2 } ;
|
|
aux1 (m-1) sp1' sp2' ;
|
|
aux0 (m-1) sp1' (power rho0'' (m-1)) ;
|
|
assert { is_fo_term_free_var_in_fo_term z (rhoi z) &&
|
|
(is_fo_term_free_var_in_fo_term z (st tm sp1') ->
|
|
is_fo_term_free_var_in_fo_term z (st (st tm sp1') rhoi) &&
|
|
is_fo_term_free_var_in_fo_term z stm) &&
|
|
not(is_fo_term_free_var_in_fo_term z (st tm sp1')) } ;
|
|
free_var_equivalence_of_subst_fo_term (st tm sp1') subst_id_symbol
|
|
subst_id_symbol rho0 rho0'
|
|
)
|
|
else assert { sp1 = subst_id_fo_term = sp2 }
|
|
in*)(*
|
|
let rec ghost aux2 (m:int) (sp1 sp2 sp3:int -> (fo_term int int)) : unit
|
|
requires { m >= 0 }
|
|
requires { power_rel rho0 m sp2 /\
|
|
power_rel rho0' n0 sp3 /\
|
|
power_rel rho0' (m+n0+1) sp1 }
|
|
variant { m }
|
|
ensures { sp1 = sc sp2 (sc rho0'' sp3) }
|
|
=
|
|
let sp0 = sc rhoi rhoi in
|
|
assert { power_rel rho0 (n0+n0) sp0 } ;
|
|
aux0 n0 rhoi (power rho0'' n0) ; (*rho0^(2*n0) = rhoi *)
|
|
aux1 n0 rhoi sp3 ; (* st t rho^n0 = st t rho'^n0 *)
|
|
let sp3_ = sc sp3 sp3 in
|
|
assert { power_rel rho0' (2*n0) sp3_ } ;
|
|
aux1 (2*n0) sp0 sp3_ ; (* st t rho^(2*n0) = st t (rho'^(2*n0)) *)
|
|
assert { st tm sp3 = st tm rhoi = st tm sp0 = st tm sp3_
|
|
= st (st tm sp3) sp3 = st (st tm rhoi) sp3 = st stm sp3 } ;
|
|
assert { extensionalEqual (sc rho0' sp3)
|
|
(update (sc rho0 sp3) z (st tm sp3)) } ;
|
|
assert { extensionalEqual (sc rho0'' sp3)
|
|
(update (sc rho0 sp3) z (st stm sp3)) } ;
|
|
assert { sc rho0' sp3 = sc rho0'' sp3 } ;
|
|
assert { power_rel rho0' (1+n0) (sc rho0' sp3) &&
|
|
power_rel rho0' (n0+1) (sc sp3 rho0') &&
|
|
sc sp3 rho0' = sc rho0' sp3 } ;
|
|
if m = 0
|
|
then assert { sp2 = subst_id_fo_term /\
|
|
sp1 = sc rho0' sp3 }
|
|
else (
|
|
let sp1' = power rho0' (m+n0) in
|
|
assert { power_rel rho0' (m+n0+1) (sc sp1' rho0') &&
|
|
sp1 = sc sp1' rho0' } ;
|
|
let sp2' = power rho0 (m-1) in
|
|
assert { power_rel rho0 1 rho0 &&
|
|
power_rel rho0 ((m-1)+1) (sc sp2' rho0) &&
|
|
sc sp2' rho0 = sp2 } ;
|
|
aux2 (m-1) sp1' sp2' sp3 ;
|
|
free_var_equivalence_of_subst_fo_term stm subst_id_symbol
|
|
subst_id_symbol rho0'' rho0 ;
|
|
assert { (forall x:int. x <> z ->
|
|
sc rho0'' rho0'' x = sc rho0 rho0'' x) /\
|
|
sc rho0'' rho0'' z = st stm rho0'' = st stm rho0
|
|
= st tm (sc rhoi rho0) = stm = sc rho0 rho0'' z } ;
|
|
assert { extensionalEqual (sc rho0'' rho0'') (sc rho0 rho0'') } ;
|
|
assert { sp1 = sc sp2' (sc (sc rho0'' sp3) rho0')
|
|
= sc sp2' (sc rho0'' (sc sp3 rho0'))
|
|
= sc sp2' (sc rho0'' (sc rho0'' sp3))
|
|
= sc (sc sp2' (sc rho0'' rho0'')) sp3
|
|
= sc (sc (sc sp2' rho0) rho0'') sp3
|
|
= sc (sc sp2' rho0) (sc rho0'' sp3)
|
|
= sc sp2 (sc rho0'' sp3) }
|
|
)
|
|
in*)
|
|
(*let sp3 = power rho0' n0 in
|
|
let rhoi_ = power rho0' n1 in
|
|
aux2 n0 rhoi_ rhoi sp3 ;
|
|
assert { power_rel rho0' 1 rho0' &&
|
|
power_rel rho0' (1+n1) (sc rho0' rhoi_) &&
|
|
power_rel rho0' (n1+1) (sc rhoi_ rho0') } ;
|
|
assert { power_rel rho0 1 rho0 &&
|
|
power_rel rho0 (1+n0) (sc rho0 rhoi) } ;
|
|
aux2 (1+n0) (sc rho0' rhoi_) (sc rho0 rhoi) sp3 ;
|
|
assert { sc rhoi' (sc rho0 sp3)
|
|
= sc rhoi (sc uf (sc rho0 sp3)) = rhoi_
|
|
= sc rho0' rhoi_
|
|
= sc (sc rho0 rhoi) (sc rho0'' sp3)
|
|
= sc rho0 (sc rhoi (sc rho0'' sp3))
|
|
= sc rho0 rhoi_ } ;
|
|
assert { rhoi_ = sc rhoi_ rho0' } ;
|
|
assert { rhoi_ = sc (sc rhoi' rho0) sp3
|
|
= sc (sc rhoi' rho0') sp3 = sc rhoi' (sc rho0' sp3) } ;*)
|
|
(*let rec ghost aux3 (m:int) (sp:int -> (fo_term int int)) : unit
|
|
requires { m >= 0 }
|
|
requires { power_rel rho0' m sp }
|
|
variant { m }
|
|
ensures { sc rhoi' sp = rhoi' }
|
|
=
|
|
if m = 0
|
|
then assert { sp = subst_id_fo_term }
|
|
else (
|
|
let sp' = power rho0' (m-1) in
|
|
assert { power_rel rho0' 1 rho0' &&
|
|
power_rel rho0' m (sc rho0' sp') &&
|
|
sc rho0' sp' = sp } ;
|
|
aux3 (m-1) sp' ;
|
|
assert { forall x:int.
|
|
(forall y:int.
|
|
is_fo_term_free_var_in_fo_term y (rhoi x) ->
|
|
st (rhoi x) rho0 = st (rhoi x) subst_id_fo_term &&
|
|
rho0 y = subst_id_fo_term y &&
|
|
rho0'' y = uf y) &&
|
|
(forall y:int.
|
|
is_fo_term_free_var_in_fo_term y (rhoi x) ->
|
|
rho0'' y = uf y) &&
|
|
(forall y:int.
|
|
is_symbol_free_var_in_fo_term y (rhoi x) ->
|
|
subst_id_symbol y = subst_id_symbol y) &&
|
|
st (rhoi x) rho0'' = st (rhoi x) uf &&
|
|
sc rhoi rho0'' x = sc rhoi uf x } ;
|
|
assert { extensionalEqual (sc rhoi rho0'') (sc rhoi uf) &&
|
|
sc rhoi' rho0' = sc rhoi' rho0 = sc rhoi (sc uf rho0)
|
|
= sc rhoi rho0'' = sc rhoi uf = rhoi' &&
|
|
sc rhoi' sp = sc rhoi' sp' = rhoi' }
|
|
) in
|
|
aux3 (n0+1) (sc rho0' sp3) ;*)
|
|
(* Main difficulty done : rhoi' is indeed the idempotent limit of rho0'. *)
|
|
(*assert { rhoi_ = rhoi' } ;
|
|
aux3 n1 rhoi_ ;*)
|
|
(*assert { sc rhoi' rhoi' = rhoi' } ;*)
|
|
(*let rec ghost aux4 (m:int) (sp:int -> (fo_term int int)) : unit
|
|
requires { m >= 0 }
|
|
requires { power_rel rho0 m sp }
|
|
variant { m }
|
|
ensures { sc rhoi' sp = rhoi' }
|
|
=
|
|
if m = 0
|
|
then assert { sp = subst_id_fo_term }
|
|
else (
|
|
let sp' = power rho0 (m-1) in
|
|
assert { power_rel rho0 1 rho0 &&
|
|
power_rel rho0 m (sc rho0 sp') &&
|
|
sc rho0 sp' = sp } ;
|
|
aux4 (m-1) sp' ;
|
|
assert { sc rhoi' sp = sc (sc rhoi' rho0) sp' = sc rhoi' sp' }
|
|
) in
|
|
aux4 n0 rhoi ;
|
|
assert { forall x:int, t0:nlimpl_fo_term.
|
|
AS.model rho'' x = Some t0 ->
|
|
((x = z -> t0 = t) /\ (x <> z ->
|
|
AS.model rho.unifier_base x = AS.model rho'.unifier_base x
|
|
= AS.model rho'' x &&
|
|
AS.model rho.unifier_base x = Some t0))
|
|
&& nlimpl_fo_term_ok t0 } ;
|
|
assert { ugly_hack rho'' } ;*)
|
|
free_var_equivalence_of_subst_fo_term stm subst_id_symbol
|
|
subst_id_symbol uf subst_id_fo_term ;
|
|
assert { rhoi' z = st (rhoi z) uf = st (Var_fo_term z) uf
|
|
= stm = st stm uf = st tm rhoi' } ;
|
|
assert { ((forall x:int.
|
|
x <> z -> uf x = Var_fo_term x && sc uf rhoi' x = rhoi' x) /\
|
|
(sc uf rhoi' z = st stm rhoi' = st (st stm rhoi) uf = st (st tm rhoi) uf
|
|
= st stm uf = stm = uf z = st (Var_fo_term z) uf =
|
|
sc rhoi uf z = rhoi' z
|
|
)) && extensionalEqual (sc uf rhoi') rhoi' &&
|
|
sc rhoi' rhoi' = rhoi' } ;
|
|
(*assert { forall x y:int.
|
|
mem x fv /\ is_fo_term_free_var_in_fo_term y (rho0' x) ->
|
|
((x = z -> rho0' x = tm && mem y fv) /\
|
|
(x <> z -> rho0' x = rho0 x && mem y fv)) && mem y fv } ;
|
|
assert { forall x:int.
|
|
mem x fv /\
|
|
AS.model rho'' x = None ->
|
|
x <> z && AS.model rho'' x = AS.model rho.unifier_base x &&
|
|
mem x s && mem x (remove z s) } ;*)
|
|
assert { forall s0:int -> (fo_term int int).
|
|
let s0' = sc rhoi s0 in
|
|
s0' z = st tm s0' ->
|
|
st stm s0 = s0' z = st (rhoi z) s0 = s0 z &&
|
|
(forall x:int. x <> z ->
|
|
update s0 z (st stm s0) x = s0 x = st (uf x) s0 &&
|
|
update s0 z (st stm s0) x = sc uf s0 x) &&
|
|
(update s0 z (st stm s0) z = st stm s0 = st (uf z) s0 &&
|
|
update s0 z (st stm s0) z = sc uf s0 z) &&
|
|
extensionalEqual (sc uf s0) (update s0 z (st stm s0)) &&
|
|
extensionalEqual (update s0 z (s0 z)) s0 &&
|
|
sc uf s0 = s0 &&
|
|
sc rhoi' s0 = sc rhoi (sc uf s0) = sc rhoi s0 } ;
|
|
assert { sc rho0 rhoi' = sc (sc rho0 rhoi) uf = rhoi' } ;
|
|
assert { sc rhoi rhoi' = sc (sc rhoi rhoi) uf = rhoi' } ;
|
|
assert { sc rhoi' rho0 = sc rhoi rho0'' = sc rhoi' rho0' } ;
|
|
assert { (forall x:int. let tx = rhoi x in
|
|
st tx rho0 = st tx subst_id_fo_term &&
|
|
(forall y:int. is_fo_term_free_var_in_fo_term y tx ->
|
|
rho0 y = subst_id_fo_term y) &&
|
|
(forall y:int. is_fo_term_free_var_in_fo_term y tx ->
|
|
rho0'' y = uf y) &&
|
|
st tx rho0'' = st tx uf
|
|
) &&
|
|
extensionalEqual (sc rhoi rho0'') rhoi' &&
|
|
sc rhoi' rho0 = rhoi' = sc rhoi' rho0' } ;
|
|
let ghost rhoi'' = rhoi[z <- stm] in
|
|
assert { ((forall x:int. x <> z ->
|
|
uf x = Var_fo_term x &&
|
|
rhoi'' x = rhoi x = sc uf rhoi x) /\
|
|
(rhoi'' z = stm = st stm rhoi = sc uf rhoi z)
|
|
) && extensionalEqual rhoi'' (sc uf rhoi) } ;
|
|
assert { (forall x:int. let tx = rhoi x in
|
|
st tx rhoi = st tx subst_id_fo_term &&
|
|
(forall y:int. is_fo_term_free_var_in_fo_term y tx ->
|
|
rhoi y = subst_id_fo_term y) &&
|
|
(forall y:int. is_fo_term_free_var_in_fo_term y tx ->
|
|
rhoi'' y = uf y) &&
|
|
st tx rhoi'' = st tx uf
|
|
) &&
|
|
extensionalEqual (sc rhoi rhoi'') rhoi' &&
|
|
sc rhoi' rhoi = rhoi' } ;
|
|
assert { ((forall x:int. x <> z ->
|
|
sc rho0' rhoi' x = st (rho0 x) rhoi' = rhoi' x) /\
|
|
(sc rho0' rhoi' z = st (st tm rhoi) uf = st stm uf = stm
|
|
= uf z = st (rhoi z) uf = rhoi' z)) &&
|
|
extensionalEqual (sc rho0' rhoi') rhoi' && sc rho0' rhoi' = rhoi' } ;
|
|
assert { forall x:int.
|
|
(rho0' x = Var_fo_term x -> x <> z &&
|
|
((rho0' x = rho0 x = Var_fo_term x &&
|
|
rhoi x = Var_fo_term x &&
|
|
rhoi' x = uf x = Var_fo_term x) /\
|
|
(table (current_timestamp rhob) x =
|
|
table (current_timestamp (rhob at Init)) x &&
|
|
unassigned (current_timestamp rhob) x)))
|
|
&& (rho0' x = Var_fo_term x -> rhoi' x = Var_fo_term x)
|
|
&& (rho0' x = Var_fo_term x ->
|
|
unassigned (current_timestamp rhob) x)
|
|
} ;(*
|
|
assert { forall y:int,yt:int.
|
|
is_fo_term_free_var_in_fo_term yt tm /\
|
|
is_fo_term_free_var_in_fo_term y (rhoi' yt) ->
|
|
(yt <> z -> rhoi' yt = rhoi yt
|
|
&& is_fo_term_free_var_in_fo_term y (st tm rhoi) && y >= 0) /\
|
|
(yt = z -> rhoi' yt = stm && y >= 0) && y >= 0
|
|
} ;*)
|
|
let rhou = {(*
|
|
unifier_base = rho'' ;*)
|
|
unifier_base_model = rho0' ;
|
|
(*iteration = n1 ;*)
|
|
unifier = rhoi' } in
|
|
let res = { final_unifier = rhou ;
|
|
unifier_factor = uf (*;
|
|
unassigned_set = remove z s*) } in
|
|
res
|
|
|
|
(*
|
|
meta "remove_logic" predicate ugly_hack
|
|
*)
|
|
|
|
(* Forced because of the model fields. *)
|
|
val ghost unassigned_vars (rhob:subst) : int -> bool
|
|
ensures { forall x:int.
|
|
result x <-> unassigned (current_timestamp rhob) x }
|
|
|
|
let rec unification_term (t1 t2:nlimpl_fo_term) (lv:ref (list int))
|
|
(rhob:subst) (ghost rho:unifier_subst) (ghost lp:int -> bool)
|
|
(*(ghost fv s:S.set int) (ghost it1 it2:int)*) : unification_return
|
|
|
|
(* Invariant requirements. *)
|
|
requires { nlimpl_fo_term_ok t1 }
|
|
requires { nlimpl_fo_term_ok t2 }
|
|
requires { unifier_subst_ok rhob rho }
|
|
requires { forall y:int. is_fo_term_free_var_in_fo_term y
|
|
t1.model_fo_term_field -> y >= 0 }
|
|
requires { forall y:int. is_fo_term_free_var_in_fo_term y
|
|
t2.model_fo_term_field -> y >= 0 }
|
|
|
|
(* Variant requirements. *)
|
|
(*requires { forall x:int.
|
|
is_fo_term_free_var_in_fo_term x t1.model_fo_term_field -> mem x fv }
|
|
requires { forall x:int.
|
|
is_fo_term_free_var_in_fo_term x t2.model_fo_term_field -> mem x fv }
|
|
requires { forall x y:int.
|
|
mem x fv /\
|
|
is_fo_term_free_var_in_fo_term y (eval rho.unifier_base_model x)
|
|
-> mem y fv }
|
|
requires { forall x:int.
|
|
mem x fv /\ AS.model rho.unifier_base x = None -> mem x s }
|
|
requires { forall sp:int -> (fo_term int int).
|
|
let tm = t1.model_fo_term_field in
|
|
power_rel rho.unifier_base_model it1 sp ->
|
|
st tm sp = st tm rho.unifier }
|
|
requires { it1 >= 0 }
|
|
requires { forall sp:int -> (fo_term int int).
|
|
let tm = t2.model_fo_term_field in
|
|
power_rel rho.unifier_base_model it2 sp ->
|
|
st tm sp = st tm rho.unifier }
|
|
requires { it2 >= 0 }*)
|
|
|
|
(* Invariant ensures. *)
|
|
ensures { unifier_subst_ok rhob result.final_unifier }
|
|
ensures { precede (old rhob) rhob }
|
|
|
|
requires { forall x:int. mem x !lv ->
|
|
lp x /\ x >= 0 }
|
|
requires { forall x:int. unassigned (current_timestamp rhob) x -> lp x }
|
|
ensures { forall x:int. mem x !lv ->
|
|
lp x /\ x >= 0 }
|
|
ensures { forall x:int. unassigned (current_timestamp rhob) x -> lp x }
|
|
|
|
(* Unifier properties. *)
|
|
(* The final unifier is obtained by composition with
|
|
the first one and some given factor. *)
|
|
ensures { sc rho.unifier result.unifier_factor =
|
|
result.final_unifier.unifier }
|
|
(* Any possible unifier obtained in such a way can be
|
|
factorised with the final unifier as factor. In fact,
|
|
the factorisation is trivial, so we can avoid existentials. *)
|
|
ensures { forall s:int -> (fo_term int int).
|
|
let s' = sc rho.unifier s in
|
|
st t1.model_fo_term_field s' = st t2.model_fo_term_field s' ->
|
|
s' = sc result.final_unifier.unifier s }
|
|
(* It is of course an unifier. *)
|
|
ensures { let s0 = result.final_unifier.unifier in
|
|
st t1.model_fo_term_field s0 = st t2.model_fo_term_field s0 }
|
|
ensures { let s0 = result.final_unifier.unifier in
|
|
let s1 = rho.unifier_base_model in
|
|
sc s0 s1 = s0 = sc s1 s0 }
|
|
ensures { let s0 = result.final_unifier.unifier in
|
|
let s1 = rho.unifier in
|
|
sc s0 s1 = s0 = sc s1 s0 }
|
|
|
|
(* Variant postconditions. *)
|
|
(*ensures { result.unassigned_set = s ->
|
|
rho.unifier = result.final_unifier.unifier /\
|
|
rho.unifier_base_model = result.final_unifier.unifier_base_model }
|
|
ensures { result.unassigned_set <> s ->
|
|
cardinal result.unassigned_set < cardinal s }
|
|
ensures { forall x:int.
|
|
mem x fv /\ AS.model result.final_unifier.unifier_base x = None ->
|
|
mem x result.unassigned_set }
|
|
ensures { forall x y:int.
|
|
mem x fv /\
|
|
is_fo_term_free_var_in_fo_term y (
|
|
eval result.final_unifier.unifier_base_model x)
|
|
-> mem y fv }*)
|
|
raises { UnificationFailure -> precede (old rhob) rhob /\ correct rhob
|
|
(*-> forall s:int -> (fo_term int int).
|
|
let s' = sc rho.unifier s in
|
|
st t1.model_fo_term_field s' <> st t2.model_fo_term_field s'*) }
|
|
diverges (* variant { 0 } *)
|
|
(*variant { S.cardinal s , it1 + it2 ,
|
|
size_fo_term t1.model_fo_term_field +
|
|
size_fo_term t2.model_fo_term_field }*)
|
|
=
|
|
let t1m = t1.model_fo_term_field in
|
|
let t2m = t2.model_fo_term_field in
|
|
match destruct_fo_term t1 , destruct_fo_term t2 with
|
|
| NLCVar_fo_term x , NLCVar_fo_term y ->
|
|
assert { t1m = Var_fo_term x } ;
|
|
assert { t2m = Var_fo_term y } ;
|
|
if x = y
|
|
then { final_unifier = rho ;
|
|
unifier_factor = subst_id_fo_term (*;
|
|
unassigned_set = s*) }
|
|
else let bx = BA.get rhob x in
|
|
match bx with
|
|
| Cons (Assign bx) _ -> (*checkit rho x it1 ;*)
|
|
let bxm = bx.model_fo_term_field in
|
|
let rhobm = rho.unifier_base_model in
|
|
let rhoi = rho.unifier in
|
|
assert { bxm = rhobm x (*/\ mem x fv*) } ;
|
|
assert { st bxm rhoi = sc rhobm rhoi x = rhoi x = st t1m rhoi
|
|
&& forall s:int -> (fo_term int int).
|
|
st bxm (sc rhoi s) = st t1m (sc rhoi s) } ;
|
|
let res = unification_term bx t2 lv rhob rho lp (*
|
|
fv s (it1-1) it2*) in
|
|
let rhoi' = res.final_unifier.unifier in
|
|
assert { st bxm rhoi' = sc rhobm rhoi' x
|
|
= rhoi' x = st t1m rhoi' && st bxm rhoi' = st t1m rhoi' } ;
|
|
res
|
|
| _ -> let by' = BA.get rhob y in
|
|
match by' with
|
|
| Cons (Assign by') _ -> (*checkit rho y it2 ;*)
|
|
let bym = by'.model_fo_term_field in
|
|
let rhobm = rho.unifier_base_model in
|
|
let rhoi = rho.unifier in
|
|
assert { sdata_inv (Assign by') } ;
|
|
assert { bym = rhobm y (*/\ mem y fv*) } ;
|
|
assert { st bym rhoi = sc rhobm rhoi y = rhoi y = st t2m rhoi
|
|
&& forall s:int -> (fo_term int int).
|
|
st bym (sc rhoi s) = st t2m (sc rhoi s) } ;
|
|
let res = unification_term t1 by' lv rhob rho lp (*fv s it1 (it2-1)*) in
|
|
let rhoi' = res.final_unifier.unifier in
|
|
assert { st bym rhoi' = sc rhobm rhoi' y
|
|
= rhoi' y = st t2m rhoi' && st bym rhoi' = st t2m rhoi' } ;
|
|
res
|
|
| _ -> bottomvar rhob rho y ;
|
|
bottomvar rhob rho x ;
|
|
if x < y
|
|
then assign x t2 lv rhob rho lp (*fv s*)
|
|
else assign y t1 lv rhob rho lp
|
|
end
|
|
end
|
|
| NLC_App f1 l1 , NLC_App f2 l2 ->
|
|
let l1m = l1.model_fo_term_list_field in
|
|
let l2m = l2.model_fo_term_list_field in
|
|
let f1m = f1.model_symbol_field in
|
|
let f2m = f2.model_symbol_field in
|
|
assert { t1m = App f1m l1m } ;
|
|
assert { t2m = App f2m l2m } ;
|
|
match destruct_symbol f1 , destruct_symbol f2 with
|
|
| NLCVar_symbol f1 , NLCVar_symbol f2 -> if f1 = f2
|
|
then (
|
|
assert { forall l1 l2:fo_term_list int int,
|
|
s1 s2:int -> (fo_term int int).
|
|
st (App f1m l1) s1 = st (App f2m l2) s2 <->
|
|
stl l1 s1 = stl l2 s2 } ;
|
|
unification_term_list l1 l2 lv rhob rho lp (*fv s it1 it2*)
|
|
)
|
|
else raise UnificationFailure
|
|
end
|
|
| NLCVar_fo_term x , NLC_App f l ->
|
|
let fm = f.model_symbol_field in
|
|
let lm = l.model_fo_term_list_field in
|
|
assert { t1m = Var_fo_term x } ;
|
|
assert { t2m = App fm lm } ;
|
|
let bx = BA.get rhob x in
|
|
match bx with
|
|
| Cons (Assign bx) _ ->
|
|
(*checkit rho x it1 ;*)
|
|
let bxm = bx.model_fo_term_field in
|
|
let rhobm = rho.unifier_base_model in
|
|
let rhoi = rho.unifier in
|
|
assert { bxm = rhobm x } ;
|
|
assert { st bxm rhoi = sc rhobm rhoi x = rhoi x = st t1m rhoi
|
|
&& forall s:int -> (fo_term int int).
|
|
st bxm (sc rhoi s) = st t1m (sc rhoi s) } ;
|
|
let res = unification_term bx t2 lv rhob rho lp (*
|
|
fv s (it1-1) it2*) in
|
|
let rhoi' = res.final_unifier.unifier in
|
|
assert { st bxm rhoi' = sc rhobm rhoi' x
|
|
= rhoi' x = st t1m rhoi' && st bxm rhoi' = st t1m rhoi' } ;
|
|
res
|
|
| _ -> assign x t2 lv rhob rho lp (*fv s*)
|
|
end
|
|
| NLC_App f l , NLCVar_fo_term x ->
|
|
let fm = f.model_symbol_field in
|
|
let lm = l.model_fo_term_list_field in
|
|
assert { t2m = Var_fo_term x } ;
|
|
assert { t1m = App fm lm } ;
|
|
let bx = BA.get rhob x in
|
|
match bx with
|
|
| Cons (Assign bx) _ -> (*checkit rho x it2 ;*)
|
|
let bxm = bx.model_fo_term_field in
|
|
let rhobm = rho.unifier_base_model in
|
|
let rhoi = rho.unifier in
|
|
assert { bxm = rhobm x } ;
|
|
assert { st bxm rhoi = sc rhobm rhoi x = rhoi x = st t2m rhoi
|
|
&& forall s:int -> (fo_term int int).
|
|
st bxm (sc rhoi s) = st t2m (sc rhoi s) } ;
|
|
let res = unification_term t1 bx lv rhob rho lp
|
|
(*fv s it1 (it2-1)*) in
|
|
let rhoi' = res.final_unifier.unifier in
|
|
assert { st bxm rhoi' = sc rhobm rhoi' x
|
|
= rhoi' x = st t2m rhoi' && st bxm rhoi' = st t2m rhoi' } ;
|
|
res
|
|
| _ -> assign x t1 lv rhob rho lp (*fv s*)
|
|
end
|
|
end
|
|
|
|
with unification_term_list (t1 t2:nlimpl_fo_term_list) (lv:ref (list int))
|
|
(rhob:subst) (ghost rho:unifier_subst) (ghost lp:int -> bool)
|
|
(*(ghost fv s:S.set int) (ghost it1 it2:int)*) :
|
|
unification_return
|
|
(* Invariant requirements. *)
|
|
requires { nlimpl_fo_term_list_ok t1 }
|
|
requires { nlimpl_fo_term_list_ok t2 }
|
|
requires { unifier_subst_ok rhob rho }
|
|
requires { forall y:int. is_fo_term_free_var_in_fo_term_list y
|
|
t1.model_fo_term_list_field -> y >= 0 }
|
|
requires { forall y:int. is_fo_term_free_var_in_fo_term_list y
|
|
t2.model_fo_term_list_field -> y >= 0 }
|
|
|
|
(* Variant requirements. *)
|
|
(*requires { forall x:int.
|
|
is_fo_term_free_var_in_fo_term_list x t1.model_fo_term_list_field ->
|
|
mem x fv }
|
|
requires { forall x:int.
|
|
is_fo_term_free_var_in_fo_term_list x t2.model_fo_term_list_field ->
|
|
mem x fv }
|
|
requires { forall x y:int.
|
|
mem x fv /\
|
|
is_fo_term_free_var_in_fo_term y (eval rho.unifier_base_model x) ->
|
|
mem y fv }
|
|
requires { forall x:int.
|
|
mem x fv /\ AS.model rho.unifier_base x = None -> mem x s }
|
|
requires { forall sp:int -> (fo_term int int).
|
|
let tm = t1.model_fo_term_list_field in
|
|
power_rel rho.unifier_base_model it1 sp ->
|
|
stl tm sp = stl tm rho.unifier }
|
|
requires { it1 >= 0 }
|
|
requires { forall sp:int -> (fo_term int int).
|
|
let tm = t2.model_fo_term_list_field in
|
|
power_rel rho.unifier_base_model it2 sp ->
|
|
stl tm sp = stl tm rho.unifier }
|
|
requires { it2 >= 0 }*)
|
|
|
|
(* Invariant ensures. *)
|
|
ensures { unifier_subst_ok rhob result.final_unifier }
|
|
ensures { precede (old rhob) rhob }
|
|
|
|
requires { forall x:int. mem x !lv ->
|
|
lp x /\ x >= 0 }
|
|
requires { forall x:int. unassigned (current_timestamp rhob) x -> lp x }
|
|
ensures { forall x:int. mem x !lv ->
|
|
lp x /\ x >= 0 }
|
|
ensures { forall x:int. unassigned (current_timestamp rhob) x -> lp x }
|
|
|
|
(* Unifier properties. *)
|
|
ensures { sc rho.unifier result.unifier_factor =
|
|
result.final_unifier.unifier }
|
|
ensures { forall s:int -> (fo_term int int).
|
|
let s' = sc rho.unifier s in
|
|
stl t1.model_fo_term_list_field s' = stl t2.model_fo_term_list_field s' ->
|
|
s' = sc result.final_unifier.unifier s }
|
|
ensures { let s0 = result.final_unifier.unifier in
|
|
stl t1.model_fo_term_list_field s0 =
|
|
stl t2.model_fo_term_list_field s0 }
|
|
ensures { let s0 = result.final_unifier.unifier in
|
|
let s1 = rho.unifier_base_model in
|
|
sc s0 s1 = s0 = sc s1 s0 }
|
|
ensures { let s0 = result.final_unifier.unifier in
|
|
let s1 = rho.unifier in
|
|
sc s0 s1 = s0 = sc s1 s0 }
|
|
|
|
(* Variant postconditions. *)
|
|
(*ensures { result.unassigned_set = s ->
|
|
rho.unifier = result.final_unifier.unifier /\
|
|
rho.unifier_base_model = result.final_unifier.unifier_base_model }
|
|
ensures { result.unassigned_set <> s ->
|
|
cardinal result.unassigned_set < cardinal s }
|
|
ensures { forall x:int.
|
|
mem x fv /\ AS.model result.final_unifier.unifier_base x = None ->
|
|
mem x result.unassigned_set }
|
|
ensures { forall x y:int.
|
|
mem x fv /\
|
|
is_fo_term_free_var_in_fo_term y (
|
|
eval result.final_unifier.unifier_base_model x)
|
|
-> mem y fv }*)
|
|
raises { UnificationFailure -> precede (old rhob) rhob /\ correct rhob
|
|
(*-> forall s:int -> (fo_term int int).
|
|
let s' = sc rho.unifier s in
|
|
stl t1.model_fo_term_list_field s' <>
|
|
stl t2.model_fo_term_list_field s'*) }
|
|
diverges (* variant { 0 } *)
|
|
(*variant { S.cardinal s , it1 + it2 ,
|
|
size_fo_term_list t1.model_fo_term_list_field +
|
|
size_fo_term_list t2.model_fo_term_list_field }*)
|
|
=
|
|
let t1m = t1.model_fo_term_list_field in
|
|
let t2m = t2.model_fo_term_list_field in
|
|
match destruct_fo_term_list t1 , destruct_fo_term_list t2 with
|
|
| NLC_FONil , NLC_FONil -> { final_unifier = rho ;
|
|
unifier_factor = subst_id_fo_term (*;
|
|
unassigned_set = s*) }
|
|
| NLC_FOCons u1 q1 , NLC_FOCons u2 q2 ->
|
|
let u1m = u1.model_fo_term_field in
|
|
let u2m = u2.model_fo_term_field in
|
|
let q1m = q1.model_fo_term_list_field in
|
|
let q2m = q2.model_fo_term_list_field in
|
|
assert { t1m = FOCons u1m q1m /\ t2m = FOCons u2m q2m } ;
|
|
assert { forall a c:fo_term int int,b d:fo_term_list int int,
|
|
s1 s2:int -> (fo_term int int).
|
|
stl (FOCons a b) s1 = stl (FOCons c d) s2 <->
|
|
st a s1 = st c s2 /\ stl b s1 = stl d s2 } ;
|
|
let rho0 = rho.unifier in
|
|
let rho2 = unification_term_list q1 q2 lv rhob rho lp (*fv s it1 it2*) in
|
|
let rho2f = rho2.final_unifier in
|
|
let rho20 = rho2f.unifier in
|
|
assert { forall s:int -> (fo_term int int).
|
|
stl t1m (sc rho0 s) = stl t2m (sc rho0 s) ->
|
|
stl q1m (sc rho0 s) = stl q2m (sc rho0 s) &&
|
|
sc rho0 s = sc rho20 s &&
|
|
st u1m (sc rho20 s) = st u2m (sc rho20 s) } ;
|
|
(*let u = rho2f.iteration in*)
|
|
(*let ghost aux_ (u_:unit) : (int,int)
|
|
returns { (it'1,it'2) ->
|
|
(rho2.unassigned_set = s -> it1=it'1 /\ it2 = it'2) /\
|
|
(forall sp:int -> (fo_term int int).
|
|
power_rel rho2f.unifier_base_model it'1 sp ->
|
|
stl t1m sp = stl t1m rho20) /\
|
|
(forall sp:int -> (fo_term int int).
|
|
power_rel rho2f.unifier_base_model it'2 sp ->
|
|
stl t2m sp = stl t2m rho20) /\
|
|
it'1 >= 0 /\
|
|
it'2 >= 0 }
|
|
= if rho2.unassigned_set = s
|
|
then (it1,it2)
|
|
else ( assert { forall sp:int -> (fo_term int int).
|
|
power_rel rho2f.unifier_base_model u sp ->
|
|
sp = rho2f.unifier } ; (u,u) ) in
|
|
let (it1,it2) = aux_ () in*)
|
|
let rho3 = unification_term u1 u2 lv rhob rho2f lp
|
|
(*fv rho2.unassigned_set it1 it2*) in
|
|
let rho30 = rho3.final_unifier.unifier in
|
|
assert { forall s:int -> (fo_term int int).
|
|
stl t1m (sc rho0 s) = stl t2m (sc rho0 s) ->
|
|
sc rho0 s = sc rho20 s &&
|
|
st u1m (sc rho20 s) = st u2m (sc rho20 s) &&
|
|
sc rho30 s = sc rho0 s } ;
|
|
let rhof3 = rho3.unifier_factor in
|
|
assert { stl q1m rho30 = stl (stl q1m rho20) rhof3
|
|
= stl (stl q2m rho20) rhof3 = stl q2m rho30 } ;
|
|
{ final_unifier = rho3.final_unifier ;
|
|
unifier_factor = ghost sc rho2.unifier_factor rho3.unifier_factor (*;
|
|
unassigned_set = rho3.unassigned_set*) }
|
|
| NLC_FONil , NLC_FOCons u q ->
|
|
(*assert { forall s:int -> (fo_term int int).
|
|
subst_fo_term_list t1m subst_id_symbol s = FONil /\
|
|
let um = u.model_fo_term_field in
|
|
let qm = q.model_fo_term_list_field in
|
|
stl t2m s = FOCons (st um s) (stl qm s) } ;*)
|
|
raise UnificationFailure
|
|
| NLC_FOCons u q , NLC_FONil ->
|
|
(*assert { forall s:int -> (fo_term int int).
|
|
subst_fo_term_list t2m subst_id_symbol s = FONil /\
|
|
let um = u.model_fo_term_field in
|
|
let qm = q.model_fo_term_list_field in
|
|
stl t1m s = FOCons (st um s) (stl qm s) } ;*)
|
|
raise UnificationFailure
|
|
end
|
|
|
|
let conflict (t1 t2:nlimpl_fo_term_list) (rhob:subst) (ghost rho:unifier_subst) : unit
|
|
requires { sdata_inv (PConflict t1 t2) }
|
|
requires { unifier_subst_ok rhob rho }
|
|
diverges
|
|
ensures { unifier_subst_ok rhob rho }
|
|
(* Useless : trivial consequence of unifier_subst_ok rhob rho.
|
|
ensures { smodel (current_timestamp rhob) =
|
|
smodel (current_timestamp (old rhob)) }*)
|
|
ensures { precede (old rhob) rhob }
|
|
(*raises { UnificationFailure -> unifier_subst_ok rhob rho }*)
|
|
(*raises { UnificationFailure -> (current_timestamp rhob).table =
|
|
(current_timestamp (old rhob).table }*)
|
|
raises { UnificationFailure -> precede (old rhob) rhob /\ correct rhob }
|
|
=
|
|
label Init in
|
|
let l = ref Nil in
|
|
let t = stamp rhob in
|
|
let lp = unassigned_vars rhob in
|
|
let u = try Some (unification_term_list t1 t2 l rhob rho lp)
|
|
with UnificationFailure -> None end in
|
|
label Mid0 in
|
|
match u with
|
|
| Some _ -> match !l with
|
|
| Nil -> raise UnificationFailure
|
|
| Cons v _ -> backtrack t rhob ;
|
|
assert { backtrack_to (rhob at Init) (rhob at Mid0) rhob } ;
|
|
label Middle in
|
|
add v (PConflict t1 t2) rhob ;
|
|
assert { (forall t:timesubst,x:int. unassigned t x ->
|
|
let u = smodel t x in match table t x with
|
|
| Nil -> u = Var_fo_term x
|
|
| Cons (PConflict _ _) _ -> u = Var_fo_term x
|
|
| _ -> false end &&
|
|
u = Var_fo_term x) &&
|
|
(forall x:int.
|
|
x <> v -> smodel (current_timestamp rhob) x =
|
|
smodel (current_timestamp (rhob at Middle)) x) &&
|
|
lp v &&
|
|
unassigned (current_timestamp (rhob at Middle)) v &&
|
|
unassigned (current_timestamp rhob) v &&
|
|
(let u = current_timestamp rhob in
|
|
let u' = current_timestamp (rhob at Middle) in
|
|
let ut = u.time in
|
|
let utb = u.table in
|
|
let us = u.size in
|
|
u = { time = u.time ; table = u.table ; size = u.size } /\
|
|
u' = { time = u'.time ; table = u'.table ; size = u'.size }) &&
|
|
smodel (current_timestamp rhob) v = Var_fo_term v =
|
|
smodel (current_timestamp (rhob at Middle)) v &&
|
|
extensionalEqual (smodel (current_timestamp rhob))
|
|
(smodel (current_timestamp (rhob at Middle))) &&
|
|
smodel (current_timestamp rhob) = smodel (current_timestamp (rhob at Middle)) } ;
|
|
assert { (forall x:int.
|
|
x <> v -> unassigned (current_timestamp (rhob at Middle)) x ->
|
|
unassigned (current_timestamp rhob) x) &&
|
|
(forall x:int.
|
|
unifier_base_model rho x = Var_fo_term x ->
|
|
unassigned (current_timestamp (rhob at Middle)) x &&
|
|
unassigned (current_timestamp rhob) x) }
|
|
end
|
|
| None -> backtrack t rhob ;
|
|
assert { backtrack_to (rhob at Init) (rhob at Mid0) rhob }
|
|
end
|
|
|
|
let rec conflicts (lv:list sdata) (rhob:subst) (ghost rho:unifier_subst) : unit
|
|
requires { list_forall sdata_inv lv }
|
|
requires { unifier_subst_ok rhob rho }
|
|
ensures { unifier_subst_ok rhob rho }
|
|
(*ensures { smodel (current_timestamp rhob) = smodel (current_timestamp (old rhob)) }*)
|
|
ensures { precede (old rhob) rhob }
|
|
diverges (* variant { lv } *)
|
|
raises { UnificationFailure -> correct rhob /\ precede (old rhob) rhob }
|
|
=
|
|
match lv with
|
|
| Nil -> ()
|
|
| Cons (Assign _) q -> conflicts q rhob rho
|
|
| Cons (PConflict t1 t2) q -> conflict t1 t2 rhob rho ; conflicts q rhob rho
|
|
end
|
|
|
|
let rec unif_conflicts (lv:list int) (rhob:subst) (ghost rho:unifier_subst) : unit
|
|
requires { forall x:int. mem x lv -> x >= 0 }
|
|
requires { unifier_subst_ok rhob rho }
|
|
ensures { unifier_subst_ok rhob rho }
|
|
ensures { precede (old rhob) rhob }
|
|
diverges (* variant { lv } *)
|
|
raises { UnificationFailure -> correct rhob /\ precede (old rhob) rhob }
|
|
=
|
|
match lv with
|
|
| Nil -> ()
|
|
| Cons v0 q -> conflicts (get rhob v0) rhob rho ; unif_conflicts q rhob rho
|
|
end
|
|
|
|
let unify_term_list (t1 t2:nlimpl_fo_term_list) (watch:ref (list int))
|
|
(rhob:subst) (ghost rho:unifier_subst) :
|
|
unification_return
|
|
requires { !watch = Nil }
|
|
requires { nlimpl_fo_term_list_ok t1 }
|
|
requires { forall x:int. is_fo_term_free_var_in_fo_term_list x
|
|
t1.model_fo_term_list_field -> x >= 0 }
|
|
requires { nlimpl_fo_term_list_ok t2 }
|
|
requires { forall x:int. is_fo_term_free_var_in_fo_term_list x
|
|
t2.model_fo_term_list_field -> x >= 0 }
|
|
requires { unifier_subst_ok rhob rho }
|
|
diverges
|
|
ensures { unifier_subst_ok rhob result.final_unifier }
|
|
ensures { result.final_unifier.unifier = sc rho.unifier result.unifier_factor }
|
|
ensures { precede (old rhob) rhob }
|
|
ensures { forall s:int -> (fo_term int int).
|
|
let s' = sc rho.unifier s in
|
|
stl t1.model_fo_term_list_field s' = stl t2.model_fo_term_list_field s' ->
|
|
s' = sc result.final_unifier.unifier s }
|
|
ensures { let s0 = result.final_unifier.unifier in
|
|
stl t1.model_fo_term_list_field s0 =
|
|
stl t2.model_fo_term_list_field s0 }
|
|
raises { UnificationFailure -> correct rhob /\ precede (old rhob) rhob }
|
|
=
|
|
let lp = unassigned_vars rhob in
|
|
let u = unification_term_list t1 t2 watch rhob rho lp in
|
|
unif_conflicts !watch rhob u.final_unifier ;
|
|
u
|
|
|
|
(*let rec conflicts (lv:list sdata) (rhob:subst) (ghost rho:unifier_subst) : unit
|
|
requires { list_forall sdata_inv lv }
|
|
requires { unifier_subst_ok rhob rho }
|
|
ensures { unifier_subst_ok rhob rho }
|
|
raises { UnificationFailure -> }*)
|
|
|
|
(*
|
|
let rec ghost term_free_var_set (t:fo_term int int) (it:int)
|
|
(rho:unifier_subst) : set int
|
|
requires { unifier_subst_ok rho }
|
|
requires { it >= 0 }
|
|
requires { forall sp:int -> (fo_term int int).
|
|
power_rel rho.unifier_base_model it sp ->
|
|
st t sp = st t rho.unifier }
|
|
ensures { forall x:int. is_fo_term_free_var_in_fo_term x t ->
|
|
mem x result }
|
|
ensures { forall x y:int.
|
|
is_fo_term_free_var_in_fo_term x (eval rho.unifier_base_model y) /\
|
|
mem y result -> mem x result }
|
|
variant { it , size_fo_term t }
|
|
=
|
|
match t with
|
|
| Var_fo_term x -> let rho0 = rho.unifier_base_model in
|
|
let rhoi = rho.unifier in
|
|
if it = 0
|
|
then (assert { t = st t subst_id_fo_term = st t rhoi &&
|
|
t = st t (sc rhoi rho0) = st t rho0 && rho0 x = t } ;
|
|
assert { forall y:int. is_fo_term_free_var_in_fo_term y (rho0 x) ->
|
|
y = x } ;
|
|
add x empty)
|
|
else
|
|
let t2 = eval rho0 x in
|
|
(assert { forall sp:int -> (fo_term int int).
|
|
power_rel rho0 (it-1) sp ->
|
|
power_rel rho0 it (sc rho0 sp) &&
|
|
st t2 sp = st t (sc rho0 sp) = st t rhoi =
|
|
st t (sc rho0 rhoi) = st t2 rhoi && st t2 sp = st t2 rhoi } ;
|
|
add x (term_free_var_set t2 (it-1) rho))
|
|
| App _ l -> assert { forall s s2:int -> (fo_term int int).
|
|
st t s = st t s2 <-> stl l s = stl l s2 } ;
|
|
term_list_free_var_set l it rho
|
|
end
|
|
|
|
with ghost term_list_free_var_set (t:fo_term_list int int) (it:int)
|
|
(rho:unifier_subst) : set int
|
|
requires { unifier_subst_ok rho }
|
|
requires { it >= 0 }
|
|
requires { forall sp:int -> (fo_term int int).
|
|
power_rel rho.unifier_base_model it sp ->
|
|
stl t sp = stl t rho.unifier }
|
|
ensures { forall x:int. is_fo_term_free_var_in_fo_term_list x t ->
|
|
mem x result }
|
|
ensures { forall x y:int.
|
|
is_fo_term_free_var_in_fo_term x (eval rho.unifier_base_model y) /\
|
|
mem y result -> mem x result }
|
|
variant { it , size_fo_term_list t }
|
|
=
|
|
match t with
|
|
| FONil -> empty
|
|
| FOCons x q -> assert { forall s s2:int -> (fo_term int int).
|
|
stl t s = stl t s2 <->
|
|
st x s = st x s2 /\ stl q s = stl q s2 } ;
|
|
union (term_free_var_set x it rho)
|
|
(term_list_free_var_set q it rho)
|
|
end
|
|
|
|
(* Two main
|
|
functions, far more preferable for the user than
|
|
the incredibly ugly functions before !
|
|
Unification functions which are :
|
|
1) sound (if it returns, then it returns an unifier factor+
|
|
if it fails, then there is no unifier factor)
|
|
2) complete/terminating (either case is true) *)
|
|
|
|
let unify_term (t1 t2:nlimpl_fo_term) (rho:unifier_subst) : unify_return
|
|
requires { nlimpl_fo_term_ok t1 }
|
|
requires { nlimpl_fo_term_ok t2 }
|
|
requires { unifier_subst_ok rho }
|
|
(* Factorisation using previous unifier. *)
|
|
ensures { sc rho.unifier result.factor =
|
|
result.usubst.unifier }
|
|
(* All possible unifier factorisable using rho
|
|
can be factorised using the generated one. *)
|
|
ensures { forall s:int -> (fo_term int int).
|
|
let s' = sc rho.unifier s in
|
|
st t1.model_fo_term_field s' = st t2.model_fo_term_field s' ->
|
|
s' = sc result.usubst.unifier s }
|
|
(* this is an unifier. *)
|
|
ensures { let s0 = result.usubst.unifier in
|
|
st t1.model_fo_term_field s0 =
|
|
st t2.model_fo_term_field s0 }
|
|
ensures { unifier_subst_ok result.usubst }
|
|
(* There is no unifier factorisable by rho. *)
|
|
raises { UnificationFailure -> forall s:int -> (fo_term int int).
|
|
let s' = sc rho.unifier s in
|
|
st t1.model_fo_term_field s' <>
|
|
st t2.model_fo_term_field s' }
|
|
=
|
|
let it = rho.iteration in
|
|
let fv = term_free_var_set t1.model_fo_term_field it rho in
|
|
let fv = union fv (term_free_var_set t2.model_fo_term_field it rho) in
|
|
let res = unification_term t1 t2 rho fv fv it it in
|
|
{ usubst = res.final_unifier ; factor = res.unifier_factor }
|
|
|
|
let unify_term_list (t1 t2:nlimpl_fo_term_list) (rho:unifier_subst) :
|
|
unify_return
|
|
requires { nlimpl_fo_term_list_ok t1 }
|
|
requires { nlimpl_fo_term_list_ok t2 }
|
|
requires { unifier_subst_ok rho }
|
|
ensures { sc rho.unifier result.factor =
|
|
result.usubst.unifier }
|
|
ensures { forall s:int -> (fo_term int int).
|
|
let s' = sc rho.unifier s in
|
|
stl t1.model_fo_term_list_field s' = stl t2.model_fo_term_list_field s' ->
|
|
s' = sc result.usubst.unifier s }
|
|
ensures { let s0 = result.usubst.unifier in
|
|
stl t1.model_fo_term_list_field s0 =
|
|
stl t2.model_fo_term_list_field s0 }
|
|
ensures { unifier_subst_ok result.usubst }
|
|
raises { UnificationFailure -> forall s:int -> (fo_term int int).
|
|
let s' = sc rho.unifier s in
|
|
stl t1.model_fo_term_list_field s' <>
|
|
stl t2.model_fo_term_list_field s' }
|
|
=
|
|
let it = rho.iteration in
|
|
let fv = term_list_free_var_set t1.model_fo_term_list_field it rho in
|
|
let fv = union fv
|
|
(term_list_free_var_set t2.model_fo_term_list_field it rho) in
|
|
let res = unification_term_list t1 t2 rho fv fv it it in
|
|
{ usubst = res.final_unifier ; factor = res.unifier_factor }
|
|
*)
|
|
|
|
end
|