Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Page
Library
Module
Module type
Parameter
Class
Class type
Source
package psmt2-frontend
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Module Psmt2Frontend.Smtlib_typingSource
Source
val inst_and_unify :
('a * Smtlib_ty.ty Smtlib_ty.SMap.t) ->
Smtlib_ty.ty Smtlib_ty.IMap.t ->
Smtlib_ty.ty ->
Smtlib_ty.ty ->
(Lexing.position * Lexing.position) option ->
unitSource
val find_par_ty :
(Smtlib_typed_env.env * Smtlib_ty.ty Smtlib_typed_env.SMap.t) ->
Smtlib_typed_env.SMap.key Smtlib_syntax.data ->
Smtlib_ty.ty list ->
string list ->
Smtlib_ty.tySource
val find_pattern :
(Smtlib_typed_env.env * Smtlib_ty.ty Smtlib_typed_env.SMap.t) ->
Smtlib_typed_env.SMap.key Smtlib_syntax.data ->
Smtlib_ty.ty list ->
string list ->
bool ->
Smtlib_ty.ty * Smtlib_ty.ty Smtlib_typed_env.SMap.tSource
val check_if_dummy :
'a Smtlib_syntax.data ->
'a Smtlib_syntax.data list ->
'a Smtlib_syntax.data listSource
val type_qualidentifier :
(Smtlib_typed_env.env * Smtlib_ty.ty Smtlib_typed_env.SMap.t) ->
Smtlib_syntax.qualidentifier_aux Smtlib_syntax.data ->
Smtlib_ty.ty list ->
Smtlib_ty.tySource
val type_match_case :
(Smtlib_typed_env.env
* Smtlib_ty.ty Smtlib_typed_env.SMap.t
* Smtlib_syntax.term_aux Smtlib_syntax.data list
* int Smtlib_typed_env.SMap.t) ->
Smtlib_ty.ty ->
(Smtlib_syntax.pattern_aux Smtlib_syntax.data
* Smtlib_syntax.term_aux Smtlib_syntax.data) ->
int Smtlib_typed_env.SMap.t ->
Smtlib_ty.ty
* Smtlib_syntax.term_aux Smtlib_syntax.data list
* int Smtlib_typed_env.SMap.tSource
val type_key_term :
(Smtlib_typed_env.env
* Smtlib_ty.ty Smtlib_typed_env.SMap.t
* Smtlib_syntax.term_aux Smtlib_syntax.data list) ->
Smtlib_syntax.key_term_aux Smtlib_syntax.data ->
Smtlib_syntax.term_aux Smtlib_syntax.data listSource
val type_term :
(Smtlib_typed_env.env
* Smtlib_ty.ty Smtlib_typed_env.SMap.t
* Smtlib_syntax.term_aux Smtlib_syntax.data list) ->
Smtlib_syntax.term_aux Smtlib_syntax.data ->
Smtlib_ty.ty * Smtlib_syntax.term_aux Smtlib_syntax.data listSource
val get_term :
(Smtlib_typed_env.env * Smtlib_ty.ty Smtlib_typed_env.SMap.t) ->
Smtlib_typed_env.SMap.key Smtlib_syntax.data list ->
Smtlib_syntax.term_aux Smtlib_syntax.data ->
Smtlib_ty.tySource
val get_sorted_locals :
(Smtlib_typed_env.env * Smtlib_ty.ty Smtlib_typed_env.SMap.t) ->
(Smtlib_typed_env.SMap.key Smtlib_syntax.data
* Smtlib_syntax.sort_aux Smtlib_syntax.data)
list ->
Smtlib_ty.ty Smtlib_typed_env.SMap.tSource
val get_fun_def_locals :
(Smtlib_typed_env.env * Smtlib_ty.ty Smtlib_typed_env.SMap.t) ->
('a
* Smtlib_typed_env.SMap.key Smtlib_syntax.data list
* (Smtlib_typed_env.SMap.key Smtlib_syntax.data
* Smtlib_syntax.sort_aux Smtlib_syntax.data)
list
* Smtlib_syntax.sort_aux Smtlib_syntax.data) ->
Smtlib_ty.ty Smtlib_typed_env.SMap.t
* Smtlib_ty.ty
* ('a
* Smtlib_syntax.sort_aux Smtlib_syntax.data list
* Smtlib_syntax.sort_aux Smtlib_syntax.data)Source
val type_command :
(Smtlib_typed_env.env * Smtlib_ty.ty Smtlib_typed_env.SMap.t) ->
Smtlib_syntax.command_aux Smtlib_syntax.data ->
Smtlib_typed_env.env