fixes

TODO

-We need a good way of configuring or discovering where TLC is installed.
-    and a good way of fixing the ROOT of the CFML local tree
-    and a good way of fixing the CFML installed tree
 
-Maybe the tlc binary should be in the path
-  and should have options to report where the CFML library (and TLC) are installed
+-> DemoMake, corriger  let n = null
+
 
 unifier main.ml et makecmj.ml
 
@@ -13,3 +10,5 @@ NullPointers et StrongPointers sont spéciaux puisque l'utilisateur
 va devoir lier son code OCaml avec eux; ils ne devraient pas être
 installés avec la lib standard?
 
+
+

dev/okasaki/BankersDeque_proof.v

@@ -3,6 +3,16 @@ Require Import FuncTactics LibCore.
 Require Import DequeSig_ml DequeSig_proof.
 Require Import BankersDeque_ml.
 
+(* begin hide *)
+Axiom nat_int_eq : forall (n:int) (m:nat),
+  m = abs n -> m = n :> int.
+Axiom abs_pos_le : forall (n:int) (m:nat),
+  0 <= n -> n <= m -> abs n <= m.
+(* todo: prove differently *)
+Implicit Arguments nat_int_eq [n m].
+(* end hide *)
+
+
 Definition C := 2.
 
 Lemma c_spec : c = C.

dev/okasaki/HoodMelvilleQueue_proof.v

@@ -3,6 +3,31 @@ Require Import LibCore FuncTactics.
 Require Import QueueSig_ml QueueSig_proof.
 Require Import HoodMelvilleQueue_ml.
 
+(* begin hide *)
+(*TODO: under construction *)
+
+Axiom abs_le : forall (a:int) (b:nat),
+  (a <= b) -> (abs a <= b).
+
+Lemma take_last_int : forall l (n:int),
+  n > 0 -> n <= length l -> exists x,
+  take (abs n) l = (take (abs (n - 1)) l) & x.
+Proof using.
+  introv Gt Le.
+  destruct (take_struct (abs (n-1)) l) as (l'&L&E).
+  apply abs_le. math.
+  destruct l'.
+    false. rewrite app_nil_r in E.
+    asserts M: (forall A B (f:A->B) (x y:A), x = y -> f x = f y).
+      introv Q. rewrite~ Q.
+    asserts N: (forall A B (f:A->B) (x y:A), x = y -> f x <> f y -> False).
+      introv Q D. apply D. apply M. auto.
+    applys N (@length A) E.
+    rewrite length_take. admit. admit. admit.
+Qed.
+
+(* end hide *)
+
 Module HoodMelvilleQueueSpec <: QueueSigSpec.
 
 (** instantiations *)

examples/CPSappend/Makefile

 
-OCAML_FLAGS := -rectypes
+OCAMLBUILD_FLAGS:=-cflag -rectypes
+OCAML_FLAGS:=-rectypes
 
 include ../Makefile.example
 

examples/DemoMake/Main.ml

@@ -3,4 +3,4 @@ open NullPointers
 
 let g x = Aux.f x
 
-let n = null
\ No newline at end of file
+(* TODO: bug:: let n = null *)
\ No newline at end of file

examples/Dijkstra/Dijkstra_proof.v

 Set Implicit Arguments.
 Generalizable Variables a A.
-Require Import CFLib Dijkstra_ml.
+Require Import CFLib.
+Require Import Dijkstra_ml.
 Open Scope comp_scope.
-Require Import LibArray LibGraph MinInf LibMultiset.
+Require Import LibGraph MinInf LibMultiset.
 
+  
 (*************************************************************)
 (** * More on graphs *)
 
@@ -17,7 +19,7 @@ Definition nodes_index A (G:graph A) (n:int) :=
 
 Definition GraphAdjList (G:graph int) (g:loc) :=
   Hexists N, g ~> Array N
-   \* [nodes_index G (LibArray.length N)]
+   \* [nodes_index G (length N)]
    \* [forall x y w, x \in nodes G ->
          Mem (y,w) (N\(x)) = has_edge G x y w].
 
@@ -116,10 +118,11 @@ Hint Extern 1 (RegisterSpec le) => Provide le_spec.
 
 End MLNextNodeSpec.
 
+
 (*************************************************************)
 (** Properties of [len], the data type representing distances *)
 
-Global Instance len_inhab : Inhab len.
+Global Instance len_inhab : Inhab Dijkstra_ml.len.
 Proof using. apply (prove_Inhab Infinite). Qed.
 Hint Resolve len_inhab.
 
@@ -166,13 +169,21 @@ Lemma graph_adj_index : forall B (G:graph B) n m x,
   nodes_index G n -> x \in nodes G -> n = m -> index m x.
 Proof using. introv N Nx L. subst. rewrite~ <- N. Qed.
 
-Hint Resolve @index_array_length_eq @index_make @index_update.
+Lemma length_update_eq : forall A (i:int) (v:A) (l:list A) (n:int),
+  n = length (l\(i:=v)) -> n = length l.
+Proof. introv H. rewrite~ LibListZ.length_update in H. Qed.
+
+Hint Resolve @LibListZ.index_length_unfold @index_zmake
+   @index_update length_update_eq.
 Hint Extern 1 (nodes_index _ _) => congruence.
 Hint Extern 1 (index ?n ?x) =>
   eapply graph_adj_index; 
   [ try eassumption 
   | instantiate; try eassumption
   | instantiate; try congruence ].
+Hint Extern 1 (?n = length ?l :> int) => 
+  match goal with H: context [ length (l\(?i := ?v)) ] |- _ => 
+   apply (@length_update_eq _ i v) end.
 
 (** Other hints *)
 
@@ -182,7 +193,7 @@ Hint Constructors Mem is_path.
 (** ** Implicit types and implicit parameters *)
 
 Implicit Types V : array bool.
-Implicit Types B : array len.
+Implicit Types B : array Dijkstra_ml.len.
 Implicit Types Q : multiset (int*int).
 Implicit Types p : path int.
 
@@ -190,6 +201,12 @@ Section Invariants.
 Variables (G:graph int) (n:int) (s:int).
 Variables (Neg:nonneg_edges G) (Ind: nodes_index G n) (Ns:s \in nodes G).
 
+Lemma n_pos : n >= 0.
+Proof.
+  lets H: Ind s. lets P: Ns. rewrite H in P. rewrite int_index_def in P. math.
+Qed.
+
+
 (*-----------------------------------------------------------*)
 (** ** Definition of the invariants *)
 
@@ -204,8 +221,8 @@ Record inv_of z V B Q reach : Prop := {
 
 Record inv V B Q reach : Prop := {
   Invof: forall z, inv_of z V B Q reach;
-  SizeV: length V = n;
-  SizeB: length B = n }.
+  SizeV: len V = n;
+  SizeB: len B = n }.
 
 Definition from_out V z p :=
   is_path G s z p /\ ~ istrue(V\(z)).
@@ -281,7 +298,7 @@ Proof using Neg Ind Ns. introv [F _]. apply* from_out_in_nodes. Qed.
 Hint Resolve from_out_in_nodes from_out_cons_in_nodes crossing_in_nodes.
 
 Lemma crossing_step : forall L V x, 
-  ~ istrue (V\(x)) -> length V = n -> x \in nodes G ->
+  ~ istrue (V\(x)) -> len V = n -> x \in nodes G ->
   outgoing_edges x L ->
   new_crossing x L V = crossing (V\(x:=true)).
 Proof using Neg Ind Ns.
@@ -335,10 +352,10 @@ Qed.
 
 Lemma inv_start : 
   (forall x, x \in nodes G -> index n x) ->
-  inv (make n false) (make n Infinite\(s:=Finite 0)) 
-      ('{(s, 0)}) (crossing (make n false)).
+  inv (zmake n false) (zmake n Infinite\(s:=Finite 0)) 
+      ('{(s, 0)}) (crossing (zmake n false)).
 Proof using Neg Ind Ns.
-  introv EQ. asserts Es: (crossing (make n false) s nil). 
+  introv EQ. asserts Es: (crossing (zmake n false) s nil). 
     splits~. splits~. rew_array~.
   constructors. 
   intros z. constructors~.
@@ -355,8 +372,8 @@ Proof using Neg Ind Ns.
     exists 0. subst p. destruct P as [P _]. inverts P.
      split~. rewrite weight_nil. math.
     rew_array* in Ey. false. 
-  rewrite~ length_make.
-  rewrite~ length_update. rewrite~ length_make.
+  rewrite~ length_zmake. apply n_pos.
+  rewrite LibListZ.length_update. rewrite~ length_zmake. apply n_pos.
 Qed.
 
 Lemma inv_end_elim : forall x V B,
@@ -415,14 +432,14 @@ Proof using Neg Ind Ns.
   intros z. lets [Bd Bb Hc Hk]: Inv z. tests: (x = z).
   constructors.
     auto.
-    rew_arr~; auto_false.
-    introv Hd. forwards [? ?]: Hc Hd. split~. rew_arr~; auto_false.
-    introv Nz En. lets ((_&N)&_): En. rew_arr~ in N. false.
+    rew_arr*; auto_false.
+    introv Hd. forwards [? ?]: Hc Hd. split~. rew_arr*; auto_false.
+    introv Nz En. lets ((_&N)&_): En. rew_arr* in N. false.
   constructors.
     auto.
-    rewrite~ crossing_step in Bb.
-    introv Hzd. forwards~ [? M]: Hc Hzd. rewrite~ crossing_step in M.
-    introv Nz En. apply~ Hk. rewrite~ crossing_step.
+    rewrite~ crossing_step in Bb. symmetry; eauto.
+    introv Hzd. forwards~ [? M]: Hc Hzd. rewrite~ crossing_step in M. symmetry; eauto.
+    introv Nz En. apply~ Hk. rewrite~ crossing_step. symmetry; eauto.
 Qed.
 
 Lemma inv_no_update : forall V' B Q x d,
@@ -451,7 +468,7 @@ Proof using Neg Ind Ns.
     If len_gt (B\(y)) dy 
     then inv_of z V' (B\(y:=Finite dy)) ('{(y, dy)} \u Q) (new_crossing x ((y,w)::L) V)
     else inv_of z V' B Q (new_crossing x ((y, w)::L) V)).
-    case_If; constructors~.
+    case_If; constructors~. rewrite~ LibListZ.length_update.
   lets NegP: nonneg_edges_to_path Neg.
   intros z. lets [Bd Bb Hc Hk]: Inv z. tests: (z = y).
   (* case z = y *)
@@ -468,12 +485,12 @@ Proof using Neg Ind Ns.
   introv In. forwards [? ?]: Hc In. split~. auto_false.
   intros py _ Ey. lets [E|(Nxy&(P'&Vy')&(p'&Ep))]: (new_crossing_inv Ey).
     forwards~ (d&D'&In'): Hcomp E.
-    subst V'. rew_array~ in C. auto_false.
+    subst V'. rew_array~ in C. auto_false. eauto.
   (* subcase y not visisted, distance improved *)
   asserts P: (new_crossing x ((y, w) :: L) V y p).
-    subst p. split. intro_subst. subst V'. rew_arr~ in C.
+    subst p. split. intro_subst. subst V'. rew_arr* in C.
     right. split. split. auto.
-    subst V'. tests: (x = y). rew_arr~ in C. rew_array~ in C. exists___~. 
+    subst V'. tests: (x = y). rew_arr* in C. rew_array* in C. exists___~. 
   constructors.
     auto_false.
     introv Vi. rew_arr~. rewrite~ (mininf_finite p). rewrite~ W.
@@ -525,6 +542,13 @@ Definition VQ_type := (array bool * multiset (int*int))%type.
 (*-----------------------------------------------------------*)
 (** Proof of Dijkstra's algorithm using the characteristic formula *)
 
+Parameter ml_array_length_spec : forall a,
+  Spec ml_array_length (l:loc) |R>> forall (t:array a),
+    keep R (l ~> Array t) (fun (x : int) => [x = length t]).
+Hint Extern 1 (RegisterSpec ml_array_length) => Provide ml_array_length_spec.
+
+
+
 Lemma shortest_path_spec :
   Spec shortest_path g a b |R>> forall G,
     nonneg_edges G ->
@@ -540,7 +564,7 @@ Proof using.
   set (hinv := fun VQ => let '(V,Q) := VQ in
     Hexists B, data B V Q \* [inv G n s V B Q (crossing G s V)]).
   xseq (# Hexists V, hinv (V,\{})). 
-  set (W := lexico2 (binary_map (count (=true)) (upto (length N)))
+  set (W := lexico2 (binary_map (zcount (=true)) (upto (length N)))
                     (binary_map (fun Q:multiset(int*int) => card Q:int) (downto 0))). 
   set (C := (fun (VQ:VQ_type) => bool_of (let '(V,Q) := VQ in istrue (!(Q '= \{}))))).
   xwhile_inv W hinv C. 
@@ -584,7 +608,8 @@ Proof using.
   (* -------- iter post-condition -- *) 
   clears update. subst hinv'. unfold data.
   hextract as L B' Q'' I' Leq. hsimpl~ (V',Q'') B'.
-  left. unfolds. subst V'. applys~ @array_count_upto. math.
+  left. unfolds. subst V'. applys~ @LibListZ.zcount_upto. math. 
+    (* TODO: check new hypothesis of zcount_upto *)
   rew_app in Leq. applys~ inv_end_loop I'.
     hnf. intros. rewrite~ <- Adj. rewrite Leq. apply Mem_rev_eq.
   (* ------ node ignored -- *) 

examples/FingerTree/FingerTree_proof.v

 Set Implicit Arguments.
-Require Import CFLib LibSet LibMap LibArray.
+Require Import CFLib LibSet LibMap.
 Require Import ReducerSig_ml ReducerSig_proof FingerTree_ml.
 
 Module MakeSpec (R:MLReducer) (RS:ReducerSigSpec with Module R:=R).

examples/Makefile

 EXAMPLE_DIRS=\
    DemoMake \
-   Dijkstra \
-	FingerTree \
 	Compose \
 	CPSappend \
 	MutableLists \
+	BatchedQueue \
+	FingerTree \
 	BinaryTrees \
-	BatchedQueue
+   Dijkstra
 
 
 

examples/SparseArray/SparseArray_proof.v

@@ -57,6 +57,8 @@ Ltac myunfold :=
   | H: good_sizes _ _ _ _ |- _ => hnf in H 
   end; jauto_set.
 
+TODO: fix array_index as the index_inst typeclass from LibListZ.
+
 Hint Extern 1 (@index _ _ (array_index _) ?t ?i) =>
   myunfold; eassumption.
 Hint Extern 1 (@index _ _ int_index ?t ?i) =>

lib/coq/CFPrim.v

 Set Implicit Arguments.
-Require Export LibInt LibArray CFSpec CFPrint.
+Require Export LibInt CFSpec CFPrint.
 Generalizable Variables a A. 
 
 (* TODO: replace "ml" prefix with a "Pervasives_ml" module *)

lib/coq/CFPrimSpec.v

 Set Implicit Arguments.
-Require Export LibInt LibArray CFSpec CFPrint CFPrim.
+Require Export LibInt LibListZ CFSpec CFPrint CFPrim.
 Generalizable Variables a A. 
 
 
@@ -298,15 +298,22 @@ Hint Extern 1 (RegisterSpec ml_snd) => Provide ml_snd_spec.
 (************************************************************)
 (** Arrays *)
 
+(** The model of an imperative array is a sequence, represented as a list *)
+
+Definition array (A:Type) := list A.
+
 Parameter ArrayOf : forall a A (T:htype A a) (M:array A) (l:loc), hprop.
 
 Notation "'Array'" := (ArrayOf Id).
 
+Notation "'len' L" := (length L : int) (at level 69, only parsing).
+
 Require Import LibBag.
 
 Parameter ml_array_make_spec : forall a,
   Spec ml_array_make (n:int) (v:a) |R>> 
-     R [] (fun l => l ~> Array (LibArray.make n v)).
+     R [] (fun l => l ~> Array (zmake n v)).
+(* Note: zmake is the make function for lists with an argument in Z *)
 
 Parameter ml_array_get_spec : forall a,
   Spec ml_array_get (l:loc) (i:int) |R>> 
@@ -315,12 +322,12 @@ Parameter ml_array_get_spec : forall a,
 
 Parameter ml_array_set_spec : forall a,
   Spec ml_array_set (l:loc) (i:int) (v:a) |R>> 
-    forall (t:array a), index t i -> 
+    forall (t:list a), index t i -> 
     R (l ~> Array t) (# l ~> Array (t\(i:=v))).
 
 Parameter ml_array_length_spec : forall a,
   Spec ml_array_length (l:loc) |R>> forall (t:array a),
-    keep R (l ~> Array t) (fun x => [x = LibArray.length t]).
+    keep R (l ~> Array t) (fun x => [x = length t]).
 
 Hint Extern 1 (RegisterSpec ml_array_make) => Provide ml_array_make_spec.
 Hint Extern 1 (RegisterSpec ml_array_get) => Provide ml_array_get_spec.

lib/coq/CFPrimSpecCredits.v

 Set Implicit Arguments.
-Require Export LibInt LibArray CFSpec CFPrint CFPrimSpec.
+Require Export LibInt LibListZ CFSpec CFPrint CFPrimSpec.
 Generalizable Variables a A. 
 
 Parameter array_make_cst : nat.
@@ -7,6 +7,6 @@ Parameter array_make_cst : nat.
 Parameter ml_array_make_spec : forall a,
   Spec ml_array_make (n:int) (v:a) |R>> 
      R (\$ (abs n * array_make_cst))
-       (fun l => l ~> Array (LibArray.make n v)).
+       (fun l => l ~> Array (zmake n v)).
 
 Hint Extern 1 (RegisterSpecCredits ml_array_make) => Provide ml_array_make_spec.