X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReductionNaif.ml;h=1ab5e92bc49a64fe89a4829326658b7cdcab98e5;hb=756c1e676368d9addc75438bce97a71e34287f18;hp=b4296f1c14081c0aebb3c08ce2957e115a38dfd9;hpb=c169f48a31abaea726adf852081e274fcb67f770;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml index b4296f1c1..1ab5e92bc 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml @@ -48,12 +48,16 @@ exception ReferenceToCurrentProof;; exception ReferenceToInductiveDefinition;; (* takes a well-typed term *) -let whd = +let whd context = 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.Rel n as t -> + (match List.nth context (n-1) with + C.Decl _ -> if l = [] then t else C.Appl (t::l) + | C.Def bo -> whdaux l (S.lift n bo) + ) | C.Var uri as t -> (match CicEnvironment.get_cooked_obj uri 0 with C.Definition _ -> raise ReferenceToDefinition @@ -171,102 +175,109 @@ let whd = | 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 +(*CSC +function t -> +prerr_endline ("PRIMA WHD" ^ CicPp.ppterm t) ; flush stderr ; +List.iter (function (Cic.Decl t) -> prerr_endline ("Context: " ^ CicPp.ppterm t) | (Cic.Def t) -> prerr_endline ("Context:= " ^ CicPp.ppterm t)) context ; flush stderr ; prerr_endline " 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 ;-) *) - | (_,_) -> false - end - in - if aux2 t1 t2 then true - else - begin - debug t1 [t2] "PREWHD"; - let t1' = whd t1 - and t2' = whd t2 in - debug t1' [t2'] "POSTWHD"; - aux2 t1' t2' - end + let rec aux context t1 t2 = + let aux2 t1 t2 = + (* 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 + 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 context s1 s2 && aux ((C.Decl s1)::context) t1 t2 + | (C.Lambda (_,s1,t1), C.Lambda(_,s2,t2)) -> + aux context s1 s2 && aux ((C.Decl s1)::context) t1 t2 + | (C.LetIn (_,s1,t1), C.LetIn(_,s2,t2)) -> + aux context s1 s2 && aux ((C.Def s1)::context) t1 t2 + | (C.Appl l1, C.Appl l2) -> + (try + List.fold_right2 (fun x y b -> aux context 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 context outtype1 outtype2 should be true if *) + (* aux context pl1 pl2 *) + U.eq uri1 uri2 && i1 = i2 && aux context outtype1 outtype2 && + aux context term1 term2 && + List.fold_right2 (fun x y b -> b && aux context x y) pl1 pl2 true + | (C.Fix (i1,fl1), C.Fix (i2,fl2)) -> +(*CSC: C.Decl e' giusto? *) + let tys = List.map (function (_,_,ty,_) -> C.Decl ty) fl1 in + i1 = i2 && + List.fold_right2 + (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) b -> + b && recindex1 = recindex2 && aux context ty1 ty2 && + aux (tys@context) bo1 bo2) + fl1 fl2 true + | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) -> +(*CSC: C.Decl e' giusto? *) + let tys = List.map (function (_,ty,_) -> C.Decl ty) fl1 in + i1 = i2 && + List.fold_right2 + (fun (_,ty1,bo1) (_,ty2,bo2) b -> + b && aux context ty1 ty2 && aux (tys@context) 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 ;-) *) + | (_,_) -> false + end + in + if aux2 t1 t2 then true + else + begin + debug t1 [t2] "PREWHD"; + let t1' = whd context t1 + and t2' = whd context t2 in + debug t1' [t2'] "POSTWHD"; + aux2 t1' t2' + end in aux ;;