Procedural: some comments added in the generated script

[helm.git] / helm / software / components / acic_procedural / proceduralHelpers.ml

diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml
index 54e8ebe050fb5a59cad06150b1c4238daa9da784..d6f844d71af04d448973934ef3c07820fa169383 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralHelpers.ml
+++ b/helm/software/components/acic_procedural/proceduralHelpers.ml
@@ -133,11 +133,11 @@ let get_ind_type uri tyno =
 let get_default_eliminator context uri tyno ty =
    let _, (name, _, _, _) = get_ind_type uri tyno in
    let ext = match get_tail context (get_type context ty) with
-      | C.Sort C.Prop     -> "_ind"
-      | C.Sort C.Set      -> "_rec"
-      | C.Sort (C.CProp _)   -> "_rect"
-      | C.Sort (C.Type _) -> "_rect"
-      | t                 -> 
+      | C.Sort C.Prop      -> "_ind"
+      | C.Sort C.Set       -> "_rec"
+      | C.Sort (C.CProp _) -> "_rect"
+      | C.Sort (C.Type _)  -> "_rect"
+      | t                  -> 
          Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t);
          assert false
    in
@@ -171,6 +171,20 @@ let occurs c ~what ~where =
    let _ = PER.replace_lifting ~equality ~context ~what ~with_what ~where in
    !result
 
+let name_of_uri uri tyno cno =
+   let get_ind_type tys tyno =
+      let s, _, _, cs = List.nth tys tyno in s, cs
+   in
+   match (fst (E.get_obj Un.oblivion_ugraph uri)), tyno, cno with
+      | C.Variable (s, _, _, _, _), _, _                     -> s
+      | C.Constant (s, _, _, _, _), _, _                     -> s
+      | C.InductiveDefinition (tys, _, _, _), Some i, None   ->
+         let s, _ = get_ind_type tys i in s
+      | C.InductiveDefinition (tys, _, _, _), Some i, Some j ->
+         let _, cs = get_ind_type tys i in
+        let s, _ = List.nth cs (pred j) in s
+      | _                                                    -> assert false
+
 (* Ensuring Barendregt convenction ******************************************)
 
 let rec add_entries map c = function