Previous  Up  

Module UntypedAST.T

module T: STerm
type location = ParseLocation.t 
type var =
| V of string
| Wildcard 
type t = private {
   term : view;
   loc : location option;
} 
type view =
| Var of var (*
variable
*)
| Const of string (*
constant
*)
| AppBuiltin of Builtin.t * t list
| App of t * t list (*
apply term
*)
| Bind of Binder.t * typed_var list * t (*
bind n variables
*)
| List of t list (*
special constructor for lists
*)
| Record of (string * t) list * var option (*
extensible record
*) 
type typed_var = var * t option 
type term = t 
val view : t -> view
val loc : t -> location option
include Interfaces.HASH
include Interfaces.ORD
val var : ?loc:location -> string -> t
val v_wild : t
wildcard
val mk_var : ?loc:location -> var -> t
val app : ?loc:location -> t -> t list -> t
val builtin : ?loc:location -> Builtin.t -> t
val app_builtin : ?loc:location -> Builtin.t -> t list -> t
val const : ?loc:location -> string -> t
val bind : ?loc:location -> Binder.t -> typed_var list -> t -> t
val list_ : ?loc:location -> t list -> t
val nil : t
val record : ?loc:location ->
       (string * t) list -> rest:var option -> t
val at_loc : loc:location -> t -> t
val wildcard : t
val is_app : t -> bool
val is_var : t -> bool
val true_ : t
val false_ : t
val and_ : ?loc:location -> t list -> t
val or_ : ?loc:location -> t list -> t
val not_ : ?loc:location -> t -> t
val equiv : ?loc:location -> t -> t -> t
val xor : ?loc:location -> t -> t -> t
val imply : ?loc:location -> t -> t -> t
val eq : ?loc:location -> t -> t -> t
val neq : ?loc:location -> t -> t -> t
val forall : ?loc:location -> typed_var list -> t -> t
val exists : ?loc:location -> typed_var list -> t -> t
val lambda : ?loc:location -> typed_var list -> t -> t
val int_ : Z.t -> t
val of_int : int -> t
val rat : Q.t -> t
val tType : t
val term : t
val prop : t
val ty_int : t
val ty_rat : t
val fun_ty : ?loc:location -> t list -> t -> t
val forall_ty : ?loc:location -> typed_var list -> t -> t
module Set: CCSet.S  with type elt = term
module Map: CCMap.S  with type key = term
module Tbl: CCHashtbl.S  with type key = term
module StringSet: CCSet.S  with type elt = string
module Seq: sig .. end
val ground : t -> bool
val close_all : Binder.t -> t -> t
Bind all free vars with the symbol
val subterm : strict:bool -> t -> sub:t -> bool
is sub a (strict?) subterm of the other arg?
include Interfaces.PRINT
module TPTP: sig .. end
module ZF: sig .. end