X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngineReduction.ml;fp=helm%2FgTopLevel%2FproofEngineReduction.ml;h=0000000000000000000000000000000000000000;hp=bb724fc758d2736c40a7c199b60898501fe4308a;hb=869549224eef6278a48c16ae27dd786376082b38;hpb=89262281b6e83bd2321150f81f1a0583645eb0c8 diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml deleted file mode 100644 index bb724fc75..000000000 --- a/helm/gTopLevel/proofEngineReduction.ml +++ /dev/null @@ -1,678 +0,0 @@ -(* Copyright (C) 2002, 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;; -exception RelToHiddenHypothesis;; - -(* syntactic_equality up to cookingsno for uris *) -(* (which is often syntactically irrilevant) *) -let syntactic_equality ~alpha_equivalence = - let module C = Cic in - 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 && 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 && (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 *) -let replace ~equality ~what ~with_what ~where = - let module C = Cic in - let rec aux = - function - t when (equality 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 -> - (* Invariant enforced: no application of an application *) - (match List.map aux l with - (C.Appl l')::tl -> C.Appl (l'@tl) - | l' -> C.Appl l') - | C.Const _ 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 -;; - -(* 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 what = - let module C = Cic in - let module S = CicSubstitution in - function - 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 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 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 what) tl in - begin - match substaux k what he with - C.Appl l -> C.Appl (l@tl') - | _ as he' -> C.Appl (he'::tl') - end - | C.Appl _ -> assert false - | C.Const _ 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,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 what ty, substaux (k+len) (S.lift len what) 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, substaux k what ty, substaux (k+len) (S.lift len what) bo)) - fl - in - C.CoFix (i, substitutedfl) - in - substaux 1 what where -;; - -(* Takes a well-typed term and fully reduces it. *) -(*CSC: It does not perform reduction in a Case *) -let reduce context = - let rec reduceaux context l = - let module C = Cic in - let module S = CicSubstitution in - function - C.Rel n as t -> - (match List.nth context (n-1) with - Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l) - | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo) - | None -> raise RelToHiddenHypothesis - ) - | 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 context 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) -> - C.Cast (reduceaux context l te, reduceaux context l ty) - | C.Prod (name,s,t) -> - assert (l = []) ; - C.Prod (name, - reduceaux context [] s, - reduceaux ((Some (name,C.Decl s))::context) [] t) - | C.Lambda (name,s,t) -> - (match l with - [] -> - C.Lambda (name, - reduceaux context [] s, - reduceaux ((Some (name,C.Decl s))::context) [] t) - | he::tl -> reduceaux context tl (S.subst he t) - (* when name is Anonimous the substitution should be superfluous *) - ) - | C.LetIn (n,s,t) -> - reduceaux context l (S.subst (reduceaux context [] s) t) - | C.Appl (he::tl) -> - let tl' = List.map (reduceaux context []) tl in - reduceaux context (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 context l body - | C.Axiom _ -> if l = [] then t else C.Appl (t::l) - | C.Variable _ -> raise ReferenceToVariable - | C.CurrentProof (_,_,body,_) -> reduceaux context l body - | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - ) - | 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 tys = - List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl - in - 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 (tys@context) [] body' - | C.Appl (C.CoFix (i,fl) :: tl) -> - let tys = - List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl - in - 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 context []) tl in - reduceaux (tys@context) tl' body' - | t -> t - in - (match decofix (reduceaux context [] term) with - C.MutConstruct (_,_,_,j) -> reduceaux context 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 context (ts@l) (List.nth pl (j-1)) - | C.Cast _ | C.Implicit -> - raise (Impossible 2) (* we don't trust our whd ;-) *) - | _ -> - let outtype' = reduceaux context [] outtype in - let term' = reduceaux context [] term in - let pl' = List.map (reduceaux context []) 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 tys = - List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl - in - let t' () = - let fl' = - List.map - (function (n,recindex,ty,bo) -> - (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] 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 context [] 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 context 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 tys = - List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl - in - let t' = - let fl' = - List.map - (function (n,ty,bo) -> - (n,reduceaux context [] ty, reduceaux (tys@context) [] bo) - ) fl - in - C.CoFix (i, fl') - in - if l = [] then t' else C.Appl (t'::l) - in - reduceaux context [] -;; - -exception WrongShape;; -exception AlreadySimplified;; - -(*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 context = - (* reduceaux is equal to the reduceaux locally defined inside *) - (*reduce, but for the const case. *) - (**** Step 1 ****) - let rec reduceaux context l = - let module C = Cic in - let module S = CicSubstitution in - function - C.Rel n as t -> - (match List.nth context (n-1) with - Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l) - | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo) - | None -> raise RelToHiddenHypothesis - ) - | 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 context 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) -> - C.Cast (reduceaux context l te, reduceaux context l ty) - | C.Prod (name,s,t) -> - assert (l = []) ; - C.Prod (name, - reduceaux context [] s, - reduceaux ((Some (name,C.Decl s))::context) [] t) - | C.Lambda (name,s,t) -> - (match l with - [] -> - C.Lambda (name, - reduceaux context [] s, - reduceaux ((Some (name,C.Decl s))::context) [] t) - | he::tl -> reduceaux context tl (S.subst he t) - (* when name is Anonimous the substitution should be superfluous *) - ) - | C.LetIn (n,s,t) -> - reduceaux context l (S.subst (reduceaux context [] s) t) - | C.Appl (he::tl) -> - let tl' = List.map (reduceaux context []) tl in - reduceaux context (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 (_,s,t) -> - aux rev_constant_args l (S.subst s t) - | C.Fix (i,fl) as t -> - let tys = - List.map (function (name,_,ty,_) -> - Some (C.Name name, C.Decl ty)) fl - in - let (_,recindex,_,body) = List.nth fl i in - let recparam = - try - List.nth l recindex - with - _ -> raise AlreadySimplified - in - (match CicReduction.whd context 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 (tys@context) 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 context term_to_fold in - 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 context 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 context l body - | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - ) - | 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 tys = - List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in - 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 (tys@context) [] body' - | C.Appl (C.CoFix (i,fl) :: tl) -> - let tys = - List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in - 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 context []) tl in - reduceaux (tys@context) tl body' - | t -> t - in - (match decofix (reduceaux context [] term) with - C.MutConstruct (_,_,_,j) -> reduceaux context 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 context (ts@l) (List.nth pl (j-1)) - | C.Cast _ | C.Implicit -> - raise (Impossible 2) (* we don't trust our whd ;-) *) - | _ -> - let outtype' = reduceaux context [] outtype in - let term' = reduceaux context [] term in - let pl' = List.map (reduceaux context []) 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 tys = - List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl - in - let t' () = - let fl' = - List.map - (function (n,recindex,ty,bo) -> - (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] 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 context [] 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 context 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 tys = - List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl - in - let t' = - let fl' = - List.map - (function (n,ty,bo) -> - (n,reduceaux context [] ty, reduceaux (tys@context) [] bo) - ) fl - in - C.CoFix (i, fl') - in - if l = [] then t' else C.Appl (t'::l) - in - reduceaux context [] -;;