← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to src/transl/agda/ISynEnv.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/transl/agda/ISynEnv.hs
1
 
module ISynEnv  where
2
 
 
3
 
import Data.List
4
 
import Id(UId,isDummyUId,SymTab)
5
 
import Position(Position,noPosition)
6
 
import ISynType
7
 
--import CITrans(CITrans,initCIT_CST)
8
 
 
9
 
type MValue = Exp   -- A value where the meta variables are evaluated
10
 
 
11
 
 
12
 
data Judgement a  = IsType a
13
 
                  | a :! Value
14
 
                  --deriving Show
15
 
 
16
 
type Context = [(UId,Exp)]    -- Context is in reverse order of Tel
17
 
 
18
 
type TCEnv = (Context,Environment)
19
 
 
20
 
emptyEnv :: Environment
21
 
emptyEnv = E ([],[])
22
 
 
23
 
update :: Env ->  UId -> Value -> Env
24
 
update env x v = (x,v):env
25
 
 
26
 
updateEnv :: Environment -> UId -> Value -> Environment
27
 
updateEnv (E (env,sigma)) x v = E (update env x v,sigma)
28
 
 
29
 
updateEnvMany :: Environment -> [(UId,Value)] -> Environment
30
 
updateEnvMany = foldl (\env -> uncurry (updateEnv env))
31
 
 
32
 
updatesEnv :: Environment -> [(Bool,UId)] -> [(Bool,Value)] -> (Environment,[(Bool,UId)],[(Bool,Value)])
33
 
updatesEnv env ((_,x):xs) ((_,v):vs) = updatesEnv (updateEnv env x v) xs vs
34
 
updatesEnv env xs vs = (env,xs,vs)
35
 
 
36
 
updatesEnv' :: Environment -> [(Bool,UId)] -> [Value] -> (Environment,[(Bool,UId)],[Value])
37
 
updatesEnv' env ((_,x):xs) (v:vs) = updatesEnv' (updateEnv env x v) xs vs
38
 
updatesEnv' env xs vs = (env,xs,vs)
39
 
 
40
 
addIdEnv :: Environment -> [UId] -> [UId] -> Environment
41
 
addIdEnv env [] _ = env
42
 
addIdEnv env (x:xs) (x':xs') = addIdEnv (updateEnv env x (EVar x' Nothing)) xs xs'
43
 
addIdEnv _   _       _       = error "addIdEnv: "
44
 
 
45
 
addHIdEnv :: Environment -> [(Bool,UId)] -> [(Bool,UId)] -> Environment
46
 
addHIdEnv env [] _ = env
47
 
addHIdEnv env ((_,x):xs) ((_,x'):xs') = addHIdEnv (updateEnv env x (EVar x' Nothing)) xs xs'
48
 
addHIdEnv _   _       _       = error "addHIdEnv: "
49
 
 
50
 
lookupE :: Env -> UId -> Maybe Value
51
 
lookupE env x = lookup x env
52
 
 
53
 
 
54
 
retrieveE :: Environment -> [UId] -> Environment
55
 
retrieveE env xs = env
56
 
 
57
 
--retrieveE (E (_,sigma)) []  =  E ([],sigma)
58
 
--retrieveE env (x:xs) = let env' = retrieveE env xs
59
 
 
60
 
domEnv :: Environment -> [UId]
61
 
domEnv (E (env,_)) = nub $ map fst env
62
 
 
63
 
accessible :: Environment -> [UId]
64
 
accessible (E (_,sigma)) = sigma
65
 
 
66
 
addAccessible :: Environment -> UId -> Environment
67
 
addAccessible (E (env,sigma)) c = E (env,(c:sigma))
68
 
 
69
 
resetAccessible (E (env,_)) = E (env,[])
70
 
 
71
 
emptyC :: Context
72
 
emptyC = []
73
 
 
74
 
addC :: Context -> UId -> Exp  -> Context
75
 
addC gamma x e = (x,e):gamma
76
 
 
77
 
addDeclC  :: Context -> Decl -> Context
78
 
addDeclC gamma (xs,a) = foldr (\(_,x) -> \gamma -> (x,a):gamma) gamma xs
79
 
 
80
 
 
81
 
domC :: Context -> [UId]
82
 
domC gamma = map fst gamma
83
 
 
84
 
lookupC :: UId -> Context -> Maybe Exp
85
 
lookupC x gamma = lookup x gamma
86
 
 
87
 
appendCT :: Context -> Tel -> Context
88
 
appendCT gamma [] = gamma
89
 
appendCT gamma (d:tel) =  appendCT (addDeclC gamma d) tel
90
 
 
91
 
typeOfJudg :: Judgement a -> Value
92
 
typeOfJudg (a :! v) = v
93
 
typeOfJudg _        = (ESort noPosition (Sort 1))
94
 
 
95
 
mapJudg :: (a -> b) -> Judgement a -> Judgement b
96
 
mapJudg f (IsType a) = IsType (f a)
97
 
mapJudg f (a :! v) = (f a) :! v
98
 
 
99
 
 
100
 
env :: TCEnv -> Environment
101
 
env (_,rho) = rho
102
 
 
103
 
ctx :: TCEnv -> Context
104
 
ctx (gamma,_) = gamma
105
 
 
106
 
 
107
 
emptyTCEnv :: TCEnv
108
 
emptyTCEnv = (emptyC,emptyEnv)
109
 
 
110
 
 
111
 
addAbsConst :: TCEnv -> UId -> TCEnv
112
 
addAbsConst (gamma,env) c = (gamma,addAccessible env c)
113
 
 
114
 
{- still used in (now broken) import -}
115
 
resetAbs :: TCEnv -> TCEnv
116
 
resetAbs (gamma,env) = (gamma,resetAccessible env)
117
 
 
118
 
 
119
 
breakTCEnv::TCEnv -> [UId] -> (TCEnv,TCEnv)
120
 
breakTCEnv ce@(g,E(r,sigma)) us = let
121
 
     (g2,g1) = (\ (x,y) -> (reverse x, reverse y))
122
 
             . break ((`elem` us). fst) . reverse  $ g
123
 
     dom1    = map fst g1
124
 
     (r1,r2) = partition ((`elem` dom1).fst) r
125
 
     (s1,s2) = partition (`elem` dom1) sigma
126
 
  in ((g1,E(r1,s1)),(g2,E(r2,s2)))
127
 
 
128
 
addBind::TCEnv -> Bind -> TCEnv
129
 
addBind (g,r) b@(hxs,_) = let (_,xs) = unzip hxs
130
 
                          in (addDeclC g b, addIdEnv r xs xs)
131
 
 
132
 
addBind1 (g,r) x a = (addC g x a, updateEnv r x (EVar x Nothing))
133
 
 
134
 
 
135
 
catEnv::Environment -> Environment -> Environment
136
 
catEnv (E(r1,s1)) (E( r2,s2)) = E (r1 ++ r2, s1 `union` s2)
137
 
 
138
 
 
139
 
listEnv::Environment -> [(UId,Value)]
140
 
listEnv (E(env, _)) = env
141
 
 
142
 
 
143
 
 
144
 
shrinkEnv:: Environment -> [UId] -> Environment
145
 
shrinkEnv (E (xvs, acs)) xs = E (xvs', acs \\ xs)
146
 
          where xvs' = filter (\(key,_) ->  key `notElem` xs) xvs
147
 
 
148
 
 
149
 
rangeEnv :: Environment -> [Value]
150
 
rangeEnv (E(xvs  ,_)) = map snd xvs