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
|
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 (Universe {s}) = pure (Universe s)
abstractSyntax ctx (Pi {var, domain, codomain}) = do
a <- abstractSyntaxBounds ctx domain
b <- abstractSyntaxBounds (bind ctx var.val) codomain
pure (Pi var a b)
abstractSyntax ctx (Lambda {var, body}) = do
t <- abstractSyntaxBounds (bind ctx var.val) body
pure (Lambda var t)
abstractSyntax ctx (App {fun, arg}) = do
t <- abstractSyntaxBounds ctx fun
u <- abstractSyntaxBounds ctx arg
pure (App t u)
abstractSyntax ctx (Sigma {var, index, element}) = do
a <- abstractSyntaxBounds ctx index
b <- abstractSyntaxBounds (bind ctx var.val) element
pure (Sigma var a b)
abstractSyntax ctx (Pair {first, second}) = do
t <- abstractSyntaxBounds ctx first
u <- abstractSyntaxBounds ctx second
pure (Pair t u)
abstractSyntax ctx (First {arg}) = do
t <- abstractSyntaxBounds ctx arg
pure (Fst t)
abstractSyntax ctx (Second {arg}) = do
t <- abstractSyntaxBounds ctx arg
pure (Snd t)
abstractSyntax ctx Bool = pure Bool
abstractSyntax ctx True = pure True
abstractSyntax ctx False = pure False
abstractSyntax ctx (If {var, returnType, discriminant, true, false}) = do
a <- abstractSyntaxBounds (bind ctx var.val) returnType
t <- abstractSyntaxBounds ctx discriminant
f <- abstractSyntaxBounds ctx true
g <- abstractSyntaxBounds ctx false
pure (If var a t f g)
abstractSyntax ctx Top = pure Top
abstractSyntax ctx Point = pure Point
abstractSyntax ctx Bottom = pure Bottom
abstractSyntax ctx (Absurd {contradiction}) = do
t <- abstractSyntaxBounds ctx contradiction
pure (Absurd t)
abstractSyntax ctx (Equal {left, right}) = do
t <- abstractSyntaxBounds ctx left
u <- abstractSyntaxBounds ctx right
pure (Equal t u)
abstractSyntax ctx (Refl {value}) = do
t <- abstractSyntaxBounds ctx value
pure (Refl t)
abstractSyntax ctx (Transp {indexedType, oldIndex, value, newIndex, equality}) = do
a <- abstractSyntaxBounds ctx indexedType
t <- abstractSyntaxBounds ctx oldIndex
u <- abstractSyntaxBounds ctx value
t' <- abstractSyntaxBounds ctx newIndex
e <- abstractSyntaxBounds ctx equality
pure (Transp a t u t' e)
abstractSyntax ctx (Cast {oldType, newType, equality, value}) = do
a <- abstractSyntaxBounds ctx oldType
b <- abstractSyntaxBounds ctx newType
e <- abstractSyntaxBounds ctx equality
t <- abstractSyntaxBounds ctx value
pure (Cast a b e t)
abstractSyntax ctx (CastId {value}) = do
t <- abstractSyntaxBounds ctx value
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
|
