diff options
Diffstat (limited to 'src/Obs/Syntax.idr')
| -rw-r--r-- | src/Obs/Syntax.idr | 179 |
1 files changed, 85 insertions, 94 deletions
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr index 32e86c0..a8a468c 100644 --- a/src/Obs/Syntax.idr +++ b/src/Obs/Syntax.idr @@ -12,35 +12,37 @@ import Text.PrettyPrint.Prettyprinter public export data Syntax : Type where - Var : String -> Syntax + Var : (var : String) -> Syntax -- Universes - Universe : Universe -> Syntax + Universe : (s : Universe) -> Syntax -- Dependent Products - Pi : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> Syntax - Lambda : WithBounds String -> WithBounds Syntax -> Syntax - App : WithBounds Syntax -> WithBounds Syntax -> Syntax + Pi : (var : WithBounds String) -> (domain, codomain : WithBounds Syntax) -> Syntax + Lambda : (var : WithBounds String) -> (body : WithBounds Syntax) -> Syntax + App : (fun, arg : WithBounds Syntax) -> Syntax -- Dependent Sums - Sigma : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> Syntax - Pair : WithBounds Syntax -> WithBounds Syntax -> Syntax - Fst : WithBounds Syntax -> Syntax - Snd : WithBounds Syntax -> Syntax + Sigma : (var : WithBounds String) -> (index, element : WithBounds Syntax) -> Syntax + Pair : (first, second : WithBounds Syntax) -> Syntax + First : (arg : WithBounds Syntax) -> Syntax + Second : (arg : WithBounds Syntax) -> Syntax -- Booleans Bool : Syntax True : Syntax False : Syntax - If : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax + If : (var : WithBounds String) -> + (returnType, discriminant, true, false : WithBounds Syntax) -> + Syntax -- True Top : Syntax Point : Syntax -- False Bottom : Syntax - Absurd : WithBounds Syntax -> Syntax + Absurd : (contradiction : WithBounds Syntax) -> Syntax -- Equality - Equal : WithBounds Syntax -> WithBounds Syntax -> Syntax - Refl : WithBounds Syntax -> Syntax - Transp : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax - Cast : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax - CastId : WithBounds Syntax -> Syntax + Equal : (left, right : WithBounds Syntax) -> Syntax + Refl : (value : WithBounds Syntax) -> Syntax + Transp : (indexedType, oldIndex, value, newIndex, equality : WithBounds Syntax) -> Syntax + Cast : (oldType, newType, equality, value : WithBounds Syntax) -> Syntax + CastId : (value : WithBounds Syntax) -> Syntax public export record Definition where @@ -51,102 +53,91 @@ record Definition where -- Pretty Print ---------------------------------------------------------------- -prettyPrec : Prec -> Syntax -> Doc ann -prettyPrecBounds : Prec -> WithBounds Syntax -> Doc ann +prettyDecl : (name : String) -> (ty : Doc ann) -> Doc ann +prettyDecl name ty = parens $ group (pretty name <++> colon <+> line <+> align ty) -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) = +prettyDeclForm : (prec : Prec) -> + (name : String) -> + (ty : Doc ann) -> + (sep : String) -> + (tail : Doc ann) -> + Doc ann +prettyDeclForm d name ty sep tail = 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) = + vsep $ + [prettyDecl name ty <++> pretty sep, align tail] + +prettyLambda : (prec : Prec) -> (name : String) -> (body : Doc ann) -> Doc ann +prettyLambda d name body = 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) = + backslash <+> pretty name <++> pretty "=>" <+> line <+> align body + +prettyApp : (prec : Prec) -> (head : Doc ann) -> (tail : List (Doc ann)) -> Doc ann +prettyApp d head tail = parenthesise (d >= App) $ group $ vsep (align head :: map (hang 2) tail) + +prettyPrec : Prec -> Syntax -> Doc ann +prettyPrecBounds : Prec -> WithBounds Syntax -> Doc ann + +prettyPrec d (Var {var}) = 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}) = 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] + neutral <++> + align (prettyPrecBounds Open first) <+> + comma <+> + line <+> + align (prettyPrecBounds Open second) <++> + neutral +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 >= App) $ - group $ - vsep [pretty "absurd", prettyPrecBounds App t] -prettyPrec d (Equal t u) = +prettyPrec d (Absurd {contradiction}) = + prettyApp d (pretty "absurd") [prettyPrecBounds App contradiction] +prettyPrec d (Equal {left, right}) = 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 + align (prettyPrecBounds Equal left) <++> + pretty "~" <+> + line <+> + align (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 val _ _) = prettyPrec d val |