programs: syntax for infix and prefix symbols

parent 9ddba7a4
......@@ -17,14 +17,14 @@ let test_and_1 () =
{ result = 1 }
let test_and_2 () =
{ !x <> 0 }
{ x <> 0 }
if id_not_0 !x >= 1 && !x <= 1 then !x else 0+1
{ result = 1 }
let test_or_1 () =
{ }
if (incr x; !x > 0) || !x < 0 then 1 else 2
{ result = 1 -> !x <> 0 }
{ result = 1 -> x <> 0 }
let test_or_2 () =
{ }
......@@ -34,17 +34,17 @@ let test_or_2 () =
let test_not_1 () =
{ }
if not (!x = 0) then x := 0
{ !x = 0 }
{ x = 0 }
let test_not_2 () =
{ !x <= 0 }
{ x <= 0 }
while not (!x = 0) do invariant { !x <= 0 } incr x done
{ !x = 0 }
{ x = 0 }
let test_all_1 () =
{ }
(!x >= 0 && not (!x = 0) || !x >= 1)
{ result=True <-> !x>=1 }
{ result=True <-> x>=1 }
(* from Cesar Munoz's CD3D *)
......@@ -58,7 +58,7 @@ parameter sq : x:int -> {} int { result = x*x }
let test_cd3d () =
{ true }
if !vx=0 && !vy=0 && sq !vx + sq !vy < sq d then 1 else 2
{ result=1 -> !vx=0 and !vy=0 }
{ result=1 -> vx=0 and vy=0 }
end
......
......@@ -7,9 +7,9 @@ module Ref
parameter ref : v:'a -> {} ref 'a { result=v }
parameter get : r:ref 'a -> {} 'a reads r { result=r }
parameter (!) : r:ref 'a -> {} 'a reads r { result=r }
parameter set : r:ref 'a -> v:'a -> {} unit writes r { r=v }
parameter (:=) : r:ref 'a -> v:'a -> {} unit writes r { r=v }
end
......
......@@ -855,13 +855,13 @@ list1_program_decl:
program_decl:
| decl
{ Dlogic $1 }
| LET lident labels list1_type_v_binder opt_cast EQUAL triple
| LET lident_rich labels list1_type_v_binder opt_cast EQUAL triple
{ Dlet (add_lab $2 $3, mk_expr_i 7 (Efun ($4, cast_body $5 $7))) }
| LET lident labels EQUAL FUN list1_type_v_binder ARROW triple
| LET lident_rich labels EQUAL FUN list1_type_v_binder ARROW triple
{ Dlet (add_lab $2 $3, mk_expr_i 8 (Efun ($6, $8))) }
| LET REC list1_recfun_sep_and
{ Dletrec $3 }
| PARAMETER lident labels COLON type_v
| PARAMETER lident_rich labels COLON type_v
{ Dparam (add_lab $2 $3, $5) }
| EXCEPTION uident labels
{ Dexn (add_lab $2 $3, None) }
......@@ -893,7 +893,7 @@ list1_recfun_sep_and:
;
recfun:
| lident labels list1_type_v_binder opt_cast opt_variant EQUAL triple
| lident_rich labels list1_type_v_binder opt_cast opt_variant EQUAL triple
{ add_lab $1 $2, $3, $5, cast_body $4 $7 }
;
......
......@@ -8,21 +8,19 @@ module P
let incr (r : ref int) : unit =
{ }
set r (get r + 1)
r := !r + 1
{ r = old r + 1 }
parameter r : ref int
let foo (x : int) =
{ x = 1 }
if x = 1 || absurd then 2 else 3
{ result = 2 }
let rec (!!) (x : ref int) =
{ x>=0 } if !x > 0 then begin x := !x - 1; !! x end { x=0 }
let f (r : ref int) =
let test (r : ref int) =
{ r = 0 }
assert { r = 0 };
incr r;
get r
!r
{ result = 1 }
end
......
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