From fa70e8149a0c5405c4498cb3b7898d733a91910b Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 11 Jan 2005 16:02:53 +0000
Subject: [PATCH] snapshot, not yet completed, but ...

---
 helm/ocaml/cic_proof_checking/cicElim.ml  | 46 +++++++++++++++--------
 helm/ocaml/cic_proof_checking/cicElim.mli |  8 +++-
 2 files changed, 36 insertions(+), 18 deletions(-)

diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml
index 1de440d56..77304c1ec 100644
--- a/helm/ocaml/cic_proof_checking/cicElim.ml
+++ b/helm/ocaml/cic_proof_checking/cicElim.ml
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+open Printf
+
 let fresh_binder =
   let counter = ref ~-1 in
   function
@@ -81,9 +83,11 @@ let rec delta (uri, typeno, subst) dependent paramsno consno t p args =
       if recursive uri src then
         let args = List.map (CicSubstitution.lift 2) args in
         let phi =
-          (delta (uri, typeno, subst) dependent paramsno consno src
-            (CicSubstitution.lift 1 p) [Cic.Rel 1])
+          let src = CicSubstitution.lift 1 src in
+          delta (uri, typeno, subst) dependent paramsno consno src
+            (CicSubstitution.lift 1 p) [Cic.Rel 1]
         in
+        let tgt = CicSubstitution.lift 1 tgt in
         Cic.Prod (fresh_binder dependent, src,
           Cic.Prod (Cic.Anonymous, phi,
             delta (uri, typeno, subst) dependent paramsno consno tgt
@@ -132,24 +136,23 @@ let rec count_pi = function
   | Cic.Prod (_, _, tgt) -> count_pi tgt + 1
   | t -> 0
 
-let rec type_of_p dependent leftno indty = function
+let rec type_of_p sort dependent leftno indty = function
   | Cic.Prod (n, src, tgt) when leftno = 0 ->
-      Cic.Prod (n, src, type_of_p dependent leftno indty tgt)
-  | Cic.Prod (_, _, tgt) -> type_of_p dependent (leftno - 1) indty tgt
+      Cic.Prod (n, src, type_of_p sort dependent leftno indty tgt)
+  | Cic.Prod (_, _, tgt) -> type_of_p sort dependent (leftno - 1) indty tgt
   | t ->
       if dependent then
-        Cic.Prod (Cic.Anonymous, indty,
-          Cic.Sort (Cic.Type (CicUniv.fresh ())))
+        Cic.Prod (Cic.Anonymous, indty, Cic.Sort sort)
       else
-        Cic.Sort (Cic.Type (CicUniv.fresh ()))
+        Cic.Sort sort
 
-let rec add_right_pi dependent strip liftno rightno indty = function
+let rec add_right_pi dependent strip liftno liftfrom rightno indty = function
   | Cic.Prod (_, src, tgt) when strip = 0 ->
       Cic.Prod (fresh_binder true,
-        CicSubstitution.lift liftno src,
-        add_right_pi dependent strip liftno rightno indty tgt)
+        CicSubstitution.lift_from (liftfrom + 1) liftno src,
+        add_right_pi dependent strip liftno (liftfrom + 1) rightno indty tgt)
   | Cic.Prod (_, _, tgt) ->
-      add_right_pi dependent (strip - 1) liftno rightno indty tgt
+      add_right_pi dependent (strip - 1) liftno liftfrom rightno indty tgt
   | t ->
       if dependent then
         Cic.Prod (fresh_binder dependent,
@@ -163,7 +166,15 @@ let rec add_right_pi dependent strip liftno rightno indty = function
           else
             Cic.Appl (Cic.Rel (1 + liftno + rightno) :: mk_rels 1 rightno))
 
-let elim_of uri typeno =
+exception Failure of string
+
+let string_of_sort = function
+  | Cic.Prop -> "Prop"
+  | Cic.CProp -> "CProp"
+  | Cic.Set -> "Set"
+  | Cic.Type _ -> "Type"
+
+let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
   let (obj, univ) = (CicEnvironment.get_obj uri CicUniv.empty_ugraph) in
   let subst = [] in
   match obj with
@@ -177,9 +188,12 @@ let elim_of uri typeno =
       let dependent = (strip_pi ty <> Cic.Sort Cic.Prop) in
       let conslen = List.length constructors in
       let consno = ref (conslen + 1) in
+      if (not dependent) && (sort <> Cic.Prop) && (conslen > 1) then
+        raise (Failure (sprintf "can't eliminate from Prop to %s"
+          (string_of_sort sort)));
       let indty =
         let indty = Cic.MutInd (uri, typeno, subst) in
-        if leftno = 0 then
+        if paramsno = 0 then
           indty
         else
           Cic.Appl (indty :: mk_rels 0 paramsno)
@@ -192,9 +206,9 @@ let elim_of uri typeno =
           Cic.Appl (constructor :: mk_rels consno leftno)
       in
       let eliminator =
-        let p_ty = type_of_p dependent leftno indty ty in
+        let p_ty = type_of_p sort dependent leftno indty ty in
         let final_ty =
-          add_right_pi dependent leftno (conslen + 1) (paramsno - leftno)
+          add_right_pi dependent leftno (conslen + 1) 1 (paramsno - leftno)
             indty ty
         in
         Cic.Prod (Cic.Name "P", p_ty,
diff --git a/helm/ocaml/cic_proof_checking/cicElim.mli b/helm/ocaml/cic_proof_checking/cicElim.mli
index 828028d0a..b341d36a4 100644
--- a/helm/ocaml/cic_proof_checking/cicElim.mli
+++ b/helm/ocaml/cic_proof_checking/cicElim.mli
@@ -23,8 +23,12 @@
  * http://helm.cs.unibo.it/
  *)
 
-(** @param uri inductive type uri
+exception Failure of string
+
+(** @param sort target sort, defaults to Type
+* @param uri inductive type uri
 * @param typeno inductive type number
+* @raise Failure
 *)
-val elim_of: UriManager.uri -> int -> Cic.term
+val elim_of: ?sort:Cic.sort -> UriManager.uri -> int -> Cic.term
 
-- 
2.39.2