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.

Structural descent checking

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

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	`*)`

type prop_decl = prop_kind * prsymbol * Term.term

Declaration type

type decl = private {

`d_node : decl_node;`
`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

Used symbols

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

Exceptions

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

Utilities

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

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