Module Raw

Parser level AST and translation to final AST

type pordi = pordi' Pos.loc
and pordi' =
| PConv
| PSucc of pordi
| PVari of string
| POVar
type pkind = pkind' Pos.loc
and pkind' =
| PTVar of string * pordi list * pkind list
| PFunc of pkind * pkind
| PProd of (string * pkind) list * bool
| PDSum of (string * pkind option) list
| PKAll of string list * pkind
| PKExi of string list * pkind
| POAll of string list * pkind
| POExi of string list * pkind
| PFixM of pordi * string * pkind
| PFixN of pordi * string * pkind
| PWith of pkind * string * pkind
| PDPrj of Pos.strloc * string
| PUCst of pterm * string * pkind
| PECst of pterm * string * pkind
| PUVar
and pterm = pterm' Pos.loc
and pterm' =
| PCoer of pterm * pkind
| PMLet of string list * string list * pkind * string * pterm
| PLVar of string
| PLAbs of Pos.strloc * pkind option * pterm * Ast.sugar
| PAppl of pterm * pterm
| PReco of (string * pterm) list
| PProj of pterm * string
| PCons of string * pterm option
| PCase of pterm * (string * ppat * pterm) list * (ppat * pterm) option
| PPrnt of string
| PFixY of Pos.strloc * int * pterm
| PAbrt
and ppat =
| NilPat
| Simple of (Pos.strloc * pkind option) option
| Record of (string * (Pos.strloc * pkind option)) list
val list_nil : Pos.pos -> pterm' Pos.loc
val list_cons : Pos.pos -> pterm -> pterm -> pterm' Pos.loc
val unit_var : Pos.popt -> string Pos.loc * pkind' Pos.loc option
val sequence : Pos.pos -> pterm -> pterm -> pterm' Pos.loc
val fixpoint_depth : int Stdlib.ref
val pfixY : (Pos.strloc * pkind option) -> Pos.pos -> int option -> pterm -> pterm' Pos.loc
val pcoer : Pos.pos -> pterm -> pkind option -> pterm
val padd : Pos.pos -> pordi -> int -> pordi
val pappl : Pos.pos -> pterm' Pos.loc -> pterm -> pterm' Pos.loc
val apply_rpat : string -> ppat -> pterm -> pterm' Pos.loc
val plabs : Pos.pos -> ppat list -> pterm -> pterm
val pcond : Pos.pos -> pterm -> pterm -> pterm -> pterm' Pos.loc
type env = {
terms : (string * Ast.tvar) list;
kinds : (string * (Ast.kbox * Ast.occur)) list;
ordinals : (string * (Ast.obox * Ast.occur)) list;
}
val empty_env : env
val add_term : string -> Ast.tvar -> env -> env
val add_kind : string -> Ast.kvar -> Ast.occur -> env -> env
val add_ordi : string -> Ast.ovar -> Ast.occur -> env -> env
val add_kinds : string array -> Ast.kvar array -> env -> env
val add_ordis : string array -> Ast.ovar array -> env -> env
exception Unbound of string * Pos.popt
val unbound : string Pos.loc -> 'a
exception Arity_error of Pos.popt * string
val arity_error : Pos.popt -> string -> 'a
exception Positivity_error of Pos.popt * string
val positivity_error : Pos.popt -> string -> 'a
val term_variable : env -> Pos.strloc -> Ast.tbox
val ordinal_variable : Ast.occur -> env -> Pos.strloc -> Ast.obox
val kind_variable : Ast.occur -> env -> Pos.strloc -> pordi array -> pkind array -> Ast.kbox
val unsugar_ordinal : ?pos:Ast.occur -> env -> pordi -> Ast.obox
val unsugar_kind : ?pos:Ast.occur -> env -> pkind -> Ast.kbox
val unsugar_term : env -> pterm -> Ast.tbox