Module Logtk_parsers.Ast_dkSource

AST utils for dedukti

include module type of struct include T end

Simple Terms

.

Simple terms, that are not hashconsed, nor typed.

Those do not use De Bruijn indices for variable binding, but simply names (scoping is done later). Their simplicity make them good for heavy AST transformations, output of parsing, etc.

Terms are only compared, hashsed, etc. by their "term" component (the algebraic variant). Additional fields (location…) are ignored for almost every operation.

Sourcetype var = Logtk.STerm.var =
  1. | V of string
  2. | Wildcard
Sourcetype t = private Logtk.STerm.t = {
  1. term : view;
  2. loc : location option;
}
Sourceand match_branch = Logtk.STerm.match_branch =
  1. | Match_case of string * var list * t
  2. | Match_default of t
Sourceand view = Logtk.STerm.view =
  1. | Var of var
    (*

    variable

    *)
  2. | Const of string
    (*

    constant

    *)
  3. | AppBuiltin of Logtk.Builtin.t * t list
  4. | App of t * t list
    (*

    apply term

    *)
  5. | Ite of t * t * t
  6. | Match of t * match_branch list
  7. | Let of (var * t) list * t
  8. | Bind of Logtk.Binder.t * typed_var list * t
    (*

    bind n variables

    *)
  9. | List of t list
    (*

    special constructor for lists

    *)
  10. | Record of (string * t) list * var option
    (*

    extensible record

    *)
Sourceand typed_var = var * t option
Sourcetype term = t
Sourceval view : t -> view
Sourceval loc : t -> location option
include Logtk.Interfaces.HASH with type t := t
include Logtk.Interfaces.EQ with type t := t
Sourceval equal : t -> t -> bool
Sourceval hash : t -> int
include Logtk.Interfaces.ORD with type t := t
Sourceval compare : t -> t -> int
Sourceval v_wild : t

wildcard

Sourceval app : ?loc:location -> t -> t list -> t
Sourceval app_const : ?loc:location -> string -> t list -> t
Sourceval builtin : ?loc:location -> Logtk.Builtin.t -> t
Sourceval app_builtin : ?loc:location -> Logtk.Builtin.t -> t list -> t
Sourceval bind : ?loc:location -> Logtk.Binder.t -> typed_var list -> t -> t
Sourceval ite : ?loc:location -> t -> t -> t -> t
Sourceval match_ : ?loc:location -> t -> match_branch list -> t
Sourceval let_ : ?loc:location -> (var * t) list -> t -> t
Sourceval list_ : ?loc:location -> t list -> t
Sourceval nil : t
Sourceval record : ?loc:location -> (string * t) list -> rest:var option -> t
Sourceval at_loc : loc:location -> t -> t
Sourceval wildcard : t
Sourceval is_app : t -> bool
Sourceval is_var : t -> bool
Sourceval true_ : t
Sourceval false_ : t
Sourceval and_ : ?loc:location -> t list -> t
Sourceval or_ : ?loc:location -> t list -> t
Sourceval not_ : ?loc:location -> t -> t
Sourceval equiv : ?loc:location -> t -> t -> t
Sourceval xor : ?loc:location -> t -> t -> t
Sourceval imply : ?loc:location -> t -> t -> t
Sourceval eq : ?loc:location -> t -> t -> t
Sourceval neq : ?loc:location -> t -> t -> t
Sourceval forall : ?loc:location -> typed_var list -> t -> t
Sourceval exists : ?loc:location -> typed_var list -> t -> t
Sourceval lambda : ?loc:location -> typed_var list -> t -> t
Sourceval int_ : Z.t -> t
Sourceval of_int : int -> t
Sourceval rat : Q.t -> t
Sourceval real : string -> t
Sourceval tType : t
Sourceval term : t
Sourceval prop : t
Sourceval ty_int : t
Sourceval ty_rat : t
Sourceval ty_real : t
Sourceval fun_ty : ?loc:location -> t list -> t -> t
Sourceval forall_ty : ?loc:location -> typed_var list -> t -> t
Sourceval ty_unfold : t -> t list * t
Sourceval unfold_bind : Logtk.Binder.t -> t -> typed_var list * t
Sourcemodule Set = T.Set
Sourcemodule Map = T.Map
Sourcemodule Tbl = T.Tbl
Sourcemodule StringSet = T.StringSet
Sourcemodule Seq = T.Seq
Sourceval ground : t -> bool
Sourceval close_all : Logtk.Binder.t -> t -> t

Bind all free vars with the symbol

Sourceval subterm : strict:bool -> t -> sub:t -> bool

is sub a (strict?) subterm of the other arg?

Print

include Logtk.Interfaces.PRINT with type t := t
Sourceval to_string : t -> string

Formats

Sourcemodule TPTP = T.TPTP
Sourcemodule ZF = T.ZF

Subst

Sourcemodule StrMap = T.StrMap
Sourcetype subst = t StrMap.t
Sourceval empty_subst : subst
Sourceval merge_subst : subst -> subst -> subst

merge a b merges a into b, but favors b in case of conflict

Sourceval apply_subst : subst -> term -> term
Sourcetype ty = T.t
Sourceval cast : T.t -> T.t -> term
Sourceval const : string -> T.t
Sourceval mk_const : string -> T.t -> term
Sourceval mk_const_t : string -> term
Sourceval var : string -> T.t
Sourceval mk_var : string -> T.t -> term
Sourceval mk_var_t : string -> term
Sourceval v : string -> var
Sourceval ty_aliases : (string, ty) Hashtbl.t
Sourceval find_alias : or_else:ty -> string -> ty
Sourceval add_alias : string -> T.t -> unit
Sourceval type_nat : term
Sourceexception Unknown_builtin of string
Sourceexception Bad_arity of string * int
Sourceexception Application_head_is_not_a_var of term
Sourceval mk_app : T.t -> T.t list -> T.t
Sourceval mk_app_const : string -> T.t list -> T.t
Sourceval mk_arrow_l : T.t list -> T.t -> T.t
Sourceval mk_arrow : T.t -> T.t -> T.t
Sourceval mk_fun : T.typed_var list -> T.t -> T.t
Sourceval mk_forall : T.typed_var list -> T.t -> T.t
Sourceval mk_int : string -> T.t
Sourceval ty_prop : T.t
Sourceval mk_ty_decl : ?loc:A.Loc.t -> string -> A.ty -> A.statement
Sourceval mk_assert : ?loc:A.Loc.t -> name:string -> A.term -> A.statement
Sourceval mk_goal : ?loc:A.Loc.t -> name:string -> A.term -> A.statement
Sourceval mk_def : ?loc:A.Loc.t -> string -> A.ty -> T.t -> A.statement
Sourceval mk_rewrite : ?loc:A.Loc.t -> A.term -> A.statement