programs: typing programs first, then annotations

parent 10d709b6
...@@ -89,7 +89,7 @@ parameter add_edge : ...@@ -89,7 +89,7 @@ parameter add_edge :
path (old graph) x b and path (old graph) a y) path (old graph) x b and path (old graph) a y)
} }
let add_edge_and_union (u:ref uf) (a:int) (b:int) = let add_edge_and_union u (a:int) (b:int) =
{ 0 <= a < size u and 0 <= b < size u and { 0 <= a < size u and 0 <= b < size u and
not same u a b and not path graph a b and not same u a b and not path graph a b and
forall x y:int. forall x y:int.
......
...@@ -46,7 +46,7 @@ parameter add : ...@@ -46,7 +46,7 @@ parameter add :
let (d, t) = r in let (d, t) = r in
memt t k v or (v = d and forall v':value. not (memt t k v')) memt t k v or (v = d and forall v':value. not (memt t k v'))
let create d = let create (d : int) =
{ } { }
let x = (d, Leaf) in ref x (* BUG: ref (d, Leaf) *) let x = (d, Leaf) in ref x (* BUG: ref (d, Leaf) *)
{ default result = d and { default result = d and
......
...@@ -91,7 +91,7 @@ parameter ghost_find : u:ref uf -> x:int -> ...@@ -91,7 +91,7 @@ parameter ghost_find : u:ref uf -> x:int ->
int reads u int reads u
{ repr !u x result } { repr !u x result }
let increment (u : ref uf) (r : int) = let increment u r =
{ inv !u and 0 <= r < size !u } { inv !u and 0 <= r < size !u }
let i = ref 0 in let i = ref 0 in
let d = ref (dist !u) in let d = ref (dist !u) in
...@@ -108,7 +108,7 @@ let increment (u : ref uf) (r : int) = ...@@ -108,7 +108,7 @@ let increment (u : ref uf) (r : int) =
{ forall i:int. 0 <= i < size !u -> { forall i:int. 0 <= i < size !u ->
result#i = (dist !u)#i + if repr !u i r then 1 else 0 } result#i = (dist !u)#i + if repr !u i r then 1 else 0 }
let union (u:ref uf) (a b:int) = let union u a b =
{ inv !u and { inv !u and
0 <= a < size !u and 0 <= b < size !u and not same !u a b } 0 <= a < size !u and 0 <= b < size !u and not same !u a b }
let ra = find u a in let ra = find u a in
......
...@@ -46,12 +46,7 @@ type deffect = { ...@@ -46,12 +46,7 @@ type deffect = {
de_raises : esymbol list; de_raises : esymbol list;
} }
type dpre = Denv.dfmla (* specialized type_v *)
type dpost_fmla = Denv.dty * Denv.dfmla
type dexn_post_fmla = Denv.dty option * Denv.dfmla
type dpost = dpost_fmla * (Term.lsymbol * dexn_post_fmla) list
type dtype_v = type dtype_v =
| DTpure of Denv.dty | DTpure of Denv.dty
| DTarrow of dbinder list * dtype_c | DTarrow of dbinder list * dtype_c
...@@ -59,15 +54,35 @@ type dtype_v = ...@@ -59,15 +54,35 @@ type dtype_v =
and dtype_c = and dtype_c =
{ dc_result_type : dtype_v; { dc_result_type : dtype_v;
dc_effect : deffect; dc_effect : deffect;
dc_pre : dpre; dc_pre : Denv.dfmla;
dc_post : dpost; } dc_post : (Denv.dty * Denv.dfmla) *
(Term.lsymbol * (Denv.dty option * Denv.dfmla)) list; }
and dbinder = ident * Denv.dty * dtype_v and dbinder = ident * Denv.dty * dtype_v
type dvariant = Denv.dterm * Term.lsymbol option (* user type_v *)
type dpre = Ptree.pre
type dpost_fmla = Ptree.lexpr
type dexn_post_fmla = Ptree.lexpr
type dpost = dpost_fmla * (Term.lsymbol * dexn_post_fmla) list
type dutype_v =
| DUTpure of Denv.dty
| DUTarrow of dubinder list * dutype_c
and dutype_c =
{ duc_result_type : dutype_v;
duc_effect : deffect;
duc_pre : Ptree.lexpr;
duc_post : Ptree.lexpr * (Term.lsymbol * Ptree.lexpr) list; }
and dubinder = ident * Denv.dty * dutype_v
type dvariant = Ptree.lexpr * Term.lsymbol option
type dloop_annotation = { type dloop_annotation = {
dloop_invariant : Denv.dfmla option; dloop_invariant : Ptree.lexpr option;
dloop_variant : dvariant option; dloop_variant : dvariant option;
} }
...@@ -84,7 +99,7 @@ and dexpr_desc = ...@@ -84,7 +99,7 @@ and dexpr_desc =
| DEglobal of psymbol * dtype_v | DEglobal of psymbol * dtype_v
| DElogic of Term.lsymbol | DElogic of Term.lsymbol
| DEapply of dexpr * dexpr | DEapply of dexpr * dexpr
| DEfun of dbinder list * dtriple | DEfun of dubinder list * dtriple
| DElet of ident * dexpr * dexpr | DElet of ident * dexpr * dexpr
| DEletrec of drecfun list * dexpr | DEletrec of drecfun list * dexpr
...@@ -96,13 +111,13 @@ and dexpr_desc = ...@@ -96,13 +111,13 @@ and dexpr_desc =
| DEabsurd | DEabsurd
| DEraise of esymbol * dexpr option | DEraise of esymbol * dexpr option
| DEtry of dexpr * (esymbol * string option * dexpr) list | DEtry of dexpr * (esymbol * string option * dexpr) list
| DEfor of ident * dexpr * for_direction * dexpr * Denv.dfmla option * dexpr | DEfor of ident * dexpr * for_direction * dexpr * Ptree.lexpr option * dexpr
| DEassert of assertion_kind * Denv.dfmla | DEassert of assertion_kind * Ptree.lexpr
| DElabel of string * dexpr | DElabel of string * dexpr
| DEany of dtype_c | DEany of dutype_c
and drecfun = (ident * Denv.dty) * dbinder list * dvariant option * dtriple and drecfun = (ident * Denv.dty) * dubinder list * dvariant option * dtriple
and dtriple = dpre * dexpr * dpost and dtriple = dpre * dexpr * dpost
...@@ -111,15 +126,18 @@ and dtriple = dpre * dexpr * dpost ...@@ -111,15 +126,18 @@ and dtriple = dpre * dexpr * dpost
type variant = Term.term * Term.lsymbol option type variant = Term.term * Term.lsymbol option
type reference = R.t type loop_annotation = {
loop_invariant : Term.fmla option;
loop_variant : variant option;
}
type pre = T.pre type ipre = T.pre
type post = T.post type ipost = T.post
(* each program variable is materialized by two logic variables (vsymbol): (* each program variable is materialized by two logic variables (vsymbol):
one for typing programs and another for typing annotations *) one for typing programs and another for typing annotations *)
type ivsymbol = { type ivsymbol (* = Term.vsymbol *) = {
i_pgm : Term.vsymbol; (* in programs *) i_pgm : Term.vsymbol; (* in programs *)
i_logic : Term.vsymbol; (* in annotations *) i_logic : Term.vsymbol; (* in annotations *)
} }
...@@ -141,16 +159,11 @@ type itype_v = ...@@ -141,16 +159,11 @@ type itype_v =
and itype_c = and itype_c =
{ ic_result_type : itype_v; { ic_result_type : itype_v;
ic_effect : ieffect; ic_effect : ieffect;
ic_pre : pre; ic_pre : T.pre;
ic_post : post; } ic_post : T.post; }
and ibinder = ivsymbol * itype_v and ibinder = ivsymbol * itype_v
type loop_annotation = {
loop_invariant : Term.fmla option;
loop_variant : variant option;
}
type label = Term.vsymbol type label = Term.vsymbol
type irec_variant = ivsymbol * Term.term * Term.lsymbol option type irec_variant = ivsymbol * Term.term * Term.lsymbol option
...@@ -160,7 +173,7 @@ type ipattern = { ...@@ -160,7 +173,7 @@ type ipattern = {
ipat_node : ipat_node; ipat_node : ipat_node;
} }
and ipat_node = and ipat_node =
| IPwild | IPwild
| IPvar of ivsymbol | IPvar of ivsymbol
| IPapp of Term.lsymbol * ipattern list | IPapp of Term.lsymbol * ipattern list
...@@ -199,12 +212,18 @@ and iexpr_desc = ...@@ -199,12 +212,18 @@ and iexpr_desc =
and irecfun = ivsymbol * ibinder list * irec_variant option * itriple and irecfun = ivsymbol * ibinder list * irec_variant option * itriple
and itriple = pre * iexpr * post and itriple = ipre * iexpr * ipost
(*****************************************************************************) (*****************************************************************************)
(* phase 3: effect inference *) (* phase 3: effect inference *)
type reference = R.t
type pre = T.pre
type post = T.post
type rec_variant = pvsymbol * Term.term * Term.lsymbol option type rec_variant = pvsymbol * Term.term * Term.lsymbol option
type pattern = { type pattern = {
......
...@@ -68,6 +68,10 @@ let ts_arrow = ...@@ -68,6 +68,10 @@ let ts_arrow =
let v = List.map (fun s -> create_tvsymbol (Ident.id_fresh s)) ["a"; "b"] in let v = List.map (fun s -> create_tvsymbol (Ident.id_fresh s)) ["a"; "b"] in
Ty.create_tysymbol (Ident.id_fresh "arrow") v None Ty.create_tysymbol (Ident.id_fresh "arrow") v None
let make_arrow_type tyl ty =
let arrow ty1 ty2 = Ty.ty_app ts_arrow [ty1; ty2] in
List.fold_right arrow tyl ty
module Sexn = Term.Sls module Sexn = Term.Sls
module rec T : sig module rec T : sig
...@@ -182,10 +186,6 @@ end = struct ...@@ -182,10 +186,6 @@ end = struct
let purify ty = try model_type ty with NotMutable -> ty let purify ty = try model_type ty with NotMutable -> ty
let make_arrow_type tyl ty =
let arrow ty1 ty2 = Ty.ty_app ts_arrow [ty1; ty2] in
List.fold_right arrow tyl ty
let rec uncurry_type ?(logic=false) = function let rec uncurry_type ?(logic=false) = function
| Tpure ty when not logic -> | Tpure ty when not logic ->
[], ty [], ty
......
...@@ -29,6 +29,7 @@ val is_mutable_ts : tysymbol -> bool ...@@ -29,6 +29,7 @@ val is_mutable_ts : tysymbol -> bool
val is_mutable_ty : ty -> bool val is_mutable_ty : ty -> bool
val ts_arrow : tysymbol val ts_arrow : tysymbol
val make_arrow_type : ty list -> ty -> ty
val ts_exn : tysymbol val ts_exn : tysymbol
val ty_exn : ty val ty_exn : ty
......
This diff is collapsed.
...@@ -4,17 +4,17 @@ module P ...@@ -4,17 +4,17 @@ module P
use import int.Int use import int.Int
use import module stdlib.Ref use import module stdlib.Ref
parameter b : ref int (* parameter b : ref int *)
let f () = (* let f () = *)
{ b>0 } !b + 1 { result > b } (* { b>0 } !b + 1 { result > b } *)
use import module stdlib.Array let test r =
{ r = 1 }
let test (a : array int) = assert { r = 1 };
{ A.length a >= 1 } r := !r + 1;
Array.get a 0 assert { r = 2 }
{ result = a#0 } { true }
end end
......
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