Commit 09a28bc9 authored by Guillaume Melquiond's avatar Guillaume Melquiond
parents 3b1cba98 5baf128f
......@@ -157,6 +157,9 @@ why3.conf
/plugins/tptp/tptp_parser.mli
/plugins/tptp/tptp_parser.output
# /drivers
/drivers/coq-realizations.aux
# /tests/
/tests/test-jcf/
/tests/test-pgm-jcf/
......
......@@ -29,7 +29,7 @@
;; Note: comment font-lock is guaranteed by suitable syntax entries
'("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face)
'("{}\\|{[^|]\\([^}]*\\)}" . font-lock-type-face)
`(,(why-regexp-opt '("use" "clone" "namespace" "import" "export" "inductive" "external" "constant" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "model" "abstract" "reads" "writes" "raises")) . font-lock-builtin-face)
`(,(why-regexp-opt '("use" "clone" "namespace" "import" "export" "inductive" "external" "constant" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "model" "abstract" "private" "reads" "writes" "raises")) . font-lock-builtin-face)
`(,(why-regexp-opt '("any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "invariant" "variant" "for" "to" "downto" "do" "done" "label" "loop" "assert" "absurd" "assume" "check" "ghost" "try" "with" "theory" "uses" "module")) . font-lock-keyword-face)
; `(,(why-regexp-opt '("unit" "bool" "int" "float" "prop" "array")) . font-lock-type-face)
)
......
......@@ -144,6 +144,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
<match>\]</match>
</context>
<context id="keywords" style-ref="meta-keyword">
<keyword>abstract</keyword>
<keyword>axiom</keyword>
<keyword>clone</keyword>
<keyword>end</keyword>
......@@ -152,12 +153,14 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
<keyword>constant</keyword>
<keyword>function</keyword>
<keyword>goal</keyword>
<keyword>ghost</keyword>
<keyword>import</keyword>
<keyword>inductive</keyword>
<keyword>lemma</keyword>
<keyword>module</keyword>
<keyword>namespace</keyword>
<keyword>predicate</keyword>
<keyword>private</keyword>
<keyword>theory</keyword>
<keyword>type</keyword>
<keyword>use</keyword>
......
......@@ -86,12 +86,13 @@
"exception", EXCEPTION;
"for", FOR;
"fun", FUN;
(* "ghost", GHOST; *)
"ghost", GHOST;
"invariant", INVARIANT;
"loop", LOOP;
"model", MODEL;
"module", MODULE;
"mutable", MUTABLE;
"private", PRIVATE;
"raise", RAISE;
"raises", RAISES;
"reads", READS;
......
......@@ -211,7 +211,7 @@ end
%token ABSTRACT ABSURD ANY ASSERT ASSUME BEGIN CHECK DO DONE DOWNTO
%token EXCEPTION FOR
%token FUN INVARIANT LOOP MODEL MODULE MUTABLE RAISE
%token FUN GHOST INVARIANT LOOP MODEL MODULE MUTABLE PRIVATE RAISE
%token RAISES READS REC TO TRY VAL VARIANT WHILE WRITES
/* symbols */
......@@ -421,9 +421,9 @@ list1_type_decl:
type_decl:
| lident labels type_args typedefn
{ let model, def = $4 in
{ let model, vis, def = $4 in
{ td_loc = floc (); td_ident = add_lab $1 $2;
td_params = $3; td_model = model; td_def = def } }
td_params = $3; td_model = model; td_vis = vis; td_def = def } }
;
type_args:
......@@ -432,11 +432,20 @@ type_args:
;
typedefn:
| /* epsilon */ { false, TDabstract }
| equal_model primitive_type { $1, TDalias $2 }
| equal_model typecases { $1, TDalgebraic $2 }
| equal_model BAR typecases { $1, TDalgebraic $3 }
| equal_model record_type { $1, TDrecord $2 }
| /* epsilon */ { false, Public, TDabstract }
| equal_model visibility typecases { $1, $2, TDalgebraic $3 }
| equal_model visibility BAR typecases { $1, $2, TDalgebraic $4 }
| equal_model visibility record_type { $1, $2, TDrecord $3 }
/* abstract/private is not allowed for alias type */
| equal_model visibility primitive_type
{ if $2 <> Public then Loc.error ~loc:(floc_i 2) Parsing.Parse_error;
$1, Public, TDalias $3 }
;
visibility:
| /* epsilon */ { Public }
| PRIVATE { Private }
| ABSTRACT { Abstract }
;
equal_model:
......@@ -453,9 +462,21 @@ list1_record_field:
| list1_record_field SEMICOLON record_field { $3 :: $1 }
;
field_modifiers:
| /* epsilon */ { false, false }
| MUTABLE { true, false }
| GHOST { false, true }
| GHOST MUTABLE { true, true }
| MUTABLE GHOST { true, true }
;
record_field:
| opt_mutable lident labels COLON primitive_type
{ floc (), $1, add_lab $2 $3, $5 }
| field_modifiers lident labels COLON primitive_type
{ { f_loc = floc ();
f_ident = add_lab $2 $3;
f_mutable = fst $1;
f_ghost = snd $1;
f_pty = $5 } }
;
typecases:
......@@ -1054,11 +1075,6 @@ lident_rich_pgm:
{ mk_id (mixfix "[]<-") (floc ()) }
;
opt_mutable:
| /* epsilon */ { false }
| MUTABLE { true }
;
opt_semicolon:
| /* epsilon */ {}
| SEMICOLON {}
......
......@@ -110,19 +110,28 @@ type clone_subst =
| CSlemma of loc * qualid
| CSgoal of loc * qualid
type is_mutable = bool
type field = {
f_loc : loc;
f_ident : ident;
f_pty : pty;
f_mutable : bool;
f_ghost : bool
}
type type_def =
| TDabstract
| TDalias of pty
| TDalgebraic of (loc * ident * param list) list
| TDrecord of (loc * is_mutable * ident * pty) list
| TDrecord of field list
type visibility = Public | Private | Abstract
type type_decl = {
td_loc : loc;
td_ident : ident;
td_params : ident list;
td_model : bool;
td_vis : visibility;
td_def : type_def;
}
......
......@@ -912,12 +912,16 @@ let add_types dl th =
let prepare_typedef td =
if td.td_model then
errorm ~loc:td.td_loc "model types are not allowed in the logic";
if td.td_vis <> Public then
errorm ~loc:td.td_loc "a logic type cannot be abstract or private";
match td.td_def with
| TDabstract | TDalgebraic _ | TDalias _ ->
td
| TDrecord fl ->
let field (loc, mut, id, ty) =
let field { f_loc = loc; f_ident = id; f_pty = ty;
f_mutable = mut; f_ghost = gh } =
if mut then errorm ~loc "a logic record field cannot be mutable";
if gh then errorm ~loc "a logic record field cannot be ghost";
Some id, ty
in
(* constructor for type t is "mk t" (and not String.capitalize t) *)
......
......@@ -1991,8 +1991,8 @@ let check_type_vars ~loc vars ty =
check ty
let make_immutable_type td =
let td = { td with td_model = false } in
let make_immutable_field (loc, _, id, ty) = (loc, false, id, ty) in
let td = { td with td_model = false; td_vis = Public } in
let make_immutable_field f = { f with f_mutable = false; f_ghost = false } in
match td.td_def with
(* | TDrecord [_, _, _, ty] -> (\* singleton record *\) *)
(* { td with td_def = TDalias ty } *)
......@@ -2045,7 +2045,7 @@ let add_types uc dl =
| TDrecord fl ->
let nf = List.length fl in
List.fold_left
(fun n (loc, mut, _, ty) ->
(fun n { f_loc=loc; f_mutable=mut; f_pty=ty } ->
if mut && nf = 1 then Hashtbl.add singletons x ();
let nty = nregions_of_type ty in
if mut then begin
......@@ -2119,17 +2119,19 @@ let add_types uc dl =
let constructor (loc, id, pl) = (loc, id, List.map add pl) in
TDalgebraic (List.map constructor cl)
| TDrecord fl ->
let add i (loc, mut, id, ty) =
let add i ({ f_mutable=mut; f_ident=id; f_pty=ty } as f) =
add_projection id;
if mut then begin
let j, _ = region () in
if effect then Hashtbl.add mutable_field (x, i) j
end;
(loc, false, id, add_regions_to_type ty)
{ f with f_mutable = false; f_ghost = false;
f_pty = add_regions_to_type ty }
in
TDrecord (list_mapi add fl)
in
{ d with td_params = params; td_model = false; td_def = def }
{ d with
td_params = params; td_model = false; td_vis = Public; td_def = def }
in
let dli = List.map (add_regions ~effect:false) dl in
let uc = Pgm_module.add_impure_pdecl (Ptree.TypeDecl dli) uc in
......
......@@ -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] *)