package zelus

  1. Overview
  2. Docs
package zelus
Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

module S : SIG

Signature

module SSet : sig ... end
val uniq : SSet.elt list -> SSet.elt list
val is_complete : SSet.elt list -> bool
val not_in : SSet.elt list -> S.tag
val head_constrs : 'a pattern -> ('b * int) list

Extract constructors from pattern.

val matS : S.tag -> int -> S.tag pattern list list -> S.tag pattern list list

Implementation of S(c,p) as described in the paper's first part.

val matD : 'a pattern list list -> 'a pattern list list

Implementation of D(p) as described in the paper's first part.

val algU : SSet.elt pattern list list -> S.tag pattern list -> bool

U(p,q) from the paper. Most important function, called by higher level ones. Tests the usefulness of q relatively to p.

type 'a trivec = {
  1. p : 'a patt_vec;
  2. q : 'a patt_vec;
  3. r : 'a patt_vec;
}

Type used for efficient testing of usefulness and redundancy of pattern-matching cases.

and 'a trimat = 'a trivec list
val trimatS : S.tag -> int -> S.tag trivec list -> S.tag trivec list

Second de finition of S(c,p) for tri-matrices.

val shift1 : 'a trivec -> 'b trivec

shift1 l shifts an element from l.p to l.q.

val shift2 : 'a trivec -> 'b trivec

shift2 l shifts an element from l.p to l.r.

S.tag pattern list option is used for results of usefulness testing for Or(r1,r2) patterns. Some means that r1 and r2 are both useful, Some r1 (resp. Some r2) means that r1 (resp. r2) is useless, and None means that both are.

The following functions implement useful shortcuts.

val simple_union : 'a list option -> 'a list option -> 'a list option
val union : 'a -> 'b -> 'c list option -> 'c list option -> 'c list option
val algU' : SSet.elt trivec list -> SSet.elt trivec -> S.tag pattern list option

Efficient usefulness check with special Or pattern management.

val algI : SSet.elt pattern list list -> int -> SSet.elt pattern list option

Completely construct a non-matched pattern. If none is returned, this matrix is exhaustive.

type result = {
  1. not_matched : S.pattern_ast option;
  2. redundant_patterns : S.pattern_ast list;
}
val check : S.pattern_ast list -> result