SHARE
TWEET

Untitled

a guest Mar 21st, 2019 58 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    -- расширенный функциональный тип
  14.     deriving (Read,Show,Eq,Ord)
  15.  
  16. data Decl = EDecl Symb Expr
  17.     deriving (Read,Show,Ord)
  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. OK, I Understand
 
Top