No commit message

No commit message

misc/why.el

+
+;; why.el - GNU Emacs mode for Why
+;; Copyright (C) 2002 Jean-Christophe FILLIATRE
+
+(defvar why-mode-hook nil)
+
+(defvar why-mode-map nil
+  "Keymap for Why major mode")
+
+(if why-mode-map nil
+  (setq why-mode-map (make-keymap))
+  (define-key why-mode-map "\C-c\C-c" 'why-generate-obligations)
+  (define-key why-mode-map "\C-c\C-a" 'why-find-alternate-file)
+  (define-key why-mode-map "\C-c\C-v" 'why-viewer)
+  (define-key why-mode-map [(control return)] 'font-lock-fontify-buffer))
+
+(setq auto-mode-alist
+      (append
+       '(("\\.mlw" . why-mode))
+       auto-mode-alist))
+
+;; font-lock
+
+(defun why-regexp-opt (l)
+  (concat "\\<" (concat (regexp-opt l t) "\\>")))
+
+(defconst why-font-lock-keywords-1
+  (list
+   '("(\\*\\([^*]\\|\\*[^)]\\)*\\*)" . font-lock-comment-face)
+   '("{\\([^}]*\\)}" . font-lock-type-face)
+   `(,(why-regexp-opt '("include" "inductive" "external" "logic" "parameter" "exception" "axiom" "predicate" "function" "goal" "type")) . font-lock-builtin-face)
+   `(,(why-regexp-opt '("let" "rec" "in" "if" "then" "else" "begin" "end" "while" "do" "done" "label" "assert" "try" "with" "theory")) . font-lock-keyword-face)
+   ; `(,(why-regexp-opt '("unit" "bool" "int" "float" "prop" "array")) . font-lock-type-face)
+   )
+  "Minimal highlighting for Why mode")
+
+(defvar why-font-lock-keywords why-font-lock-keywords-1
+  "Default highlighting for Why mode")
+
+;; syntax
+
+(defvar why-mode-syntax-table nil
+  "Syntax table for why-mode")
+
+(defun why-create-syntax-table ()
+  (if why-mode-syntax-table
+      ()
+    (setq why-mode-syntax-table (make-syntax-table))
+    (set-syntax-table why-mode-syntax-table)
+    (modify-syntax-entry ?' "w" why-mode-syntax-table)
+    (modify-syntax-entry ?_ "w" why-mode-syntax-table)))
+
+;; utility functions 
+
+(defun why-go-and-get-next-proof ()
+  (let ((bp (search-forward "Proof." nil t)))
+    (if (null bp) (progn (message "Cannot find a proof below") nil)
+      (let ((bs (re-search-forward "Save\\|Qed\\." nil t)))
+	(if (null bs) (progn (message "Cannot find a proof below") nil)
+	  (if (> bs (+ bp 6))
+	      (let ((br (+ bp 1))
+		    (er (progn (goto-char bs) (beginning-of-line) (point))))
+		(progn (kill-region br er) t))
+	    (why-go-and-get-next-proof)))))))
+
+(defun why-grab-next-proof ()
+  "grab the next non-empty proof below and insert it at current point"
+  (interactive)
+  (if (save-excursion (why-go-and-get-next-proof)) (yank)))
+
+;; custom variables
+
+(require 'custom)
+
+(defcustom why-prover "coq"
+  "Why prover"
+  :group 'why :type '(choice (const :tag "Coq" "coq")
+			     (const :tag "PVS" "pvs")))
+
+(defcustom why-prog-name "why"
+  "Why executable name"
+  :group 'why :type 'string)
+
+(defcustom why-options "--valid"
+  "Why options"
+  :group 'why :type 'string)
+
+(defcustom why-viewer-prog-name "why_viewer"
+  "Why viewer executable name"
+  :group 'why :type 'string)
+
+(defun why-command-line (file)
+  (concat why-prog-name " -" why-prover " " why-options " " file))
+
+(defun why-find-alternate-file ()
+  "switch to the proof obligations buffer"
+  (interactive)
+  (let* ((f (buffer-file-name))
+	 (fcoq (concat (file-name-sans-extension f) "_why.v")))
+    (find-file fcoq)))
+
+(defun why-generate-obligations ()
+  "generate the proof obligations"
+  (interactive)
+  (let ((f (buffer-name)))
+    (compile (why-command-line f))))
+
+(defun why-viewer-command-line (file)
+  (concat why-viewer-prog-name " " file))
+
+(defun why-viewer ()
+  "launch the why viewer"
+  (interactive)
+  (let ((f (buffer-name)))
+    (compile (why-viewer-command-line f))))
+
+(defun why-generate-ocaml ()
+  "generate the ocaml code"
+  (interactive)
+  (let ((f (buffer-name)))
+    (compile (concat why-prog-name " --ocaml " f))))
+
+;; menu
+
+(require 'easymenu)
+
+(defun why-menu ()
+  (easy-menu-define
+   why-mode-menu (list why-mode-map)
+   "Why Mode Menu." 
+   '("Why"
+     ["Customize Why mode" (customize-group 'why) t]
+     "---"
+     ["Type-check buffer" why-type-check t]
+     ; ["Show WP" why-show-wp t]
+     ["Why viewer" why-viewer t]
+     ["Generate obligations" why-generate-obligations t]
+     ["Switch to obligations buffer" why-find-alternate-file t]
+     ["Generate Ocaml code" why-generate-ocaml t]
+     ["Recolor buffer" font-lock-fontify-buffer t]
+     "---"
+     "Coq"
+     ["Grab next proof" why-grab-next-proof t]
+     "---"
+     "PVS"
+     "---"
+     ))
+  (easy-menu-add why-mode-menu))
+
+;; setting the mode
+
+(defun why-mode ()
+  "Major mode for editing Why programs.
+
+\\{why-mode-map}"
+  (interactive)
+  (kill-all-local-variables)
+  (why-create-syntax-table)
+  ; hilight
+  (make-local-variable 'font-lock-defaults)
+  (setq font-lock-defaults '(why-font-lock-keywords))
+  ; indentation
+  ; (make-local-variable 'indent-line-function)
+  ; (setq indent-line-function 'why-indent-line)
+  ; menu
+  ; providing the mode
+  (setq major-mode 'why-mode)
+  (setq mode-name "WHY")
+  (use-local-map why-mode-map)
+  (font-lock-mode 1)
+  (why-menu)
+  (run-hooks 'why-mode-hook))
+
+(provide 'why-mode)
+

src/lexer.mll

@@ -83,10 +83,12 @@
 	"ref", REF;
 	"returns", RETURNS;
 	"then", THEN;
+	"theory", THEORY;
 	"true", TRUE;
 	"try", TRY;
 	"type", TYPE;
 	"unit", UNIT;
+	"uses", USES;
 	"variant", VARIANT;
 	"void", VOID;
 	"while", WHILE;

src/main.ml

@@ -37,7 +37,7 @@ let () =
     Loc.set_file file lb;
     let f = Lexer.parse_logic_file lb in 
     close_in c;
-    ignore (List.fold_left Typing.add Typing.empty f)
+    ignore (Typing.add_decls Typing.empty f)
   with e ->
     eprintf "%a@." report e;
     exit 1

src/parser.mly

@@ -101,7 +101,7 @@
 %token QUOTE RAISE RAISES READS REAL REC REF RETURNS RIGHTB RIGHTBRIGHTB
 %token RIGHTPAR RIGHTSQ 
 %token SEMICOLON SLASH 
-%token THEN TIMES TRUE TRY TYPE UNIT VARIANT VOID WHILE WITH WRITES
+%token THEN THEORY TIMES TRUE TRY TYPE UNIT USES VARIANT VOID WHILE WITH WRITES
 
 /* Precedences */
 
@@ -147,6 +147,8 @@
 logic_file:
 | list1_decl EOF 
    { $1 }
+| list1_theory EOF
+   { $1 }
 | EOF 
    { [] }
 ;
@@ -158,6 +160,13 @@ list1_decl:
    { $1 :: $2 }
 ;
 
+list0_decl:
+| /* epsilon */
+   { [] }
+| list1_decl 
+   { $1 }
+;
+
 decl:
 | external_ LOGIC list1_ident_sep_comma COLON logic_type
    { Logic (loc_i 3, $1, $3, $5) }
@@ -178,6 +187,24 @@ decl:
    { let loc, vl, id = $2 in $3 loc vl id }
 ;
 
+list1_theory:
+| theory 
+   { [$1] }
+| theory list1_theory 
+   { $1 :: $2 }
+;
+
+theory:
+| THEORY ident uses list0_decl END { Theory (loc (), $2, $3, $4) }
+;
+
+uses:
+| /* epsilon */ 
+    { [] }
+| USES list1_ident_sep_comma
+    { $2 }
+;
+
 typedecl:
 | ident
     { (loc_i 1, [], $1) }

src/ptree.mli

@@ -72,6 +72,8 @@ type plogic_type =
   | PPredicate of ppure_type list
   | PFunction of ppure_type list * ppure_type
 
+type uses = string
+
 type logic_decl = 
   | Logic of loc * external_ * string list * plogic_type
   | Predicate_def of loc * string * (loc * string * ppure_type) list * lexpr
@@ -83,5 +85,6 @@ type logic_decl =
   | TypeDecl of loc * external_ * string list * string
   | AlgType of (loc * string list * string
       * (loc * string * ppure_type list) list) list
+  | Theory of loc * string * uses list * logic_decl list
 
 type logic_file = logic_decl list

src/test.why

 
 (* test file *)
 
-type 'a list 
-
-logic nil  : 'a list
-
-logic cons : 'a, 'a list -> 'a list
-
-type int
-
-logic length : 'a list -> int
-
-logic is_nil : 'a list -> prop
-
-logic eq : 'a, 'a -> prop
-
-axiom a : forall x : 'a. not eq(nil, cons(x, nil))
-
-
+theory test  
 
+  type 'a list
 
+  logic nil  : 'a list
 
+  logic cons : 'a, 'a list -> 'a list
 
+  type int
 
+  logic length : 'a list -> int
 
+  logic is_nil : 'a list -> prop
 
+  logic eq : 'a, 'a -> prop
 
+  axiom a : forall x : 'a. not eq(nil, cons(nil, nil))
 
+end
 
+theory test2
 
+  type elt
 
+  type t 
 
+  logic add : elt, t -> t
 
+end

src/typing.ml

@@ -34,6 +34,7 @@ type error =
   | TermExpectedType of (formatter -> unit) * (formatter -> unit) 
       (* actual / expected *)
   | BadNumberOfArguments of Name.t * int * int 
+  | ClashTheory of string
 
 exception Error of error
 
@@ -65,6 +66,8 @@ let report fmt = function
   | TermExpectedType (ty1, ty2) ->
       fprintf fmt "@[This term has type "; ty1 fmt; 
       fprintf fmt "@ but is expected to have type@ "; ty2 fmt; fprintf fmt "@]"
+  | ClashTheory s ->
+      fprintf fmt "clash with previous theory %s" s
 
 (** typing environments *)
 
@@ -74,14 +77,21 @@ type env = {
   tysymbols : tysymbol M.t; (* type symbols *)
   fsymbols  : fsymbol M.t;  (* function symbols *)
   psymbols  : psymbol M.t;  (* predicate symbols *)
+  theories  : env M.t;
 }
 
 let empty = {
   tysymbols = M.empty;
   fsymbols  = M.empty;
   psymbols  = M.empty;
+  theories  = M.empty;
 }
 
+let is_empty env = 
+  M.is_empty env.tysymbols &&
+  M.is_empty env.fsymbols &&
+  M.is_empty env.psymbols
+
 let find_tysymbol s env = M.find s env.tysymbols
 let find_fsymbol s env = M.find s env.fsymbols
 let find_psymbol s env = M.find s env.psymbols
@@ -160,22 +170,18 @@ let rec unify t1 t2 = match t1, t2 with
       t1 = t2
 
 (** Destructive typing environment, that is
-    environment + type variables (user or destructive) + local variables.
+    environment + local variables.
     It is only local to this module and created with [create_denv] below. *)
 
-module Htv = Hashtbl.Make(Name)
-
 type denv = { 
   env : env;
   utyvars : (string, type_var) Hashtbl.t; (* user type variables *)
-  dtyvars : type_var Htv.t;  (* destructive type variables for unification *)
   dvars : dty M.t; (* local variables, to be bound later *)
 }
 
 let create_denv env = { 
   env = env; 
   utyvars = Hashtbl.create 17; 
-  dtyvars = Htv.create 17; 
   dvars = M.empty;
 }
 
@@ -187,14 +193,6 @@ let find_user_type_var x env =
     Hashtbl.add env.utyvars x v;
     v
  
-let find_type_var tv env =
-  try
-    Htv.find env.dtyvars tv
-  with Not_found ->
-    let v = create_type_var ~user:false tv in
-    Htv.add env.dtyvars tv v;
-    v
- 
 (** Typing types *)
 
 (* parsed types -> intermediate types *)
@@ -218,12 +216,35 @@ let rec ty = function
   | Tyapp (s, tl) ->
       Ty.ty_app s (List.map ty tl)
 
+(* Specialize *)
+
+module Htv = Hashtbl.Make(Name)
+
+let find_type_var tv env =
+  try
+    Htv.find env tv
+  with Not_found ->
+    let v = create_type_var ~user:false tv in
+    Htv.add env tv v;
+    v
+ 
 let rec specialize env t = match t.Ty.ty_node with
   | Ty.Tyvar tv -> 
       Tyvar (find_type_var tv env)
   | Ty.Tyapp (s, tl) ->
       Tyapp (s, List.map (specialize env) tl)
 	
+let specialize_fsymbol x env =
+  let s = find_fsymbol x env.env in
+  let tl, t = s.fs_scheme in
+  let env = Htv.create 17 in
+  s, List.map (specialize env) tl, specialize env t
+
+let specialize_psymbol x env =
+  let s = find_psymbol x env.env in
+  let env = Htv.create 17 in
+  s, List.map (specialize env) s.ps_scheme
+
 (** Typing terms and formulas *)
 
 type dterm = { dt_node : dterm_node; dt_ty : dty }
@@ -254,11 +275,6 @@ let binop = function
   | PPiff -> Fiff
   | _ -> assert false 
 
-let specialize_fsymbol x env =
-  let s = find_fsymbol x env.env in
-  let tl, t = s.fs_scheme in
-  s, List.map (specialize env) tl, specialize env t
-
 let rec dterm env t = 
   let n, ty = dterm_node t.pp_loc env t.pp_desc in
   { dt_node = n; dt_ty = ty }
@@ -311,10 +327,9 @@ and dfmla env e = match e.pp_desc with
       let env = { env with dvars = M.add id ty env.dvars } in
       Fquant (Fexists, id, ty, dfmla env a)
   | PPapp (x, tl) ->
-      let s, tyl =
+      let s, tyl = 
 	try 
-	  let s = find_psymbol x env.env in
-	  s, List.map (specialize env) s.ps_scheme
+	  specialize_psymbol x env 
 	with Not_found -> 
 	  error ~loc:e.pp_loc (UnboundSymbol x)
       in
@@ -414,7 +429,7 @@ let axiom loc s f env =
   ignore (fmla env f);
   env
 
-let add env = function
+let rec add_decl env = function
   | TypeDecl (loc, ext, sl, s) ->
       add_type loc ext sl s env
   | Logic (loc, ext, ids, PPredicate pl) ->
@@ -423,5 +438,16 @@ let add env = function
       List.fold_left (add_function loc pl t) env ids
   | Axiom (loc, s, f) ->
       axiom loc s f env
+  | Theory (loc, s, u, dl) ->
+      add_theory loc s u dl env
   | _ ->
       assert false (*TODO*)
+
+and add_decls env = List.fold_left add_decl env
+
+and add_theory loc s u dl env =
+  assert (is_empty env);
+  if M.mem s env.theories then error ~loc (ClashTheory s);
+  let env = add_decls env dl in
+  { empty with theories = M.add s env env.theories }
+

src/typing.mli

@@ -33,7 +33,8 @@ val fmla : env -> Ptree.lexpr -> fmla
 
 (** building environments *)
 
-val add : env -> Ptree.logic_decl -> env
+val add_decl : env -> Ptree.logic_decl -> env
+val add_decls : env -> Ptree.logic_decl list -> env
 
 (** error reporting *)