Procedural: explicit flavour specification for constants is now working

[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 4d86521074122e31e6907a28c25887355809dd99..d6f844d71af04d448973934ef3c07820fa169383 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralHelpers.ml
+++ b/helm/software/components/acic_procedural/proceduralHelpers.ml
@@ -32,6 +32,8 @@ module PEH  = ProofEngineHelpers
 module E    = CicEnvironment
 module UM   = UriManager
 module D    = Deannotate
+module PER  = ProofEngineReduction
+module Ut   = CicUtil
 
 (* fresh name generator *****************************************************)
 
@@ -131,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
@@ -159,6 +161,30 @@ let get_ind_parameters c t =
 
 let cic = D.deannotate_term
 
+let occurs c ~what ~where =
+   let result = ref false in
+   let equality c t1 t2 =
+      let r = Ut.alpha_equivalence t1 t2 in
+      result := !result || r; r
+   in
+   let context, what, with_what = c, [what], [C.Rel 0] in
+   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