why3 1.0.0 · OCaml Package

exception NoMatch of Term.term * Term.term

val remove_bp : Term.term -> Term.term

val matching : 
  Ty.ty Ty.Mtv.t ->
  Term.term Term.Mvs.t ->
  Term.term ->
  Term.term ->
  Ty.ty Ty.Mtv.t * Term.term Term.Mvs.t

type construction =

| Crigid of Term.vsymbol
| Cbound of int
| Cconst of Term.term
| Capp of Term.lsymbol
| Cif
| Clet
| Ccase of int
| Ceps
| Cquant of Term.quant * int
| Cbinop of Term.binop
| Cnot

module C : sig ... end

module MC : sig ... end

type ty_construction =

| TyCrigid of Ty.tvsymbol
| TyCapp of Ty.tysymbol

module Cty : sig ... end

module MCty : sig ... end

type pat_construction =

| PatCwild
| PatCvar
| PatCapp of Term.lsymbol
| PatCor
| PatCas

module Cpat : sig ... end

module MCpat : sig ... end

type !'i instruction =

| Fragment of 'i * construction
| Store of 'i
| FragmentPat of pat_construction
| FragmentTy of 'i * ty_construction
| StoreTv
| Subst of Term.vsymbol
| SubstTv of Ty.tvsymbol
| Occurs of Term.vsymbol
| Nop

module IL : sig ... end

module MIL : sig ... end

module Instr : sig ... end

module MInstr : sig ... end

type !'id code_point = {

highest_id : 'id;
straight_code : int list instruction list;
branch : 'id code_branch;

}

and !'id code_branch =

| Stop
| Fork of 'id code_point MInstr.t
| Switch of 'id code_point MIL.t MC.t
| SwitchTy of 'id code_point MIL.t MCty.t
| SwitchPat of 'id code_point MCpat.t

type !'id matching_state = {

mutable term_stack : Term.term list;
mutable match_stack : Term.term list;
mutable ty_stack : Ty.ty list;
mutable ty_match_stack : Ty.ty list;
mutable pat_stack : Term.pattern list;
mutable type_match : Ty.ty Ty.Mtv.t;
mutable term_match : Term.term Term.Mvs.t;
mutable bind_level : int;
mutable bound_levels : int Term.Mvs.t;
code_loc : 'id code_point;

}

val ms_bind : 'a matching_state -> Term.Mvs.key -> unit

val drop : 'a matching_state -> ('b -> Ty.ty) -> 'b list -> int list -> unit

val ms_tyl : 'a matching_state -> Ty.ty list -> int list -> unit

val ms_quant : 
  'a matching_state ->
  Term.Mvs.key list ->
  Term.term ->
  int list ->
  unit

val add_dty : 'a matching_state -> Term.term -> 'b list -> unit

val instr : 'a matching_state -> int list instruction -> bool

val instrs : 'a matching_state -> int list instruction list -> bool

val run_match : 
  ('a -> 'a -> int) ->
  'a code_point ->
  Ty.ty Ty.Mtv.t ->
  Term.term Term.Mvs.t ->
  Term.term ->
  ('a * Ty.ty Ty.Mtv.t * Term.term Term.Mvs.t) option

val _fragment : 'a list instruction

val _fragment_ty : 'a list instruction

val _fragment_pat : 'a instruction

val id_branch : 'a code_branch -> 'b list instruction

val sw_fragment : MIL.key -> MC.key -> 'a -> 'a MIL.t MC.t

val sw_fragment_ty : MIL.key -> MCty.key -> 'a -> 'a MIL.t MCty.t

val sw_fragment_pat : MCpat.key -> 'a -> 'a MCpat.t

val join_code_points : 
  ('a -> 'a -> int) ->
  'a code_point ->
  'a code_point ->
  'a code_point

module TyG : sig ... end

val compile : 'a -> 'b Ty.Mtv.t -> 'c Term.Mvs.t -> Term.term -> 'a code_point

package why3