git.iko.soy/Idris-dev
on master help sign in
Pattern matcher, evaluation of 2+2 now works
c637850Edwin Brady
decls.mi+7−1
compare with master
unifiedsplit
@@ -1,7 +1,7 @@
1infixl 5 +, - ;
1infixl 5 +, - ;
2infixl 6 *, / ;
2infixl 6 *, / ;
3
3
4−infixl 7 :: ;
4+infixr 7 :: ;
5
5
6data Nat = O | S Nat;
6data Nat = O | S Nat;
7data List a = Nil | Cons a (List a);
7data List a = Nil | Cons a (List a);
@@ -22,6 +22,12 @@ app : Vect a n -> Vect a m -> Vect a (plus n m);
22app VNil ys = ys;
22app VNil ys = ys;
23app (x :: xs) ys = x :: app xs ys;
23app (x :: xs) ys = x :: app xs ys;
24
24
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+
25infixl 5 .+. ;
31infixl 5 .+. ;
26
32
27(.+.) : Nat -> Nat -> Nat;
33(.+.) : Nat -> Nat -> Nat;
miniidris.cabal+1
@@ -20,6 +20,7 @@ Executable miniidris
20 Other-modules: Core.TT, Core.Evaluate, Core.Typecheck,
20 Other-modules: Core.TT, Core.Evaluate, Core.Typecheck,
21 Core.ProofShell, Core.ProofState, Core.CoreParser,
21 Core.ProofShell, Core.ProofState, Core.CoreParser,
22 Core.ShellParser, Core.Unify, Core.Elaborate,
22 Core.ShellParser, Core.Unify, Core.Elaborate,
23+ Core.CaseTree,
23
24
24 Idris.AbsSyntax, Idris.Parser, Idris.REPL,
25 Idris.AbsSyntax, Idris.Parser, Idris.REPL,
25 Idris.REPLParser, Idris.ElabDecls
26 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 @@
3
3
4module Core.Evaluate(normalise,
4module Core.Evaluate(normalise,
5 Fun(..), Def(..), Context,
5 Fun(..), Def(..), Context,
6− addToCtxt, addConstant, addDatatype,
6+ addToCtxt, addConstant, addDatatype, addCasedef,
7− lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv) where
7+ lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv,
8+ Value) where
8
9
9import Debug.Trace
10import Debug.Trace
11+
10import Core.TT
12import Core.TT
13+import Core.CaseTree
11
14
12-- VALUES (as HOAS) ---------------------------------------------------------
15-- VALUES (as HOAS) ---------------------------------------------------------
13
16
@@ -49,8 +52,10 @@ eval :: Context -> Env -> TT Name -> Value
49eval ctxt genv tm = ev [] tm where
52eval ctxt genv tm = ev [] tm where
50 ev env (P Bound n ty)
53 ev env (P Bound n ty)
51 | Just (Let t v) <- lookup n genv = ev env v
54 | Just (Let t v) <- lookup n genv = ev env v
52− ev env (P Ref n ty)
55+ ev env (P Ref n ty) = case lookupDef n ctxt of
53− | Just v <- lookupVal n ctxt = v
56+ Just (Function (Fun _ _ _ v)) -> v
57+ Just (Constant nt ty hty) -> VP nt n hty
58+ _ -> VP Ref n (ev env ty)
54 ev env (P nt n ty) = VP nt n (ev env ty)
59 ev env (P nt n ty) = VP nt n (ev env ty)
55 ev env (V i) | i < length env = env !! i
60 ev env (V i) | i < length env = env !! i
56 | otherwise = error $ "Internal error: V" ++ show i
61 | otherwise = error $ "Internal error: V" ++ show i
@@ -67,12 +72,57 @@ eval ctxt genv tm = ev [] tm where
67 evApply env args f = apply env (ev env f) args
72 evApply env args f = apply env (ev env f) args
68
73
69 apply env (VBind n (Lam t) sc) (a:as) = wknV (-1) $ apply env (sc (ev env a)) as
74 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
70 apply env f (a:as) = unload env f (a:as)
80 apply env f (a:as) = unload env f (a:as)
71 apply env f [] = f
81 apply env f [] = f
72
82
73 unload env f [] = f
83 unload env f [] = f
74 unload env f (a:as) = unload env (VApp f (ev env a)) as
84 unload env f (a:as) = unload env (VApp f (ev env a)) as
75
85
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+
76quote :: Int -> Value -> TT Name
126quote :: Int -> Value -> TT Name
77quote i (VP nt n v) = P nt n (quote i v)
127quote i (VP nt n v) = P nt n (quote i v)
78quote i (VV x) = V x
128quote i (VV x) = V x
@@ -97,17 +147,19 @@ data Fun = Fun Type Value Term Value
97{- A definition is either a simple function (just an expression with a type),
147{- A definition is either a simple function (just an expression with a type),
98 a constant, which could be a data or type constructor, an axiom or as an
148 a constant, which could be a data or type constructor, an axiom or as an
99 yet undefined function, or an Operator.
149 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 -}
102
152
103data Def = Function Fun
153data Def = Function Fun
104 | Constant NameType Type Value
154 | Constant NameType Type Value
105− | Operator Type [(Term, Term)] ([Value] -> Maybe Value)
155+ | Operator Type ([Value] -> Maybe Value)
156+ | CaseOp Type [Name] SC
106
157
107instance Show Def where
158instance Show Def where
108 show (Function f) = "Function: " ++ show f
159 show (Function f) = "Function: " ++ show f
109 show (Constant nt ty val) = "Constant: " ++ show nt ++ " " ++ show ty
160 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
111
163
112-------
164-------
113
165
@@ -132,11 +184,17 @@ addDatatype (Data n ty cons) ctxt
132 addCons (tag+1) cons (addDef n
184 addCons (tag+1) cons (addDef n
133 (Constant (DCon tag (arity ty')) ty (eval ctxt [] ty)) ctxt)
185 (Constant (DCon tag (arity ty')) ty (eval ctxt [] ty)) ctxt)
134
186
187+addCasedef :: Name -> CaseDef -> Type -> Context -> Context
188+addCasedef n (CaseDef args sc) ty ctxt
189+ = addDef n (CaseOp ty args sc) ctxt
190+
135lookupTy :: Name -> Context -> Maybe Type
191lookupTy :: Name -> Context -> Maybe Type
136lookupTy n ctxt = do def <- lookupCtxt n ctxt
192lookupTy n ctxt = do def <- lookupCtxt n ctxt
137 case def of
193 case def of
138 (Function (Fun ty _ _ _)) -> return ty
194 (Function (Fun ty _ _ _)) -> return ty
139 (Constant _ ty _) -> return ty
195 (Constant _ ty _) -> return ty
196+ (Operator ty _) -> return ty
197+ (CaseOp ty _ _) -> return ty
140
198
141lookupP :: Name -> Context -> Maybe Term
199lookupP :: Name -> Context -> Maybe Term
142lookupP n ctxt
200lookupP n ctxt
@@ -144,13 +202,11 @@ lookupP n ctxt
144 case def of
202 case def of
145 (Function (Fun ty _ tm _)) -> return (P Ref n ty)
203 (Function (Fun ty _ tm _)) -> return (P Ref n ty)
146 (Constant nt ty hty) -> return (P nt n ty)
204 (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)
147
207
148−lookupDef :: Name -> Context -> Maybe Term
208+lookupDef :: Name -> Context -> Maybe Def
149−lookupDef n ctxt
209+lookupDef n ctxt = lookupCtxt 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)
154
210
155lookupVal :: Name -> Context -> Maybe Value
211lookupVal :: Name -> Context -> Maybe Value
156lookupVal n ctxt
212lookupVal n ctxt
src/Core/TT.hs+39−2
@@ -130,8 +130,6 @@ type RProgram = [(Name, RDef)]
130data NameType = Bound | Ref | DCon Int Int | TCon Int
130data NameType = Bound | Ref | DCon Int Int | TCon Int
131 deriving (Show, Eq)
131 deriving (Show, Eq)
132
132
133−-- FIXME: Consider changing this to birectional, with type annotations.
134−
135data TT n = P NameType n (TT n) -- embed type
133data TT n = P NameType n (TT n) -- embed type
136 | V Int
134 | V Int
137 | Bind n (Binder (TT n)) (TT n)
135 | Bind n (Binder (TT n)) (TT n)
@@ -156,6 +154,45 @@ instance Eq n => Eq (TT n) where
156
154
157-- A few handy operations on well typed terms:
155-- A few handy operations on well typed terms:
158
156
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+
159-- Returns true if V 0 and bound name n do not occur in the term
196-- Returns true if V 0 and bound name n do not occur in the term
160
197
161noOccurrence :: Eq n => n -> TT n -> Bool
198noOccurrence :: Eq n => n -> TT n -> Bool
src/Core/Typecheck.hs−29
@@ -127,35 +127,6 @@ check ctxt env (RBind n b sc)
127 checkNotHoley i (Bind n b sc) = checkNotHoley (i+1) sc
127 checkNotHoley i (Bind n b sc) = checkNotHoley (i+1) sc
128 checkNotHoley _ _ = return ()
128 checkNotHoley _ _ = return ()
129
129
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
159
130
160checkProgram :: Context -> RProgram -> TC Context
131checkProgram :: Context -> RProgram -> TC Context
161checkProgram ctxt [] = return ctxt
132checkProgram ctxt [] = return ctxt
src/Idris/AbsSyntax.hs+24−14
@@ -10,9 +10,11 @@ import Control.Monad.State
10import Data.List
10import Data.List
11import Data.Char
11import Data.Char
12
12
13−data IOption = Logging
13+data IOption = IOption { opt_logLevel :: Int }
14 deriving (Show, Eq)
14 deriving (Show, Eq)
15
15
16+defaultOpts = IOption 0
17+
16-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
18-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
17-- without typechecking).
19-- without typechecking).
18-- This will include all the functions and data declarations, plus fixity declarations
20-- This will include all the functions and data declarations, plus fixity declarations
@@ -22,10 +24,10 @@ data IState = IState { tt_ctxt :: Context,
22 idris_infixes :: [FixDecl],
24 idris_infixes :: [FixDecl],
23 idris_implicits :: Ctxt [Name],
25 idris_implicits :: Ctxt [Name],
24 idris_log :: String,
26 idris_log :: String,
25− idris_options :: [IOption]
27+ idris_options :: IOption
26 }
28 }
27
29
28−idrisInit = IState emptyContext [] emptyContext "" []
30+idrisInit = IState emptyContext [] emptyContext "" defaultOpts
29
31
30-- The monad for the main REPL - reading and processing files and updating
32-- The monad for the main REPL - reading and processing files and updating
31-- global state (hence the IO inner monad).
33-- global state (hence the IO inner monad).
@@ -48,17 +50,25 @@ tclift tc = case tc of
48 OK v -> return v
50 OK v -> return v
49 err -> fail (show err)
51 err -> fail (show err)
50
52
51−setOpt :: IOption -> Bool -> Idris ()
53+setLogLevel :: Int -> Idris ()
52−setOpt o True = do i <- get
54+setLogLevel l = do i <- get
55+ let opts = idris_options i
56+ let opt' = opts { opt_logLevel = l }
53− put (i { idris_options = nub (o : idris_options i) })
57+ put (i { idris_options = opt' } )
54−setOpt o False = do i <- get
58+
55− put (i { idris_options = idris_options i \\ [o] })
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" } )
56
69
57iLOG :: String -> Idris ()
70iLOG :: String -> Idris ()
58−iLOG str = do i <- get
71+iLOG = logLvl 1
59− when (Logging `elem` idris_options i)
60− $ do lift (putStrLn str)
61− put (i { idris_log = idris_log i ++ str ++ "\n" } )
62
72
63-- Taken from the library source code - for ghc 6.12/7 compatibility
73-- Taken from the library source code - for ghc 6.12/7 compatibility
64liftCatch :: (m (a,s) -> (e -> m (a,s)) -> m (a,s)) ->
74liftCatch :: (m (a,s) -> (e -> m (a,s)) -> m (a,s)) ->
@@ -97,7 +107,7 @@ data Plicity = Imp | Exp deriving Show
97
107
98data PDecl' t = PFix Fixity [String] -- fixity declaration
108data PDecl' t = PFix Fixity [String] -- fixity declaration
99 | PTy Name t -- type declaration
109 | PTy Name t -- type declaration
100− | PClauses [PClause' t] -- pattern clause
110+ | PClauses Name [PClause' t] -- pattern clause
101 | PData (PData' t) -- data declaration
111 | PData (PData' t) -- data declaration
102 deriving Functor
112 deriving Functor
103
113
@@ -134,7 +144,7 @@ instance Show PTerm where
134instance Show PDecl where
144instance Show PDecl where
135 show (PFix f ops) = show f ++ " " ++ showSep ", " ops
145 show (PFix f ops) = show f ++ " " ++ showSep ", " ops
136 show (PTy n ty) = show n ++ " : " ++ show ty
146 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)
138 show (PData d) = show d
148 show (PData d) = show d
139
149
140instance Show PClause where
150instance Show PClause where
src/Idris/ElabDecls.hs+38−13
@@ -8,6 +8,7 @@ import Core.TT
8import Core.Elaborate
8import Core.Elaborate
9import Core.Evaluate
9import Core.Evaluate
10import Core.Typecheck
10import Core.Typecheck
11+import Core.CaseTree
11
12
12import Control.Monad
13import Control.Monad
13
14
@@ -16,7 +17,7 @@ elabType n ty
16 = do ctxt <- getContext
17 = do ctxt <- getContext
17 (ty', log) <- tclift $ elaborate ctxt n (Set 0) (build False ty)
18 (ty', log) <- tclift $ elaborate ctxt n (Set 0) (build False ty)
18 (cty, _) <- tclift $ recheck ctxt [] ty'
19 (cty, _) <- tclift $ recheck ctxt [] ty'
19− iLOG $ "---> " ++ show cty
20+ logLvl 2 $ "---> " ++ show cty
20 updateContext (addConstant n cty)
21 updateContext (addConstant n cty)
21
22
22elabData :: PData -> Idris ()
23elabData :: PData -> Idris ()
@@ -24,7 +25,7 @@ elabData (PDatadecl n t dcons)
24 = do ctxt <- getContext
25 = do ctxt <- getContext
25 (t', log) <- tclift $ elaborate ctxt n (Set 0) (build False t)
26 (t', log) <- tclift $ elaborate ctxt n (Set 0) (build False t)
26 (cty, _) <- tclift $ recheck ctxt [] t'
27 (cty, _) <- tclift $ recheck ctxt [] t'
27− iLOG $ "---> " ++ show cty
28+ logLvl 2 $ "---> " ++ show cty
28 updateContext (addConstant n cty) -- temporary, to check cons
29 updateContext (addConstant n cty) -- temporary, to check cons
29 cons <- mapM elabCon dcons
30 cons <- mapM elabCon dcons
30 setContext (addDatatype (Data n cty cons) ctxt)
31 setContext (addDatatype (Data n cty cons) ctxt)
@@ -36,23 +37,46 @@ elabCon (n, t)
36 (t', log) <- tclift $ elaborate ctxt n (Set 0) (build False t)
37 (t', log) <- tclift $ elaborate ctxt n (Set 0) (build False t)
37-- iLOG $ "Rechecking " ++ show t'
38-- iLOG $ "Rechecking " ++ show t'
38 (cty, _) <- tclift $ recheck ctxt [] t'
39 (cty, _) <- tclift $ recheck ctxt [] t'
39− iLOG $ "---> " ++ show n ++ " : " ++ show cty
40+ logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty
40 return (n, cty)
41 return (n, cty)
41
42
42−elabClauses :: [PClause] -> Idris ()
43+elabClauses :: Name -> [PClause] -> Idris ()
44+elabClauses n cs
43−elabClauses cs = do pats <- mapM elabClause cs
45+ = do pats <- mapM elabClause cs
44− iLOG (showSep "\n" (map (\ (l,r) ->
46+ logLvl 3 (showSep "\n" (map (\ (l,r) ->
45− show l ++ " = " ++
47+ show l ++ " = " ++
46− show r) pats))
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
47
67
48elabClause :: PClause -> Idris (Term, Term)
68elabClause :: PClause -> Idris (Term, Term)
49elabClause (PClause _ lhs rhs)
69elabClause (PClause _ lhs rhs)
50 = do ctxt <- getContext
70 = do ctxt <- getContext
71+ -- Build the LHS as an "Infer", and pull out its type and
72+ -- pattern bindings
51 (lhs', _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP
73 (lhs', _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP
52 (build True (infTerm lhs))
74 (build True (infTerm lhs))
53 let lhs_tm = getInferTerm lhs'
75 let lhs_tm = getInferTerm lhs'
54 let lhs_ty = getInferType lhs'
76 let lhs_ty = getInferType lhs'
55 (clhs, clhsty) <- tclift $ recheck ctxt [] lhs_tm
77 (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)
56 (rhs', _) <- tclift $ elaborate ctxt (MN 0 "patRHS") clhsty
80 (rhs', _) <- tclift $ elaborate ctxt (MN 0 "patRHS") clhsty
57 (do pbinds lhs_tm
81 (do pbinds lhs_tm
58 build False rhs
82 build False rhs
@@ -76,8 +100,8 @@ elabDecl' (PTy n ty) = do iLOG $ "Elaborating type decl " ++ show n
76 elabType n ty
100 elabType n ty
77elabDecl' (PData d) = do iLOG $ "Elaborating " ++ show d
101elabDecl' (PData d) = do iLOG $ "Elaborating " ++ show d
78 elabData d
102 elabData d
79−elabDecl' d@(PClauses ps) = do iLOG $ "Elaborating " ++ show d
103+elabDecl' d@(PClauses n ps) = do iLOG $ "Elaborating " ++ show n
80− elabClauses ps
104+ elabClauses n ps
81
105
82-- Using the elaborator, convert a term in raw syntax to a fully
106-- Using the elaborator, convert a term in raw syntax to a fully
83-- elaborated, typechecked term.
107-- elaborated, typechecked term.
@@ -121,9 +145,10 @@ elab pattern tm = do elab' tm
121 elab' sc
145 elab' sc
122 solve
146 solve
123 elab' (PApp (PRef f) imps args)
147 elab' (PApp (PRef f) imps args)
124− = do ns <- apply (Var f) (map isph imps ++ map (\x -> False) args)
148+ = try (do ns <- apply (Var f) (map isph imps ++ map (\x -> False) args)
125− solve
149+ solve
126− elabArgs ns (map snd imps ++ args)
150+ elabArgs ns (map snd imps ++ args))
151+ (do fail "Not tried this way yet")
127 elab' x = fail $ "Not implemented " ++ show x
152 elab' x = fail $ "Not implemented " ++ show x
128
153
129 elabArgs [] _ = return ()
154 elabArgs [] _ = return ()
src/Idris/Parser.hs+4−4
@@ -49,10 +49,10 @@ parseProg fname = do file <- lift $ readFile fname
49
49
50-- Collect PClauses with the same function name
50-- Collect PClauses with the same function name
51collect :: [PDecl] -> [PDecl]
51collect :: [PDecl] -> [PDecl]
52−collect (PClauses [c@(PClause n l r)] : ds) = clauses n [c] 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)
53+ where clauses n acc (PClauses _ [c@(PClause n' l r)] : ds)
54 | n == n' = clauses n (c : acc) ds
54 | 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
56collect (d : ds) = d : collect ds
56collect (d : ds) = d : collect ds
57collect [] = []
57collect [] = []
58
58
@@ -200,7 +200,7 @@ pSimpleCon = do cn <- pfName
200
200
201pPattern :: IParser PDecl
201pPattern :: IParser PDecl
202pPattern = do clause <- pClause
202pPattern = do clause <- pClause
203− return (PClauses [clause]) -- collect together later
203+ return (PClauses (MN 0 "_") [clause]) -- collect together later
204
204
205pClause :: IParser PClause
205pClause :: IParser PClause
206pClause = try (do n <- pfName
206pClause = try (do n <- pfName
src/Idris/REPL.hs+7−1
@@ -4,6 +4,9 @@ module Idris.REPL where
4
4
5import Idris.AbsSyntax
5import Idris.AbsSyntax
6import Idris.REPLParser
6import Idris.REPLParser
7+import Idris.ElabDecls
8+
9+import Core.Evaluate
7import Core.ProofShell
10import Core.ProofShell
8
11
9import System.Console.Readline
12import System.Console.Readline
@@ -33,7 +36,10 @@ processInput cmd
33process :: Command -> Idris ()
36process :: Command -> Idris ()
34process Help
37process Help
35 = iputStrLn "At some point I'll write some help text. Thanks for asking though."
38 = iputStrLn "At some point I'll write some help text. Thanks for asking though."
39+process (Eval t) = do (tm, ty) <- elabVal t
40+ ctxt <- getContext
41+ let tm' = normalise ctxt [] tm
36−process (Eval t) = iputStrLn $ "Not implemented: " ++ show t
42+ iputStrLn (show tm' ++ " : " ++ show ty)
37process TTShell = do ist <- get
43process TTShell = do ist <- get
38 let shst = initState (tt_ctxt ist)
44 let shst = initState (tt_ctxt ist)
39 shst' <- lift $ runShell shst
45 shst' <- lift $ runShell shst
src/Main.hs+8−5
@@ -25,7 +25,7 @@ import Idris.ElabDecls
25
25
26data Opt = Filename String
26data Opt = Filename String
27 | Version
27 | Version
28− | OLogging
28+ | OLogging Int
29 deriving Eq
29 deriving Eq
30
30
31main = do xs <- getArgs
31main = do xs <- getArgs
@@ -35,9 +35,12 @@ main = do xs <- getArgs
35runIdris :: [Opt] -> Idris ()
35runIdris :: [Opt] -> Idris ()
36runIdris opts =
36runIdris opts =
37 do let inputs = opt getFile opts
37 do let inputs = opt getFile opts
38− when (OLogging `elem` opts) (setOpt Logging True)
38+ mapM_ makeOption opts
39 mapM_ loadModule inputs
39 mapM_ loadModule inputs
40 repl
40 repl
41+ where
42+ makeOption (OLogging i) = setLogLevel i
43+ makeOption _ = return ()
41
44
42loadModule :: FilePath -> Idris ()
45loadModule :: FilePath -> Idris ()
43loadModule f = do iLOG ("Reading " ++ show f)
46loadModule f = do iLOG ("Reading " ++ show f)
@@ -56,7 +59,7 @@ dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
56
59
57dumpDecl (PFix f ops) = show f ++ " " ++ showSep ", " ops
60dumpDecl (PFix f ops) = show f ++ " " ++ showSep ", " ops
58dumpDecl (PTy n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
61dumpDecl (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)
60dumpDecl (PData d) = showDImp True d
63dumpDecl (PData d) = showDImp True d
61
64
62getFile :: Opt -> Maybe String
65getFile :: Opt -> Maybe String
@@ -71,8 +74,8 @@ usage = do putStrLn "You're doing it wrong"
71
74
72parseArgs :: [String] -> IO [Opt]
75parseArgs :: [String] -> IO [Opt]
73parseArgs [] = return []
76parseArgs [] = return []
74−parseArgs ("--log":ns) = liftM (OLogging : ) (parseArgs ns)
77+parseArgs ("--log":lvl:ns) = liftM (OLogging (read lvl) : ) (parseArgs ns)
75−parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)
78+parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)
76
79
77{-
80{-
78main'
81main'