Previous  Up  Next

Module Statement

module Statement: sig .. end

Top-level statement


type id = ID.t 
type loc = Location.t 
type 'a var = 'a Var.t 
type 'a printer = Format.formatter -> 'a -> unit 
type 'ty defined = {
   defined_head : id;
   defined_ty : 'ty;
} 
type ('t, 'ty) equations =
| Eqn_nested of ('ty var list * 't list * 't * 't list) list
| Eqn_single of 'ty var list * 't
| Eqn_app of ID.t list * 'ty var list * 't * 't 
type ('t, 'ty) rec_def = {
   rec_defined : 'ty defined;
   rec_ty_vars : 'ty var list;
   rec_eqns : ('t, 'ty) equations;
} 
type ('t, 'ty) rec_defs = ('t, 'ty) rec_def list 
type ('t, 'ty) spec_defs = {
   spec_ty_vars : 'ty var list;
   spec_defined : 'ty defined list;
   spec_axioms : 't list;
} 
type 'ty ty_constructor = {
   cstor_name : id; (*
Name
*)
   cstor_args : 'ty list; (*
type arguments
*)
   cstor_type : 'ty; (*
type of the constructor (shortcut)
*)
}
A type constructor: name + type of arguments
type 'ty tydef = {
   ty_id : id;
   ty_vars : 'ty Var.t list;
   ty_type : 'ty; (*
shortcut for type -> type -> ... -> type
*)
   ty_cstors : 'ty ty_constructor ID.Map.t;
}
A (co)inductive type. The type variables ty_vars occur freely in the constructors' types.
type 'ty mutual_types = 'ty tydef list
Mutual definitions of several types
type ('t, 'ty) axiom =
| Axiom_std of 't list (*
Axiom list that can influence consistency (no assumptions)
*)
| Axiom_spec of ('t, 'ty) spec_defs (*
Axioms can be safely ignored, they are consistent
*)
| Axiom_rec of ('t, 'ty) rec_defs (*
Axioms are part of an admissible (partial) definition
*)
Flavour of axiom
type ('t, 'ty) pred_clause = {
   clause_vars : 'ty var list;
   clause_guard : 't option;
   clause_concl : 't;
} 
type ('t, 'ty) pred_def = {
   pred_defined : 'ty defined;
   pred_tyvars : 'ty var list;
   pred_clauses : ('t, 'ty) pred_clause list;
} 
type 't copy_wrt =
| Wrt_nothing
| Wrt_subset of 't
| Wrt_quotient of [ `Partial | `Total ] * 't 
type ('t, 'ty) copy = {
   copy_id : ID.t;
   copy_vars : 'ty Var.t list;
   copy_ty : 'ty;
   copy_of : 'ty;
   copy_to : 'ty;
   copy_wrt : 't copy_wrt;
   copy_abstract : ID.t;
   copy_abstract_ty : 'ty;
   copy_concrete : ID.t;
   copy_concrete_ty : 'ty;
} 
type decl_attr =
| Attr_card_max of int (*
maximal cardinality of type
*)
| Attr_card_min of int (*
minimal cardinality of type
*)
| Attr_card_hint of Cardinality.t (*
hint on the card of a type
*)
| Attr_incomplete (*
encoding of some type with some values removed
*)
| Attr_abstract (*
encoding of some type where some values are conflated
*)
| Attr_infinite (*
infinite uninterpreted type
*)
| Attr_finite_approx of ID.t (*
finite approximation of an infinite type
*)
| Attr_infinite_upcast (*
cast finite approx to infinite type
*)
| Attr_pseudo_prop (*
encoding of prop
*)
| Attr_pseudo_true (*
encoding of true_ : pseudo_prop
*)
| Attr_exn of exn (*
open case
*)
Attribute on declarations
type ('term, 'ty) view =
| Decl of id * 'ty * decl_attr list
| Axiom of ('term, 'ty) axiom
| TyDef of [ `Codata | `Data ] * 'ty mutual_types
| Pred of [ `Not_wf | `Wf ] * [ `Copred | `Pred ]
* ('term, 'ty) pred_def list
| Copy of ('term, 'ty) copy
| Goal of 'term 
type info = {
   loc : loc option;
   name : string option;
}
Additional informations on the statement
type ('term, 'ty) t = private {
   view : ('term, 'ty) view;
   info : info;
} 
type ('t, 'ty) statement = ('t, 'ty) t 
val mk_defined : ID.t -> 'ty -> 'ty defined
val tydef_vars : 'ty tydef -> 'ty Var.t list
val tydef_id : 'a tydef -> id
val tydef_type : 'ty tydef -> 'ty
val tydef_cstors : 'ty tydef -> 'ty ty_constructor ID.Map.t
val info_default : info
val info_of_loc : Location.t option -> info
val view : ('term, 'ty) t -> ('term, 'ty) view
val loc : ('a, 'b) t -> loc option
val name : ('a, 'b) t -> string option
val info : ('a, 'b) t -> info
val mk_axiom : info:info -> ('a, 'ty) axiom -> ('a, 'ty) t
val mk_ty_def : info:info ->
       [ `Codata | `Data ] -> 'ty mutual_types -> ('a, 'ty) t
val decl : info:info ->
       attrs:decl_attr list -> id -> 'a -> ('b, 'a) t
declare a type/function/predicate
val axiom : info:info -> 'a list -> ('a, 'b) t
Axioms without additional assumptions
val axiom1 : info:info -> 'a -> ('a, 'b) t
val axiom_spec : info:info -> ('a, 'ty) spec_defs -> ('a, 'ty) t
Axiom that can be ignored if not explicitely depended upon by the goal
val axiom_rec : info:info -> ('a, 'ty) rec_defs -> ('a, 'ty) t
Axiom that is part of an admissible (mutual, partial) definition.
val data : info:info -> 'ty mutual_types -> ('a, 'ty) t
val codata : info:info -> 'ty mutual_types -> ('a, 'ty) t
val pred : info:info ->
       wf:[ `Not_wf | `Wf ] ->
       ('t, 'ty) pred_def list -> ('t, 'ty) t
val copred : info:info ->
       wf:[ `Not_wf | `Wf ] ->
       ('t, 'ty) pred_def list -> ('t, 'ty) t
val mk_pred : info:info ->
       wf:[ `Not_wf | `Wf ] ->
       [ `Copred | `Pred ] ->
       ('t, 'ty) pred_def list -> ('t, 'ty) t
val copy : info:info -> ('t, 'ty) copy -> ('t, 'ty) t
val goal : info:info -> 'a -> ('a, 'b) t
The goal of the problem
val mk_mutual_ty : ID.t ->
       ty_vars:'ty Var.t list ->
       cstors:(ID.t * 'ty list * 'ty) list -> ty:'ty -> 'ty tydef
Constructor for Statement.tydef
val mk_copy : wrt:'t copy_wrt ->
       of_:'ty ->
       to_:'ty ->
       ty:'ty ->
       abstract:ID.t * 'ty ->
       concrete:ID.t * 'ty ->
       vars:'ty Var.t list -> ID.t -> ('t, 'ty) copy
Invariants: to_ = app id vars snd abstract = of_ -> to_ snd concrete = to_ -> of_
val find_rec_def : defs:('a, 'b) rec_def list ->
       ID.t -> ('a, 'b) rec_def option
val find_tydef : defs:'a tydef list -> ID.t -> 'a tydef option
val find_pred : defs:('a, 'b) pred_def list ->
       ID.t -> ('a, 'b) pred_def option
val map_defined : f:('ty -> 'ty2) -> 'ty defined -> 'ty2 defined
val map_eqns : term:('t -> 't2) ->
       ty:('ty -> 'ty2) ->
       ('t, 'ty) equations -> ('t2, 'ty2) equations
val map_eqns_bind : bind:('acc -> 'ty Var.t -> 'acc * 'ty1 Var.t) ->
       term:('acc -> 'term -> 'term1) ->
       'acc ->
       ('term, 'ty) equations -> ('term1, 'ty1) equations
val map_clause : term:('t -> 't2) ->
       ty:('ty -> 'ty2) ->
       ('t, 'ty) pred_clause -> ('t2, 'ty2) pred_clause
val map_clause_bind : bind:('acc -> 'ty Var.t -> 'acc * 'ty1 Var.t) ->
       term:('acc -> 'term -> 'term1) ->
       'acc ->
       ('term, 'ty) pred_clause -> ('term1, 'ty1) pred_clause
val map_rec_def : term:('t -> 't2) ->
       ty:('ty -> 'ty2) ->
       ('t, 'ty) rec_def -> ('t2, 'ty2) rec_def
val map_rec_def_bind : bind:('a -> 'b Var.t -> 'a * 'c Var.t) ->
       term:('a -> 'd -> 'e) ->
       ty:('a -> 'b -> 'c) ->
       'a -> ('d, 'b) rec_def -> ('e, 'c) rec_def
val map_rec_defs : term:('t -> 't2) ->
       ty:('ty -> 'ty2) ->
       ('t, 'ty) rec_defs -> ('t2, 'ty2) rec_defs
val map_ty_def : ty:('ty -> 'ty2) -> 'ty tydef -> 'ty2 tydef
val map_ty_defs : ty:('ty -> 'ty2) -> 'ty mutual_types -> 'ty2 mutual_types
val map_spec_defs : term:('t -> 't2) ->
       ty:('ty -> 'ty2) ->
       ('t, 'ty) spec_defs -> ('t2, 'ty2) spec_defs
val map_spec_defs_bind : bind:('b_acc -> 'ty Var.t -> 'b_acc * 'ty2 Var.t) ->
       term:('b_acc -> 't -> 't2) ->
       ty:('b_acc -> 'ty -> 'ty2) ->
       'b_acc -> ('t, 'ty) spec_defs -> ('t2, 'ty2) spec_defs
val map_pred : term:('a -> 'a1) ->
       ty:('b -> 'b1) ->
       ('a, 'b) pred_def -> ('a1, 'b1) pred_def
val map_pred_bind : bind:('acc -> 'ty Var.t -> 'acc * 'ty2 Var.t) ->
       term:('acc -> 'term -> 'term2) ->
       ty:('acc -> 'ty -> 'ty2) ->
       'acc -> ('term, 'ty) pred_def -> ('term2, 'ty2) pred_def
val map_preds : term:('a -> 'a1) ->
       ty:('b -> 'b1) ->
       ('a, 'b) pred_def list -> ('a1, 'b1) pred_def list
val map_copy_wrt : ('a -> 'b) -> 'a copy_wrt -> 'b copy_wrt
val map_copy_bind : bind:('a -> 'b var -> 'a * 'c var) ->
       term:('a -> 'd -> 'e) ->
       ty:('a -> 'b -> 'c) ->
       'a -> ('d, 'b) copy -> ('e, 'c) copy
val map_copy : term:('t1 -> 't2) ->
       ty:('ty1 -> 'ty2) -> ('t1, 'ty1) copy -> ('t2, 'ty2) copy
val map : term:('t -> 't2) ->
       ty:('ty -> 'ty2) -> ('t, 'ty) t -> ('t2, 'ty2) t
val map_bind : bind:('b_acc -> 'ty Var.t -> 'b_acc * 'ty2 Var.t) ->
       term:('b_acc -> 't -> 't2) ->
       ty:('b_acc -> 'ty -> 'ty2) ->
       'b_acc -> ('t, 'ty) t -> ('t2, 'ty2) t
Similar to Statement.map, but accumulating some value of type b_acc when entering binders
val fold_bind : bind:('b_acc -> 'ty Var.t -> 'b_acc) ->
       term:('b_acc -> 'a -> 't -> 'a) ->
       ty:('b_acc -> 'a -> 'ty -> 'a) -> 'b_acc -> 'a -> ('t, 'ty) t -> 'a
val fold : term:('a -> 't -> 'a) ->
       ty:('a -> 'ty -> 'a) -> 'a -> ('t, 'ty) t -> 'a
val iter : term:('t -> unit) -> ty:('ty -> unit) -> ('t, 'ty) t -> unit
val id_of_defined : 'a defined -> ID.t
val ty_of_defined : 'ty defined -> 'ty
val defined_of_rec : ('a, 'ty) rec_def -> 'ty defined
val defined_of_recs : ('a, 'ty) rec_defs -> 'ty defined Sequence.t
val defined_of_spec : ('a, 'ty) spec_defs -> 'ty defined Sequence.t
val defined_of_pred : ('a, 'ty) pred_def -> 'ty defined
val defined_of_preds : ('a, 'ty) pred_def list -> 'ty defined Sequence.t
val defined_of_cstor : 'ty ty_constructor -> 'ty defined
val defined_of_data : 'ty tydef -> 'ty defined Sequence.t
val defined_of_datas : 'ty mutual_types -> 'ty defined Sequence.t
val defined_of_copy : ('a, 'ty) copy -> 'ty defined Sequence.t
val ids_of_copy : ('a, 'b) copy -> ID.t Sequence.t

Print


val print_attr : decl_attr printer
val print_attrs : decl_attr list printer
module Print (Pt : TermInner.PRINT)  (Pty : TermInner.PRINT) : sig .. end