package logtk

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

Trivial AST for parsing

val pp_str : Stdlib.Format.formatter -> string -> unit
val pp_to_string : (Stdlib.Format.formatter -> 'a -> 'b) -> 'a -> string
module Loc = Logtk.ParseLocation
type var = string
type ty_var = string
type ty =
  1. | Ty_bool
  2. | Ty_app of ty_var * ty list
  3. | Ty_arrow of ty list * ty

Polymorphic types

type typed_var = var * ty
type term =
  1. | True
  2. | False
  3. | Const of string
  4. | App of string * term list
  5. | HO_app of term * term
  6. | Match of term * match_branch list
  7. | If of term * term * term
  8. | Let of (var * term) list * term
  9. | Fun of typed_var * term
  10. | Eq of term * term
  11. | Imply of term * term
  12. | And of term list
  13. | Or of term list
  14. | Not of term
  15. | Distinct of term list
  16. | Cast of term * ty
  17. | Forall of (var * ty) list * term
  18. | Exists of (var * ty) list * term

AST: S-expressions with locations

and match_branch =
  1. | Match_default of term
  2. | Match_case of string * var list * term
type cstor = {
  1. cstor_name : string;
  2. cstor_args : (string * ty) list;
}
type 'arg fun_decl = {
  1. fun_ty_vars : ty_var list;
  2. fun_name : string;
  3. fun_args : 'arg list;
  4. fun_ret : ty;
}
type fun_def = {
  1. fr_decl : typed_var fun_decl;
  2. fr_body : term;
}
type funs_rec_def = {
  1. fsr_decls : typed_var fun_decl list;
  2. fsr_bodies : term list;
}
type statement = {
  1. stmt : stmt;
  2. loc : Loc.t option;
}
and stmt =
  1. | Stmt_decl_sort of string * int
  2. | Stmt_decl of ty fun_decl
  3. | Stmt_fun_def of fun_def
  4. | Stmt_fun_rec of fun_def
  5. | Stmt_funs_rec of funs_rec_def
  6. | Stmt_data of ty_var list * (string * cstor list) list
  7. | Stmt_assert of term
  8. | Stmt_lemma of term
  9. | Stmt_assert_not of ty_var list * term
  10. | Stmt_check_sat
val ty_bool : ty
val ty_app : ty_var -> ty list -> ty
val ty_const : ty_var -> ty
val ty_arrow_l : ty list -> ty -> ty
val ty_arrow : ty -> ty -> ty
val true_ : term
val false_ : term
val const : string -> term
val app : string -> term list -> term
val ho_app : term -> term -> term
val ho_app_l : term -> term list -> term
val match_ : term -> match_branch list -> term
val if_ : term -> term -> term -> term
val fun_ : typed_var -> term -> term
val fun_l : typed_var list -> term -> term
val let_ : (var * term) list -> term -> term
val eq : term -> term -> term
val imply : term -> term -> term
val and_ : term list -> term
val or_ : term list -> term
val distinct : term list -> term
val cast : term -> ty:ty -> term
val forall : (var * ty) list -> term -> term
val exists : (var * ty) list -> term -> term
val not_ : term -> term
val _mk : ?loc:Loc.t -> stmt -> statement
val mk_cstor : string -> (string * ty) list -> cstor
val mk_fun_decl : ty_vars:ty_var list -> string -> 'a list -> ty -> 'a fun_decl
val mk_fun_rec : ty_vars:ty_var list -> string -> typed_var list -> ty -> term -> fun_def
val decl_sort : ?loc:Loc.t -> string -> arity:int -> statement
val decl_fun : ?loc:Loc.t -> tyvars:ty_var list -> string -> ty list -> ty -> statement
val fun_def : ?loc:Loc.t -> fun_def -> statement
val fun_rec : ?loc:Loc.t -> fun_def -> statement
val funs_rec : ?loc:Loc.t -> typed_var fun_decl list -> term list -> statement
val data : ?loc:Loc.t -> ty_var list -> (string * cstor list) list -> statement
val assert_ : ?loc:Loc.t -> term -> statement
val lemma : ?loc:Loc.t -> term -> statement
val assert_not : ?loc:Loc.t -> ty_vars:ty_var list -> term -> statement
val check_sat : ?loc:Loc.t -> unit -> statement
val loc : statement -> Loc.t option
val view : statement -> stmt
val fpf : Stdlib.Format.formatter -> ('a, Stdlib.Format.formatter, unit) Stdlib.format -> 'a
val pp_list : ?start:string -> ?stop:string -> ?sep:string -> (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> 'a list -> unit
val pp_tyvar : Stdlib.Format.formatter -> string -> unit
val pp_ty : Stdlib.Format.formatter -> ty -> unit
val pp_term : Stdlib.Format.formatter -> term -> unit
val pp_typed_var : Stdlib.Format.formatter -> typed_var -> unit
val pp_par : (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> (string list * 'a) -> unit
val pp_fun_decl : (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> 'a fun_decl -> unit
val pp_fr : Stdlib.Format.formatter -> fun_def -> unit
val pp_stmt : Stdlib.Format.formatter -> statement -> unit

Errors

exception Parse_error of Loc.t option * string
val parse_error : ?loc:Loc.t -> string -> 'a
val parse_errorf : ?loc:Loc.t -> ('a, unit, string, 'b) Stdlib.format4 -> 'a
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct