Commit e6709fbf authored by David Hauzar's avatar David Hauzar
Browse files
parents a6b1d368 0ba97e2e
#!/bin/sh
# tests for the safe prover
timelimit=60
timelimit=1
memlimit=1000
report="report.txt"
reperr="report_errors.txt"
report_xml="why3session.xml"
TMP=bench.out
TMPERR=bench.err
WHY3CPULIMIT=../../../lib/why3-cpulimit
run_dir () {
for file in `ls $1/*.p`; do
$WHY3CPULIMIT $timelimit $memlimit -s build/prover $file 2> $TMPERR > $TMP
cat << EOF > $report_xml
<?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="SafeProver" version="0.0.0" timelimit="$timelimit" memlimit="$memlimit"/>
<prover id="1" name="Zenon" version="0.8.0" timelimit="$timelimit" memlimit="$memlimit"/>
<prover id="2" name="Eprover" version="1.8" timelimit="$timelimit" memlimit="$memlimit"/>
<prover id="3" name="SPASS" version="3.7" timelimit="$timelimit" memlimit="$memlimit"/>
<prover id="4" name="Zenon_modulo" version="0.4.1" timelimit="$timelimit" memlimit="$memlimit"/>
<prover id="5" name="Vampire" version="0.6" timelimit="$timelimit" memlimit="$memlimit"/>
<file name="$1.why">
<theory name="Goals">
EOF
for file in `ls $1/???00*.p`; do
$WHY3CPULIMIT $timelimit $memlimit -s build/prover $file > $TMP 2>&1
ret=$?
if test "$ret" != "0" -a "$ret" != 152 ; then
printf "$file: ret code=$ret\n" >> $reperr
cat $TMP >> $reperr
cat $TMPERR >> $reperr
else
printf "<goal name=\"$file\">\n" >> $report_xml
printf "$file:\n" >> $report
time=`sed -n -e 's|.*time : \(.*\) s.*|\1|p' $TMPERR`
time=`sed -n -e 's|.*time : \(.*\) s.*|\1|p' $TMP`
if grep "Unsat" $TMP > /dev/null ; then
printf "<proof prover=\"0\"><result status=\"valid\" time=\"$time\"/></proof>\n" >> $report_xml
printf "Proved $time\n" >> $report
else
printf "<proof prover=\"0\"><result status=\"timeout\" time=\"$time\"/></proof>\n" >> $report_xml
printf "Not proved $time\n" >> $report
fi
# zenon
$WHY3CPULIMIT `expr $timelimit + 1` $memlimit -s zenon-0.7.1 -p0 -itptp -max-size $memlimit"M" -max-time $timelimit"s" $file 2> $TMPERR > $TMP
$WHY3CPULIMIT `expr $timelimit + 1` $memlimit -s zenon-0.8.0 -p0 -itptp -max-size $memlimit"M" -max-time $timelimit"s" $file > $TMP 2>&1
ret=$?
res=`sed -n -e 's|.*(\* \(.*PROOF.*\) \*).*|\1|p' $TMP`
time=`sed -n -e 's|.*time : \(.*\) s.*|\1|p' $TMPERR`
time=`sed -n -e 's|.*time : \(.*\) s.*|\1|p' $TMP`
if grep "PROOF-FOUND" $TMP > /dev/null ; then
printf "<proof prover=\"1\"><result status=\"valid\" time=\"$time\"/></proof>\n" >> $report_xml
elif grep "Zenon error: could not find a proof within the time limit" $TMP > /dev/null ; then
printf "<proof prover=\"1\"><result status=\"timeout\" time=\"$time\"/></proof>\n" >> $report_xml
elif grep "Zenon error: could not find a proof within the memory size limit" $TMP > /dev/null ; then
printf "<proof prover=\"1\"><result status=\"outofmemory\" time=\"$time\"/></proof>\n" >> $report_xml
else
printf "<proof prover=\"1\"><result status=\"unknown\" time=\"$time\"/></proof>\n" >> $report_xml
fi
printf "zenon: $res $time\n" >> $report
# eprover
$WHY3CPULIMIT `expr $timelimit + 1` $memlimit -s eprover -s -R -xAuto -tAuto --cpu-limit=$timelimit --tstp-in $file 2> $TMPERR > $TMP
$WHY3CPULIMIT `expr $timelimit + 1` $memlimit -s eprover -s -R -xAuto -tAuto --cpu-limit=$timelimit --tstp-in $file > $TMP 2>&1
ret=$?
res=`sed -n -e 's|# SZS status \(.*\)|\1|p' $TMP`
time=`sed -n -e 's|.*time : \(.*\) s.*|\1|p' $TMPERR`
time=`sed -n -e 's|.*time : \(.*\) s.*|\1|p' $TMP`
if grep "Proof found" $TMP > /dev/null ; then
printf "<proof prover=\"2\"><result status=\"valid\" time=\"$time\"/></proof>\n" >> $report_xml
elif grep "Ran out of time\|CPU time limit exceeded" $TMP > /dev/null ; then
printf "<proof prover=\"2\"><result status=\"timeout\" time=\"$time\"/></proof>\n" >> $report_xml
elif grep "Out of Memory" $TMP > /dev/null ; then
printf "<proof prover=\"2\"><result status=\"outofmemory\" time=\"$time\"/></proof>\n" >> $report_xml
else
printf "<proof prover=\"2\"><result status=\"unknown\" time=\"$time\"/></proof>\n" >> $report_xml
fi
printf "eprover: $res $time\n" >> $report
# SPASS
$WHY3CPULIMIT `expr $timelimit + 1` $memlimit -s SPASS -TPTP -PGiven=0 -PProblem=0 -TimeLimit=$timelimit $file 2> $TMPERR > $TMP
$WHY3CPULIMIT `expr $timelimit + 1` $memlimit -s SPASS -TPTP -PGiven=0 -PProblem=0 -TimeLimit=$timelimit $file > $TMP 2>&1
ret=$?
res=`sed -n -e 's|SPASS beiseite: \(.*\)|\1|p' $TMP`
time=`sed -n -e 's|.*time : \(.*\) s.*|\1|p' $TMPERR`
time=`sed -n -e 's|.*time : \(.*\) s.*|\1|p' $TMP`
if grep "Proof found" $TMP > /dev/null ; then
printf "<proof prover=\"3\"><result status=\"valid\" time=\"$time\"/></proof>\n" >> $report_xml
elif grep "Ran out of time\|CPU time limit exceeded" $TMP > /dev/null ; then
printf "<proof prover=\"3\"><result status=\"timeout\" time=\"$time\"/></proof>\n" >> $report_xml
elif grep "Out of Memory" $TMP > /dev/null ; then
printf "<proof prover=\"3\"><result status=\"outofmemory\" time=\"$time\"/></proof>\n" >> $report_xml
else
printf "<proof prover=\"3\"><result status=\"unknown\" time=\"$time\"/></proof>\n" >> $report_xml
fi
printf "SPASS: $res $time\n" >> $report
# zenon modulo
$WHY3CPULIMIT `expr $timelimit + 1` $memlimit -s zenon_modulo-0.4.1 -p0 -itptp -max-size $memlimit"M" -max-time $timelimit"s" $file > $TMP 2>&1
ret=$?
time=`sed -n -e 's|.*time : \(.*\) s.*|\1|p' $TMP`
if grep "PROOF-FOUND" $TMP > /dev/null ; then
printf "<proof prover=\"4\"><result status=\"valid\" time=\"$time\"/></proof>\n" >> $report_xml
elif grep "Zenon error: could not find a proof within the time limit" $TMP > /dev/null ; then
printf "<proof prover=\"4\"><result status=\"timeout\" time=\"$time\"/></proof>\n" >> $report_xml
elif grep "Zenon error: could not find a proof within the memory size limit" $TMP > /dev/null ; then
printf "<proof prover=\"4\"><result status=\"outofmemory\" time=\"$time\"/></proof>\n" >> $report_xml
else
printf "<proof prover=\"4\"><result status=\"unknown\" time=\"$time\"/></proof>\n" >> $report_xml
fi
printf "zenon_modulo: $res $time\n" >> $report
# Vampire
$WHY3CPULIMIT `expr $timelimit + 1` $memlimit -s vampire -t $timelimit"s" < $file > $TMP 2>&1
ret=$?
time=`sed -n -e 's|.*time : \(.*\) s.*|\1|p' $TMP`
if grep "Refutation found" $TMP > /dev/null ; then
printf "<proof prover=\"5\"><result status=\"valid\" time=\"$time\"/></proof>\n" >> $report_xml
elif grep "Time limit reached\|Time out" $TMP > /dev/null ; then
printf "<proof prover=\"5\"><result status=\"timeout\" time=\"$time\"/></proof>\n" >> $report_xml
elif grep "Memory limit exceeded" $TMP > /dev/null ; then
printf "<proof prover=\"5\"><result status=\"outofmemory\" time=\"$time\"/></proof>\n" >> $report_xml
else
printf "<proof prover=\"5\"><result status=\"unknown\" time=\"$time\"/></proof>\n" >> $report_xml
fi
printf "vampire: $res $time\n" >> $report
# end of proofs
printf "</goal>\n" >> $report_xml
fi
done
cat << EOF >> $report_xml
</theory>
</file>
</why3session>
EOF
}
......
......@@ -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 }