module Decl:sig
..end
Logic Declarations
typeconstructor =
Term.lsymbol * Term.lsymbol option list
constructor symbol with the list of projections
typedata_decl =
Ty.tysymbol * constructor list
type
ls_defn
typelogic_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.
type
call_set
type
vs_graph
val create_call_set : unit -> call_set
val create_vs_graph : Term.vsymbol list -> vs_graph
val register_call : call_set ->
Ident.ident -> vs_graph -> Ident.ident -> Term.term list -> unit
val vs_graph_drop : vs_graph -> Term.vsymbol -> vs_graph
val vs_graph_let : vs_graph -> Term.term -> Term.vsymbol -> vs_graph
val vs_graph_pat : vs_graph -> Term.term -> Term.pattern -> vs_graph
val find_variant : exn -> call_set -> Ident.ident -> int list
type
prsymbol = private {
|
pr_name : |
}
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
typeind_decl =
Term.lsymbol * (prsymbol * Term.term) list
type
ind_sign =
| |
Ind |
| |
Coind |
typeind_list =
ind_sign * ind_decl list
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 | *) |
typeprop_decl =
prop_kind * prsymbol * Term.term
type
decl = private {
|
d_node : |
|||
|
d_news : |
(* | idents introduced in declaration | *) |
|
d_tag : |
(* | unique magical tag | *) |
}
type
decl_node = private
| |
Dtype of |
(* | abstract types and aliases | *) |
| |
Ddata of |
(* | recursive algebraic types | *) |
| |
Dparam of |
(* | abstract functions and predicates | *) |
| |
Dlogic of |
(* | defined functions and predicates (possibly recursively) | *) |
| |
Dind of |
(* | (co)inductive predicates | *) |
| |
Dprop of |
(* | 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
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
val get_used_syms_ty : Ty.ty -> Ident.Sid.t
get_used_syms_ty ty
returns the set of identifiers used (i.e.,
assumed to be defined before) in ty
val get_used_syms_decl : decl -> Ident.Sid.t
get_used_syms_decl d
returns the set of identifiers used (i.e.,
assumed to be defined before) in d
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 BadRecordCons of Term.lsymbol * Ty.tysymbol
exception BadRecordType of Term.lsymbol * Ty.tysymbol
exception BadRecordUnnamed of Term.lsymbol * Ty.tysymbol
exception RecordFieldMissing of Term.lsymbol
exception DuplicateRecordField of Term.lsymbol
exception UnexpectedProjOrConstr of Term.lsymbol
val decl_map : (Term.term -> Term.term) -> decl -> decl
val decl_fold : ('a -> Term.term -> 'a) -> 'a -> decl -> 'a
open recursion style. Need a Why3.Term.fold for looking at subterms
val decl_map_fold : ('a -> Term.term -> 'a * Term.term) -> 'a -> decl -> 'a * decl
module DeclTF:sig
..end
typeknown_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
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