From: Claudio Sacerdoti Coen Date: Tue, 16 Apr 2002 11:09:39 +0000 (+0000) Subject: proofEngineReduction.ml added X-Git-Tag: V_0_3_0_debian_8~153 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9f6cd4bd4cf91930f8a49bc7a274ac5b08459956;p=helm.git proofEngineReduction.ml added It holds functions to perform reduction and simplification of terms. They are used in the implementation of the reduction/conversion tactics. --- diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index 661d1055b..5540d5d1a 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -1,8 +1,10 @@ +proofEngine.cmo: proofEngineReduction.cmo +proofEngine.cmx: proofEngineReduction.cmx logicalOperations.cmo: proofEngine.cmo logicalOperations.cmx: proofEngine.cmx sequentPp.cmo: cic2Xml.cmo cic2acic.cmo proofEngine.cmo sequentPp.cmx: cic2Xml.cmx cic2acic.cmx proofEngine.cmx -gTopLevel.cmo: cic2Xml.cmo cic2acic.cmo logicalOperations.cmo sequentPp.cmo \ - xml2Gdome.cmo -gTopLevel.cmx: cic2Xml.cmx cic2acic.cmx logicalOperations.cmx sequentPp.cmx \ - xml2Gdome.cmx +gTopLevel.cmo: cic2Xml.cmo cic2acic.cmo logicalOperations.cmo proofEngine.cmo \ + sequentPp.cmo xml2Gdome.cmo +gTopLevel.cmx: cic2Xml.cmx cic2acic.cmx logicalOperations.cmx proofEngine.cmx \ + sequentPp.cmx xml2Gdome.cmx diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index c0d7aabd0..0b936260c 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -1,6 +1,6 @@ BIN_DIR = /usr/local/bin REQUIRES = lablgtkmathview helm-cic_textual_parser helm-cic_proof_checking \ - helm-xml gdome_xslt helm-cic_unification + helm-xml gdome2-xslt helm-cic_unification PREDICATES = OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) @@ -13,11 +13,12 @@ LIBRARIES_OPT = $(shell ocamlfind query -recursive -predicates "native $(PREDICA all: gTopLevel opt: gTopLevel.opt -DEPOBJS = xml2Gdome.ml proofEngine.ml cic2Xml.ml cic2acic.ml \ - logicalOperations.ml sequentPp.ml gTopLevel.ml +DEPOBJS = xml2Gdome.ml proofEngineReduction.ml proofEngine.ml cic2Xml.ml \ + cic2acic.ml logicalOperations.ml sequentPp.ml gTopLevel.ml -TOPLEVELOBJS = xml2Gdome.cmo proofEngine.cmo cic2Xml.cmo cic2acic.cmo \ - logicalOperations.cmo sequentPp.cmo gTopLevel.cmo +TOPLEVELOBJS = xml2Gdome.cmo proofEngineReduction.cmo proofEngine.cmo \ + cic2Xml.cmo cic2acic.cmo logicalOperations.cmo sequentPp.cmo \ + gTopLevel.cmo depend: $(OCAMLDEP) $(DEPOBJS) > .depend diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml new file mode 100644 index 000000000..52f07e4dc --- /dev/null +++ b/helm/gTopLevel/proofEngineReduction.ml @@ -0,0 +1,502 @@ +(* 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/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 12/04/2002 *) +(* *) +(* *) +(******************************************************************************) + + +(* The code of this module is derived from the code of CicReduction *) + +exception Impossible of int;; +exception ReferenceToDefinition;; +exception ReferenceToAxiom;; +exception ReferenceToVariable;; +exception ReferenceToCurrentProof;; +exception ReferenceToInductiveDefinition;; +exception WrongUriToInductiveDefinition;; + +(* "textual" replacement of a subterm with another one *) +let replace ~what ~with_what ~where = + let module C = Cic in + let rec aux = + function + t when t = what -> with_what + | C.Rel _ as t -> t + | 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 (aux te, aux ty) + | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t) + | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t) + | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t) + | C.Appl l -> C.Appl (List.map aux 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,aux outt, aux t, + List.map aux pl) + | C.Fix (i,fl) -> + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo)) + fl + in + C.Fix (i, substitutedfl) + | C.CoFix (i,fl) -> + let substitutedfl = + List.map + (fun (name,ty,bo) -> (name, aux ty, aux bo)) + fl + in + C.CoFix (i, substitutedfl) + in + aux where +;; + +(* Takes a well-typed term and fully reduces it. *) +(*CSC: It does not perform reduction in a Case *) +let reduce = + let rec reduceaux 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,_) -> reduceaux 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) -> reduceaux l te (*CSC E' GIUSTO BUTTARE IL CAST? *) + | C.Prod (name,s,t) -> + assert (l = []) ; + C.Prod (name, reduceaux [] s, reduceaux [] t) + | C.Lambda (name,s,t) -> + (match l with + [] -> C.Lambda (name, reduceaux [] s, reduceaux [] t) + | he::tl -> reduceaux tl (S.subst he t) + (* when name is Anonimous the substitution should be superfluous *) + ) + | C.LetIn (n,s,t) -> reduceaux l (S.subst (reduceaux [] s) t) + | C.Appl (he::tl) -> + let tl' = List.map (reduceaux []) tl in + reduceaux (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,_,_) -> reduceaux l body + | C.Axiom _ -> if l = [] then t else C.Appl (t::l) + | C.Variable _ -> raise ReferenceToVariable + | C.CurrentProof (_,_,body,_) -> reduceaux 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,outtype,term,pl) -> + 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 + reduceaux [] 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 + let tl' = List.map (reduceaux []) tl in + reduceaux tl body' + | t -> t + in + (match decofix (reduceaux [] term) with + C.MutConstruct (_,_,_,j) -> reduceaux 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 + reduceaux (ts@l) (List.nth pl (j-1)) + | C.Abst _ | C.Cast _ | C.Implicit -> + raise (Impossible 2) (* we don't trust our whd ;-) *) + | _ -> + let outtype' = reduceaux [] outtype in + let term' = reduceaux [] term in + let pl' = List.map (reduceaux []) pl in + let res = + C.MutCase (mutind,cookingsno,i,outtype',term',pl') + in + if l = [] then res else C.Appl (res::l) + ) + | C.Fix (i,fl) -> + let t' () = + let fl' = + List.map + (function (n,recindex,ty,bo) -> + (n,recindex,reduceaux [] ty, reduceaux [] bo) + ) fl + in + C.Fix (i, fl') + in + 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 reduceaux [] 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 *) + reduceaux 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) -> + let t' = + let fl' = + List.map + (function (n,ty,bo) -> + (n,reduceaux [] ty, reduceaux [] bo) + ) fl + in + C.CoFix (i, fl') + in + if l = [] then t' else C.Appl (t'::l) + in +function t -> let res = +prerr_endline ("<<<<<<<<<<<<<<<<" ^ CicPp.ppterm t) ; flush stderr ; + reduceaux [] +t in prerr_endline ("++++++++++++++++++" ^ CicPp.ppterm res) ; flush stderr ; res +;; + +exception WrongShape;; +exception AlreadySimplified;; +exception WhatShouldIDo;; + +(*CSC: I fear it is still weaker than Coq's one. For example, Coq is *) +(*CSCS: able to simpl (foo (S n) (S n)) to (foo (S O) n) where *) +(*CSC: Fix foo *) +(*CSC: {foo [n,m:nat]:nat := *) +(*CSC: Cases m of O => n | (S p) => (foo (S O) p) end *) +(*CSC: } *) +(* Takes a well-typed term and *) +(* 1) Performs beta-iota-zeta reduction until delta reduction is needed *) +(* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *) +(* w.r.t. zero or more variables and if the Fix can be reduced, than it *) +(* is reduced, the delta-reduction is succesfull and the whole algorithm *) +(* is applied again to the new redex; Step 3) is applied to the result *) +(* of the recursive simplification. Otherwise, if the Fix can not be *) +(* reduced, than the delta-reductions fails and the delta-redex is *) +(* not reduced. Otherwise, if the delta-residual is not the *) +(* lambda-abstraction of a Fix, then it is reduced and the result is *) +(* directly returned, without performing step 3). *) +(* 3) Folds the application of the constant to the arguments that did not *) +(* change in every iteration, i.e. to the actual arguments for the *) +(* lambda-abstractions that precede the Fix. *) +(*CSC: It does not perform simplification in a Case *) +let simpl = + (* reduceaux is equal to the reduceaux locally defined inside *) + (*reduce, but for the const case. *) + (**** Step 1 ****) + let rec reduceaux 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,_) -> reduceaux 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) -> reduceaux l te (*CSC E' GIUSTO BUTTARE IL CAST? *) + | C.Prod (name,s,t) -> + assert (l = []) ; + C.Prod (name, reduceaux [] s, reduceaux [] t) + | C.Lambda (name,s,t) -> + (match l with + [] -> C.Lambda (name, reduceaux [] s, reduceaux [] t) + | he::tl -> reduceaux tl (S.subst he t) + (* when name is Anonimous the substitution should be superfluous *) + ) + | C.LetIn (n,s,t) -> reduceaux l (S.subst (reduceaux [] s) t) + | C.Appl (he::tl) -> + let tl' = List.map (reduceaux []) tl in + reduceaux (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,_,_) -> + begin + try + (**** Step 2 ****) + let res,constant_args = + let rec aux rev_constant_args l = + function + C.Lambda (name,s,t) as t' -> + begin + match l with + [] -> raise WrongShape + | he::tl -> + (* when name is Anonimous the substitution should be *) + (* superfluous *) + aux (he::rev_constant_args) tl (S.subst he t) + end + | C.LetIn (_,_,_) -> raise WhatShouldIDo (*CSC: ?????????? *) + | C.Fix (i,fl) as t -> + let (_,recindex,_,body) = List.nth fl i in + let recparam = + try + List.nth l recindex + with + _ -> raise AlreadySimplified + in + (match CicReduction.whd recparam with + C.MutConstruct _ + | C.Appl ((C.MutConstruct _)::_) -> + let body' = + let counter = ref (List.length fl) in + List.fold_right + (function _ -> + decr counter ; S.subst (C.Fix (!counter,fl)) + ) fl body + in + (* Possible optimization: substituting whd *) + (* recparam in l *) + reduceaux l body', List.rev rev_constant_args + | _ -> raise AlreadySimplified + ) + | _ -> raise WrongShape + in + aux [] l body + in + (**** Step 3 ****) + let term_to_fold = + match constant_args with + [] -> C.Const (uri,cookingsno) + | _ -> C.Appl ((C.Const (uri,cookingsno))::constant_args) + in + let reduced_term_to_fold = reduce term_to_fold in +prerr_endline ("TERM TO FOLD: " ^ CicPp.ppterm term_to_fold) ; flush stderr ; +prerr_endline ("REDUCED TERM TO FOLD: " ^ CicPp.ppterm reduced_term_to_fold) ; flush stderr ; + replace reduced_term_to_fold term_to_fold res + with + WrongShape -> + (* The constant does not unfold to a Fix lambda-abstracted *) + (* w.r.t. zero or more variables. We just perform reduction. *) + reduceaux l body + | AlreadySimplified -> + (* If we performed delta-reduction, we would find a Fix *) + (* not applied to a constructor. So, we refuse to perform *) + (* delta-reduction. *) + if l = [] then + t + else + C.Appl (t::l) + end + | C.Axiom _ -> if l = [] then t else C.Appl (t::l) + | C.Variable _ -> raise ReferenceToVariable + | C.CurrentProof (_,_,body,_) -> reduceaux 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,outtype,term,pl) -> + 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 + reduceaux [] 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 + let tl' = List.map (reduceaux []) tl in + reduceaux tl body' + | t -> t + in + (match decofix (reduceaux [] term) with + C.MutConstruct (_,_,_,j) -> reduceaux 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 + reduceaux (ts@l) (List.nth pl (j-1)) + | C.Abst _ | C.Cast _ | C.Implicit -> + raise (Impossible 2) (* we don't trust our whd ;-) *) + | _ -> + let outtype' = reduceaux [] outtype in + let term' = reduceaux [] term in + let pl' = List.map (reduceaux []) pl in + let res = + C.MutCase (mutind,cookingsno,i,outtype',term',pl') + in + if l = [] then res else C.Appl (res::l) + ) + | C.Fix (i,fl) -> + let t' () = + let fl' = + List.map + (function (n,recindex,ty,bo) -> + (n,recindex,reduceaux [] ty, reduceaux [] bo) + ) fl + in + C.Fix (i, fl') + in + 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 reduceaux [] 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 *) + reduceaux 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) -> + let t' = + let fl' = + List.map + (function (n,ty,bo) -> + (n,reduceaux [] ty, reduceaux [] bo) + ) fl + in + C.CoFix (i, fl') + in + if l = [] then t' else C.Appl (t'::l) + in + reduceaux [] +;;