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
|
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
domain <- abstractSyntaxBounds ctx domain
codomain <- abstractSyntaxBounds (bind ctx var.val) codomain
pure (Pi {var, domain, codomain})
abstractSyntax ctx (Lambda {var, body}) = do
body <- abstractSyntaxBounds (bind ctx var.val) body
pure (Lambda {var, body})
abstractSyntax ctx (App {fun, arg}) = do
fun <- abstractSyntaxBounds ctx fun
arg <- abstractSyntaxBounds ctx arg
pure (App {fun, arg})
abstractSyntax ctx (Sigma {var, index, element}) = do
index <- abstractSyntaxBounds ctx index
element <- abstractSyntaxBounds (bind ctx var.val) element
pure (Sigma {var, index, element})
abstractSyntax ctx (Pair {first, second}) = do
first <- abstractSyntaxBounds ctx first
second <- abstractSyntaxBounds ctx second
pure (Pair {first, second})
abstractSyntax ctx (First {arg}) = do
arg <- abstractSyntaxBounds ctx arg
pure (First {arg})
abstractSyntax ctx (Second {arg}) = do
arg <- abstractSyntaxBounds ctx arg
pure (Second {arg})
abstractSyntax ctx Bool = pure Bool
abstractSyntax ctx True = pure True
abstractSyntax ctx False = pure False
abstractSyntax ctx (If {var, returnType, discriminant, true, false}) = do
returnType <- abstractSyntaxBounds (bind ctx var.val) returnType
discriminant <- abstractSyntaxBounds ctx discriminant
true <- abstractSyntaxBounds ctx true
false <- abstractSyntaxBounds ctx false
pure (If {var, returnType, discriminant, true, false})
abstractSyntax ctx Top = pure Top
abstractSyntax ctx Point = pure Point
abstractSyntax ctx Bottom = pure Bottom
abstractSyntax ctx (Absurd {contradiction}) = do
contradiction <- abstractSyntaxBounds ctx contradiction
pure (Absurd {contradiction})
abstractSyntax ctx (Equal {left, right}) = do
left <- abstractSyntaxBounds ctx left
right <- abstractSyntaxBounds ctx right
pure (Equal {left, right})
abstractSyntax ctx (Refl {value}) = do
value <- abstractSyntaxBounds ctx value
pure (Refl {value})
abstractSyntax ctx (Transp {indexedType, oldIndex, value, newIndex, equality}) = do
indexedType <- abstractSyntaxBounds ctx indexedType
oldIndex <- abstractSyntaxBounds ctx oldIndex
value <- abstractSyntaxBounds ctx value
newIndex <- abstractSyntaxBounds ctx newIndex
equality <- abstractSyntaxBounds ctx equality
pure (Transp {indexedType, oldIndex, value, newIndex, equality})
abstractSyntax ctx (Cast {oldType, newType, equality, value}) = do
oldType <- abstractSyntaxBounds ctx oldType
newType <- abstractSyntaxBounds ctx newType
equality <- abstractSyntaxBounds ctx equality
value <- abstractSyntaxBounds ctx value
pure (Cast {oldType, newType, equality, value})
abstractSyntax ctx (CastId {value}) = do
value <- abstractSyntaxBounds ctx value
pure (CastId {value})
abstractSyntaxBounds ctx val@(MkBounded v irrel bnds) = do
term <- inBounds $ (MkBounded (abstractSyntax ctx v) irrel bnds)
pure $ map (const term) val
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
|
