abstract types within tuples

src/programs/pgm_pretty.ml

@@ -12,7 +12,8 @@ open Pgm_ttree
 
 let rec print_expr fmt e = match e.expr_desc with
   | Elogic t ->
-      fprintf fmt "@[<hov 2><term: %a>@]" Pretty.print_term t
+      fprintf fmt "@[<hov 2><term %a : %a>@]" Pretty.print_term t
+	Pretty.print_ty t.t_ty
   | Elocal v ->
       fprintf fmt "%a" print_pv v
   | Eglobal ls ->
@@ -33,8 +34,8 @@ let rec print_expr fmt e = match e.expr_desc with
 
   | Elabel (_, _)  ->
       fprintf fmt "<todo: Elabel>"
-  | Eassert (_, _) ->
-      fprintf fmt "<todo: Eassert>"
+  | Eassert (_, f) ->
+      fprintf fmt "@[assert {%a}@]" print_fmla f
   | Efor (_, _, _, _, _, _) ->
       fprintf fmt "<todo: Efor>"
   | Etry (_, _) ->
@@ -52,8 +53,7 @@ let rec print_expr fmt e = match e.expr_desc with
       fprintf fmt "absurd"
 
 and print_pv fmt v =
-  fprintf fmt "<@[%s : %a/%a@]>" 
-    v.pv_name.id_string print_ty v.pv_ty print_vs v.pv_vs
+  fprintf fmt "<@[%a : %a@]>" print_vs v.pv_vs print_ty v.pv_ty
 
 and print_triple fmt (p, e, q) =
   fprintf fmt "@[<hv 0>%a@ %a@ %a@]" print_pre p print_expr e print_post q

src/programs/pgm_typing.ml

@@ -717,18 +717,18 @@ let make_logic_app gl loc ty ls el =
   let rec make args = function
     | [] ->
         begin match ls.ls_value with
-          | Some _ -> IElogic (t_app ls (List.rev args) ty)
+          | Some _ -> IElogic (t_app ls (List.rev args) (purify ty))
           | None -> IElogic (mk_t_if gl (f_app ls (List.rev args)))
         end
     | ({ iexpr_desc = IElogic t }, _) :: r ->
 	make (t :: args) r
     | ({ iexpr_desc = IElocal v }, _) :: r ->
-	make (t_var v.i_pgm :: args) r
+	make (t_var v.i_logic :: args) r
     | ({ iexpr_desc = IEglobal (s, _); iexpr_type = ty }, _) :: r ->
 	make (t_app s.p_ls [] ty :: args) r
     | (e, _) :: r ->
 	let v = create_ivsymbol (id_user "x" loc) e.iexpr_type in
-	let d = mk_iexpr loc ty (make (t_var v.i_pgm :: args) r) in
+	let d = mk_iexpr loc ty (make (t_var v.i_logic :: args) r) in
 	IElet (v, e, d)
   in
   make [] el
@@ -1069,13 +1069,7 @@ let rec pattern env p =
   env, { ppat_pat = lp; ppat_node = n }
 
 and pattern_node env ty p = 
-  let add1 env i = 
-    let v = 
-      create_pvsymbol (id_clone i.i_pgm.vs_name) ~vs:i.i_logic 
-	(tpure i.i_pgm.vs_ty) 
-    in
-    Mvs.add i.i_pgm v env, v
-  in
+  let add1 env i = add_local env i (tpure i.i_pgm.vs_ty) in
   match p with
   | IPwild -> 
       env, (pat_wild ty, Pwild)

tests/test-pgm-jcf.mlw

@@ -4,11 +4,10 @@ module P
   use import module stdlib.Ref
   use import module stdlib.Array
 
-  let foo () =
-    {}
-    let a = make 17 42 in
-    a[0]
-    {result=42}
+  abstract type t 'a model 'a
+  parameter t : x:'a -> {} t 'a { result=x }
+
+  let f () = {} (1, t 2) { true }
 
   parameter c : ghost int
 
@@ -16,8 +15,7 @@ module P
 
   let gid (x:int) = {} ghost (c + x) { result=c+x }
 
-  (* FIXME *)
-  (* let gid (x:int) = {} (x, ghost x) { let a,b = result in a=x and b=x } *)
+  let foo (x:int) = {} (x, ghost x) { let a,b = result in a=x and b=x }
 
   (* FIXME : make c a first parameter of gid => then to type gid c y inside
      ghost we should not insert unghost *)