programs: optional cast for function body

bench/programs/bad-typing/undefined_type_variable2.mlw

+
+let rec f (x:int) = f (x-1)

bench/programs/bad-typing/variant1.mlw

 
 (* missing variant *)
 
-let rec even (x:int) variant {x} =
-  odd (x-1) : int
-and odd (x:int) =
-  even (x-1) : int
+let rec even (x:int) : int variant {x} =
+  odd (x-1) 
+and odd (x:int) : int =
+  even (x-1)
 

bench/programs/bad-typing/variant2.mlw

@@ -5,8 +5,8 @@
 logic rel(int, int)
 }
 
-let rec even (x:int) variant {x} for rel =
-  odd (x-1) : int
-and odd (x:int) variant {x} =
-  even (x-1) : int
+let rec even (x:int) : int variant {x} for rel =
+  odd (x-1) 
+and odd (x:int) : int variant {x} =
+  even (x-1)
 

examples/programs/bresenham.mlw

@@ -34,7 +34,7 @@ logic invariant(x:int, y:int, e:int) =
 lemma Invariant_is_ok : forall x,y,e:int. invariant(x,y,e) -> best(x,y)
 }
 
-let bresenham =
+let bresenham () =
   let x = ref 0 in
   let y = ref 0 in
   let e = ref (2 * y2 - x2) in

src/ide/ide_main.ml

@@ -154,7 +154,7 @@ let main () =
       ~packing:top_box#add ()
   in
   ignore (button#connect#clicked
-	    (fun () -> Format.printf "Andrei, tu es trop fort !@."));
+	    ~callback:(fun () -> Format.printf "Andrei, tu es trop fort !@."));
 
   (* horizontal paned *)
   let hp = GPack.paned `HORIZONTAL  ~border_width:3 ~packing:vbox#add () in
@@ -198,6 +198,6 @@ let () =
 
 (*
 Local Variables: 
-compile-command: "unset LANG; make -C ../.. ide-opt-yes"
+compile-command: "unset LANG; make -C ../.. bin/whyide.opt"
 End: 
 *)

src/programs/pgm_parser.mly

@@ -88,6 +88,10 @@
       pc_pre         = p;
       pc_post        = q; }
 
+  let cast_body c ((p,e,q) as t) = match c with
+    | None -> t
+    | Some pt -> p, { e with expr_desc = Ecast (e, pt) }, q
+
 %}
 
 /* Tokens */ 
@@ -181,11 +185,9 @@ list1_decl:
 
 decl:
 | LOGIC
-    { Dlogic $1 (*(logic_list0_decl $1)*) }
-| LET lident EQUAL expr
-    { Dlet ($2, $4) }
-| LET lident list1_type_v_binder EQUAL triple
-    { Dlet ($2, mk_expr_i 3 (Efun ($3, $5))) }
+    { Dlogic $1 }
+| LET lident list1_type_v_binder opt_cast EQUAL triple
+    { Dlet ($2, mk_expr_i 3 (Efun ($3, cast_body $4 $6))) }
 | LET REC list1_recfun_sep_and 
     { Dletrec $3 }
 | PARAMETER lident COLON type_v
@@ -202,8 +204,8 @@ list1_recfun_sep_and:
 ;
 
 recfun:
-| lident list1_type_v_binder opt_variant EQUAL triple
-   { $1, $2, $3, $5 }
+| lident list1_type_v_binder opt_cast opt_variant EQUAL triple
+   { $1, $2, $4, cast_body $3 $6 }
 ;
 
 lident:
@@ -506,6 +508,11 @@ opt_variant:
 | VARIANT LOGIC FOR lqualid { Some ($2, $4) }
 ;
 
+opt_cast:
+| /* epsilon */   { None }
+| COLON pure_type { Some $2 }
+;
+
 list0_lident_sep_comma:
 | /* epsilon */          { [] }
 | list1_lident_sep_comma { $1 }

src/programs/pgm_typing.ml

@@ -671,7 +671,7 @@ End:
 TODO:
 - tuples
 
-- mutually recursive functions: check variants are all present or all absent
+- mutually recursive functions: allow only one order relation specified
 
 - program symbol table outside of the theory
 

tests/test-pgm-jcf.mlw

@@ -11,10 +11,10 @@ exception Found of int
 
 let test_raise (x:bool) = raise Not_found : int 
 
-let test (n:int) = 
+let test (n:int) : int = 
   let rec is_even (x:int) = 
     {true} 
-    is_even x : int
+    is_even x
     {true}
   in
   is_even n
@@ -24,7 +24,7 @@ logic rel(int, int)
 logic rel2(int, int)
 }
 
-let rec is_even (x:int) variant {x} for rel = 
+let rec is_even (x:int) : bool variant {x} for rel = 
     {x>=1} 
     if x = 0 then True else not (is_odd (x-1))
     {true}
@@ -32,8 +32,6 @@ let rec is_even (x:int) variant {x} for rel =
 and is_odd (x:int) variant {x} for rel =
   if x = 0 then False else not (is_even (x-1))
 
-let b = is_even 2
-
 let rec mem (x:int) (l:int list) = 
   { true }
   match l with
@@ -42,7 +40,7 @@ let rec mem (x:int) (l:int list) =
   end
   { true }
 
-let p =
+let p () =
   let x = ref 0 in
   x := 1;
   assert { !x = 1 };
@@ -59,7 +57,7 @@ parameter g : x:int -> y:int ref -> { true } int { result = x + old(!y) }
 
 parameter r : int ref
 
-let foo = g 2 r
+let foo () = g 2 r
 
 let p12 () =
   let x = any int in