syntax for mutable types

parent 97c25a01
......@@ -63,7 +63,9 @@
"label", LABEL;
"let", LET;
"match", MATCH;
"model", MODEL;
"module", MODULE;
"mutable", MUTABLE;
"namespace", NAMESPACE;
"not", NOT;
"of", OF;
......
......@@ -13,12 +13,14 @@ module Mnm = Mstr
type namespace = {
ns_pr : psymbol Mnm.t; (* program symbols *)
ns_ex : esymbol Mnm.t; (* exceptions*)
ns_mt : mtsymbol Mnm.t; (* mutable types *)
ns_ns : namespace Mnm.t; (* inner namespaces *)
}
let empty_ns = {
ns_pr = Mnm.empty;
ns_ex = Mnm.empty;
ns_mt = Mnm.empty;
ns_ns = Mnm.empty;
}
......@@ -38,6 +40,7 @@ let rec merge_ns chk ns1 ns2 =
let fusion _ ns1 ns2 = Some (merge_ns chk ns1 ns2) in
{ ns_pr = ns_union pr_equal chk ns1.ns_pr ns2.ns_pr;
ns_ex = ns_union ls_equal chk ns1.ns_ex ns2.ns_ex;
ns_mt = ns_union mt_equal chk ns1.ns_mt ns2.ns_mt;
ns_ns = Mnm.union fusion ns1.ns_ns ns2.ns_ns; }
let nm_add chk x ns m = Mnm.change x (function
......@@ -50,9 +53,11 @@ let ns_add eq chk x v m = Mnm.change x (function
let pr_add = ns_add pr_equal
let ex_add = ns_add ls_equal
let mt_add = ns_add mt_equal
let add_pr chk x ts ns = { ns with ns_pr = pr_add chk x ts ns.ns_pr }
let add_ex chk x ls ns = { ns with ns_ex = ex_add chk x ls ns.ns_ex }
let add_mt chk x mt ns = { ns with ns_mt = mt_add chk x mt ns.ns_mt }
let add_ns chk x nn ns = { ns with ns_ns = nm_add chk x nn ns.ns_ns }
let rec ns_find get_map ns = function
......@@ -62,6 +67,7 @@ let rec ns_find get_map ns = function
let ns_find_pr = ns_find (fun ns -> ns.ns_pr)
let ns_find_ex = ns_find (fun ns -> ns.ns_ex)
let ns_find_mt = ns_find (fun ns -> ns.ns_mt)
let ns_find_ns = ns_find (fun ns -> ns.ns_ns)
(* modules under construction *)
......@@ -130,6 +136,9 @@ let add_psymbol ps uc =
let add_esymbol ls uc =
add_symbol add_ex ls.ls_name ls uc
let add_mtsymbol mt uc =
add_symbol add_mt mt.mt_name mt uc
let add_decl d uc =
{ uc with uc_decls = d :: uc.uc_decls }
......
......@@ -9,11 +9,13 @@ module Mnm : Map.S with type key = string
type namespace = private {
ns_pr : psymbol Mnm.t; (* program symbols *)
ns_ex : esymbol Mnm.t; (* exception symbols *)
ns_mt : mtsymbol Mnm.t; (* mutable types *)
ns_ns : namespace Mnm.t; (* inner namespaces *)
}
val ns_find_pr : namespace -> string list -> psymbol
val ns_find_ex : namespace -> string list -> esymbol
val ns_find_mt : namespace -> string list -> mtsymbol
val ns_find_ns : namespace -> string list -> namespace
(** a module under construction *)
......@@ -44,6 +46,7 @@ exception ClashSymbol of string
val add_psymbol : psymbol -> uc -> uc
val add_esymbol : esymbol -> uc -> uc
val add_mtsymbol : mtsymbol -> uc -> uc
val add_decl : Pgm_ttree.decl -> uc -> uc
val add_logic_decl : Decl.decl -> uc -> uc
......
......@@ -118,7 +118,7 @@
%token ABSURD AND ANY AS ASSERT ASSUME BEGIN CHECK DO DONE DOWNTO ELSE END
%token EXCEPTION EXPORT FOR
%token FUN GHOST IF IMPORT IN INVARIANT LABEL LET MATCH MODULE
%token FUN GHOST IF IMPORT IN INVARIANT LABEL LET MATCH MODEL MODULE MUTABLE
%token NAMESPACE NOT OF PARAMETER
%token RAISE RAISES READS REC
%token THEN TO TRY TYPE USE VARIANT WHILE WITH WRITES
......@@ -234,6 +234,8 @@ decl:
{ $3 }
| NAMESPACE opt_import uident list0_decl END
{ Dnamespace ($3, $2, $4) }
| MUTABLE TYPE lident type_args model
{ Dmutable_type ($3, $4, $5) }
;
use:
......@@ -254,6 +256,20 @@ opt_import:
| IMPORT { true }
;
type_args:
| /* epsilon */ { [] }
| type_var type_args { $1 :: $2 }
;
model:
| /* epsilon */ { None }
| MODEL pure_type { Some $2 }
;
type_var:
| QUOTE ident { $2 }
;
list1_recfun_sep_and:
| recfun { [ $1 ] }
| recfun AND list1_recfun_sep_and { $1 :: $3 }
......
......@@ -110,6 +110,7 @@ type decl =
(* modules *)
| Duse of qualid * Ptree.imp_exp * (*as:*) ident option
| Dnamespace of ident * (* import: *) bool * decl list
| Dmutable_type of ident * ident list * Ptree.pty option
type module_ = {
mod_name : ident;
......
......@@ -68,6 +68,20 @@ let create_psymbol id v =
type esymbol = lsymbol
type mtsymbol = {
mt_name : ident;
mt_args : tvsymbol list;
mt_model : ty option;
}
let create_mtsymbol name args model = {
mt_name = id_register name;
mt_args = args;
mt_model = model;
}
let mt_equal = (==)
(* misc. functions *)
let v_result ty = create_vsymbol (id_fresh "result") ty
......
......@@ -45,6 +45,16 @@ val create_psymbol : preid -> type_v -> psymbol
type esymbol = lsymbol
type mtsymbol = private {
mt_name : ident;
mt_args : tvsymbol list;
mt_model : ty option;
}
val create_mtsymbol : preid -> tvsymbol list -> ty option -> mtsymbol
val mt_equal : mtsymbol -> mtsymbol -> bool
(* program types -> logic types *)
val ts_arrow : tysymbol
......
......@@ -1394,6 +1394,8 @@ let rec decl ~wp env penv lmod uc = function
let uc = List.fold_left (decl ~wp env penv lmod) uc dl in
begin try close_namespace uc import (Some id.id)
with ClashSymbol s -> errorm ~loc "clash with previous symbol %s" s end
| Pgm_ptree.Dmutable_type _ ->
assert false (*TODO*)
(*
Local Variables:
......
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