typage des programmes (en cours

parent c50f0034
...@@ -174,7 +174,7 @@ testl: bin/whyl.byte ...@@ -174,7 +174,7 @@ testl: bin/whyl.byte
# programs # 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)) PGM_CMO := $(addprefix src/programs/, $(PGM_CMO))
WHYL_CMO = $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) $(DRIVER_CMO)\ WHYL_CMO = $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) $(DRIVER_CMO)\
......
...@@ -29,7 +29,7 @@ ...@@ -29,7 +29,7 @@
'("(\\*\\([^*]\\|\\*[^)]\\)*\\*)" . font-lock-comment-face) '("(\\*\\([^*]\\|\\*[^)]\\)*\\*)" . font-lock-comment-face)
'("{\\([^}]*\\)}" . font-lock-type-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 '("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) ; `(,(why-regexp-opt '("unit" "bool" "int" "float" "prop" "array")) . font-lock-type-face)
) )
"Minimal highlighting for Why mode") "Minimal highlighting for Why mode")
......
...@@ -136,7 +136,21 @@ theory Set ...@@ -136,7 +136,21 @@ theory Set
end 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: Local Variables:
......
...@@ -16,3 +16,4 @@ ...@@ -16,3 +16,4 @@
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *) (* *)
(**************************************************************************) (**************************************************************************)
...@@ -148,6 +148,8 @@ rule token = parse ...@@ -148,6 +148,8 @@ rule token = parse
{ COLON } { COLON }
| ";" | ";"
{ SEMICOLON } { SEMICOLON }
| "!"
{ BANG }
| ":=" | ":="
{ COLONEQUAL } { COLONEQUAL }
| "->" | "->"
...@@ -158,7 +160,7 @@ rule token = parse ...@@ -158,7 +160,7 @@ rule token = parse
{ OP0 s } { OP0 s }
| "+" | "-" as c | "+" | "-" as c
{ OP2 (String.make 1 c) } { OP2 (String.make 1 c) }
| "*" | "/" | "%" | "!" as c | "*" | "/" | "%" as c
{ OP3 (String.make 1 c) } { OP3 (String.make 1 c) }
| "@" | "@"
{ AT } { AT }
......
...@@ -69,7 +69,7 @@ let type_file file = ...@@ -69,7 +69,7 @@ let type_file file =
List.fold_left List.fold_left
(fun uc d -> match d with (fun uc d -> match d with
| Dlogic dl -> List.fold_left (Typing.add_decl env Mnm.empty) uc dl | 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 uc p
in in
() ()
......
...@@ -96,7 +96,7 @@ ...@@ -96,7 +96,7 @@
/* symbols */ /* symbols */
%token UNDERSCORE QUOTE COMMA LEFTPAR RIGHTPAR COLON SEMICOLON %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 LEFTBLEFTB RIGHTBRIGHTB BAR BARBAR AMPAMP BIGARROW
%token EOF %token EOF
...@@ -234,12 +234,11 @@ expr: ...@@ -234,12 +234,11 @@ expr:
{ mk_expr (Ewhile ($2, $4, $5)) } { mk_expr (Ewhile ($2, $4, $5)) }
; ;
/* FIXME: prefix operators should be part of simple_expr
otherwise we can't parse "f !x" */
simple_expr: simple_expr:
| constant | constant
{ mk_expr (Econstant $1) } { mk_expr (Econstant $1) }
| BANG expr
{ mk_prefix "!" $2 }
| lqualid | lqualid
{ mk_expr (Eident $1) } { mk_expr (Eident $1) }
| LEFTPAR expr RIGHTPAR | LEFTPAR expr RIGHTPAR
......
(**************************************************************************)
(* *)
(* 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:
*)
...@@ -2,25 +2,19 @@ ...@@ -2,25 +2,19 @@
(* test file for ML-why *) (* test file for ML-why *)
{ {
use import prelude.Programs
use import prelude.Int use import prelude.Int
logic f(int) : int logic f(int) : int
logic g(x : int) : int = f(x+1) logic g(x : int) : int = f(x+1)
} }
let p = let p =
if !x = 1 then begin end else ghost begin !x end; let x = ref 0 in
L: L:
assert { !x = 0 }; assert { !x = 0 };
check { false }; x := 1;
let z = !x + !x in assert { at(!x, L) = 0 };
let t = ghost (ref 2) in !x
assume { true -> old(!z) = 2 };
while !x >= 0 do
invariant { true } variant { t }
x := 2
done;
(* for x in s do () done; *)
f !x
{ {
axiom A : forall x:int. f(x) = g(x-1) axiom A : forall x:int. f(x) = g(x-1)
......
(**************************************************************************)
(* *)
(* 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. *)
(* *)
(**************************************************************************)
(**************************************************************************)
(* *)
(* 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. *)
(* *)
(**************************************************************************)
...@@ -16,6 +16,7 @@ ...@@ -16,6 +16,7 @@
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *) (* *)
(**************************************************************************) (**************************************************************************)
open Ident open Ident
open Term open Term
open Decl open Decl
......
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