module E = CicEnvironment
module UM = UriManager
module D = Deannotate
+module PER = ProofEngineReduction
+module Ut = CicUtil
(* fresh name generator *****************************************************)
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 -> "_rec"
- | 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
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