Module Logtk_parsers.Ast_dk

AST utils for dedukti

module A = Logtk.UntypedAST
module T = Logtk.STerm
include T

Simple Terms

.

type location = Logtk.ParseLocation.t
type var =
| V of string
| Wildcard
type t = private {
term : view;
loc : location option;
attrs : attr list;
}
and match_branch =
| Match_case of string * var list * t
| Match_default of t
and view =
| Var of var

variable

| Const of string

constant

| AppBuiltin of Logtk.Builtin.t * t list
| App of t * t list

apply term

| Ite of t * t * t
| Match of t * match_branch list
| Let of (var * t) list * t
| Bind of Logtk.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

and typed_var = var * t option
and attr =
| Attr_distinct_const
type term = t
val view : t -> view
val loc : t -> location option
include Logtk.Interfaces.HASH with type t := t
include Logtk.Interfaces.EQ
type t
val equal : t -> t -> bool
val hash : t -> int
include Logtk.Interfaces.ORD with type t := t
type t
val compare : t -> t -> int
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 app_const : ?⁠loc:location -> string -> t list -> t
val builtin : ?⁠loc:location -> Logtk.Builtin.t -> t
val app_builtin : ?⁠loc:location -> Logtk.Builtin.t -> t list -> t
val const : ?⁠loc:location -> ?⁠attrs:attr list -> string -> t
val bind : ?⁠loc:location -> Logtk.Binder.t -> typed_var list -> t -> t
val ite : ?⁠loc:location -> t -> t -> t -> t
val match_ : ?⁠loc:location -> t -> match_branch list -> t
val let_ : ?⁠loc:location -> (var * t) 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 real : string -> t
val tType : t
val term : t
val prop : t
val ty_int : t
val ty_rat : t
val ty_real : t
val fun_ty : ?⁠loc:location -> t list -> t -> t
val forall_ty : ?⁠loc:location -> typed_var list -> t -> t
val ty_unfold : t -> t list * t
val unfold_bind : Logtk.Binder.t -> t -> typed_var list * t
module Set = Logtk.STerm.Set
module Map = Logtk.STerm.Map
module Tbl = Logtk.STerm.Tbl
module StringSet = Logtk.STerm.StringSet
module Seq = Logtk.STerm.Seq
val ground : t -> bool
val close_all : Logtk.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?

Print

include Logtk.Interfaces.PRINT with type t := t
type t
val pp : t CCFormat.printer
val to_string : t -> string
val pp_typed_var : typed_var CCFormat.printer
val pp_var : var CCFormat.printer

Formats

module TPTP = Logtk.STerm.TPTP
module TPTP_THF = Logtk.STerm.TPTP_THF
module ZF = Logtk.STerm.ZF
val pp_in : Logtk.Output_format.t -> t CCFormat.printer

Subst

module StrMap = Logtk.STerm.StrMap
type subst = t StrMap.t
val empty_subst : subst
val merge_subst : subst -> subst -> subst

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

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