programs in progress

src/programs/pgm_itree.ml

@@ -52,6 +52,8 @@ type expr = {
 
 and expr_desc =
   | Elogic of Term.term
+  | Elocal of Term.vsymbol
+  | Eglobal of Term.lsymbol
   | Efun of binder list * triple
   | Elet of Term.vsymbol * expr * expr
   | Eletrec of recfun list * expr

src/programs/pgm_typing.mli

@@ -24,6 +24,8 @@ type error
 
 exception Error of error
 
+val errorm : ?loc:Loc.position -> ('a, Format.formatter, unit, 'b) format4 -> 'a
+
 val report : Format.formatter -> error -> unit
 
 val file : Env.env -> theory_uc -> Pgm_ptree.file -> theory_uc * Pgm_ttree.file

src/programs/pgm_wp.ml

@@ -26,6 +26,8 @@ open Pgm_itree
 
 module E = Pgm_effect
 
+let errorm = Pgm_typing.errorm
+
 (* translation to intermediate trees and effect inference *)
 
 let rec expr e =
@@ -34,9 +36,22 @@ let rec expr e =
   let d, ef = expr_desc loc ty e.Pgm_ttree.expr_desc in
   { expr_desc = d; expr_type = ty; expr_effect = ef; expr_loc = loc }
 
-and expr_desc _loc ty = function
+and expr_desc loc ty = function
   | Pgm_ttree.Econstant c ->
       Elogic (t_const c ty), E.empty
+  | Pgm_ttree.Elogic ls ->
+      begin match ls.ls_args with
+	| [] -> 
+	    Elogic (t_app ls [] ty), E.empty
+	| al -> 
+	    errorm ~loc "function symbol %s is expecting %d arguments"
+	      ls.ls_name.id_string (List.length al)
+      end
+  | Pgm_ttree.Eapply _ as e ->
+      assert false (*TODO*)
+  | Pgm_ttree.Efun (_bl, (p, e, q)) ->
+      let e = expr e in
+      assert false (*TODO*)
   | _ -> 
       assert false (*TODO*)
 

tests/test-pgm-jcf.mlw

 
 { 
 use import list.List
+logic f(int, int) : int
 logic c : int
 }
 
-let ff () = { } 1+2 { result = 3 }
+let ff () = { } f 1 2 { result = result }
 
 
 (*