programs: syntax for recursive functions; still more typing

src/programs/pgm_main.ml

@@ -73,13 +73,7 @@ let type_file file =
   let uc = Theory.create_theory (Ident.id_fresh "Pgm") in
   let th = Env.find_theory env ["programs"] "Prelude" in
   let uc = Theory.use_export uc th in
-  let _uc = 
-    List.fold_left
-      (fun uc d -> match d with
-	 | Dlogic dl -> List.fold_left (Typing.add_decl env Mnm.empty) uc dl
-	 | Dcode (id, e) -> ignore (Pgm_typing.code uc id e); uc)
-      uc p
-  in
+  let _uc, _dl = Pgm_typing.file env uc p in
   ()
 
 let handle_file file =

src/programs/pgm_parser.mly

@@ -179,11 +179,21 @@ decl:
 | LOGIC
     { Dlogic (logic_list0_decl $1) }
 | LET lident EQUAL expr
-    { Dcode ($2, $4) }
+    { Dlet ($2, $4) }
 | LET lident list1_type_v_binder EQUAL triple
-    { Dcode ($2, let p,e,q = $5 in mk_expr_i 3 (Efun ($3, p, e, q))) }
-| LET REC lident list1_type_v_binder opt_variant EQUAL triple
-    { Dcode ($3, let p,e,q = $7 in mk_expr_i 3 (Erec ($3, $4, $5, p, e, q))) }
+    { Dlet ($2, mk_expr_i 3 (Efun ($3, $5))) }
+| LET REC list1_recfun_sep_and 
+    { Dletrec $3 }
+;
+
+list1_recfun_sep_and:
+| recfun                          { [ $1 ] }
+| recfun AND list1_recfun_sep_and { $1 :: $3 }
+;
+
+recfun:
+| lident list1_type_v_binder opt_variant EQUAL triple
+   { $1, $2, $3, $5 }
 ;
 
 lident:
@@ -254,13 +264,11 @@ expr:
 | LET lident EQUAL expr IN expr
    { mk_expr (Elet ($2, $4, $6)) }
 | LET lident list1_type_v_binder EQUAL triple IN expr
-   { let p,e,q = $5 in 
-     mk_expr (Elet ($2, mk_expr_i 3 (Efun ($3, p, e, q)), $7)) }
-| LET REC lident list1_type_v_binder opt_variant EQUAL triple IN expr
-   { let p,e,q = $7 in 
-     mk_expr (Elet ($3, mk_expr_i 3 (Erec ($3, $4, $5, p, e, q)), $9)) }
+   { mk_expr (Elet ($2, mk_expr_i 3 (Efun ($3, $5)), $7)) }
+| LET REC list1_recfun_sep_and IN expr
+   { mk_expr (Eletrec ($3, $5)) }
 | FUN list1_type_v_binder ARROW triple
-   { let p,e,q = $4 in mk_expr (Efun ($2, p, e, q)) }
+   { mk_expr (Efun ($2, $4)) }
 | MATCH list1_expr_sep_comma WITH option_bar match_cases END
    { mk_expr (Ematch ($2, $5)) }
 | GHOST expr

src/programs/pgm_ptree.ml

@@ -53,6 +53,8 @@ and type_c =
 
 type variant = lexpr 
 
+type binder = ident * type_v option
+
 type expr = {
   expr_desc : expr_desc;
   expr_loc  : loc;
@@ -63,10 +65,9 @@ and expr_desc =
   | Econstant of constant
   | Eident of qualid
   | Eapply of expr * expr
+  | Efun of binder list * triple
   | Elet of ident * expr * expr
-  | Efun of (ident * type_v option) list * lexpr * expr * lexpr
-  | Erec of ident * 
-      (ident * type_v option) list * variant option * lexpr * expr * lexpr
+  | Eletrec of (ident * binder list * variant option * triple) list * expr
   (* control *)
   | Esequence of expr * expr
   | Eif of expr * expr * expr
@@ -84,9 +85,12 @@ and expr_desc =
   (* TODO: raise, try, any, post?, 
            ghost *)
 
+and triple = lexpr * expr * lexpr
+
 type decl =
-  | Dcode  of ident * expr
-  | Dlogic of Ptree.decl list
+  | Dlet    of ident * expr
+  | Dletrec of (ident * binder list * variant option * triple) list
+  | Dlogic  of Ptree.decl list
 
 type file = decl list
 

src/programs/pgm_ttree.ml

@@ -29,8 +29,24 @@ type lazy_op = Pgm_ptree.lazy_op
 
 (* phase 1: destructive typing *)
 
+type deffect = string list
+
 type dtype_v = 
   | DTpure of Denv.dty
+  | DTarrow of (string * dtype_v) list * dtype_c
+
+and dtype_c = 
+  { dc_result_name : Term.vsymbol;
+    dc_result_type : dtype_v;
+    dc_effect      : deffect;
+    dc_pre         : Ptree.lexpr;
+    dc_post        : Ptree.lexpr; }
+
+type dvariant = Pgm_ptree.lexpr 
+
+type dbinder = string * dtype_v
+
+type dlexpr = Typing.denv * Ptree.lexpr
 
 type dexpr = {
   dexpr_desc : dexpr_desc;
@@ -44,7 +60,9 @@ and dexpr_desc =
   | DElocal of string
   | DEglobal of Term.lsymbol
   | DEapply of dexpr * dexpr
+  | DEfun of dbinder list * dtriple
   | DElet of string * dexpr * dexpr
+  | DEletrec of (string * dbinder list * dvariant option * dtriple) * dexpr
 
   | DEsequence of dexpr * dexpr
   | DEif of dexpr * dexpr * dexpr
@@ -57,11 +75,30 @@ and dexpr_desc =
   | DEghost of dexpr
   | DElabel of string * dexpr
 
+and dtriple = dlexpr * dexpr * dlexpr
+
 (* phase 2: typing annotations *)
 
+type variant = Term.term
+
+type effect = Term.vsymbol list
+
+type type_v = 
+  | Tpure of Ty.ty
+  | Tarrow of Term.vsymbol list * type_c
+
+and type_c = 
+  { pc_result_name : Term.vsymbol;
+    pc_result_type : type_v;
+    pc_effect      : effect;
+    pc_pre         : Term.fmla;
+    pc_post        : Term.fmla; }
+
+type binder = Term.vsymbol * type_v
+
 type loop_annotation = {
   loop_invariant : Term.fmla option;
-  loop_variant   : Term.term option;
+  loop_variant   : variant option;
 }
 
 type expr = {
@@ -75,6 +112,7 @@ and expr_desc =
   | Elocal of Term.vsymbol
   | Eglobal of Term.lsymbol
   | Eapply of expr * expr
+  | Efun of binder list * triple
   | Elet of Term.vsymbol * expr * expr
 
   | Esequence of expr * expr
@@ -88,6 +126,12 @@ and expr_desc =
   | Eghost of expr
   | Elabel of string * expr
 
+and triple = Term.fmla * expr * Term.fmla
+
+type decl =
+  | Dlet of Term.lsymbol * expr
+  | Dletrec of (Term.lsymbol * Term.vsymbol list * variant option * triple) list
+
 (*
 Local Variables: 
 compile-command: "unset LANG; make -C ../.. testl"

src/programs/pgm_typing.ml

@@ -21,6 +21,7 @@ open Format
 open Why
 open Util
 open Ident
+open Ty
 open Term
 open Theory
 open Denv
@@ -51,35 +52,53 @@ let report fmt = function
   | Message s ->
       fprintf fmt "%s" s
 
-(*** from Typing *************************************************************)
-type denv = {
+let id_result = "result"
+
+(* environments *)
+
+type global_env = {
   uc : theory_uc;
-  denv : Typing.denv;
   (* predefined symbols from theory programs.Prelude *)
   ty_bool  : dty;
   ty_unit  : dty;
+  ty_label : dty;
   ts_arrow : Ty.tysymbol;
 }
 
-let create_denv uc = 
+let create_global_env uc =
   let ns = get_namespace uc in
   { uc = uc;
-    denv = Typing.create_denv uc;
     ty_bool  = Tyapp (ns_find_ts ns ["bool"], []);
     ty_unit  = Tyapp (ns_find_ts ns ["unit"], []);
+    ty_label = Tyapp (ns_find_ts ns ["label"], []);
     ts_arrow = ns_find_ts ns ["arrow"];
+  }
 
+type denv = {
+  genv : global_env;
+  denv : Typing.denv;
+}
+
+let create_denv genv = 
+  { genv = genv;
+    denv = Typing.create_denv genv.uc;
   }
-(*****************************************************************************)
 
 let create_type_var loc =
   let tv = Ty.create_tvsymbol (id_user "a" loc) in
   Tyvar (create_ty_decl_var ~loc ~user:false tv)
 
-let currying env tyl ty =
-  let make_arrow_type ty1 ty2 = Tyapp (env.ts_arrow, [ty1; ty2]) in
+let currying genv tyl ty =
+  let make_arrow_type ty1 ty2 = Tyapp (genv.ts_arrow, [ty1; ty2]) in
   List.fold_right make_arrow_type tyl ty
 
+let uncurrying genv ty =
+  let rec uncurry acc ty = match ty.ty_node with
+    | Ty.Tyapp (ts, [t1; t2]) when ts == genv.ts_arrow -> uncurry (t1 :: acc) t2
+    | _ -> List.rev acc, ty
+  in
+  uncurry [] ty
+
 let expected_type e ty =
   if not (Denv.unify e.dexpr_type ty) then
     errorm ~loc:e.dexpr_loc 
@@ -94,6 +113,19 @@ let rec dtype_v env = function
   | Pgm_ptree.Tpure pt -> DTpure (pure_type env pt)
   | Pgm_ptree.Tarrow _ -> assert false (*TODO*)
 
+let dpurify _env = function
+  | DTpure ty -> ty
+  | DTarrow _ -> assert false (*TODO*)
+
+let dbinder env ({id=x; id_loc=loc}, v) =
+  let v = match v with
+    | Some v -> dtype_v env v 
+    | None -> DTpure (create_type_var loc)
+  in
+  let ty = dpurify env v in
+  let env = { env with denv = Typing.add_var x ty env.denv } in
+  env, (x, v)
+
 let rec dexpr env e = 
   let d, ty = expr_desc env e.Pgm_ptree.expr_loc e.Pgm_ptree.expr_desc in
   { dexpr_desc = d; dexpr_loc = e.Pgm_ptree.expr_loc;
@@ -109,67 +141,72 @@ and expr_desc env loc = function
       let ty = Typing.find_var x env.denv in
       DElocal x, ty
   | Pgm_ptree.Eident p ->
-      let s, tyl, ty = Typing.specialize_fsymbol p env.uc in
-      DEglobal s, currying env tyl ty
+      let s, tyl, ty = Typing.specialize_fsymbol p env.genv.uc in
+      DEglobal s, currying env.genv tyl ty
   | Pgm_ptree.Eapply (e1, e2) ->
       let e1 = dexpr env e1 in
       let e2 = dexpr env e2 in
       begin match e1.dexpr_type with
-	| Tyapp (ts, [ty2; ty]) when Ty.ts_equal ts env.ts_arrow ->
+	| Tyapp (ts, [ty2; ty]) when Ty.ts_equal ts env.genv.ts_arrow ->
 	    expected_type e2 ty2;
 	    DEapply (e1, e2), ty
 	| _ ->
 	    errorm ~loc:e1.dexpr_loc "this expression is not a function"
       end
+  | Pgm_ptree.Efun (bl, t) ->
+      let env, bl = map_fold_left dbinder env bl in
+      let (_,e,_) as t = dtriple env t in
+      let tyl = List.map (fun (x,_) -> Typing.find_var x env.denv) bl in
+      let ty = currying env.genv tyl e.dexpr_type in
+      DEfun (bl, t), ty
   | Pgm_ptree.Elet ({id=x}, e1, e2) ->
       let e1 = dexpr env e1 in
       let ty1 = e1.dexpr_type in
       let env = { env with denv = Typing.add_var x ty1 env.denv } in
       let e2 = dexpr env e2 in
       DElet (x, e1, e2), e2.dexpr_type
-  | Pgm_ptree.Efun _ (*(bl, p, e, q)*) ->
-      assert false (*TODO*)
-  | Pgm_ptree.Erec _ (*(id, bl, v, p, e, q)*) ->
+  | Pgm_ptree.Eletrec _ (*(id, bl, v, p, e, q)*) ->
       assert false (*TODO*)
 
   | Pgm_ptree.Esequence (e1, e2) ->
       let e1 = dexpr env e1 in
-      expected_type e1 env.ty_unit;
+      expected_type e1 env.genv.ty_unit;
       let e2 = dexpr env e2 in
       DEsequence (e1, e2), e2.dexpr_type
   | Pgm_ptree.Eif (e1, e2, e3) ->
       let e1 = dexpr env e1 in
-      expected_type e1 env.ty_bool;
+      expected_type e1 env.genv.ty_bool;
       let e2 = dexpr env e2 in
       let e3 = dexpr env e3 in
       expected_type e3 e2.dexpr_type;
       DEif (e1, e2, e3), e2.dexpr_type
   | Pgm_ptree.Ewhile (e1, a, e2) ->
       let e1 = dexpr env e1 in
-      expected_type e1 env.ty_bool;
+      expected_type e1 env.genv.ty_bool;
       let e2 = dexpr env e2 in
-      expected_type e2 env.ty_unit;
-      DEwhile (e1, a, e2), env.ty_unit
+      expected_type e2 env.genv.ty_unit;
+      DEwhile (e1, a, e2), env.genv.ty_unit
   | Pgm_ptree.Elazy (op, e1, e2) ->
       let e1 = dexpr env e1 in
-      expected_type e1 env.ty_bool;
+      expected_type e1 env.genv.ty_bool;
       let e2 = dexpr env e2 in
-      expected_type e2 env.ty_bool;
-      DElazy (op, e1, e2), env.ty_bool
+      expected_type e2 env.genv.ty_bool;
+      DElazy (op, e1, e2), env.genv.ty_bool
   | Pgm_ptree.Ematch (_el, _bl) ->
       assert false (*TODO*)
   | Pgm_ptree.Eskip ->
-      DEskip, env.ty_unit
+      DEskip, env.genv.ty_unit
   | Pgm_ptree.Eabsurd ->
       DEabsurd, create_type_var loc
 
   | Pgm_ptree.Eassert (k, le) ->
-      DEassert (k, le), env.ty_unit
+      DEassert (k, le), env.genv.ty_unit
   | Pgm_ptree.Eghost e1 ->
       let e1 = dexpr env e1 in
       DEghost e1, e1.dexpr_type
   | Pgm_ptree.Elabel ({id=l}, e1) ->
-      (* TODO: add label to env *)
+      let ty = env.genv.ty_label in
+      let env = { env with denv = Typing.add_var l ty env.denv } in
       let e1 = dexpr env e1 in
       DElabel (l, e1), e1.dexpr_type
   | Pgm_ptree.Ecast (e1, ty) ->
@@ -178,8 +215,30 @@ and expr_desc env loc = function
       expected_type e1 ty;
       e1.dexpr_desc, ty
 
+and dtriple env (p, e, q) =     
+  let p = env.denv, p in
+  let e = dexpr env e in
+  let ty = e.dexpr_type in
+  let denvq = Typing.add_var id_result ty env.denv in
+  let q = denvq, q in
+  (p, e, q)
+
 (* phase 2: typing annotations *)
 
+let rec type_v = function
+  | DTpure ty -> Tpure (Denv.ty_of_dty ty)
+  | DTarrow _ -> assert false (*TODO*)
+
+let purify = function
+  | Tpure ty -> ty
+  | Tarrow _ -> assert false (*TODO*)
+
+let binder env (x, tyv) = 
+  let tyv = type_v tyv in
+  let v = create_vsymbol (id_fresh x) (purify tyv) in
+  let env = Mstr.add x v env in
+  env, (v, tyv)
+
 let rec expr env e =
   let d = expr_desc env e.dexpr_denv e.dexpr_desc in
   let ty = Denv.ty_of_dty e.dexpr_type in
@@ -194,11 +253,16 @@ and expr_desc env denv = function
       Eglobal ls
   | DEapply (e1, e2) ->
       Eapply (expr env e1, expr env e2)
+  | DEfun (bl, e1) ->
+      let env, bl = map_fold_left binder env bl in
+      Efun (bl, triple env e1)
   | DElet (x, e1, e2) ->
       let e1 = expr env e1 in
       let v = create_vsymbol (id_fresh x) e1.expr_type in
       let env = Mstr.add x v env in
       Elet (v, e1, expr env e2)
+  | DEletrec _ ->
+      assert false (*TODO*)
 
   | DEsequence (e1, e2) ->
       Esequence (expr env e1, expr env e2)
@@ -225,12 +289,41 @@ and expr_desc env denv = function
   | DEghost e1 -> 
       Eghost (expr env e1)
   | DElabel (s, e1) ->
+      let ty = Denv.ty_of_dty (Typing.find_var s e1.dexpr_denv) in
+      let v = create_vsymbol (id_fresh s) ty in
+      let env = Mstr.add s v env in 
       Elabel (s, expr env e1)
 
-let code uc _id e =
-  let env = create_denv uc in
-  let e = dexpr env e in
-  ignore (expr Mstr.empty e)
+and triple env ((denvp, p), e, (denvq, q)) =
+  let p = Typing.type_fmla denvp env p in
+  let e = expr env e in
+  let v_result = create_vsymbol (id_fresh id_result) e.expr_type in
+  let envq = Mstr.add id_result v_result env in
+  let q = Typing.type_fmla denvq envq q in
+  (p, e, q)
+
+let type_expr genv e =
+  let denv = create_denv genv in
+  let e = dexpr denv e in
+  expr Mstr.empty e
+
+let file env uc dl =
+  let genv = create_global_env uc in
+  let uc, dl =
+    List.fold_left
+      (fun (uc, acc) d -> match d with
+	 | Pgm_ptree.Dlogic dl -> 
+	     List.fold_left (Typing.add_decl env Mnm.empty) uc dl, acc
+	 | Pgm_ptree.Dlet (id, e) -> 
+	     let e = type_expr genv e in
+	     let tyl, ty = uncurrying genv e.expr_type in
+	     let ls = create_lsymbol (id_user id.id id.id_loc) tyl (Some ty) in
+	     uc, Dlet (ls, e) :: acc
+	 | Pgm_ptree.Dletrec _ -> 
+	     assert false (*TODO*))
+      (uc, []) dl
+  in
+  uc, List.rev dl
 
 (*
 Local Variables: 

tests/test-pgm-jcf.mlw

@@ -3,6 +3,7 @@
 use import list.List
 }
 
+(*
 let rec mem (x:int) (l:int list) = 
   { true }
   match l with
@@ -10,19 +11,20 @@ let rec mem (x:int) (l:int list) =
   | Cons (y, r) -> x = y || mem x r
   end
   { true }
+*)
 
 let p =
   let x = ref 0 in
   x := 1;
   assert { !x = 1 };
   label L:
-  assume { !x = 2 };
+  assume { at(!x, L) = 2 };
   absurd : int ref
 
-let f (x : int) = 
-  { x >= 0 }
-  (fun y -> { y >= 0 } y+1 { result > y }) x
-  { result > 0 }
+let f (x : int ref) = 
+  { !x >= 0 }
+  (fun y -> { y >= 0 } y+1 { result > y }) 2
+  { result > 0 and old(!x)>=0 }
 
 (*
 Local Variables: