blob: 9215ddaf88af6f9db936c5f51dcc74549476bcd9 (
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
|
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
export
abstractSyntax : Context n -> Syntax -> Logging ann (Term n)
abstractSyntax ctx (Var var) = do
let Just i = lookup var.val ctx
| Nothing => inScope "unbound variable" $ fatal var
pure (Var var i)
abstractSyntax ctx (Sort bounds s) = pure (Sort bounds s)
abstractSyntax ctx (Pi bounds var a b) = do
a <- abstractSyntax ctx a
b <- abstractSyntax (bind ctx var.val) b
pure (Pi bounds var.val a b)
abstractSyntax ctx (Lambda bounds var t) = do
t <- abstractSyntax (bind ctx var.val) t
pure (Lambda bounds var.val t)
abstractSyntax ctx (App t u) = do
t <- abstractSyntax ctx t
u <- abstractSyntax ctx u
pure (App t u)
abstractSyntax ctx (Sigma bounds var a b) = do
a <- abstractSyntax ctx a
b <- abstractSyntax (bind ctx var.val) b
pure (Sigma bounds var.val a b)
abstractSyntax ctx (Pair b t u) = do
t <- abstractSyntax ctx t
u <- abstractSyntax ctx u
pure (Pair b t u)
abstractSyntax ctx (Fst b t) = do
t <- abstractSyntax ctx t
pure (Fst b t)
abstractSyntax ctx (Snd b t) = do
t <- abstractSyntax ctx t
pure (Snd b t)
abstractSyntax ctx (Top b) = pure (Top b)
abstractSyntax ctx (Point b) = pure (Point b)
abstractSyntax ctx (Bottom b) = pure (Bottom b)
abstractSyntax ctx (Absurd bounds a t) = do
a <- abstractSyntax ctx a
t <- abstractSyntax ctx t
pure (Absurd bounds a t)
abstractSyntax ctx (Equal bounds t u) = do
t <- abstractSyntax ctx t
u <- abstractSyntax ctx u
pure (Equal bounds t u)
abstractSyntax ctx (Refl bounds t) = do
t <- abstractSyntax ctx t
pure (Refl bounds t)
abstractSyntax ctx (Transp bounds t b u t' e) = do
t <- abstractSyntax ctx t
b <- abstractSyntax ctx b
u <- abstractSyntax ctx u
t' <- abstractSyntax ctx t'
e <- abstractSyntax ctx e
pure (Transp bounds t b u t' e)
abstractSyntax ctx (Cast bounds b e t) = do
b <- abstractSyntax ctx b
e <- abstractSyntax ctx e
t <- abstractSyntax ctx t
pure (Cast bounds b e t)
abstractSyntax ctx (CastId bounds t) = do
t <- abstractSyntax ctx t
pure (CastId bounds t)
abstractDefinition : Context n -> Definition -> Logging ann (Definition n)
abstractDefinition ctx def = pure $ MkDefinition
{ name = def.name
, bounds = def.bounds
, ty = !(abstractSyntax ctx def.ty)
, tm = !(abstractSyntax 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
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
|
