blob: ad1d0a7b7af4f03325b3ff6b3b52a2b40f2118c8 (
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
|
module Obs.Typing.Context
import Data.Fin
import public Data.List
import Data.List.Elem
import Obs.Logging
import Obs.NormalForm
import Obs.NormalForm.Normalise
import Obs.Substitution
import Obs.Universe
import Text.Bounded
-- Definitions -----------------------------------------------------------------
infix 5 ::<
public export
record FreeVar (ctx : List Relevance) where
constructor MkFreeVar
sort : Universe
ty : TypeNormalForm ctx
name : String
public export
record TyDef (b : Relevance) (ctx : List Relevance) where
constructor MkDefinition
name : String
sort : Universe
ty : TypeNormalForm ctx
tm : NormalForm (relevance sort) ctx
correct : relevance sort = b
public export
data TyContext : Unsorted.Family Relevance where
Nil : TyContext []
(:<) : TyContext ctx -> (def : Definition ctx) -> TyContext (relevance def.sort :: ctx)
(::<) : TyContext ctx -> (var : FreeVar ctx) -> TyContext (relevance var.sort :: ctx)
-- Properties ------------------------------------------------------------------
freeVars : TyContext ctx -> List Relevance
freeVars [] = []
freeVars (ctx :< def) = freeVars ctx
freeVars (ctx ::< var) = relevance var.sort :: freeVars ctx
Sorted.Rename Relevance TyDef where
rename def f = {ty := rename def.ty f, tm := rename def.tm f} def
-- Construction ----------------------------------------------------------------
fromDef : (def : Definition ctx) -> TyDef (relevance def.sort) ctx
fromDef def = MkDefinition
{ name = def.name.val
, sort = def.sort
, ty = def.ty
, tm = def.tm
, correct = Refl
}
fromVar : (var : FreeVar ctx) -> TyDef (relevance var.sort) (relevance var.sort :: ctx)
fromVar var = MkDefinition
{ name = var.name
, sort = var.sort
, ty = weaken [relevance var.sort] var.ty
, tm = point (Just var.name) Here
, correct = Refl
}
export
fromContext : Context ctx -> TyContext ctx
fromContext [] = []
fromContext (ctx :< def) = fromContext ctx :< def
-- Destruction -----------------------------------------------------------------
export
getContext : TyContext ctx -> (ctx' ** ctx = ctx')
getContext [] = ([] ** Refl)
getContext (ctx :< def) =
let (ctx' ** prf) = getContext ctx in
(relevance def.sort :: ctx' ** cong (relevance def.sort ::) prf)
getContext (ctx ::< var) =
let (ctx' ** prf) = getContext ctx in
(relevance var.sort :: ctx' ** cong (relevance var.sort ::) prf)
export
index : TyContext ctx -> Map ctx TyDef ctx
index [] = absurd
index (ctx :< def) = weaken [_] . add TyDef (fromDef def) (index ctx)
index (ctx ::< var) = add TyDef (fromVar var) (weaken [_] . index ctx)
finToElem : {xs : List a} -> (i : Fin (length xs)) -> Elem (index' xs i) xs
finToElem {xs = (x :: xs)} FZ = Here
finToElem {xs = (x :: xs)} (FS i) = There (finToElem i)
export
index' : TyContext ctx -> (i : Fin (length ctx)) -> TyDef (index' ctx i) ctx
index' ctx i = let (ctx' ** Refl) = getContext ctx in index ctx (finToElem i)
export
reduce : (tyCtx : TyContext ctx) -> Map ctx (LogNormalForm ann) (freeVars tyCtx)
reduce [] = absurd
reduce (ctx :< def) = add (LogNormalForm ann) (subst def.tm (reduce ctx)) (reduce ctx)
reduce (ctx ::< var) = add (LogNormalForm ann)
(pure $ point (Just var.name) Here)
(\i => pure $ weaken [_] $ !(reduce ctx i))
|
