Module `Tip_ast`Source

Trivial AST for parsing

Sourceval pp_to_string : (Format.formatter -> 'a -> unit) -> 'a -> string

Sourcemodule Loc = Tip_loc

Sourcetype var = string

Sourcetype ty_var = string

Sourcetype ty =

| Ty_bool
| Ty_app of ty_var * ty list
| Ty_arrow of ty list * ty

Polymorphic types

Sourcetype typed_var = var * ty

Sourcetype term =

| True
| False
| Const of string
| App of string * term list
| HO_app of term * term
| Match of term * match_branch list
| If of term * term * term
| Let of (var * term) list * term
| Is_a of string * term
| Fun of typed_var * term
| Eq of term * term
| Imply of term * term
| And of term list
| Or of term list
| Not of term
| Distinct of term list
| Cast of term * ty
| Forall of (var * ty) list * term
| Exists of (var * ty) list * term

AST: S-expressions with locations

Sourceand match_branch =

| Match_default of term
| Match_case of string * var list * term

Sourcetype cstor = {

cstor_name : string;
cstor_args : (string * ty) list;

}

Sourcetype 'arg fun_decl = {

fun_ty_vars : ty_var list;
fun_name : string;
fun_args : 'arg list;
fun_ret : ty;

}

Sourcetype fun_def = {

fr_decl : typed_var fun_decl;
fr_body : term;

}

Sourcetype funs_rec_def = {

fsr_decls : typed_var fun_decl list;
fsr_bodies : term list;

}

Sourcetype statement = {

stmt : stmt;
loc : Loc.t option;

}

Sourceand stmt =

| Stmt_set_logic of string
| Stmt_set_info of string * string
| Stmt_decl_sort of string * int
| Stmt_decl of ty fun_decl
| Stmt_fun_def of fun_def
| Stmt_fun_rec of fun_def
| Stmt_funs_rec of funs_rec_def
| Stmt_data of ty_var list * (string * cstor list) list
| Stmt_assert of term
| Stmt_lemma of term
| Stmt_assert_not of ty_var list * term
| Stmt_prove of ty_var list * term
| Stmt_check_sat
| Stmt_exit

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 is_a : string -> 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

Source

val 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

Source

val 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 prove : ?loc:Loc.t -> ty_vars:ty_var list -> term -> statement

Sourceval check_sat : ?loc:Loc.t -> unit -> statement

Sourceval exit : ?loc:Loc.t -> unit -> statement

Sourceval set_logic : ?loc:Loc.t -> string -> statement

Sourceval set_info : ?loc:Loc.t -> string -> string -> statement

Sourceval loc : statement -> Loc.t option

Sourceval view : statement -> stmt

Sourceval fpf : Format.formatter -> ('a, Format.formatter, unit) format -> 'a

Source

val pp_list : 
  (Format.formatter -> 'a -> unit) ->
  Format.formatter ->
  'a list ->
  unit

Sourceval pp_str : Format.formatter -> string -> unit

Sourceval pp_tyvar : Format.formatter -> string -> unit

Sourceval pp_ty : Format.formatter -> ty -> unit

Sourceval lvl_top : int

Sourceval lvl_q : int

Sourceval lvl_let : int

Sourceval lvl_match : int

Sourceval lvl_and : int

Sourceval lvl_or : int

Sourceval lvl_not : int

Sourceval lvl_app : int

Sourceval pp_typed_var : Format.formatter -> typed_var -> unit

Sourceval pp_term : Format.formatter -> term -> unit

Source

val pp_par : 
  (Format.formatter -> 'a -> unit) ->
  Format.formatter ->
  (string list * 'a) ->
  unit

Source

val 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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/tip-parser/Tip_ast/index.html

Module `Tip_ast`Source

Trivial AST for parsing

Errors

package tip-parser

Install

Dune Dependency

Authors

Maintainers

Sources

doc/tip-parser/Tip_ast/index.html

Module Tip_astSource

Trivial AST for parsing

Errors

Module `Tip_ast`Source