Something went wrong. Try again.
forked from gbury/dolmen
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250
(* This file is free software, part of dolmen. See file "LICENSE" for more information *)
(** {2 First-order View} *)
module Sexpr = struct (** This explicits a view of untyped terms as first-order terms/formulas *)
type _ view = | Symbol : 'id -> < id : 'id; .. > view | App : 'term list -> < term : 'term; .. > view
module type S = sig
type t type id
exception Not_an_sexpr of t
val view : t -> < id : id; term : t; > view
end
end
(** {2 First-order View} *)
module TFF = struct (** This explicits a view of terms as polymorphic first-order types and terms. In strict first-order, the distinction between types and terms is clear and useful enough that the view distinguishes the two. *)
module Sig = struct
type _ view = | Signature : 'ty_var list * 'ty list * 'ty -> < ty_var : 'ty_var; ty : 'ty; .. > view (** Function signature *) (** View of type signatures. *)
end
module Ty = struct
type _ view = | Var : 'ty_var -> < ty_var : 'ty_var; .. > view (**) | App : 'ty_cst * 'ty list -> < ty_cst : 'ty_cst; builtin : 'blt; ty : 'ty; .. > view (**) (** View of types in first-order. In first-order, types, which include basically variables and application of type constructors to types, are differentiated from type signatures, which include function types. *)
end
module TypeDef = struct
type _ algebraic_case = | Case : { constructor : 'term_cst; params : ('ty * 'term_cst) list; } -> < ty : 'ty; term_cst : 'term_cst > algebraic_case
type _ view = | Abstract : _ view | Algebraic : { vars : 'ty_var list; cases : < term_cst : 'term_cst; ty : 'ty; > algebraic_case list; } -> < ty : 'ty; ty_var : 'ty_var; term_cst : 'term_cst; > view
end
module Term = struct
type _ binder = | Exists : { type_vars : 'ty_var list; term_vars : 'term_var list; triggers : 'term list; } -> < ty_var : 'ty_var; term_var : 'term_var; term : 'term; .. > binder (** Existancial quantification *) | Forall : { type_vars : 'ty_var list; term_vars : 'term_var list; triggers : 'term list; } -> < ty_var : 'ty_var; term_var : 'term_var; term : 'term; .. > binder (** Universal quantification *) | Letin : ('term_var * 'term) list -> < term_var : 'term_var; term : 'term; .. > binder (** Sequential Let bindings *) | Letand : ('term_var * 'term) list -> < term_var : 'term_var; term : 'term; .. > binder (** Parallel Let bindings *) | Map : 'term_var list -> < term_var : 'term_var; .. > binder (** Maps: encoding of higher-order functions in first-order. *) (** First-order binders that can occur in terms. *)
type _ pattern = | Var : 'term_var -> < term_var : 'term_var; .. > pattern | Constructor : 'term_cst * 'term_var list -> < term_var : 'term_var; term_cst : 'term_cst; .. > pattern (**) (** First-order patterns. *)
type _ view = | Var : 'term_var -> < term_var : 'term_var; .. > view (** Term Variables*) | App : 'term_cst * 'ty list * 'term list -> < ty : 'ty; term : 'term; term_cst : 'term_cst; builtin : 'blt; .. > view (** Polymorphic application of a function symbol, with explicit type arguments *) | Match : 'term * ('t pattern * 'term) list -> (< term_var : 'term_var; term_cst : 'term_cst; term : 'term; .. > as 't) view (** Pattern matching. *) | Binder : < ty_var : 'ty_var; term_var : 'term_var; term : 'term; .. > binder * 'term -> < ty_var : 'ty_var; term_var : 'term_var; term : 'term; .. > view (** Binders over a body term. *) (** View of terms in first-order. *)
end
(* Aliases to avoid shadowing in the module type S below *) module Vty = Ty module VT = Term
(** The signature for a module that provides a first-order view of terms and types. *) module type S = sig
type ty type ty_var type ty_cst type ty_def type term type term_var type term_cst
type builtin = < ty : ty; ty_var : ty_var; ty_cst : ty_cst; term : term; term_var : term_var; term_cst : term_cst; > Builtin.t (** builtin symbols *)
module Ty : sig
type t = ty
module Var : sig
type t = ty_var
end
module Cst : sig
type t = ty_cst
val arity : t -> int
val builtin : t -> builtin
end
module Def : sig
type t = ty_def
val view : expand:bool -> t -> < ty : ty; ty_var : ty_var; term_cst : term_cst > TypeDef.view
end
exception Not_first_order of t (** exceptions raised by view functions on types that cannot be represented as first-order. *)
val view : expand:bool -> t -> < ty_var : Var.t; ty_cst : Cst.t; builtin : builtin; ty : t; .. > Ty.view (** View function for types. @raise Not_first_order_ty if the type cannot be viewed as first-order. *)
end
module Sig : sig
type t
val view : expand:bool -> t -> < ty_var : Ty.Var.t; ty : Ty.t; .. > Sig.view
end
module Term : sig
type t = term
val equal : t -> t -> bool
module Var : sig
type t = term_var
val ty : t -> Ty.t
val equal : t -> t -> bool
end
module Cst : sig
type t = term_cst
val ty : t -> Sig.t
val builtin : t -> builtin
val hash : t -> int
val equal : t -> t -> bool end
exception Not_first_order of t (** exceptions raised by view functions on terms that cannot be represented as first-order. *)
val ty : t -> Ty.t (** Return the type of a term. *)
val view : t -> < ty_var: Ty.Var.t; term_var: Var.t; term_cst : Cst.t; builtin : builtin; ty : Ty.t; term : t; .. > Term.view (** View function for terms. @raise Not_first_order_term if the term cannot be viewed as first-order. *)
end
end
end