Commit 9345a9b6 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

programs: added syntax for let pat = expr in expr

parent 37d8adbc
...@@ -123,6 +123,7 @@ ...@@ -123,6 +123,7 @@
%nonassoc prec_post %nonassoc prec_post
%nonassoc BAR %nonassoc BAR
%nonassoc prec_id_pattern
%nonassoc prec_recfun %nonassoc prec_recfun
%nonassoc prec_triple %nonassoc prec_triple
%left LEFTBLEFTB %left LEFTBLEFTB
...@@ -277,6 +278,8 @@ expr: ...@@ -277,6 +278,8 @@ expr:
{ mk_expr (Elazy (LazyOr, $1, $3)) } { mk_expr (Elazy (LazyOr, $1, $3)) }
| LET lident EQUAL expr IN expr | LET lident EQUAL expr IN expr
{ mk_expr (Elet ($2, $4, $6)) } { mk_expr (Elet ($2, $4, $6)) }
| LET pattern EQUAL expr IN expr
{ mk_expr (Ematch ([$4], [[$2], $6])) }
| LET lident list1_type_v_binder EQUAL triple IN expr | LET lident list1_type_v_binder EQUAL triple IN expr
{ mk_expr (Elet ($2, mk_expr_i 3 (Efun ($3, $5)), $7)) } { mk_expr (Elet ($2, mk_expr_i 3 (Efun ($3, $5)), $7)) }
| LET REC list1_recfun_sep_and IN expr | LET REC list1_recfun_sep_and IN expr
...@@ -389,7 +392,7 @@ pat_args: ...@@ -389,7 +392,7 @@ pat_args:
pat_arg: pat_arg:
| UNDERSCORE | UNDERSCORE
{ mk_pat (PPpwild) } { mk_pat (PPpwild) }
| lident | lident %prec prec_id_pattern
{ mk_pat (PPpvar $1) } { mk_pat (PPpvar $1) }
| uqualid | uqualid
{ mk_pat (PPpapp ($1, [])) } { mk_pat (PPpapp ($1, [])) }
......
let rec div x y variant {x} =
{ 0 <= x and 0 < y }
if y < x then
(0, x)
else
let (q,r) = div (x-y) y in (q+1, r)
{ let (q,r) = result in x = q*y + r and 0 <= r < x }
{ {
type tree 'a = type tree 'a =
| Leaf (x : 'a) | Empty
| Node (tree 'a) (x: 'a) (tree 'a) | Node (tree 'a) 'a (tree 'a)
} }
let rec mem x t = match t : tree int with
| Empty -> False
| Node l y r -> x=y || mem x (if x < y then l else r)
end
let test (t: tree int) = let root t : 'a =
{ t <> Empty }
match t with match t with
| Leaf y -> y | Empty -> absurd
| Node _ y _ -> y | Node _ x _ -> x
end end
{ }
(* (*
Local Variables: Local Variables:
......
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