Skip to content

KIL

Jump to bottom Edit New page
mdmkolbe edited this page Oct 31, 2013 · 14 revisions

The KIL classes reside in org.kframework.kil and can be divided into three groups:

  • The classes that represent Basic syntax,
  • The classes that represent Concrete syntax, and
  • Other miscellaneous classes.

Sub-packages

  • org.kframework.kil.loader
  • org.kframework.kil.matchers: Classes and interfaces for matcher pattern???
  • org.kframework.kil.rewriter
  • org.kframework.kil.visitors: Classes and interfaces for visitor pattern

ASTNode

ASTNode is the root of the inheritance hierarchy for most KIL classes. Contains a mapping from tags (i.e., Strings) to Attribute values.

The most important classes are those implementing Basic Syntax and those implementing Concrete Syntax. The ones implementing Concrete Syntax inherit from Term while the ones implementing Basic Syntax inherit from one of the following classes:

  • DefinitionItem
  • ModuleItem
  • PriorityBlockExtended
  • PriorityBlock
  • ProductionItem
  • Production

Misc Classes

The following classes inherit from ASTNode but are not part of either Concrete or Basic Syntax.

  • Attribute: A pair of a String key and a String value. Contains String constants for "builtin", "function", "hook", "macro" and "simplification. Contains Attribute constants for "bracket", "function", "predicate", "anywhere", and "equality". Why are some constants Strings and others Attributes? Why is "function" in both?
    • Location: An attribute that stores location information in already parsed form. Is this really needed? Does this need to inherit from ASTNode?
  • Attributes: A collection of Attribute objects. Used as the attribute field of ASTNode. Does this need to inherit from ASTNode? Why don't we use a standard collection (e.g. java.util.List)?
  • ParseError: What is this? At first, I thought this was thrown on a parse error, but now I suspect otherwise.
  • Definition

Non-ASTNodes

The following public classes do not inherit from ASTNode.

  • KSort: An enumeration of the built in sorts. See Sorts. Missing KResult?
  • KSorts: An empty class containing static constants for the sort names. Why isn't this part of KSort?
  • LiterateComment: An interface for both LiterateModuleComment and LiterateDefinitionComment.
  • ConfigurationNotFound: Extends Exception. Who throws this and when?
  • ConfigurationNotUnique: Extends Exception. Who throws this and when?
  • DataStructureSort: What is this???

Basic Syntax

These classes represent the Basic Syntax and are generated by org.kframework.parser.basic.Basic which is generated by javacc from Basic.jj.

In the following Assoc is a String that is "left", "right" or "non-assoc".

  • DefinitionItem: An item that goes on the outside

    • Require: A "require String" where String is a file name. Similar to a C-style '#include'
    • Module: A "module endmodule" or "interface ... endinterface". Can we do away with "interface"?
    • LiterateDefinitionComment: A comment outside any particular module

  • ModuleItem: A clause that goes in a module

    • Import: import String where String is a module name
    • LiterateModuleComment: A comment inside a module.
    • StringSentence: A rule, context, or configuration that has not been parsed by the concrete parser yet.
    • PriorityExtended: syntax priorities List{PriorityBlockExtended, ">"}
    • PriorityExtendedAssoc: syntax Assoc List{KLabelConstant, " "}
    • Restrictions: syntax restrictions Sort -/- String or syntax restrictions Terminal -/- String. The String is a "." separated sequence of regex character classes.
    • Syntax: syntax Sort ::= List{PriorityBlock, ">"}

The following are all related to "syntax" declarations.

  • PriorityBlockExtended: Assoc List{KLabelConstant, " "}
  • PriorityBlock: Assoc: List{Production, "|"}
  • Production: List{ProductionItem, " "}. A "syntax" production. Also contains Strings for the names of the Sort and Module the Production belongs to.
  • ProductionItem: An atomic item in a syntax production
    • Terminal: A literal string in a production. A fixed, constant terminal.
    • Lexical: Lexical{String} or Token{String}. A non-constant terminal. The String is a regex. Contains a String for follow restricts when a "Token".
    • Sort: A reference to a named non-terminal in a production. NOTE: This is abused in non-productions to just refer to a specific sort. Can we fix that?
    • UserList: A List{Sort, String} or a NeList{Sort, String}.

Concrete Syntax

Sentences

The following classes extend ModuleItem, but are not parsed by the Basic parser (can we fix that?) and so are considered the domain of Concrete Syntax (for now).

  • Sentence: A "rule", "context" or "configuration" sentence. Why are the fields in Sentence instead of its children?
    • Configuration: configuration Term
    • Context: context Term
    • Rule: rule Term Why does this have builtinLookups in it?

Terms

The classes defining the actual concrete syntax inherit from Term. Every Term has a Sort associated with it. (Why is the Sort a String instead of Structured?)

Generic terms

These can appear anywhere. But as a consequence, they also cause problems. Can we fix that?

  • Variable
  • Ambiguity
  • Rewrite: Could we parameterize this? Where is this legal?
  • Bracket
  • Cast
  • Hole
  • FrezerHole

Collections

  • Collection: How does this differ from CollectionBuiltin? Do these things really belong together?

    • Ambiguity: Does not exist after disambiguation?
    • KList: Argument to a KApp? Are these first class? Why not just embed them in KApp?
    • KSequence: "~>" List. How is different from List{KItem, "~>"}?
    • Bag
    • List: Elements are all ListItems (except variables, etc.)
    • Map
    • Set

  • DataStructureBuiltin: How does this differ from Collection? Newer than Collections but not fully implemented

    • MapBuiltin: why not under CollectionBuiltin? How are baseTerms and elements different? Why does it not inherit from CollectionBuiltin? Sort = MyMap
    • CollectionBuiltin: How are elements different from baseTerms? Thing were elements are a single things rather than "Map" where elements are pairs
      • ListBuiltin: How are elementsRight different from elements? Sort = MyList Only one variable (of sort MyList) in this list
      • SetBuiltin: Sort = MySet

  • CollectionItem: Just for Collection

    • BagItem
    • ListItem
    • MapItem
    • SetItem

  • ListUpdate: What is this? What are remove left and remove right (constructor args)?

  • MapUpdate

  • SetUpdate: What is this? What are removeEntries? Where is addEntries? (constructor args)

  • BuiltinLookup: Contains a Term key and Variable base. What is base? What is being looked up in?

    • ListLookup: What is the extra Term value?
    • MapLookup: What is the extra Term value?
    • SetLookup

Other

  • BackendTerm: An uninterpreted (Maude) backend term represented as a String. Is this still used? Is this used for anything other than Maude?
  • Bracket: What is this?
  • Cast: What is this? Is it a cast in the Java sense or something else? What is the boolean syntactic field? Is this any different from Bracket? Where is the sort being cast to?
  • Cell
  • Empty: (depricated?)
    • ListTerminator: how is different from empty w/ null separator? unused?
  • FreezerHole: A hole in a freezer?
  • Freezer: does the term contain a single FreezerHole? something that you do not rewrite under.
  • Hole: What sorts of terms is the allowed to occur in? A hole in a context?
  • KApp: Contains two Terms. Why not KLabel and KList? b/c it needs ambig?
  • KInjectedLabel: What is this? Should this be a subclass of KLabel? This turns a Term into a KLabel?
    • FreezerLabel: What is this? (used to avoid generic recursion into Freezers?, produced only late in Maude backend?)
  • KLabel
    • KLabelConstant: What is the list of Productions that the constructor takes as argument?
    • Token: Does a KToken need to be applied (via KApp) to arguments before it is a proper K term? Is it valid for a KToken to be applied?
      • BoolBuiltin
      • GenericToken.java
      • IntBuiltin.java
      • StringBuiltin.java
  • TermComment: A line break tag.
  • TermCons: What is this? What are these fields? (Used during parsing and then converted to the "real" KIL class? Also hangs around for non K-sorted functions? TODO: eliminate SDF name in favor of Klabel (then remove SDF to K label mapping from context)) precursor to KApp that names a production instead of a Klabel
Add a custom footer
Add a custom sidebar

Clone this wiki locally