1 files changed, 115 insertions, 0 deletions
diff --git a/contrib/correctness/pred.ml b/contrib/correctness/pred.ml
new file mode 100644
index 00000000..732dcf08
--- /dev/null
+++ b/contrib/correctness/pred.ml
@@ -0,0 +1,115 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Certification of Imperative Programs / Jean-Christophe Filliâtre *)
+
+(* $Id: pred.ml,v 1.6.14.1 2004/07/16 19:30:05 herbelin Exp $ *)
+
+open Pp
+open Past
+open Pmisc
+
+let rec cc_subst subst = function
+  | CC_var id as c -> 
+      (try CC_expr (List.assoc id subst) with Not_found -> c)
+  | CC_letin (b,ty,bl,c1,c2) ->
+      CC_letin (b, real_subst_in_constr subst ty, cc_subst_binders subst bl,
+		cc_subst subst c1, cc_subst (cc_cross_binders subst bl) c2)
+  | CC_lam (bl, c) ->
+      CC_lam (cc_subst_binders subst bl, 
+	      cc_subst (cc_cross_binders subst bl) c)
+  | CC_app (c, cl) ->
+      CC_app (cc_subst subst c, List.map (cc_subst subst) cl)
+  | CC_tuple (b, tl, cl) ->
+      CC_tuple (b, List.map (real_subst_in_constr subst) tl,
+		List.map (cc_subst subst) cl)
+  | CC_case (ty, c, cl) ->
+      CC_case (real_subst_in_constr subst ty, cc_subst subst c,
+	       List.map (cc_subst subst) cl)
+  | CC_expr c ->
+      CC_expr (real_subst_in_constr subst c)
+  | CC_hole ty ->
+      CC_hole (real_subst_in_constr subst ty)
+
+and cc_subst_binders subst = List.map (cc_subst_binder subst)
+
+and cc_subst_binder subst = function
+  | id,CC_typed_binder c -> id,CC_typed_binder (real_subst_in_constr subst c)
+  | b -> b
+
+and cc_cross_binders subst = function
+  | [] -> subst
+  | (id,_) :: bl -> cc_cross_binders (List.remove_assoc id subst) bl
+
+(* here we only perform eta-reductions on programs to eliminate
+ * redexes of the kind
+ *
+ *   let (x1,...,xn) = e in (x1,...,xn)  -->  e
+ *
+ *)
+
+let is_eta_redex bl al =
+  try
+    List.for_all2
+      (fun (id,_) t -> match t with CC_var id' -> id=id' | _ -> false)
+      bl al
+  with
+      Invalid_argument("List.for_all2") -> false
+
+let rec red = function
+  | CC_letin (_, _, [id,_], CC_expr c1, e2) ->
+      red (cc_subst [id,c1] e2)
+  | CC_letin (dep, ty, bl, e1, e2) ->
+      begin match red e2 with
+	| CC_tuple (false,tl,al) ->
+	    if is_eta_redex bl al then
+	      red e1
+	    else
+	      CC_letin (dep, ty, bl, red e1,
+			CC_tuple (false,tl,List.map red al))
+	| e -> CC_letin (dep, ty, bl, red e1, e)
+      end
+  | CC_lam (bl, e) ->
+      CC_lam (bl, red e)
+  | CC_app (e, al) ->
+      CC_app (red e, List.map red al)
+  | CC_case (ty, e1, el) ->
+      CC_case (ty, red e1, List.map red el)
+  | CC_tuple (dep, tl, al) ->
+      CC_tuple (dep, tl, List.map red al)
+  | e -> e
+
+
+(* How to reduce uncomplete proof terms when they have become constr *)
+
+open Term
+open Reductionops
+
+(* Il ne faut pas reduire de redexe (beta/iota) qui impliquerait
+ * la substitution d'une métavariable.
+ * 
+ * On commence par rendre toutes les applications binaire (strong bin_app)
+ * puis on applique la reduction spéciale programmes définie dans
+ * typing/reduction *)
+
+(*i
+let bin_app = function
+  | DOPN(AppL,v) as c ->
+      (match Array.length v with
+	 | 1 -> v.(0)
+	 | 2 -> c
+	 | n ->
+	     let f = DOPN(AppL,Array.sub v 0 (pred n)) in
+	     DOPN(AppL,[|f;v.(pred n)|]))
+  | c -> c
+i*)
+
+let red_cci c = 
+  (*i let c = strong bin_app c in i*) 
+  strong whd_programs (Global.env ()) Evd.empty c
+