diff options
Diffstat (limited to 'src/Obs/Term.idr')
| -rw-r--r-- | src/Obs/Term.idr | 186 |
1 files changed, 68 insertions, 118 deletions
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr index c4d9e40..95ed08b 100644 --- a/src/Obs/Term.idr +++ b/src/Obs/Term.idr @@ -2,9 +2,11 @@ module Obs.Term import Data.Fin + +import Obs.Pretty import Obs.Universe + import Text.Bounded -import Text.PrettyPrint.Prettyprinter %default total @@ -12,56 +14,51 @@ import Text.PrettyPrint.Prettyprinter public export data Term : Nat -> Type where - Var : String -> Fin n -> Term n + Var : (var : String) -> (i : Fin n) -> Term n -- Universes - Universe : Universe -> Term n + Universe : (s : Universe) -> Term n -- Dependent Product - Pi : WithBounds String -> WithBounds (Term n) -> WithBounds (Term (S n)) -> Term n - Lambda : WithBounds String -> WithBounds (Term (S n)) -> Term n - App : WithBounds (Term n) -> WithBounds (Term n) -> Term n + Pi : (var : WithBounds String) -> + (domain : WithBounds (Term n)) -> + (codomain : WithBounds (Term (S n))) -> + Term n + Lambda : (var : WithBounds String) -> (body : WithBounds (Term (S n))) -> Term n + App : (fun, arg : WithBounds (Term n)) -> Term n -- Dependent Sums - Sigma : WithBounds String -> WithBounds (Term n) -> WithBounds (Term (S n)) -> Term n - Pair : WithBounds (Term n) -> WithBounds (Term n) -> Term n - Fst : WithBounds (Term n) -> Term n - Snd : WithBounds (Term n) -> Term n + Sigma : (var : WithBounds String) -> + (index : WithBounds (Term n)) -> + (element : WithBounds (Term (S n))) -> + Term n + Pair : (first, second : WithBounds (Term n)) -> Term n + First : (arg : WithBounds (Term n)) -> Term n + Second : (arg : WithBounds (Term n)) -> Term n -- Booleans Bool : Term n True : Term n False : Term n - If : WithBounds String -> - WithBounds (Term (S n)) -> - WithBounds (Term n) -> - WithBounds (Term n) -> - WithBounds (Term n) -> + If : (var : WithBounds String) -> + (returnType : WithBounds (Term (S n))) -> + (discriminant, true, false : WithBounds (Term n)) -> Term n -- True Top : Term n Point : Term n -- False Bottom : Term n - Absurd : WithBounds (Term n) -> Term n + Absurd : (contradiction : WithBounds (Term n)) -> Term n -- Equality - Equal : WithBounds (Term n) -> WithBounds (Term n) -> Term n - Refl : WithBounds (Term n) -> Term n - Transp : WithBounds (Term n) -> - WithBounds (Term n) -> - WithBounds (Term n) -> - WithBounds (Term n) -> - WithBounds (Term n) -> - Term n - Cast : WithBounds (Term n) -> - WithBounds (Term n) -> - WithBounds (Term n) -> - WithBounds (Term n) -> - Term n - CastId : WithBounds (Term n) -> Term n + Equal : (left, right : WithBounds (Term n)) -> Term n + Refl : (value : WithBounds (Term n)) -> Term n + Transp : (indexedType, oldIndex, value, newIndex, equality : WithBounds (Term n)) -> Term n + Cast : (oldType, newType, equality, value : WithBounds (Term n)) -> Term n + CastId : (value : WithBounds (Term n)) -> Term n public export record Definition (n : Nat) where constructor MkDefinition - name : WithBounds String - ty : WithBounds (Term n) - tm : WithBounds (Term n) + name : WithBounds String + ty : WithBounds (Term n) + tm : WithBounds (Term n) public export data Block : Nat -> Type where @@ -70,102 +67,55 @@ data Block : Nat -> Type where -- Pretty Print ---------------------------------------------------------------- -prettyPrec : Prec -> Term n -> Doc ann prettyPrecBounds : Prec -> WithBounds (Term n) -> Doc ann -prettyPrec d (Var var _) = pretty var -prettyPrec d (Universe s) = prettyPrec d s -prettyPrec d (Pi var a b) = - parenthesise (d > Open) $ - group $ - parens (pretty var.val <++> colon <+> softline <+> align (prettyPrecBounds Open a)) <++> - pretty "->" <+> line <+> - align (prettyPrecBounds Open b) -prettyPrec d (Lambda var t) = - parenthesise (d > Open) $ - group $ - backslash <+> pretty var.val <++> - pretty "=>" <+> line <+> - align (prettyPrecBounds Open t) -prettyPrec d (App t u) = - parenthesise (d >= App) $ - group $ - vsep [prettyPrecBounds Open t, prettyPrecBounds App u] -prettyPrec d (Sigma var a b) = - parenthesise (d >= App) $ - group $ - parens (pretty var.val <++> colon <+> softline <+> align (prettyPrecBounds Open a)) <++> - pretty "**" <+> line <+> - align (prettyPrecBounds Open b) -prettyPrec d (Pair t u) = - angles $ - group $ - neutral <++> prettyPrecBounds Open t <+> comma <+> line <+> prettyPrecBounds Open u <++> neutral -prettyPrec d (Fst t) = - parenthesise (d >= App) $ - group $ - vsep [pretty "fst", prettyPrecBounds App t] -prettyPrec d (Snd t) = - parenthesise (d >= App) $ - group $ - vsep [pretty "snd", prettyPrecBounds App t] +prettyPrec : Prec -> Term n -> Doc ann +prettyPrec d (Var {var, i}) = pretty var +prettyPrec d (Universe {s}) = prettyPrec d s +prettyPrec d (Pi {var, domain, codomain}) = + prettyDeclForm d var.val (prettyPrecBounds Open domain) "->" (prettyPrecBounds Open codomain) +prettyPrec d (Lambda {var, body}) = prettyLambda d var.val (prettyPrecBounds Open body) +prettyPrec d (App {fun, arg}) = prettyApp d (prettyPrecBounds Open fun) [prettyPrecBounds App arg] +prettyPrec d (Sigma {var, index, element}) = + prettyDeclForm d var.val (prettyPrecBounds Open index) "**" (prettyPrecBounds Open element) +prettyPrec d (Pair {first, second}) = + prettyPair (prettyPrecBounds Open first) (prettyPrecBounds Open second) +prettyPrec d (First {arg}) = prettyApp d (pretty "fst") [prettyPrecBounds App arg] +prettyPrec d (Second {arg}) = prettyApp d (pretty "snd") [prettyPrecBounds App arg] prettyPrec d Bool = pretty "Bool" prettyPrec d True = pretty "True" prettyPrec d False = pretty "False" -prettyPrec d (If var a t f g) = - parenthesise (d >= App) $ - group $ - vsep $ - [ pretty "if" - , parens $ - group $ - backslash <+> pretty var.val <++> - pretty "=>" <+> line <+> - align (prettyPrecBounds Open a) - , prettyPrecBounds App t - , prettyPrecBounds App f - , prettyPrecBounds App g +prettyPrec d (If {var, returnType, discriminant, true, false}) = + prettyApp d (pretty "if") $ + [ prettyLambda App var.val (prettyPrecBounds Open returnType) + , prettyPrecBounds App discriminant + , prettyPrecBounds App true + , prettyPrecBounds App false ] prettyPrec d Top = pretty "()" prettyPrec d Point = pretty "tt" prettyPrec d Bottom = pretty "Void" -prettyPrec d (Absurd t) = - parenthesise (d > Open) $ - group $ - vsep [pretty "absurd", prettyPrecBounds App t] -prettyPrec d (Equal t u) = - parenthesise (d >= Equal) $ - group $ - prettyPrecBounds Equal t <++> pretty "~" <+> line <+> prettyPrecBounds Equal u -prettyPrec d (Refl t) = - parenthesise (d >= App) $ - group $ - vsep [pretty "refl", prettyPrecBounds App t] -prettyPrec d (Transp a t u t' e) = - parenthesise (d >= App) $ - group $ - vsep $ - [ pretty "transp" - , prettyPrecBounds App a - , prettyPrecBounds App t - , prettyPrecBounds App u - , prettyPrecBounds App t' - , prettyPrecBounds App e +prettyPrec d (Absurd {contradiction}) = + prettyApp d (pretty "absurd") [prettyPrecBounds App contradiction] +prettyPrec d (Equal {left, right}) = + prettyEqual d (prettyPrecBounds Equal left) (prettyPrecBounds Equal right) +prettyPrec d (Refl {value}) = prettyApp d (pretty "refl") [prettyPrecBounds App value] +prettyPrec d (Transp {indexedType, oldIndex, value, newIndex, equality}) = + prettyApp d (pretty "transp") $ + [ prettyPrecBounds App indexedType + , prettyPrecBounds App oldIndex + , prettyPrecBounds App value + , prettyPrecBounds App newIndex + , prettyPrecBounds App equality ] -prettyPrec d (Cast a b e t) = - parenthesise (d >= App) $ - group $ - vsep $ - [ pretty "cast" - , prettyPrecBounds App a - , prettyPrecBounds App b - , prettyPrecBounds App e - , prettyPrecBounds App t +prettyPrec d (Cast {oldType, newType, equality, value}) = + prettyApp d (pretty "cast") $ + [ prettyPrecBounds App oldType + , prettyPrecBounds App newType + , prettyPrecBounds App equality + , prettyPrecBounds App value ] -prettyPrec d (CastId t) = - parenthesise (d >= App) $ - group $ - vsep [pretty "castRefl", prettyPrecBounds App t] +prettyPrec d (CastId {value}) = prettyApp d (pretty "castRefl") [prettyPrecBounds App value] prettyPrecBounds d (MkBounded v _ _) = prettyPrec d v |