package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Logtk.Compute_precSource

Compute Precedence

This module computes precedences that satisfy a list of constraints. See Precedence.Constr for more details on constraints.

Sourcetype t
Sourceval empty : t
Sourceval add_constr : int -> [ `partial ] Precedence.Constr.t -> t -> t

Add a precedence constraint with its priority. The lower the priority, the stronger influence the constraint will have.

Sourceval add_constrs : (int * [ `partial ] Precedence.Constr.t) list -> t -> t
Sourcetype 'a parametrized = Statement.clause_t Iter.t -> 'a

Some values are parametrized by the list of statements

Sourceval add_constr_rule : int -> [ `partial ] Precedence.Constr.t parametrized -> t -> t

Add a precedence constraint rule

Sourceval set_weight_rule : Precedence.weight_fun parametrized -> t -> t

Choose the way weights are computed

Sourceval add_status : (ID.t * Precedence.symbol_status) list -> t -> t

Specify explicitly the status of some symbols

Sourceval mk_precedence : db_w:int -> lmb_w:int -> t -> Statement.clause_t Iter.t -> Precedence.t

Parameters db_w and lmb_w correspond to the weight de-Bruijn and lambda abstraction given for computation of KBO.

Make a precedence