diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /contrib/correctness/pred.ml |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'contrib/correctness/pred.ml')
-rw-r--r-- | contrib/correctness/pred.ml | 115 |
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 + |