Module Decl

module Decl: sig .. end
Logic Declarations


Type declaration


type constructor = Term.lsymbol * Term.lsymbol option list 
constructor symbol with the list of projections
type data_decl = Ty.tysymbol * constructor list 

Logic symbols declaration


type ls_defn 
type logic_decl = Term.lsymbol * ls_defn 
val make_ls_defn : Term.lsymbol -> Term.vsymbol list -> Term.term -> logic_decl
val open_ls_defn : ls_defn -> Term.vsymbol list * Term.term
val open_ls_defn_cb : ls_defn ->
Term.vsymbol list * Term.term *
(Term.lsymbol -> Term.vsymbol list -> Term.term -> logic_decl)
val ls_defn_axiom : ls_defn -> Term.term
val ls_defn_of_axiom : Term.term -> logic_decl option
tries to reconstruct a definition from a defining axiom. Do not apply this to recursive definitions: it may successfully build a logic_decl, which will fail later because of non-assured termination
val ls_defn_decrease : ls_defn -> int list
ls_defn_decrease ld returns a list of argument positions (numbered from 0) that ensures a lexicographical structural descent for every recursive call. Triggers are ignored.

NOTE: This is only meaningful if the ls_defn comes from a declaration; on the result of make_ls_defn, ls_defn_decrease will always return an empty list.


Proposition names


type prsymbol = private {
   pr_name : Ident.ident;
}
module Mpr: Extmap.S  with type key = prsymbol
module Spr: Extset.S  with module M = Mpr
module Hpr: Exthtbl.S  with type key = prsymbol
module Wpr: Weakhtbl.S  with type key = prsymbol
val create_prsymbol : Ident.preid -> prsymbol
val pr_equal : prsymbol -> prsymbol -> bool
val pr_hash : prsymbol -> int

Inductive predicate declaration


type ind_decl = Term.lsymbol * (prsymbol * Term.term) list 
type ind_sign = 
| Ind
| Coind
type ind_list = ind_sign * ind_decl list 

Proposition declaration


type prop_kind = 
| Plemma (*
prove, use as a premise
*)
| Paxiom (*
do not prove, use as a premise
*)
| Pgoal (*
prove, do not use as a premise
*)
| Pskip (*
do not prove, do not use as a premise
*)
type prop_decl = prop_kind * prsymbol * Term.term 

Declaration type


type decl = private {
   d_node : decl_node;
   d_syms : Ident.Sid.t; (*
idents used in declaration
*)
   d_news : Ident.Sid.t; (*
idents introduced in declaration
*)
   d_tag : Weakhtbl.tag; (*
unique magical tag
*)
}
type decl_node = private 
| Dtype of Ty.tysymbol (*
abstract types and aliases
*)
| Ddata of data_decl list (*
recursive algebraic types
*)
| Dparam of Term.lsymbol (*
abstract functions and predicates
*)
| Dlogic of logic_decl list (*
defined functions and predicates (possibly recursively)
*)
| Dind of ind_list (*
(co)inductive predicates
*)
| Dprop of prop_decl (*
axiom / lemma / goal
*)
module Mdecl: Extmap.S  with type key = decl
module Sdecl: Extset.S  with module M = Mdecl
module Wdecl: Weakhtbl.S  with type key = decl
module Hdecl: Exthtbl.S  with type key = decl
val d_equal : decl -> decl -> bool
val d_hash : decl -> int

Declaration constructors


val create_ty_decl : Ty.tysymbol -> decl
val create_data_decl : data_decl list -> decl
val create_param_decl : Term.lsymbol -> decl
val create_logic_decl : logic_decl list -> decl
val create_ind_decl : ind_sign -> ind_decl list -> decl
val create_prop_decl : prop_kind -> prsymbol -> Term.term -> decl
exception IllegalTypeAlias of Ty.tysymbol
exception NonPositiveTypeDecl of Ty.tysymbol * Term.lsymbol * Ty.ty
exception InvalidIndDecl of Term.lsymbol * prsymbol
exception NonPositiveIndDecl of Term.lsymbol * prsymbol * Term.lsymbol
exception NoTerminationProof of Term.lsymbol
exception BadLogicDecl of Term.lsymbol * Term.lsymbol
exception UnboundVar of Term.vsymbol
exception ClashIdent of Ident.ident
exception EmptyDecl
exception EmptyAlgDecl of Ty.tysymbol
exception EmptyIndDecl of Term.lsymbol
exception BadConstructor of Term.lsymbol
exception BadRecordField of Term.lsymbol
exception RecordFieldMissing of Term.lsymbol * Term.lsymbol
exception DuplicateRecordField of Term.lsymbol * Term.lsymbol

Utilities


val decl_map : (Term.term -> Term.term) -> decl -> decl
val decl_fold : ('a -> Term.term -> 'a) -> 'a -> decl -> 'a
val decl_map_fold : ('a -> Term.term -> 'a * Term.term) -> 'a -> decl -> 'a * decl
module DeclTF: sig .. end

Known identifiers


type known_map = decl Ident.Mid.t 
val known_id : known_map -> Ident.ident -> unit
val known_add_decl : known_map -> decl -> known_map
val merge_known : known_map -> known_map -> known_map
exception KnownIdent of Ident.ident
exception UnknownIdent of Ident.ident
exception RedeclaredIdent of Ident.ident
exception NonFoundedTypeDecl of Ty.tysymbol
val find_constructors : known_map -> Ty.tysymbol -> constructor list
val find_inductive_cases : known_map -> Term.lsymbol -> (prsymbol * Term.term) list
val find_logic_definition : known_map -> Term.lsymbol -> ls_defn option
val find_prop : known_map -> prsymbol -> Term.term
val find_prop_decl : known_map -> prsymbol -> prop_kind * Term.term

Records


exception EmptyRecord
val parse_record : known_map ->
(Term.lsymbol * 'a) list -> Term.lsymbol * Term.lsymbol list * 'a Term.Mls.t
parse_record kn field_list takes a list of record field assignments, checks it for well-formedness and returns the corresponding constructor, the full list of projection symbols, and the map from projection symbols to assigned values.
val make_record : known_map -> (Term.lsymbol * Term.term) list -> Ty.ty -> Term.term
val make_record_update : known_map ->
Term.term -> (Term.lsymbol * Term.term) list -> Ty.ty -> Term.term
val make_record_pattern : known_map -> (Term.lsymbol * Term.pattern) list -> Ty.ty -> Term.pattern