From: Claudio Sacerdoti Coen Date: Mon, 9 Dec 2002 10:50:18 +0000 (+0000) Subject: Simpl now handles let-in reductions as delta-reductions. Cool. X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fadf62404244f8f44b206f1e453f5453930948f2;p=helm.git Simpl now handles let-in reductions as delta-reductions. Cool. --- diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml index 9a1b0e3ca..1b36e686e 100644 --- a/helm/gTopLevel/proofEngineReduction.ml +++ b/helm/gTopLevel/proofEngineReduction.ml @@ -453,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 *) @@ -485,7 +479,8 @@ 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,exp_named_subst) -> @@ -533,82 +528,10 @@ let simpl context = 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 context l body', - List.rev rev_constant_args - | _ -> raise AlreadySimplified - ) - | _ -> raise WrongShape - in - aux [] l (CicSubstitution.subst_vars exp_named_subst' body) - in - (**** Step 3 ****) - let term_to_fold, delta_expanded_term_to_fold = - let body' = CicSubstitution.subst_vars exp_named_subst' body in - match constant_args with - [] -> C.Const (uri,exp_named_subst'), body' - | _ -> - C.Appl ((C.Const (uri,exp_named_subst'))::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 - (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 (_,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) @@ -743,6 +666,77 @@ let simpl context = 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 [] ;;