exception Uncertain of string
exception AssertFailure of string
-exception SubstNotFound of int
-
(* The entry (i,t) in a substitution means that *)
(* (META i) have been instantiated with t. *)
-type substitution = (int * (Cic.context * Cic.term)) list
+(* type substitution = (int * (Cic.context * Cic.term)) list *)
(** @raise SubstNotFound *)
-val lookup_subst: int -> substitution -> Cic.context * Cic.term
(* apply_subst subst t *)
(* applies the substitution [subst] to [t] *)
(* [subst] must be already unwinded *)
-val apply_subst : substitution -> Cic.term -> Cic.term
-
-val apply_subst_context : substitution -> Cic.context -> Cic.context
-val apply_subst_metasenv: substitution -> Cic.metasenv -> Cic.metasenv
-
-(* {2 Kernel wrappers}
- * From now on we recreate a kernel abstraction where substitutions are part of
- * the calculus *)
-val lift : substitution -> int -> Cic.term -> Cic.term
-val subst: substitution -> Cic.term -> Cic.term -> Cic.term
-val whd: substitution -> Cic.context -> Cic.term -> Cic.term
-val are_convertible: substitution -> Cic.context -> Cic.term -> Cic.term -> bool
-
-val type_of_aux':
- Cic.metasenv -> substitution -> Cic.context -> Cic.term -> Cic.term
-
-val tempi_type_of_aux : float ref
-val tempi_subst : float ref
-val tempi_type_of_aux_subst : float ref
+val apply_subst : Cic.substitution -> Cic.term -> Cic.term
+val apply_subst_context : Cic.substitution -> Cic.context -> Cic.context
+val apply_subst_metasenv: Cic.substitution -> Cic.metasenv -> Cic.metasenv
(*** delifting ***)
val delift :
- int -> substitution -> Cic.context -> Cic.metasenv ->
+ int -> Cic.substitution -> Cic.context -> Cic.metasenv ->
(Cic.term option) list -> Cic.term ->
- Cic.term * Cic.metasenv * substitution
-
+ Cic.term * Cic.metasenv * Cic.substitution
+val restrict :
+ Cic.substitution -> (int * int) list -> Cic.metasenv ->
+ Cic.metasenv * Cic.substitution
(** {2 Pretty printers} *)
-val ppsubst: substitution -> string
-val ppterm: substitution -> Cic.term -> string
-val ppcontext: ?sep: string -> substitution -> Cic.context -> string
+val ppsubst_unfolded: Cic.substitution -> string
+val ppsubst: Cic.substitution -> string
+val ppterm: Cic.substitution -> Cic.term -> string
+val ppcontext: ?sep: string -> Cic.substitution -> Cic.context -> string
val ppterm_in_context:
- substitution -> Cic.term -> (Cic.name option) list -> string
-val ppmetasenv: ?sep: string -> Cic.metasenv -> substitution -> string
+ Cic.substitution -> Cic.term -> (Cic.name option) list -> string
+val ppmetasenv: ?sep: string -> Cic.metasenv -> Cic.substitution -> string
(** {2 Format-like pretty printers}
* As above with prototypes suitable for toplevel/ocamldebug printers. No
* with only one argument.
*)
-val fppsubst: Format.formatter -> substitution -> unit
+val fppsubst: Format.formatter -> Cic.substitution -> unit
val fppterm: Format.formatter -> Cic.term -> unit
val fppmetasenv: Format.formatter -> Cic.metasenv -> unit
+(*
(* DEBUG *)
val print_counters: unit -> unit
val reset_counters: unit -> unit
+*)
+(* val clean_up_meta :
+ Cic.substitution -> Cic.metasenv -> Cic.term -> Cic.term
+*)