git.iko.soy/Idris-dev
on master help sign in
Changed contexts to Data.Map
commitac25f15f9bc9b33d0e0a5ca9a7e0dc9819028984 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateMon 3 Oct 2011, 09:57 (15 years ago) parent575b043
5 files changed+39−30
compare with master
unifiedsplit
miniidris.cabal+2−1 src/Core.hs+1−1 src/Elaborate.hs+8−21 src/Evaluate.hs+25−5 src/Main.hs+3−2
miniidris.cabal+2−1
@@ -21,7 +21,8 @@ Executable miniidris
2121 ProofState, CoreParser, ShellParser,
2222 Unify, Elaborate
2323
24− Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline
24+ Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline,
25+ containers
2526
2627 Extensions: MultiParamTypeClasses, FunctionalDependencies,
2728 FlexibleInstances
src/Core.hs+1−1
@@ -54,7 +54,7 @@ instance MonadPlus TC where
5454
5555data Name = UN [String]
5656 | MN Int String
57− deriving Eq
57+ deriving (Eq, Ord)
5858
5959instance Show Name where
6060 show (UN [n]) = n
src/Elaborate.hs+8−21
@@ -191,24 +191,11 @@ arg n tyhole = do ty <- unique_hole tyhole
191191 claim ty (RSet 0)
192192 forall n (Var ty)
193193
194−-- patarg :: Name -> Name -> Elab ()
195−-- patarg n tyhole = do ty <- unique_hole tyhole
196−-- claim ty (RSet 0)
197−-- patvar n (Var ty)
198−
199−-- Some combinators on elaborations
200−
201−-- Sequencing
202−-- infixr 5 ==>
203−
204−-- (==>) :: Elab -> Elab -> Elab
205−-- (==>) t1 t2 ps = do (ps', log') <- t1 ps
206−-- (ps'', log'') <- t2 ps'
207−-- return (ps'', log' ++ log')
208−--
209−-- -- Try a tactic, if it fails, try another
210−-- try :: Elab -> Elab -> Elab
211−-- try t1 t2 ps = case t1 ps of
212−-- OK v -> return v
213−-- _ -> t2 ps
214−--
194+-- Try a tactic, if it fails, try another
195+try :: Elab a -> Elab a -> Elab a
196+try t1 t2 = do s <- get
197+ case runStateT t1 s of
198+ OK (v, s') -> do put s'
199+ return v
200+ _ -> t2
201+
src/Evaluate.hs+25−5
@@ -1,10 +1,11 @@
11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
22
33module Evaluate(normalise,
4− Fun(..), Def(..), Context,
4+ Fun(..), Def(..), Context, toAlist,
55 emptyContext, addToCtxt, addConstant, addDatatype,
66 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv) where
77
8+import qualified Data.Map as Map
89import Debug.Trace
910import Core
1011
@@ -97,6 +98,7 @@ data Def = Function Fun
9798 | Constant NameType Type Value
9899 deriving Show
99100
101+{-
100102type Context = [(Name, Def)]
101103
102104emptyContext = []
@@ -104,6 +106,24 @@ emptyContext = []
104106addDef :: Name -> Def -> Context -> Context
105107addDef n d ctxt = (n, d) : ctxt
106108
109+lookupCtxt :: Name -> Context -> Maybe Def
110+lookupCtxt n c = lookup n c
111+-}
112+
113+type Context = Map.Map Name Def
114+emptyContext = Map.empty
115+
116+addDef :: Name -> Def -> Context -> Context
117+addDef = Map.insert
118+
119+lookupCtxt :: Name -> Context -> Maybe Def
120+lookupCtxt = Map.lookup
121+
122+toAlist :: Context -> [(Name, Def)]
123+toAlist = Map.toList
124+
125+-------
126+
107127addToCtxt :: Name -> Term -> Type -> Context -> Context
108128addToCtxt n tm ty ctxt = addDef n (Function (Fun ty (eval ctxt [] ty)
109129 tm (eval ctxt [] tm))) ctxt
@@ -124,28 +144,28 @@ addDatatype (Data n ty cons) ctxt
124144 (Constant (DCon tag (arity ty')) ty (eval ctxt [] ty)) ctxt)
125145
126146lookupTy :: Name -> Context -> Maybe Type
127−lookupTy n ctxt = do def <- lookup n ctxt
147+lookupTy n ctxt = do def <- lookupCtxt n ctxt
128148 case def of
129149 (Function (Fun ty _ _ _)) -> return ty
130150 (Constant _ ty _) -> return ty
131151
132152lookupP :: Name -> Context -> Maybe Term
133153lookupP n ctxt
134− = do def <- lookup n ctxt
154+ = do def <- lookupCtxt n ctxt
135155 case def of
136156 (Function (Fun ty _ tm _)) -> return (P Ref n ty)
137157 (Constant nt ty hty) -> return (P nt n ty)
138158
139159lookupDef :: Name -> Context -> Maybe Term
140160lookupDef n ctxt
141− = do def <- lookup n ctxt
161+ = do def <- lookupCtxt n ctxt
142162 case def of
143163 (Function (Fun ty _ tm _)) -> return tm
144164 (Constant nt ty hty) -> return (P nt n ty)
145165
146166lookupVal :: Name -> Context -> Maybe Value
147167lookupVal n ctxt
148− = do def <- lookup n ctxt
168+ = do def <- lookupCtxt n ctxt
149169 case def of
150170 (Function (Fun _ _ _ htm)) -> return htm
151171 (Constant nt ty hty) -> return (VP nt n hty)
src/Main.hs+3−2
@@ -5,14 +5,15 @@ import ShellParser
55import Core
66import Typecheck
77import ProofShell
8+import Evaluate
89
910main = do f <- readFile "test.mi"
1011 case parseFile f of
1112 Left err -> print err
1213 Right defs -> do
1314 print defs
14− case checkProgram [] defs of
15− OK ctxt -> do print ctxt
15+ case checkProgram emptyContext defs of
16+ OK ctxt -> do print (toAlist ctxt)
1617 runShell (initState ctxt)
1718 return ()
1819 err -> print err