syntax for ghost fields and private/abstract types

share/emacs/why.el

@@ -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)
    )

share/lang/why.lang

@@ -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>

src/parser/lexer.mll

@@ -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;

src/parser/parser.mly

@@ -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     {}

src/parser/ptree.ml

@@ -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;
 }
 

src/parser/typing.ml

@@ -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) *)

src/programs/pgm_typing.ml

@@ -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

tests/test-pgm-jcf.mlw

+module M0
+  type t = private int
+end
+
 
 (*
 module ExcepAndRec