From b81fd5db31ec6286c74a2b49871d336836f300c4 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 18 Jul 2006 14:30:57 +0000
Subject: [PATCH] head_beta_reduce can now optionally perform delta reduction
 too

---
 components/cic_proof_checking/cicReduction.ml | 31 +++++++++++++++++--
 .../cic_proof_checking/cicReduction.mli       |  5 +--
 2 files changed, 31 insertions(+), 5 deletions(-)

diff --git a/components/cic_proof_checking/cicReduction.ml b/components/cic_proof_checking/cicReduction.ml
index ce8f66deb..b636c2a72 100644
--- a/components/cic_proof_checking/cicReduction.ml
+++ b/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/components/cic_proof_checking/cicReduction.mli b/components/cic_proof_checking/cicReduction.mli
index e3619053d..bee4607d5 100644
--- a/components/cic_proof_checking/cicReduction.mli
+++ b/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