package acgtk

You can search for identifiers within the package.

in-package search v0.2.0

package acgtk

acgtk
- Library acgtkLib.acgData
  - AcgData
    
    Acg_lexicon
    
    Data_Lexicon
    
    Signature
    
    Environment
    
    Environment_sig
    
    Signature1
    
    Lexicon
    
    Signature
    
    Environment
    
    Signature1
    
    Lexicon
    
    Signature
    
    Error
    
    Interface
    
    Signature_sig
    
    Lexicon_sig
    
    Signature
    
    Reduction
    
    Make
    
    Signature
    
    Data_Signature
    
    Type_system
    
    SIG_ACCESS
    
    Type_System
    
    Make
- Library acgtkLib.datalogLib
  - DatalogLib
    
    ArrayTraversal
    
    Evaluator_TYPE
    
    Make
    
    Evaluator_TYPE2
    
    CellSet
    
    Make2
    
    Datalog
    
    ASPred
    
    PredIdMap
    
    PredIdTable
    
    PredIds
    
    ASRule
    
    Rules
    
    RuleMap
    
    ASProg
    
    Datalog_Sig
    
    UF
    
    Predicate
    
    PredMap
    
    FactSet
    
    PredicateMap
    
    Premise
    
    PremiseSet
    
    Rule
    
    FactArray
    
    Rules
    
    Program
    
    Make
    
    UF
    
    Predicate
    
    PredMap
    
    FactSet
    
    PredicateMap
    
    Premise
    
    PremiseSet
    
    Rule
    
    FactArray
    
    Rules
    
    Program
    
    Datalog
    
    UF
    
    Predicate
    
    PredMap
    
    FactSet
    
    PredicateMap
    
    Premise
    
    PremiseSet
    
    Rule
    
    FactArray
    
    Rules
    
    Program
    
    Datalog_AbstractSyntax
    
    VarGen
    
    IdMap
    
    Table
    
    ConstGen
    
    IdMap
    
    Table
    
    AbstractSyntax
    
    Predicate
    
    PredIdMap
    
    PredIdTable
    
    PredIds
    
    Proto_Rule
    
    Rule
    
    Rules
    
    RuleMap
    
    Proto_Program
    
    Program
    
    Db_lexer
    
    Db_parser
    
    DlError
    
    E
    
    Error
    
    Dl_lexer
    
    Dl_parse_functions
    
    Dl_parser
    
    MenhirInterpreter
    
    Incremental
    
    Messages
    
    PersistentArray
    
    PersistentArray
    
    UnionFind
    
    S
    
    Store
    
    Make
    
    StoreAsMap
- Library acgtkLib.logic
  - Logic
    
    Abstract_syntax
    
    Abstract_syntax
    
    Lambda
    
    Lambda
    
    TypeInference
    
    Type
    
    VarUnionFind
    
    UF
- Library acgtkLib.utilsLib
  - UtilsLib
    
    DependencyManager
    
    Manager_sig
    
    Make
    
    ErrorMg
    
    E
    
    ERROR
    
    Make
    
    Focused_list
    
    Focused_list
    
    IdGenerator
    
    CorrespondanceTableTYPE
    
    IdGen_TYPE
    
    IdMap
    
    Table
    
    IdType
    
    IdGen
    
    IdMap
    
    Table
    
    IntIdGen
    
    IdMap
    
    Table
    
    Log
    
    SharedForest
    
    SharedForest
    
    Log
    
    Table
    
    BASE
    
    TABLE
    
    Make_table
    
    Tries
    
    Tries
    
    Utils
    
    StringSet
    
    StringMap
    
    IntMap
    
    IntSet
    
    Version
    
    Warnings
- Sources
  - acgtkLib.acgData
    
    acgData.ml
    
    acg_lexicon.ml
    
    environment.ml
    
    error.ml
    
    interface.ml
    
    reduction.ml
    
    signature.ml
    
    type_system.ml
  - acgtkLib.datalogLib
    
    arrayTraversal.ml
    
    datalog.ml
    
    datalogLib.ml
    
    datalog_AbstractSyntax.ml
    
    db_lexer.ml
    
    db_parser.ml
    
    dlError.ml
    
    dl_lexer.ml
    
    dl_parse_functions.ml
    
    dl_parser.ml
    
    messages.ml
    
    persistentArray.ml
    
    unionFind.ml
  - acgtkLib.logic
    
    abstract_syntax.ml
    
    lambda.ml
    
    logic.ml
    
    typeInference.ml
    
    varUnionFind.ml
  - acgtkLib.utilsLib
    
    dependencyManager.ml
    
    errorMg.ml
    
    focused_list.ml
    
    idGenerator.ml
    
    log.ml
    
    sharedForest.ml
    
    table.ml
    
    tries.ml
    
    utils.ml
    
    utilsLib.ml
    
    version.ml
    
    warnings.ml

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Lambda.Lambda`Source

Sourcetype kind =

| Type
| Depend of stype * kind

Sourceand stype =

| Atom of int
| DAtom of int
| LFun of stype * stype
| Fun of stype * stype
| Dprod of string * stype * stype
| Record of int * stype list
| Variant of int * stype list
| TAbs of string * stype
| TApp of stype * term

Sourceand term =

| Var of int
| LVar of int
| Const of int
| DConst of int
| Abs of string * term
| LAbs of string * term
| App of term * term
| Rcons of int * term list
| Proj of int * int * term
| Vcons of int * int * term
| Case of int * term * (string * term) list
| Unknown of int

Sourcetype env = (int * string) list

Source

type consts =
  int ->
  Abstract_syntax.Abstract_syntax.syntactic_behavior * string

Sourceval env_to_string : env -> string

Sourceval generate_var_name : string -> (env * env) -> string

Sourceval unfold_labs : env -> int -> (env * env) -> term -> env * int * term

Sourceval unfold_abs : env -> int -> (env * env) -> term -> env * int * term

Sourceval unfold_app : term list -> term -> term list * term

Sourceval is_binder : int -> consts -> bool

Sourceval is_infix : int -> consts -> bool

Sourceval is_prefix : int -> consts -> bool

Source

val unfold_binder : 
  int ->
  int ->
  int ->
  consts ->
  (int * (string * Abstract_syntax.Abstract_syntax.abstraction)) list ->
  (env * env) ->
  term ->
  (int * (string * Abstract_syntax.Abstract_syntax.abstraction)) list
  * int
  * int
  * term

Sourceval kind_to_string : kind -> consts -> string

Sourceval type_to_string : stype -> consts -> string

Sourceval term_to_string : term -> consts -> string

Sourceval kind_to_formatted_string : Format.formatter -> kind -> consts -> unit

Sourceval type_to_formatted_string : Format.formatter -> stype -> consts -> unit

Sourceval term_to_formatted_string : Format.formatter -> term -> consts -> unit

Sourceval raw_to_string : term -> string

Sourceval raw_type_to_string : stype -> string

Sourceval raw_to_caml : term -> string

Sourceval raw_type_to_caml : stype -> string

Sourceval normalize : ?id_to_term:(int -> term) -> term -> term

Sourceval unlinearize_term : term -> term

Sourceval unlinearize_type : stype -> stype

Sourceval eta_long_form : term -> stype -> (int -> stype) -> term

eta_long_form t ty type_of_cst returns the eta-long form of t with respect of type ty. t is supposed to be in beta-normal form and all the definitions of t and ty should have been unfolded. type_of_cst i returns the type (with unfolded definitions) of the constant whose id is i. i is supposed to be an actual id of a constant.

Sourceval is_2nd_order : stype -> (int -> stype) -> bool

is_2nd_order ty type_definition returns true if ty is 2nd order. ty should have been unfolded and type_definition i is returns the unfolded type of a defined type (DAtom) whose id is i. i is supposed to be an actual id of such a defined type.

package acgtk

Module Lambda.LambdaSource

Module `Lambda.Lambda`Source