package dedukti

You can search for identifiers within the package.

in-package search v0.2.0

package dedukti

dedukti.api
- Api
  - Dep
  - Env
  - Errors
  - Files
  - Meta
    
    APP
    
    ENCODING
    
    LF
    
    MetaConfiguration
    
    PROD
  - Pp
    
    Default
    
    Make
    
    S
    
    Printer
    
    Sig
  - Processor
    
    CustomEnv
    
    Interface
    
    MakeDependencies
    
    E
    
    MakeEntryPrinter
    
    E
    
    MakeSignatureBuilder
    
    E
    
    MakeTypeChecker
    
    E
    
    Registration
    
    S
    
    T
dedukti.kernel
- Kernel
  - Ac
  - Basic
    
    Debug
    
    LList
  - Confluence
  - Dtree
  - Exsubst
    
    ExSubst
  - Matching
    
    Make
    
    R
    
    Matcher
    
    Reducer
  - Reduction
    
    ConvChecker
    
    Default
    
    Make
    
    C
    
    M
    
    S
  - Rule
  - Signature
  - Srcheck
    
    SRChecker
    
    R
  - Subst
  - Term
  - Typing
    
    Default
    
    Make
    
    R
    
    S
  - Version
dedukti.parsers
- Parsers
  - Entry
  - Lexer
  - Menhir_parser
  - Parser
  - Preterm
  - Scoping
  - Tokens

Legend:
Library
Module
Module type
Parameter
Class
Class type

Term reduction and conversion test.

val d_reduce : Basic.Debug.flag

type red_target =

| Snf
| Whnf

type red_strategy =

| ByName
| ByValue
| ByStrongValue

type dtree_finder = Signature.t -> Basic.loc -> Basic.name -> Dtree.t

type red_cfg = {

select : (Rule.rule_name -> bool) option;
nb_steps : int option;
target : red_target;
strat : red_strategy;
beta : bool;
logger : Term.position -> Rule.rule_name -> Term.term Stdlib.Lazy.t -> Term.term Stdlib.Lazy.t -> unit;
finder : dtree_finder;

}

Configuration for reduction. select = Some f restreins rules according to the given filter on names. select = None is the default behaviour (all rules allowed). nb_steps = Some n Allows only n reduction steps. nb_steps = None is the default behaviour. target is the normal form to compute. strat is the reduction strategy. beta flag enables/disables beta reductions. logger is the function to call upon applying a reduction rule. finder specifies where to find the decision tree.

val pp_red_cfg : red_cfg Basic.printer

val default_cfg : red_cfg

default configuration where:

select = None
nb_steps = None
strategy = ByName
target = Snf
beta = true
logger = fun _ _ _ -> ()
finder = Signature.get_dtree

val eta : bool Stdlib.ref

Set to true to allow eta expansion at conversion check

exception Not_convertible

type convertibility_test = Signature.t -> Term.term -> Term.term -> bool

val selection : (Rule.rule_name -> bool) option Stdlib.ref

This predicate restrict the rules which can be used by the rewrite engine. Default is None meaning that every rules in Signature are used

module type ConvChecker = sig ... end

module type S = sig ... end

module Make (C : ConvChecker) (M : Matching.Matcher) : S

module Default : S