package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

AST utils for dedukti

module A = Logtk.UntypedAST
module T = Logtk.STerm
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.

type location = Logtk.ParseLocation.t
type var = Logtk.STerm.var =
  1. | V of string
  2. | Wildcard
type t = private Logtk.STerm.t = {
  1. term : view;
  2. loc : location option;
  3. attrs : attr list;
}
and match_branch = Logtk.STerm.match_branch =
  1. | Match_case of string * var list * t
  2. | Match_default of t
and 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. | With of (var * t) list * t
  9. | Bind of Logtk.Binder.t * typed_var list * t
    (*

    bind n variables

    *)
  10. | List of t list
    (*

    special constructor for lists

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

    extensible record

    *)
and typed_var = var * t option
and attr = Logtk.STerm.attr =
  1. | 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 with type t := t
val equal : t -> t -> bool
val hash : t -> int
include Logtk.Interfaces.ORD with type t := t
val compare : t -> t -> int
val v_wild : t

wildcard

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 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 with_ : ?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 is_lam : 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_ : Logtk_arith.Z.t -> t
val of_int : int -> t
val rat : Logtk_arith.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 = T.Set
module Map = T.Map
module Tbl = T.Tbl
module StringSet = T.StringSet
module Seq = T.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
val to_string : t -> string
val pp_typed_var : typed_var CCFormat.printer
val pp_var : var CCFormat.printer

Formats

module TPTP = T.TPTP
module TPTP_THF = T.TPTP_THF
module ZF = T.ZF

Subst

module StrMap = T.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 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) 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