From 0054d117ebed7924a96bcaadc9bcbbef9d372938 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 16 Apr 2002 09:00:50 +0000 Subject: [PATCH] 1. CicReduction moved into CicReductionNaif 2. CicReductionMachine is the new implementation based on an "environment machine". You must make a sumbolic link from one implementation (.ml) to cicReduction.ml --- helm/ocaml/cic_proof_checking/.depend | 8 + helm/ocaml/cic_proof_checking/Makefile | 2 +- .../cic_proof_checking/cicReductionMachine.ml | 382 ++++++++++++++++++ .../cicReductionMachine.mli | 34 ++ .../cic_proof_checking/cicReductionNaif.ml | 268 ++++++++++++ .../cic_proof_checking/cicReductionNaif.mli | 34 ++ 6 files changed, 727 insertions(+), 1 deletion(-) create mode 100644 helm/ocaml/cic_proof_checking/cicReductionMachine.ml create mode 100644 helm/ocaml/cic_proof_checking/cicReductionMachine.mli create mode 100644 helm/ocaml/cic_proof_checking/cicReductionNaif.ml create mode 100644 helm/ocaml/cic_proof_checking/cicReductionNaif.mli diff --git a/helm/ocaml/cic_proof_checking/.depend b/helm/ocaml/cic_proof_checking/.depend index 81126bbdf..64a4fb254 100644 --- a/helm/ocaml/cic_proof_checking/.depend +++ b/helm/ocaml/cic_proof_checking/.depend @@ -6,10 +6,18 @@ cicPp.cmo: cicEnvironment.cmi cicPp.cmi cicPp.cmx: cicEnvironment.cmx cicPp.cmi cicMiniReduction.cmo: cicSubstitution.cmi cicMiniReduction.cmi cicMiniReduction.cmx: cicSubstitution.cmx cicMiniReduction.cmi +cicReductionNaif.cmo: cicEnvironment.cmi cicPp.cmi cicSubstitution.cmi \ + cicReductionNaif.cmi +cicReductionNaif.cmx: cicEnvironment.cmx cicPp.cmx cicSubstitution.cmx \ + cicReductionNaif.cmi cicReduction.cmo: cicEnvironment.cmi cicPp.cmi cicSubstitution.cmi \ cicReduction.cmi cicReduction.cmx: cicEnvironment.cmx cicPp.cmx cicSubstitution.cmx \ cicReduction.cmi +cicReductionMachine.cmo: cicEnvironment.cmi cicPp.cmi cicSubstitution.cmi \ + cicReductionMachine.cmi +cicReductionMachine.cmx: cicEnvironment.cmx cicPp.cmx cicSubstitution.cmx \ + cicReductionMachine.cmi cicTypeChecker.cmo: cicEnvironment.cmi cicPp.cmi cicReduction.cmi \ cicSubstitution.cmi cicTypeChecker.cmi cicTypeChecker.cmx: cicEnvironment.cmx cicPp.cmx cicReduction.cmx \ diff --git a/helm/ocaml/cic_proof_checking/Makefile b/helm/ocaml/cic_proof_checking/Makefile index ad31350c2..591446ccd 100644 --- a/helm/ocaml/cic_proof_checking/Makefile +++ b/helm/ocaml/cic_proof_checking/Makefile @@ -3,7 +3,7 @@ REQUIRES = helm-cic PREDICATES = INTERFACE_FILES = cicSubstitution.mli cicEnvironment.mli cicPp.mli \ - cicMiniReduction.mli cicReduction.mli cicTypeChecker.mli \ + cicMiniReduction.mli cicReductionNaif.mli cicReduction.mli cicReductionMachine.mli cicTypeChecker.mli \ cicCooking.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml new file mode 100644 index 000000000..c69ef5b75 --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml @@ -0,0 +1,382 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +exception CicReductionInternalError;; +exception WrongUriToInductiveDefinition;; + +let fdebug = ref 1;; +let debug t env s = + let rec debug_aux t i = + let module C = Cic in + let module U = UriManager in + CicPp.ppobj (C.Variable ("DEBUG", None, t)) ^ "\n" ^ i + in + if !fdebug = 0 then + begin + print_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "") ; + flush stdout + end +;; + +exception Impossible of int;; +exception ReferenceToDefinition;; +exception ReferenceToAxiom;; +exception ReferenceToVariable;; +exception ReferenceToCurrentProof;; +exception ReferenceToInductiveDefinition;; + +type env = Cic.term list;; +type stack = Cic.term list;; +type config = int * env * Cic.term * stack;; + +(* k is the length of the environment e *) +(* m is the current depth inside the term *) +let unwind' m k e t = + let module C = Cic in + let module S = CicSubstitution in + if e = [] & k = 0 then t else + let rec unwind_aux m = function + C.Rel n as t -> if n <= m then t else + let d = try Some (List.nth e (n-m-1)) + with _ -> None + in (match d with + Some t' -> if m = 0 then t' + else S.lift m t' + | None -> C.Rel (n-k)) + | C.Var _ as t -> t + | C.Meta _ as t -> t + | C.Sort _ as t -> t + | C.Implicit as t -> t + | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ??? *) + | C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t) + | C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t) + | C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t) + | C.Appl l -> C.Appl (List.map (unwind_aux m) l) + | C.Const _ as t -> t + | C.Abst _ as t -> t + | C.MutInd _ as t -> t + | C.MutConstruct _ as t -> t + | C.MutCase (sp,cookingsno,i,outt,t,pl) -> + C.MutCase (sp,cookingsno,i,unwind_aux m outt, unwind_aux m t, + List.map (unwind_aux m) pl) + | C.Fix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> (name, i, unwind_aux m ty, unwind_aux (m+len) bo)) + fl + in + C.Fix (i, substitutedfl) + | C.CoFix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,ty,bo) -> (name, unwind_aux m ty, unwind_aux (m+len) bo)) + fl + in + C.CoFix (i, substitutedfl) + in + unwind_aux m t + ;; + +let unwind = + unwind' 0 +;; + +let rec reduce : config -> Cic.term = + let module C = Cic in + let module S = CicSubstitution in + function + (k, e, (C.Rel n as t), s) -> let d = +(* prerr_string ("Rel " ^ string_of_int n) ; flush stderr ; *) + try Some (List.nth e (n-1)) + with _ -> None + in (match d with + Some t' -> reduce (0, [],t',s) + | None -> if s = [] then C.Rel (n-k) + else C.Appl (C.Rel (n-k)::s)) + | (k, e, (C.Var uri as t), s) -> + (match CicEnvironment.get_cooked_obj uri 0 with + C.Definition _ -> raise ReferenceToDefinition + | C.Axiom _ -> raise ReferenceToAxiom + | C.CurrentProof _ -> raise ReferenceToCurrentProof + | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + | C.Variable (_,None,_) -> if s = [] then t else C.Appl (t::s) + | C.Variable (_,Some body,_) -> reduce (0, [], body, s) + ) + | (k, e, (C.Meta _ as t), s) -> if s = [] then t + else C.Appl (t::s) + | (k, e, (C.Sort _ as t), s) -> t (* s should be empty *) + | (k, e, (C.Implicit as t), s) -> t (* s should be empty *) + | (k, e, (C.Cast (te,ty) as t), s) -> reduce (k, e,te,s) (* s should be empty *) + | (k, e, (C.Prod _ as t), s) -> unwind k e t (* s should be empty *) + | (k, e, (C.Lambda (_,_,t) as t'), []) -> unwind k e t' + | (k, e, C.Lambda (_,_,t), p::s) -> +(* prerr_string ("Lambda body: " ^ CicPp.ppterm t) ; flush stderr ; *) + reduce (k+1, p::e,t,s) + | (k, e, (C.LetIn (_,m,t) as t'), s) -> let m' = reduce (k,e,m,[]) in + reduce (k+1, m'::e,t,s) + | (k, e, C.Appl [], s) -> raise (Impossible 1) + (* this is lazy + | (k, e, C.Appl (he::tl), s) -> let tl' = List.map (unwind k e) tl + in reduce (k, e, he, (List.append tl' s)) *) + (* this is strict *) + | (k, e, C.Appl (he::tl), s) -> + (* constants are NOT unfolded *) + let red = function + C.Const _ as t -> t + | t -> reduce (k, e,t,[]) in + let tl' = List.map red tl in + reduce (k, e, he , List.append tl' s) +(* + | (k, e, C.Appl ((C.Lambda _ as he)::tl), s) + | (k, e, C.Appl ((C.Const _ as he)::tl), s) + | (k, e, C.Appl ((C.MutCase _ as he)::tl), s) + | (k, e, C.Appl ((C.Fix _ as he)::tl), s) -> +(* strict evaluation, but constants are NOT + unfolded *) + let red = function + C.Const _ as t -> t + | t -> reduce (k, e,t,[]) in + let tl' = List.map red tl in + reduce (k, e, he , List.append tl' s) + | (k, e, C.Appl l, s) -> C.Appl (List.append (List.map (unwind k e) l) s) *) + | (k, e, (C.Const (uri,cookingsno) as t), s) -> + (match CicEnvironment.get_cooked_obj uri cookingsno with + C.Definition (_,body,_,_) -> reduce (0, [], body, s) + (* constants are closed *) + | C.Axiom _ -> if s = [] then t else C.Appl (t::s) + | C.Variable _ -> raise ReferenceToVariable + | C.CurrentProof (_,_,body,_) -> reduce (0, [], body, s) + | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + ) + | (k, e, (C.Abst _ as t), s) -> t (* s should be empty ????? *) + | (k, e, (C.MutInd (uri,_,_) as t),s) -> let t' = unwind k e t in + if s = [] then t' else C.Appl (t'::s) + | (k, e, (C.MutConstruct (uri,_,_,_) as t),s) -> + let t' = unwind k e t in + if s = [] then t' else C.Appl (t'::s) + | (k, e, (C.MutCase (mutind,cookingsno,i,_,term,pl) as t),s) -> + let decofix = + function + C.CoFix (i,fl) as t -> + let (_,_,body) = List.nth fl i in + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) + fl + body + in + reduce (0,[],body',[]) + | C.Appl (C.CoFix (i,fl) :: tl) -> + let (_,_,body) = List.nth fl i in + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) + fl + body + in + reduce (0,[], body', tl) + | t -> t + in + (match decofix (reduce (k, e,term,[])) with + C.MutConstruct (_,_,_,j) -> reduce (k, e, (List.nth pl (j-1)), s) + | C.Appl (C.MutConstruct (_,_,_,j) :: tl) -> + let (arity, r, num_ingredients) = + match CicEnvironment.get_obj mutind with + C.InductiveDefinition (tl,ingredients,r) -> + let (_,_,arity,_) = List.nth tl i + and num_ingredients = + List.fold_right + (fun (k,l) i -> + if k < cookingsno then i + List.length l else i + ) ingredients 0 + in + (arity,r,num_ingredients) + | _ -> raise WrongUriToInductiveDefinition + in + let ts = + let num_to_eat = r + num_ingredients in + let rec eat_first = + function + (0,l) -> l + | (n,he::tl) when n > 0 -> eat_first (n - 1, tl) + | _ -> raise (Impossible 5) + in + eat_first (num_to_eat,tl) + in + reduce (k, e, (List.nth pl (j-1)),(ts@s)) + | C.Abst _| C.Cast _ | C.Implicit -> + raise (Impossible 2) (* we don't trust our whd ;-) *) + | _ -> let t' = unwind k e t in + if s = [] then t' else C.Appl (t'::s) + ) + | (k, e, (C.Fix (i,fl) as t), s) -> + let (_,recindex,_,body) = List.nth fl i in + let recparam = + try + Some (List.nth s recindex) + with + _ -> None + in + (match recparam with + Some recparam -> + (match reduce (0,[],recparam,[]) with + (* match recparam with *) + C.MutConstruct _ + | C.Appl ((C.MutConstruct _)::_) -> + (* OLD + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl))) + fl + body + in + reduce (k, e, body', s) *) + (* NEW *) + let leng = List.length fl in + let fl' = + let unwind_fl (name,recindex,typ,body) = + (name,recindex,unwind' leng k e typ, unwind' leng k e body) in + List.map unwind_fl fl in + let new_env = + let counter = ref leng in + let rec build_env e = + if !counter = 0 then e else (decr counter; + build_env ((C.Fix (!counter,fl'))::e)) in + build_env e in + reduce (k+leng, new_env, body,s) + | _ -> let t' = unwind k e t in + if s = [] then t' else C.Appl (t'::s) + ) + | None -> let t' = unwind k e t in + if s = [] then t' else C.Appl (t'::s) + ) + | (k, e,(C.CoFix (i,fl) as t),s) -> let t' = unwind k e t in + if s = [] then t' else C.Appl (t'::s);; + +let rec whd = let module C = Cic in + function + C.Rel _ as t -> t + | C.Var _ as t -> reduce (0, [], t, []) + | C.Meta _ as t -> t + | C.Sort _ as t -> t + | C.Implicit as t -> t + | C.Cast (te,ty) -> whd te + | C.Prod _ as t -> t + | C.Lambda _ as t -> t + | C.LetIn (n,s,t) -> reduce (1, [s], t, []) + | C.Appl [] -> raise (Impossible 1) + | C.Appl (he::tl) -> reduce (0, [], he, tl) + | C.Const _ as t -> reduce (0, [], t, []) + | C.Abst _ as t -> t + | C.MutInd _ as t -> t + | C.MutConstruct _ as t -> t + | C.MutCase _ as t -> reduce (0, [], t, []) + | C.Fix _ as t -> reduce (0, [], t, []) + | C.CoFix _ as t -> reduce (0, [], t, []) + ;; + +(* let whd t = reduce (0, [],t,[]);; + let res = reduce (0, [],t,[]) in + let rescsc = CicReductionNaif.whd t in + if not (CicReductionNaif.are_convertible res rescsc) then + begin + prerr_endline ("PRIMA: " ^ CicPp.ppterm t) ; + flush stderr ; + prerr_endline ("DOPO: " ^ CicPp.ppterm res) ; + flush stderr ; + prerr_endline ("CSC: " ^ CicPp.ppterm rescsc) ; + flush stderr ; + assert false ; + end + else + res ;; *) + + +(* t1, t2 must be well-typed *) +let are_convertible = + let rec aux t1 t2 = + if t1 = t2 then true + else + let aux2 t1 t2 = + let module U = UriManager in + let module C = Cic in + match (t1,t2) with + (C.Rel n1, C.Rel n2) -> n1 = n2 + | (C.Var uri1, C.Var uri2) -> U.eq uri1 uri2 + | (C.Meta n1, C.Meta n2) -> n1 = n2 + | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *) + | (C.Prod (_,s1,t1), C.Prod(_,s2,t2)) -> + aux s1 s2 && aux t1 t2 + | (C.Lambda (_,s1,t1), C.Lambda(_,s2,t2)) -> + aux s1 s2 && aux t1 t2 + | (C.Appl l1, C.Appl l2) -> + (try + List.fold_right2 (fun x y b -> aux x y && b) l1 l2 true + with + Invalid_argument _ -> false + ) + | (C.Const (uri1,_), C.Const (uri2,_)) -> + U.eq uri1 uri2 + | (C.MutInd (uri1,k1,i1), C.MutInd (uri2,k2,i2)) -> + U.eq uri1 uri2 && i1 = i2 + | (C.MutConstruct (uri1,_,i1,j1), C.MutConstruct (uri2,_,i2,j2)) -> + U.eq uri1 uri2 && i1 = i2 && j1 = j2 + | (C.MutCase (uri1,_,i1,outtype1,term1,pl1), + C.MutCase (uri2,_,i2,outtype2,term2,pl2)) -> + (* aux outtype1 outtype2 should be true if aux pl1 pl2 *) + U.eq uri1 uri2 && i1 = i2 && aux outtype1 outtype2 && + aux term1 term2 && + List.fold_right2 (fun x y b -> b && aux x y) pl1 pl2 true + | (C.Fix (i1,fl1), C.Fix (i2,fl2)) -> + i1 = i2 && + List.fold_right2 + (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) b -> + b && recindex1 = recindex2 && aux ty1 ty2 && aux bo1 bo2) + fl1 fl2 true + | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) -> + i1 = i2 && + List.fold_right2 + (fun (_,ty1,bo1) (_,ty2,bo2) b -> + b && aux ty1 ty2 && aux bo1 bo2) + fl1 fl2 true + | (_,_) -> false + in + if aux2 t1 t2 then true + else aux2 (whd t1) (whd t2) +in + aux +;; + + + + + + + diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.mli b/helm/ocaml/cic_proof_checking/cicReductionMachine.mli new file mode 100644 index 000000000..d61bc7251 --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.mli @@ -0,0 +1,34 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +exception WrongUriToInductiveDefinition +exception ReferenceToDefinition +exception ReferenceToAxiom +exception ReferenceToVariable +exception ReferenceToCurrentProof +exception ReferenceToInductiveDefinition +val fdebug : int ref +val whd : Cic.term -> Cic.term +val are_convertible : Cic.term -> Cic.term -> bool diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml new file mode 100644 index 000000000..e0ad91f59 --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml @@ -0,0 +1,268 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +exception CicReductionInternalError;; +exception WrongUriToInductiveDefinition;; + +let fdebug = ref 1;; +let debug t env s = + let rec debug_aux t i = + let module C = Cic in + let module U = UriManager in + CicPp.ppobj (C.Variable ("DEBUG", None, t)) ^ "\n" ^ i + in + if !fdebug = 0 then + begin + print_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "") ; + flush stdout + end +;; + +exception Impossible of int;; +exception ReferenceToDefinition;; +exception ReferenceToAxiom;; +exception ReferenceToVariable;; +exception ReferenceToCurrentProof;; +exception ReferenceToInductiveDefinition;; + +(* takes a well-typed term *) +let whd = + let rec whdaux l = + let module C = Cic in + let module S = CicSubstitution in + function + C.Rel _ as t -> if l = [] then t else C.Appl (t::l) + | C.Var uri as t -> + (match CicEnvironment.get_cooked_obj uri 0 with + C.Definition _ -> raise ReferenceToDefinition + | C.Axiom _ -> raise ReferenceToAxiom + | C.CurrentProof _ -> raise ReferenceToCurrentProof + | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l) + | C.Variable (_,Some body,_) -> whdaux l body + ) + | C.Meta _ as t -> if l = [] then t else C.Appl (t::l) + | C.Sort _ as t -> t (* l should be empty *) + | C.Implicit as t -> t + | C.Cast (te,ty) -> whdaux l te (*CSC E' GIUSTO BUTTARE IL CAST? *) + | C.Prod _ as t -> t (* l should be empty *) + | C.Lambda (name,s,t) as t' -> + (match l with + [] -> t' + | he::tl -> whdaux tl (S.subst he t) + (* when name is Anonimous the substitution should be superfluous *) + ) + | C.LetIn (n,s,t) -> whdaux l (S.subst (whdaux [] s) t) + | C.Appl (he::tl) -> whdaux (tl@l) he + | C.Appl [] -> raise (Impossible 1) + | C.Const (uri,cookingsno) as t -> + (match CicEnvironment.get_cooked_obj uri cookingsno with + C.Definition (_,body,_,_) -> whdaux l body + | C.Axiom _ -> if l = [] then t else C.Appl (t::l) + | C.Variable _ -> raise ReferenceToVariable + | C.CurrentProof (_,_,body,_) -> whdaux l body + | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + ) + | C.Abst _ as t -> t (*CSC l should be empty ????? *) + | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l) + | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l) + | C.MutCase (mutind,cookingsno,i,_,term,pl) as t -> + let decofix = + function + C.CoFix (i,fl) as t -> + let (_,_,body) = List.nth fl i in + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) + fl + body + in + whdaux [] body' + | C.Appl (C.CoFix (i,fl) :: tl) -> + let (_,_,body) = List.nth fl i in + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) + fl + body + in + whdaux tl body' + | t -> t + in + (match decofix (whdaux [] term) with + C.MutConstruct (_,_,_,j) -> whdaux l (List.nth pl (j-1)) + | C.Appl (C.MutConstruct (_,_,_,j) :: tl) -> + let (arity, r, num_ingredients) = + match CicEnvironment.get_obj mutind with + C.InductiveDefinition (tl,ingredients,r) -> + let (_,_,arity,_) = List.nth tl i + and num_ingredients = + List.fold_right + (fun (k,l) i -> + if k < cookingsno then i + List.length l else i + ) ingredients 0 + in + (arity,r,num_ingredients) + | _ -> raise WrongUriToInductiveDefinition + in + let ts = + let num_to_eat = r + num_ingredients in + let rec eat_first = + function + (0,l) -> l + | (n,he::tl) when n > 0 -> eat_first (n - 1, tl) + | _ -> raise (Impossible 5) + in + eat_first (num_to_eat,tl) + in + whdaux (ts@l) (List.nth pl (j-1)) + | C.Abst _| C.Cast _ | C.Implicit -> + raise (Impossible 2) (* we don't trust our whd ;-) *) + | _ -> t + ) + | C.Fix (i,fl) as t -> + let (_,recindex,_,body) = List.nth fl i in + let recparam = + try + Some (List.nth l recindex) + with + _ -> None + in + (match recparam with + Some recparam -> + (match whdaux [] recparam with + C.MutConstruct _ + | C.Appl ((C.MutConstruct _)::_) -> + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl))) + fl + body + in + (* Possible optimization: substituting whd recparam in l *) + whdaux l body' + | _ -> if l = [] then t else C.Appl (t::l) + ) + | None -> if l = [] then t else C.Appl (t::l) + ) + | C.CoFix (i,fl) as t -> + (*CSC vecchio codice + let (_,_,body) = List.nth fl i in + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) + fl + body + in + whdaux l body' + *) + if l = [] then t else C.Appl (t::l) + in + whdaux [] +;; + +(* t1, t2 must be well-typed *) +let are_convertible t1 t2 = + let module U = UriManager in + let rec aux t1 t2 = + debug t1 [t2] "PREWHD"; + (* this trivial euristic cuts down the total time of about five times ;-) *) + (* this because most of the time t1 and t2 are "sintactically" the same *) + if t1 = t2 then + true + else + begin + let module C = Cic in + let t1' = whd t1 + and t2' = whd t2 in + debug t1' [t2'] "POSTWHD"; + (*if !fdebug = 0 then ignore(Unix.system "read" );*) + match (t1',t2') with + (C.Rel n1, C.Rel n2) -> n1 = n2 + | (C.Var uri1, C.Var uri2) -> U.eq uri1 uri2 + | (C.Meta n1, C.Meta n2) -> n1 = n2 + | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *) + | (C.Prod (_,s1,t1), C.Prod(_,s2,t2)) -> + aux s1 s2 && aux t1 t2 + | (C.Lambda (_,s1,t1), C.Lambda(_,s2,t2)) -> + aux s1 s2 && aux t1 t2 + | (C.Appl l1, C.Appl l2) -> + (try + List.fold_right2 (fun x y b -> aux x y && b) l1 l2 true + with + Invalid_argument _ -> false + ) + | (C.Const (uri1,_), C.Const (uri2,_)) -> + (*CSC: questo commento e' chiaro o delirante? Io lo sto scrivendo *) + (*CSC: mentre sono delirante, quindi ... *) + (* WARNING: it is really important that the two cookingsno are not *) + (* checked for equality. This allows not to cook an object with no *) + (* ingredients only to update the cookingsno. E.g: if a term t has *) + (* a reference to a term t1 which does not depend on any variable *) + (* and t1 depends on a term t2 (that can't depend on any variable *) + (* because of t1), then t1 cooked at every level could be the same *) + (* as t1 cooked at level 0. Doing so, t2 will be extended in t *) + (* with cookingsno 0 and not 2. But this will not cause any trouble*) + (* if here we don't check that the two cookingsno are equal. *) + U.eq uri1 uri2 + | (C.MutInd (uri1,k1,i1), C.MutInd (uri2,k2,i2)) -> + (* WARNIG: see the previous warning *) + U.eq uri1 uri2 && i1 = i2 + | (C.MutConstruct (uri1,_,i1,j1), C.MutConstruct (uri2,_,i2,j2)) -> + (* WARNIG: see the previous warning *) + U.eq uri1 uri2 && i1 = i2 && j1 = j2 + | (C.MutCase (uri1,_,i1,outtype1,term1,pl1), + C.MutCase (uri2,_,i2,outtype2,term2,pl2)) -> + (* WARNIG: see the previous warning *) + (* aux outtype1 outtype2 should be true if aux pl1 pl2 *) + U.eq uri1 uri2 && i1 = i2 && aux outtype1 outtype2 && + aux term1 term2 && + List.fold_right2 (fun x y b -> b && aux x y) pl1 pl2 true + | (C.Fix (i1,fl1), C.Fix (i2,fl2)) -> + i1 = i2 && + List.fold_right2 + (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) b -> + b && recindex1 = recindex2 && aux ty1 ty2 && aux bo1 bo2) + fl1 fl2 true + | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) -> + i1 = i2 && + List.fold_right2 + (fun (_,ty1,bo1) (_,ty2,bo2) b -> + b && aux ty1 ty2 && aux bo1 bo2) + fl1 fl2 true + | (C.Abst _, _) | (_, C.Abst _) | (C.Cast _, _) | (_, C.Cast _) + | (C.Implicit, _) | (_, C.Implicit) -> + raise (Impossible 3) (* we don't trust our whd ;-) *) + | (_,_) -> + debug t1' [t2'] "NOT-CONVERTIBLE" ; + false + end + in + aux t1 t2 +;; diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.mli b/helm/ocaml/cic_proof_checking/cicReductionNaif.mli new file mode 100644 index 000000000..d61bc7251 --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.mli @@ -0,0 +1,34 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +exception WrongUriToInductiveDefinition +exception ReferenceToDefinition +exception ReferenceToAxiom +exception ReferenceToVariable +exception ReferenceToCurrentProof +exception ReferenceToInductiveDefinition +val fdebug : int ref +val whd : Cic.term -> Cic.term +val are_convertible : Cic.term -> Cic.term -> bool -- 2.39.2