Commit 560952e5 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

program API in progress

parent 260257bc
......@@ -40,7 +40,7 @@ and vty_node =
| Vtyvar of tvsymbol
| Vtypur of tysymbol * vty list
| Vtyapp of vtysymbol * vty list * region list
| Vtymod of tysymbol * vty
(* | Vtymod of tysymbol * vty *)
and region = {
reg_ty : vty;
......@@ -90,13 +90,17 @@ module Hsvty = Hashcons.Make (struct
type t = vty
let equal vty1 vty2 = match vty1.vty_node, vty2.vty_node with
| Vtyvar n1, Vtyvar n2 -> tv_equal n1 n2
| Vtyvar n1, Vtyvar n2 ->
tv_equal n1 n2
| Vtypur (s1,l1), Vtypur (s2,l2) ->
ts_equal s1 s2 && List.for_all2 vty_equal l1 l2
| Vtyapp (s1,l1,r1), Vtyapp (s2,l2,r2) ->
vts_equal s1 s2 && List.for_all2 vty_equal l1 l2
&& List.for_all2 reg_equal r1 r2
| _ -> false
(* | Vtymod (s1, vty1), Vtymod (s2, vty2) -> *)
(* ts_equal s1 s2 && vty_equal vty1 vty2 *)
| _ ->
false
let hash vty = match vty.vty_node with
| Vtyvar v -> tv_hash v
......@@ -104,8 +108,8 @@ module Hsvty = Hashcons.Make (struct
| Vtyapp (s,tl,rl) ->
Hashcons.combine_list reg_hash
(Hashcons.combine_list vty_hash (vts_hash s) tl) rl
| Vtymod (ts, vty) ->
Hashcons.combine (ts_hash ts) (vty_hash vty)
(* | Vtymod (ts, vty) -> *)
(* Hashcons.combine (ts_hash ts) (vty_hash vty) *)
let tag n vty = { vty with vty_tag = Hashweak.create_tag n }
end)
......@@ -128,7 +132,7 @@ let mk_vty n = {
let vty_var n = Hsvty.hashcons (mk_vty (Vtyvar n))
let vty_pur s tl = Hsvty.hashcons (mk_vty (Vtypur (s,tl)))
let vty_app s tl rl = Hsvty.hashcons (mk_vty (Vtyapp (s,tl,rl)))
let vty_mod ts vty = Hsvty.hashcons (mk_vty (Vtymod (ts,vty)))
(* let vty_mod ts vty = Hsvty.hashcons (mk_vty (Vtymod (ts,vty))) *)
(* generic traversal functions *)
......@@ -136,13 +140,13 @@ let vty_map fn vty = match vty.vty_node with
| Vtyvar _ -> vty
| Vtypur (f,tl) -> vty_pur f (List.map fn tl)
| Vtyapp (f,tl,rl) -> vty_app f (List.map fn tl) rl
| Vtymod (ts, vty) -> vty_mod ts (fn vty)
(* | Vtymod (ts, vty) -> vty_mod ts (fn vty) *)
let vty_fold fn acc vty = match vty.vty_node with
| Vtyvar _ -> acc
| Vtypur (_,tl)
| Vtyapp (_,tl,_) -> List.fold_left fn acc tl
| Vtymod (_,vty) -> fn acc vty
(* | Vtymod (_,vty) -> fn acc vty *)
let vty_all pr vty =
try vty_fold (all_fn pr) true vty with FoldSkip -> false
......@@ -159,8 +163,8 @@ let rec vty_v_map fnv fnr vty = match vty.vty_node with
vty_pur f (List.map (vty_v_map fnv fnr) tl)
| Vtyapp (f,tl,rl) ->
vty_app f (List.map (vty_v_map fnv fnr) tl) (List.map fnr rl)
| Vtymod (ts, vty) ->
vty_mod ts (vty_v_map fnv fnr vty)
(* | Vtymod (ts, vty) -> *)
(* vty_mod ts (vty_v_map fnv fnr vty) *)
let rec vty_v_fold fnv fnr acc vty = match vty.vty_node with
| Vtyvar v ->
......@@ -169,8 +173,8 @@ let rec vty_v_fold fnv fnr acc vty = match vty.vty_node with
List.fold_left (vty_v_fold fnv fnr) acc tl
| Vtyapp (_,tl,rl) ->
List.fold_left (vty_v_fold fnv fnr) (List.fold_left fnr acc rl) tl
| Vtymod (_, vty) ->
vty_v_fold fnv fnr acc vty
(* | Vtymod (_, vty) -> *)
(* vty_v_fold fnv fnr acc vty *)
let vty_v_all prv prr vty =
try vty_v_fold (all_fn prv) (all_fn prr) true vty with FoldSkip -> false
......@@ -195,11 +199,67 @@ exception DuplicateRegion of region
exception UnboundRegion of region
exception InvalidRegion of region
exception RegionMismatch of region * region
exception TypeMismatch of vty * vty
let vty_equal_check ty1 ty2 =
if not (vty_equal ty1 ty2) then raise (TypeMismatch (ty1, ty2))
type vty_subst = {
vty_subst_tv: vty Mtv.t;
vty_subst_reg: region Mreg.t;
}
let vty_subst_empty = {
vty_subst_tv = Mtv.empty;
vty_subst_reg = Mreg.empty;
}
let vty_inst s vty =
vty_v_map
(fun v -> Mtv.find_default v (vty_var v) s.vty_subst_tv)
(fun r -> Mreg.find_default r r s.vty_subst_reg)
vty
let rec vty_match s vty1 vty2 =
let set = function
| None -> Some vty2
| Some vty3 as r when vty_equal vty3 vty2 -> r
| _ -> raise Exit
in
match vty1.vty_node, vty2.vty_node with
| Vtyapp (s1, l1, r1), Vtyapp (s2, l2, r2) when vts_equal s1 s2 ->
let s = List.fold_left2 vty_match s l1 l2 in
List.fold_left2 reg_match s r1 r2
| Vtypur (s1, l1), Vtypur (s2, l2) when ts_equal s1 s2 ->
List.fold_left2 vty_match s l1 l2
(* | Vtymod (s1, vty1), Vtymod (s2, vty2) when ts_equal s1 s2 -> *)
(* vty_match s vty1 vty2 *)
| Vtyvar tv1, _ ->
{ s with vty_subst_tv = Mtv.change tv1 set s.vty_subst_tv }
| _ ->
raise Exit
and reg_match s r1 r2 =
let is_new = ref false in
let set = function
| None -> is_new := true; Some r2
| Some r3 as r when reg_equal r3 r2 -> r
| _ -> raise Exit
in
let reg_map = Mreg.change r1 set s.vty_subst_reg in
let s = { s with vty_subst_reg = reg_map } in
if !is_new then vty_match s r1.reg_ty r2.reg_ty else s
let vty_match s vty1 vty2 =
try vty_match s vty1 vty2
with Exit -> raise (TypeMismatch (vty_inst s vty1, vty2))
let rec ty_of_vty vty = match vty.vty_node with
| Vtyvar v -> ty_var v
| Vtypur (s,tl) -> ty_app s (List.map ty_of_vty tl)
| Vtyapp (s,tl,_) -> ty_app s.vts_pure (List.map ty_of_vty tl)
| Vtymod (_,vty) -> ty_of_vty vty
(* | Vtymod (_,vty) -> ty_of_vty vty *)
let rec vty_of_ty ty = match ty.ty_node with
| Tyvar v -> vty_var v
......@@ -212,21 +272,26 @@ let vty_app s tl rl =
let srl = List.length s.vts_regs in
if tll <> stl then raise (BadVtyArity (s,stl,tll));
if rll <> srl then raise (BadRegArity (s,srl,rll));
let add m v t = Mtv.add v t m in
let mv = List.fold_left2 add Mtv.empty s.vts_args tl in
let add m v r = Mreg.add v r m in
let mr = List.fold_left2 add Mreg.empty s.vts_regs rl in
(* check that region types do unify *)
let sub = { vty_subst_tv = mv; vty_subst_reg = mr } in
let rmatch sub r1 r2 = vty_match sub r1.reg_ty r2.reg_ty in
ignore (List.fold_left2 rmatch sub s.vts_regs rl);
(* to instantiate def, mv and mr are enough *)
match s.vts_def with
| Some vty ->
let add m v t = Mtv.add v t m in
let mv = List.fold_left2 add Mtv.empty s.vts_args tl in
let add m v r = Mreg.add v r m in
let mr = List.fold_left2 add Mreg.empty s.vts_regs rl in
vty_full_inst mv mr vty
| None ->
vty_app s tl rl
let rec vty_unmod vty = match vty.vty_node with
| Vtyvar _ -> vty
| Vtypur (s,tl) -> vty_pur s (List.map vty_unmod tl)
| Vtyapp (s,tl,rl) -> vty_app s (List.map vty_unmod tl) rl
| Vtymod (_,vty) -> vty_unmod vty
(* let rec vty_unmod vty = match vty.vty_node with *)
(* | Vtyvar _ -> vty *)
(* | Vtypur (s,tl) -> vty_pur s (List.map vty_unmod tl) *)
(* | Vtyapp (s,tl,rl) -> vty_app s (List.map vty_unmod tl) rl *)
(* | Vtymod (_,vty) -> vty_unmod vty *)
let vty_pur s tl = match s.ts_def with
| Some ty ->
......@@ -236,15 +301,22 @@ let vty_pur s tl = match s.ts_def with
| None ->
vty_pur s tl
let create_vtysymbol name args regs def model =
let create_vtysymbol name args regs def (* model *) =
let puredef = option_map ty_of_vty def in
let purets = create_tysymbol name args puredef in
(* all regions *)
let add s v = Sreg.add_new v (DuplicateRegion v) s in
let s = List.fold_left add Sreg.empty regs in
let check r = Sreg.mem r s || raise (UnboundRegion r) in
let sregs = List.fold_left add Sreg.empty regs in
(* all type variables *)
let sargs = List.fold_right Stv.add args Stv.empty in
(* all type variables in [regs] must be in [args] *)
let check tv = Stv.mem tv sargs || raise (UnboundTypeVar tv) in
List.iter (fun r -> ignore (vty_v_all check Util.ttrue r.reg_ty)) regs;
(* all regions in [def] must be in [regs] *)
let check r = Sreg.mem r sregs || raise (UnboundRegion r) in
ignore (option_map (vty_v_all Util.ttrue check) def);
(* if a type is a model alias, expand everything on the RHS *)
let def = if model then option_map (vty_mod purets) def else def in
(* let def = if model then option_map (vty_mod purets) def else def in *)
{ vts_pure = purets;
vts_args = args;
vts_regs = regs;
......
......@@ -40,7 +40,7 @@ and vty_node = private
| Vtyvar of tvsymbol
| Vtypur of tysymbol * vty list
| Vtyapp of vtysymbol * vty list * region list
| Vtymod of tysymbol * vty
(* | Vtymod of tysymbol * vty *)
and region = private {
reg_ty : vty;
......@@ -80,7 +80,7 @@ exception InvalidRegion of region
val create_region : vty -> region
val create_vtysymbol :
preid -> tvsymbol list -> region list -> vty option -> bool -> vtysymbol
preid -> tvsymbol list -> region list -> vty option -> vtysymbol
val vty_var : tvsymbol -> vty
val vty_pur : tysymbol -> vty list -> vty
......@@ -88,7 +88,7 @@ val vty_pur : tysymbol -> vty list -> vty
val vty_app : vtysymbol -> vty list -> region list -> vty
(* erases all [Vtymod] *)
val vty_unmod : vty -> vty
(* val vty_unmod : vty -> vty *)
(* all aliases expanded, all regions removed *)
val ty_of_vty : vty -> ty
......@@ -121,15 +121,88 @@ val vty_s_map : (vtysymbol -> vtysymbol) -> vty -> vty
val vty_s_fold : ('a -> vtysymbol -> 'a) -> 'a -> vty -> 'a
val vty_s_all : (vtysymbol -> bool) -> vty -> bool
val vty_s_any : (vtysymbol -> bool) -> vty -> bool
*)
val vty_freevars : Stv.t -> vty -> Stv.t
val vty_closed : vty -> bool
val vty_pure: vty -> bool
exception RegionMismatch of region * region
exception TypeMismatch of vty * vty
val vty_match : vty Mreg.t -> vty -> vty -> vty Mreg.t
val vty_inst : vty Mreg.t -> vty -> vty
val vty_freevars : Srv.t -> vty -> Srv.t
val vty_closed : vty -> bool
type vty_subst = private {
vty_subst_tv: vty Mtv.t;
vty_subst_reg: region Mreg.t;
}
val vty_subst_empty: vty_subst
val vty_match : vty_subst -> vty -> vty -> vty_subst
val vty_equal_check : vty -> vty -> unit
*)
(*****
(** computation types (with effects) *)
(* exception symbols *)
type xsymbol = private {
xs_id : ident;
xs_vty: vty; (* closed and pure *)
}
val create_xsymbol: preid -> vty -> xsymbol
module Mexn: Map.S with type key = xsymbol
module Sexn: Mexn.Set
(* effects *)
type effect = private {
eff_reads: Sreg.t;
eff_writes: Sreg.t;
eff_erases: Sreg.t;
eff_renames: region Mreg.t; (* if r1->r2 then r1 appears in ty(r2) *)
eff_raises: Sexn.t;
}
val eff_empty: effect
val eff_union: effect -> effect -> effect
val eff_read: region -> effect
val eff_write: region -> effect
val eff_raise: xsymbol -> effect
val eff_remove_raise: xsymbol -> effect -> effect
(* program symbols *)
type psymbol = private {
p_vs: vsymbol;
p_vty: vty;
p_ghost: bool;
p_mutable: region option;
}
val create_psymbol: ?mut:region -> ?ghost:bool -> vty -> psymbol
(* expression types *)
type ety = private
| Evalue of psymbol
| Earrow of psymbol * cty
(* computation types *)
and cty = private {
c_pre: fmla;
c_ety: ety;
c_eff: effect;
c_post: fmla;
c_xpost: xpost;
}
and xpost = (psymbol * fmla) Xmap.t
(* smart constructors *)
val ety_value: psymbol -> ety
val ety_arrow: psymbol -> cty -> ety
val create_cty: ?pre:fmla -> ?post:post -> ?xpost:xpost -> ety -> effect -> cty
****)
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