Module Generalise

exception FailGeneralise

Raised when generalisation is not a good idea. Currently when

  • KMRec and KNRec are present.
type 'a particular = (int * Ast.ordi) list * Ast.ordi list * 'a * Ast.kind

the type of a particular judgement, ordinal being witnesses or ordinal variables

val recompose : ?general:bool -> Ast.schema -> Ast.term_or_kind particular

function to apply a schema. I

  • If general = false, it replace the ordinals with appropriate witnesses to prove the schema (not to use it).
  • If general = true, we want to use the schema and all ordinals are replaced with variables
val recompose_kind : ?general:bool -> Ast.schema -> Ast.kind particular

recompose for subtyping

val recompose_term : ?general:bool -> Ast.schema -> unit particular

recompose for typing

val generalise : ?manual:bool -> Ast.ordi list -> Ast.term_or_kind -> Ast.kind -> Sct.t -> (Ast.schema * (int * Ast.ordi) list) option
val kuvar_list : Ast.kind -> (Ast.kuvar * Ast.ordi array) list

Returns the list of unification variables. When a variable has arguments, they should be identical for all occurences.

val ouvar_list : Ast.kind -> Ast.ouvar list

Same as above for ordinal variables