programs: typing variants (in progress)

src/parser/typing.mli

@@ -49,6 +49,9 @@ val report : Format.formatter -> error -> unit
 val specialize_fsymbol : 
   Ptree.qualid -> theory_uc -> lsymbol * Denv.dty list * Denv.dty
 
+val specialize_psymbol : 
+  Ptree.qualid -> theory_uc -> lsymbol * Denv.dty list
+
 val specialize_tysymbol : 
   Loc.position -> Ptree.qualid -> theory_uc -> Ty.tysymbol * int
 
@@ -75,5 +78,6 @@ val dpat_list :
 
 val pattern : vsymbol Mstr.t -> dpattern -> vsymbol Mstr.t * pattern
 
+val qloc : Ptree.qualid -> Loc.position
 
 

src/programs/pgm_parser.mly

@@ -72,6 +72,8 @@
   let id_result () = { id = "result"; id_loc = loc () }
   let id_anonymous () = { id = "_"; id_loc = loc () }
 
+  let id_wf_lt_int () = Qident { id = "wf_lt_int"; id_loc = loc () }
+
   let ty_unit () = Tpure (PPTtyapp ([], Qident (id_unit ())))
 
   let lexpr_true () = symbol_start_pos (), "true"
@@ -380,7 +382,7 @@ assertion_kind:
 ;
 
 loop_annotation:
-| loop_invariant loop_variant { { loop_invariant = $1; loop_variant = $2 } }
+| loop_invariant opt_variant { { loop_invariant = $1; loop_variant = $2 } }
 ;
 
 loop_invariant:
@@ -388,11 +390,6 @@ loop_invariant:
 | /* epsilon */   { None    }
 ;
 
-loop_variant:
-| VARIANT LOGIC { Some $2 }
-| /* epsilon */ { None    }
-;
-
 constant:
 | INTEGER
    { Term.ConstInt $1 }
@@ -504,8 +501,9 @@ opt_raises:
 ;
 
 opt_variant:
-| /* epsilon */ { None }
-| VARIANT LOGIC  { Some $2 }
+| /* epsilon */             { None }
+| VARIANT LOGIC             { Some ($2, id_wf_lt_int ()) }
+| VARIANT LOGIC FOR lqualid { Some ($2, $4) }
 ;
 
 list0_lident_sep_comma:

src/programs/pgm_ptree.ml

@@ -35,9 +35,11 @@ type logic = Lexing.position * string
 
 type lexpr = logic
 
+type variant = lexpr * qualid
+
 type loop_annotation = {
   loop_invariant : lexpr option;
-  loop_variant   : lexpr option;
+  loop_variant   : variant option;
 }
 
 type effect = {
@@ -63,8 +65,6 @@ and type_c =
 
 and binder = ident * type_v option
 
-type variant = lexpr 
-
 type expr = {
   expr_desc : expr_desc;
   expr_loc  : loc;

src/programs/pgm_ttree.ml

@@ -58,13 +58,13 @@ and dtype_c =
 
 and dbinder = string * dtype_v
 
+type dvariant = Ptree.lexpr * Term.lsymbol
+
 type dloop_annotation = {
   dloop_invariant : Ptree.lexpr option;
-  dloop_variant   : Ptree.lexpr option;
+  dloop_variant   : dvariant option;
 }
 
-type dvariant = Ptree.lexpr 
-
 type dexpr = {
   dexpr_desc : dexpr_desc;
   dexpr_denv : Typing.denv;
@@ -102,7 +102,7 @@ and dtriple = dpre * dexpr * dpost
 
 (* phase 2: typing annotations *)
 
-type variant = Term.term
+type variant = Term.term * Term.lsymbol
 
 type reference = 
   | Rlocal  of Term.vsymbol

src/programs/pgm_typing.ml

@@ -199,9 +199,22 @@ and dbinder env ({id=x; id_loc=loc}, v) =
   let env = { env with denv = Typing.add_var x ty env.denv } in
   env, (x, v)
 
-let dloop_annotation a =
+let dvariant uc (l, p) =
+  let l = lexpr l in
+  let s, _ = Typing.specialize_psymbol p uc in
+  let loc = Typing.qloc p in
+  begin match s.ls_args with
+    | [t1; t2] when Ty.ty_equal t1 t2 -> 
+	()
+    | _ -> 
+	errorm ~loc "predicate %s should be a binary relation" 
+	  s.ls_name.id_string
+  end;
+  l, s
+
+let dloop_annotation uc a =
   { dloop_invariant = option_map lexpr a.Pgm_ptree.loop_invariant;
-    dloop_variant   = option_map lexpr a.Pgm_ptree.loop_variant; }
+    dloop_variant   = option_map (dvariant uc) a.Pgm_ptree.loop_variant; }
 
 let rec dexpr env e = 
   let d, ty = dexpr_desc env e.Pgm_ptree.expr_loc e.Pgm_ptree.expr_desc in
@@ -263,7 +276,7 @@ and dexpr_desc env loc = function
       expected_type e1 (dty_bool env.uc);
       let e2 = dexpr env e2 in
       expected_type e2 (dty_unit env.uc);
-      DEwhile (e1, dloop_annotation a, e2), (dty_unit env.uc)
+      DEwhile (e1, dloop_annotation env.uc a, e2), (dty_unit env.uc)
   | Pgm_ptree.Elazy (op, e1, e2) ->
       let e1 = dexpr env e1 in
       expected_type e1 (dty_bool env.uc);
@@ -352,7 +365,7 @@ and dletrec env dl =
   let add_one env (id, bl, var, t) = 
     let ty = create_type_var id.id_loc in
     let env = { env with denv = Typing.add_var id.id ty env.denv } in
-    env, ((id, ty), bl, option_map lexpr var, t)
+    env, ((id, ty), bl, option_map (dvariant env.uc) var, t)
   in
   let env, dl = map_fold_left add_one env dl in
   (* then type-check all of them and unify *)
@@ -417,6 +430,18 @@ let post env ty (q, ql) =
   let env = Mstr.add id_result v_result env in
   Typing.type_fmla denv env l, List.map exn ql
 
+let variant denv env (t, ps) =
+  let loc = t.pp_loc in
+  let t = Typing.type_term denv env t in
+  match ps.ls_args with
+    | [t1; _] when Ty.ty_equal t1 t.t_ty -> 
+	t, ps
+    | [t1; _] -> 
+	errorm ~loc "variant has type %a, but is expected to have type %a"
+	  Pretty.print_ty t.t_ty Pretty.print_ty t1
+    | _ -> 
+	assert false
+
 let rec type_v uc env = function
   | DTpure ty -> 
       Tpure (Denv.ty_of_dty ty)
@@ -477,7 +502,7 @@ and expr_desc uc env denv = function
 	{ loop_invariant = 
 	    option_map (Typing.type_fmla denv env) la.dloop_invariant;
 	  loop_variant   = 
-	    option_map (Typing.type_term denv env) la.dloop_variant; }
+	    option_map (variant denv env) la.dloop_variant; }
       in
       Ewhile (expr uc env e1, la, expr uc env e2)
   | DElazy (op, e1, e2) ->
@@ -537,7 +562,7 @@ and letrec uc env dl =
   let step2 (v, bl, var, (_,e,_ as t)) =
     let env, bl = map_fold_left (binder uc) env bl in
     let denv = e.dexpr_denv in
-    let var = option_map (Typing.type_term denv env) var in
+    let var = option_map (variant denv env) var in
     let t = triple uc env t in
     (v, bl, var, t)
   in

tests/test-pgm-jcf.mlw

@@ -4,6 +4,8 @@ use import list.List
 logic c : int
 }
 
+let p42 () = { wf_lt_int(4,3) } 1 { true }
+
 exception Not_found
 exception Found of int
 
@@ -17,12 +19,17 @@ let test (n:int) =
   in
   is_even n
 
-let rec is_even (x:int) variant {x} = 
+{ 
+logic rel(int, int)
+logic rel2(int, int)
+}
+
+let rec is_even (x:int) variant {x} for rel = 
     {x>=1} 
     if x = 0 then True else not (is_odd (x-1))
     {true}
 
-and is_odd (x:int) variant {x} =
+and is_odd (x:int) variant {x} for rel2 =
   if x = 0 then False else not (is_even (x-1))
 
 let b = is_even 2
@@ -58,6 +65,28 @@ let p12 () =
   let x = any int in
   x + any int
   
+{ 
+type 'a tree =
+  | Empty
+  | Node ('a, 'a forest)
+
+type 'a forest =
+  | Fnil
+  | Fcons ('a tree, 'a forest)
+
+logic tree_height('a tree) : int
+logic forest_height('a forest) : int
+}
+
+let rec size_tree (t: 'a tree) variant {tree_height(t)} = match t with
+  | Empty -> 0
+  | Node (_, f) -> 1 + size_forest f
+  end
+and size_forest (f: 'a forest) = match f with
+  | Fnil -> 0
+  | Fcons (t, f) -> size_tree t + size_forest f
+  end
+
 
 (*
 Local Variables: 

theories/programs.why

@@ -25,4 +25,7 @@ theory Prelude
   logic old ('a)        : 'a
 
   type exn
+
+  logic wf_lt_int(x:int, y:int) = 0 <= y and x < y
+
 end