From a86e50c2f080bd288d1a37b27fd4d0ea3044c5df Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 28 May 2002 17:37:10 +0000 Subject: [PATCH] * Bug fixed: syntactic equality for CIC term (which was used in the Fold tactic) is not the structural equality of Ocaml (i.e. '=') because of cooking numbers that can differ denoting the very same term. So a new function syntactic_equality has been added to proofEngineReduction.ml and it is now used for Fold. --- helm/gTopLevel/proofEngine.ml | 6 ++- helm/gTopLevel/proofEngineReduction.ml | 58 ++++++++++++++++++++++++++ 2 files changed, 62 insertions(+), 2 deletions(-) diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 695ef7a7f..f33c69e35 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -749,8 +749,10 @@ let fold term = (* the type of one metavariable. So we replace it everywhere. *) (*CSC: ma si potrebbe ovviare al problema. Ma non credo *) (*CSC: che si guadagni nulla in fatto di efficienza. *) - let replace = ProofEngineReduction.replace - ~equality:(=) ~what:term' ~with_what:term + let replace = + ProofEngineReduction.replace + ~equality:(ProofEngineReduction.syntactic_equality) + ~what:term' ~with_what:term in let ty' = replace ty in let context' = diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml index 7d4a79960..460c8d726 100644 --- a/helm/gTopLevel/proofEngineReduction.ml +++ b/helm/gTopLevel/proofEngineReduction.ml @@ -45,6 +45,64 @@ exception ReferenceToInductiveDefinition;; exception WrongUriToInductiveDefinition;; exception RelToHiddenHypothesis;; +(* syntactic_equality up to cookingsno for uris *) +(* (which is often syntactically irrilevant) *) +let rec syntactic_equality t t' = + let module C = Cic in + if t = t' then true + else + match t,t' with + C.Rel _, C.Rel _ + | C.Var _, C.Var _ + | C.Meta _, C.Meta _ + | C.Sort _, C.Sort _ + | C.Implicit, C.Implicit -> false (* we already know that t != t' *) + | C.Cast (te,ty), C.Cast (te',ty') -> + syntactic_equality te te' && + syntactic_equality ty ty' + | C.Prod (n,s,t), C.Prod (n',s',t') -> + n = n' && + syntactic_equality s s' && + syntactic_equality t t' + | C.Lambda (n,s,t), C.Lambda (n',s',t') -> + n = n' && + syntactic_equality s s' && + syntactic_equality t t' + | C.LetIn (n,s,t), C.LetIn(n',s',t') -> + n = n' && + syntactic_equality s s' && + syntactic_equality t t' + | C.Appl l, C.Appl l' -> + List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l' + | C.Const (uri,_), C.Const (uri',_) -> UriManager.eq uri uri' + | C.Abst _, C.Abst _ -> assert false + | C.MutInd (uri,_,i), C.MutInd (uri',_,i') -> + UriManager.eq uri uri' && i = i' + | C.MutConstruct (uri,_,i,j), C.MutConstruct (uri',_,i',j') -> + UriManager.eq uri uri' && i = i' && j = j' + | C.MutCase (sp,_,i,outt,t,pl), C.MutCase (sp',_,i',outt',t',pl') -> + UriManager.eq sp sp' && i = i' && + syntactic_equality outt outt' && + syntactic_equality t t' && + List.fold_left2 + (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl' + | C.Fix (i,fl), C.Fix (i',fl') -> + i = i' && + List.fold_left2 + (fun b (name,i,ty,bo) (name',i',ty',bo') -> + b && name = name' && i = i' && + syntactic_equality ty ty' && + syntactic_equality bo bo') true fl fl' + | C.CoFix (i,fl), C.CoFix (i',fl') -> + i = i' && + List.fold_left2 + (fun b (name,ty,bo) (name',ty',bo') -> + b && name = name' && + syntactic_equality ty ty' && + syntactic_equality bo bo') true fl fl' + | _,_ -> false +;; + (* "textual" replacement of a subterm with another one *) let replace ~equality ~what ~with_what ~where = let module C = Cic in -- 2.39.2