blob: 48709c1c722014756eaed8c4ddbcb320b57df3be (
plain)
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
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
|
module Obs.Abstract
import Data.Fin
import Data.String
import Obs.Logging
import Obs.Syntax
import Obs.Term
import System
import Text.Bounded
%default total
Context : Nat -> Type
Context n = List (String, Fin n)
bind : Context n -> String -> Context (S n)
bind ctx str = (str, 0) :: map (mapSnd FS) ctx
abstractSyntax : Context n -> Syntax -> Logging ann (Term n)
abstractSyntaxBounds : Context n -> WithBounds Syntax -> Logging ann (WithBounds (Term n))
abstractSyntax ctx (Var var) = do
let Just i = lookup var ctx
| Nothing => inScope "unbound variable" $ fatal var
pure (Var var i)
abstractSyntax ctx (Sort s) = pure (Sort s)
abstractSyntax ctx (Pi var a b) = do
a <- abstractSyntaxBounds ctx a
b <- abstractSyntaxBounds (bind ctx var.val) b
pure (Pi var a b)
abstractSyntax ctx (Lambda var t) = do
t <- abstractSyntaxBounds (bind ctx var.val) t
pure (Lambda var t)
abstractSyntax ctx (App t u) = do
t <- abstractSyntaxBounds ctx t
u <- abstractSyntaxBounds ctx u
pure (App t u)
abstractSyntax ctx (Sigma var a b) = do
a <- abstractSyntaxBounds ctx a
b <- abstractSyntaxBounds (bind ctx var.val) b
pure (Sigma var a b)
abstractSyntax ctx (Pair t u) = do
t <- abstractSyntaxBounds ctx t
u <- abstractSyntaxBounds ctx u
pure (Pair t u)
abstractSyntax ctx (Fst t) = do
t <- abstractSyntaxBounds ctx t
pure (Fst t)
abstractSyntax ctx (Snd t) = do
t <- abstractSyntaxBounds ctx t
pure (Snd t)
abstractSyntax ctx (Sum a b) = do
a <- abstractSyntaxBounds ctx a
b <- abstractSyntaxBounds ctx b
pure (Sum a b)
abstractSyntax ctx (Left t) = do
t <- abstractSyntaxBounds ctx t
pure (Left t)
abstractSyntax ctx (Right t) = do
t <- abstractSyntaxBounds ctx t
pure (Right t)
abstractSyntax ctx (Case t s b f g) = do
t <- abstractSyntaxBounds ctx t
s <- abstractSyntaxBounds ctx s
b <- abstractSyntaxBounds ctx b
f <- abstractSyntaxBounds ctx f
g <- abstractSyntaxBounds ctx g
pure (Case t s b f g)
abstractSyntax ctx (Container a s s') = do
a <- abstractSyntaxBounds ctx a
s <- abstractSyntaxBounds ctx s
s' <- abstractSyntaxBounds ctx s'
pure (Container a s s')
abstractSyntax ctx (MkContainer t p f) = do
t <- abstractSyntaxBounds ctx t
p <- abstractSyntaxBounds ctx p
f <- abstractSyntaxBounds ctx f
pure (MkContainer t p f)
abstractSyntax ctx (Tag t) = do
t <- abstractSyntaxBounds ctx t
pure (Tag t)
abstractSyntax ctx (Position t) = do
t <- abstractSyntaxBounds ctx t
pure (Position t)
abstractSyntax ctx (Next t) = do
t <- abstractSyntaxBounds ctx t
pure (Next t)
abstractSyntax ctx (Sem s a t) = do
s <- abstractSyntaxBounds ctx s
a <- abstractSyntaxBounds ctx a
t <- abstractSyntaxBounds ctx t
pure (Sem s a t)
abstractSyntax ctx Top = pure Top
abstractSyntax ctx Point = pure Point
abstractSyntax ctx Bottom = pure Bottom
abstractSyntax ctx (Absurd a t) = do
a <- abstractSyntaxBounds ctx a
t <- abstractSyntaxBounds ctx t
pure (Absurd a t)
abstractSyntax ctx (Equal t u) = do
t <- abstractSyntaxBounds ctx t
u <- abstractSyntaxBounds ctx u
pure (Equal t u)
abstractSyntax ctx (Refl t) = do
t <- abstractSyntaxBounds ctx t
pure (Refl t)
abstractSyntax ctx (Transp t b u t' e) = do
t <- abstractSyntaxBounds ctx t
b <- abstractSyntaxBounds ctx b
u <- abstractSyntaxBounds ctx u
t' <- abstractSyntaxBounds ctx t'
e <- abstractSyntaxBounds ctx e
pure (Transp t b u t' e)
abstractSyntax ctx (Cast b e t) = do
b <- abstractSyntaxBounds ctx b
e <- abstractSyntaxBounds ctx e
t <- abstractSyntaxBounds ctx t
pure (Cast b e t)
abstractSyntax ctx (CastId t) = do
t <- abstractSyntaxBounds ctx t
pure (CastId t)
abstractSyntaxBounds ctx (MkBounded v irrel bnds) =
pure $ MkBounded !(abstractSyntax ctx v) irrel bnds
abstractDefinition : Context n -> Definition -> Logging ann (Definition n)
abstractDefinition ctx def = pure $ MkDefinition
{ name = def.name
, ty = !(abstractSyntaxBounds ctx def.ty)
, tm = !(abstractSyntaxBounds ctx def.tm)
}
export
abstractBlock : (defs : List Definition) -> Logging ann (Block (length defs))
abstractBlock defs =
let asContext : Block n -> Context n
asContext [] = []
asContext (defs :< def) = bind (asContext defs) def.name.val
in let helper : Block n -> (defs : List Definition) -> Logging ann (Block (length defs + n))
helper blk [] = pure blk
helper blk (def :: defs) = do
def <- abstractDefinition (asContext blk) def
(rewrite plusSuccRightSucc (length defs) n in helper (blk :< def) defs)
in rewrite sym $ plusZeroRightNeutral (length defs) in helper [] defs
|
