X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineReduction.ml;fp=helm%2Focaml%2Ftactics%2FproofEngineReduction.ml;h=0000000000000000000000000000000000000000;hp=99eb43f6a56e65e8419b090e43a0d2016dd6651b;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1 diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml deleted file mode 100644 index 99eb43f6a..000000000 --- a/helm/ocaml/tactics/proofEngineReduction.ml +++ /dev/null @@ -1,867 +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 ReferenceToConstant;; -exception ReferenceToVariable;; -exception ReferenceToCurrentProof;; -exception ReferenceToInductiveDefinition;; -exception WrongUriToInductiveDefinition;; -exception WrongUriToConstant;; -exception RelToHiddenHypothesis;; - -let alpha_equivalence = - let module C = Cic in - let rec aux t t' = - if t = t' then true - else - match t,t' with - C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2) -> - UriManager.eq uri1 uri2 && - aux_exp_named_subst exp_named_subst1 exp_named_subst2 - | C.Cast (te,ty), C.Cast (te',ty') -> - aux te te' && aux ty ty' - | C.Prod (_,s,t), C.Prod (_,s',t') -> - aux s s' && aux t t' - | C.Lambda (_,s,t), C.Lambda (_,s',t') -> - aux s s' && aux t t' - | C.LetIn (_,s,t), C.LetIn(_,s',t') -> - 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,exp_named_subst1), C.Const (uri',exp_named_subst2) -> - UriManager.eq uri uri' && - aux_exp_named_subst exp_named_subst1 exp_named_subst2 - | C.MutInd (uri,i,exp_named_subst1), C.MutInd (uri',i',exp_named_subst2) -> - UriManager.eq uri uri' && i = i' && - aux_exp_named_subst exp_named_subst1 exp_named_subst2 - | C.MutConstruct (uri,i,j,exp_named_subst1), - C.MutConstruct (uri',i',j',exp_named_subst2) -> - UriManager.eq uri uri' && i = i' && j = j' && - aux_exp_named_subst exp_named_subst1 exp_named_subst2 - | 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 (_,i,ty,bo) (_,i',ty',bo') -> - b && 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 (_,ty,bo) (_,ty',bo') -> - b && aux ty ty' && aux bo bo' - ) true fl fl' - with - Invalid_argument _ -> false) - | _,_ -> false (* we already know that t != t' *) - and aux_exp_named_subst exp_named_subst1 exp_named_subst2 = - try - List.fold_left2 - (fun b (uri1,t1) (uri2,t2) -> - b && UriManager.eq uri1 uri2 && aux t1 t2 - ) true exp_named_subst1 exp_named_subst2 - with - Invalid_argument _ -> false - in - aux -;; - -exception WhatAndWithWhatDoNotHaveTheSameLength;; - -(* "textual" replacement of several subterms with other ones *) -let replace ~equality ~what ~with_what ~where = - let module C = Cic in - let find_image t = - let rec find_image_aux = - function - [],[] -> raise Not_found - | what::tl1,with_what::tl2 -> - if equality t what then with_what else find_image_aux (tl1,tl2) - | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength - in - find_image_aux (what,with_what) - in - let rec aux t = - try - find_image t - with Not_found -> - match t with - C.Rel _ -> t - | C.Var (uri,exp_named_subst) -> - C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst) - | C.Meta _ -> t - | C.Sort _ -> 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 (uri,exp_named_subst) -> - C.Const (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst) - | C.MutInd (uri,i,exp_named_subst) -> - C.MutInd - (uri,i,List.map (function (uri,t) -> uri, aux t) exp_named_subst) - | C.MutConstruct (uri,i,j,exp_named_subst) -> - C.MutConstruct - (uri,i,j,List.map (function (uri,t) -> uri, aux t) exp_named_subst) - | C.MutCase (sp,i,outt,t,pl) -> - C.MutCase (sp,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 module C = Cic in - let module S = CicSubstitution in - let find_image what t = - let rec find_image_aux = - function - [],[] -> raise Not_found - | what::tl1,with_what::tl2 -> - if equality t what then with_what else find_image_aux (tl1,tl2) - | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength - in - find_image_aux (what,with_what) - in - let rec substaux k what t = - try - S.lift (k-1) (find_image what t) - with Not_found -> - match t with - C.Rel n as t -> t - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst - in - C.Var (uri,exp_named_subst') - | 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) (List.map (S.lift 1) what) t) - | C.Lambda (n,s,t) -> - C.Lambda - (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t) - | C.LetIn (n,s,t) -> - C.LetIn - (n, substaux k what s, substaux (k + 1) (List.map (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 (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst - in - C.Const (uri,exp_named_subst') - | C.MutInd (uri,i,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst - in - C.MutInd (uri,i,exp_named_subst') - | C.MutConstruct (uri,i,j,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst - in - C.MutConstruct (uri,i,j,exp_named_subst') - | C.MutCase (sp,i,outt,t,pl) -> - C.MutCase (sp,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) (List.map (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) (List.map (S.lift len) what) bo) - ) fl - in - C.CoFix (i, substitutedfl) - in - substaux 1 what where -;; - -(* replaces in a term a list of terms with other ones. *) -(* Lifting are performed as usual. *) -let replace_lifting_csc nnn ~equality ~what ~with_what ~where = - let module C = Cic in - let module S = CicSubstitution in - let find_image t = - let rec find_image_aux = - function - [],[] -> raise Not_found - | what::tl1,with_what::tl2 -> - if equality t what then with_what else find_image_aux (tl1,tl2) - | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength - in - find_image_aux (what,with_what) - in - let rec substaux k t = - try - S.lift (k-1) (find_image t) - with Not_found -> - match t with - C.Rel n as t -> - if n < k then C.Rel n else C.Rel (n + nnn) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k t) exp_named_subst - in - C.Var (uri,exp_named_subst') - | C.Meta (i, l) as t -> - let l' = - List.map - (function - None -> None - | Some t -> Some (substaux k 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.Appl (he::tl) -> - (* Invariant: no Appl applied to another Appl *) - let tl' = List.map (substaux k) tl in - begin - match substaux k he with - C.Appl l -> C.Appl (l@tl') - | _ as he' -> C.Appl (he'::tl') - end - | C.Appl _ -> assert false - | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k t) exp_named_subst - in - C.Const (uri,exp_named_subst') - | C.MutInd (uri,i,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k t) exp_named_subst - in - C.MutInd (uri,i,exp_named_subst') - | C.MutConstruct (uri,i,j,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k t) exp_named_subst - in - C.MutConstruct (uri,i,j,exp_named_subst') - | C.MutCase (sp,i,outt,t,pl) -> - C.MutCase (sp,i,substaux k outt, substaux k t, - List.map (substaux k) 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)) - 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 ty, substaux (k+len) bo)) - fl - in - C.CoFix (i, substitutedfl) - in - substaux 1 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,exp_named_subst) -> - let exp_named_subst' = - reduceaux_exp_named_subst context l exp_named_subst - in - (match CicEnvironment.get_obj uri with - C.Constant _ -> raise ReferenceToConstant - | C.CurrentProof _ -> raise ReferenceToCurrentProof - | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - | C.Variable (_,None,_,_) -> - let t' = C.Var (uri,exp_named_subst') in - if l = [] then t' else C.Appl (t'::l) - | C.Variable (_,Some body,_,_) -> - (reduceaux context l - (CicSubstitution.subst_vars exp_named_subst' 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,exp_named_subst) -> - let exp_named_subst' = - reduceaux_exp_named_subst context l exp_named_subst - in - (match CicEnvironment.get_obj uri with - C.Constant (_,Some body,_,_) -> - (reduceaux context l - (CicSubstitution.subst_vars exp_named_subst' body)) - | C.Constant (_,None,_,_) -> - let t' = C.Const (uri,exp_named_subst') in - if l = [] then t' else C.Appl (t'::l) - | C.Variable _ -> raise ReferenceToVariable - | C.CurrentProof (_,_,body,_,_) -> - (reduceaux context l - (CicSubstitution.subst_vars exp_named_subst' body)) - | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - ) - | C.MutInd (uri,i,exp_named_subst) -> - let exp_named_subst' = - reduceaux_exp_named_subst context l exp_named_subst - in - let t' = C.MutInd (uri,i,exp_named_subst') in - if l = [] then t' else C.Appl (t'::l) - | C.MutConstruct (uri,i,j,exp_named_subst) as t -> - let exp_named_subst' = - reduceaux_exp_named_subst context l exp_named_subst - in - let t' = C.MutConstruct (uri,i,j,exp_named_subst') in - if l = [] then t' else C.Appl (t'::l) - | C.MutCase (mutind,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 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 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) = - match CicEnvironment.get_obj mutind with - C.InductiveDefinition (tl,_,r) -> - let (_,_,arity,_) = List.nth tl i in - (arity,r) - | _ -> raise WrongUriToInductiveDefinition - in - let ts = - 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 (r,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,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) - and reduceaux_exp_named_subst context l = - List.map (function uri,t -> uri,reduceaux context [] t) - in - reduceaux context [] -;; - -exception WrongShape;; -exception AlreadySimplified;; - -(* 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,_)) -> - try_delta_expansion l t (S.lift n bo) - | None -> raise RelToHiddenHypothesis - ) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - reduceaux_exp_named_subst context l exp_named_subst - in - (match CicEnvironment.get_obj uri with - C.Constant _ -> raise ReferenceToConstant - | C.CurrentProof _ -> raise ReferenceToCurrentProof - | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - | C.Variable (_,None,_,_) -> - let t' = C.Var (uri,exp_named_subst') in - if l = [] then t' else C.Appl (t'::l) - | C.Variable (_,Some body,_,_) -> - reduceaux context l - (CicSubstitution.subst_vars exp_named_subst' 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,exp_named_subst) -> - let exp_named_subst' = - reduceaux_exp_named_subst context l exp_named_subst - in - (match CicEnvironment.get_obj uri with - C.Constant (_,Some body,_,_) -> - try_delta_expansion l - (C.Const (uri,exp_named_subst')) - (CicSubstitution.subst_vars exp_named_subst' body) - | C.Constant (_,None,_,_) -> - let t' = C.Const (uri,exp_named_subst') in - 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,i,exp_named_subst) -> - let exp_named_subst' = - reduceaux_exp_named_subst context l exp_named_subst - in - let t' = C.MutInd (uri,i,exp_named_subst') in - if l = [] then t' else C.Appl (t'::l) - | C.MutConstruct (uri,i,j,exp_named_subst) -> - let exp_named_subst' = - reduceaux_exp_named_subst context l exp_named_subst - in - let t' = C.MutConstruct(uri,i,j,exp_named_subst') in - if l = [] then t' else C.Appl (t'::l) - | C.MutCase (mutind,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 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 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) = - match CicEnvironment.get_obj mutind with - C.InductiveDefinition (tl,ingredients,r) -> - let (_,_,arity,_) = List.nth tl i in - (arity,r) - | _ -> raise WrongUriToInductiveDefinition - in - let ts = - 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 (r,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,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) - and reduceaux_exp_named_subst context l = - List.map (function uri,t -> uri,reduceaux context [] t) - (**** Step 2 ****) - and try_delta_expansion l term body = - let module C = Cic in - let module S = CicSubstitution in - try - 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 context l body', - List.rev rev_constant_args - | _ -> raise AlreadySimplified - ) - | _ -> raise WrongShape - in - aux [] l body - in - (**** Step 3 ****) - let term_to_fold, delta_expanded_term_to_fold = - match constant_args with - [] -> term,body - | _ -> C.Appl (term::constant_args), C.Appl (body::constant_args) - in - let simplified_term_to_fold = - reduceaux context [] delta_expanded_term_to_fold - in - replace (=) [simplified_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 term else C.Appl (term::l) - in - reduceaux context [] -;;