blob: 62e2be7d085de342a5613c88adcf2f2f7e1c8763 (
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
|
module Term.Semantics
import Control.Monad.Identity
import Data.Nat
import Term
import public Data.SnocList.Quantifiers
public export
TypeOf : Ty -> Type
TypeOf N = Nat
TypeOf (ty ~> ty') = TypeOf ty -> TypeOf ty'
rec : Nat -> a -> (a -> a) -> a
rec 0 x f = x
rec (S k) x f = f (rec k x f)
%inline
init : All p (sx :< x) -> All p sx
init (psx :< px) = psx
%inline
mapInit : (All p sx -> All p sy) -> All p (sx :< z) -> All p (sy :< z)
mapInit f (psx :< px) = f psx :< px
restrict : Applicative m => sx `Thins` sy -> m (All p sy -> All p sx)
restrict Id = pure id
restrict Empty = pure (const [<])
restrict (Drop thin) = [| restrict thin . [| init |] |]
restrict (Keep thin) = [| mapInit (restrict thin) |]
%inline
indexVar : All p [<x] -> p x
indexVar [<px] = px
%inline
opSem : Operator tys ty -> TypeOf (foldr (~>) ty tys)
opSem (Lit n) = n
opSem Suc = S
opSem Plus = (+)
opSem Mult = (*)
opSem Pred = pred
opSem Minus = minus
opSem Div = div
opSem Mod = mod
%inline
sem' : Monad m => Term ty ctx -> m (All TypeOf ctx -> TypeOf ty)
fullSem' : Monad m => FullTerm ty ctx -> m (All TypeOf ctx -> TypeOf ty)
sem' (t `Over` thin) = [| fullSem' t . restrict thin |]
fullSem' Var = pure indexVar
fullSem' (Const t) = do
t <- fullSem' t
pure (const . t)
fullSem' (Abs t) = do
t <- fullSem' t
pure (t .: (:<))
fullSem' (App (MakePair t u _)) = do
t <- sem' t
u <- sem' u
pure (\ctx => t ctx (u ctx))
fullSem' (Op op) = pure (const $ opSem op)
fullSem' (Rec (MakePair t (MakePair u v _ `Over` thin) _)) = do
t <- sem' t
u <- sem' u
v <- sem' v
f <- restrict thin
pure
(\ctx =>
let ctx' = f ctx in
rec (t ctx) (u ctx') (v ctx'))
export
sem : Term ty ctx -> All TypeOf ctx -> TypeOf ty
sem t = runIdentity (sem' t)
|
