data BasicSpec = BasicSpec [Annoted BasicItem]
data BasicItem = SigItems SigItems
| ProgItems [Annoted ProgEq] [Pos]
| ClassItems Instance [Annoted ClassItem] [Pos]
| GenVarItems [GenVarDecl] [Pos]
| FreeDatatype [Annoted DatatypeDecl] [Pos]
-- pos "free", "type", ";"s
| GenItems [Annoted BasicItem] [Pos]
-- pos "generated" "{", ";"s, "}"
-- or "generated" "type" ";"s
| LocalVarAxioms [GenVarDecl] [Annoted Formula] [Pos]
| AxiomItems [Annoted Formula] [Pos]
data SigItems = TypeItems Instance [Annoted TypeItem] [Pos] -- including sort
| OpItems [Annoted OpItem] [Pos]
| PredItems [Annoted PredItem] [Pos]
data Instance = Instance | Plain deriving (Show,Eq)
data ClassItem = ClassItem ClassDecl [Annoted BasicItem] [Pos]
data ClassDecl = ClassDecl [ClassName] [Pos]
| SubclassDecl [ClassName] Class [Pos]
| ClassDefn ClassName Class [Pos]
| DownsetDefn ClassName TypeVar Type [Pos]
-- pos " =" "{", dot, "<", typeVar, "}"
data TypeItem = TypeDecl [TypePattern] Kind [Pos]
| SubtypeDecl [TypePattern] Type [Pos]
| IsoDecl [TypePattern] [Pos]
| SubtypeDefn TypePattern Var Type (Annoted Formula) [Pos]
-- pos "=", "{", ":", dot, "}"
| AliasType TypePattern Kind PseudoType [Pos]
data TypePattern = TypePattern TypeName [TypeArg] [Pos]
| MixfixTypePattern [TypePattern]
| BracketTypePattern BracketKind [TypePattern] [Pos]
| TypePatternArgs [TypeArg]
data PseudoType = SimplePseudoType Type
| PseudoType [TypeArgs] PseudoType [Pos]
-- pos "\" "("s, ")"s, dot
data Type = TypeConstrAppl TypeName Kind [Type] [Pos] -- analysed
| BracketType BracketKind [Type] [Pos]
| KindedType Type Kind Pos
-- pos "," (between type arguments)
| ProductType [Type] [Pos]
| FunType Type Arrow Type Pos
data Arrow = FunArr| PFunArr | ContFunArr | PContFunArr
-- no curried notation for bound variables
data TypeScheme = SimpleTypeScheme Type
| TypeScheme [TypeVarDecl] TypeScheme [Pos]
-- pos "forall", ";"s, dot
data Partiality = Partial | Total deriving (Show,Eq)
data OpItem = OpDecl [OpName] TypeScheme [OpAttr] [Pos]
-- pos ","s, ":", ","s, "assoc", "comm", "idem", "unit"
| OpDefn OpName [Pattern] TypeScheme Term [Pos]
-- pos "("s, ")"s, ":" or ":?", "="
data PredItem = PredDecl [OpName] TypeScheme [Pos]
-- pos ","s, ":", ","s, "assoc", "comm", "idem", "unit"
| PredDefn OpName [Pattern] Formula [Pos]
data BinOpAttr = Assoc | Comm | Idem deriving (Show,Eq)
data OpAttr = BinOpAttr BinOpAttr | UnitOpAttr Term deriving (Show,Eq)
data DatatypeDecl = DatatypeDecl
-- pos "::=", "|"s, "deriving"
data Alternative = Constructor UninstOpName [Components] Partiality [Pos]
data Components = Selector UninstOpName Partiality Type SeparatorKind Pos
| NestedComponents [Components] [Pos]
data Quantifier = Universal | Existential | Unique
data TypeQual = OfType | AsType | InType deriving (Show,Eq)
data BracketKind = Parens | Squares | Braces deriving (Show,Eq)
data LogOp = NotOp | AndOp | OrOp | ImplOp | EquivOp deriving (Show,Eq)
data EqOp = EqualOp | ExEqualOp deriving (Show,Eq)
-- proper formulae only exist after static analysis
data Formula = TermFormula Term
| ConnectFormula LogOp [Formula] [Pos]
-- pos not, "/\", "\/", impl, "<=>"
| EqFormula EqOp Term Term [Pos]
| QuantifiedFormula Quantifier [VarDecl] Formula [Pos]
-- pos quantifier, ";"s, dot
| PolyFormula [TypeVarDecl] Formula [Pos]
-- pos "forall", ";"s, dot
-- parse quantified formulae as terms first
-- eases also parsing of formulae in parenthesis
data Term = CondTerm Term Formula Term [Pos]
-- pos "(", "var", ":", ")"
| QualOp InstOpName TypeScheme [Pos]
-- pos "(", "op", ":", ")"
| ApplTerm Term Term [Pos] -- analysed
| TypedTerm Term TypeQual Type Pos
| QuantifiedTerm Quantifier [GenVarDecl] Term [Pos]
-- pos quantifier, ";"s, dot
-- only "forall" may have a TypeVarDecl
| LambdaTerm [Pattern] Partiality Term [Pos]
-- pos "\", dot (plus "!")
| CaseTerm Term [ProgEq] [Pos]
-- pos "case", "of", "|"s
| LetTerm [ProgEq] Term [Pos]
| BracketTerm BracketKind [Term] [Pos]
data Pattern = PatternVars [VarDecl] [Pos]
| PatternConstr InstOpName TypeScheme [Pattern] [Pos]
-- constructor or toplevel operation applied to arguments
| BracketPattern BracketKind [Pattern] [Pos]
-- pos brackets, ";"s, ","s
| TuplePattern [Pattern] [Pos]
| MixfixPattern [Pattern] -- or HO-Pattern
| TypedPattern Pattern Type [Pos]
| AsPattern Pattern Pattern [Pos]
data ProgEq = ProgEq Pattern Term Pos deriving (Show,Eq)
-- pos "=" (or "->" following case-of)
-- ----------------------------------------------------------------------------
-- ----------------------------------------------------------------------------
data SeparatorKind = Comma | Other deriving (Show,Eq)
data VarDecl = VarDecl Var Type SeparatorKind Pos deriving (Show,Eq)
data TypeVarDecl = TypeVarDecl TypeVar Class SeparatorKind Pos
data TypeVarDecls = TypeVarDecls [TypeVarDecl] [Pos] deriving (Show,Eq)
data TypeArg = TypeArg TypeVar ExtClass SeparatorKind Pos
-- pos "," or ":" ("+" or "-" pos is moved to ExtClass)
data TypeArgs = TypeArgs [TypeArg] [Pos] deriving (Show,Eq)
data GenVarDecl = GenVarDecl VarDecl
| GenTypeVarDecl TypeVarDecl
-- ----------------------------------------------------------------------------
-- ----------------------------------------------------------------------------
data Variance = CoVar | ContraVar | InVar deriving (Show,Eq)
data ExtClass = ExtClass Class Variance Pos deriving (Show,Eq)
-- pos "+" or "-" (or nullPos)
data ProdClass = ProdClass [ExtClass] [Pos] deriving (Show,Eq)
data Kind = Kind [ProdClass] Class [Pos] deriving (Show,Eq)
-- pos "->"s (first order)
data Class = Universe Pos -- pos "type" (or nullPos)
| Downset Type -- not parsed directly
| Intersection [Class] [Pos]
-- ----------------------------------------------------------------------------
-- ----------------------------------------------------------------------------
data OpName = OpName UninstOpName [TypeVarDecls] deriving (Show,Eq)
data Types = Types [Type] [Pos] deriving (Show,Eq) -- [TYPE, ..., TYPE]
data InstOpName = InstOpName UninstOpName [Types] deriving (Show,Eq)
-- ----------------------------------------------------------------------------
-- ----------------------------------------------------------------------------