Type Members

1.  case class ADT(name: String, constructors: List[CONS] = Nil) extends DECL with Product with Serializable

   abstract data types: name -> id%%(args) | ...

   abstract data types: name -> id%%(args) | ... | id(args) name and id's ADT and CONS respectively but using implicit conversions in Program, they can also be strings anonymous record types are not permitted

2.  case class ADTRec(adts: List[ADT]) extends DECL with Product with Serializable

   a group of mutually recursive abstract data types

3.  case class ALIST(elems: List[EXP]) extends EXP with Product with Serializable

   a list

4.  case class AND(left: EXP, right: EXP) extends EXP with Product with Serializable

   conjunction

5.  case class APPLY(fun: String, args: EXP*) extends EXP with Product with Serializable

   function application

6.  case class ARECORD(tp: String, fields: List[FIELD]) extends EXP with Product with Serializable

   record value

7.  case class ARG(name: String, tp: EXP) extends Product with Serializable

   auxiliary class for arguments of a FUNCTION

8.  case class AT(l: EXP, index: EXP) extends EXP with Product with Serializable

   element of a list at a given index

9.  case class Binder(name: String, argument: Option[CatRef], bound: CatRef, scope: CatRef) extends Constructor with Product with Serializable

   a binder with some argument types and a typed bound variable we assume that the LF types of all binders are of the form {x:a} (b x -> s) -> c or (b -> s) -> c where a, b, s, c are atomic

10.  case class BuiltinType(e: EXP) extends Type with Product with Serializable
11.  case class CASE(pattern: EXP, body: EXP) extends Product with Serializable

    auxiliary class for cases in a MATCH

12.  case class COMMENT(text: String) extends DECL with Product with Serializable

    comments

13.  case class CONCAT(left: EXP, right: EXP) extends EXP with Product with Serializable

    concatenation of lists

14.  case class CONS(name: String, args: List[EXP] = Nil) extends Product with Serializable

    auxiliary class for constructors of an ADT

15.  case class CONSHEAD(name: String) extends Product with Serializable

    auxiliary class for constructors of an ADT as f of ("x" :: "type", ...)

16.  case class CatRef(target: String) extends Product with Serializable

    a reference to a type (family); possible type arguments are erased

17.  case class Category(name: String, constructors: List[Constructor]) extends Product with Serializable

    a type (family) with constructors; possible type arguments are erased

18.  class Compiler extends Program

    an example backend that transforms a LogicSyntax L into the SML code that represents and validates L-theories

19.  case class Connective(name: String, arguments: List[CatRef]) extends Constructor with Product with Serializable

    also works as a constructor for formulas, i.e.

    also works as a constructor for formulas, i.e. true : bool, false : bool, has no args in that case

20.  case class ConstantSymbol(pattern: String, name: String, arguments: List[CatRef]) extends Constructor with Product with Serializable

    a (Connective-like) constructor declared in a pattern body with some argument types

21.  abstract class Constructor extends AnyRef

    constructor for a Category

22.  case class Context(vars: List[(String, Type)]) extends Product with Serializable
23.  sealed abstract class DECL extends AnyRef

    declarations of a simple functional language

24.  case class DECLHEAD(name: String) extends Product with Serializable

    auxiliary class for constructing DECL's as name keyword arguments

    auxiliary class for constructing DECL's as name keyword arguments

    name

    the name of the declaration works with EXPConversions.stringToDECLHEAD

25.  case class Declaration(pattern: String, arguments: List[CatRef]) extends Product with Serializable

    a pragmatic declaration with some argument types

26.  case class EQUAL(left: EXP, right: EXP) extends EXP with Product with Serializable

    equality

27.  case class ERROR(name: String, msg: EXP) extends EXP with Product with Serializable

    throwing of an exception

28.  case class EXCEPTION(name: String) extends DECL with Product with Serializable

    exception declaration; all exception take a single string argument

29.  sealed abstract class EXP extends AnyRef

    expressions of a simple functional language

30.  case class FIELD(name: String, value: EXP) extends Product with Serializable

    auxiliary class for records types and values

31.  case class FUNCTION(name: String)(args: ARG*)(ret: EXP)(body: EXP) extends DECL with Product with Serializable

    function definition

32.  case class FUNCTIONRec(funs: List[FUNCTION]) extends DECL with Product with Serializable

    a group of mutually recursive functions

33.  case class FUNCTYPE(args: List[ARG], ret: EXP) extends Product with Serializable

    auxiliary class for function types

34.  case class FUNCVALUE(args: List[ARG], ret: EXP, body: EXP) extends Product with Serializable

    auxiliary class for anonymous functions

35.  abstract class FuncLang[A] extends AnyRef

    a simple functional language represented as transformation functions from declarations and expressions to strings

36.  case class FunctionalType(args: List[EXP], ret: EXP) extends Type with Product with Serializable
37.  case class ID(name: String) extends EXP with Product with Serializable

    identifiers the empty identifier ID("") is reserved: it refers to the current declaration, which is useful in recursive ADT and FUNCTION definitions

38.  case class IF(cond: EXP, thn: EXP, els: EXP) extends EXP with Product with Serializable

    if then else

39.  case class INT(value: Int) extends EXP with Product with Serializable

    integer literals

40.  case class LENGTH(l: EXP) extends EXP with Product with Serializable

    length of a list

41.  case class LIST(tp: EXP) extends EXP with Product with Serializable

    type of lists

42.  case class LogicSyntax(cats: List[Category], form: CatRef, decls: List[Declaration]) extends Product with Serializable

    a logic syntax consists of some categories (one of which is the category of formulas) and declarations

43.  class LogicWriter extends AnyRef
44.  case class MAP(l: EXP, fun: ID) extends EXP with Product with Serializable

    map over a list

45.  case class MATCH(arg: EXP, cases: List[CASE]) extends EXP with Product with Serializable

    pattern matching

46.  case class OPTION(tp: EXP) extends EXP with Product with Serializable

    type of options

47.  case class OR(left: EXP, right: EXP) extends EXP with Product with Serializable

    disjunction

48.  case class PLUS(left: EXP, right: EXP) extends EXP with Product with Serializable

    addition

49.  case class PROD(tps: List[EXP]) extends EXP with Product with Serializable

    product type

50.  case class PROJ(exp: EXP, proj: Int) extends EXP with Product with Serializable

    projection out of a product

51.  abstract class Program extends AnyRef

    convenience class for writing a program inside Scala concrete syntax

52.  case class RECORD(name: String, fields: List[FIELD] = Nil) extends DECL with Product with Serializable

    record type declaration: RECORD(n) ^{c1 :: A1} ...

    record type declaration: RECORD(n) ^{c1 :: A1} ... ^ cN :: AN anonymous record types are not permitted

53.  case class SELECT(record: EXP, field: String) extends EXP with Product with Serializable

    selection from a record

54.  case class SOME(elem: EXP) extends EXP with Product with Serializable

    a defined option

55.  case class STRING(value: String) extends EXP with Product with Serializable

    string literals

56.  case class STRINGCONCAT(left: EXP, right: EXP) extends EXP with Product with Serializable

    concatenation of strings

57.  case class SyntaxError(msg: String) extends Throwable with Product with Serializable
58.  case class TIMES(left: EXP, right: EXP) extends EXP with Product with Serializable

    multiplication

59.  case class TUPLE(tps: List[EXP]) extends EXP with Product with Serializable

    tuple

60.  case class TYPEDEF(name: String, df: EXP) extends DECL with Product with Serializable

    type definition

61.  class Theory2LogicSyntax extends AnyRef
62.  sealed abstract class Type extends AnyRef
63.  case class UNOPTION(sm: EXP) extends EXP with Product with Serializable

    unsafe access of the optional element (.get)

64.  case class Unsupported(msg: String) extends Throwable with Product with Serializable