1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
|
||| Raw syntax for terms. This is before eliminating names.
module Obs.Syntax
import Obs.Pretty
import Obs.Universe
import Text.Bounded
%default total
-- Definition ------------------------------------------------------------------
public export
data Syntax : Type where
Var : (var : String) -> Syntax
-- Universes
Universe : (s : Universe) -> Syntax
-- Dependent Products
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 : (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 : (var : WithBounds String) ->
(returnType, discriminant, true, false : WithBounds Syntax) ->
Syntax
-- True
Top : Syntax
Point : Syntax
-- False
Bottom : Syntax
Absurd : (contradiction : WithBounds Syntax) -> Syntax
-- Equality
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
constructor MkDefinition
name : WithBounds String
ty : WithBounds Syntax
tm : WithBounds Syntax
-- Pretty Print ----------------------------------------------------------------
prettyPrecBounds : Prec -> WithBounds Syntax -> Doc ann
prettyPrec : Prec -> 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}) =
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, 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 {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 {oldType, newType, equality, value}) =
prettyApp d (pretty "cast") $
[ prettyPrecBounds App oldType
, prettyPrecBounds App newType
, prettyPrecBounds App equality
, prettyPrecBounds App value
]
prettyPrec d (CastId {value}) = prettyApp d (pretty "castRefl") [prettyPrecBounds App value]
prettyPrecBounds d (MkBounded val _ _) = prettyPrec d val
export
Pretty Syntax where
prettyPrec = Syntax.prettyPrec
export
Pretty Definition where
pretty def = group $
pretty def.name.val <++> colon <+> softline <+> pretty def.ty.val <+> hardline <+>
pretty def.name.val <++> equals <+> softline <+> pretty def.tm.val
|
