program API: expressions (WIP)

src/whyml/mlw_expr.ml

@@ -20,8 +20,14 @@
 open Why3
 open Ident
 open Ty
+open Term
 open Mlw_ty
 
+type variant = {
+  v_term : term;           (* : tau *)
+  v_rel  : lsymbol option; (* tau tau : prop *)
+}
+
 (* program symbols *)
 type psymbol = {
   p_name : ident;
@@ -30,13 +36,15 @@ type psymbol = {
   p_vty  : vty;
 }
 
-let create_psymbol id tvars regs vty = {
-  (* TODO? check that tvars/regs are in vty *)
-  p_name = id_register id;
-  p_tvs  = tvars;
-  p_reg  = regs;
-  p_vty  = vty;
-}
+let create_psymbol id tvars regs = function
+  | VTvalue pv ->
+      let pv =
+        create_pvsymbol id ?mut:pv.pv_mutable ~ghost:pv.pv_ghost pv.pv_ity in
+      { p_name = pv.pv_vs.vs_name;
+        p_tvs = tvars; p_reg = regs; p_vty = vty_value pv; }
+  | VTarrow _ as vty ->
+      (* TODO? check that tvars/regs are in vty *)
+      { p_name = id_register id; p_tvs = tvars; p_reg = regs; p_vty = vty; }
 
 let ps_equal : psymbol -> psymbol -> bool = (==)
 
@@ -44,8 +52,37 @@ type expr = private {
   e_node  : expr_node;
   e_vty   : vty;
   e_eff   : effect;
+  e_ghost : bool;
   e_label : Slab.t;
   e_loc   : Loc.position option;
 }
 
-and expr_node
+and expr_node =
+  | Elogic  of term
+  | Esym    of psymbol (* function *)
+  | Eapp    of psymbol * expr * cty
+  | Elet    of psymbol * expr * expr
+  | Eletrec of recfun list * expr
+  | Efun    of lambda
+  | Eif     of expr * expr * expr
+  | Eassign of pvsymbol * psymbol * region * expr (* e1.f<rho> <- e2 *)
+
+and recfun = psymbol * lambda
+
+and lambda = {
+  l_args    : pvsymbol list;
+  l_variant : variant list; (* lexicographic order *)
+  l_pre     : term;
+  l_body    : expr;
+  l_post    : term;
+  l_xpost   : xpost;
+}
+
+let lapp _ = assert false (*TODO*)
+let papp _ = assert false (*TODO*)
+let app _ = assert false (*TODO*)
+let plet _ = assert false (*TODO*)
+let pletrec _ = assert false (*TODO*)
+let pfun _ = assert false (*TODO*)
+let assign _ = assert false (*TODO*)
+

src/whyml/mlw_expr.mli

@@ -20,6 +20,7 @@
 open Why3
 open Ident
 open Ty
+open Term
 open Mlw_ty
 
 (* program symbols *)
@@ -36,17 +37,45 @@ val ps_equal : psymbol -> psymbol -> bool
 
 (* program expressions *)
 
+type variant = {
+  v_term : term;           (* : tau *)
+  v_rel  : lsymbol option; (* tau tau : prop *)
+}
+
 type expr = private {
   e_node  : expr_node;
   e_vty   : vty;
   e_eff   : effect;
+  e_ghost : bool;
   e_label : Slab.t;
   e_loc   : Loc.position option;
 }
 
-and expr_node
-(*
-  | Letrec of (psymbol * lambda) list * expr
-  | Let of pvsymbol * expr * expr
-*)
+and expr_node = private
+  | Elogic  of term
+  | Esym    of psymbol (* function *)
+  | Eapp    of psymbol * expr * cty
+  | Elet    of psymbol * expr * expr
+  | Eletrec of recfun list * expr
+  | Efun    of lambda
+  | Eif     of expr * expr * expr
+  | Eassign of pvsymbol * psymbol * region * expr (* e1.f<rho> <- e2 *)
+
+and recfun = psymbol * lambda
+
+and lambda = private {
+  l_args    : pvsymbol list;
+  l_variant : variant list; (* lexicographic order *)
+  l_pre     : term;
+  l_body    : expr;
+  l_post    : term;
+  l_xpost   : xpost;
+}
 
+val lapp : lsymbol -> expr list -> expr
+val papp : psymbol -> expr list -> expr
+val app : expr -> expr -> expr
+val plet : psymbol -> expr -> expr -> expr
+val pletrec : recfun list -> expr -> expr
+val pfun : lambda -> expr
+val assign : expr -> psymbol -> expr -> expr

tests/test-jcf.why

 
 theory T
 
-  use import int.Int
-  goal G: let x,y = (1,2) in x=y
+  type t = None | Some int
 
-end
-
-theory TestPVS
-
-  use import bool.Bool
-  use import int.Int
-  use import map.Map
-
-  function m: map int bool
-
-  axiom a: get m 0 = True
-  axiom b: get m 1 = False
-
-  goal G: get (const False) 42 = False
+  goal G: forall x: t. x <> None ->
+          match x with None -> false | Some z -> z = 0 end
 
 end
 

tests/test-pgm-jcf.mlx

@@ -8,6 +8,7 @@ module M
   use import T
   function f (x: t) : t = x+1
   goal G: forall x: t. x=x
+
 end
 
 module N