program API: arrow types

src/util/util.ml

@@ -182,6 +182,11 @@ let rec chop n l =
   else if n < 0 || l = [] then invalid_arg "Util.chop"
   else chop (n - 1) (List.tl l)
 
+let rec chop_last = function
+  | [] -> invalid_arg "Util.chop_last"
+  | [r] -> [], r
+  | x :: s -> let s, r = chop_last s in x :: s, r
+
 (* boolean fold accumulators *)
 
 exception FoldSkip

src/util/util.mli

@@ -126,6 +126,8 @@ val prefix : int -> 'a list -> 'a list
 val chop : int -> 'a list -> 'a list
   (** removes the first n elements of a list;
       raises Invalid_argument if the list is not long enough *)
+val chop_last : 'a list -> 'a list * 'a
+  (** removes (and returns) the last element of a list *)
 
 (* boolean fold accumulators *)
 

src/whyml/mlw_decl.ml

@@ -77,12 +77,15 @@ type pre_ity_defn =
 
 type pre_ity_decl = itysymbol * pre_ity_defn
 
+exception ConstantConstructor of ident
+
 let create_ity_decl tdl =
   let syms = ref Sid.empty in
   let add s (its,_) = news_id s its.its_pure.ts_name in
   let news = ref (List.fold_left add Sid.empty tdl) in
   let projections = Hvs.create 17 in (* vs -> ps_ls *)
   let build_constructor its (id, al) =
+    if al = [] then raise (ConstantConstructor (id_register id));
     (* check well-formedness *)
     let tvs = List.fold_right Stv.add its.its_args Stv.empty in
     let regs = List.fold_right Sreg.add its.its_regs Sreg.empty in
@@ -105,9 +108,10 @@ let create_ity_decl tdl =
     let add_erase ef r = eff_union ef (eff_erase r) in
     let add_erase ef (pv,_) = option_fold add_erase ef pv.pv_mutable in
     let effect = List.fold_left add_erase eff_empty al in
-    let c = create_cty ~post ~effect (vty_value result) in
-    let arrow (pv,_) c = create_cty (vty_arrow pv c) in
-    let v = (List.fold_right arrow al c).c_vty in
+    let al, (a, _) = Util.chop_last al in
+    let c = vty_arrow a ~post ~effect (vty_value result) in
+    let arrow (pv,_) c = vty_arrow pv c in
+    let v = List.fold_right arrow al c in
     let ps = create_psymbol id Stv.empty Sreg.empty v in
     let ps_ls = { ps = ps; ls = ls } in
     news := Sid.add ps.p_name !news;
@@ -119,7 +123,7 @@ let create_ity_decl tdl =
       let post = t_equ (t_var pv.pv_vs) t in
       let add_read ef r = eff_union ef (eff_read r) in
       let effect = option_fold add_read eff_empty pv.pv_mutable in
-      let vty = vty_arrow result (create_cty ~post ~effect (vty_value pv)) in
+      let vty = vty_arrow result ~post ~effect (vty_value pv) in
       let ps = create_psymbol id Stv.empty Sreg.empty vty in
       let ps_ls = { ps = ps; ls = ls } in
       news := Sid.add ps.p_name !news;

src/whyml/mlw_expr.ml

@@ -60,7 +60,7 @@ type expr = private {
 and expr_node =
   | Elogic  of term
   | Esym    of psymbol (* function *)
-  | Eapp    of psymbol * expr * cty
+  | Eapp    of psymbol * expr
   | Elet    of psymbol * expr * expr
   | Eletrec of recfun list * expr
   | Efun    of lambda

src/whyml/mlw_expr.mli

@@ -54,7 +54,7 @@ type expr = private {
 and expr_node = private
   | Elogic  of term
   | Esym    of psymbol (* function *)
-  | Eapp    of psymbol * expr * cty
+  | Eapp    of psymbol * expr
   | Elet    of psymbol * expr * expr
   | Eletrec of recfun list * expr
   | Efun    of lambda

src/whyml/mlw_pretty.ml

@@ -108,8 +108,9 @@ let print_ty_arg fmt ty = fprintf fmt "@ %a" (print_ity_node true) ty
 let print_constr fmt (cs,pjl) =
   let rec cs_args vty pjl = match vty, pjl with
     | VTvalue _, [] -> []
-    | VTarrow (pv,cty), pj::pjl ->
-        (pv,pj) :: cs_args cty.c_vty pjl
+    | VTarrow a, pj::pjl ->
+        let pv, vty = open_vty_arrow a in
+        (pv,pj) :: cs_args vty pjl
     | _, _ -> assert false
   in
   let pjl = cs_args cs.ps.p_vty pjl in

src/whyml/mlw_ty.ml

@@ -186,7 +186,7 @@ let ity_v_all prv prr ity =
 let ity_v_any prv prr ity =
   try ity_v_fold (any_fn prv) (any_fn prr) false ity with FoldSkip -> true
 
-let ity_full_inst mv mr ity =
+let ity_subst mv mr ity =
   ity_v_map (fun v -> Mtv.find v mv) (fun r -> Mreg.find r mr) ity
 
 let ity_freevars = ity_v_fold (fun s v -> Stv.add v s) Util.const
@@ -209,6 +209,9 @@ exception TypeMismatch of ity * ity
 let ity_equal_check ty1 ty2 =
   if not (ity_equal ty1 ty2) then raise (TypeMismatch (ty1, ty2))
 
+let reg_equal_check r1 r2 =
+  if not (reg_equal r1 r2) then raise (RegionMismatch (r1, r2))
+
 type ity_subst = {
   ity_subst_tv  : ity Mtv.t;
   ity_subst_reg : region Mreg.t;
@@ -219,12 +222,27 @@ let ity_subst_empty = {
   ity_subst_reg = Mreg.empty;
 }
 
+let ity_subst_union s1 s2 =
+  let check_ity _ ity1 ity2 = ity_equal_check ity1 ity2; Some ity1 in
+  let check_reg _ r1 r2 = reg_equal_check r1 r2; Some r1 in
+  { ity_subst_tv  = Mtv.union  check_ity s1.ity_subst_tv  s2.ity_subst_tv;
+    ity_subst_reg = Mreg.union check_reg s1.ity_subst_reg s2.ity_subst_reg }
+
+let reg_inst s r =
+  Mreg.find_def r r s.ity_subst_reg
+
+let reg_full_inst s r =
+  Mreg.find r s.ity_subst_reg
+
 let ity_inst s ity =
   ity_v_map
     (fun v -> Mtv.find_def (ity_var v) v s.ity_subst_tv)
     (fun r -> Mreg.find_def r r s.ity_subst_reg)
     ity
 
+let ity_full_inst s ity =
+  ity_subst s.ity_subst_tv s.ity_subst_reg ity
+
 let rec ity_match s ity1 ity2 =
   let set = function
     | None -> Some ity2
@@ -296,7 +314,7 @@ let ity_app_fresh s tl =
   let mr,rl = Util.map_fold_left (reg_refresh mv) Mreg.empty s.its_regs in
   (* every external region in def is guaranteed to be in mr *)
   match s.its_def with
-  | Some ity -> ity_full_inst mv mr ity
+  | Some ity -> ity_subst mv mr ity
   | None -> ity_app s tl rl
 
 let ity_app s tl rl =
@@ -316,14 +334,14 @@ let ity_app s tl rl =
   ignore (List.fold_left2 rmatch sub s.its_regs rl);
   (* to instantiate def, mv and mr are enough *)
   match s.its_def with
-  | Some ity -> ity_full_inst mv mr ity
+  | Some ity -> ity_subst mv mr ity
   | None -> ity_app s tl rl
 
 let ity_pur s tl = match s.ts_def with
   | Some ty ->
       let add m v t = Mtv.add v t m in
       let m = List.fold_left2 add Mtv.empty s.ts_args tl in
-      ity_full_inst m Mreg.empty (ity_of_ty ty)
+      ity_subst m Mreg.empty (ity_of_ty ty)
   | None ->
       ity_pur s tl
 
@@ -411,6 +429,9 @@ let eff_erase r = { eff_empty with eff_erases = Sreg.singleton r }
 let eff_raise xs = { eff_empty with eff_raises = Sexn.singleton xs }
 let eff_remove_raise xs e = { e with eff_raises = Sexn.remove xs e.eff_raises }
 
+let eff_full_inst _s _ef =
+  assert false (*TODO*)
+
 (* program variables *)
 type pvsymbol = {
   pv_vs      : vsymbol;
@@ -419,6 +440,16 @@ type pvsymbol = {
   pv_mutable : region option;
 }
 
+module Pv = StructMake (struct
+  type t = pvsymbol
+  let tag pv = Hashweak.tag_hash pv.pv_vs.vs_name.id_tag
+end)
+
+module Spv = Pv.S
+module Mpv = Pv.M
+
+let pv_equal : pvsymbol -> pvsymbol -> bool = (==)
+
 exception InvalidPVsymbol of ident
 
 let create_pvsymbol id ?mut ?(ghost=false) ity =
@@ -435,43 +466,93 @@ let create_pvsymbol id ?mut ?(ghost=false) ity =
     pv_ghost = ghost;
     pv_mutable = mut; }
 
-let pv_equal : pvsymbol -> pvsymbol -> bool = (==)
+let pv_full_inst s pv =
+  let ghost = pv.pv_ghost in
+  let mut = option_map (reg_full_inst s) pv.pv_mutable in
+  let ity = ity_full_inst s pv.pv_ity in
+  create_pvsymbol (id_clone pv.pv_vs.vs_name) ~ghost ?mut ity
 
 (* value types *)
+type pre = term
+type post = term
+type xpost = (pvsymbol * post) Mexn.t
+
 type vty =
   | VTvalue of pvsymbol
-  | VTarrow of pvsymbol * cty
+  | VTarrow of vty_arrow
 
 (* computation types *)
-and cty = {
-  c_pre   : term;
+and vty_arrow = {
+  c_arg   : pvsymbol; (* formal argument *)
+  c_pre   : pre;
   c_vty   : vty;
   c_eff   : effect;
-  c_post  : term;
+  c_post  : post;
   c_xpost : xpost;
+  c_subst : ity_subst;      (* not yet applied to the 5 fields above *)
+  c_pvmap : pvsymbol Mpv.t; (* idem *)
 }
 
-and xpost = (pvsymbol * term) Mexn.t
-
 (* smart constructors *)
-let create_cty
-  ?(pre=t_true) ?(post=t_true) ?(xpost=Mexn.empty) ?(effect=eff_empty) vty =
-  { c_pre = pre;
-    c_vty = vty;
-    c_eff = effect;
-    c_post = post;
-    c_xpost = xpost; }
-(* TODO/FIXME: in xpost, the type of pvsymbol must coincide with
-   that of the exception *)
 
 let vty_value pvs = VTvalue pvs
 
-let vty_arrow x cty =
+exception InvalidExceptionPost of xsymbol * pvsymbol
+
+let check_xpost xs (pv, _) =
+  if not (ity_equal xs.xs_ity pv.pv_ity) then
+    raise (InvalidExceptionPost (xs, pv))
+
+let vty_arrow
+  x ?(pre=t_true) ?(post=t_true) ?(xpost=Mexn.empty) ?(effect=eff_empty) vty =
   (* check that x does not appear in cty *)
   let rec check = function
-    | VTvalue y -> if pv_equal x y then raise (DuplicateVar x.pv_vs)
-    | VTarrow (y, c) ->
-        if pv_equal x y then raise (DuplicateVar x.pv_vs); check c.c_vty
+    | VTvalue y | VTarrow { c_arg = y } when pv_equal x y ->
+        raise (DuplicateVar x.pv_vs)
+    | VTarrow { c_vty = v } ->
+        check v
+    | VTvalue _ ->
+        ()
   in
-  check cty.c_vty;
-  VTarrow (x, cty)
+  check vty;
+  Mexn.iter check_xpost xpost;
+  VTarrow {
+    c_arg = x;
+    c_pre = pre;
+    c_vty = vty;
+    c_eff = effect;
+    c_post = post;
+    c_xpost = xpost;
+    c_subst = ity_subst_empty;
+    c_pvmap = Mpv.empty;
+  }
+
+exception NotAFunction
+
+let get_arrow = function
+  | VTvalue _ -> raise NotAFunction
+  | VTarrow a -> a
+
+let vty_full_inst ~ghost s = function
+  | VTvalue pv ->
+      let pv = pv_full_inst s pv in
+      VTvalue { pv with pv_ghost = ghost || pv.pv_ghost }
+  | VTarrow _a ->
+      assert false (*TODO*)
+
+let vty_app_arrow subst a pv =
+  let s = ity_subst_union subst a.c_subst in
+  let s = ity_match s a.c_arg.pv_ity pv.pv_ity in
+  eff_full_inst s a.c_eff, vty_full_inst ~ghost:pv.pv_ghost s a.c_vty
+
+let vty_app subst v pv =
+  vty_app_arrow subst (get_arrow v) pv
+
+let vty_app_spec _subst _v _pv (* : pre * post * xpost *) =
+  assert false (*TODO*)
+
+let open_vty_arrow a =
+  let pv = pv_full_inst a.c_subst a.c_arg in
+  pv, snd (vty_app_arrow ity_subst_empty a pv)
+
+

src/whyml/mlw_ty.mli

@@ -185,25 +185,29 @@ val create_pvsymbol : preid -> ?mut:region -> ?ghost:bool -> ity -> pvsymbol
 val pv_equal : pvsymbol -> pvsymbol -> bool
 
 (* value types *)
+type vty_arrow
+
 type vty = private
   | VTvalue of pvsymbol
-  | VTarrow of pvsymbol * cty
-
-(* computation types *)
-and cty = private {
-  c_pre   : term;
-  c_vty   : vty;
-  c_eff   : effect;
-  c_post  : term;
-  c_xpost : xpost;
-}
-
-and xpost = (pvsymbol * term) Mexn.t
+  | VTarrow of vty_arrow
 
 (* smart constructors *)
-val create_cty :
-  ?pre:term -> ?post:term -> ?xpost:xpost -> ?effect:effect -> vty -> cty
-
 val vty_value : pvsymbol -> vty
-val vty_arrow : pvsymbol -> cty -> vty
+
+type pre = term
+type post = term
+type xpost = (pvsymbol * post) Mexn.t
+
+val vty_arrow :
+  pvsymbol ->
+  ?pre:term -> ?post:term -> ?xpost:xpost -> ?effect:effect -> vty -> vty
+
+val vty_app : ity_subst -> vty -> pvsymbol -> effect * vty
+
+val vty_app_spec : ity_subst -> vty -> pvsymbol -> pre * post * xpost
+
+val open_vty_arrow : vty_arrow -> pvsymbol * vty
+
+
+
 

tests/test-pgm-jcf.mlw

 module M0
-  type t = private int
+  use import module ref.Ref
+
+  let gensym () =
+    let r = ref 0 in
+    (fun () -> {} r := 1 { !r = 1 })
+
+  region rho0
+
+  let rec loop ... =
+    {}
+    let g = f rho0 () erases rho0 in
+    ... g() writes rho0 ...
+    : erases rho0
+    {}
+
 end