blob: a630fcbadd680dd88d6c4b0101913b0e30f02eb3 (
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
|
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 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
-- Properties ------------------------------------------------------------------
freeVars : Context 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
}
fromParam : (param : Parameter ctx) -> TyDef (relevance param.sort) (relevance param.sort :: ctx)
fromParam param = MkDefinition
{ name = param.name.val
, sort = param.sort
, ty = weaken [relevance param.sort] param.ty
, tm = point (Just param.name.val) Here
, correct = Refl
}
-- Destruction -----------------------------------------------------------------
export
getContext : Context 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 ::< param) =
let (ctx' ** prf) = getContext ctx in
(relevance param.sort :: ctx' ** cong (relevance param.sort ::) prf)
export
index : Context ctx -> Map ctx TyDef ctx
index [] = absurd
index (ctx :< def) = weaken [_] . add TyDef (fromDef def) (index ctx)
index (ctx ::< param) = add TyDef (fromParam param) (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' : Context 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 : Context ctx) -> Map ctx (LogNormalForm ann) (freeVars tyCtx)
reduce [] = absurd
reduce (ctx :< def) = add (LogNormalForm ann) (subst def.tm (reduce ctx)) (reduce ctx)
reduce (ctx ::< param) = add (LogNormalForm ann)
(pure $ point (Just param.name.val) Here)
(\i => pure $ weaken [_] $ !(reduce ctx i))
|
