Commit 5a6b6c7d authored by Martin Clochard's avatar Martin Clochard
Browse files

in progress: formalization of why3 logic

parent ddaf081e
(* TODO: enforce the restriction (enforced by Why3) that all type variables
occur in a type scheme.
Also allow world creation. *)
module Ident
(* Identifiers types from Why3.
Note: as Why3 has no support for string whatsoever,
any transformation that should create particular names (pre-id)
(for readability) should do so by calling an abstract value
implemented in drivers. Nothing will be verified about actual names
anyway. *)
type preid
type ident
end
module Ty
use import logic_syntax.Defs as D
use import logic_syntax.VarsIn
use import logic_syntax.Substs
use import support.HO
use import support.Finite
use import ref.Ref
use import list.List
use import logic_typing.Env as E
use import Ident
use import option.Option
(* Type variables. *)
type tvsymbol
(* Interpretation of type variable. Variable interpretation is indeed
context-dependent. A type variable 'world' is a bijective mapping
between type variables and integers. It typically represent the
binding context for type variables. It live only in spec/ghost code. *)
type tvworld
function tv_m tvworld tvsymbol : int
function tv_mi tvworld int : tvsymbol
axiom tv_m_bijection : (forall tvw x. tv_mi tvw (tv_m tvw x) = x) /\
(forall tvw x. tv_m tvw (tv_mi tvw x) = x)
(* Machinery for generation of fresh type variables: maintain an ever-growing
finite set of generated names. *)
type tv_all model { mutable tv_all : tvsymbol -> bool }
type tv_all_s model { tv_all_s : tvsymbol -> bool }
val ghost tv_all_set : tv_all
(* Ensures growth of tv_all_set without having to state it in every
post-condition. *)
val ghost tv_all_snapshot () : tv_all_s
ensures { result.tv_all_s = tv_all_set.tv_all }
val ghost tv_all_growth (u:tv_all_s) : unit
ensures { forall x. u.tv_all_s x -> tv_all_set.tv_all x }
(* Every generated tvsymbol must be in the set.
Note: such an axiom is dangerous, as it may be a source of contradiction.
It basically states a type invariant dependent of a mutable variable.
However, the mentioned variable can only 'grow', and the invariant
'increase' with its growth, so the invariant may never become wrong.
Such statement becomes dangerous iff it is somehow possible to do an
infinite number of call to the statement => It is correct in current Why3,
but would be wrong in an imaginable extension with a Dafny-like forall.
(also, implementing a module with such a specification is currently
unfeasible in Why3) *)
val ghost tvsymbol_in (x:tvsymbol) : unit
ensures { tv_all_set.tv_all x }
val create_tvsymbol (x:preid) : tvsymbol
writes { tv_all_set }
ensures { not (old tv_all_set).tv_all result }
ensures { forall x. (old tv_all_set).tv_all x -> tv_all_set.tv_all x }
val tv_name (x:tvsymbol) : ident
val tv_equal (x y:tvsymbol) : bool
ensures { result <-> x = y }
(* Global world for top-level definitions. *)
val ghost tv_global : tvworld
(* Type symbols, types, and global signature.
Global signature behave roughly like tv_all_set. *)
(* Particular type symbol for propositions. Exists only at specification
level, in Why3 it is encoded specially using options (hence cannot
occur at any place beyond term toplevel) *)
constant tys_prop : D.ty_symbol
constant ty_prop : D.ty = D.TyApp tys_prop Nil
(* Particular logical symbol for equality. This version exists only
at specification level, and must be stated here because it is a signature
built-in. *)
constant ls_equ : D.lsymbol
type tysymbol
type ty
type ty_cons =
| TyVar tvsymbol
| TyApp tysymbol (list ty)
type signature model { mutable sig_m : E.signature }
invariant { sig_wf self.sig_m /\
self.sig_m.E.tys_prop = tys_prop /\
self.sig_m.E.ls_equ = ls_equ /\
forall tys. self.sig_m.tys_belong tys ->
finite (self.sig_m.tys_constr tys) }
type signature_s model { sig_s_m : E.signature }
invariant { sig_wf self.sig_s_m /\
self.sig_s_m.E.tys_prop = tys_prop /\
self.sig_s_m.E.ls_equ = ls_equ /\
forall tys. self.sig_s_m.tys_belong tys ->
finite (self.sig_s_m.tys_constr tys) }
function ts_m tysymbol : D.ty_symbol
(* Encode the stateless information into the name. Not only it is
what is actually done in Why3 anyway, but it also simplify preservation
proofs for stateless information through environmental extension. *)
function ts_arity tysymbol : int
function ty_m tvworld ty : D.ty
function tyl_m (tvw:tvworld) (tyl:list ty) : list D.ty = match tyl with
| Nil -> Nil
| Cons x q -> Cons (ty_m tvw x) (tyl_m tvw q)
end
val ghost global_sig : signature
val ghost global_sig_snapshot () : signature_s
ensures { result.sig_s_m = global_sig.sig_m }
val ghost global_sig_growth (s:signature_s) : unit
ensures { let so = s.sig_s_m in let sc = global_sig.sig_m in
(forall tys. so.tys_belong tys -> sc.tys_belong tys /\
sc.tys_arity tys = so.tys_arity tys) /\
(forall tys ls. so.tys_belong tys /\ so.tys_constr tys ls ->
sc.tys_constr tys ls) /\
(forall ls. so.ls_belong ls -> sc.ls_belong ls /\
sc.ls_ty_arity ls = so.ls_ty_arity ls /\
sc.ls_args ls = so.ls_args ls /\
sc.ls_ret ls = so.ls_ret ls) /\
(forall ls. so.ls_constr ls -> sc.ls_constr ls) }
val ghost tysymbol_in (tys:tysymbol) : unit
ensures { global_sig.sig_m.tys_belong (ts_m tys) }
ensures { global_sig.sig_m.tys_arity (ts_m tys) = ts_arity tys }
ensures { ts_m tys <> tys_prop }
val ghost ty_inv (ghost tvw:tvworld) (ty:ty) : unit
ensures { ty_wf global_sig.sig_m (ty_m tvw ty) }
ensures { let s0 = compose tv_all_set.tv_all (tv_mi tvw) in
ty_vars_in s0 global_sig.sig_m.tys_belong (ty_m tvw ty) }
let rec ghost tyl_inv (ghost tvw:tvworld) (tyl:list ty) : unit
ensures { tyl_wf global_sig.sig_m (tyl_m tvw tyl) }
ensures { let s0 = compose tv_all_set.tv_all (tv_mi tvw) in
tyl_vars_in s0 global_sig.sig_m.tys_belong (tyl_m tvw tyl) }
variant { tyl }
= match tyl with Cons x q -> ty_inv tvw x;tyl_inv tvw q | _ -> () end
val ts_equal (u v:tysymbol) : bool
ensures { result -> u = v }
ensures { ts_m u = ts_m v -> result }
val ts_arity (u:tysymbol) : int
ensures { result = ts_arity u = global_sig.sig_m.tys_arity (ts_m u) }
val create_tysymbol (p:preid) (ar:int) : tysymbol
writes { global_sig }
ensures { not (old global_sig).sig_m.tys_belong result.ts_m }
ensures { ts_arity result = ar = global_sig.sig_m.tys_arity result.ts_m }
val ty_var (ghost tvw:tvworld) (tyv:tvsymbol) : ty
ensures { ty_m tvw result = D.TyVar (tv_m tvw tyv) }
val ty_app (ghost tvw:tvworld) (tys:tysymbol) (tyl:list ty) : ty
ensures { ty_m tvw result = D.TyApp (ts_m tys) (tyl_m tvw tyl) }
val ty_case (ghost tvw:tvworld) (ty:ty) : ty_cons
returns { TyVar tv -> ty_m tvw ty = D.TyVar (tv_m tvw tv)
| TyApp tys tyl -> ty_m tvw ty = D.TyApp (ts_m tys) (tyl_m tvw tyl) }
function tyo_m (tvw:tvworld) (ty:option ty) : D.ty = match ty with
| None -> ty_prop
| Some ty -> ty_m tvw ty
end
(*
(* TODO: Replace the functional arguments in substitution, using
some kind of maps abstraction.
Though relatively easy to specify as itself, requires backup from
such specified implementation of maps, which is not written yet. *)
val ty_inst (ghost tvg:tvgroup) (f:tvsymbol -> ty) (ty:ty) : ty
requires { forall x. ty_var_g x = ty_g ty -> ty_g (f x) = tvg }
ensures { let f0 = compose ty_m (compose f (get_tvs (ty_g ty))) in
ty_g result = tvg /\
ty_m result = ty_subst f0 identity (ty_m ty) /\
ty_wf env.sig_m (ty_m result) }
(* TODO: type matching... *)
(* TODO: add other various built-in type symbols. *)
*)
end
module Term
use import logic_syntax.Defs as D
use import logic_syntax.VarsIn
use import logic_syntax.Substs
use import support.HO
use import support.Finite
use import ref.Ref
use import list.List
use import logic_typing.Env as E
use import option.Option
use import int.Int
use import Ident
use import Ty
(* First, logical symbols. *)
type lsymbol
function ls_m lsymbol : D.lsymbol
function ls_constr lsymbol : int
function ls_tvworld lsymbol : tvworld
function ls_ty_arity lsymbol : int
function ls_args lsymbol : list D.ty
function ls_ret lsymbol : D.ty
axiom ls_constr_pos : forall ls. ls.ls_constr >= 0
(* tys_constr global environment. *)
type ts_constr_env model { mutable tsc : D.ty_symbol -> int }
type ts_constr_env_s model { tsc_s : D.ty_symbol -> int }
val ghost ts_constr_env : ts_constr_env
val ghost ts_constr_env_snapshot () : ts_constr_env_s
ensures { result.tsc_s = ts_constr_env.tsc }
val ghost ts_constr_env_fixed (e:ts_constr_env_s) : unit
ensures { forall tys. tys_alg global_sig.sig_m tys ->
ts_constr_env.tsc tys = e.tsc_s tys }
val ghost ts_constr_env_s_inv (e:ts_constr_env_s) : unit
ensures { let sig = global_sig.sig_m in
forall tys. tys_alg sig tys ->
e.tsc_s tys > 0 /\ e.tsc_s tys >= cardinal (sig.tys_constr tys) /\
(e.tsc_s tys = cardinal (sig.tys_constr tys) <->
sig.tys_constr_complete tys) }
let ghost ts_constr_env_inv () : unit
ensures { let e = ts_constr_env in let sig = global_sig.sig_m in
forall tys. tys_alg sig tys ->
e.tsc tys > 0 /\ e.tsc tys >= cardinal (sig.tys_constr tys) /\
(e.tsc tys = cardinal (sig.tys_constr tys) <->
sig.tys_constr_complete tys) }
= ts_constr_env_s_inv (ts_constr_env_snapshot ())
val ls_name lsymbol : ident
val ls_args (ls:lsymbol) : list ty
ensures { tyl_m ls.ls_tvworld result = ls.ls_args
= global_sig.sig_m.E.ls_args ls.ls_m }
val ls_value (ls:lsymbol) : option ty
ensures { tyo_m ls.ls_tvworld result = ls.ls_ret
= global_sig.sig_m.E.ls_ret ls.ls_m }
val ghost ls_ty_arity (ls:lsymbol) : int
ensures { result = ls.ls_ty_arity
= global_sig.sig_m.E.ls_ty_arity ls.ls_m }
val ghost ls_tvworld (ls:lsymbol) : tvworld
ensures { result = ls.ls_tvworld }
(* ls_constr is a complicated field: if it is > 0, then the lsymbol
is a constructor, and the cardinal of constructors in the same type
being ls_constr is equivalent to the type being complete for this
decomposition. *)
val ls_constr (ls:lsymbol) : int
ensures { result = ls.ls_constr }
ensures { result > 0 -> let sig = global_sig.sig_m in
sig.E.ls_constr ls.ls_m /\ match sig.E.ls_ret ls.ls_m with
| D.TyVar _ -> false
| D.TyApp tys _ -> result = ts_constr_env.tsc tys end }
val ls_equal (a b:lsymbol) : bool
ensures { result -> a = b }
ensures { ls_m a = ls_m b -> result }
val create_lsymbol (ghost tvw:tvworld) (ghost ty_ar:int)
(constr:int) (p:preid) (tyl:list ty) (vl:option ty) : lsymbol
writes { ts_constr_env , global_sig }
requires { ty_vars_in (range 0 ty_ar) all (tyo_m tvw vl) }
requires { tyl_vars_in (range 0 ty_ar) all (tyl_m tvw tyl) }
requires { constr >= 0 }
requires { constr > 0 -> match tyo_m tvw vl with
| D.TyApp tys _ -> tys_alg global_sig.sig_m tys ->
constr = ts_constr_env.tsc tys
| _ -> false
end }
ensures { not (old global_sig).sig_m.ls_belong result.ls_m }
ensures { result.ls_ty_arity = ty_ar }
ensures { result.ls_constr = constr }
ensures { result.ls_args = tyl_m tvw tyl }
ensures { result.ls_ret = tyo_m tvw vl }
(* MISSING: equivalent of ls_ty_freevars. *)
(* Variable symbols. *)
type vsymbol
function vs_ty tvworld vsymbol : D.ty
val vs_equal (a b:vsymbol) : bool
ensures { result <-> a = b }
(* Terms (without patterns for now). *)
type term 'tv
function t_ptl (term 'tv) : 'tv -> vsymbol
function t_ltp (term 'tv) : vsymbol -> 'tv
function t_ty tvworld (term 'tv) : D.tys
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<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>
</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>
</goal>
</theory>
</file>
</why3session>
......@@ -572,14 +572,18 @@ module WellTyped
sig.tys_constr ty_alg f /\ sig.tys_constr ty_alg g /\ f <> g /\
m.ty_doms (m.ty_funs ty_alg ty_a) u ->
not m.ls_case f ty_a u \/ not m.ls_case g ty_a u) /\
(* All elements in an algebraic type can be
(* All elements in a complete algebraic type can be
inverted to some constructor. *)
(forall ty_alg ty_a x.
tys_alg sig ty_alg /\ m.ty_doms (m.ty_funs ty_alg ty_a) x ->
sig.tys_constr_complete ty_alg /\ m.ty_doms (m.ty_funs ty_alg ty_a) x ->
exists f. sig.tys_constr ty_alg f /\ m.ls_case f ty_a x) /\
(* Constructors are injective. *)
(forall f ty_a args.
sig.ls_constr f -> m.ls_proj f ty_a (m.ls_eval f ty_a args) = args)
sig.ls_constr f -> m.ls_proj f ty_a (m.ls_eval f ty_a args) = args) /\
(* Semantics for equality. *)
(forall ty_a x y. m.ty_doms ty_a x /\ m.ty_doms ty_a y ->
m.ls_eval sig.ls_equ (Cons ty_a Nil) (Cons x (Cons y Nil)) = m.i_true <->
x = y)
predicate valuation_coherence (m:model 'univ)
(tyv:ty_valuation 'univ) (env:ty_env 'tv) (v:valuation 'tv 'univ) =
......@@ -622,13 +626,44 @@ module WellTyped
possible to refine the skeletal shape to a point where a given case
does not accept the shape anymore. Once done through the whole
pattern-matching, we have a skeletal shape that is NOT accepted by
any case, which is an obvious contradication. *)
any case, which is an obvious contradication.
Note: again, there is a bit of trouble with extension to incomplete
algebraic types. We cannot simply use pat_accept to represent
acceptation by a skeletal pattern.
*)
predicate skeleton_accept (sig:signature) (m:model 'univ)
(tyv:ty_valuation 'univ) (pat:pattern) (ty:ty) (x:'univ) = match pat with
| PWild -> true
| PVar _ -> match ty with
| TyApp tys tyl -> (forall f. sig.tys_constr tys f ->
not m.ls_case f (tyl_sem m tyv tyl) x)
| TyVar _ -> true
end
| PApp f tyl args -> let prj = (m.ls_proj f (tyl_sem m tyv tyl) x) in
m.ls_case f (tyl_sem m tyv tyl) x /\
skeleton_l_accept sig m tyv args (ty_args sig f tyl) prj
| _ -> false
end
with skeleton_l_accept (sig:signature) (m:model 'univ)
(tyv:ty_valuation 'univ)
(patl:list pattern) (tyl:list ty) (lx:list 'univ) =
match patl , lx , tyl with
| Nil , Nil , Nil -> true
| Cons hp qp , Cons hx qx , Cons hty qty ->
skeleton_accept sig m tyv hp hty hx /\
skeleton_l_accept sig m tyv qp qty qx
| _ -> false
end
(* p1 is a skeleton refinement of p2. *)
predicate pat_refine (p1 p2:pattern) =
match p2 with
| PWild -> true
| PApp f tyl l -> exists l'. p1 = PApp f tyl l' /\ patl_refine l' l
| PVar _ -> p1 = p2
| _ -> false
end
......@@ -640,48 +675,55 @@ module WellTyped
end
(* Some properties of skeleton pattern refinement. *)
let rec lemma pat_refine_self (p:pattern) : unit
requires { pat_skeleton p }
let rec lemma pat_refine_self (sig:signature) (p:pattern) (ty:ty) : unit
requires { skeleton_wty sig p ty }
ensures { pat_refine p p }
variant { p }
= match p with
| PApp _ _ l -> patl_refine_self l
| PApp f tyl l -> patl_refine_self sig l (ty_args sig f tyl)
| _ -> ()
end
with lemma patl_refine_self (l:list pattern) : unit
requires { patl_skeleton l }
with lemma patl_refine_self (sig:signature) (l:list pattern)
(tyl:list ty) : unit
requires { skeleton_l_wty sig l tyl }
ensures { patl_refine l l }
variant { l }
= match l with
| Cons x q -> pat_refine_self x; patl_refine_self q
| _ -> ()
= match l , tyl with
| Cons x q , Cons hty qty -> pat_refine_self sig x hty;
patl_refine_self sig q qty
| Nil , Nil -> ()
| _ -> absurd
end
let rec lemma pat_refine_trans (p1 p2 p3:pattern) : unit
requires { pat_skeleton p1 /\ pat_refine p1 p2 }
requires { pat_skeleton p2 /\ pat_refine p2 p3 }
let rec lemma pat_refine_trans (sig:signature)
(p1 p2 p3:pattern) (ty:ty) : unit
requires { skeleton_wty sig p1 ty /\ pat_refine p1 p2 }
requires { skeleton_wty sig p2 ty /\ pat_refine p2 p3 }
ensures { pat_refine p1 p3 }
variant { p1 }
= match p1 , p2 , p3 with
| PApp _ _ l1 , PApp _ _ l2 , PApp _ _ l3 -> patl_refine_trans l1 l2 l3
| PApp f tyl l1 , PApp _ _ l2 , PApp _ _ l3 ->
patl_refine_trans sig l1 l2 l3 (ty_args sig f tyl)
| _ , _ , _ -> ()
end
with lemma patl_refine_trans (l1 l2 l3:list pattern) : unit
requires { patl_skeleton l1 /\ patl_refine l1 l2 }
requires { patl_skeleton l2 /\ patl_refine l2 l3 }
with lemma patl_refine_trans (sig:signature)
(l1 l2 l3:list pattern) (tyl:list ty) : unit
requires { skeleton_l_wty sig l1 tyl /\ patl_refine l1 l2 }
requires { skeleton_l_wty sig l2 tyl /\ patl_refine l2 l3 }
ensures { patl_refine l1 l3 }
variant { l1 }
= match l1 , l2 , l3 with
| Cons x1 q1 , Cons x2 q2 , Cons x3 q3 ->
pat_refine_trans x1 x2 x3; patl_refine_trans q1 q2 q3
| Nil , Nil , Nil -> ()
| _ , _ , _ -> absurd
= match l1 , l2 , l3 , tyl with
| Cons x1 q1 , Cons x2 q2 , Cons x3 q3 , Cons hty qty ->
pat_refine_trans sig x1 x2 x3 hty ; patl_refine_trans sig q1 q2 q3 qty
| Nil , Nil , Nil , Nil -> ()
| _ , _ , _ , _ -> absurd
end
let rec lemma pat_refine_skeleton_match (p1 p2 p3:pattern) : unit
requires { pat_skeleton p1 /\ pat_refine p1 p2 }
let rec lemma pat_refine_skeleton_match (sig:signature)
(p1 p2 p3:pattern) (ty:ty) : unit
requires { skeleton_wty sig p1 ty /\ pat_refine p1 p2 }
requires { pat_skeleton_match p1 p3 }
ensures { pat_skeleton_match p2 p3 }
variant { p3 }
......@@ -689,26 +731,29 @@ module WellTyped
| _ , PWild , _ -> ()
| PWild , _ , _ -> absurd
| _ , _ , (PWild | PVar _) -> ()
| _ , _ , PAs p3 _ -> pat_refine_skeleton_match p1 p2 p3
| _ , _ , PAs p3 _ -> pat_refine_skeleton_match sig p1 p2 p3 ty
| _ , _ , POr p3 p4 ->
let u = if pat_skeleton_match p1 p3 then p3 else p4 in
pat_refine_skeleton_match p1 p2 u
| PApp _ _ l1 , PApp _ _ l2 , PApp _ _ l3 ->
patl_refine_skeleton_match l1 l2 l3
pat_refine_skeleton_match sig p1 p2 u ty
| PApp f tyl l1 , PApp _ _ l2 , PApp _ _ l3 ->
patl_refine_skeleton_match sig l1 l2 l3 (ty_args sig f tyl)
| _ -> absurd
end
with lemma patl_refine_skeleton_match (l1 l2 l3:list pattern) : unit
requires { patl_skeleton l1 /\ patl_refine l1 l2 }
with lemma patl_refine_skeleton_match (sig:signature)
(l1 l2 l3:list pattern) (tyl:list ty) : unit
requires { skeleton_l_wty sig l1 tyl /\ patl_refine l1 l2 }
requires { patl_skeleton_match l1 l3 }
ensures { patl_skeleton_match l2 l3 }
variant { l3 }
= match l1 , l2 , l3 with
| Nil , Nil , Nil -> ()
| Cons x1 q1 , Cons x2 q2 , Cons x3 q3 ->
patl_refine_skeleton_match q1 q2 q3;
pat_refine_skeleton_match x1 x2 x3
| _ , _ , _ -> absurd
= match l1 , l2 , l3 , tyl with
| Nil , Nil , Nil , Nil -> ()
| Cons x1 q1 , Cons x2 q2 , Cons x3 q3 , Cons hty qty ->
patl_refine_skeleton_match sig q1 q2 q3 qty;
pat_refine_skeleton_match sig x1 x2 x3 hty
| Nil , _ , _ , _ | _ , Nil , _ , _ | _ , _ , Nil , _ | _ , _ , _ , Nil ->
"keep_on_simp" absurd
| _ , _ , _ , _ -> absurd
end
(* Build a list of wildcard patterns. *)
......@@ -716,8 +761,8 @@ module WellTyped
(tyv:ty_valuation 'univ) (args:list 'univ) (tyl:list ty) : list pattern
requires { tyl_doms m (tyl_sem m tyv tyl) args }
ensures { patl_wty sig result tyl }
ensures { patl_skeleton result }
ensures { patl_accept m tyv result args }
ensures { skeleton_l_wty sig result tyl }
ensures { skeleton_l_accept sig m tyv result tyl args }
variant { tyl }
= match args , tyl with
| Nil , Nil -> let res = Nil in
......@@ -725,9 +770,6 @@ module WellTyped
| Cons _ q1 , Cons _ q2 ->
let qr = pat_wild_list m sig tyv q1 q2 in
let res = Cons PWild qr in
assert { not patl_accept m tyv res args ->
(forall s. patl_sem m tyv qr q1 s ->
patl_sem m tyv res args (extend (const None) s) && false) && false };
res
| _ , _ -> absurd
end
......@@ -736,17 +778,20 @@ module WellTyped
(ty_alg:ty_symbol) (tyl:list 'univ) (x:'univ) : lsymbol -> bool =
\f. m.ls_case f tyl x /\ sig.tys_constr ty_alg f
meta rewrite_def function is_constructor
predicate eis_constructor (m:model 'univ) (sig:signature)
(ty_alg:ty_symbol) (tyl:list 'univ) (x:'univ) =
exists g. is_constructor m sig ty_alg tyl x g
(* Skeleton refinement through a pattern. *)
let rec ghost pat_refine_unaccepted (m:model 'univ) (sig:signature)
(tyv:ty_valuation 'univ) (x:'univ) (coh pat:pattern) (ty:ty) : pattern
requires { model_ok m /\ sig_wf sig /\ model_sig_coherence m sig }
requires { pat_wty sig pat ty /\ pat_wty sig coh ty }
requires { pat_accept m tyv coh x /\ pat_skeleton coh }
requires { pat_wty sig pat ty /\ skeleton_wty sig coh ty }
requires { skeleton_accept sig m tyv coh ty x }
requires { m.ty_doms (ty_sem m tyv ty) x }
requires { not pat_accept m tyv pat x }
ensures { pat_accept m tyv result x /\ pat_skeleton result }
ensures { pat_refine result coh /\ pat_wty sig result ty }
ensures { skeleton_accept sig m tyv result ty x }
ensures { pat_refine result coh /\ skeleton_wty sig result ty }
ensures { not pat_skeleton_match result pat }
variant { pat }
= match coh , pat with
......@@ -754,7 +799,7 @@ module WellTyped
if f = g
then match sig.ls_ret f , sig.ls_ret g with
| TyApp ty_alg1 _ , TyApp ty_alg2 _ ->
assert { sig.tys_belong ty_alg1 &&
assert { sig.tys_belong ty_alg1 && sig.tys_belong ty_alg2 &&
sig.tys_constr ty_alg1 f && sig.tys_constr ty_alg2 g &&
TyApp ty_alg1 tylf = ty = TyApp ty_alg2 tylg &&
ty_alg1 = ty_alg2 && tylf = tylg };
......@@ -764,9 +809,6 @@ module WellTyped
assert { tyl_doms m (ty_inst_args m sig f tyl_s) lx };
let l_coh = patl_refine_unaccepted m sig tyv lx lf lg ty_a in
let res = PApp g tylg l_coh in
assert { not pat_accept m tyv res x ->
(forall s. patl_sem m tyv l_coh lx s ->
pat_sem m tyv res x s && false) && false };
res
| _ -> absurd
end else coh
......@@ -776,31 +818,28 @@ module WellTyped
sig.tys_constr ty_alg f && ty = TyApp ty_alg tyl &&
tys_alg sig ty_alg };
let tyl_s = tyl_sem m tyv tyl in
let g = choose (is_constructor m sig ty_alg tyl_s x) in
match sig.ls_ret g with
| TyApp ty_algg _ -> assert { sig.tys_constr ty_algg g &&
ty_algg = ty_alg && ty_ret sig g tyl = ty };
let ty_a = ty_args sig g tyl in
let lx = m.ls_proj g tyl_s x in
assert { tyl_doms m (ty_inst_args m sig g tyl_s) lx };
let lg = pat_wild_list m sig tyv lx ty_a in
if f = g
then begin
let l_coh = patl_refine_unaccepted m sig tyv lx lg lf ty_a in
let res = PApp g tyl l_coh in
assert { not pat_accept m tyv res x ->
(forall s. patl_sem m tyv l_coh lx s ->
pat_sem m tyv res x s && false) && false };
res
end else begin
let res = PApp g tyl lg in
assert { not pat_accept m tyv res x ->
(forall s. patl_sem m tyv lg lx s ->
pat_sem m tyv res x s && false) && false };
res
if eis_constructor m sig ty_alg tyl_s x
then let g = choose (is_constructor m sig ty_alg tyl_s x) in
match sig.ls_ret g with
| TyApp ty_algg _ -> assert { sig.tys_constr ty_algg g &&
ty_algg = ty_alg && ty_ret sig g tyl = ty };
let ty_a = ty_args sig g tyl in
let lx = m.ls_proj g tyl_s x in
assert { tyl_doms m (ty_inst_args m sig g tyl_s) lx };
let lg = pat_wild_list m sig tyv lx ty_a in
if f = g
then begin
let l_coh = patl_refine_unaccepted m sig tyv lx lg lf ty_a in
let res = PApp g tyl l_coh in
res
end else begin
let res = PApp g tyl lg in
res
end
| _ -> absurd
end
| _ -> absurd
end
else let (u:pat_var) = choose all in
PVar u
| _ -> absurd
end
| _ , PWild -> assert { pat_sem m tyv pat x (const None) };absurd
......@@ -829,6 +868,7 @@ module WellTyped
| PWild , _ | _ , PWild -> ("keep_on_simp" true) && false
| _ -> false end && false };
coh2
| PVar _ , _ -> coh
| _ -> absurd