X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngineReduction.ml;h=1b36e686e4337da522ce688450316af2ce94e4b4;hb=7ff85e55518d06d96b9abbea4aa68d83e6be35b0;hp=87cf24c2158be45bf601d879c4bfc2690315ec84;hpb=76cb30ecd0159512548aee0ba7085ab17c6fd5bd;p=helm.git diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml index 87cf24c21..1b36e686e 100644 --- a/helm/gTopLevel/proofEngineReduction.ml +++ b/helm/gTopLevel/proofEngineReduction.ml @@ -37,69 +37,84 @@ (* The code of this module is derived from the code of CicReduction *) exception Impossible of int;; -exception ReferenceToDefinition;; -exception ReferenceToAxiom;; +exception ReferenceToConstant;; exception ReferenceToVariable;; exception ReferenceToCurrentProof;; exception ReferenceToInductiveDefinition;; exception WrongUriToInductiveDefinition;; +exception WrongUriToConstant;; exception RelToHiddenHypothesis;; -(* syntactic_equality up to cookingsno for uris *) -(* (which is often syntactically irrilevant) *) -let rec syntactic_equality t t' = +let 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' -> - 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.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.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 && 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 + (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 ;; (* "textual" replacement of a subterm with another one *) @@ -109,7 +124,8 @@ let replace ~equality ~what ~with_what ~where = function t when (equality t what) -> with_what | C.Rel _ as t -> t - | C.Var _ as t -> t + | C.Var (uri,exp_named_subst) -> + C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst) | C.Meta _ as t -> t | C.Sort _ as t -> t | C.Implicit as t -> t @@ -122,12 +138,16 @@ let replace ~equality ~what ~with_what ~where = (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.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 @@ -146,6 +166,87 @@ let replace ~equality ~what ~with_what ~where = 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 (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) (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 (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) (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 = @@ -159,14 +260,20 @@ let reduce context = | 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.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,_) -> if l = [] then t else C.Appl (t::l) - | C.Variable (_,Some body,_) -> reduceaux context l body + | 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 *) @@ -193,17 +300,36 @@ let reduce context = 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) -> + | 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 -> @@ -218,7 +344,7 @@ let reduce context = fl body in - reduceaux (tys@context) [] body' + 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 @@ -232,34 +358,27 @@ let reduce context = body in let tl' = List.map (reduceaux context []) tl in - reduceaux (tys@context) tl' body' + 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, num_ingredients) = + 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 - 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) + C.InductiveDefinition (tl,_,r) -> + let (_,_,arity,_) = List.nth tl i in + (arity,r) | _ -> 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) + 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 -> @@ -269,7 +388,7 @@ let reduce context = let term' = reduceaux context [] term in let pl' = List.map (reduceaux context []) pl in let res = - C.MutCase (mutind,cookingsno,i,outtype',term',pl') + C.MutCase (mutind,i,outtype',term',pl') in if l = [] then res else C.Appl (res::l) ) @@ -325,6 +444,8 @@ let reduce context = 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 [] ;; @@ -332,12 +453,6 @@ let reduce 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 *) @@ -355,7 +470,7 @@ exception AlreadySimplified;; (*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. *) + (* reduce, but for the const case. *) (**** Step 1 ****) let rec reduceaux context l = let module C = Cic in @@ -364,18 +479,25 @@ let simpl context = 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) + | Some (_,C.Def bo) -> + try_delta_expansion l t (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.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 @@ -401,88 +523,35 @@ let simpl context = 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.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.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) -> + | 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 -> @@ -496,7 +565,7 @@ let simpl context = fl body in - reduceaux (tys@context) [] body' + 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 @@ -509,34 +578,27 @@ let simpl context = body in let tl' = List.map (reduceaux context []) tl in - reduceaux (tys@context) tl body' + 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, num_ingredients) = + 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 - 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) + let (_,_,arity,_) = List.nth tl i in + (arity,r) | _ -> 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) + 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 -> @@ -546,7 +608,7 @@ let simpl context = let term' = reduceaux context [] term in let pl' = List.map (reduceaux context []) pl in let res = - C.MutCase (mutind,cookingsno,i,outtype',term',pl') + C.MutCase (mutind,i,outtype',term',pl') in if l = [] then res else C.Appl (res::l) ) @@ -602,6 +664,79 @@ let simpl context = 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 [] ;;