Module TypingBase

Data structure and basic functions for typing

exception Type_error of string

Raised in case of type error, not propagated because replaced by an error constructor in the proof

val type_error : string -> 'a
exception Subtype_error of string

Raised in case of subtyping error, not propagated because replaced by an error constructor in the proof

val subtype_error : string -> 'a
exception Loop_error of Pos.popt

Raised when the termination checkers fails, propagated

val loop_error : Pos.popt -> 'a
type induction_node = Sct.index * (int * Ast.ordi) list
type ctxt = {
sub_ihs : Ast.schema list;
fix_ihs : fix_induction list;
fix_todo : (unit -> unit) list Stdlib.ref;
top_induction : induction_node;
call_graphs : Sct.t;
non_zero : Ast.ordi list;
}
and fix_induction = (Ast.term', Ast.term) Bindlib.binder * Ast.schema list Stdlib.ref

induction hypothesis for typing recursive programs

val empty_ctxt : unit -> ctxt

the initial empty context

val run_fix_todo : ctxt -> unit

run the registered functions.

val find_indexes : Sct.t -> Ast.ordi list -> Sct.index -> Sct.index -> (int * Ast.ordi) list -> (int * Ast.ordi) list -> Sct.matrix
val consecutive : (int * Ast.ordi) list -> bool
val build_call : ctxt -> Sct.index -> (int * Ast.ordi) list -> bool -> Sct.call
val add_call : ctxt -> Sct.index -> (int * Ast.ordi) list -> bool -> unit
val opred : Ast.ordi -> Ast.ord_wit -> Ast.ordi

construction of an ordinal < o such that w

val ofindpred : ctxt -> Ast.ordi -> Ast.ordi

find an ordinal o' < o

val dot_proj : Ast.term -> Ast.kind -> string -> Ast.kind
val print_nz : 'a -> ctxt -> unit
val add_pos : Ast.ordi list -> Ast.ordi -> Ast.ordi list
val add_positive : ctxt -> Ast.ordi -> ctxt
val add_positives : ctxt -> Ast.ordi list -> ctxt
val has_leading_ord_quantifier : Ast.kind -> bool
val has_leading_exists : Ast.kind -> bool
val has_leading_forall : Ast.kind -> bool
val has_uvar : Ast.kind -> bool