From 6e11c32e6dba873e3afa4344573a53d618645323 Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Sun, 23 Jan 2011 22:32:23 +0100 Subject: [PATCH] programs: abstract types --- modules/string.mlw | 24 +++++++++++++++ share/emacs/why.el | 2 +- src/parser/lexer.mll | 1 + src/parser/parser.pre.mly | 7 +++-- src/parser/ptree.ml | 2 +- src/programs/TODO | 2 ++ src/programs/pgm_types.ml | 60 +++++++++++++++++++++----------------- src/programs/pgm_types.mli | 18 +++++++----- src/programs/pgm_typing.ml | 4 +-- src/programs/pgm_wp.ml | 5 +++- tests/test-pgm-jcf.mlw | 7 ++--- 11 files changed, 86 insertions(+), 46 deletions(-) create mode 100644 modules/string.mlw diff --git a/modules/string.mlw b/modules/string.mlw new file mode 100644 index 000000000..d124db646 --- /dev/null +++ b/modules/string.mlw @@ -0,0 +1,24 @@ + +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 diff --git a/share/emacs/why.el b/share/emacs/why.el index b120ce355..5b1c9f419 100644 --- a/share/emacs/why.el +++ b/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) ) diff --git a/src/parser/lexer.mll b/src/parser/lexer.mll index 89808928a..db1152e31 100644 --- a/src/parser/lexer.mll +++ b/src/parser/lexer.mll @@ -76,6 +76,7 @@ "use", USE; "with", WITH; (* programs *) + "abstract", ABSTRACT; "absurd", ABSURD; "any", ANY; "assert", ASSERT; diff --git a/src/parser/parser.pre.mly b/src/parser/parser.pre.mly index ab334d516..5288bd11a 100644 --- a/src/parser/parser.pre.mly +++ b/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: diff --git a/src/parser/ptree.ml b/src/parser/ptree.ml index 8ea6ac6c3..8a2a5e640 100644 --- a/src/parser/ptree.ml +++ b/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; diff --git a/src/programs/TODO b/src/programs/TODO index 3ec9a270a..c98945b9f 100644 --- a/src/programs/TODO +++ b/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) diff --git a/src/programs/pgm_types.ml b/src/programs/pgm_types.ml index bbfad8fb8..7241fe5e8 100644 --- a/src/programs/pgm_types.ml +++ b/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 -> diff --git a/src/programs/pgm_types.mli b/src/programs/pgm_types.mli index 79ec0350c..d67675b3e 100644 --- a/src/programs/pgm_types.mli +++ b/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 diff --git a/src/programs/pgm_typing.ml b/src/programs/pgm_typing.ml index 4ac5dd569..51e2eee07 100644 --- a/src/programs/pgm_typing.ml +++ b/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 diff --git a/src/programs/pgm_wp.ml b/src/programs/pgm_wp.ml index 9328b6371..5d79777e8 100644 --- a/src/programs/pgm_wp.ml +++ b/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) diff --git a/tests/test-pgm-jcf.mlw b/tests/test-pgm-jcf.mlw index 0db54bc80..8f76100a3 100644 --- a/tests/test-pgm-jcf.mlw +++ b/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 -- GitLab