git.iko.soy/Idris-dev
on master help sign in
Pattern matcher, evaluation of 2+2 now works
commitc637850551e25e41361c6b6c06ff9c10c9dfbd9e authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSun 9 Oct 2011, 09:12 (15 years ago) parent17e22af
11 files changed+385−83
compare with master
unifiedsplit
decls.mi+7−1 miniidris.cabal+1 src/Core/CaseTree.hs+187 src/Core/Evaluate.hs+70−14 src/Core/TT.hs+39−2 src/Core/Typecheck.hs−29 src/Idris/AbsSyntax.hs+24−14 src/Idris/ElabDecls.hs+38−13 src/Idris/Parser.hs+4−4 src/Idris/REPL.hs+7−1 src/Main.hs+8−5
decls.mi+7−1
@@ -1,7 +1,7 @@
11infixl 5 +, - ;
22infixl 6 *, / ;
33
4−infixl 7 :: ;
4+infixr 7 :: ;
55
66data Nat = O | S Nat;
77data List a = Nil | Cons a (List a);
@@ -22,6 +22,12 @@ app : Vect a n -> Vect a m -> Vect a (plus n m);
2222app VNil ys = ys;
2323app (x :: xs) ys = x :: app xs ys;
2424
25+test : Nat -> Vect Nat (S (S O));
26+test n = n :: n :: VNil;
27+
28+tvect : Vect Nat (S (S (S (S O))));
29+tvect = app (test O) (test (S O));
30+
2531infixl 5 .+. ;
2632
2733(.+.) : Nat -> Nat -> Nat;
miniidris.cabal+1
@@ -20,6 +20,7 @@ Executable miniidris
2020 Other-modules: Core.TT, Core.Evaluate, Core.Typecheck,
2121 Core.ProofShell, Core.ProofState, Core.CoreParser,
2222 Core.ShellParser, Core.Unify, Core.Elaborate,
23+ Core.CaseTree,
2324
2425 Idris.AbsSyntax, Idris.Parser, Idris.REPL,
2526 Idris.REPLParser, Idris.ElabDecls
src/Core/CaseTree.hsnew file+187
@@ -0,0 +1,187 @@
1+module Core.CaseTree(CaseDef(..), SC(..), CaseAlt(..), CaseTree,
2+ simpleCase) where
3+
4+import Core.TT
5+-- import Core.Evaluate
6+
7+import Control.Monad.State
8+
9+data CaseDef = CaseDef [Name] SC
10+ deriving Show
11+
12+data SC = Case Name [CaseAlt]
13+ | STerm Term
14+ | UnmatchedCase String -- error message
15+ deriving Show
16+
17+type Const = Int -- TMP until constants implemented
18+
19+data CaseAlt = ConCase Name Int [Name] SC
20+ | ConstCase Const SC
21+ | DefaultCase SC
22+ deriving Show
23+
24+type CaseTree = SC
25+type Clause = ([Pat], Term)
26+type CS = Int
27+
28+simpleCase :: [(Term, Term)] -> CaseDef
29+simpleCase [] = CaseDef [] (UnmatchedCase "No pattern clauses")
30+simpleCase cs = let pats = map (\ (l, r) -> (toPats l, r)) cs
31+ numargs = length (fst (head pats))
32+ ns = take numargs args in
33+ CaseDef ns (evalState (match ns pats (UnmatchedCase "Error")) numargs)
34+ where args = map (\i -> MN i "e") [0..]
35+
36+data Pat = PCon Name Int [Pat]
37+ | PConst Const
38+ | PV Name
39+ | PAny
40+ deriving Show
41+
42+toPats :: Term -> [Pat]
43+toPats f = map toPat (reverse (getArgs f)) where
44+ getArgs (App f a) = a : getArgs f
45+ getArgs _ = []
46+
47+toPat :: Term -> Pat
48+toPat tm = evalState (toPat' tm []) []
49+ where
50+ toPat' (P (DCon t a) n _) args = return $ PCon n t args
51+ toPat' (P Bound n _) [] = do ns <- get
52+ if n `elem` ns
53+ then return PAny
54+ else return (PV n)
55+ toPat' (App f a) args = do a' <- toPat' a []
56+ toPat' f (a' : args)
57+ toPat' _ _ = return PAny
58+
59+data Partition = Cons [Clause]
60+ | Vars [Clause]
61+
62+isVarPat (PV _ : ps , _) = True
63+isVarPat (PAny : ps , _) = True
64+isVarPat _ = False
65+
66+isConPat (PCon _ _ _ : ps, _) = True
67+-- constants too
68+isConPat _ = False
69+
70+partition :: [Clause] -> [Partition]
71+partition [] = []
72+partition ms@(m : _)
73+ | isVarPat m = let (vars, rest) = span isVarPat ms in
74+ Vars vars : partition rest
75+ | isConPat m = let (cons, rest) = span isConPat ms in
76+ Cons cons : partition rest
77+partition xs = error $ "Partition " ++ show xs
78+
79+match :: [Name] -> [Clause] -> SC -- error case
80+ -> State CS SC
81+match [] (([], ret) : _) err = return $ STerm ret -- run out of arguments
82+match vs cs err = mixture vs (partition cs) err
83+
84+mixture :: [Name] -> [Partition] -> SC -> State CS SC
85+mixture vs [] err = return err
86+mixture vs (Cons ms : ps) err = do fallthrough <- mixture vs ps err
87+ conRule vs ms fallthrough
88+mixture vs (Vars ms : ps) err = do fallthrough <- mixture vs ps err
89+ varRule vs ms fallthrough
90+
91+data ConType = CName Name Int -- named constructor
92+ | CConst Const -- constant, not implemented yet
93+
94+data Group = ConGroup ConType -- Constructor
95+ [([Pat], Clause)] -- arguments and rest of alternative
96+
97+conRule :: [Name] -> [Clause] -> SC -> State CS SC
98+conRule (v:vs) cs err = do groups <- groupCons cs
99+ caseGroups (v:vs) groups err
100+
101+caseGroups :: [Name] -> [Group] -> SC -> State CS SC
102+caseGroups (v:vs) gs err = do g <- altGroups gs
103+ return $ Case v g
104+ where
105+ altGroups [] = return [DefaultCase err]
106+ altGroups (ConGroup (CName n i) args : cs)
107+ = do g <- altGroup n i args
108+ rest <- altGroups cs
109+ return (g : rest)
110+ altGroups (ConGroup (CConst c) args : cs)
111+ = do g <- altConstGroup c args
112+ rest <- altGroups cs
113+ return (g : rest)
114+
115+ altGroup n i gs = do (newArgs, nextCs) <- argsToAlt gs
116+ matchCs <- match (newArgs ++ vs) nextCs err
117+ return $ ConCase n i newArgs matchCs
118+ altConstGroup n gs = do (_, nextCs) <- argsToAlt gs
119+ matchCs <- match vs nextCs err
120+ return $ ConstCase n matchCs
121+
122+argsToAlt :: [([Pat], Clause)] -> State CS ([Name], [Clause])
123+argsToAlt [] = return ([], [])
124+argsToAlt rs@((r, m) : _)
125+ = do newArgs <- getNewVars r
126+ return (newArgs, addRs rs)
127+ where
128+ getNewVars [] = return []
129+ getNewVars ((PV n) : ns) = do nsv <- getNewVars ns
130+ return (n : nsv)
131+ getNewVars (_ : ns) = do v <- getVar
132+ nsv <- getNewVars ns
133+ return (v : nsv)
134+ addRs [] = []
135+ addRs ((r, (ps, res)) : rs) = ((r++ps, res) : addRs rs)
136+
137+getVar :: State CS Name
138+getVar = do v <- get; put (v+1); return (MN v "e")
139+
140+groupCons :: [Clause] -> State CS [Group]
141+groupCons cs = gc [] cs
142+ where
143+ gc acc [] = return acc
144+ gc acc ((p : ps, res) : cs) =
145+ do acc' <- addGroup p ps res acc
146+ gc acc' cs
147+ addGroup p ps res acc = case p of
148+ PCon con i args -> return $ addg con i args (ps, res) acc
149+ PConst cval -> return $ addConG cval (ps, res) acc
150+ pat -> fail $ show pat ++ " is not a constructor or constant (can't happen)"
151+
152+ addg con i conargs res [] = [ConGroup (CName con i) [(conargs, res)]]
153+ addg con i conargs res (g@(ConGroup (CName n j) cs):gs)
154+ | i == j = ConGroup (CName n i) (cs ++ [(conargs, res)]) : gs
155+ | otherwise = g : addg con i conargs res gs
156+
157+ addConG con res [] = [ConGroup (CConst con) [([], res)]]
158+ addConG con res (g@(ConGroup (CConst n) cs) : gs)
159+ | con == n = ConGroup (CConst n) (cs ++ [([], res)]) : gs
160+ | otherwise = g : addConG con res gs
161+
162+varRule :: [Name] -> [Clause] -> SC -> State CS SC
163+varRule (v : vs) alts err =
164+ do let alts' = map (repVar v) alts
165+ match vs alts' err
166+ where
167+ repVar v (PV p : ps , res) = (ps, subst p (P Bound v undefined) res)
168+ repVar v (PAny : ps , res) = (ps, res)
169+
170+{-
171+mkOperator :: CaseDef -> [Value] -> Maybe Value
172+mkOperator (CaseDef ns casetree) args
173+ | length args /= length ns = Nothing
174+ | otherwise = evalArgs (zip ns args) casetree
175+ where
176+ evalArgs map (Case n alts) =
177+ do v <- lookup n map
178+ (altmap, tm) <- findAlt (getValArgs v) alts map
179+ evalArgs altmap tm
180+ evalArgs map (STerm tm) =
181+ evalArgs map (UnmatchedCase _) = Nothing
182+
183+ getValArgs tm = getValArgs' tm []
184+ getValArgs' (VApp f a) as = getValArgs' f (a:as)
185+ getValArgs' f as = (f, as)
186+
187+-}
src/Core/Evaluate.hs+70−14
@@ -3,11 +3,14 @@
33
44module Core.Evaluate(normalise,
55 Fun(..), Def(..), Context,
6− addToCtxt, addConstant, addDatatype,
7− lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv) where
6+ addToCtxt, addConstant, addDatatype, addCasedef,
7+ lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv,
8+ Value) where
89
910import Debug.Trace
11+
1012import Core.TT
13+import Core.CaseTree
1114
1215-- VALUES (as HOAS) ---------------------------------------------------------
1316
@@ -49,8 +52,10 @@ eval :: Context -> Env -> TT Name -> Value
4952eval ctxt genv tm = ev [] tm where
5053 ev env (P Bound n ty)
5154 | Just (Let t v) <- lookup n genv = ev env v
52− ev env (P Ref n ty)
53− | Just v <- lookupVal n ctxt = v
55+ ev env (P Ref n ty) = case lookupDef n ctxt of
56+ Just (Function (Fun _ _ _ v)) -> v
57+ Just (Constant nt ty hty) -> VP nt n hty
58+ _ -> VP Ref n (ev env ty)
5459 ev env (P nt n ty) = VP nt n (ev env ty)
5560 ev env (V i) | i < length env = env !! i
5661 | otherwise = error $ "Internal error: V" ++ show i
@@ -67,12 +72,57 @@ eval ctxt genv tm = ev [] tm where
6772 evApply env args f = apply env (ev env f) args
6873
6974 apply env (VBind n (Lam t) sc) (a:as) = wknV (-1) $ apply env (sc (ev env a)) as
75+ apply env (VP Ref n ty) args
76+ | Just (CaseOp _ ns tree) <- lookupDef n ctxt
77+ = case evCase env ns args tree of
78+ Nothing -> unload env (VP Ref n ty) args
79+ Just v -> v
7080 apply env f (a:as) = unload env f (a:as)
7181 apply env f [] = f
7282
7383 unload env f [] = f
7484 unload env f (a:as) = unload env (VApp f (ev env a)) as
7585
86+ evCase env ns args tree
87+ | length ns == length args
88+ = evTree env (zipWith (\n t -> (n, ev env t)) ns args) tree
89+ | otherwise = Nothing
90+
91+ evTree :: [Value] -> [(Name, Value)] -> SC -> Maybe Value
92+ evTree env amap (UnmatchedCase str) = Nothing
93+ evTree env amap (STerm tm)
94+ = Just $ ev (map snd amap ++ env) (pToVs (map fst amap) tm)
95+ evTree env amap (Case n alts)
96+ = do v <- lookup n amap
97+ (altmap, sc) <- chooseAlt v (getValArgs v) alts amap
98+ evTree env altmap sc
99+
100+ chooseAlt :: Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->
101+ Maybe ([(Name, Value)], SC)
102+ chooseAlt _ (VP (DCon i a) _ _, args) alts amap
103+ | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
104+ | Just sc <- findDefault alts = Just (amap, sc)
105+-- chooseAlt v _ alts amap
106+-- | Just sc <- safeDefault alts = Just (amap, sc)
107+ chooseAlt _ _ _ _ = Nothing
108+
109+ -- Replace old variable names in the map with new matches
110+ -- (This is possibly unnecessary since we make unique names and don't
111+ -- allow repeated variables...?)
112+ updateAmap newm amap
113+ = newm ++ amap --filter (\ (x, _) -> not (elem x (map fst newm))) amap
114+ findTag i [] = Nothing
115+ findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
116+ findTag i (_ : xs) = findTag i xs
117+
118+ findDefault [] = Nothing
119+ findDefault (DefaultCase sc : xs) = Just sc
120+ findDefault (_ : xs) = findDefault xs
121+
122+ getValArgs tm = getValArgs' tm []
123+ getValArgs' (VApp f a) as = getValArgs' f (a:as)
124+ getValArgs' f as = (f, as)
125+
76126quote :: Int -> Value -> TT Name
77127quote i (VP nt n v) = P nt n (quote i v)
78128quote i (VV x) = V x
@@ -97,17 +147,19 @@ data Fun = Fun Type Value Term Value
97147{- A definition is either a simple function (just an expression with a type),
98148 a constant, which could be a data or type constructor, an axiom or as an
99149 yet undefined function, or an Operator.
100− An Operator is a collection of pattern matching definitions, and a function
101− which explains how to reduce. -}
150+ An Operator is a function which explains how to reduce.
151+ A CaseOp is a function defined by a simple case tree -}
102152
103153data Def = Function Fun
104154 | Constant NameType Type Value
105− | Operator Type [(Term, Term)] ([Value] -> Maybe Value)
155+ | Operator Type ([Value] -> Maybe Value)
156+ | CaseOp Type [Name] SC
106157
107158instance Show Def where
108159 show (Function f) = "Function: " ++ show f
109160 show (Constant nt ty val) = "Constant: " ++ show nt ++ " " ++ show ty
110− show (Operator ty ps _) = "Operator: " ++ show ty ++ " " ++ show ps
161+ show (Operator ty _) = "Operator: " ++ show ty
162+ show (CaseOp ty ns sc) = "Case: " ++ show ns ++ " " ++ show sc
111163
112164-------
113165
@@ -132,11 +184,17 @@ addDatatype (Data n ty cons) ctxt
132184 addCons (tag+1) cons (addDef n
133185 (Constant (DCon tag (arity ty')) ty (eval ctxt [] ty)) ctxt)
134186
187+addCasedef :: Name -> CaseDef -> Type -> Context -> Context
188+addCasedef n (CaseDef args sc) ty ctxt
189+ = addDef n (CaseOp ty args sc) ctxt
190+
135191lookupTy :: Name -> Context -> Maybe Type
136192lookupTy n ctxt = do def <- lookupCtxt n ctxt
137193 case def of
138194 (Function (Fun ty _ _ _)) -> return ty
139195 (Constant _ ty _) -> return ty
196+ (Operator ty _) -> return ty
197+ (CaseOp ty _ _) -> return ty
140198
141199lookupP :: Name -> Context -> Maybe Term
142200lookupP n ctxt
@@ -144,13 +202,11 @@ lookupP n ctxt
144202 case def of
145203 (Function (Fun ty _ tm _)) -> return (P Ref n ty)
146204 (Constant nt ty hty) -> return (P nt n ty)
205+ (CaseOp ty _ _) -> return (P Ref n ty)
206+ (Operator ty _) -> return (P Ref n ty)
147207
148−lookupDef :: Name -> Context -> Maybe Term
149−lookupDef n ctxt
150− = do def <- lookupCtxt n ctxt
151− case def of
152− (Function (Fun ty _ tm _)) -> return tm
153− (Constant nt ty hty) -> return (P nt n ty)
208+lookupDef :: Name -> Context -> Maybe Def
209+lookupDef n ctxt = lookupCtxt n ctxt
154210
155211lookupVal :: Name -> Context -> Maybe Value
156212lookupVal n ctxt
src/Core/TT.hs+39−2
@@ -130,8 +130,6 @@ type RProgram = [(Name, RDef)]
130130data NameType = Bound | Ref | DCon Int Int | TCon Int
131131 deriving (Show, Eq)
132132
133−-- FIXME: Consider changing this to birectional, with type annotations.
134−
135133data TT n = P NameType n (TT n) -- embed type
136134 | V Int
137135 | Bind n (Binder (TT n)) (TT n)
@@ -156,6 +154,45 @@ instance Eq n => Eq (TT n) where
156154
157155-- A few handy operations on well typed terms:
158156
157+instantiate :: TT n -> TT n -> TT n
158+instantiate e = subst 0 where
159+ subst i (V x) | i == x = e
160+ subst i (Bind x b sc) = Bind x (fmap (subst i) b) (subst (i+1) sc)
161+ subst i (App f a) = App (subst i f) (subst i a)
162+ subst i t = t
163+
164+pToV :: Eq n => n -> TT n -> TT n
165+pToV n = pToV' n 0
166+pToV' n i (P _ x _) | n == x = V i
167+pToV' n i (Bind x b sc)
168+ | n == x = Bind x (fmap (pToV' n i) b) sc
169+ | otherwise = Bind x (fmap (pToV' n i) b) (pToV' n (i+1) sc)
170+pToV' n i (App f a) = App (pToV' n i f) (pToV' n i a)
171+pToV' n i t = t
172+
173+-- Convert several names. First in the list comes out as V 0
174+pToVs :: Eq n => [n] -> TT n -> TT n
175+pToVs ns tm = pToVs' ns tm 0 where
176+ pToVs' [] tm i = tm
177+ pToVs' (n:ns) tm i = pToV' n i (pToVs' ns tm (i+1))
178+
179+vToP :: TT n -> TT n
180+vToP = vToP' [] where
181+ vToP' env (V i) = let (n, b) = (env !! i) in
182+ P Bound n (binderTy b)
183+ vToP' env (Bind n b sc) = let b' = fmap (vToP' env) b in
184+ Bind n b' (vToP' ((n, b'):env) sc)
185+ vToP' env (App f a) = App (vToP' env f) (vToP' env a)
186+ vToP' env t = t
187+
188+finalise :: Eq n => TT n -> TT n
189+finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))
190+finalise (App f a) = App (finalise f) (finalise a)
191+finalise t = t
192+
193+subst :: Eq n => n -> TT n -> TT n -> TT n
194+subst n v tm = instantiate v (pToV n tm)
195+
159196-- Returns true if V 0 and bound name n do not occur in the term
160197
161198noOccurrence :: Eq n => n -> TT n -> Bool
src/Core/Typecheck.hs−29
@@ -127,35 +127,6 @@ check ctxt env (RBind n b sc)
127127 checkNotHoley i (Bind n b sc) = checkNotHoley (i+1) sc
128128 checkNotHoley _ _ = return ()
129129
130−pToV :: Eq n => n -> TT n -> TT n
131−pToV n = pToV' 0 where
132− pToV' i (P _ x _) | n == x = V i
133− pToV' i (Bind x b sc)
134− | n == x = Bind x (fmap (pToV' i) b) sc
135− | otherwise = Bind x (fmap (pToV' i) b) (pToV' (i+1) sc)
136− pToV' i (App f a) = App (pToV' i f) (pToV' i a)
137− pToV' i t = t
138−
139−vToP :: TT n -> TT n
140−vToP = vToP' [] where
141− vToP' env (V i) = let (n, b) = (env !! i) in
142− P Bound n (binderTy b)
143− vToP' env (Bind n b sc) = let b' = fmap (vToP' env) b in
144− Bind n b' (vToP' ((n, b'):env) sc)
145− vToP' env (App f a) = App (vToP' env f) (vToP' env a)
146− vToP' env t = t
147−
148−instantiate :: TT n -> TT n -> TT n
149−instantiate e = subst 0 where
150− subst i (V x) | i == x = e
151− subst i (Bind x b sc) = Bind x (fmap (subst i) b) (subst (i+1) sc)
152− subst i (App f a) = App (subst i f) (subst i a)
153− subst i t = t
154−
155−finalise :: Eq n => TT n -> TT n
156−finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))
157−finalise (App f a) = App (finalise f) (finalise a)
158−finalise t = t
159130
160131checkProgram :: Context -> RProgram -> TC Context
161132checkProgram ctxt [] = return ctxt
src/Idris/AbsSyntax.hs+24−14
@@ -10,9 +10,11 @@ import Control.Monad.State
1010import Data.List
1111import Data.Char
1212
13−data IOption = Logging
13+data IOption = IOption { opt_logLevel :: Int }
1414 deriving (Show, Eq)
1515
16+defaultOpts = IOption 0
17+
1618-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
1719-- without typechecking).
1820-- This will include all the functions and data declarations, plus fixity declarations
@@ -22,10 +24,10 @@ data IState = IState { tt_ctxt :: Context,
2224 idris_infixes :: [FixDecl],
2325 idris_implicits :: Ctxt [Name],
2426 idris_log :: String,
25− idris_options :: [IOption]
27+ idris_options :: IOption
2628 }
2729
28−idrisInit = IState emptyContext [] emptyContext "" []
30+idrisInit = IState emptyContext [] emptyContext "" defaultOpts
2931
3032-- The monad for the main REPL - reading and processing files and updating
3133-- global state (hence the IO inner monad).
@@ -48,17 +50,25 @@ tclift tc = case tc of
4850 OK v -> return v
4951 err -> fail (show err)
5052
51−setOpt :: IOption -> Bool -> Idris ()
52−setOpt o True = do i <- get
53− put (i { idris_options = nub (o : idris_options i) })
54−setOpt o False = do i <- get
55− put (i { idris_options = idris_options i \\ [o] })
53+setLogLevel :: Int -> Idris ()
54+setLogLevel l = do i <- get
55+ let opts = idris_options i
56+ let opt' = opts { opt_logLevel = l }
57+ put (i { idris_options = opt' } )
58+
59+logLevel :: Idris Int
60+logLevel = do i <- get
61+ return (opt_logLevel (idris_options i))
62+
63+logLvl :: Int -> String -> Idris ()
64+logLvl l str = do i <- get
65+ let lvl = opt_logLevel (idris_options i)
66+ when (lvl >= l)
67+ $ do lift (putStrLn str)
68+ put (i { idris_log = idris_log i ++ str ++ "\n" } )
5669
5770iLOG :: String -> Idris ()
58−iLOG str = do i <- get
59− when (Logging `elem` idris_options i)
60− $ do lift (putStrLn str)
61− put (i { idris_log = idris_log i ++ str ++ "\n" } )
71+iLOG = logLvl 1
6272
6373-- Taken from the library source code - for ghc 6.12/7 compatibility
6474liftCatch :: (m (a,s) -> (e -> m (a,s)) -> m (a,s)) ->
@@ -97,7 +107,7 @@ data Plicity = Imp | Exp deriving Show
97107
98108data PDecl' t = PFix Fixity [String] -- fixity declaration
99109 | PTy Name t -- type declaration
100− | PClauses [PClause' t] -- pattern clause
110+ | PClauses Name [PClause' t] -- pattern clause
101111 | PData (PData' t) -- data declaration
102112 deriving Functor
103113
@@ -134,7 +144,7 @@ instance Show PTerm where
134144instance Show PDecl where
135145 show (PFix f ops) = show f ++ " " ++ showSep ", " ops
136146 show (PTy n ty) = show n ++ " : " ++ show ty
137− show (PClauses c) = showSep "\n" (map show c)
147+ show (PClauses n c) = showSep "\n" (map show c)
138148 show (PData d) = show d
139149
140150instance Show PClause where
src/Idris/ElabDecls.hs+38−13
@@ -8,6 +8,7 @@ import Core.TT
88import Core.Elaborate
99import Core.Evaluate
1010import Core.Typecheck
11+import Core.CaseTree
1112
1213import Control.Monad
1314
@@ -16,7 +17,7 @@ elabType n ty
1617 = do ctxt <- getContext
1718 (ty', log) <- tclift $ elaborate ctxt n (Set 0) (build False ty)
1819 (cty, _) <- tclift $ recheck ctxt [] ty'
19− iLOG $ "---> " ++ show cty
20+ logLvl 2 $ "---> " ++ show cty
2021 updateContext (addConstant n cty)
2122
2223elabData :: PData -> Idris ()
@@ -24,7 +25,7 @@ elabData (PDatadecl n t dcons)
2425 = do ctxt <- getContext
2526 (t', log) <- tclift $ elaborate ctxt n (Set 0) (build False t)
2627 (cty, _) <- tclift $ recheck ctxt [] t'
27− iLOG $ "---> " ++ show cty
28+ logLvl 2 $ "---> " ++ show cty
2829 updateContext (addConstant n cty) -- temporary, to check cons
2930 cons <- mapM elabCon dcons
3031 setContext (addDatatype (Data n cty cons) ctxt)
@@ -36,23 +37,46 @@ elabCon (n, t)
3637 (t', log) <- tclift $ elaborate ctxt n (Set 0) (build False t)
3738-- iLOG $ "Rechecking " ++ show t'
3839 (cty, _) <- tclift $ recheck ctxt [] t'
39− iLOG $ "---> " ++ show n ++ " : " ++ show cty
40+ logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty
4041 return (n, cty)
4142
42−elabClauses :: [PClause] -> Idris ()
43−elabClauses cs = do pats <- mapM elabClause cs
44− iLOG (showSep "\n" (map (\ (l,r) ->
45− show l ++ " = " ++
46− show r) pats))
43+elabClauses :: Name -> [PClause] -> Idris ()
44+elabClauses n cs
45+ = do pats <- mapM elabClause cs
46+ logLvl 3 (showSep "\n" (map (\ (l,r) ->
47+ show l ++ " = " ++
48+ show r) pats))
49+ let tree = simpleCase (map debind pats)
50+ logLvl 3 (show tree)
51+ ctxt <- getContext
52+ case lookupTy n ctxt of
53+ Just ty -> updateContext (addCasedef n tree ty)
54+ Nothing -> return ()
55+ where
56+ debind (x, y) = (depat x, depat y)
57+ depat (Bind n (PVar t) sc) = depat (instantiate (P Bound n t) sc)
58+ depat x = x
59+
60+elabVal :: PTerm -> Idris (Term, Type)
61+elabVal tm
62+ = do ctxt <- getContext
63+ (tm', _) <- tclift $ elaborate ctxt (MN 0 "val") infP
64+ (build False (infTerm tm))
65+ let vtm = getInferTerm tm'
66+ tclift $ recheck ctxt [] vtm
4767
4868elabClause :: PClause -> Idris (Term, Term)
4969elabClause (PClause _ lhs rhs)
5070 = do ctxt <- getContext
71+ -- Build the LHS as an "Infer", and pull out its type and
72+ -- pattern bindings
5173 (lhs', _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP
5274 (build True (infTerm lhs))
5375 let lhs_tm = getInferTerm lhs'
5476 let lhs_ty = getInferType lhs'
5577 (clhs, clhsty) <- tclift $ recheck ctxt [] lhs_tm
78+ -- Now build the RHS, using the type of the LHS as the goal.
79+ iLOG (showImp True rhs)
5680 (rhs', _) <- tclift $ elaborate ctxt (MN 0 "patRHS") clhsty
5781 (do pbinds lhs_tm
5882 build False rhs
@@ -76,8 +100,8 @@ elabDecl' (PTy n ty) = do iLOG $ "Elaborating type decl " ++ show n
76100 elabType n ty
77101elabDecl' (PData d) = do iLOG $ "Elaborating " ++ show d
78102 elabData d
79−elabDecl' d@(PClauses ps) = do iLOG $ "Elaborating " ++ show d
80− elabClauses ps
103+elabDecl' d@(PClauses n ps) = do iLOG $ "Elaborating " ++ show n
104+ elabClauses n ps
81105
82106-- Using the elaborator, convert a term in raw syntax to a fully
83107-- elaborated, typechecked term.
@@ -121,9 +145,10 @@ elab pattern tm = do elab' tm
121145 elab' sc
122146 solve
123147 elab' (PApp (PRef f) imps args)
124− = do ns <- apply (Var f) (map isph imps ++ map (\x -> False) args)
125− solve
126− elabArgs ns (map snd imps ++ args)
148+ = try (do ns <- apply (Var f) (map isph imps ++ map (\x -> False) args)
149+ solve
150+ elabArgs ns (map snd imps ++ args))
151+ (do fail "Not tried this way yet")
127152 elab' x = fail $ "Not implemented " ++ show x
128153
129154 elabArgs [] _ = return ()
src/Idris/Parser.hs+4−4
@@ -49,10 +49,10 @@ parseProg fname = do file <- lift $ readFile fname
4949
5050-- Collect PClauses with the same function name
5151collect :: [PDecl] -> [PDecl]
52−collect (PClauses [c@(PClause n l r)] : ds) = clauses n [c] ds
53− where clauses n acc (PClauses [c@(PClause n' l r)] : ds)
52+collect (PClauses _ [c@(PClause n l r)] : ds) = clauses n [c] ds
53+ where clauses n acc (PClauses _ [c@(PClause n' l r)] : ds)
5454 | n == n' = clauses n (c : acc) ds
55− clauses n acc xs = PClauses (reverse acc) : collect xs
55+ clauses n acc xs = PClauses n (reverse acc) : collect xs
5656collect (d : ds) = d : collect ds
5757collect [] = []
5858
@@ -200,7 +200,7 @@ pSimpleCon = do cn <- pfName
200200
201201pPattern :: IParser PDecl
202202pPattern = do clause <- pClause
203− return (PClauses [clause]) -- collect together later
203+ return (PClauses (MN 0 "_") [clause]) -- collect together later
204204
205205pClause :: IParser PClause
206206pClause = try (do n <- pfName
src/Idris/REPL.hs+7−1
@@ -4,6 +4,9 @@ module Idris.REPL where
44
55import Idris.AbsSyntax
66import Idris.REPLParser
7+import Idris.ElabDecls
8+
9+import Core.Evaluate
710import Core.ProofShell
811
912import System.Console.Readline
@@ -33,7 +36,10 @@ processInput cmd
3336process :: Command -> Idris ()
3437process Help
3538 = iputStrLn "At some point I'll write some help text. Thanks for asking though."
36−process (Eval t) = iputStrLn $ "Not implemented: " ++ show t
39+process (Eval t) = do (tm, ty) <- elabVal t
40+ ctxt <- getContext
41+ let tm' = normalise ctxt [] tm
42+ iputStrLn (show tm' ++ " : " ++ show ty)
3743process TTShell = do ist <- get
3844 let shst = initState (tt_ctxt ist)
3945 shst' <- lift $ runShell shst
src/Main.hs+8−5
@@ -25,7 +25,7 @@ import Idris.ElabDecls
2525
2626data Opt = Filename String
2727 | Version
28− | OLogging
28+ | OLogging Int
2929 deriving Eq
3030
3131main = do xs <- getArgs
@@ -35,9 +35,12 @@ main = do xs <- getArgs
3535runIdris :: [Opt] -> Idris ()
3636runIdris opts =
3737 do let inputs = opt getFile opts
38− when (OLogging `elem` opts) (setOpt Logging True)
38+ mapM_ makeOption opts
3939 mapM_ loadModule inputs
4040 repl
41+ where
42+ makeOption (OLogging i) = setLogLevel i
43+ makeOption _ = return ()
4144
4245loadModule :: FilePath -> Idris ()
4346loadModule f = do iLOG ("Reading " ++ show f)
@@ -56,7 +59,7 @@ dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
5659
5760dumpDecl (PFix f ops) = show f ++ " " ++ showSep ", " ops
5861dumpDecl (PTy n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
59−dumpDecl (PClauses cs) = "pat\t" ++ showSep "\n\t" (map (showCImp True) cs)
62+dumpDecl (PClauses n cs) = "pat\t" ++ showSep "\n\t" (map (showCImp True) cs)
6063dumpDecl (PData d) = showDImp True d
6164
6265getFile :: Opt -> Maybe String
@@ -71,8 +74,8 @@ usage = do putStrLn "You're doing it wrong"
7174
7275parseArgs :: [String] -> IO [Opt]
7376parseArgs [] = return []
74−parseArgs ("--log":ns) = liftM (OLogging : ) (parseArgs ns)
75−parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)
77+parseArgs ("--log":lvl:ns) = liftM (OLogging (read lvl) : ) (parseArgs ns)
78+parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)
7679
7780{-
7881main'