diff --git a/Makefile.in b/Makefile.in index b81eb7559ef399aa0f44eced86c1686f7d0d1032..5616bf41540f6e7d357d058d953bdd25b38b41f1 100644 --- a/Makefile.in +++ b/Makefile.in @@ -174,7 +174,7 @@ testl: bin/whyl.byte # programs ########## -PGM_CMO := pgm_parser.cmo pgm_lexer.cmo pgm_main.cmo +PGM_CMO := pgm_parser.cmo pgm_lexer.cmo pgm_typing.cmo pgm_main.cmo PGM_CMO := $(addprefix src/programs/, $(PGM_CMO)) WHYL_CMO = $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) $(DRIVER_CMO)\ diff --git a/lib/emacs/why.el b/lib/emacs/why.el index 2ba95ac9512e98dea6ade4b58c1a4457b7f26070..79f492c0b937ff429eed876679b77afa04335970 100644 --- a/lib/emacs/why.el +++ b/lib/emacs/why.el @@ -29,7 +29,7 @@ '("(\\*\\([^*]\\|\\*[^)]\\)*\\*)" . 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")) . font-lock-builtin-face) - `(,(why-regexp-opt '("match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "invariant" "variant" "do" "done" "label" "assert" "assume" "check" "ghost" "try" "with" "theory" "uses")) . font-lock-keyword-face) + `(,(why-regexp-opt '("match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "invariant" "variant" "do" "done" "assert" "assume" "check" "ghost" "try" "with" "theory" "uses")) . font-lock-keyword-face) ; `(,(why-regexp-opt '("unit" "bool" "int" "float" "prop" "array")) . font-lock-type-face) ) "Minimal highlighting for Why mode") diff --git a/lib/prelude/prelude.why b/lib/prelude/prelude.why index ef67f7997acdb3341fa9bf7c48bc8fd35d7a59ea..e12d0519af27c198bb6f2eb9c8cb54397f5f3131 100644 --- a/lib/prelude/prelude.why +++ b/lib/prelude/prelude.why @@ -136,7 +136,21 @@ theory Set end +theory Programs + logic old('a) : 'a + + type label + + logic at('a, label) : 'a + + type 'a ref + + logic (!_)('a ref) : 'a + + logic ref('a) : 'a ref + +end (* Local Variables: diff --git a/src/printer/smt.mli b/src/printer/smt.mli index 6ba5bcfe8d71e48303454e87e059b555e2a24ed4..81fccfe9c9422316b52813ab27a2d15c31f67db3 100644 --- a/src/printer/smt.mli +++ b/src/printer/smt.mli @@ -16,3 +16,4 @@ (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) (* *) (**************************************************************************) + diff --git a/src/programs/pgm_lexer.mll b/src/programs/pgm_lexer.mll index 43a4ae89fb84ed2cf4a1043c8e079c5d206c3054..a03f7f6bb483ccb583de22e10d3476c983bda917 100644 --- a/src/programs/pgm_lexer.mll +++ b/src/programs/pgm_lexer.mll @@ -148,6 +148,8 @@ rule token = parse { COLON } | ";" { SEMICOLON } + | "!" + { BANG } | ":=" { COLONEQUAL } | "->" @@ -158,7 +160,7 @@ rule token = parse { OP0 s } | "+" | "-" as c { OP2 (String.make 1 c) } - | "*" | "/" | "%" | "!" as c + | "*" | "/" | "%" as c { OP3 (String.make 1 c) } | "@" { AT } diff --git a/src/programs/pgm_main.ml b/src/programs/pgm_main.ml index b986455eebfa86ef3de49b656608cdac9ed79c32..813539c29fda557f689b8508cb00e2b020758c65 100644 --- a/src/programs/pgm_main.ml +++ b/src/programs/pgm_main.ml @@ -69,7 +69,7 @@ let type_file file = List.fold_left (fun uc d -> match d with | Dlogic dl -> List.fold_left (Typing.add_decl env Mnm.empty) uc dl - | Dcode _ -> uc) + | Dcode (id, e) -> ignore (Pgm_typing.code id e); uc) uc p in () diff --git a/src/programs/pgm_parser.mly b/src/programs/pgm_parser.mly index 242440959cf15056a9bab33048ab9b7a3fa2518f..8659d8d9b03d54813f54103f2b216fc993f275ad 100644 --- a/src/programs/pgm_parser.mly +++ b/src/programs/pgm_parser.mly @@ -96,7 +96,7 @@ /* symbols */ %token UNDERSCORE QUOTE COMMA LEFTPAR RIGHTPAR COLON SEMICOLON -%token COLONEQUAL ARROW EQUAL AT DOT LEFTSQ RIGHTSQ +%token COLONEQUAL ARROW EQUAL AT DOT LEFTSQ RIGHTSQ BANG %token LEFTBLEFTB RIGHTBRIGHTB BAR BARBAR AMPAMP BIGARROW %token EOF @@ -234,12 +234,11 @@ expr: { mk_expr (Ewhile ($2, $4, $5)) } ; -/* FIXME: prefix operators should be part of simple_expr - otherwise we can't parse "f !x" */ - simple_expr: | constant { mk_expr (Econstant $1) } +| BANG expr + { mk_prefix "!" $2 } | lqualid { mk_expr (Eident $1) } | LEFTPAR expr RIGHTPAR diff --git a/src/programs/pgm_typing.ml b/src/programs/pgm_typing.ml new file mode 100644 index 0000000000000000000000000000000000000000..1bf319dc74491e1ba695caeb3f25f39810b9f72f --- /dev/null +++ b/src/programs/pgm_typing.ml @@ -0,0 +1,27 @@ +(**************************************************************************) +(* *) +(* Copyright (C) 2010- *) +(* Francois Bobot *) +(* Jean-Christophe Filliatre *) +(* Johannes Kanig *) +(* Andrei Paskevich *) +(* *) +(* This software is free software; you can redistribute it and/or *) +(* modify it under the terms of the GNU Library General Public *) +(* License version 2.1, with the special exception on linking *) +(* described in file LICENSE. *) +(* *) +(* This software is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) +(* *) +(**************************************************************************) + +let code id e = + assert false (*TODO*) + +(* +Local Variables: +compile-command: "unset LANG; make -C ../.. testl" +End: +*) diff --git a/src/programs/test.mlw b/src/programs/test.mlw index dc52ea811f43e742adb4e838eeb146ff5382d4cf..5605f9dd5ea01f8118233e10a5d2c396b37e498b 100644 --- a/src/programs/test.mlw +++ b/src/programs/test.mlw @@ -2,25 +2,19 @@ (* test file for ML-why *) { +use import prelude.Programs use import prelude.Int logic f(int) : int logic g(x : int) : int = f(x+1) } let p = - if !x = 1 then begin end else ghost begin !x end; + let x = ref 0 in L: assert { !x = 0 }; - check { false }; - let z = !x + !x in - let t = ghost (ref 2) in - assume { true -> old(!z) = 2 }; - while !x >= 0 do - invariant { true } variant { t } - x := 2 - done; - (* for x in s do () done; *) - f !x + x := 1; + assert { at(!x, L) = 0 }; + !x { axiom A : forall x:int. f(x) = g(x-1) diff --git a/src/transform/compile_match.mli b/src/transform/compile_match.mli index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..81fccfe9c9422316b52813ab27a2d15c31f67db3 100644 --- a/src/transform/compile_match.mli +++ b/src/transform/compile_match.mli @@ -0,0 +1,19 @@ +(**************************************************************************) +(* *) +(* Copyright (C) 2010- *) +(* Francois Bobot *) +(* Jean-Christophe Filliatre *) +(* Johannes Kanig *) +(* Andrei Paskevich *) +(* *) +(* This software is free software; you can redistribute it and/or *) +(* modify it under the terms of the GNU Library General Public *) +(* License version 2.1, with the special exception on linking *) +(* described in file LICENSE. *) +(* *) +(* This software is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) +(* *) +(**************************************************************************) + diff --git a/src/transform/eliminate_inductive.mli b/src/transform/eliminate_inductive.mli index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..81fccfe9c9422316b52813ab27a2d15c31f67db3 100644 --- a/src/transform/eliminate_inductive.mli +++ b/src/transform/eliminate_inductive.mli @@ -0,0 +1,19 @@ +(**************************************************************************) +(* *) +(* Copyright (C) 2010- *) +(* Francois Bobot *) +(* Jean-Christophe Filliatre *) +(* Johannes Kanig *) +(* Andrei Paskevich *) +(* *) +(* This software is free software; you can redistribute it and/or *) +(* modify it under the terms of the GNU Library General Public *) +(* License version 2.1, with the special exception on linking *) +(* described in file LICENSE. *) +(* *) +(* This software is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) +(* *) +(**************************************************************************) + diff --git a/src/transform/remove_logic_definition.ml b/src/transform/remove_logic_definition.ml index dc6aeb9f61738c6d011233427b1351f21ac25032..e065a75992694a3c9b18c4f3f599a98e82093512 100644 --- a/src/transform/remove_logic_definition.ml +++ b/src/transform/remove_logic_definition.ml @@ -16,6 +16,7 @@ (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) (* *) (**************************************************************************) + open Ident open Term open Decl