Up  Next

Module Tip_ast

module Tip_ast: sig .. end

Trivial AST for parsing


val pp_str : Format.formatter -> string -> unit
val pp_to_string : (Format.formatter -> 'a -> 'b) -> 'a -> string
module Loc: Tip_loc
type var = string 
type ty_var = string 
type ty =
| Ty_bool
| Ty_app of ty_var * ty list
| Ty_arrow of ty list * ty
Polymorphic types
type typed_var = var * ty 
type 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
| 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


type match_branch =
| Match_default of term
| Match_case of string * var list * term 
type cstor = {
   cstor_name : string;
   cstor_args : (string * ty) list;
} 
type 'arg fun_decl = {
   fun_ty_vars : ty_var list;
   fun_name : string;
   fun_args : 'arg list;
   fun_ret : ty;
} 
type fun_def = {
   fr_decl : typed_var fun_decl;
   fr_body : term;
} 
type funs_rec_def = {
   fsr_decls : typed_var fun_decl list;
   fsr_bodies : term list;
} 
type statement = {
   stmt : stmt;
   loc : Loc.t option;
} 
type stmt =
| 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_check_sat 
val ty_bool : ty
val ty_app : ty_var -> ty list -> ty
val ty_const : ty_var -> ty
val ty_arrow_l : ty list -> ty -> ty
val ty_arrow : ty -> ty -> ty
val true_ : term
val false_ : term
val const : string -> term
val app : string -> term list -> term
val ho_app : term -> term -> term
val match_ : term -> match_branch list -> term
val if_ : term -> term -> term -> term
val fun_ : typed_var -> term -> term
val fun_l : typed_var list -> term -> term
val let_ : (var * term) list -> term -> term
val eq : term -> term -> term
val imply : term -> term -> term
val and_ : term list -> term
val or_ : term list -> term
val not_ : term -> term
val distinct : term list -> term
val cast : term -> ty:ty -> term
val forall : (var * ty) list -> term -> term
val exists : (var * ty) list -> term -> term
val _mk : ?loc:Loc.t -> stmt -> statement
val mk_cstor : string -> (string * ty) list -> cstor
val mk_fun_decl : ty_vars:ty_var list ->
       string -> 'a list -> ty -> 'a fun_decl
val mk_fun_rec : ty_vars:ty_var list ->
       string ->
       typed_var list -> ty -> term -> fun_def
val decl_sort : ?loc:Loc.t -> string -> arity:int -> statement
val decl_fun : ?loc:Loc.t ->
       tyvars:ty_var list ->
       string -> ty list -> ty -> statement
val fun_def : ?loc:Loc.t -> fun_def -> statement
val fun_rec : ?loc:Loc.t -> fun_def -> statement
val funs_rec : ?loc:Loc.t ->
       typed_var fun_decl list ->
       term list -> statement
val data : ?loc:Loc.t ->
       ty_var list ->
       (string * cstor list) list -> statement
val assert_ : ?loc:Loc.t -> term -> statement
val lemma : ?loc:Loc.t -> term -> statement
val assert_not : ?loc:Loc.t ->
       ty_vars:ty_var list -> term -> statement
val check_sat : ?loc:Loc.t -> unit -> statement
val loc : statement -> Loc.t option
val view : statement -> stmt
val fpf : Format.formatter -> ('a, Format.formatter, unit) Pervasives.format -> 'a
val pp_list : ?start:string ->
       ?stop:string ->
       ?sep:string ->
       (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
val pp_tyvar : Format.formatter -> string -> unit
val pp_ty : Format.formatter -> ty -> unit
val pp_term : Format.formatter -> term -> unit
val pp_typed_var : Format.formatter -> typed_var -> unit
val pp_par : (Format.formatter -> 'a -> unit) ->
       Format.formatter -> string list * 'a -> unit
val pp_fun_decl : (Format.formatter -> 'a -> unit) ->
       Format.formatter -> 'a fun_decl -> unit
val pp_fr : Format.formatter -> fun_def -> unit
val pp_stmt : Format.formatter -> statement -> unit

Errors


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