From c7eb56246dc1199f098ed6c8c77aa08fea9a62f8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 14 Oct 2002 11:44:07 +0000 Subject: [PATCH] - bug fixed: some liftings were missing in the implementation of rewrite - new feature: rewrite now works up to alpha-equivalence --- helm/gTopLevel/fourierR.ml | 3 +- helm/gTopLevel/gTopLevel.ml | 2 +- helm/gTopLevel/proofEngine.ml | 3 +- helm/gTopLevel/proofEngineReduction.ml | 152 ++++++++++++------------ helm/gTopLevel/proofEngineReduction.mli | 6 +- 5 files changed, 83 insertions(+), 83 deletions(-) diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index d2725ff15..c46973e2c 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -57,7 +57,8 @@ let rewrite_tac ~term:equality ~status:(proof,goal) = let t1' = CicSubstitution.lift 1 t1 in let gty'' = ProofEngineReduction.replace_lifting - ~equality:ProofEngineReduction.syntactic_equality + ~equality: + (ProofEngineReduction.syntactic_equality ~alpha_equivalence:true) ~what:t1' ~with_what:(C.Rel 1) ~where:gty' in C.Lambda (C.Name "dummy_for_rewrite", ty, gty'') diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 3c37b3ed2..cbfe18e73 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -1466,7 +1466,7 @@ class rendering_window output proofw (label : GMisc.label) = GButton.button ~label:"Fourier" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in let rewriteb = - GButton.button ~label:"Rewrite" + GButton.button ~label:"Rewrite ->" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in let outputhtml = GHtml.xmhtml diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 0885f3037..64d68a37e 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -224,7 +224,8 @@ let fold term = (*CSC: che si guadagni nulla in fatto di efficienza. *) let replace = ProofEngineReduction.replace - ~equality:(ProofEngineReduction.syntactic_equality) + ~equality: + (ProofEngineReduction.syntactic_equality ~alpha_equivalence:false) ~what:term' ~with_what:term in let ty' = replace ty in diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml index 442873cec..bb724fc75 100644 --- a/helm/gTopLevel/proofEngineReduction.ml +++ b/helm/gTopLevel/proofEngineReduction.ml @@ -47,72 +47,65 @@ exception RelToHiddenHypothesis;; (* syntactic_equality up to cookingsno for uris *) (* (which is often syntactically irrilevant) *) -let rec syntactic_equality t t' = +let syntactic_equality ~alpha_equivalence = 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' -> - (try - List.fold_left2 - (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l' - with - Invalid_argument _ -> false) - | C.Const (uri,_), C.Const (uri',_) -> UriManager.eq uri uri' - | 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' && + let rec aux t t' = + 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') -> + aux te te' && aux ty ty' + | C.Prod (n,s,t), C.Prod (n',s',t') -> + (alpha_equivalence || n = n') && aux s s' && aux t t' + | C.Lambda (n,s,t), C.Lambda (n',s',t') -> + (alpha_equivalence || n = n') && aux s s' && aux t t' + | C.LetIn (n,s,t), C.LetIn(n',s',t') -> + (alpha_equivalence || n = n') && aux s s' && aux t t' + | C.Appl l, C.Appl l' -> + (try + List.fold_left2 + (fun b t1 t2 -> b && aux t1 t2) true l l' + with + Invalid_argument _ -> false) + | C.Const (uri,_), C.Const (uri',_) -> UriManager.eq uri uri' + | 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' && + aux outt outt' && aux t t' && (try List.fold_left2 - (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl' + (fun b t1 t2 -> b && aux t1 t2) true pl pl' with Invalid_argument _ -> false) - | C.Fix (i,fl), C.Fix (i',fl') -> - i = i' && - (try - 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' - with - Invalid_argument _ -> false) - | C.CoFix (i,fl), C.CoFix (i',fl') -> - i = i' && - (try - 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' - with - Invalid_argument _ -> false) - | _,_ -> false + | C.Fix (i,fl), C.Fix (i',fl') -> + i = i' && + (try + List.fold_left2 + (fun b (name,i,ty,bo) (name',i',ty',bo') -> + b && (alpha_equivalence || name = name') && i = i' && + aux ty ty' && aux bo bo') true fl fl' + with + Invalid_argument _ -> false) + | C.CoFix (i,fl), C.CoFix (i',fl') -> + i = i' && + (try + List.fold_left2 + (fun b (name,ty,bo) (name',ty',bo') -> + b && (alpha_equivalence || name = name') && + aux ty ty' && aux bo bo') true fl fl' + with + Invalid_argument _ -> false) + | _,_ -> false + in + aux ;; (* "textual" replacement of a subterm with another one *) @@ -162,33 +155,36 @@ let replace ~equality ~what ~with_what ~where = (* replaces in a term a term with another one. *) (* Lifting are performed as usual. *) let replace_lifting ~equality ~what ~with_what ~where = - let rec substaux k = + let rec substaux k what = let module C = Cic in + let module S = CicSubstitution in function -(*CSC: Possibile bug: debbo liftare di k what? *) - t when (equality t what) -> CicSubstitution.lift (k-1) with_what - | C.Rel n as t -> t (*CSC: ??? BUG ? *) + t when (equality t what) -> S.lift (k-1) with_what + | C.Rel n as t -> t | C.Var _ as t -> t | C.Meta (i, l) as t -> let l' = List.map (function None -> None - | Some t -> Some (substaux k t) + | Some t -> Some (substaux k what t) ) l in C.Meta(i,l') | C.Sort _ as t -> t | C.Implicit as t -> t - | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty) - | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t) - | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t) - | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t) + | C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty) + | C.Prod (n,s,t) -> + C.Prod (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t) + | C.Lambda (n,s,t) -> + C.Lambda (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t) + | C.LetIn (n,s,t) -> + C.LetIn (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t) | C.Appl (he::tl) -> (* Invariant: no Appl applied to another Appl *) - let tl' = List.map (substaux k) tl in + let tl' = List.map (substaux k what) tl in begin - match substaux k he with + match substaux k what he with C.Appl l -> C.Appl (l@tl') | _ as he' -> C.Appl (he'::tl') end @@ -197,13 +193,14 @@ let replace_lifting ~equality ~what ~with_what ~where = | C.MutInd _ as t -> t | C.MutConstruct _ as t -> t | C.MutCase (sp,cookingsno,i,outt,t,pl) -> - C.MutCase (sp,cookingsno,i,substaux k outt, substaux k t, - List.map (substaux k) pl) + C.MutCase (sp,cookingsno,i,substaux k what outt, substaux k what t, + List.map (substaux k what) pl) | C.Fix (i,fl) -> let len = List.length fl in let substitutedfl = List.map - (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo)) + (fun (name,i,ty,bo) -> + (name, i, substaux k what ty, substaux (k+len) (S.lift len what) bo)) fl in C.Fix (i, substitutedfl) @@ -211,12 +208,13 @@ let replace_lifting ~equality ~what ~with_what ~where = let len = List.length fl in let substitutedfl = List.map - (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo)) + (fun (name,ty,bo) -> + (name, substaux k what ty, substaux (k+len) (S.lift len what) bo)) fl in C.CoFix (i, substitutedfl) in - substaux 1 where + substaux 1 what where ;; (* Takes a well-typed term and fully reduces it. *) diff --git a/helm/gTopLevel/proofEngineReduction.mli b/helm/gTopLevel/proofEngineReduction.mli index e2d96f40b..aa0a3a648 100644 --- a/helm/gTopLevel/proofEngineReduction.mli +++ b/helm/gTopLevel/proofEngineReduction.mli @@ -34,12 +34,12 @@ exception RelToHiddenHypothesis exception WrongShape exception AlreadySimplified -val syntactic_equality : Cic.term -> Cic.term -> bool +val syntactic_equality : alpha_equivalence:bool -> Cic.term -> Cic.term -> bool val replace : equality:(Cic.term -> 'a -> bool) -> what:'a -> with_what:Cic.term -> where:Cic.term -> Cic.term val replace_lifting : - equality:(Cic.term -> 'a -> bool) -> - what:'a -> with_what:Cic.term -> where:Cic.term -> Cic.term + equality:(Cic.term -> Cic.term -> bool) -> + what:Cic.term -> with_what:Cic.term -> where:Cic.term -> Cic.term val reduce : Cic.context -> Cic.term -> Cic.term val simpl : Cic.context -> Cic.term -> Cic.term -- 2.39.2