X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngineReduction.ml;h=21f2cbebf72aa68f375e204345dbed3a52b717c0;hb=6ab193f88745acd3def85e47d643a92efb2f9fc5;hp=7d4a799601dad71082943a92b5685480996b60da;hpb=ee35bf33520d92753899985329cc4bfee141b808;p=helm.git diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml index 7d4a79960..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,14 +37,85 @@ (* 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 ~equality ~what ~with_what ~where = let module C = Cic in @@ -52,7 +123,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 @@ -65,13 +137,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.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.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 @@ -90,6 +165,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 = @@ -103,14 +259,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 *) @@ -137,18 +299,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.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 -> @@ -181,40 +361,33 @@ let reduce context = | 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.Abst _ | C.Cast _ | C.Implicit -> + | 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') + C.MutCase (mutind,i,outtype',term',pl') in if l = [] then res else C.Appl (res::l) ) @@ -270,13 +443,14 @@ 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 [] ;; 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 *) @@ -313,15 +487,21 @@ let simpl 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.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 @@ -347,88 +527,102 @@ 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 (_,_,_) -> raise WhatShouldIDo (*CSC: ?????????? *) - | 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) + | 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 + 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 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) + (**** 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 context 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 -> @@ -459,40 +653,33 @@ let simpl context = | 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.Abst _ | C.Cast _ | C.Implicit -> + | 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') + C.MutCase (mutind,i,outtype',term',pl') in if l = [] then res else C.Appl (res::l) ) @@ -548,6 +735,8 @@ 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) in reduceaux context [] ;;