*)
exception NotEnoughElements
-exception NameExpected
val source_id_of_id : string -> string
{annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
;;
-val acic_of_cic_context' :
- int ref -> (* seed *)
- (Cic.id, Cic.term) Hashtbl.t -> (* ids_to_terms *)
- (Cic.id, Cic.id option) Hashtbl.t -> (* ids_to_father_ids *)
- (Cic.id, string) Hashtbl.t -> (* ids_to_inner_sorts *)
- (Cic.id, anntypes) Hashtbl.t -> (* ids_to_inner_types *)
- Cic.metasenv -> (* metasenv *)
- Cic.context -> (* context *)
- Cic.id list -> (* idrefs *)
- Cic.term -> (* term *)
- Cic.term option -> (* expected type *)
- Cic.annterm (* annotated term *)
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
+
+val string_of_sort: sort_kind -> string
+(*val sort_of_string: string -> sort_kind*)
+val sort_of_sort: Cic.sort -> sort_kind
val acic_object_of_cic_object :
+ ?eta_fix: bool -> (* perform eta_fixing; default: true*)
Cic.obj -> (* object *)
- Cic.annobj * (* annotated object *)
- (Cic.id, Cic.term) Hashtbl.t * (* ids_to_terms *)
- (Cic.id, Cic.id option) Hashtbl.t * (* ids_to_father_ids *)
- (Cic.id, string) Hashtbl.t * (* ids_to_inner_sorts *)
- (Cic.id, anntypes) Hashtbl.t * (* ids_to_inner_types *)
- (Cic.id, Cic.conjecture) Hashtbl.t * (* ids_to_conjectures *)
- (Cic.id, Cic.hypothesis) Hashtbl.t (* ids_to_hypotheses *)
+ Cic.annobj * (* annotated object *)
+ (Cic.id, Cic.term) Hashtbl.t * (* ids_to_terms *)
+ (Cic.id, Cic.id option) Hashtbl.t * (* ids_to_father_ids *)
+ (Cic.id, sort_kind) Hashtbl.t * (* ids_to_inner_sorts *)
+ (Cic.id, anntypes) Hashtbl.t * (* ids_to_inner_types *)
+ (Cic.id, Cic.conjecture) Hashtbl.t * (* ids_to_conjectures *)
+ (Cic.id, Cic.hypothesis) Hashtbl.t (* ids_to_hypotheses *)
+
+val asequent_of_sequent :
+ Cic.metasenv -> (* metasenv *)
+ Cic.conjecture -> (* sequent *)
+ Cic.conjecture * (* unshared sequent *)
+ (Cic.annconjecture * (* annotated sequent *)
+ (Cic.id, Cic.term) Hashtbl.t * (* ids_to_terms *)
+ (Cic.id, Cic.id option) Hashtbl.t * (* ids_to_father_ids *)
+ (Cic.id, sort_kind) Hashtbl.t * (* ids_to_inner_sorts *)
+ (Cic.id, Cic.hypothesis) Hashtbl.t) (* ids_to_hypotheses *)
+
+val plain_acic_object_of_cic_object : Cic.obj -> Cic.annobj