loop_down

TODO

 
+MAJOR TODAY
+
+
+let f () =
+  let r : '_a ref = ref [] in
+  !r
+
+let f () =
+  let r : int ref = ref [] in
+  !r
+
+let f () : 'a list =
+  let r : 'a ref = ref [] in
+  !r
+
 
-xwhile: error reporting when arguments don't have the right types.
 
+xwhile: error reporting when arguments don't have the right types.
 
 rename xextract to xpull;  and xgen to xpush.
 
@@ -15,32 +30,30 @@ infix_eq_
   forall x : int, comparable_value x
 
 
+- record with
 
+- when clauses
 
-MAJOR TODAY
-
-- loops
+- open no scope in CF.
 
-- for downto
+- add support for pure records
 
 - inline CFHeader.pred  as -1
 
-MAJOR NEXT
-
 - xchanges
 
-- record with
 
-- when clauses
 
-- partial/over application
 
-- xabstract => reimplement and rename as xgen
 
-- open no scope in CF.
+MAJOR NEXT
 
-- add support for pure records
 
+- partial/over application
+
+- xabstract => reimplement and rename as xgen
+
+- eliminate notations for tags
 
 MAJOR NEXT NEXT
 

examples/BasicDemos/Demo.ml

@@ -8,21 +8,52 @@ open Pervasives
  *)
 
 
-(*--TODO
+(********************************************************************)
+(* ** Value restriction *)
+
+(* -- accepted program: even though the internal type-checking 
+     involves a ['_a ref] type, the result type is ['a list]. *)
+
+let value_restriction_0 () =
+  let r = ref [] in
+  !r
+
+(* -- rejected program: use of ['_a ref] type annotation is not supported.
 
-let f () =
+let value_restriction_1 () =
   let r : '_a ref = ref [] in
   !r
+*)
+
+(* -- accepted program: monomorphic annotation on the let-bindings *)
 
-let f () =
-  let r : int ref = ref [] in
+let value_restriction_2 () =
+  let r : (int list) ref = ref [] in
   !r
 
-let f () : 'a list =
-  let r : 'a ref = ref [] in
+(* -- accepted program: monomorphic annotation on the empty list *)
+
+let value_restriction_3 () =
+  let r = ref ([] : int list) in
   !r
 
-*)
+(* -- accepted program: the polymorphic type annotation is accepted,
+   but it fact it is refined by the type-checker as [(int list) ref]. *)
+
+let value_restriction_4 () =
+  let r : ('a list) ref = ref [] in
+  r := [4];
+  !r
+
+(* -- accepted program: likewise, the list [[5]] is accepted at type
+    ['a list], but it comes out at type [int list] from the type-checker. *)
+
+let value_restriction_5 () : 'a list =
+  let r = ref [] in
+  r := [5];
+  !r
+
+
 
 (********************************************************************)
 (* ** Encoding of names *)
@@ -39,11 +70,11 @@ type 'a_ renaming_t4 = int
 let renaming_demo () =
    (* let x_ = 3 in   --rejected *)
    (* let x__ = 3 in  --rejected *)
-   let x = 3 in
-   let x' = 3 in
-   let x_' = 3 in
-   let exists = 3 in
-   let array = 3 in
+   let _x = 3 in
+   let _x' = 3 in
+   let _x_' = 3 in
+   let _exists = 3 in
+   let _array = 3 in
    ()
 
 
@@ -364,7 +395,7 @@ let assert_same (x:int) (y:int) =
   3
 
 let assert_let () =
-  assert (let x = true in true); 
+  assert (let _x = true in true); 
   3
 
 let assert_seq () =
@@ -482,9 +513,9 @@ let order_array () =
 
 let ref_gc () =
   let r1 = ref 1 in
-  let r2 = ref 1 in
-  let r3 = ref 1 in
-  let r4 = ref 1 in
+  let _r2 = ref 1 in
+  let _r3 = ref 1 in
+  let _r4 = ref 1 in
   let x = 
      let r5 = ref 2 in
      !r5 
@@ -531,7 +562,6 @@ let for_to_incr r =
    done;
    !n
 
-(*
 let for_downto r =
    let n = ref 0 in
    for i = pred r downto 0 do
@@ -539,7 +569,6 @@ let for_downto r =
    done;
    !n
 
-*)
 
 (********************************************************************)
 (* ** Recursive function *)

examples/BasicDemos/Demo_proof.v

@@ -8,43 +8,7 @@ Require Import Stdlib.
 
 
 
-(********************************************************************)
-(* ** For loops *)
 
-Lemma for_to_incr_spec : forall (r:int), r >= 0 ->
-  app for_to_incr [r] \[] \[= r].
-Proof using.
-  xcf. xapps. unfolds CFHeader.pred. dup 7. 
-  { xfor. intros S LS HS.
-    cuts PS: (forall i, (i <= r) -> S i (n ~~> i) (# n ~~> r)).
-    { applys PS. math. }
-    { intros i. induction_wf IH: (upto r) i. intros Li.
-      applys (rm HS). xif.
-      { xapps. applys IH. hnf. skip. skip. (* math. *) }
-      { xrets. skip. (* math. *) } } 
-    xapps. xsimpl~. } 
-  { xfor as S. skip. skip. }
-  { xfor_inv (fun (i:int) => n ~~> i). skip. skip. skip. skip. } 
-  { xseq (# n ~~> r). xfor_inv (fun (i:int) => n ~~> i). skip. skip. skip. skip. skip. }
-  { xseq (# n ~~> r). xfor_inv_void. skip. skip. skip. }
-  { xfor_inv_void. skip. skip. }
-  { xseq (# n ~~> r). 
-    xfor_inv_case (fun (i:int) => n ~~> i); intros C.
-    { exists \[]. splits. skip. skip. skip. } 
-    { false. skip. (* math. *) }
-    { xapps. xsimpl~. } }
-Qed.
-
-(* TODO
-
-let for_downto r =
-   let n = ref 0 in
-   for i = pred r downto 0 do
-      incr n;
-   done;
-   !n
-
-*)
 
 
 
@@ -707,6 +671,77 @@ Qed.
 
 
 
+(********************************************************************)
+(* ** For loops *)
+
+Lemma for_to_incr_spec : forall (r:int), r >= 0 ->
+  app for_to_incr [r] \[] \[= r].
+Proof using.
+  xcf. xapps. dup 7. 
+  { xfor. intros S LS HS.
+    cuts PS: (forall i, (i <= r) -> S i (n ~~> i) (# n ~~> r)).
+    { applys PS. math. }
+    { intros i. induction_wf IH: (upto r) i. intros Li.
+      applys (rm HS). xif.
+      { xapps. applys IH. hnf. math. math. }
+      { xrets. math. } } 
+    xapps. xsimpl~. } 
+  { xfor as S. skip. skip. }
+  { xfor_inv (fun (i:int) => n ~~> i).
+    { math. }
+    { xsimpl. }
+    { introv L. xapps. }
+    xapps. xsimpl. math. } 
+  { xseq (# n ~~> r). xfor_inv (fun (i:int) => n ~~> i).
+    skip. skip. skip. skip. skip. }
+  { xseq (# n ~~> r). xfor_inv_void. skip. skip. skip. }
+  { xfor_inv_void. skip. skip. }
+  { try xfor_inv_case (fun (i:int) => n ~~> i). 
+    (* fails because no post condition *)
+    xseq (# n ~~> r).
+    { xfor_inv_case (fun (i:int) => n ~~> i).
+      { xsimpl. }
+      { introv L. xapps. }
+      { xsimpl. math. } 
+      { math_rewrite (r = 0). xsimpl. } }
+    { xapps. xsimpl~. } }
+Abort.
+
+Lemma for_downto_spec : forall (r:int), r >= 0 ->
+  app for_downto [r] \[] \[= r].
+Proof using.
+  xcf. xapps. dup 7. 
+  { xfor_down. intros S LS HS.
+    cuts PS: (forall i, (i >= -1) -> S i (n ~~> (r-1-i)) (# n ~~> r)).
+    { xapplys PS. math. math. }
+    { intros i. induction_wf IH: (downto (-1)) i. intros Li.
+      applys (rm HS). xif.
+      { xapps. xapplys IH. hnf. math. math. math. }
+      { xrets. math. } } 
+    xapps. xsimpl~. } 
+  { xfor_down as S. skip. skip. }
+  { xfor_down_inv (fun (i:int) => n ~~> (r-1-i)). 
+    { math. }
+    { xsimpl. math. }
+    { introv L. xapps. xsimpl. math. }
+    xapps. xsimpl. math. }
+  { xseq (# n ~~> r). xfor_down_inv (fun (i:int) => n ~~> (r-1-i)).
+    skip. skip. skip. skip. skip. }
+  { xseq (# n ~~> r). xfor_down_inv_void. skip. skip. skip. }
+  { xfor_down_inv_void. skip. skip. }
+  { try xfor_down_inv_case (fun (i:int) => n ~~> (r-1-i)).
+    (* fails because no post condition *)
+    xseq (# n ~~> r).
+    { xfor_down_inv_case (fun (i:int) => n ~~> (r-1-i)).
+      { xsimpl. math. }
+      { introv L. xapps. xsimpl. math. }
+      { xsimpl. math. } 
+      { math_rewrite (r = 0). xsimpl. } }
+    { xapps. xsimpl~. } }
+Abort.
+
+
+
 (********************************************************************)
 (* ** Lazy binary operators *)
 

generator/characteristic.ml

@@ -114,12 +114,12 @@ let rec lift_btyp t =
    let aux = lift_btyp in
    match t with
    | Btyp_val -> 
-      val_type
+      func_type
    | Btyp_arrow (t1,t2) -> 
-      val_type
+      func_type
+   (* DEPRECATED
    | Btyp_constr (id,[t]) when Path.name id = "array" -> 
-      (* || Path.name id = "Pervasives.array" *)
-      loc_type
+      loc_type *)
    | Btyp_constr (id,ts) -> 
       coq_apps (Coq_var (type_constr_name (lift_path_name id))) (List.map aux ts)
    | Btyp_tuple ts -> 
@@ -310,10 +310,13 @@ let pattern_aliases p : (typed_var*coq) list =
 (* ** Helper functions for various things *)
 
 let register_cf x =
-   Coqtop_register ("database_cf", x, cf_axiom_name x)
+   Coqtop_custom (sprintf "Hint Extern 1 (RegisterCF %s) => CFHeader_Provide %s." x (cf_axiom_name x))
+   (* DEPRECATED 
+      Coqtop_register ("CFML.CFPrint.database_cf", x, cf_axiom_name x)
+    *)
 
 let register_spec x v =
-   Coqtop_register ("database_spec", x, v)
+   Coqtop_register ("CFML.CFPrint.database_spec", x, v)
 
 
 (* TODO: rewrite this function by using a normalization function that returns p *)
@@ -752,11 +755,13 @@ let rec cfg_exp env e =
    | Texp_while(cond, body) -> 
       Cf_while (aux cond, aux body)
 
-   | Texp_for(param, low, high, dir, body) -> 
-      begin match dir with 
-        | Upto -> Cf_for (Ident.name param, lift low, lift high, aux body)
-        | Downto -> unsupported loc "for-downto expressions" (* later *)
-      end
+   | Texp_for(param, low, high, caml_dir, body) -> 
+      let dir = 
+        match caml_dir with
+        | Upto -> For_loop_up
+        | Downto -> For_loop_down
+        in
+      Cf_for (dir, Ident.name param, lift low, lift high, aux body)
 
    | Texp_array args -> 
       let arg = coq_list (List.map lift args) in
@@ -876,7 +881,7 @@ let rec cfg_structure_item s : cftops =
            | Default -> unsupported loc "Default recursion mode"
            in
         let ncs = List.map (fun (pat,bod) -> (pattern_name_protect_infix pat, cfg_func env' fvs pat bod)) pat_expr_list in
-          (List.map (fun (name,_) -> Cftop_val (name, val_type)) ncs)
+          (List.map (fun (name,_) -> Cftop_val (name, func_type)) ncs)
         @ (List.map (fun (name,cf_body) -> Cftop_fun_cf (name, cf_body)) ncs)
         @ [Cftop_coqs (List.map (fun (name,_) -> register_cf name) ncs)]
    
@@ -1054,10 +1059,10 @@ and record_functions name record_constr repr_name params fields_names fields_typ
    let new_name = record_make_name name in
    let get_names = for_indices (fun i -> record_field_get_name (nth i fields_names)) in
    let set_names = for_indices (fun i -> record_field_set_name (nth i fields_names)) in
-   let new_decl = Coqtop_param (new_name, val_type) in
+   let new_decl = Coqtop_param (new_name, func_type) in
    let get_set_decl i =
-      [ Coqtop_param (nth i get_names, val_type); 
-        Coqtop_param (nth i set_names, val_type) ] in
+      [ Coqtop_param (nth i get_names, func_type); 
+        Coqtop_param (nth i set_names, func_type) ] in
    
    let logicals = List.map str_capitalize_1 fields_names in
    let reprs = for_indices (fun i -> sprintf "_T%d" (i+1)) in
@@ -1499,12 +1504,12 @@ and cfg_module id m =
 let cfg_file str =
    [ Cftop_coqs ([ 
       Coqtop_set_implicit_args; 
-      Coqtop_require [ "Coq.ZArith.BinInt"; "TLC.LibLogic"; "TLC.LibRelation"; "TLC.LibInt"; "TLC.LibListZ"; "CFML.Shared"; "CFML.CFHeaps"; "CFML.CFApp" ];  
-      Coqtop_require_import ["CFHeader"];
-      Coqtop_require ["CFPrint"];
-      Coqtop_custom "Open Scope list_scope.";
-      Coqtop_custom "Local Notation \"'int'\" := (Coq.ZArith.BinInt.Z).";
-      Coqtop_custom "Delimit Scope Z_scope with Z." 
+      Coqtop_require [ "Coq.ZArith.BinInt"; "TLC.LibLogic"; "TLC.LibRelation"; "TLC.LibInt"; "TLC.LibListZ"; "CFML.Shared"; "CFML.CFHeaps"; "CFML.CFApp"; "CFML.CFPrint"; "CFML.CFBuiltin" ];
+      Coqtop_require_import [ "CFML.CFHeader" ];
+      Coqtop_custom "Delimit Scope Z_scope with Z.";
+      Coqtop_custom "Local Open Scope cfheader_scope.";
+      (*DEPRECATED Coqtop_custom "Open Scope list_scope.";*)
+      (*DEPRECATED Coqtop_custom "Local Notation \"'int'\" := (Coq.ZArith.BinInt.Z).";*)
       ]
       @ (external_modules_get_coqtop())) ]
    @ cfg_structure str

generator/coq.ml

@@ -283,12 +283,20 @@ let coq_exists xcs c2 =
 let coq_le c1 c2 =
   coq_apps (Coq_var "TLC.LibOrder.le") [ c1; c2 ]
 
+let coq_ge c1 c2 =
+  coq_apps (Coq_var "TLC.LibOrder.ge") [ c1; c2 ]
+
+let coq_lt c1 c2 =
+  coq_apps (Coq_var "TLC.LibOrder.lt") [ c1; c2 ]
+
 let coq_gt c1 c2 =
   coq_apps (Coq_var "TLC.LibOrder.gt") [ c1; c2 ]
 
 let coq_plus c1 c2 =
   coq_apps (Coq_var "Coq.ZArith.BinInt.Zplus") [ c1; c2 ]
 
+let coq_minus c1 c2 =
+  coq_apps (Coq_var "Coq.ZArith.BinInt.Zminus") [ c1; c2 ]
 
 (** Toplevel *)
 

generator/formula.ml

@@ -5,6 +5,8 @@ open Mytools
 (*#########################################################################*)
 (* ** Syntax of characteristic formulae *)
 
+type for_loop_dir = For_loop_up | For_loop_down
+
 type cf =
     Cf_ret of coq
   | Cf_fail
@@ -22,7 +24,7 @@ type cf =
       (typed_var * coq) list * cf * cf
   | Cf_match of var * int * cf
   | Cf_seq of cf * cf
-  | Cf_for of var * coq * coq * cf
+  | Cf_for of for_loop_dir * var * coq * coq * cf
   | Cf_while of cf * cf
   | Cf_manual of coq
   | Cf_pay of cf
@@ -50,7 +52,7 @@ let coq_dyn_at = coq_var_at "CFML.CFHeaps.dyn"
 
 (** Abstract datatype for functions *)
 
-let val_type = Coq_var "CFML.CFApp.func"   
+let func_type = Coq_var "CFML.CFApp.func"   
 
 (** Abstract data type for locations *)
 

generator/formula.mli

@@ -7,6 +7,9 @@ open Coq
     (as described in [coq.ml]), using an algorithm contained in this file. *)
 
 
+(** For loop direction *)
+
+type for_loop_dir = For_loop_up | For_loop_down
 
 (** Characteristic formulae for terms *)
 
@@ -41,7 +44,7 @@ type cf =
     (* Match ?lab n Q *)
   | Cf_seq of cf * cf
     (* Q1 ;; Q2 *)
-  | Cf_for of var * coq * coq * cf 
+  | Cf_for of for_loop_dir * var * coq * coq * cf 
     (* for i = v1 to v2 do Q done *)
   | Cf_while of cf * cf
     (* while Q1 do Q2 done *)
@@ -86,7 +89,7 @@ val coq_dyn_at : Coq.coq
 
 (** Abstract datatype for functions (func) *)
 
-val val_type : Coq.coq
+val func_type : Coq.coq
 
 (** Abstract data type for locations (loc) *)
 

generator/formula_to_coq.ml

@@ -76,7 +76,7 @@ let rec coqtops_of_imp_cf cf =
 
   | Cf_body (f, fvs, targs, typ, cf1) ->
       let narity = Coq_nat (List.length targs) in
-      let h_curried = coq_apps (Coq_var "curried") [narity; coq_var f] in 
+      let h_curried = coq_apps (Coq_var "CFML.CFApp.curried") [narity; coq_var f] in 
       let h_body_hyp = coq_apps (coq_of_cf cf1) [h; q] in
       let args = List.map (fun (x,t) -> coq_apps coq_dyn_at [t; coq_var x]) targs in
       let h_body_conc = coq_apps (Coq_var "CFML.CFApp.app_def") [coq_var f; coq_list args; h; q]  in
@@ -104,7 +104,7 @@ let rec coqtops_of_imp_cf cf =
  
   | Cf_fun (ncs, cf) ->
       let ns, cs = List.split ncs in
-      let fs = List.map (fun n -> (n, val_type)) ns in
+      let fs = List.map (fun n -> (n, func_type)) ns in
       let chyps = List.map coq_of_cf cs in
       let cconc = coq_apps (coq_of_cf cf) [h;q] in
       let x = List.hd ns in
@@ -115,8 +115,8 @@ let rec coqtops_of_imp_cf cf =
   | Cf_fun (ncs, cf) ->
       let ns, cs = List.split ncs in
       let p_of n = "P" ^ n in
-      let fs = List.map (fun n -> (n, val_type)) ns in
-      let ps = List.map (fun n -> (p_of n, coq_pred val_type)) ns in
+      let fs = List.map (fun n -> (n, func_type)) ns in
+      let ps = List.map (fun n -> (p_of n, coq_pred func_type)) ns in
       let c1hyps = List.map coq_of_cf cs in
       let c1conc = coq_conjs (List.map (fun n -> Coq_app (Coq_var (p_of n), Coq_var n)) ns) in
       let c1 = coq_impls c1hyps c1conc in
@@ -177,29 +177,45 @@ let rec coqtops_of_imp_cf cf =
       funhq "tag_seq" (coq_exist "Q'" wild_to_hprop (coq_conj c1 c2))
       (* (!S: fun H Q => exists Q', F1 H Q /\ F2 (Q' tt) Q *)
 
-  | Cf_for (i_name,v1,v2,cf) ->
+  | Cf_for (dir,i_name,v1,v2,cf) ->
       let s = Coq_var "S" in
       let i = Coq_var i_name in
+      let tag, cond_test, istep = 
+         match dir with
+         | For_loop_up -> "tag_for", (coq_le i v2), (coq_plus i (Coq_int 1))
+         | For_loop_down -> "tag_for_down", (coq_ge i v2), (coq_minus i (Coq_int 1))
+         in
       let typs = Coq_impl (coq_int,formula_type) in
       let locals = Coq_app (Coq_var "CFML.CFHeaps.is_local_pred", s) in
-      let snext = coq_apps s [ coq_plus i (Coq_int 1) ] in
+      let snext = coq_apps s [ istep ] in
       let cf_step = Cf_seq (cf, Cf_manual snext) in 
       let cf_ret = Cf_ret coq_tt in
-      let cond = coq_apps (Coq_var "TLC.LibReflect.isTrue") [ coq_le i v2 ] in
+      let cond = coq_apps (Coq_var "TLC.LibReflect.isTrue") [ cond_test ] in
       let cf_if = Cf_caseif (cond, cf_step, cf_ret) in
       let bodys = coq_of_cf cf_if in
       let hypr = coq_foralls [(i_name, coq_int); ("H", hprop); ("Q", Coq_impl (coq_unit, hprop))] (Coq_impl (coq_apps bodys [h;q], (coq_apps s [i;h;q]))) in
-      funhq "tag_for" (Coq_forall (("S",typs), coq_impls [locals; hypr] (coq_apps s [v1;h;q])))
+      funhq tag (Coq_forall (("S",typs), coq_impls [locals; hypr] (coq_apps s [v1;h;q])))
+
+      (* UP:
+         (!For (fun H Q => forall S:int->~~unit, is_local_pred S ->
+           (forall i H Q,  
+               (If_ i <= v2       
+                  Then Seq (F1 ;; S (i+1)) H Q))
+                  Else Ret tt) H Q
+              -> S i H Q) 
+            -> S v1 H Q) 
+         
+        DOWN:
+           (!For (fun H Q => forall S:int->~~unit, is_local_pred S ->
+             (forall i H Q,  
+               (If_ i >= v2       
+                  Then Seq (F1 ;; S (i-1)) H Q))
+                  Else Ret tt) H Q
+              -> S i H Q) 
+            -> S v1 H Q)      
+         
+         *)
 
-      (* (!For (fun H Q => forall S:int->~~unit, is_local_pred S ->
-        (forall i H Q,  
-            (If_ i <= v2       
-               Then Seq (F1 ;; S (i+1)) H Q))
-               Else Ret tt) H Q
-           -> S i H Q) 
-         -> S v1 H Q)  *)
-         (*--todo:optimize using rec calls *)
-     
       (* DEPRECATED
       let s = Coq_var "S" in
       let i = Coq_var i_name in
@@ -240,7 +256,7 @@ let rec coqtops_of_imp_cf cf =
       funhq "tag_pay" (coq_exist "H'" hprop (coq_conj c1 c2))
       (* (!Pay: fun H Q => exists H', pay_one H H' /\ F1 H' Q *)
 
-(* old:
+(* DEPRECATED:
       let r = Coq_var "R" in
       let typr = formula_type in
       let q' = Coq_var "Q'" in

generator/print_coq.ml

@@ -402,7 +402,7 @@ let top = function
       brackets (flow_map space implicit xs)
       ^^ dot
   | Coqtop_register (db, x, v) ->
-      sprintf "Hint Extern 1 (Register %s %s) => CFPrint_Provide %s." db x v
+      sprintf "Hint Extern 1 (Register %s %s) => CFHeader_Provide %s." db x v
   | Coqtop_hint_constructors (xs, base) ->
       string "Hint Constructors " ^^
       flow_map space string xs ^^

generator/renaming.ml

@@ -236,9 +236,24 @@ let type_variable_name name =
 
 (** Convention for naming type constructors *)
 
+
+
+let type_constr_builtin_name name =
+   if name = "float" then unsupported_noloc "float not yet supported";
+   try List.assoc name
+      [ ("int", "Coq.ZArith.BinInt.Z");
+        ("unit", "Coq.Init.Datatypes.unit"); 
+        ("bool", "Coq.Init.Datatypes.bool");
+        ("option", "Coq.Init.Datatypes.option");
+        ("list", "Coq.Init.Datatypes.list");
+        ("string", "Coq.Strings.String.string");
+        ("array", "CFML.CFBuiltin.array");
+      ]
+   with Not_found -> failwith ("type_constr_builtin_name: missing name for " ^ name)
+
 let type_constr_name name =
   if List.mem name builtin_type_constructors
-    then name 
+    then type_constr_builtin_name name 
     else name ^ "_"
 
 (** Note: see function [lift_btyp] in characteristic.ml 
@@ -301,7 +316,7 @@ type primitive_arity =
 
 let inlined_primitives_table =