psmt2-frontend 0.4.0 · OCaml Package

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 ->
  (Stdlib.Lexing.position * Stdlib.Lexing.position) option ->
  unit

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.ty

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.t

val check_if_dummy : 
  'a Smtlib_syntax.data ->
  'a Smtlib_syntax.data list ->
  'a Smtlib_syntax.data list

val check_if_escaped : 'a Smtlib_syntax.data list -> unit

val type_cst : Smtlib_syntax.constant -> 'a -> Smtlib_ty.ty

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.ty

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.t

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 list

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 list

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.ty

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.t

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
  * ('b
     * Smtlib_syntax.sort_aux Smtlib_syntax.data list
     * Smtlib_syntax.sort_aux Smtlib_syntax.data)

val assertion_stack : Smtlib_typed_env.env Stdlib.Stack.t

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

val typing : Smtlib_syntax.command_aux Smtlib_syntax.data list -> unit

package psmt2-frontend