X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngineReduction.ml;h=710a48164585c97aefe718f90d53a409cdd5c690;hb=370f967a478c116fcc85a81c7953363b4351a2e9;hp=208864c801f1a2fdeafa99506ade65b46f901f51;hpb=086c66b6682a49fec4041c25e741b2736f385e6a;p=helm.git diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml index 208864c80..710a48164 100644 --- a/helm/gTopLevel/proofEngineReduction.ml +++ b/helm/gTopLevel/proofEngineReduction.ml @@ -247,6 +247,90 @@ let replace_lifting ~equality ~what ~with_what ~where = substaux 1 what where ;; +(* replaces in a term a term with another one. *) +(* Lifting are performed as usual. *) +let replace_lifting_csc nnn ~equality ~what ~with_what ~where = + let rec substaux k = + 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 -> + 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 +let res = + substaux 1 where +in prerr_endline ("@@@@ risultato replace: " ^ (CicPp.ppterm res)); res +;; + (* Takes a well-typed term and fully reduces it. *) (*CSC: It does not perform reduction in a Case *) let reduce context = @@ -344,7 +428,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 @@ -358,7 +442,7 @@ 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 @@ -453,12 +537,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 +563,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 +612,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 (tys@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) @@ -642,7 +649,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 @@ -655,7 +662,7 @@ 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 @@ -743,6 +750,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 [] ;;