Module Logtk_parsers.Tip_astSource

Trivial AST for parsing

Sourceval pp_str : Format.formatter -> string -> unit
Sourceval pp_to_string : (Format.formatter -> 'a -> 'b) -> 'a -> string
Sourcetype var = string
Sourcetype ty_var = string
Sourcetype ty =
  1. | Ty_bool
  2. | Ty_app of ty_var * ty list
  3. | Ty_arrow of ty list * ty

Polymorphic types

Sourcetype typed_var = var * ty
Sourcetype term =
  1. | True
  2. | False
  3. | Const of string
  4. | App of string * term list
  5. | HO_app of term * term
  6. | Match of term * match_branch list
  7. | If of term * term * term
  8. | Let of (var * term) list * term
  9. | Fun of typed_var * term
  10. | Eq of term * term
  11. | Imply of term * term
  12. | And of term list
  13. | Or of term list
  14. | Not of term
  15. | Distinct of term list
  16. | Cast of term * ty
  17. | Forall of (var * ty) list * term
  18. | Exists of (var * ty) list * term

AST: S-expressions with locations

Sourceand match_branch =
  1. | Match_default of term
  2. | Match_case of string * var list * term
Sourcetype cstor = {
  1. cstor_name : string;
  2. cstor_args : (string * ty) list;
}
Sourcetype 'arg fun_decl = {
  1. fun_ty_vars : ty_var list;
  2. fun_name : string;
  3. fun_args : 'arg list;
  4. fun_ret : ty;
}
Sourcetype fun_def = {
  1. fr_decl : typed_var fun_decl;
  2. fr_body : term;
}
Sourcetype funs_rec_def = {
  1. fsr_decls : typed_var fun_decl list;
  2. fsr_bodies : term list;
}
Sourcetype statement = {
  1. stmt : stmt;
  2. loc : Loc.t option;
}
Sourceand stmt =
  1. | Stmt_decl_sort of string * int
  2. | Stmt_decl of ty fun_decl
  3. | Stmt_fun_def of fun_def
  4. | Stmt_fun_rec of fun_def
  5. | Stmt_funs_rec of funs_rec_def
  6. | Stmt_data of ty_var list * (string * cstor list) list
  7. | Stmt_assert of term
  8. | Stmt_lemma of term
  9. | Stmt_assert_not of ty_var list * term
  10. | Stmt_check_sat
Sourceval ty_bool : ty
Sourceval ty_app : ty_var -> ty list -> ty
Sourceval ty_const : ty_var -> ty
Sourceval ty_arrow_l : ty list -> ty -> ty
Sourceval ty_arrow : ty -> ty -> ty
Sourceval true_ : term
Sourceval false_ : term
Sourceval const : string -> term
Sourceval app : string -> term list -> term
Sourceval ho_app : term -> term -> term
Sourceval ho_app_l : term -> term list -> term
Sourceval match_ : term -> match_branch list -> term
Sourceval if_ : term -> term -> term -> term
Sourceval fun_ : typed_var -> term -> term
Sourceval fun_l : typed_var list -> term -> term
Sourceval let_ : (var * term) list -> term -> term
Sourceval eq : term -> term -> term
Sourceval imply : term -> term -> term
Sourceval and_ : term list -> term
Sourceval or_ : term list -> term
Sourceval distinct : term list -> term
Sourceval cast : term -> ty:ty -> term
Sourceval forall : (var * ty) list -> term -> term
Sourceval exists : (var * ty) list -> term -> term
Sourceval not_ : term -> term
Sourceval _mk : ?loc:Loc.t -> stmt -> statement
Sourceval mk_cstor : string -> (string * ty) list -> cstor
Sourceval mk_fun_decl : ty_vars:ty_var list -> string -> 'a list -> ty -> 'a fun_decl
Sourceval mk_fun_rec : ty_vars:ty_var list -> string -> typed_var list -> ty -> term -> fun_def
Sourceval decl_sort : ?loc:Loc.t -> string -> arity:int -> statement
Sourceval decl_fun : ?loc:Loc.t -> tyvars:ty_var list -> string -> ty list -> ty -> statement
Sourceval fun_def : ?loc:Loc.t -> fun_def -> statement
Sourceval fun_rec : ?loc:Loc.t -> fun_def -> statement
Sourceval funs_rec : ?loc:Loc.t -> typed_var fun_decl list -> term list -> statement
Sourceval data : ?loc:Loc.t -> ty_var list -> (string * cstor list) list -> statement
Sourceval assert_ : ?loc:Loc.t -> term -> statement
Sourceval lemma : ?loc:Loc.t -> term -> statement
Sourceval assert_not : ?loc:Loc.t -> ty_vars:ty_var list -> term -> statement
Sourceval check_sat : ?loc:Loc.t -> unit -> statement
Sourceval loc : statement -> Loc.t option
Sourceval view : statement -> stmt
Sourceval fpf : Format.formatter -> ('a, Format.formatter, unit) format -> 'a
Sourceval pp_list : ?start:string -> ?stop:string -> ?sep:string -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
Sourceval pp_tyvar : Format.formatter -> string -> unit
Sourceval pp_ty : Format.formatter -> ty -> unit
Sourceval pp_term : Format.formatter -> term -> unit
Sourceval pp_typed_var : Format.formatter -> typed_var -> unit
Sourceval pp_par : (Format.formatter -> 'a -> unit) -> Format.formatter -> (string list * 'a) -> unit
Sourceval pp_fun_decl : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a fun_decl -> unit
Sourceval pp_fr : Format.formatter -> fun_def -> unit
Sourceval pp_stmt : Format.formatter -> statement -> unit

Errors

Sourceexception Parse_error of Loc.t option * string
Sourceval parse_error : ?loc:Loc.t -> string -> 'a
Sourceval parse_errorf : ?loc:Loc.t -> ('a, unit, string, 'b) format4 -> 'a