Commit b5e59b06 authored by Martin Clochard's avatar Martin Clochard
Browse files

(wip) example: formalization of Why3 term API

parent 510a24ec
......@@ -10,14 +10,41 @@ module Ctx
function c_pdom (context 'p 'l) : 'p -> bool
function c_ltp (context 'p 'l) : 'l -> 'p
function c_ptl (context 'p 'l) : 'p -> 'l
axiom context_inv : forall c:context 'p 'l.
maps_to c.c_ldom c.c_ltp c.c_pdom /\
maps_to c.c_pdom c.c_ptl c.c_ldom /\
(forall x. c.c_ldom x -> c.c_ptl (c.c_ltp x) = x) /\
(forall x. c.c_pdom x -> c.c_ltp (c.c_ptl x) = x)
predicate context_pred (ld:'l -> bool) (pd:'p -> bool)
(ltp:'l -> 'p) (ptl:'p -> 'l) =
maps_to ld ltp pd /\ maps_to pd ptl ld /\
(forall x. ld x -> ptl (ltp x) = x) /\ (forall x. pd x -> ltp (ptl x) = x)
predicate context_inv (c:context 'p 'l) =
context_pred c.c_ldom c.c_pdom c.c_ltp c.c_ptl
axiom context_inv : forall c:context 'p 'l. context_inv c
function make_context (ld:'l -> bool) (pd:'p -> bool)
(ltp:'l -> 'p) (ptl:'p -> 'l) : context 'p 'l
axiom make_context_ok : forall ld pd,ltp:'l -> 'p,ptl.
context_pred ld pd ltp ptl -> let u = make_context ld pd ltp ptl in
u.c_ldom = ld /\ u.c_pdom = pd /\ u.c_ltp = ltp /\ u.c_ptl = ptl
let ghost make_context (ld:'l -> bool) (pd:'p -> bool)
(ltp:'l -> 'p) (ptl:'p -> 'l) : context 'p 'l
requires { context_pred ld pd ltp ptl }
ensures { let r = result in r = make_context ld pd ltp ptl /\
r.c_ldom = ld /\ r.c_pdom = pd /\ r.c_ltp = ltp /\ r.c_ptl = ptl }
= make_context ld pd ltp ptl
predicate context_inj (c1:context 'p 'l1) (f:'l1 -> 'l2) (c2:context 'p 'l2) =
forall x. c1.c_pdom x -> c2.c_pdom x /\ c2.c_ptl x = f (c1.c_ptl x)
let lemma context_inj_maps_to
(c1:context 'p 'l1) (f:'l1 -> 'l2) (c2:context 'p 'l2) : unit
ensures { context_inj c1 f c2 -> maps_to c1.c_ldom f c2.c_ldom }
= ()
predicate sub_context (c1 c2:context 'p 'l) = context_inj c1 id c2
let lemma sub_context_subset (c1 c2:context 'p 'l) : unit
ensures { sub_context c1 c2 -> subset c1.c_ldom c2.c_ldom }
= ()
end
......@@ -2,8 +2,19 @@
<!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"/>
<prover id="1" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../context.mlw" expanded="true">
<theory name="Ctx" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="Ctx" sum="d9ec23af0f527829d9a3d3ecc63fe569">
<goal name="WP_parameter make_context" expl="VC for make_context">
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter context_inj_maps_to" expl="VC for context_inj_maps_to">
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="WP_parameter sub_context_subset" expl="VC for sub_context_subset">
<proof prover="1"><result status="valid" time="0.07"/></proof>
</goal>
</theory>
</file>
</why3session>
......@@ -115,6 +115,9 @@ module Ident
pre_loc : option position;
}
(* TODO (long term): add a mechanism to get back identifier
fields (mainly labels) from their names. *)
(* Similar mechanism for identifier generation. *)
type id_set model { mutable ids : ident_name -> bool }
type id_set_snapshot model { ids_s : ident_name -> bool }
......
......@@ -46,26 +46,38 @@ module Sig
equalizer (tys_alg so) s.tsc_n_s global_sig.tsc_n }
(* Allowed symbols domain, e.g symbol contexts. *)
type sym_context
function d_tys sym_context : ty_symbol -> bool
function d_ls sym_context : lsymbol -> bool
function d_constr sym_context : lsymbol -> bool
axiom sym_context_inv : forall sc ls. sc.d_constr ls -> sc.d_ls ls
type sym_ctx
function d_tys sym_ctx : ty_symbol -> bool
function d_ls sym_ctx : lsymbol -> bool
function d_constr sym_ctx : lsymbol -> bool
axiom sym_ctx_inv : forall sc ls. sc.d_constr ls -> sc.d_ls ls
predicate sub_sym_context (s1 s2:sym_context) =
predicate sub_sym_ctx (s1 s2:sym_ctx) =
subset s1.d_tys s2.d_tys /\
subset s1.d_ls s2.d_ls /\
subset s1.d_constr s2.d_constr
predicate sym_ctx_wf (sig:S.signature) (s:sym_context) =
subset s.d_tys sig.tys_belong /\
subset s.d_ls sig.ls_belong /\
subset s.d_constr sig.ls_constr /\
(forall ls. s.d_ls ls -> ty_vars_in all s.d_tys (sig.ls_ret ls) /\
tyl_vars_in all s.d_tys (sig.ls_args ls))
predicate sym_prj_wf (sig:S.signature) (dtys:ty_symbol -> bool)
(dls:lsymbol -> bool) (dconstr:lsymbol -> bool) =
subset dtys sig.tys_belong /\
subset dls sig.ls_belong /\
subset dconstr sig.ls_constr /\
(forall ls. dls ls -> ty_vars_in all dtys (sig.ls_ret ls) /\
tyl_vars_in all dtys (sig.ls_args ls))
val ghost sym_bounds (sym_c:sym_context) : unit
predicate sym_ctx_wf (sig:S.signature) (s:sym_ctx) =
sym_prj_wf sig s.d_tys s.d_ls s.d_constr
val ghost sym_bounds (sym_c:sym_ctx) : unit
ensures { sym_ctx_wf global_sig.sig_m sym_c }
val ghost make_sym_ctx (dtys:ty_symbol -> bool)
(dls:lsymbol -> bool)
(dconstr:lsymbol -> bool) : sym_ctx
requires { sym_prj_wf global_sig.sig_m dtys dls dconstr }
ensures { result.d_tys = dtys }
ensures { result.d_ls = dls }
ensures { result.d_constr = dconstr }
end
module Vs
use import support.HO
use import ident.String
use import ident.Ident
use import ident.Label
use import list.List
use import option.Option
use import ty.Tv
use import ty.Ty
(* Toplevel declaration: ident class of term variables. *)
constant vs_id_class_name : ident_name
axiom vs_id_class_name_distinct :
vs_id_class_name <> tv_id_class_name /\
vs_id_class_name <> ts_id_class_name
val ghost vs_id_class () : id_class
ensures { result.id_class_name = vs_id_class_name }
(* Type variable symbols. *)
type vsymbol
function vs_name vsymbol : ident
function vs_ty vsymbol : ty
function vs_idn (vs:vsymbol) : ident_name = vs.vs_name.id_name
axiom vs_inv : forall x. exists y z.
x.vs_name.id_class = Cons y z /\ y.id_class_name = vs_id_class_name
val vs_name (vs:vsymbol) : ident
ensures { result = vs.vs_name }
val vs_ty (vs:vsymbol) : ty
ensures { result = vs.vs_ty }
val vs_equal (vs1 vs2:vsymbol) : bool
ensures { vs1.vs_idn = vs2.vs_idn -> result }
ensures { result -> vs1 = vs2 }
val create_vs_symbol (ghost idc:list id_class) (p:preid) : vsymbol
writes { ids }
ensures { result.vs_name.id_string = p.pre_name }
ensures { result.vs_name.id_label = p.pre_label.Mlab.domain }
ensures { result.vs_name.id_loc = p.pre_loc }
ensures { exists y. result.vs_name.id_class = Cons y idc /\
y.id_class_name = vs_id_class_name }
ensures { not (old ids).ids result.vs_idn }
ensures { subset (old ids).ids ids.ids }
ensures { ids.ids result.vs_idn }
clone extmap.FMap as Mvs with
type key = tvsymbol,
type key_l = ident_name,
function k_m = tv_idn
end
module Ls
use import int.Int
use import list.List
use import option.Option
use import ident.Ident
use import logic_syntax.Defs as D
use import logic_syntax.FreeVars
use logic_typing.Sig as E
use import context.Ctx
use import support.HO
use import support.HOList
use import signature.Sig
use import ty.Tv
use import ty.Ty
(* Split the logical view of logic symbols in two parts:
constant and non-constant symbols. *)
predicate ls_constant D.lsymbol
(* Global growing correspondance between logic symbols and
their identifiers names. *)
type ls_ctx model {
mutable ctls : context ident_name D.lsymbol;
}
type ls_ctx_snapshot model {
ctls_s : context ident_name D.lsymbol;
}
val ghost ls_ctx : ls_ctx
val ghost ls_ctx_snapshot () : ls_ctx_snapshot
ensures { result.ctls_s = ls_ctx.ctls }
val ghost ls_ctx_growth (s:ls_ctx_snapshot) : unit
ensures { sub_context s.ctls_s ls_ctx.ctls }
type lsymbol
function ls_name lsymbol : ident
function ls_m lsymbol : D.lsymbol
function ls_constr lsymbol : int
function ls_ctv lsymbol : context ident_name int
function ls_ty_arity lsymbol : int
function ls_args lsymbol : list D.ty
function ls_ret lsymbol : D.ty
axiom ls_inv : forall ls. not ls.ls_m.ls_constant /\
ls.ls_ctv.c_ldom = range 0 ls.ls_ty_arity /\
(* Additional requirement with respect to general signature:
any bound type variable must be relevant to the symbol scheme.
This enforces subsitution unicity for application. *)
forall n. 0 <= n < ls.ls_ty_arity ->
ty_tyv_free_var ls.ls_ret n \/ tyl_tyv_free_var ls.ls_args n
function ls_idn (ls:lsymbol) : ident_name = ls.ls_name.id_name
type const
function cst_m const : D.lsymbol
axiom const_inv : forall c. c.cst_m.ls_constant
val ls_name (ls:lsymbol) : ident
ensures { result = ls.ls_name }
val ghost ls_cty (sym_c:sym_ctx) (ls:lsymbol) : ty_ctx
requires { sym_c.d_ls ls.ls_m }
ensures { result.cty_sym = sym_c }
ensures { result.cty_tv = ls.ls_ctv }
val ls_args (ghost cty:ty_ctx) (ls:lsymbol) : list ty
requires { cty.cty_sym.d_ls ls.ls_m }
requires { cty.cty_tv = ls.ls_ctv }
ensures { map (cty.cty_m) result = ls.ls_args }
val ls_value (ghost cty:ty_ctx) (ls:lsymbol) : option ty
requires { cty.cty_sym.d_ls ls.ls_m }
requires { cty.cty_tv = ls.ls_ctv }
ensures { match result with
| None -> ls.ls_ret = E.ty_prop
| Some u -> ls.ls_ret = cty.cty_m u
end }
val ls_constr (ls:lsymbol) : int
ensures { result >= 0 }
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 _ -> tys <> E.tys_prop /\
result = global_sig.tsc_n tys
end }
val ghost ls_inv (ls:lsymbol) : unit
ensures { not ls_constant ls.ls_m /\ let sig = global_sig.sig_m in
sig.E.ls_belong ls.ls_m /\ ls.ls_ty_arity = sig.E.ls_ty_arity ls.ls_m /\
ls.ls_ret = sig.E.ls_ret ls.ls_m /\ ls.ls_args = sig.E.ls_args ls.ls_m /\
ls.ls_ctv.c_ldom = range 0 ls.ls_ty_arity /\
(forall n. 0 <= n < ls.ls_ty_arity ->
ty_tyv_free_var ls.ls_ret n \/ tyl_tyv_free_var ls.ls_args n) /\
ls.ls_constr >= 0 /\ (ls.ls_constr <> 0 <-> sig.E.ls_constr ls.ls_m) /\
ls.ls_constr <> 0 -> match sig.E.ls_ret ls.ls_m with
| D.TyVar _ -> false
| D.TyApp tys _ -> tys <> E.tys_prop /\
ls.ls_constr = global_sig.tsc_n tys
end /\
let ctls = ls_ctx.ctls in
ctls.c_ldom ls.ls_m /\ ctls.c_pdom ls.ls_idn /\
ctls.c_ltp ls.ls_m = ls.ls_idn /\ ctls.c_ptl ls.ls_idn = ls.ls_m }
val ghost const_inv (cst:const) : unit
ensures { ls_constant cst.cst_m /\ let sig = global_sig.sig_m in
sig.E.ls_belong cst.cst_m /\ sig.E.ls_ty_arity cst.cst_m = 0 /\
sig.E.ls_args cst.cst_m = Nil /\ not sig.E.ls_constr cst.cst_m }
val ls_equal (a b:lsymbol) : bool
ensures { result -> a = b }
ensures { a.ls_m = b.ls_m -> result }
ensures { a.ls_idn = b.ls_idn -> result }
val create_lsymbol (ghost cty:ty_ctx) (ghost ty_ar:int)
(constr:int) (p:preid) (tyl:list ty) (vl:option ty) : lsymbol
writes { global_sig , ids , ls_ctx }
requires { cty.cty_tv.c_ldom = range 0 ty_ar }
requires { for_all cty.cty_d tyl /\ match vl with
| None -> true
| Some ty -> cty.cty_d ty
end }
requires { constr = 0 -> forall n. 0 <= n < ty_ar ->
tyl_tyv_free_var (map (cty.cty_m) tyl) n \/ match vl with
| None -> false
| Some u -> ty_tyv_free_var (cty.cty_m u) n
end }
requires { constr >= 0 }
requires { constr <> 0 -> match vl with
| None -> false
| Some ty -> match cty.cty_m ty with
| D.TyVar _ -> false
| D.TyApp tys tyl -> E.tys_alg global_sig.sig_m tys ->
constr = global_sig.tsc_n tys /\
not global_sig.sig_m.E.tys_constr_complete tys /\
E.distinct_tyv tyl /\ ty_ar = global_sig.sig_m.E.tys_arity tys
end
end }
ensures { not (old ids).ids result.ls_idn }
ensures { not (old global_sig).sig_m.E.ls_belong result.ls_m }
ensures { result.ls_ty_arity = ty_ar }
ensures { result.ls_constr = constr }
ensures { result.ls_args = map (cty.cty_m) tyl }
ensures { match vl with
| None -> result.ls_ret = E.ty_prop
| Some u -> result.ls_ret = cty.cty_m u
end }
ensures { result.ls_ctv = cty.cty_tv }
ensures { constr = 0 ->
global_sig.sig_m.E.ls_constr = (old global_sig).sig_m.E.ls_constr }
ensures { constr > 0 -> global_sig.sig_m.E.ls_constr =
update (old global_sig).sig_m.E.ls_constr result.ls_m true }
val ls_ty_freevars (ls:lsymbol) : Mtv.s
ensures { result.Mtv.domain = ls.ls_ctv.c_pdom }
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">
<file name="../term.mlw" expanded="true">
<theory name="Vs" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Ls" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
</file>
</why3session>
......@@ -13,44 +13,18 @@ module Tv
val ghost tv_id_class () : id_class
ensures { result.id_class_name = tv_id_class_name }
(* Contexts for type variables. Represents the type variables allowed at
a given location and the correspondance with their models.
TODO: implements a type for general variable contexts, which is
basically a bijection between two domains on different types:
ident_name & int for type variable context,
ident_name & 'a for term variable context. *)
type tv_context
(*function ctv_m tv_context : context *)
function tv_dom tv_context : ident_name -> bool
function tv_fun tv_context : ident_name -> int
function tv_rfun tv_context : int -> ident_name
axiom tv_context_inv : forall ctv id.
ctv.tv_dom id -> ctv.tv_rfun (ctv.tv_fun id) = id
val ghost tv_bounds (ctv:tv_context) : unit
ensures { subset ctv.tv_dom ids.ids }
val ghost tv_make_context (dm:ident_name -> bool)
(fn:ident_name -> int) (rfn:int -> ident_name) : tv_context
requires { forall x. dm x -> rfn (fn x) = x }
ensures { result.tv_dom = dm }
ensures { result.tv_fun = fn }
ensures { result.tv_rfun = rfn }
(* Context injection in another. *)
predicate tv_ctx_inj (tv1:tv_context) (f:int -> int) (tv2:tv_context) =
forall i. tv1.tv_dom i -> tv2.tv_dom i /\ tv2.tv_fun i = f (tv1.tv_fun i)
(* Type variable symbols. *)
type tvsymbol
function tv_name tvsymbol : ident
function tv_idn (vty:tvsymbol) : ident_name = vty.tv_name.id_name
axiom tv_inv : forall x. exists y z.
x.tv_name.id_class = Cons y z /\ y.id_class_name = tv_id_class_name
val tv_name (vty:tvsymbol) : ident
ensures { result = vty.tv_name }
val tv_equal (vty1 vty2:tvsymbol) : bool
ensures { vty1.tv_name.id_name = vty2.tv_name.id_name -> result }
ensures { vty1.tv_idn = vty2.tv_idn -> result }
ensures { result -> vty1 = vty2 }
val create_tv_symbol (ghost idc:list id_class) (p:preid) : tvsymbol
......@@ -60,9 +34,9 @@ module Tv
ensures { result.tv_name.id_loc = p.pre_loc }
ensures { exists y. result.tv_name.id_class = Cons y idc /\
y.id_class_name = tv_id_class_name }
ensures { not (old ids).ids result.tv_name.id_name }
ensures { not (old ids).ids result.tv_idn }
ensures { subset (old ids).ids ids.ids }
ensures { ids.ids result.tv_name.id_name }
ensures { ids.ids result.tv_idn }
val tv_of_string (s:string) : tvsymbol
writes { ids }
......@@ -72,107 +46,299 @@ module Tv
ensures { exists y. result.tv_name.id_class = Cons y Nil /\
y.id_class_name = tv_id_class_name }
ensures { subset (old ids).ids ids.ids }
ensures { ids.ids result.tv_name.id_name }
ensures { ids.ids result.tv_idn }
clone extmap.FMap as Mtv with
type key = tvsymbol,
type key_l = ident_name,
function k_m = tv_idn
end
module Ty
use import ident.Label
use import ident.Ident
use import context.Ctx
use import signature.Sig
use import Tv
use import logic_syntax.Defs as D
use import logic_syntax.Maps
use import logic_syntax.Substs
use import logic_syntax.VarsIn
use import logic_syntax.FreeVars
use logic_typing.Sig as E
use import option.Option
use import list.List
use import list.Length
use import list.Nth
use import int.Int
use import support.Choice
use import support.HO
use import support.HOList
use import ident.Ident
use import signature.Sig
use import Tv
(* Types. *)
type ty
(* Type contexts: gives meaning to types by interpreting their variables. *)
type ty_ctx
function cty_tv ty_ctx : context ident_name int
function cty_sym ty_ctx : sym_ctx
function cty_d ty_ctx : ty -> bool
function cty_m ty_ctx : ty -> D.ty
(* Contexts are bounded upward by identifier sets. *)
val ghost cty_ubounds (cty:ty_ctx) : unit
ensures { subset cty.cty_tv.c_pdom ids.ids }
ensures { sym_ctx_wf global_sig.sig_m cty.cty_sym }
ensures { context_inv cty.cty_tv }
(* Contexts are bounded downward by the free variables of
their member types. *)
val ghost cty_lbounds (cty:ty_ctx) : unit
ensures { forall ty. cty.cty_d ty ->
ty_vars_in cty.cty_tv.c_ldom cty.cty_sym.d_tys (cty.cty_m ty) }
(* Can make any context as long as the upward bound is respected. *)
val ghost make_cty (ctv:context ident_name int) (sym_c:sym_ctx) : ty_ctx
requires { subset ctv.c_pdom ids.ids }
ensures { result.cty_tv = ctv /\ result.cty_sym = sym_c }
(* Transfer model function between contexts in injection relation. *)
val ghost map_cty (cty1:ty_ctx) (f:int -> int) (cty2:ty_ctx) : unit
requires { context_inj cty1.cty_tv f cty2.cty_tv }
requires { sub_sym_ctx cty1.cty_sym cty2.cty_sym }
ensures { forall ty. cty1.cty_d ty ->
cty2.cty_d ty /\ cty2.cty_m ty = ty_map f id (cty1.cty_m ty) }
(* Transfer model function between contexts in inclusion relation. *)
val ghost sub_cty (cty1 cty2:ty_ctx) : unit
requires { sub_context cty1.cty_tv cty2.cty_tv }
requires { sub_sym_ctx cty1.cty_sym cty2.cty_sym }
ensures { forall ty. cty1.cty_d ty ->
cty2.cty_d ty /\ cty2.cty_m ty = cty1.cty_m ty }
(* TODO: context shrinking via free variables membership & an
injection/inclusion relation. At least relevant for logic symbols type
schemes: they have a basic binding context, which may be shrinked
(from the point of view of type symbols) in case the symbol
is used in a smaller context later on. *)
(* dummy type context to default create_tysymbol parameter. *)
constant dummy_ty_ctx : ty_ctx
(* Fresh toplevel declaration: identifier class for type symbols. *)
constant ts_id_class_name : ident_name
axiom ts_id_class_name_distinct : ts_id_class_name <> tv_id_class_name
val ghost ts_id_class () : id_class
ensures { result.id_class_name = ts_id_class_name }
(* Type symbol may be defined or abstract (expanded alias). *)
(* Global growing correspondance between abstract type symbols and
their identifiers names. *)
type tys_ctx model {
mutable cts : context ident_name D.ty_symbol;
}
type tys_ctx_snapshot model {
cts_s : context ident_name D.ty_symbol;
}
val ghost tys_ctx : tys_ctx
val ghost tys_ctx_snapshot () : tys_ctx_snapshot
ensures { result.cts_s = tys_ctx.cts }
val ghost tys_ctx_growth (s:tys_ctx_snapshot) : unit
ensures { sub_context s.cts_s tys_ctx.cts }
(* Type symbols: either abstract or alias. *)
type tysymbol
function ts_name tysymbol : ident
function ts_arity tysymbol : int
function ts_abs tysymbol : bool
predicate ts_alias tysymbol
(* In case abstract: name in the logical world. *)
function ts_m tysymbol : D.ty_symbol
(* In case alias: fixed definition context & actual definition. *)
function ts_def_ctx tysymbol : ty_ctx
function ts_def tysymbol : D.ty
axiom tv_inv : forall x. exists y z.
x.ts_name.id_class = Cons y z /\ y.id_class_name = ts_id_class_name
function ts_idn (tys:tysymbol) : ident_name = tys.ts_name.id_name
axiom ts_inv : forall x. (exists y z.
x.ts_name.id_class = Cons y z /\ y.id_class_name = ts_id_class_name) /\
(x.ts_alias -> let dc = x.ts_def_ctx in
dc.cty_tv.c_ldom = range 0 x.ts_arity /\
ty_vars_in dc.cty_tv.c_ldom dc.cty_sym.d_tys x.ts_def) /\
x.ts_m <> E.tys_prop
val ghost ts_inv (x:tysymbol) : unit
ensures { exists y z.
x.ts_name.id_class = Cons y z /\ y.id_class_name = ts_id_class_name }
ensures { (x.ts_alias -> let dc = x.ts_def_ctx in
dc.cty_tv.c_ldom = range 0 x.ts_arity /\
ty_vars_in dc.cty_tv.c_ldom dc.cty_sym.d_tys x.ts_def) }
ensures { not x.ts_alias -> let cts = tys_ctx.cts in
cts.c_ldom x.ts_m /\ cts.c_pdom x.ts_idn /\
cts.c_ltp x.ts_m = x.ts_idn /\ cts.c_ptl x.ts_idn = x.ts_m }
ensures { not x.ts_alias -> let gs = global_sig.sig_m in
gs.E.tys_belong x.ts_m /\ gs.E.tys_arity x.ts_m = x.ts_arity }
ensures { x.ts_m <> E.tys_prop }
(* Type symbols procedures. *)
val ts_name (tys:tysymbol) : ident
ensures { result = tys.ts_name }
(* Correspondance from type symbols to identifiers.
FIXME ? using a logical function imply that all identifiers
can be pulled back to a type symbols, e.g that the cardinality
of the ident_name type is lower than the cardinality of the
type symbol type, which is a priori not evident.
(otherwise, type symbol generation simply cannot be implemented)
The other technique is to use a growing map, but this is much
more convoluted. *)
function tys_idn (tys:D.ty_symbol) : ident_name
val ts_args (tys:tysymbol) : list tvsymbol
ensures { length result = tys.ts_arity }
ensures { ts_alias tys ->
tys.ts_def_ctx.cty_tv.c_ldom = range 0 tys.ts_arity
/\ forall n. 0 <= n < tys.ts_arity ->
match nth n result with
| None -> false
| Some u -> u.tv_idn = tys.ts_def_ctx.cty_tv.c_ltp n
end }
(* TODO: type symbol generation: function from global signature ty_symbols to
identifiers & reciprocal. *)
val ts_def (tys:tysymbol) : option ty
returns { None -> not ts_alias tys
| Some ty -> ts_alias tys /\ let cty = tys.ts_def_ctx in
cty.cty_d ty /\ cty.cty_m ty = tys.ts_def }
(* Context mechanism: a type has sense only in a context. *)
type ty
(* Type context: allowed type variables/symbols and
variable name -> integer correspondance.
From the point of view of types, corresponds to a domain and
an interpretation. *)
type ty_ctx model {
cty_tv : tv_context;
cty_sym : sym_context;
cty_d : ty -> bool;
cty_m : ty -> D.ty;
}
val ts_equal (tys1 tys2:tysymbol) : bool
ensures { not tys1.ts_alias /\ not tys2.ts_alias /\
tys1.ts_m = tys2.ts_m -> result }
ensures { tys1.ts_idn = tys2.ts_idn -> result }
ensures { result -> tys1 = tys2 }
type ty_node =
| Tyvar tvsymbol
| Tyapp tysymbol (list ty)
val create_tysymbol (ghost idc:list id_class) (ghost cty:ty_ctx)
(p:preid) (args:list tvsymbol) (def:option ty) : tysymbol
writes { ids , global_sig , tys_ctx }
requires { match def with
| None -> true
| Some ty -> cty.cty_tv.c_ldom = range 0 (length args) /\
(forall n. 0 <= n < length args ->
match nth n args with
| None -> false
| Some u -> u.tv_idn = cty.cty_tv.c_ltp n
end) /\
cty.cty_d ty
end }
ensures { result.ts_name.id_string = p.pre_name }
ensures { result.ts_name.id_label = p.pre_label.Mlab.domain }
ensures { result.ts_name.id_loc = p.pre_loc }
ensures { exists y. result.ts_name.id_class = Cons y idc /\
y.id_class_name = ts_id_class_name }
ensures { not (old ids).ids result.ts_idn }
ensures { subset (old ids).ids ids.ids }