← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/transl/agda/CITrans.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/CITrans.hs
1
 
module CITrans where
2
 
--import UIdInfo
3
 
import Position(noPosition)
4
 
import Id(Id, UId, getIdPosition, addId, remId, SymTab, rangeST, initST, lookupST,toId)
5
 
import Monads
6
 
import Error
7
 
import PPrint(ppReadable)
8
 
 
9
 
type CITrans = (SymTab,   -- free + case-bound vars
10
 
                SymTab,   -- consts
11
 
                [UId],    -- case-bound vars
12
 
                Maybe     -- if in the rhs ... (not quite.) ..
13
 
                (UId,     -- current const being defined.
14
 
                 [UId]))  -- its tel vars + lambda vars after it
15
 
                          -- i.e, those vars whose values are to be printed
16
 
                          -- together with the const.  IN TEL ORDER.
17
 
 
18
 
 
19
 
freeVarScope :: CITrans -> [UId]
20
 
freeVarScope (vst,cst,cb,_) =   [x | x <- rangeST vst, x `notElem` cb]
21
 
 
22
 
 
23
 
varScope :: CITrans -> [UId]
24
 
varScope (vst,cst,cb,_) =  rangeST vst
25
 
 
26
 
 
27
 
cstScope :: CITrans -> [UId]
28
 
cstScope (vst,cst,cb,_) =  rangeST cst
29
 
 
30
 
caseVarScope :: CITrans -> [UId]
31
 
caseVarScope (vst,cst,cb,_) = cb
32
 
 
33
 
currentConstPV :: CITrans -> Maybe (UId,[UId])
34
 
currentConstPV (_,_,_,cpvs) = cpvs
35
 
 
36
 
 
37
 
scope :: CITrans -> [UId]
38
 
scope (vst,cst,cb,_) =  rangeST vst ++ rangeST cst
39
 
 
40
 
addVar :: Id -> UId -> CITrans -> CITrans
41
 
addVar x x' (vst,cst,cb,cpvs) = let vst' = addId x x' vst
42
 
                                    cst' = remId x cst
43
 
                           in (vst',cst',cb,cpvs)
44
 
 
45
 
addCst ::  Id ->  UId -> CITrans -> CITrans
46
 
addCst c c' (vst,cst,cb,cpvs) = let cst' = addId c c' cst
47
 
                                    vst' = remId c vst
48
 
                           in (vst',cst',cb,cpvs)
49
 
 
50
 
addCsts ::  [(Id,UId)] -> CITrans -> CITrans
51
 
addCsts ccs cit = foldr (uncurry addCst) cit ccs
52
 
 
53
 
 
54
 
 
55
 
addCaseVar :: UId -> CITrans -> CITrans
56
 
addCaseVar x (vst,cst,cb,cpvs) = (vst,cst,x:cb,cpvs)
57
 
 
58
 
updateCCPV :: UId -> [UId] -> CITrans -> CITrans
59
 
updateCCPV cc pvs (vst,cst,cb,_) = (vst,cst,cb, Just (cc,pvs))
60
 
 
61
 
addPV :: [UId] -> CITrans -> CITrans
62
 
addPV xs (vst,cst,cb, Just (cc,pvs)) = (vst,cst,cb, Just (cc,pvs++xs))
63
 
addPV xs cit@(_,_,_,Nothing) = cit
64
 
  -- this happens when Clam is in the lhs.
65
 
 
66
 
lookupId :: CITrans -> Id -> Error (Either UId UId)
67
 
lookupId (vst,cst,cb,_) i = case lookupST vst i of
68
 
                           Just x -> return (Left x)
69
 
                           Nothing -> case lookupST cst i of
70
 
                                         Just c -> return (Right c)
71
 
                                         Nothing -> raise (scopeError i)
72
 
 
73
 
lookupVar :: CITrans -> Id -> Error UId
74
 
lookupVar (vst,cst,_,_) x = liftMaybeE (lookupST vst x) (scopeError x)
75
 
 
76
 
lookupCst :: CITrans -> Id -> Error UId
77
 
lookupCst (vst,cst,_,_) c = liftMaybeE (lookupST cst c) (scopeError c)
78
 
 
79
 
 
80
 
 
81
 
scopeError :: Id -> EMsg
82
 
scopeError i = eMsg (getIdPosition i) (EUnbound (ppReadable i))
83
 
 
84
 
 
85
 
getCstSymTab :: CITrans -> SymTab
86
 
getCstSymTab (_,cst,_,_) = cst
87
 
 
88
 
getVarSymTab :: CITrans -> SymTab
89
 
getVarSymTab (vst,_,_,_) = vst
90
 
 
91
 
getCaseBoundVar :: CITrans -> [UId]
92
 
getCaseBoundVar (_,_,cb,_) = cb
93
 
 
94
 
initCIT :: CITrans
95
 
initCIT = (initST,initST,[],dummyCCPV "initCIT:")
96
 
 
97
 
initCIT_CST :: SymTab -> CITrans
98
 
initCIT_CST st = (initST,st,[],dummyCCPV "initCIT:")
99
 
 
100
 
 
101
 
 
102
 
dummyCCPV::String -> Maybe (UId,[UId])
103
 
dummyCCPV s = Nothing
104
 
 
105
 
 
106
 
inScopeVar :: CITrans -> UId -> Bool
107
 
inScopeVar (vst,_,_,_) x = maybe False (x==) (lookupST vst (toId x))
108
 
 
109
 
 
110
 
inScopeCst :: CITrans -> UId -> Bool
111
 
inScopeCst (_,cst,_,_) x = maybe False (x==) (lookupST cst (toId x))