Module UntypedAST

module UntypedAST: sig .. end

module Loc: Location

exception ParseError of Loc.t

exception SyntaxError of string * Loc.t option

type var = string 

type var_or_wildcard = [ `Var of string | `Wildcard ] 

module Builtin: sig .. end

type term = term_node Loc.with_loc 

type term_node = 

type ty = term 

type typed_var = var * ty option 

val view : 'a Loc.with_loc -> 'a

type rec_defs = (string * term * term list) list 

type spec_defs = (string * term) list * term list 

type mutual_types = (var * var list *
        (var * ty list) list)
       list 

type mutual_preds = (var * ty * term list) list 

type copy_wrt = 

type copy = {

type attribute = string list 

type statement_node = 

type statement = {

val wildcard : ?loc:Loc.t -> unit -> term_node Loc.with_loc

val builtin : ?loc:Loc.t -> Builtin.t -> term_node Loc.with_loc

val var : ?loc:Loc.t -> string -> term_node Loc.with_loc

val at_var : ?loc:Loc.t -> var -> term_node Loc.with_loc

val meta_var : ?loc:Loc.t -> var -> term_node Loc.with_loc

val app : ?loc:Loc.t ->
       term_node Loc.with_loc ->
       term list -> term_node Loc.with_loc

val fun_ : ?loc:Loc.t ->
       typed_var -> term -> term_node Loc.with_loc

val let_ : ?loc:Loc.t ->
       var ->
       term -> term -> term_node Loc.with_loc

val match_with : ?loc:Loc.t ->
       term ->
       (var * var_or_wildcard list * term) list ->
       term_node Loc.with_loc

val ite : ?loc:Loc.t ->
       term ->
       term -> term -> term_node Loc.with_loc

val ty_prop : term_node Loc.with_loc

val ty_type : term_node Loc.with_loc

val true_ : term_node Loc.with_loc

val false_ : term_node Loc.with_loc

val not_ : ?loc:Loc.t -> term -> term_node Loc.with_loc

val app_infix_l : ?loc:Loc.t ->
       term_node Loc.with_loc -> term list -> term

val and_ : ?loc:Loc.t -> term list -> term

val or_ : ?loc:Loc.t -> term list -> term

val imply : ?loc:Loc.t ->
       term -> term -> term_node Loc.with_loc

val equiv : ?loc:Loc.t ->
       term -> term -> term_node Loc.with_loc

val eq : ?loc:Loc.t ->
       term -> term -> term_node Loc.with_loc

val neq : ?loc:Loc.t ->
       term -> term -> term_node Loc.with_loc

val forall : ?loc:Loc.t ->
       typed_var -> term -> term_node Loc.with_loc

val exists : ?loc:Loc.t ->
       typed_var -> term -> term_node Loc.with_loc

val mu : ?loc:Loc.t ->
       typed_var -> term -> term_node Loc.with_loc

val asserting : ?loc:Loc.t -> term -> term list -> term

val ty_arrow : ?loc:Loc.t ->
       ty -> ty -> term_node Loc.with_loc

val ty_forall : ?loc:Loc.t ->
       var -> ty -> term_node Loc.with_loc

val ty_forall_list : ?loc:Loc.t -> var list -> ty -> ty

val ty_arrow_list : ?loc:Loc.t -> ty list -> ty -> ty

val forall_list : ?loc:Loc.t -> typed_var list -> term -> term

val exists_list : ?loc:Loc.t -> typed_var list -> term -> term

val fun_list : ?loc:Loc.t -> typed_var list -> term -> term

val forall_term : term_node Loc.with_loc

val exists_term : term_node Loc.with_loc

val mk_stmt_ : ?loc:Loc.t ->
       ?name:string -> statement_node -> statement

val include_ : ?name:string ->
       ?loc:Loc.t -> ?which:string list -> string -> statement

val decl : ?name:string ->
       ?loc:Loc.t ->
       attrs:attribute list ->
       var -> ty -> statement

val axiom : ?name:string -> ?loc:Loc.t -> term list -> statement

val spec : ?name:string -> ?loc:Loc.t -> spec_defs -> statement

val rec_ : ?name:string -> ?loc:Loc.t -> rec_defs -> statement

val def : ?name:string ->
       ?loc:Loc.t -> string -> term -> statement

val data : ?name:string -> ?loc:Loc.t -> mutual_types -> statement

val codata : ?name:string -> ?loc:Loc.t -> mutual_types -> statement

val pred : ?name:string ->
       ?loc:Loc.t ->
       wf:[ `Not_wf | `Wf ] -> mutual_preds -> statement

val copred : ?name:string ->
       ?loc:Loc.t ->
       wf:[ `Not_wf | `Wf ] -> mutual_preds -> statement

val copy : ?name:string ->
       ?loc:Loc.t ->
       of_:term ->
       wrt:copy_wrt ->
       abstract:var ->
       concrete:var ->
       var -> var list -> statement

val goal : ?name:string -> ?loc:Loc.t -> term -> statement

val head : term_node Loc.with_loc -> var

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

val pp_var_or_wildcard : CCFormat.t -> [< `Var of string | `Wildcard ] -> unit

val unroll_if_ : term_node Loc.with_loc ->
       (term * term) list * term_node Loc.with_loc

val pp_list_ : sep:string -> 'a CCFormat.printer -> 'a list CCFormat.printer

val print_term : CCFormat.t -> term_node Loc.with_loc -> unit

val print_term_inner : term CCFormat.printer

val print_term_in_arrow : CCFormat.t -> ty -> unit

val print_typed_var : CCFormat.t -> typed_var -> unit

val pp_rec_defs : Format.formatter ->
       (string * term_node Loc.with_loc *
        term_node Loc.with_loc list)
       list -> unit

val pp_spec_defs : Format.formatter ->
       (string * term_node Loc.with_loc) list *
       term_node Loc.with_loc list -> unit

val pp_ty_defs : Format.formatter ->
       (string * string list *
        (string * term_node Loc.with_loc list) list)
       list -> unit

val pp_wf : Format.formatter -> [< `Not_wf | `Wf ] -> unit

val pp_mutual_preds : CCFormat.t ->
       (string * term_node Loc.with_loc *
        term_node Loc.with_loc list)
       list -> unit

val pp_attr : Format.formatter -> string list -> unit

val pp_attrs : Format.formatter -> string list list -> unit

val print_statement : Format.formatter -> statement -> unit

val print_statement_list : Format.formatter -> statement list -> unit

module TPTP: sig .. end