contributions by S. Lescuyer: Einstein's puzzle, solved beautifully using...

contributions by S. Lescuyer: Einstein's puzzle, solved beautifully using Why3's new features (see examples/einstein.why); an improved Emacs mode

examples/einstein.why

+(*
+   This problem is usually referred to as Einstein's Logic Problem.
+   see http://en.wikipedia.org/wiki/Zebra_Puzzle
+   (contribution by Stéphane Lescuyer)
+*)
+
+theory Bijection
+  type t
+  type u
+
+  logic _of t : u
+  logic _to u : t
+
+  axiom To_of : forall x : t. _to(_of(x)) = x
+  axiom Of_to : forall y : u. _of(_to(y)) = y
+end
+
+theory Einstein "Einstein's problem"
+  (* Types *)
+  type house = H1 | H2 | H3 | H4 | H5
+  type color = Blue | Green | Red | White | Yellow
+  type person = Dane | Englishman | German | Norwegian | Swede
+  type drink = Beer | Coffee | Milk | Tea | Water
+  type cigar = Blend | BlueMaster | Dunhill | PallMall | Prince
+  type pet = Birds | Cats | Dogs | Fish | Horse
+  
+  (* Each house is associated bijectively to a color and a person *)
+  clone Bijection as Color with type t = house, type u = color
+  clone Bijection as Owner with type t = house, type u = person
+
+  (* Each drink, cigar brand and pet are associated bijectively to a person *)
+  clone Bijection as Drink with type t = person, type u = drink
+  clone Bijection as Cigar with type t = person, type u = cigar
+  clone Bijection as Pet with type t = person, type u = pet
+
+  (* Relative positions of the houses *)
+  logic left_of (h1 h2 : house) =
+    match h1, h2 with
+    | H1, H2 -> true
+    | H2, H3 -> true
+    | H3, H4 -> true
+    | H4, H5 -> true
+    | _, _ -> false
+    end
+  logic right_of (h1 h2 : house) =
+    left_of h2 h1
+  logic neighbour (h1 h2 : house) =
+    left_of h1 h2 \/ right_of h1 h2
+end
+
+theory EinsteinHints "Hints"
+  use import Einstein
+
+  (* The Englishman lives in a red house *)
+  axiom Hint1: Color._of (Owner._to Englishman) = Red
+
+  (* The Swede has dogs *)
+  axiom Hint2: Pet._of Swede = Dogs
+
+  (* The Dane drinks tea *)
+  axiom Hint3: Drink._of Dane = Tea
+
+  (* The green house is on the left of the white one *)
+  axiom Hint4: left_of (Color._to Green) (Color._to White)
+
+  (* The green house's owner drinks coffee *)
+  axiom Hint5: Drink._of (Owner._of (Color._to Green)) = Coffee
+
+  (* The person who smokes Pall Mall has birds *)
+  axiom Hint6: Pet._of (Cigar._to PallMall) = Birds
+
+  (* The yellow house's owner smokes Dunhill *)
+  axiom Hint7: Cigar._of (Owner._of (Color._to Yellow)) = Dunhill
+
+  (* In the house in the center lives someone who drinks milk *)
+  axiom  Hint8: Drink._of (Owner._of H3) = Milk
+
+  (* The Norwegian lives in the first house *)
+  axiom Hint9: Owner._of H1 = Norwegian
+
+  (* The man who smokes Blends lives next to the one who has cats *)
+  axiom Hint10: neighbour 
+    (Owner._to (Cigar._to Blend)) (Owner._to (Pet._to Cats))
+
+  (* The man who owns a horse lives next to the one who smokes Dunhills *)
+  axiom Hint11: neighbour
+    (Owner._to (Pet._to Horse)) (Owner._to (Cigar._to Dunhill))
+
+  (* The man who smokes Blue Masters drinks beer *)
+  axiom Hint12:
+    Drink._of (Cigar._to BlueMaster) = Beer
+
+  (* The German smokes Prince *)
+  axiom Hint13:
+    Cigar._of German = Prince
+
+  (* The Norwegian lives next to the blue house *)
+  axiom Hint14:
+    neighbour (Owner._to Norwegian) (Color._to Blue)
+
+  (* The man who smokes Blends has a neighbour who drinks water *)
+  axiom Hint15:
+    neighbour (Owner._to (Cigar._to Blend)) (Owner._to (Drink._to Water))
+
+end
+
+theory Goals "Goals about Einstein's problem"
+  use import Einstein
+  use import EinsteinHints
+
+  (* lemma First_House_Not_White: Color._of H1 <> White *)
+  (* lemma Last_House_Not_Green: Color._of H5 <> Green *)
+
+  (* lemma Blue_not_Red: Blue <> Red *)
+  (* lemma Englishman_not_H2: Owner._to Englishman <> H2 *)
+  (* lemma Englishman_not_H1: Owner._to Englishman <> H1 *)
+
+  (* lemma Second_House_Blue: Color._of H2 = Blue *)
+  (* lemma Green_H4 : Color._of H4 = Green *)
+  (* lemma White_H5 : Color._of H5 = White *)
+  (* lemma Red_H3 : Color._of H3 = Red *)
+  (* lemma Yellow_H1 : Color._of H1 = Yellow *)
+
+  goal G: Pet._to Fish = German
+
+end
+
+(*
+Local Variables: 
+compile-command: "make -C .. examples/einstein.gui"
+End: 
+*)

share/emacs/why.el

@@ -26,7 +26,8 @@
 
 (defconst why-font-lock-keywords-1
   (list
-   '("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face)
+   ;; 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")) . 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")) . font-lock-keyword-face)
@@ -52,7 +53,12 @@
     (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)))
+    (modify-syntax-entry ?_ "w" why-mode-syntax-table)
+    ; comments
+    (modify-syntax-entry ?\( ". 1" why-mode-syntax-table)
+    (modify-syntax-entry ?\) ". 4" why-mode-syntax-table)
+    (modify-syntax-entry ?* ". 23" why-mode-syntax-table)
+    ))
 
 ;; utility functions 
 
@@ -186,9 +192,15 @@
                             ))))))
         ;For the definition its very badly done...
           (if (looking-at "^[ \t]*$")
+	      ;; (save-excursion 
+	      ;; 	(forward-line -1)
+	      ;; 	(setq cur-indent (current-indentation))
+	      ;; 	(setq not-indented nil))
               (progn
                 (setq cur-indent 0)
                 (setq not-indented nil))
+	    (if (not
+		 (looking-at "^[ \t]*(\*.*"))
             (if (not 
                  (looking-at "^[ \t]*\\(logic\\|type\\|axiom\\|goal\\|lemma\\|inductive\\|use\\|theory\\|clone\\)"))
                 (save-excursion
@@ -203,7 +215,7 @@
                           "^[ \t]*\\(logic\\|type\\|axiom\\|goal\\|lemma\\|inductive\\)")
                          (setq cur-indent (+ (current-indentation) why-indent))
                        (setq cur-indent (current-indentation)))
-                     (setq not-indented nil))))))
+                     (setq not-indented nil)))))))
           ;For inside theory or namespace
           (save-excursion 
             (while not-indented
@@ -223,10 +235,7 @@
             (indent-line-to cur-indent)
           (indent-line-to 0)))))))
 
-
-
 ;; setting the mode
-
 (defun why-mode ()
   "Major mode for editing Why programs.
 
@@ -240,6 +249,8 @@
   ; indentation
   (make-local-variable 'indent-line-function)
   (setq indent-line-function 'why-indent-line)
+  ; OCaml style comments for comment-region, comment-dwim, etc.
+  (setq comment-start "(*" comment-end "*)")
   ; menu
   ; providing the mode
   (setq major-mode 'why-mode)

tests/test-jcf.why

@@ -7,7 +7,7 @@ theory Test
 
   logic p (list 'a)
 
-  goal G : p (Nil : list 'a) -> not (p (Nil : list 'b)) -> false
+  goal G : p (Nil : list 'a) -> not (p (Nil : list 'bcd)) -> false
 
 end