programs : syntax for match

share/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" "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" "label" "assert" "absurd" "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")

src/programs/pgm_parser.mly

@@ -31,7 +31,9 @@
 
   let mk_expr d = { expr_loc = loc (); expr_desc = d }
   let mk_expr_i i d = { expr_loc = loc_i i; expr_desc = d }
- 
+
+  let mk_pat p = { pat_loc = loc (); pat_desc = p }
+
   (* FIXME: factorize with parser/parser.mly *)
   let infix s = "infix " ^ s
   let prefix s = "prefix " ^ s
@@ -242,6 +244,8 @@ expr:
    { mk_expr (Elazy (LazyOr, $1, $3)) }
 | LET lident EQUAL expr IN expr
    { mk_expr (Elet ($2, $4, $6)) }
+| MATCH list1_expr_sep_comma WITH option_bar match_cases END
+   { mk_expr (Ematch ($2, $5)) }
 | GHOST expr
    { mk_expr (Eghost $2) }
 | LABEL uident COLON expr
@@ -276,6 +280,38 @@ list1_simple_expr:
 | simple_expr list1_simple_expr { $1 :: $2 }
 ;
 
+list1_expr_sep_comma:
+| expr                            { [$1] }
+| expr COMMA list1_expr_sep_comma { $1 :: $3 }
+;
+
+option_bar:
+| /* epsilon */ { () }
+| BAR           { () }
+;
+
+match_cases:
+| match_case                  { [$1] }
+| match_case BAR match_cases  { $1::$3 }
+;
+
+match_case:
+| list1_pat_sep_comma ARROW expr { ($1,$3) }
+;
+
+list1_pat_sep_comma:
+| pattern                           { [$1] }
+| pattern COMMA list1_pat_sep_comma { $1::$3 }
+
+pattern:
+| UNDERSCORE                                    { mk_pat (PPpwild) }
+| lident                                        { mk_pat (PPpvar $1) }
+| uqualid                                       { mk_pat (PPpapp ($1, [])) }
+| uqualid LEFTPAR list1_pat_sep_comma RIGHTPAR  { mk_pat (PPpapp ($1, $3)) }
+| pattern AS lident                             { mk_pat (PPpas ($1,$3)) }
+| LEFTPAR pattern RIGHTPAR                      { $2 }
+;
+
 assertion_kind:
 | ASSERT { Aassert }
 | ASSUME { Aassume }

src/programs/pgm_ptree.ml

@@ -67,6 +67,7 @@ and expr_desc =
   | Eif of expr * expr * expr
   | Ewhile of expr * loop_annotation * expr
   | Elazy of lazy_op * expr * expr
+  | Ematch of expr list * (Ptree.pattern list * expr) list
   | Eskip 
   | Eabsurd
   (* annotations *)
@@ -76,7 +77,8 @@ and expr_desc =
   | Ecast of expr * Ptree.pty
 
 
-  (* TODO: fun, rec, raise, try, absurd, any, post? *)
+  (* TODO: fun, rec, raise, try, any, post?, match 
+           ghost *)
 
 type decl =
   | Dcode  of ident * expr

src/programs/pgm_typing.ml

@@ -151,6 +151,8 @@ and expr_desc env loc = function
       let e2 = dexpr env e2 in
       expected_type e2 env.ty_bool;
       DElazy (op, e1, e2), env.ty_bool
+  | Pgm_ptree.Ematch (el, bl) ->
+      assert false (*TODO*)
   | Pgm_ptree.Eskip ->
       DEskip, env.ty_unit
   | Pgm_ptree.Eabsurd ->

src/programs/test.mlw

 
+{ 
+use import list.List
+}
+
 let p =
   let x = ref 0 in
   x := 1;
   assert { !x = 1 };
-  absurd : int
+  label L:
+  assume { !x = 2 };
+  absurd : int list
+
 
 
 (*