• API
• FAQ
• Tools
• Archive
daily pastebin goal
22%
SHARE
TWEET

# Untitled

a guest Mar 21st, 2019 57 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
1. import Data.Maybe (maybe)
2.
3. type Symb = String
4.
5. infixl 4 :@:
6. infixr 3 >-> -- теперь просто функция
7.
8. data Expr = Idx Int
9.           | Ast
10.           | Box
11.           | Expr :@: Expr
12.           | Lmb Decl Expr
13.           | Pi Decl Expr    -- расширенный функциональный тип
15.
16. data Decl = EDecl Symb Expr
18.
19. instance Eq Decl where
20.   EDecl _ t1 == EDecl _ t2 = t1 == t2
21.
22. type Env = [Decl]
23.
24. lE, pE :: Symb -> Expr -> Expr -> Expr
25. lE v = Lmb . EDecl v
26. pE v = Pi  . EDecl v
27.
28. (>->) :: Expr -> Expr -> Expr
29. a >-> b = pE "_" a (shift 1 b)
30. ----------------------
31.
32. isConst e = e == Ast || e == Box
33.
34. validEnv :: Env -> Bool
35. validEnv [] = True
36. validEnv (EDecl _ expr:ctx) = maybe False isConst (infer ctx expr) && validEnv ctx
37.
38. shift :: Int -> Expr -> Expr
39. shift = shift' 0
40.
41. shift' k v Ast = Ast
42. shift' k v Box = Box
43. shift' k v (Idx i) = Idx \$ if i < k then i else i + v
44. shift' k v (t1 :@: t2) = shift' k v t1 :@: shift' k v t2
45. shift' k v (Lmb (EDecl s e) t) = Lmb (EDecl s \$ shift' k v e) \$ shift' (k + 1) v t
46. shift' k v (Pi (EDecl n t1) t2) = Pi (EDecl n \$ shift' k v t1) (shift' (k + 1) v t2)
47.
48. subst :: Int -> Expr -> Expr -> Expr
49. subst _ _ Ast = Ast
50. subst _ _ Box = Box
51. subst i e idx@(Idx j) = if i == j then e else idx
52. subst i e (t1 :@: t2) = subst i e t1 :@: subst i e t2
53. subst i e (Lmb (EDecl n ex) t) = Lmb (EDecl n \$ subst i e ex) \$ subst (i + 1) (shift 1 e) t
54. subst j e (Pi (EDecl n ex) t) = Pi (EDecl n \$ subst j e ex) \$ subst (j + 1) (shift 1 e) t
55.
56. infer :: Env -> Expr -> Maybe Expr
57. infer en ex = if validEnv en then infer' en ex else Nothing
58.
59. infer' _ Ast = Just Box
60. infer' en (Idx i)
61.   | 0 <= i && i < length en,
62.     (EDecl _ ex) <- en !! i
63.   = Just \$ shift (i + 1) ex
64. infer' en (Pi d@(EDecl _ ex) b)
65.   | Just Ast <- infer' en ex,
66.     Just s   <- infer' (d : en) b,
67.     isConst s
68.   = Just s
69. infer' en (t1 :@: t2)
70.   | Just (Pi (EDecl _ ex) b) <- nf <\$> infer' en t1,
71.     Just ex' <- infer' en t2,
72.     nf ex == nf ex'
73.   = Just \$ shift (-1) \$ subst 0 (shift 1 t2) b
74. infer' en (Lmb d@(EDecl _ e) m)
75.   | Just Ast <- infer' en e,
76.     Just b <- infer (d : en) m
77.   = Just \$ Pi d b
78. infer' _ _ = Nothing
79.
80.
81. infer0 :: Expr -> Maybe Expr
82. infer0 = infer []
83.
84. isNF (Lmb (EDecl _ ex) t) = isNF ex && isNF t
85. isNF x = isNANF x
86.
87. isNANF (Idx _) = True
88. isNANF (t1 :@: t2) = isNANF t1 && isNF t2
89. isNANF (Pi (EDecl _ ex) b) = isNF ex && isNF b
90. isNANF e = isConst e
91.
92. isNA (Idx _)   = True
93. isNA (_ :@: _) = True
94. isNA (Pi _ _) = True
95. isNA _ = False
96.
97. oneStep :: Expr -> Maybe Expr
98. oneStep (t1 :@: t2)
99.   | isNA t1,
100.     Just t1' <- oneStep t1
101.   = Just \$ t1' :@: t2
102.   | isNANF t1,
103.     Just t2' <- oneStep t2
104.   = Just \$ t1 :@: t2'
105. oneStep (Lmb (EDecl name a) m)
106.   | Just a' <- oneStep a = Just \$ Lmb (EDecl name a') m
107.   | isNF a, Just m' <- oneStep m = Just \$ Lmb (EDecl name a)  m'
108. oneStep (Lmb (EDecl _ _) t1 :@: t2) = Just \$ shift (-1) \$ subst 0 (shift 1 t2) t1
109. oneStep (Pi (EDecl s ex) b)
110.   | Just ex' <- oneStep ex
111.   = Just \$ Pi (EDecl s ex') b
112.   | isNF ex,
113.     Just b' <- oneStep b
114.   = Just \$ Pi (EDecl s ex) b'
115.
116.
117. oneStep _ = Nothing
118.
119. nf :: Expr -> Expr
120. nf t = case oneStep t of
121.   Just t1 -> nf t1
122.   Nothing -> t
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.

Top