package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
exception NoMatch of Term.term * Term.term
val remove_bp : Term.term -> Term.term
type construction =
  1. | Crigid of Term.vsymbol
  2. | Cbound of int
  3. | Cconst of Term.term
  4. | Capp of Term.lsymbol
  5. | Cif
  6. | Clet
  7. | Ccase of int
  8. | Ceps
  9. | Cquant of Term.quant * int
  10. | Cbinop of Term.binop
  11. | Cnot
module C : sig ... end
module MC : sig ... end
type ty_construction =
  1. | TyCrigid of Ty.tvsymbol
  2. | TyCapp of Ty.tysymbol
module Cty : sig ... end
module MCty : sig ... end
type pat_construction =
  1. | PatCwild
  2. | PatCvar
  3. | PatCapp of Term.lsymbol
  4. | PatCor
  5. | PatCas
module Cpat : sig ... end
module MCpat : sig ... end
type !'i instruction =
  1. | Fragment of 'i * construction
  2. | Store of 'i
  3. | FragmentPat of pat_construction
  4. | FragmentTy of 'i * ty_construction
  5. | StoreTv
  6. | Subst of Term.vsymbol
  7. | SubstTv of Ty.tvsymbol
  8. | Occurs of Term.vsymbol
  9. | Nop
module IL : sig ... end
module MIL : sig ... end
module Instr : sig ... end
module MInstr : sig ... end
type !'id code_point = {
  1. highest_id : 'id;
  2. straight_code : int list instruction list;
  3. branch : 'id code_branch;
}
and !'id code_branch =
  1. | Stop
  2. | Fork of 'id code_point MInstr.t
  3. | Switch of 'id code_point MIL.t MC.t
  4. | SwitchTy of 'id code_point MIL.t MCty.t
  5. | SwitchPat of 'id code_point MCpat.t
type !'id matching_state = {
  1. mutable term_stack : Term.term list;
  2. mutable match_stack : Term.term list;
  3. mutable ty_stack : Ty.ty list;
  4. mutable ty_match_stack : Ty.ty list;
  5. mutable pat_stack : Term.pattern list;
  6. mutable type_match : Ty.ty Ty.Mtv.t;
  7. mutable term_match : Term.term Term.Mvs.t;
  8. mutable bind_level : int;
  9. mutable bound_levels : int Term.Mvs.t;
  10. 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 : ('i -> 'i -> int) -> 'i code_point -> Ty.ty Ty.Mtv.t -> Term.term Term.Mvs.t -> Term.term -> ('i * 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
OCaml

Innovation. Community. Security.