use std::collections::BTreeMap; use crate::semantics::Universe; use crate::syntax::map::{DupTreeMap, DupTreeSet}; use crate::syntax::visitor; use crate::syntax::*; pub type Integer = isize; pub type Natural = usize; pub type Double = NaiveDouble; /// Double with bitwise equality #[derive(Debug, Copy, Clone)] pub struct NaiveDouble(f64); /// Constants for a pure type system #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] pub enum Const { Type, Kind, Sort, } impl Const { pub(crate) fn to_universe(self) -> Universe { Universe::from_const(self) } } /// Bound variable /// /// The `Label` field is the variable's name (i.e. \"`x`\"). /// The `Int` field is a DeBruijn index. /// See dhall-lang/standard/semantics.md for details #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub struct V(pub Label, pub usize); // Definition order must match precedence order for // pretty-printing to work correctly #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] pub enum BinOp { /// `x ? y` ImportAlt, /// `x || y` BoolOr, /// `x + y` NaturalPlus, /// `x ++ y` TextAppend, /// `x # y` ListAppend, /// `x && y` BoolAnd, /// `x ∧ y` RecursiveRecordMerge, /// `x ⫽ y` RightBiasedRecordMerge, /// `x ⩓ y` RecursiveRecordTypeMerge, /// `x * y` NaturalTimes, /// `x == y` BoolEQ, /// `x != y` BoolNE, /// x === y Equivalence, } /// Built-ins #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)] pub enum Builtin { Bool, Natural, Integer, Double, Text, List, Optional, OptionalNone, NaturalBuild, NaturalFold, NaturalIsZero, NaturalEven, NaturalOdd, NaturalToInteger, NaturalShow, NaturalSubtract, IntegerToDouble, IntegerShow, IntegerNegate, IntegerClamp, DoubleShow, ListBuild, ListFold, ListLength, ListHead, ListLast, ListIndexed, ListReverse, OptionalFold, OptionalBuild, TextShow, } // Each node carries an annotation. #[derive(Debug, Clone)] pub struct Expr { kind: Box>, span: Span, } pub type UnspannedExpr = ExprKind; /// Numeric literals #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub enum NumKind { /// `True` Bool(bool), /// `1` Natural(Natural), /// `+2` Integer(Integer), /// `3.24` Double(Double), } /// Syntax tree for expressions // Having the recursion out of the enum definition enables writing // much more generic code and improves pattern-matching behind // smart pointers. #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub enum ExprKind { Const(Const), Num(NumKind), /// `x` /// `x@n` Var(V), /// `λ(x : A) -> b` Lam(Label, SubExpr, SubExpr), /// `A -> B` /// `∀(x : A) -> B` Pi(Label, SubExpr, SubExpr), /// `f a` App(SubExpr, SubExpr), /// `let x = r in e` /// `let x : t = r in e` Let(Label, Option, SubExpr, SubExpr), /// `x : t` Annot(SubExpr, SubExpr), /// `assert : t` Assert(SubExpr), /// Built-in values Builtin(Builtin), // Binary operations BinOp(BinOp, SubExpr, SubExpr), /// `if x then y else z` BoolIf(SubExpr, SubExpr, SubExpr), /// `"Some ${interpolated} text"` TextLit(InterpolatedText), /// `[] : t` EmptyListLit(SubExpr), /// `[x, y, z]` NEListLit(Vec), /// `Some e` SomeLit(SubExpr), /// `{ k1 : t1, k2 : t1 }` RecordType(DupTreeMap), /// `{ k1 = v1, k2 = v2 }` RecordLit(BTreeMap), /// `< k1 : t1, k2 >` UnionType(DupTreeMap>), /// `merge x y : t` Merge(SubExpr, SubExpr, Option), /// `toMap x : t` ToMap(SubExpr, Option), /// `e.x` Field(SubExpr, Label), /// `e.{ x, y, z }` Projection(SubExpr, DupTreeSet