From bada8520939f45188270ba7ba5e006e55d3a0d15 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 18 Jul 2006 14:30:57 +0000 Subject: [PATCH] head_beta_reduce can now optionally perform delta reduction too --- .../cic_proof_checking/cicReduction.ml | 31 +++++++++++++++++-- .../cic_proof_checking/cicReduction.mli | 5 +-- 2 files changed, 31 insertions(+), 5 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml index ce8f66deb..b636c2a72 100644 --- a/helm/software/components/cic_proof_checking/cicReduction.ml +++ b/helm/software/components/cic_proof_checking/cicReduction.ml @@ -1116,7 +1116,7 @@ let normalize ?delta ?subst ctx term = (* performs an head beta/cast reduction *) -let rec head_beta_reduce = +let rec head_beta_reduce ?(delta=false) = function (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) -> let he'' = CicSubstitution.subst he' t in @@ -1128,8 +1128,33 @@ let rec head_beta_reduce = Cic.Appl l -> Cic.Appl (l@tl') | _ -> Cic.Appl (he''::tl') in - head_beta_reduce he''' - | Cic.Cast (te,_) -> head_beta_reduce te + head_beta_reduce ~delta he''' + | Cic.Cast (te,_) -> head_beta_reduce ~delta te + | Cic.Appl (Cic.Const (uri,ens)::tl) as t when delta=true -> + let bo = + match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with + Cic.Constant (_,bo,_,_,_) -> bo + | Cic.Variable _ -> raise ReferenceToVariable + | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo + | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + in + (match bo with + None -> t + | Some bo -> + head_beta_reduce + ~delta (Cic.Appl ((CicSubstitution.subst_vars ens bo)::tl))) + | Cic.Const (uri,ens) as t when delta=true -> + let bo = + match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with + Cic.Constant (_,bo,_,_,_) -> bo + | Cic.Variable _ -> raise ReferenceToVariable + | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo + | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + in + (match bo with + None -> t + | Some bo -> + head_beta_reduce ~delta (CicSubstitution.subst_vars ens bo)) | t -> t (* diff --git a/helm/software/components/cic_proof_checking/cicReduction.mli b/helm/software/components/cic_proof_checking/cicReduction.mli index e3619053d..bee4607d5 100644 --- a/helm/software/components/cic_proof_checking/cicReduction.mli +++ b/helm/software/components/cic_proof_checking/cicReduction.mli @@ -38,5 +38,6 @@ val are_convertible : val normalize: ?delta:bool -> ?subst:Cic.substitution -> Cic.context -> Cic.term -> Cic.term -(* performs an head beta/cast reduction *) -val head_beta_reduce: Cic.term -> Cic.term +(* performs an head beta/cast reduction; the default is to not perform + delta reduction *) +val head_beta_reduce: ?delta:bool -> Cic.term -> Cic.term -- 2.39.2