(wip) example: formalization of Why3 term API

examples/in_progress/why3_logic/term.mlw

@@ -264,7 +264,7 @@ module Term
   function ct_d (t_ctx 'vs) : term -> bool
   function ct_m (t_ctx 'vs) : term -> D.term 'vs
   axiom t_ctx_inv : forall c,x:'vs. c.ct_vs.c_ldom x ->
-    ty_vars_in c.ct_ty.cty_tv.c_ldom c.ct_ty.cty_sym.d_tys (c.ct_vty x)
+    ty_vars_in c.ct_ty.cty_tv.c_ldom c.ct_ty.cty_sym.d_tys (c.ct_vty x)  
   
   function ct_tv (ct:t_ctx 'vs) : context ident_name int = ct.ct_ty.cty_tv
   function ct_sym (ct:t_ctx 'vs) : sym_ctx = ct.ct_ty.cty_sym
@@ -287,6 +287,11 @@ module Term
   function ctp_mty (ctp:pat_ctx) : pattern -> D.ty =
     \p. ctp.ct_ty.cty_m p.pat_ty
   
+  (* Type of variable symbols in contexts. *)
+  val ghost ct_vs_tys (ct:t_ctx 'vs) (vs:vsymbol) : unit
+    requires { ct.ct_vs.c_pdom vs.vs_idn }
+    ensures { ct.ct_ty.cty_d vs.vs_ty }
+    ensures { ct.ct_vty (ct.ct_vs.c_ptl vs.vs_idn) = ct.ct_ty.cty_m vs.vs_ty }
   (* Contexts bounds. *)
   val ghost ct_ubounds (ct:t_ctx 'vs) : unit
     ensures { subset ct.ct_vs.c_pdom ids.ids }
@@ -551,6 +556,10 @@ module Term
   
   type trigger = list (list term)
   
+  predicate br_ty_are (ct:t_ctx 'vs) (bty:D.ty) (oty:D.ty) (tbr:term_branch) =
+    ct.ct_ty.cty_m tbr.tbr_bty = bty /\
+    ct.ct_ty.cty_m tbr.tbr_ty = oty
+  
   (* Binding predicates. *)
   predicate bound_env (x:vsymbol) (c:t_ctx unit) =
     c.ct_vs.c_ldom = all /\
@@ -611,6 +620,7 @@ module Term
     ensures { co.ctb_d result }
     ensures { co.ctb_m result = ct.ct_m t }
     ensures { co.ct_ty.cty_m result.tb_ty = ct.ct_mty t }
+    ensures { ct.ct_ty.cty_d vs.vs_ty }
     ensures { co.ct_ty.cty_m result.tb_bty = ct.ct_ty.cty_m vs.vs_ty
                                        = ct.ct_vty (ct.ct_vs.c_ptl vs.vs_idn) }
   
@@ -650,6 +660,7 @@ module Term
       let vs = r.tbo_vs in let cb = r.tbo_cb in
       cn.ct_d t /\ fused ct cb cn /\ bound_env vs cb /\
       cn.ct_m t = ct.ctb_m tb /\ cn.ct_mty t = ct.ct_ty.cty_m tb.tb_ty /\
+      cn.ct_ty.cty_d vs.vs_ty /\
       cn.ct_ty.cty_m vs.vs_ty = cn.ct_vty (cn.ct_vs.c_ptl vs.vs_idn)
                               = ct.ct_ty.cty_m tb.tb_bty }
   
@@ -688,23 +699,179 @@ module Term
       ct.ctq_m tq = D.TImplies (trigger cn tr) (cn.ct_m t) /\
       tq.tq_qty = map vs_ty vsl /\
       vsl <> Nil /\ cn.ct_ty.cty_m t.t_ty = ty_prop }
-  (*
+  
   val t_node (ghost ct:t_ctx 'vs) (t:term) : term_node
     requires { ct.ct_d t }
     returns { Tvar vs -> ct.ct_m t = D.TVar (ct.ct_vs.c_ptl vs.vs_idn) /\
         ct.ct_vs.c_pdom vs.vs_idn /\
+        ct.ct_ty.cty_d vs.vs_ty /\
         ct.ct_mty t = ct.ct_ty.cty_m vs.vs_ty
-                  = ct.ct_vty (ct.ct_vs.ct_ptl vs.vs_idn)
+                  = ct.ct_vty (ct.ct_vs.c_ptl vs.vs_idn)
       | Tconst cst -> ct.ct_m t = D.TApp cst.cst_m Nil Nil /\
         ct.ct_mty t = ty_ret global_sig.sig_m cst.cst_m Nil
-      | Tapp f tyl tl -> for_all ct.ct_d tl /\
+      | Tapp f tyl tl -> for_all ct.ct_d tl /\ ct.ct_sym.d_ls f.ls_m /\
         ct.ct_m t = D.TApp f.ls_m tyl (map ct.ct_m tl) /\
-        ct.ct_mty t = ty_subst_ret f.ls_args tyl /\
-        map ct.ct_mty tl = ty_subst_args f.ls_ret tyl
+        ct.ct_mty t = ty_subst_ret tyl f.ls_ret /\
+        map ct.ct_mty tl = ty_subst_args tyl f.ls_args
       | Tif b th el -> ct.ct_d b /\ ct.ct_d th /\ ct.ct_d el /\
         ct.ct_m t = D.TIf (ct.ct_m b) (ct.ct_m th) (ct.ct_m el) /\
-        ct.ct_mty b = ty_prop /\ ct.ct_mty th = ct.ct_mty
-    }*)
+        ct.ct_mty b = ty_prop /\ ct.ct_mty th = ct.ct_mty el = ct.ct_mty t
+      | Tlet u v -> ct.ct_d u /\ ct.ctb_d v /\
+        ct.ct_m t = D.TLet (ct.ct_m u) (ct.ctb_m v) /\
+        ct.ct_ty.cty_m v.tb_bty = ct.ct_mty u /\
+        ct.ct_ty.cty_m v.tb_ty = ct.ct_mty t
+      | Tcase u brl -> ct.ct_d u /\ for_all ct.ctbr_d brl /\
+        for_all (br_ty_are ct (ct.ct_mty u) (ct.ct_mty t)) brl /\
+        ct.ct_m t = D.TCase (ct.ct_m u) (map ct.ctbr_m brl)
+      | Teps u -> ct.ctb_d u /\ ct.ct_m t = D.TEps (ct.ct_mty t) (ct.ctb_m u) /\
+        ct.ct_ty.cty_m u.tb_bty = ct.ct_mty t /\
+        ct.ct_ty.cty_m u.tb_ty = ty_prop
+      | Tquant q tq -> ct.ctq_d tq /\ ct.ct_mty t = ty_prop /\
+        tq.tq_qty <> Nil /\ let tyl = map ct.ct_ty.cty_m tq.tq_qty in
+        match q with
+        | Tforall -> ct.ct_m t = D.TForall tyl (ct.ctq_m tq)
+        | Texists -> ct.ct_m t = D.TExists tyl (ct.ctq_m tq)
+        end
+      | Tbinop bp a b -> ct.ct_d a /\ ct.ct_d b /\
+        ct.ct_mty a = ct.ct_mty b = ct.ct_mty t = ty_prop /\
+        let tm = ct.ct_m t in let am = ct.ct_m a in let bm = ct.ct_m b in
+        match bp with
+        | Tand -> tm = D.TAnd am bm
+        | Tor -> tm = D.TOr am bm
+        | Timplies -> tm = D.TImplies am bm
+        | Tiff -> tm = D.TIff am bm
+        end
+      | Tnot u -> ct.ct_d u /\ ct.ct_mty t = ct.ct_mty u = ty_prop /\
+        ct.ct_m t = D.TNot (ct.ct_m u)
+      | Ttrue -> ct.ct_m t = D.TTrue /\ ct.ct_mty t = ty_prop
+      | Tfalse -> ct.ct_m t = D.TFalse /\ ct.ct_mty t = ty_prop
+    }
+  
+  val t_var (ghost ct:t_ctx 'vs) (vs:vsymbol) : term
+    requires { ct.ct_vs.c_pdom vs.vs_idn }
+    ensures { ct.ct_d result }
+    ensures { ct.ct_m result = D.TVar (ct.ct_vs.c_ptl vs.vs_idn) }
+    ensures { ct.ct_ty.cty_d vs.vs_ty }
+    ensures { ct.ct_mty result = ct.ct_ty.cty_m vs.vs_ty
+                               = ct.ct_vty (ct.ct_vs.c_ptl vs.vs_idn) }
+  
+  val t_const (ghost ct:t_ctx 'vs) (cst:const) : term
+    ensures { ct.ct_d result /\ ct.ct_m result = D.TApp cst.cst_m Nil Nil }
+    ensures { ct.ct_mty result = ty_ret global_sig.sig_m cst.cst_m Nil }
+  
+  val t_app (ghost ct:t_ctx 'vs) (ls:lsymbol) (ghost tyl:list D.ty)
+            (tl:list term) (tyo:option ty) : term
+    requires { for_all ct.ct_d tl /\ ct.ct_sym.d_ls ls.ls_m }
+    requires { map ct.ct_mty tl = ty_subst_args tyl ls.ls_args }
+    requires { match tyo with
+      | None -> ty_subst_ret tyl ls.ls_ret = ty_prop
+      | Some u -> ty_subst_ret tyl ls.ls_ret = ct.ct_ty.cty_m u
+      end }
+    ensures { ct.ct_d result }
+    ensures { ct.ct_m result = D.TApp ls.ls_m tyl (map ct.ct_m tl) }
+    ensures { ct.ct_mty result = ty_subst_ret tyl ls.ls_ret }
+  
+  val t_if (ghost ct:t_ctx 'vs) (b:term) (th:term) (el:term) : term
+    requires { ct.ct_d b /\ ct.ct_d th /\ ct.ct_d el }
+    requires { ct.ct_mty th = ct.ct_mty el /\ ct.ct_mty b = ty_prop }
+    ensures { ct.ct_d result }
+    ensures { ct.ct_m result = D.TIf (ct.ct_m b) (ct.ct_m th) (ct.ct_m el) }
+    ensures { ct.ct_mty result = ct.ct_mty th }
+  
+  val t_let (ghost ct:t_ctx 'vs) (u:term) (v:term_bound) : term
+    requires { ct.ct_d u /\ ct.ctb_d v }
+    requires { ct.ct_ty.cty_m v.tb_bty = ct.ct_mty u }
+    ensures { ct.ct_d result }
+    ensures { ct.ct_m result = D.TLet (ct.ct_m u) (ct.ctb_m v) }
+    ensures { ct.ct_mty result = ct.ct_ty.cty_m v.tb_ty }
+  
+  val t_case (ghost ct:t_ctx 'vs) (ghost oty:D.ty)
+             (u:term) (brl:list term_branch) : term
+    requires { ct.ct_d u /\ for_all ct.ctbr_d brl }
+    requires { for_all (br_ty_are ct (ct.ct_mty u) oty) brl }
+    ensures { ct.ct_d result }
+    ensures { ct.ct_m result = D.TCase (ct.ct_m u) (map ct.ctbr_m brl) }
+    ensures { ct.ct_mty result = oty }
+  
+  val t_eps (ghost ct:t_ctx 'vs) (u:term_bound) : term
+    requires { ct.ctb_d u /\ ct.ct_ty.cty_m u.tb_ty = ty_prop }
+    ensures { ct.ct_d result }
+    ensures { ct.ct_m result = D.TEps (ct.ct_mty result) (ct.ctb_m u) }
+    ensures { ct.ct_mty result = ct.ct_ty.cty_m u.tb_bty }
+  
+  val t_quant (ghost ct:t_ctx 'vs) (q:quant) (tq:term_quant) : term
+    requires { ct.ctq_d tq }
+    ensures { ct.ct_d result }
+    ensures { let tyl = map ct.ct_ty.cty_m tq.tq_qty in
+      match q with
+      | Tforall -> ct.ct_m result = D.TForall tyl (ct.ctq_m tq)
+      | Texists -> ct.ct_m result = D.TExists tyl (ct.ctq_m tq)
+      end }
+    ensures { ct.ct_mty result = ty_prop }
+  
+  val t_forall (ghost ct:t_ctx 'vs) (tq:term_quant) : term
+    requires { ct.ctq_d tq }
+    ensures { ct.ct_d result }
+    ensures { let tyl = map ct.ct_ty.cty_m tq.tq_qty in
+      ct.ct_m result = D.TForall tyl (ct.ctq_m tq) }
+    ensures { ct.ct_mty result = ty_prop }
+  
+  val t_exists (ghost ct:t_ctx 'vs) (tq:term_quant) : term
+    requires { ct.ctq_d tq }
+    ensures { ct.ct_d result }
+    ensures { let tyl = map ct.ct_ty.cty_m tq.tq_qty in
+      ct.ct_m result = D.TExists tyl (ct.ctq_m tq) }
+    ensures { ct.ct_mty result = ty_prop }
+  
+  val t_binary (ghost ct:t_ctx 'vs) (bp:binop) (a b:term) : term
+    requires { ct.ct_d a /\ ct.ct_d b }
+    requires { ct.ct_mty a = ty_prop = ct.ct_mty b }
+    ensures { ct.ct_d result /\ ct.ct_mty result = ty_prop }
+    ensures {
+      let am = ct.ct_m a in let bm = ct.ct_m b in let rm = ct.ct_m result in
+      match bp with
+      | Tand -> rm = D.TAnd am bm
+      | Tor -> rm = D.TOr am bm
+      | Timplies -> rm = D.TImplies am bm
+      | Tiff -> rm = D.TIff am bm
+      end }
+  
+  val t_and (ghost ct:t_ctx 'vs) (a b:term) : term
+    requires { ct.ct_d a /\ ct.ct_d b }
+    requires { ct.ct_mty a = ty_prop = ct.ct_mty b }
+    ensures { ct.ct_d result /\ ct.ct_mty result = ty_prop }
+    ensures { ct.ct_m result = D.TAnd (ct.ct_m a) (ct.ct_m b) }
+  
+  val t_or (ghost ct:t_ctx 'vs) (a b:term) : term
+    requires { ct.ct_d a /\ ct.ct_d b }
+    requires { ct.ct_mty a = ty_prop = ct.ct_mty b }
+    ensures { ct.ct_d result /\ ct.ct_mty result = ty_prop }
+    ensures { ct.ct_m result = D.TOr (ct.ct_m a) (ct.ct_m b) }
+  
+  val t_implies (ghost ct:t_ctx 'vs) (a b:term) : term
+    requires { ct.ct_d a /\ ct.ct_d b }
+    requires { ct.ct_mty a = ty_prop = ct.ct_mty b }
+    ensures { ct.ct_d result /\ ct.ct_mty result = ty_prop }
+    ensures { ct.ct_m result = D.TImplies (ct.ct_m a) (ct.ct_m b) }
+  
+  val t_iff (ghost ct:t_ctx 'vs) (a b:term) : term
+    requires { ct.ct_d a /\ ct.ct_d b }
+    requires { ct.ct_mty a = ty_prop = ct.ct_mty b }
+    ensures { ct.ct_d result /\ ct.ct_mty result = ty_prop }
+    ensures { ct.ct_m result = D.TIff (ct.ct_m a) (ct.ct_m b) }
+  
+  val t_not (ghost ct:t_ctx 'vs) (a:term) : term
+    requires { ct.ct_d a /\ ct.ct_mty a = ty_prop }
+    ensures { ct.ct_d result /\ ct.ct_mty result = ty_prop }
+    ensures { ct.ct_m result = D.TNot (ct.ct_m a) }
+  
+  val t_true (ghost ct:t_ctx 'vs) : term
+    ensures { ct.ct_d result /\ ct.ct_mty result = ty_prop }
+    ensures { ct.ct_m result = D.TTrue }
+  
+  val t_false (ghost ct:t_ctx 'vs) : term
+    ensures { ct.ct_d result /\ ct.ct_mty result = ty_prop }
+    ensures { ct.ct_m result = D.TFalse }
   
 end
 

examples/in_progress/why3_logic/term/why3session.xml

@@ -9,7 +9,7 @@
 </theory>
 <theory name="Ls" sum="d41d8cd98f00b204e9800998ecf8427e">
 </theory>
-<theory name="Term" sum="ddbc28b7f2fe9a580e03e892dc4bc3fb">
+<theory name="Term" sum="4a7d61a3f4a3792bfc97b177c2b61c32">
  <goal name="WP_parameter fused_alt" expl="VC for fused_alt">
  <transf name="split_goal_wp">
   <goal name="WP_parameter fused_alt.1" expl="1. assertion">

examples/in_progress/why3_logic/ty.mlw

@@ -295,7 +295,7 @@ module Ty
     ensures { equalizer s.Mtv.domain s.Mtv.bindings result.Mtv.bindings }
     (* Invariant. *)
     ensures { forall x. result.Mtv.domain x ->
-      ty1.cty_d (result.Mtv.bindings x) }
+      cty1.cty_d (result.Mtv.bindings x) }
     (* Failure. *)
     raises { TypeMismatch _ -> forall f.
       (forall x. s.Mtv.domain x ->

examples/in_progress/why3_logic/ty/why3session.xml

@@ -7,7 +7,7 @@
 <file name="../ty.mlw" expanded="true">
 <theory name="Tv" sum="d41d8cd98f00b204e9800998ecf8427e">
 </theory>
-<theory name="Ty" sum="564071bf524906e6be082b8cfe54c50b" expanded="true">
+<theory name="Ty" sum="17320dd31f9e83f405ff9085004af149">
  <goal name="WP_parameter ty_match_sure" expl="VC for ty_match_sure">
  <transf name="split_goal_wp">
   <goal name="WP_parameter ty_match_sure.1" expl="1. precondition">
@@ -29,10 +29,10 @@
   <proof prover="0"><result status="valid" time="0.05" steps="8"/></proof>
   </goal>
   <goal name="WP_parameter ty_match_sure.7" expl="7. postcondition">
-  <proof prover="0"><result status="valid" time="0.06" steps="11"/></proof>
+  <proof prover="0"><result status="valid" time="0.06" steps="10"/></proof>
   </goal>
   <goal name="WP_parameter ty_match_sure.8" expl="8. unreachable point">
-  <proof prover="0"><result status="valid" time="0.07" steps="19"/></proof>
+  <proof prover="0"><result status="valid" time="0.07" steps="18"/></proof>
   </goal>
  </transf>
  </goal>