X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngineReduction.ml;h=21f2cbebf72aa68f375e204345dbed3a52b717c0;hb=6ab193f88745acd3def85e47d643a92efb2f9fc5;hp=52f07e4dc2411d8b8aa63a75fcb290c3ebefe044;hpb=9f6cd4bd4cf91930f8a49bc7a274ac5b08459956;p=helm.git diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml index 52f07e4dc..21f2cbebf 100644 --- a/helm/gTopLevel/proofEngineReduction.ml +++ b/helm/gTopLevel/proofEngineReduction.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2000, HELM Team. +(* Copyright (C) 2002, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -37,21 +37,94 @@ (* 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 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 +;; (* "textual" replacement of a subterm with another one *) -let replace ~what ~with_what ~where = +let replace ~equality ~what ~with_what ~where = let module C = Cic in let rec aux = function - t when t = what -> with_what + 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 @@ -59,14 +132,21 @@ let replace ~what ~with_what ~where = | 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.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 @@ -85,172 +165,292 @@ let replace ~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 = - let rec reduceaux l = +let reduce context = + let rec reduceaux context 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.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,_) -> if l = [] then t else C.Appl (t::l) - | C.Variable (_,Some body,_) -> reduceaux 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 *) | C.Implicit as t -> t - | C.Cast (te,ty) -> reduceaux l te (*CSC E' GIUSTO BUTTARE IL CAST? *) + | 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 [] s, reduceaux [] t) + 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 [] s, reduceaux [] t) - | he::tl -> reduceaux tl (S.subst he t) + [] -> + 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 l (S.subst (reduceaux [] s) t) + | C.LetIn (n,s,t) -> + reduceaux context l (S.subst (reduceaux context [] s) t) | C.Appl (he::tl) -> - let tl' = List.map (reduceaux []) tl in - reduceaux (tl'@l) he + 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 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) -> + | 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 (_,_,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' + 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 (_,_,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' + 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 [] term) with - C.MutConstruct (_,_,_,j) -> reduceaux l (List.nth pl (j-1)) - | C.Appl (C.MutConstruct (_,_,_,j) :: tl) -> - let (arity, r, num_ingredients) = + (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 - 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 (ts@l) (List.nth pl (j-1)) - | C.Abst _ | C.Cast _ | C.Implicit -> + 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 [] outtype in - let term' = reduceaux [] term in - let pl' = List.map (reduceaux []) pl in + 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') + C.MutCase (mutind,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') + 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 - Some (List.nth l recindex) - with - _ -> None + let t' () = + let fl' = + List.map + (function (n,recindex,ty,bo) -> + (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo) + ) fl 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 + C.Fix (i, fl') in - C.CoFix (i, fl') + 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 - if l = [] then t' else C.Appl (t'::l) + 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 -function t -> let res = -prerr_endline ("<<<<<<<<<<<<<<<<" ^ CicPp.ppterm t) ; flush stderr ; - reduceaux [] -t in prerr_endline ("++++++++++++++++++" ^ CicPp.ppterm res) ; flush stderr ; res + reduceaux context [] ;; 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 *) @@ -273,230 +473,270 @@ exception WhatShouldIDo;; (* 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 = +let simpl context = (* reduceaux is equal to the reduceaux locally defined inside *) (*reduce, but for the const case. *) (**** Step 1 ****) - let rec reduceaux l = + let rec reduceaux context 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.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) -> reduceaux l te (*CSC E' GIUSTO BUTTARE IL CAST? *) + | 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 [] s, reduceaux [] t) + 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 [] s, reduceaux [] t) - | he::tl -> reduceaux tl (S.subst he t) + [] -> + 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 l (S.subst (reduceaux [] s) t) + | C.LetIn (n,s,t) -> + reduceaux context l (S.subst (reduceaux context [] s) t) | C.Appl (he::tl) -> - let tl' = List.map (reduceaux []) tl in - reduceaux (tl'@l) he + 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 (_,_,_) -> 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 + | 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,_,_) -> + 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 - (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) + 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 (CicSubstitution.subst_vars exp_named_subst' body) 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) + (**** Step 3 ****) + let term_to_fold = + match constant_args with + [] -> C.Const (uri,exp_named_subst') + | _ -> C.Appl ((C.Const(uri,exp_named_subst'))::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 + (CicSubstitution.subst_vars exp_named_subst' body) + | AlreadySimplified -> + (* If we performed delta-reduction, we would find a Fix *) + (* not applied to a constructor. So, we refuse to perform *) + (* delta-reduction. *) + let t' = C.Const (uri,exp_named_subst') in + if l = [] then t' else C.Appl (t'::l) + end + | 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 l body + | C.CurrentProof (_,_,body,_,_) -> reduceaux context 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) -> + | 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 (_,_,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' + 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 (_,_,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' + 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 [] term) with - C.MutConstruct (_,_,_,j) -> reduceaux l (List.nth pl (j-1)) - | C.Appl (C.MutConstruct (_,_,_,j) :: tl) -> - let (arity, r, num_ingredients) = + (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 - 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 (ts@l) (List.nth pl (j-1)) - | C.Abst _ | C.Cast _ | C.Implicit -> + 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 [] outtype in - let term' = reduceaux [] term in - let pl' = List.map (reduceaux []) pl in + 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') + C.MutCase (mutind,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') + 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 - Some (List.nth l recindex) - with - _ -> None + let t' () = + let fl' = + List.map + (function (n,recindex,ty,bo) -> + (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo) + ) fl 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 + 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) + 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 [] + reduceaux context [] ;;