programs: abstract types

modules/string.mlw

+
+module Char
+
+  abstract type char model int
+
+end
+
+module String
+
+  use import int.Int
+  use import module Char
+  use array.ArrayLength as S
+
+  mutable type string model S.t int char
+
+  parameter get : s:string -> i:int ->
+    { 0 <= i < S.length s } char reads s { result = S.get s i }
+
+  parameter set : s:string -> i:int -> v:char ->
+    { 0 <= i < S.length s } unit writes s { s = S.set (old s) i v }
+
+  parameter length : s:string -> {} int reads s { result = S.length s }
+
+end

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" "logic" "parameter" "exception" "axiom" "lemma" "goal" "type" "mutable" "model")) . font-lock-builtin-face)
+   `(,(why-regexp-opt '("use" "clone" "namespace" "import" "export" "inductive" "external" "logic" "parameter" "exception" "axiom" "lemma" "goal" "type" "mutable" "model" "abstract")) . font-lock-builtin-face)
    `(,(why-regexp-opt '("and" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "invariant" "variant" "for" "to" "downto" "do" "done" "label" "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)
    )

src/parser/lexer.mll

@@ -76,6 +76,7 @@
 	"use", USE;
 	"with", WITH;
 	(* programs *)
+	"abstract", ABSTRACT;
 	"absurd", ABSURD;
 	"any", ANY;
 	"assert", ASSERT;

src/parser/parser.pre.mly

@@ -157,7 +157,8 @@
 
 /* program keywords */
 
-%token ABSURD ANY ASSERT ASSUME BEGIN CHECK DO DONE DOWNTO EXCEPTION FOR 
+%token ABSTRACT ABSURD ANY ASSERT ASSUME BEGIN CHECK DO DONE DOWNTO 
+%token EXCEPTION FOR 
 %token FUN GHOST INVARIANT LABEL MODEL MODULE MUTABLE PARAMETER RAISE 
 %token RAISES READS REC TO TRY VARIANT WHILE WRITES
 
@@ -871,8 +872,10 @@ program_decl:
     { $2 }
 | NAMESPACE namespace_import uident list0_program_decl END
     { Dnamespace ($3, $2, $4) }
+| ABSTRACT TYPE lident type_args model
+    { Dmodel_type (false, $3, $4, $5) }
 | MUTABLE TYPE lident type_args model
-    { Dmutable_type ($3, $4, $5) }
+    { Dmodel_type (true, $3, $4, $5) }
 ;
 
 use_module:

src/parser/ptree.ml

@@ -230,7 +230,7 @@ type program_decl =
   (* modules *)
   | Duse    of qualid * imp_exp * (*as:*) ident option
   | Dnamespace of ident * (* import: *) bool * program_decl list
-  | Dmutable_type of ident * ident list * pty option
+  | Dmodel_type of bool * ident * ident list * pty option
 
 type module_ = {
   mod_name   : ident;

src/programs/TODO

@@ -11,4 +11,6 @@ o fixed precedence of label (label L: e) wrt sequence (e ; e)
 
 o misfix _[_] and _[_] := _ for arrays (both in logic and programs)
 
+o model types (abstract but not mutable)
+  abstract types (no model)
 

src/programs/pgm_types.ml

@@ -7,55 +7,63 @@ open Theory
 open Term
 open Decl
 
-(* mutable types *)
+(* model types *)
 
 type mtsymbol = {
-  mt_name  : ident;
-  mt_args  : tvsymbol list;
-  mt_model : ty option;
-  mt_abstr : tysymbol;
+  mt_name   : ident;
+  mt_args   : tvsymbol list;
+  mt_model  : ty option;
+  mt_abstr  : tysymbol;
+  mt_mutable: bool;
 }
 
 let mt_equal : mtsymbol -> mtsymbol -> bool = (==)
 
-let mutable_types = Hts.create 17
+let model_types = Hts.create 17
 
-let create_mtsymbol name args model = 
+let create_mtsymbol ~mut name args model = 
   let id = id_register name in
   let ts = create_tysymbol name args None in
   let mt = 
     { mt_name  = id;
       mt_args  = args;
       mt_model = model; 
-      mt_abstr = ts; }
+      mt_abstr = ts;
+      mt_mutable = mut; }
   in
-  Hts.add mutable_types ts mt;
+  Hts.add model_types ts mt;
   mt
 
-let is_mutable_ts = Hts.mem mutable_types
+let is_mutable_ts ts = 
+  try (Hts.find model_types ts).mt_mutable with Not_found -> false
 
 let is_mutable_ty ty = match ty.ty_node with
   | Ty.Tyapp (ts, _) -> is_mutable_ts ts
   | Ty.Tyvar _ -> false
 
-exception NotMutable
+exception NotModelType
 
 let get_mtsymbol ts = 
-  try Hts.find mutable_types ts with Not_found -> raise NotMutable
-
-let model_type ty = match ty.ty_node with
-  | Tyapp (ts, tyl) when Hts.mem mutable_types ts ->
-      let mt = Hts.find mutable_types ts in
-      begin match mt.mt_model with
-	| None -> 
-	    ty
-	| Some ty ->
-	    let add mtv tv ty = Mtv.add tv ty mtv in
-	    let mtv = List.fold_left2 add Mtv.empty mt.mt_args tyl in
-	    ty_inst mtv ty
+  try Hts.find model_types ts with Not_found -> raise NotModelType
+
+let rec model_type ty = match ty.ty_node with
+  | Tyapp (ts, tyl) ->
+      let tyl = List.map model_type tyl in
+      begin try
+	let mt = Hts.find model_types ts in
+	begin match mt.mt_model with
+	  | None -> 
+	      ty
+	  | Some ty ->
+	      let add mtv tv ty = Mtv.add tv ty mtv in
+	      let mtv = List.fold_left2 add Mtv.empty mt.mt_args tyl in
+	      model_type (ty_inst mtv ty) (* FIXME: could be optimized? *)
+	end
+      with Not_found ->
+	ty_app ts tyl
       end
-  | Tyvar _ | Tyapp _ -> 
-      raise NotMutable
+  | Tyvar _ ->
+      ty
 
 (* types *)
 
@@ -185,7 +193,7 @@ end = struct
 
   (* purify: turns program types into logic types *)
 
-  let purify ty = try model_type ty with NotMutable -> ty
+  let purify ty = model_type ty
 
   let rec uncurry_type ?(logic=false) = function
     | Tpure ty when not logic ->

src/programs/pgm_types.mli

@@ -7,23 +7,25 @@ open Theory
 open Term
 open Decl
 
-(* mutable type symbols *)
+(* model type symbols *)
 
 type mtsymbol = private {
-  mt_name  : ident;
-  mt_args  : tvsymbol list;
-  mt_model : ty option;
-  mt_abstr : tysymbol;
+  mt_name   : ident;
+  mt_args   : tvsymbol list;
+  mt_model  : ty option;
+  mt_abstr  : tysymbol;
+  mt_mutable: bool;
 }
 
-val create_mtsymbol : preid -> tvsymbol list -> ty option -> mtsymbol
+val create_mtsymbol : 
+  mut:bool -> preid -> tvsymbol list -> ty option -> mtsymbol
 
 val mt_equal : mtsymbol -> mtsymbol -> bool
 
-exception NotMutable
+exception NotModelType
 
 val get_mtsymbol : tysymbol -> mtsymbol
-  (** raises [NotMutable] if [ts] is not a mutable type *)
+  (** raises [NotModelType] if [ts] is not a model type *)
 
 val is_mutable_ts : tysymbol -> bool
 val is_mutable_ty : ty       -> bool

src/programs/pgm_typing.ml

@@ -1604,7 +1604,7 @@ 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
-  | Ptree.Dmutable_type (id, args, model) ->
+  | Ptree.Dmodel_type (mut, id, args, model) ->
       let loc = id.id_loc in
       let id = id_user id.id loc in
       let denv = Typing.create_denv (theory_uc uc) in
@@ -1619,7 +1619,7 @@ let rec decl ~wp env penv lmod uc = function
 	  model 
       in
       option_iter (check_type_vars ~loc args) model;
-      let mt = create_mtsymbol id args model in
+      let mt = create_mtsymbol ~mut id args model in
       let uc = 
 	let d = Decl.create_ty_decl [mt.mt_abstr, Decl.Tabstract] in
 	Pgm_module.add_logic_decl d uc 

src/programs/pgm_wp.ml

@@ -166,7 +166,10 @@ let abstract_wp env ef (q',ql') (q,ql) =
   in
   let f =
     let res, f = q and res', f' = q' in
-    let f' = f_subst (subst1 res' (t_var res)) f' in
+    let f' = 
+      if is_arrow_ty res'.vs_ty then f' 
+      else f_subst (subst1 res' (t_var res)) f' 
+    in
     quantify_res f' f (Some res)
   in
   wp_ands (f :: List.map2 quantify_h ql' ql)

tests/test-pgm-jcf.mlw

@@ -2,13 +2,10 @@
 module P
 
   use import int.Int
-  use import module stdlib.Ref
+  use import module string.String
 
-  let f1 () (a : ref int) = !a
+  let foo (s:string) = { S.length s = 1 } get s 0 { true }
 
-  parameter r : ref int
-
-  let f2 () = f1 () r
 
 end