Commit 0773d8c0 authored by Martin Clochard's avatar Martin Clochard

in progress: specification of Why3 term library

parent d01e5acf
......@@ -6,14 +6,33 @@
<file name="../logic_impl.mlw" expanded="true">
<theory name="Ident" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Ty" sum="647747069782e1e4ffb5377c8643e469" expanded="true">
<goal name="WP_parameter tyl_inv" expl="VC for tyl_inv" expanded="true">
<proof prover="0"><result status="valid" time="0.06" steps="159"/></proof>
<theory name="Ty" sum="e6b1a0dadb3900c32ea41aeb7e9bfa0c" expanded="true">
<goal name="WP_parameter sig_world_inv" expl="VC for sig_world_inv" expanded="true">
<proof prover="0"><result status="valid" time="0.08" steps="102"/></proof>
</goal>
<goal name="WP_parameter tyl_inv" expl="VC for tyl_inv">
<proof prover="0"><result status="valid" time="0.19" steps="300"/></proof>
</goal>
</theory>
<theory name="Term" sum="17b5dd1ac03d587acacfe140e3923fef" expanded="true">
<goal name="WP_parameter ts_constr_env_inv" expl="VC for ts_constr_env_inv" expanded="true">
<proof prover="0"><result status="valid" time="0.05" steps="21"/></proof>
<theory name="Term" sum="b19687c0bc7def2d6a9d5eca04977811">
<goal name="WP_parameter vl_ty_len_nth" expl="VC for vl_ty_len_nth">
<transf name="split_goal_wp">
<goal name="WP_parameter vl_ty_len_nth.1" expl="1. variant decrease">
<proof prover="0"><result status="valid" time="0.06" steps="24"/></proof>
</goal>
<goal name="WP_parameter vl_ty_len_nth.2" expl="2. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="15"/></proof>
</goal>
<goal name="WP_parameter vl_ty_len_nth.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.06" steps="128"/></proof>
</goal>
<goal name="WP_parameter vl_ty_len_nth.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="8"/></proof>
</goal>
<goal name="WP_parameter vl_ty_len_nth.5" expl="5. postcondition">
<proof prover="0"><result status="valid" time="0.07" steps="29"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
......
......@@ -19,6 +19,8 @@ module Model
ls_case : lsymbol -> list 'univ -> 'univ -> bool;
(* Projections for invertible symbols (e.g constructors). *)
ls_proj : lsymbol -> list 'univ -> 'univ -> list 'univ;
(* Interpretation of choice operator (epsilon). *)
i_eps : 'univ -> ('univ -> bool) -> 'univ;
(* Builtin sort for proposition, with two members true and false. *)
i_prop : 'univ;
i_true : 'univ;
......@@ -31,8 +33,11 @@ module Model
(* Definition of a valid model. *)
predicate model_ok (m:model 'univ) =
(* Every semantic type is inhabited. *)
(forall ty. exists x. m.ty_doms ty x) /\
(* Choice operator fall in the right type interpretation. In particular,
it implies that every type interpretation is inhabited. *)
(forall ty s. m.ty_doms ty (m.i_eps ty s)) /\
(* Choice operator fall in the input set when possible. *)
(forall ty s x. m.ty_doms ty x /\ s x -> s (m.i_eps ty s)) /\
(* true and false are distinct inhabitant of prop. *)
m.i_true <> m.i_false /\
m.ty_doms m.i_prop m.i_true /\ m.ty_doms m.i_prop m.i_false
......@@ -146,6 +151,7 @@ module Sem
| TLet t1 t2 -> let x = t_sem m tyv tv t1 in
t_sem m tyv (bfold tv (const x)) t2
| TCase t brl -> brl_sem m tyv tv brl (t_sem m tyv tv t)
| TEps ty t -> m.i_eps (ty_sem m tyv ty) (p_sem m tyv tv t)
| TForall fty tq -> if (forall f. wty_assignment m tyv fty f ->
t_sem m tyv (bfold tv f) tq = m.i_true)
then m.i_true
......@@ -175,6 +181,10 @@ module Sem
| TFalse -> m.i_false
end
with p_sem (m:model 'univ) (tyv:ty_valuation 'univ) (tv:valuation 'tv 'univ)
(t:term (bind 'tv unit)) : 'univ -> bool =
\x. t_sem m tyv (bfold tv (const x)) t = m.i_true
with tl_sem (m:model 'univ) (tyv:ty_valuation 'univ) (tv:valuation 'tv 'univ)
(l:list (term 'tv)) : list 'univ =
match l with
......@@ -361,6 +371,14 @@ module SemSubst
t_sem m tyv g0 (t_map (bmap f) identity identity identity t2) =
t_sem m tyv (bfold (compose rho f) cv0) t2 }
| TCase t brl -> rc t;brl_map_sem m tyv f brl
| TEps _ t -> t_map_sem m tyv (bmap f) t;
assert { forall rho.
let tm = t_map (bmap f) identity identity identity t in
(forall x. t_sem m tyv (bfold rho (const x)) tm =
t_sem m tyv (compose (bfold rho (const x)) (bmap f)) t =
t_sem m tyv (bfold (compose rho f) (const x)) t) &&
extensional_equal (p_sem m tyv rho tm)
(p_sem m tyv (compose rho f) t) };
| TForall _ t | TExists _ t -> t_map_sem m tyv (bmap f) t;
assert { forall rho fv. let g0 = bfold rho fv in
t_sem m tyv g0 (t_map (bmap f) identity identity identity t) =
......@@ -438,6 +456,12 @@ module SemSubst
t_sem m (compose (ty_sem m tyv) g)
(bfold (compose (t_sem m tyv rho) f) cv0) t2 }
| TCase t brl -> rc t;brl_subst_sem m tyv f g brl
| TEps _ t -> t_subst_sem m tyv (term_lift f) g t;
let ts = t_subst (term_lift f) g identity identity t in
assert { forall rho.
extensional_equal (p_sem m tyv rho ts)
(p_sem m (compose (ty_sem m tyv) g)
(compose (t_sem m tyv rho) f) t) };
| TForall tyl t | TExists tyl t -> t_subst_sem m tyv (term_lift f) g t;
let ts = t_subst (term_lift f) g identity identity t in
let tyls = tyl_subst g identity tyl in
......@@ -1024,7 +1048,7 @@ module WellTyped
valuation_coherence m tyv env' rho' && false) && false) }
| TCase tc brl -> t_coherent_type m sig tyv tc;
brl_coherent_type m sig tyv brl
| TForall _ _ | TExists _ _
| TEps _ _ | TForall _ _ | TExists _ _
| TAnd _ _ | TOr _ _ | TImplies _ _ | TIff _ _
| TNot _ | TVar _ | TTrue | TFalse -> ()
end
......
......@@ -70,6 +70,8 @@ module Defs
| TLet (term 'tv) (term (bind 'tv unit))
(* Pattern-matching: the first matching case. *)
| TCase (term 'tv) (list (branch 'tv))
(* Hilbert epsilon. *)
| TEps ty (term (bind 'tv unit))
(* Universal/Existential quantifications. The types of the quantified
variables are given by the sequences. *)
| TForall (list ty) (term (bind 'tv int))
......@@ -141,6 +143,7 @@ module Maps
(t_map f g h i e)
| TLet t1 t2 -> TLet (t_map f g h i t1) (t_map (bmap f) g h i t2)
| TCase t lb -> TCase (t_map f g h i t) (brl_map f g h i lb)
| TEps ty t -> TEps (ty_map g h ty) (t_map (bmap f) g h i t)
| TForall tys t ->
TForall (tyl_map g h tys) (t_map (bmap f) g h i t)
| TExists tys t ->
......@@ -237,6 +240,7 @@ module Substs
| TLet t1 t2 ->
TLet (t_subst f g h i t1) (t_subst (term_lift f) g h i t2)
| TCase t lb -> TCase (t_subst f g h i t) (brl_subst f g h i lb)
| TEps ty t -> TEps (ty_subst g h ty) (t_subst (term_lift f) g h i t)
| TForall tys t ->
TForall (tyl_subst g h tys) (t_subst (term_lift f) g h i t)
| TExists tys t ->
......@@ -377,6 +381,8 @@ module VarsIn
t_vars_in (bfold tv_set all) tyv_set tys_set ls_set t2
| TCase t lb -> t_vars_in tv_set tyv_set tys_set ls_set t /\
brl_vars_in tv_set tyv_set tys_set ls_set lb
| TEps ty t -> ty_vars_in tyv_set tys_set ty /\
t_vars_in (bfold tv_set all) tyv_set tys_set ls_set t
| TForall tys t -> t_vars_in (bfold tv_set all) tyv_set tys_set ls_set t /\
tyl_vars_in tyv_set tys_set tys
| TExists tys t -> t_vars_in (bfold tv_set all) tyv_set tys_set ls_set t /\
......@@ -460,13 +466,13 @@ module VarsIn
= let ghost rc = t_vars_in_all in match t with
| TApp _ _ l -> tl_vars_in_all l
| TIf b t e -> rc b; rc t; rc e
| TLet t1 t2 ->
assert { extensional_equal (bfold all all:bind 'tv unit -> bool) all };
rc t1; rc t2
| TLet t1 t2 -> rc t1;rc t2;
assert { extensional_equal (bfold all all:bind 'tv unit -> bool) all }
| TCase t lb -> rc t; brl_vars_in_all lb
| TForall _ t | TExists _ t ->
assert { extensional_equal (bfold all all:bind 'tv int -> bool) all };
rc t
| TEps _ t -> rc t;
assert { extensional_equal (bfold all all:bind 'tv unit -> bool) all }
| TForall _ t | TExists _ t -> rc t;
assert { extensional_equal (bfold all all:bind 'tv int -> bool) all }
| TAnd t1 t2 | TOr t1 t2 | TImplies t1 t2 | TIff t1 t2 -> rc t1; rc t2
| TNot t -> rc t
| _ -> ()
......@@ -568,6 +574,8 @@ module VarsIn
t_vars_subset (bfold tv1 all) (bfold tv2 all)
tyv1 tyv2 tys1 tys2 ls1 ls2 t2
| TCase t lb -> rc t; bl_vars_subset tv1 tv2 tyv1 tyv2 tys1 tys2 ls1 ls2 lb
| TEps _ t -> t_vars_subset (bfold tv1 all) (bfold tv2 all)
tyv1 tyv2 tys1 tys2 ls1 ls2 t
| TForall _ t | TExists _ t ->
t_vars_subset (bfold tv1 all) (bfold tv2 all)
tyv1 tyv2 tys1 tys2 ls1 ls2 t
......@@ -790,6 +798,11 @@ module SubstVarsIn
&& false };
t_map_vars_in bf (bmap f) (bfold qf all) pg g qg ph h qh pi i qi t2
| TCase t lb -> rc t; brl_map_vars_in pf f qf pg g qg ph h qh pi i qi lb
| TEps _ t -> let bf = bfold pf all in
assert { forall x. bf x -> not (bfold qf all (bmap f x)) ->
match x with Fresh u -> bmap f x = Fresh u && false | _ -> false end
&& false };
t_map_vars_in bf (bmap f) (bfold qf all) pg g qg ph h qh pi i qi t
| TForall _ t | TExists _ t -> let bf = bfold pf all in
assert { forall x. bf x -> not (bfold qf all (bmap f x)) ->
match x with Fresh u -> bmap f x = Fresh u && false | _ -> false end
......@@ -953,6 +966,13 @@ module SubstVarsIn
&& false end && false };
t_subst_vars_in bf (term_lift f) (bfold qf all) pg g qg ph h qh pi i qi t2
| TCase t lb -> rc t; brl_subst_vars_in pf f qf pg g qg ph h qh pi i qi lb
| TEps _ t -> let bf = bfold pf all in
assert { forall x. bf x ->
not (t_vars_in (bfold qf all) qg qh qi (term_lift f x)) ->
match x with Fresh u -> term_lift f x = TVar (Fresh u) && false
| Old u -> term_lift f x = t_map Old identity identity identity (f u)
&& false end && false };
t_subst_vars_in bf (term_lift f) (bfold qf all) pg g qg ph h qh pi i qi t
| TForall _ t | TExists _ t -> let bf = bfold pf all in
assert { forall x. bf x ->
not (t_vars_in (bfold qf all) qg qh qi (term_lift f x)) ->
......@@ -1120,6 +1140,17 @@ module SubstVarsIn
t_subst_free_vars bf tf1 tf2 sg g1 g2 sh h1 h2 si i1 i2 t2
| TCase t lb -> rc t;
brl_subst_free_vars sf f1 f2 sg g1 g2 sh h1 h2 si i1 i2 lb
| TEps _ t ->
let bf = bfold sf all in
let tf1 = term_lift f1 in
let tf2 = term_lift f2 in
assert { forall x. bf x -> tf1 x <> tf2 x ->
match x with
| Old u -> tf1 x = t_map Old identity identity identity (f1 u) =
t_map Old identity identity identity (f2 u) = tf2 x && false
| _ -> false
end && false };
t_subst_free_vars bf tf1 tf2 sg g1 g2 sh h1 h2 si i1 i2 t
| TForall _ t | TExists _ t ->
let bf = bfold sf all in
let tf1 = term_lift f1 in
......@@ -1264,6 +1295,7 @@ module Commutations
| TIf b t e -> rc b; rc t; rc e
| TLet t1 t2 -> rc t1; rc t2
| TCase t lb -> rc t; brl_map_id lb
| TEps _ t -> rc t
| TForall _ t | TExists _ t -> rc t
| TAnd t1 t2 | TOr t1 t2 | TImplies t1 t2 | TIff t1 t2 -> rc t1; rc t2
| TNot t -> rc t
......@@ -1384,6 +1416,7 @@ module Commutations
| TLet t1 t2 -> rc t1;
t_map_compose (bmap f1) (bmap f2) g1 g2 h1 h2 i1 i2 t2
| TCase t lb -> rc t; brl_map_compose f1 f2 g1 g2 h1 h2 i1 i2 lb
| TEps _ t -> t_map_compose (bmap f1) (bmap f2) g1 g2 h1 h2 i1 i2 t
| TForall _ t | TExists _ t ->
t_map_compose (bmap f1) (bmap f2) g1 g2 h1 h2 i1 i2 t
| TAnd t1 t2 | TOr t1 t2 | TImplies t1 t2 | TIff t1 t2 -> rc t1; rc t2
......@@ -1606,6 +1639,8 @@ module Commutations
| TLet t1 t2 -> rc t1;
term_smap_compose (term_lift f1) (bmap f2) g1 g2 h1 h2 i1 i2 t2
| TCase t lb -> rc t; branch_list_smap_compose f1 f2 g1 g2 h1 h2 i1 i2 lb
| TEps _ t ->
term_smap_compose (term_lift f1) (bmap f2) g1 g2 h1 h2 i1 i2 t
| TForall _ t | TExists _ t ->
term_smap_compose (term_lift f1) (bmap f2) g1 g2 h1 h2 i1 i2 t
| TAnd t1 t2 | TOr t1 t2 | TImplies t1 t2 | TIff t1 t2 -> rc t1; rc t2
......@@ -1818,6 +1853,7 @@ module Commutations
| TLet t1 t2 -> rc t1;
t_maps_compose (bmap f1) (term_lift f2) g1 g2 h1 h2 i1 i2 t2
| TCase t lb -> rc t; brl_maps_compose f1 f2 g1 g2 h1 h2 i1 i2 lb
| TEps _ t -> t_maps_compose (bmap f1) (term_lift f2) g1 g2 h1 h2 i1 i2 t
| TForall _ t | TExists _ t ->
t_maps_compose (bmap f1) (term_lift f2) g1 g2 h1 h2 i1 i2 t
| TAnd t1 t2 | TOr t1 t2 | TImplies t1 t2 | TIff t1 t2 -> rc t1; rc t2
......@@ -2042,6 +2078,8 @@ module Commutations
| TLet t1 t2 -> rc t1;
t_subst_compose (term_lift f1) (term_lift f2) g1 g2 h1 h2 i1 i2 t2
| TCase t lb -> rc t; brl_subst_compose f1 f2 g1 g2 h1 h2 i1 i2 lb
| TEps _ t ->
t_subst_compose (term_lift f1) (term_lift f2) g1 g2 h1 h2 i1 i2 t
| TForall _ t | TExists _ t ->
t_subst_compose (term_lift f1) (term_lift f2) g1 g2 h1 h2 i1 i2 t
| TAnd t1 t2 | TOr t1 t2 | TImplies t1 t2 | TIff t1 t2 -> rc t1; rc t2
......@@ -2219,6 +2257,7 @@ module Commutations
| TIf b t e -> rc b; rc t; rc e
| TLet t1 t2 -> rc t1; rc t2
| TCase t lb -> rc t; brl_subst_id lb
| TEps _ t -> rc t
| TForall _ t | TExists _ t -> rc t
| TAnd t1 t2 | TOr t1 t2 | TImplies t1 t2 | TIff t1 t2 -> rc t1; rc t2
| TNot t -> rc t
......
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -519,6 +519,8 @@ module Term
t_wf sig (ext_env env all (const ty0)) t2 ty
| TCase t brl -> exists ty0. t_wf sig env t ty0 /\
brl_wf sig env brl ty0 ty /\ exhaustive sig brl ty0
| TEps ty2 t -> ty = ty2 /\ ty_wf sig ty /\
t_wf sig (ext_env env all (const ty)) t sig.ty_prop
| TForall tyl t | TExists tyl t -> tyl_wf sig tyl /\
let dom = range 0 (length tyl) in
let env' = ext_env env dom (list_nth tyl default) in
......@@ -595,7 +597,8 @@ module Term
let ty0 = choose (ty_case_witness sig env t brl ty) in
t_wf_ty_wf sig env t ty0;
brl_wf_ty_wf sig env brl ty0 ty
| TForall _ _ | TExists _ _ | TAnd _ _ | TOr _ _ | TImplies _ _ | TIff _ _
| TEps _ _ | TForall _ _ | TExists _ _
| TAnd _ _ | TOr _ _ | TImplies _ _ | TIff _ _
| TNot _ | TTrue | TFalse | TVar _ -> ()
end
......
......@@ -80,12 +80,12 @@
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
</theory>
<theory name="Choice" sum="68e1b9014aa75a68b118b93980778ee0" expanded="true">
<theory name="Choice" sum="68e1b9014aa75a68b118b93980778ee0">
<goal name="WP_parameter choose" expl="VC for choose">
<proof prover="0"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
</theory>
<theory name="Finite" sum="7bd24662c8f9c694425089ee7fd83fb5" expanded="true">
<theory name="Finite" sum="05eaf7bb441bba99b938a60650e78e78" expanded="true">
<goal name="WP_parameter cardinal_remove" expl="VC for cardinal_remove">
<transf name="split_goal_wp">
<goal name="WP_parameter cardinal_remove.1" expl="1. assertion">
......
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