-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathRawSyntax.hs
109 lines (99 loc) · 4.52 KB
/
RawSyntax.hs
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
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
module RawSyntax where
import AbstractSyntax
import PrettyPrinting
-- Representation for printing
import Exp.Abs
import Control.Monad
import Data.String
import Data.HashMap.Strict (HashMap, (!))
import qualified Data.HashMap.Strict as HM
{- Intermediate raw instax -}
data ITerm
= IVS String
| IV String Int
| ILam String ITerm
| IAnn ITerm ITerm
| IApp ITerm ITerm
| ILAM String ITerm
| IAppi ITerm ITerm
| IIPair ITerm ITerm
| IFst ITerm
| ISnd ITerm
| IBeta
| IRho ITerm String ITerm ITerm
| IPit String ITerm ITerm
| IIPi String ITerm ITerm
| IIota String ITerm ITerm
| IId ITerm ITerm
| IU Int
deriving (Show)
{- Convert intermediate syntax into abstract syntax -}
-- Replace string variables with deBruijin indices
index :: String -> Int -> ITerm -> ITerm
index s n (IVS x) = if s == x then IV s n else IVS x
index s n (IV st x) = IV st x
index s n (ILam x d) = ILam x (index s (1 + n) (index x 0 d))
index s n (IAnn d d1) = IAnn (index s n d) (index s n d1)
index s n (IApp d d1) = IApp (index s n d) (index s n d1)
index s n (ILAM x d) = ILAM x (index s (1 + n) (index x 0 d))
index s n (IAppi d d1) = IAppi (index s n d) (index s n d1)
index s n (IIPair d d1) = IIPair (index s n d) (index s n d1)
index s n (IFst d) = IFst (index s n d)
index s n (ISnd d) = ISnd (index s n d)
index s n IBeta = IBeta
index s n (IRho d x tp d1) = IRho (index s n d) x (index s (1 + n) (index x 0 tp)) (index s n d1)
index s n (IPit x d d1) = IPit x (index s n d) (index s (1 + n) (index x 0 d1))
index s n (IIPi x d d1) = IIPi x (index s n d) (index s (1 + n) (index x 0 d1))
index s n (IIota x d d1) = IIota x (index s n d) (index s (1 + n) (index x 0 d1))
index s n (IId d x) = IId (index s n d) (index s n x)
index s n (IU i) = IU i
-- Convert intermediate syntax into abstract syntax
fromInter :: ITerm -> Proof ATerm
fromInter (IV s x) = return $ AV s x
fromInter (IVS x) = return $ AVS x
fromInter (ILam x d) = ALam x <$> fromInter d
fromInter (IApp d d1) = AApp <$> fromInter d <*> fromInter d1
fromInter (IAnn d d1) = AAnn <$> fromInter d <*> fromInter d1
fromInter (ILAM x d) = ALAM x <$> fromInter d
fromInter (IAppi d d1) = AAppi <$> fromInter d <*> fromInter d1
fromInter (IIPair d d1) = AIPair <$> fromInter d <*> fromInter d1
fromInter (IFst d) = AFst <$> fromInter d
fromInter (ISnd d) = ASnd <$> fromInter d
fromInter IBeta = return ABeta
fromInter (IRho d x tp d1) = ARho x <$> fromInter d <*> fromInter tp <*> fromInter d1
fromInter (IPit x d d1) = APi x <$> fromInter d <*> fromInter d1
fromInter (IIPi x d d1) = AIPi x <$> fromInter d <*> fromInter d1
fromInter (IIota x d d1) = AIota x <$> fromInter d <*> fromInter d1
fromInter (IId x y) = AId <$> fromInter x <*> fromInter y
fromInter (IU i) = return (AU i)
{- Convert concrete syntax into intermediate syntax -}
fromCon :: Exp -> Proof ITerm
fromCon (SLet d e) = proofError "TO DO: Implement let expressions"
fromCon (SLam [AOTele (AIdent e)] o) = ILam e <$> fromCon o
fromCon (SLam (AOTele (AIdent e) : l) o) = ILam e <$> fromCon (SLam l o)
fromCon (SLam [POTele (PTele (SVar (AIdent e)) t)] o)
= ILam e <$> (IAnn <$> fromCon t <*> fromCon o)
fromCon (SLam (POTele (PTele (SVar (AIdent e)) t) : l) o)
= ILam e <$> (IAnn <$> fromCon t <*> fromCon (SLam l o))
fromCon (SLami [AIdent e] o) = ILAM e <$> fromCon o
fromCon (SLami (AIdent e : l) o) = ILAM e <$> fromCon (SLami l o)
fromCon (SAppi a b) = IAppi <$> fromCon a <*> fromCon b
fromCon (SApp a b) = IApp <$> fromCon a <*> fromCon b
fromCon (SRho (SVar (AIdent e)) t a b) = IRho <$> fromCon a <*> return e <*> fromCon t <*> fromCon b
fromCon (SFst a) = IFst <$> fromCon a
fromCon (SSnd a) = ISnd <$> fromCon a
fromCon (SPair a b) = IIPair <$> fromCon a <*> fromCon b
fromCon SBeta = return IBeta
fromCon (SVar (AIdent e)) = return $ IVS e
fromCon (SFun a b) = IPit "" <$> fromCon a <*> fromCon b
fromCon (SPi [PTele (SVar (AIdent e)) t] o) = IPit e <$> fromCon t <*> fromCon o
fromCon (SPi (PTele (SVar (AIdent e)) t : l) o) = IPit e <$> fromCon t <*> fromCon (SPi l o)
fromCon (SIPi [ITele (SVar (AIdent e)) t] o) = IIPi e <$> fromCon t <*> fromCon o
fromCon (SIPi (ITele (SVar (AIdent e)) t : l) o) = IIPi e <$> fromCon t <*> fromCon (SIPi l o)
fromCon (SId a b) = IId <$> fromCon a <*> fromCon b
fromCon (SIota (PTele (SVar (AIdent e)) t) b) = IIota e <$> fromCon t <*> fromCon b
fromCon (SU (Lv e)) = return (IU (read e))
fromCon s = proofError ("Parsing Error: Cannot interpret " ++ show s ++ "." )
{- Convert Concrete Syntax into Abstract Syntax -}
convert :: Exp -> Proof ATerm
convert e = fromCon e >>= fromInter . index "" 0