program type declarations

parent 1d2a1147
......@@ -21,8 +21,18 @@ open Why3
open Util
open Ident
open Ty
open Term
open Decl
open Mlw_ty
open Mlw_expr
type pconstructor = psymbol * psymbol option list
type ity_defn =
| ITabstract
| ITalgebraic of pconstructor list
type ity_decl = itysymbol * ity_defn
type pdecl = {
pd_node : pdecl_node;
......@@ -31,10 +41,108 @@ type pdecl = {
pd_tag : int; (* unique tag *)
}
and pdecl_node
and pdecl_node =
| PDtype of ity_decl list
let pd_equal : pdecl -> pdecl -> bool = (==)
let mk_decl =
let r = ref 0 in
fun node syms news ->
incr r;
{ pd_node = node; pd_syms = syms; pd_news = news; pd_tag = !r; }
let news_id s id = Sid.add_new (Decl.ClashIdent id) id s
let syms_ts s ts = Sid.add ts.ts_name s
let syms_ls s ls = Sid.add ls.ls_name s
let syms_its s its = Sid.add its.its_pure.ts_name s
let syms_ps s ps = Sid.add ps.p_name s
let syms_ty s ty = ty_s_fold syms_ts s ty
let syms_term s t = t_s_fold syms_ty syms_ls s t
let syms_ity s ity = ity_s_fold syms_its syms_ts s ity
(** {2 Declaration constructors} *)
exception BadConstructor of psymbol
exception BadRecordField of psymbol
type pre_pconstructor = preid * (pvsymbol * bool) list
type pre_ity_defn =
| PITabstract
| PITalgebraic of pre_pconstructor list
type pre_ity_decl = itysymbol * pre_ity_defn
let create_ity_decl tdl =
let syms = ref Sid.empty in
let add s (its,_) = news_id s its.its_pure.ts_name in
let news = ref (List.fold_left add Sid.empty tdl) in
let projections = Hvs.create 17 in (* vs -> psymbol *)
let build_constructor its (id, al) =
(* check well-formedness *)
let tvs = List.fold_right Stv.add its.its_args Stv.empty in
let regs = List.fold_right Sreg.add its.its_regs Sreg.empty in
let check_tv tv =
if not (Stv.mem tv tvs) then raise (UnboundTypeVar tv); true in
let check_reg r =
if not (Sreg.mem r regs) then raise (UnboundRegion r); true in
let check_pv (pv,_) = match pv.pv_mutable with
| None -> ignore (ity_v_all check_tv check_reg pv.pv_ity)
| Some r -> if not (Sreg.mem r regs) then raise (UnboundRegion r)
in
List.iter check_pv al;
(* build the constructor ps *)
let ity = ity_app its (List.map ity_var its.its_args) its.its_regs in
let result = create_pvsymbol (id_fresh "result") ity in
let ty_args = List.map (fun (pv, _) -> pv.pv_vs.vs_ty) al in
let ls = create_fsymbol id ty_args (ty_of_ity ity) in
let t = t_app ls (List.map (fun (pv,_) -> t_var pv.pv_vs) al) ls.ls_value in
let post = t_equ (t_var result.pv_vs) t in
let add_erase ef r = eff_union ef (eff_erase r) in
let add_erase ef (pv,_) = option_fold add_erase ef pv.pv_mutable in
let effect = List.fold_left add_erase eff_empty al in
let c = create_cty ~post ~effect (vty_value result) in
let arrow (pv,_) c = create_cty (vty_arrow pv c) in
let v = (List.fold_right arrow al c).c_vty in
let ps = create_psymbol id Stv.empty Sreg.empty v in
news := Sid.add ps.p_name !news;
(* build the projections, if any *)
let build_proj pv id =
let ls = create_fsymbol id [result.pv_vs.vs_ty] pv.pv_vs.vs_ty in
let t = fs_app ls [t_var result.pv_vs] pv.pv_vs.vs_ty in
let post = t_equ (t_var pv.pv_vs) t in
let add_read ef r = eff_union ef (eff_read r) in
let effect = option_fold add_read eff_empty pv.pv_mutable in
let vty = vty_arrow result (create_cty ~post ~effect (vty_value pv)) in
let ps = create_psymbol id Stv.empty Sreg.empty vty in
news := Sid.add ps.p_name !news;
Hvs.add projections pv.pv_vs ps;
ps
in
let build_proj pv =
try Hvs.find projections pv.pv_vs with Not_found -> build_proj pv id in
let build_proj (pv, pj) =
syms := ity_s_fold syms_its syms_ts !syms pv.pv_ity;
if pj then Some (build_proj pv) else None in
ps, List.map build_proj al
in
let build_type (its, defn) = its, match defn with
| PITabstract -> ITabstract
| PITalgebraic cl ->
Hvs.clear projections;
ITalgebraic (List.map (build_constructor its) cl)
in
let tdl = List.map build_type tdl in
mk_decl (PDtype tdl) !syms !news
(** {2 Known identifiers} *)
type known_map = pdecl Mid.t
let known_id kn id =
......
......@@ -21,6 +21,19 @@ open Why3
open Ident
open Ty
open Mlw_ty
open Mlw_expr
(** {2 Type declaration} *)
type pconstructor = psymbol * psymbol option list
type ity_defn =
| ITabstract
| ITalgebraic of pconstructor list
type ity_decl = itysymbol * ity_defn
(** {2 Declaration type} *)
type pdecl = private {
pd_node : pdecl_node;
......@@ -29,11 +42,25 @@ type pdecl = private {
pd_tag : int; (* unique tag *)
}
and pdecl_node
and pdecl_node =
| PDtype of ity_decl list
(** {2 Declaration constructors} *)
type pre_pconstructor = preid * (pvsymbol * bool) list
type pre_ity_defn =
| PITabstract
| PITalgebraic of pre_pconstructor list
type pre_ity_decl = itysymbol * pre_ity_defn
val create_ity_decl : pre_ity_decl list -> pdecl
(** {2 Known identifiers} *)
type known_map = pdecl Mid.t
val known_id : known_map -> ident -> unit
val known_add_decl : known_map -> pdecl -> known_map
val merge_known: known_map -> known_map -> known_map
......@@ -24,7 +24,7 @@ open Mlw_ty
(* program symbols *)
type psymbol = {
p_ident: ident;
p_name: ident;
p_tvs: Stv.t;
p_reg: Sreg.t;
p_vty: vty;
......@@ -33,7 +33,7 @@ type psymbol = {
let create_psymbol id tvars regs vty =
(* TODO? check that tvars/regs are in vty *)
{ p_ident = id_register id;
{ p_name = id_register id;
p_tvs = tvars;
p_reg = regs;
p_vty = vty; }
......
......@@ -24,9 +24,9 @@ open Mlw_ty
(* program symbols *)
type psymbol = private {
p_ident: ident;
p_tvs: Stv.t;
p_reg: Sreg.t;
p_name: ident;
p_tvs: Stv.t; (* type variables that cannot be instantiated *)
p_reg: Sreg.t; (* regions that cannot be instantiated *)
p_vty: vty;
(* pv_ghost: bool; *)
}
......
......@@ -90,6 +90,7 @@ val add_meta : module_uc -> meta -> meta_arg list -> module_uc
(** Program decls *)
(*
val add_ty_pdecl : module_uc -> ty_pdecl list -> module_uc
val add_pdecl : module_uc -> pdecl -> module_uc
val add_pdecl_with_tuples : module_uc -> pdecl -> module_uc
*)
......@@ -41,19 +41,18 @@ and ity_node =
| Ityvar of tvsymbol
| Itypur of tysymbol * ity list
| Ityapp of itysymbol * ity list * region list
(* | Itymod of tysymbol * ity *)
and region = {
reg_ity : ity;
reg_name : ident;
reg_ity : ity;
reg_ghost: bool;
reg_tag : Hashweak.tag;
}
(** regions *)
module Reg = WeakStructMake (struct
type t = region
let tag r = r.reg_tag
let tag r = r.reg_name.id_tag
end)
module Sreg = Reg.S
......@@ -62,13 +61,10 @@ module Hreg = Reg.H
module Wreg = Reg.W
let reg_equal : region -> region -> bool = (==)
let reg_hash r = Hashweak.tag_hash r.reg_tag
let reg_hash r = id_hash r.reg_name
let create_region =
let r = ref 0 in
fun ?(ghost=false) ty ->
incr r;
{ reg_ity = ty; reg_ghost = ghost; reg_tag = Hashweak.create_tag !r }
let create_region id ?(ghost=false) ty =
{ reg_name = id_register id; reg_ity = ty; reg_ghost = ghost }
(* value type symbols *)
......@@ -99,8 +95,6 @@ module Hsity = Hashcons.Make (struct
| Ityapp (s1,l1,r1), Ityapp (s2,l2,r2) ->
its_equal s1 s2 && List.for_all2 ity_equal l1 l2
&& List.for_all2 reg_equal r1 r2
(* | Itymod (s1, ity1), Itymod (s2, ity2) -> *)
(* ts_equal s1 s2 && ity_equal ity1 ity2 *)
| _ ->
false
......@@ -110,8 +104,6 @@ module Hsity = Hashcons.Make (struct
| Ityapp (s,tl,rl) ->
Hashcons.combine_list reg_hash
(Hashcons.combine_list ity_hash (its_hash s) tl) rl
(* | Itymod (ts, ity) -> *)
(* Hashcons.combine (ts_hash ts) (ity_hash ity) *)
let tag n ity = { ity with ity_tag = Hashweak.create_tag n }
end)
......@@ -134,7 +126,6 @@ let mk_ity n = {
let ity_var n = Hsity.hashcons (mk_ity (Ityvar n))
let ity_pur s tl = Hsity.hashcons (mk_ity (Itypur (s,tl)))
let ity_app s tl rl = Hsity.hashcons (mk_ity (Ityapp (s,tl,rl)))
(* let ity_mod ts ity = Hsity.hashcons (mk_ity (Itymod (ts,ity))) *)
(* generic traversal functions *)
......@@ -142,13 +133,11 @@ let ity_map fn ity = match ity.ity_node with
| Ityvar _ -> ity
| Itypur (f,tl) -> ity_pur f (List.map fn tl)
| Ityapp (f,tl,rl) -> ity_app f (List.map fn tl) rl
(* | Itymod (ts, ity) -> ity_mod ts (fn ity) *)
let ity_fold fn acc ity = match ity.ity_node with
| Ityvar _ -> acc
| Itypur (_,tl)
| Ityapp (_,tl,_) -> List.fold_left fn acc tl
(* | Itymod (_,ity) -> fn acc ity *)
let ity_all pr ity =
try ity_fold (all_fn pr) true ity with FoldSkip -> false
......@@ -156,6 +145,15 @@ let ity_all pr ity =
let ity_any pr ity =
try ity_fold (any_fn pr) false ity with FoldSkip -> true
(* symbol-wise map/fold *)
let rec ity_s_fold fn fts acc ity = match ity.ity_node with
| Ityvar _ -> acc
| Itypur (ts, tl) -> List.fold_left (ity_s_fold fn fts) (fts acc ts) tl
| Ityapp (f, tl, rl) ->
let acc = List.fold_left (ity_s_fold fn fts) (fn acc f) tl in
List.fold_left (fun acc r -> ity_s_fold fn fts acc r.reg_ity) acc rl
(* traversal functions on type variables and regions *)
let rec ity_v_map fnv fnr ity = match ity.ity_node with
......@@ -165,8 +163,6 @@ let rec ity_v_map fnv fnr ity = match ity.ity_node with
ity_pur f (List.map (ity_v_map fnv fnr) tl)
| Ityapp (f,tl,rl) ->
ity_app f (List.map (ity_v_map fnv fnr) tl) (List.map fnr rl)
(* | Itymod (ts, ity) -> *)
(* ity_mod ts (ity_v_map fnv fnr ity) *)
let rec ity_v_fold fnv fnr acc ity = match ity.ity_node with
| Ityvar v ->
......@@ -175,8 +171,6 @@ let rec ity_v_fold fnv fnr acc ity = match ity.ity_node with
List.fold_left (ity_v_fold fnv fnr) acc tl
| Ityapp (_,tl,rl) ->
List.fold_left (ity_v_fold fnv fnr) (List.fold_left fnr acc rl) tl
(* | Itymod (_, ity) -> *)
(* ity_v_fold fnv fnr acc ity *)
let ity_v_all prv prr ity =
try ity_v_fold (all_fn prv) (all_fn prr) true ity with FoldSkip -> false
......@@ -235,8 +229,6 @@ let rec ity_match s ity1 ity2 =
List.fold_left2 reg_match s r1 r2
| Itypur (s1, l1), Itypur (s2, l2) when ts_equal s1 s2 ->
List.fold_left2 ity_match s l1 l2
(* | Itymod (s1, ity1), Itymod (s2, ity2) when ts_equal s1 s2 -> *)
(* ity_match s ity1 ity2 *)
| Ityvar tv1, _ ->
{ s with ity_subst_tv = Mtv.change set tv1 s.ity_subst_tv }
| _ ->
......@@ -261,7 +253,6 @@ let rec ty_of_ity ity = match ity.ity_node with
| Ityvar v -> ty_var v
| Itypur (s,tl) -> ty_app s (List.map ty_of_ity tl)
| Ityapp (s,tl,_) -> ty_app s.its_pure (List.map ty_of_ity tl)
(* | Itymod (_,ity) -> ty_of_ity ity *)
let rec ity_of_ty ty = match ty.ty_node with
| Tyvar v -> ity_var v
......@@ -289,12 +280,6 @@ let ity_app s tl rl =
| None ->
ity_app s tl rl
(* let rec ity_unmod ity = match ity.ity_node with *)
(* | Ityvar _ -> ity *)
(* | Itypur (s,tl) -> ity_pur s (List.map ity_unmod tl) *)
(* | Ityapp (s,tl,rl) -> ity_app s (List.map ity_unmod tl) rl *)
(* | Itymod (_,ity) -> ity_unmod ity *)
let ity_pur s tl = match s.ts_def with
| Some ty ->
let add m v t = Mtv.add v t m in
......@@ -371,7 +356,7 @@ let eff_union x y =
let ry = Mreg.diff (fun _ _ _ -> None) y.eff_renames e in
let rn = Mreg.union
(fun _ r1 r2 -> if reg_equal r1 r2 then Some r1 else None) rx ry in
let re = Mreg.inter
let re = Mreg.inter
(fun _ r1 r2 -> if reg_equal r1 r2 then None else Some ()) rx ry in
{ eff_reads = Sreg.union x.eff_reads y.eff_reads;
eff_writes = Sreg.union x.eff_writes y.eff_writes;
......@@ -381,6 +366,7 @@ let eff_union x y =
let eff_read r = { eff_empty with eff_reads = Sreg.singleton r }
let eff_write r = { eff_empty with eff_writes = Sreg.singleton r }
let eff_erase r = { eff_empty with eff_erases = Sreg.singleton r }
let eff_raise xs = { eff_empty with eff_raises = Sexn.singleton xs }
let eff_remove_raise xs e = { e with eff_raises = Sexn.remove xs e.eff_raises }
......@@ -408,6 +394,8 @@ let create_pvsymbol id ?mut ?(ghost=false) ity =
pv_ghost = ghost;
pv_mutable = mut; }
let pv_equal : pvsymbol -> pvsymbol -> bool = (==)
(* value types *)
type vty =
| VTvalue of pvsymbol
......@@ -425,18 +413,22 @@ and cty = {
and xpost = (pvsymbol * term) Mexn.t
(* smart constructors *)
let vty_value pvs = VTvalue pvs
(* let vty_arrow pvs cty = VTarrow (pvs, cty) *)
let vty_arrow x ?(pre=t_true) ?(post=t_true) ?(xpost=Mexn.empty) vty eff =
let cty = {
c_pre = pre;
let create_cty
?(pre=t_true) ?(post=t_true) ?(xpost=Mexn.empty) ?(effect=eff_empty) vty =
{ c_pre = pre;
c_vty = vty;
c_eff = eff;
c_eff = effect;
c_post = post;
c_xpost = xpost;
}
in
VTarrow (x, cty)
c_xpost = xpost; }
let vty_value pvs = VTvalue pvs
let vty_arrow x cty =
(* check that x does not appear in cty *)
let rec check = function
| VTvalue y -> if pv_equal x y then raise (DuplicateVar x.pv_vs)
| VTarrow (y, c) ->
if pv_equal x y then raise (DuplicateVar x.pv_vs); check c.c_vty
in
check cty.c_vty;
VTarrow (x, cty)
......@@ -41,12 +41,11 @@ and ity_node = private
| Ityvar of tvsymbol
| Itypur of tysymbol * ity list
| Ityapp of itysymbol * ity list * region list
(* | Itymod of tysymbol * ity *)
and region = private {
reg_name : ident;
reg_ity : ity;
reg_ghost : bool;
reg_tag : Hashweak.tag;
}
module Mits : Map.S with type key = itysymbol
......@@ -79,7 +78,7 @@ exception DuplicateRegion of region
exception UnboundRegion of region
exception InvalidRegion of region
val create_region : ?ghost:bool -> ity -> region
val create_region : preid -> ?ghost:bool -> ity -> region
val create_itysymbol :
preid -> tvsymbol list -> region list -> ity option -> itysymbol
......@@ -89,9 +88,6 @@ val ity_pur : tysymbol -> ity list -> ity
val ity_app : itysymbol -> ity list -> region list -> ity
(* erases all [Itymod] *)
(* val ity_unmod : ity -> ity *)
(* all aliases expanded, all regions removed *)
val ty_of_ity : ity -> ty
......@@ -118,9 +114,11 @@ val ity_v_any : (tvsymbol -> bool) -> (region -> bool) -> ity -> bool
(** {3 symbol-wise map/fold} *)
(** visits every symbol of the type *)
val ity_s_fold :
('a -> itysymbol -> 'a) -> ('a -> tysymbol -> 'a) -> 'a -> ity -> 'a
(*
val ity_s_map : (itysymbol -> itysymbol) -> ity -> ity
val ity_s_fold : ('a -> itysymbol -> 'a) -> 'a -> ity -> 'a
val ity_s_all : (itysymbol -> bool) -> ity -> bool
val ity_s_any : (itysymbol -> bool) -> ity -> bool
*)
......@@ -169,6 +167,7 @@ val eff_empty: effect
val eff_union: effect -> effect -> effect
val eff_read: region -> effect
val eff_write: region -> effect
val eff_erase: region -> effect
val eff_raise: xsymbol -> effect
val eff_remove_raise: xsymbol -> effect -> effect
......@@ -182,6 +181,8 @@ type pvsymbol = private {
val create_pvsymbol: preid -> ?mut:region -> ?ghost:bool -> ity -> pvsymbol
val pv_equal : pvsymbol -> pvsymbol -> bool
(* value types *)
type vty = private
| VTvalue of pvsymbol
......@@ -199,7 +200,9 @@ and cty = private {
and xpost = (pvsymbol * term) Mexn.t
(* smart constructors *)
val create_cty:
?pre:term -> ?post:term -> ?xpost:xpost -> ?effect:effect -> vty -> cty
val vty_value: pvsymbol -> vty
val vty_arrow:
pvsymbol -> ?pre:term -> ?post:term -> ?xpost:xpost -> vty -> effect -> vty
val vty_arrow: pvsymbol -> cty -> vty
theory T
use import int.Int
goal G: let x,y = (1,2) in x=y
end
theory TestPVS
use import bool.Bool
......
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