blob: 10e74bb29422f1cacfc6bb62adb95821fe390733 (
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
|
module CC.Term.Raw
import CC.Name
import CC.Term
import Data.DPair
import Data.List1
import Text.Bounded
-- Definition ------------------------------------------------------------------
public export
data RawTerm : Type
public export
record RawBinding where
constructor Of
name : Maybe Name
bound : RawTerm
data RawTerm where
Bounded : WithBounds RawTerm -> RawTerm
Var : (n : Name) -> RawTerm
Let : Name -> Maybe RawTerm -> RawTerm -> RawTerm -> RawTerm
Set : RawTerm
Pi : RawBinding -> RawTerm -> RawTerm
Abs : (n : Maybe Name) -> RawTerm -> RawTerm
App : RawTerm -> RawTerm -> RawTerm
%name RawBinding bind
%name RawTerm t, u
-- Error Type ------------------------------------------------------------------
export
data NameError : Type -> Type where
Ok : ty -> NameError ty
Err : List1 Name -> NameError ty
export
Functor NameError where
map f (Ok v) = Ok (f v)
map f (Err errs) = Err errs
export
Applicative NameError where
pure = Ok
Ok f <*> Ok v = Ok (f v)
Ok f <*> Err ys = Err ys
Err xs <*> Ok v = Err xs
Err xs <*> Err ys = Err (xs ++ ys)
export
runNameError : NameError ty -> Either (List1 Name) ty
runNameError (Ok x) = Right x
runNameError (Err xs) = Left xs
-- Translation -----------------------------------------------------------------
export
lookup : (ctx : Context) -> (n : Name) -> NameError $ Subset Nat (\k => IsVar k n ctx)
lookup [<] n = Err (n ::: [])
lookup (ctx :< m) n =
case decEquiv n m of
Yes eq => Ok (Element 0 (Here eq))
No _ => map (\p => Element (S p.fst) (There p.snd)) (lookup ctx n)
|
