@@ -54,6 +54,10 @@ mkPrompt [] = "Idris"
5454mkPrompt [x] = "*" ++ dropExtension x
5555mkPrompt (x:xs) = "*" ++ dropExtension x ++ " " ++ mkPrompt xs
5656
57+lit f = case splitExtension f of
58+ (_, ".lidr") -> True
59+ _ -> False
60+
5761processInput :: String -> IState -> [FilePath] -> Idris (Maybe [FilePath])
5862processInput cmd orig inputs
5963 = do i <- get
@@ -74,7 +78,7 @@ processInput cmd orig inputs
7478 return (Just inputs)
7579 Right Quit -> do iputStrLn "Bye bye"
7680 return Nothing
77− Right cmd -> do idrisCatch (process cmd)
81+ Right cmd -> do idrisCatch (process fn cmd)
7882 (\e -> iputStrLn (show e))
7983 return (Just inputs)
8084
@@ -107,7 +111,7 @@ addProof f orig
107111 i <- get
108112 case last_proof i of
109113 Nothing -> iputStrLn "No proof to add"
110− Just (n, p) -> do let prog' = insertScript (showProof n p) (lines prog)
114+ Just (n, p) -> do let prog' = insertScript (showProof (lit f) n p) (lines prog)
111115 liftIO $ writeFile f (unlines prog')
112116 iputStrLn $ "Added proof " ++ show n
113117 put (i { last_proof = Nothing })
@@ -119,9 +123,10 @@ insertScript prf (p@"---------- Proofs ----------" : "" : xs)
119123 = p : "" : prf : xs
120124insertScript prf (x : xs) = x : insertScript prf xs
121125
122−process :: Command -> Idris ()
123−process Help = iputStrLn displayHelp
124−process (Eval t) = do (tm, ty) <- elabVal toplevel False t
126+process :: FilePath -> Command -> Idris ()
127+process fn Help = iputStrLn displayHelp
128+process fn (Eval t)
129+ = do (tm, ty) <- elabVal toplevel False t
125130 ctxt <- getContext
126131 ist <- get
127132 let tm' = normaliseAll ctxt [] tm
@@ -130,7 +135,8 @@ process (Eval t) = do (tm, ty) <- elabVal toplevel False t
130135 imp <- impShow
131136 iputStrLn (showImp imp (delab ist tm') ++ " : " ++
132137 showImp imp (delab ist ty'))
133−process (ExecVal t) = do (tm, ty) <- elabVal toplevel False t
138+process fn (ExecVal t)
139+ = do (tm, ty) <- elabVal toplevel False t
134140-- (PApp fc (PRef fc (NS (UN "print") ["prelude"]))
135141-- [pexp t])
136142 (tmpn, tmph) <- liftIO tempfile
@@ -139,7 +145,7 @@ process (ExecVal t) = do (tm, ty) <- elabVal toplevel False t
139145 liftIO $ system tmpn
140146 return ()
141147 where fc = FC "(input)" 0
142−process (Check (PRef _ n))
148+process fn (Check (PRef _ n))
143149 = do ctxt <- getContext
144150 ist <- get
145151 imp <- impShow
@@ -147,74 +153,75 @@ process (Check (PRef _ n))
147153 [t] -> iputStrLn $ show n ++ " : " ++
148154 showImp imp (delab ist t)
149155 _ -> iputStrLn $ "No such variable " ++ show n
150−process (Check t) = do (tm, ty) <- elabVal toplevel False t
151− ctxt <- getContext
152− ist <- get
153− imp <- impShow
154− let ty' = normaliseC ctxt [] ty
155− iputStrLn (showImp imp (delab ist tm) ++ " : " ++
156− showImp imp (delab ist ty))
157−process Universes = do i <- get
158− let cs = idris_constraints i
156+process fn (Check t) = do (tm, ty) <- elabVal toplevel False t
157+ ctxt <- getContext
158+ ist <- get
159+ imp <- impShow
160+ let ty' = normaliseC ctxt [] ty
161+ iputStrLn (showImp imp (delab ist tm) ++ " : " ++
162+ showImp imp (delab ist ty))
163+process fn Universes = do i <- get
164+ let cs = idris_constraints i
159165-- iputStrLn $ showSep "\n" (map show cs)
160− liftIO $ print (map fst cs)
161− let n = length cs
162− iputStrLn $ "(" ++ show n ++ " constraints)"
163− case ucheck cs of
166+ liftIO $ print (map fst cs)
167+ let n = length cs
168+ iputStrLn $ "(" ++ show n ++ " constraints)"
169+ case ucheck cs of
164170 Error e -> iputStrLn $ pshow i e
165171 OK _ -> iputStrLn "Universes OK"
166−process (Defn n) = do i <- get
167− iputStrLn "Compiled patterns:\n"
168− liftIO $ print (lookupDef Nothing n (tt_ctxt i))
169− case lookupCtxt Nothing n (idris_patdefs i) of
170− [] -> return ()
171− [d] -> do iputStrLn "Original definiton:\n"
172− mapM_ (printCase i) d
172+process fn (Defn n) = do i <- get
173+ iputStrLn "Compiled patterns:\n"
174+ liftIO $ print (lookupDef Nothing n (tt_ctxt i))
175+ case lookupCtxt Nothing n (idris_patdefs i) of
176+ [] -> return ()
177+ [d] -> do iputStrLn "Original definiton:\n"
178+ mapM_ (printCase i) d
173179 where printCase i (lhs, rhs) = do liftIO $ putStr $ showImp True (delab i lhs)
174180 liftIO $ putStr " = "
175181 liftIO $ putStrLn $ showImp True (delab i rhs)
176−process (Info n) = do i <- get
177− let oi = lookupCtxt Nothing n (idris_optimisation i)
178− liftIO $ print oi
179−process (Spec t) = do (tm, ty) <- elabVal toplevel False t
180− ctxt <- getContext
181− ist <- get
182− let tm' = specialise ctxt (idris_statics ist) tm
183− iputStrLn (show (delab ist tm'))
184−process (Prove n) = prover n
185−process (HNF t) = do (tm, ty) <- elabVal toplevel False t
186− ctxt <- getContext
187− ist <- get
188− let tm' = simplify ctxt [] tm
189− iputStrLn (show (delab ist tm'))
190−process TTShell = do ist <- get
191− let shst = initState (tt_ctxt ist)
192− shst' <- lift $ runShell shst
193− return ()
194−process Execute = do (m, _) <- elabVal toplevel False
182+process fn (Info n) = do i <- get
183+ let oi = lookupCtxt Nothing n (idris_optimisation i)
184+ liftIO $ print oi
185+process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t
186+ ctxt <- getContext
187+ ist <- get
188+ let tm' = specialise ctxt (idris_statics ist) tm
189+ iputStrLn (show (delab ist tm'))
190+process fn (Prove n) = prover (lit fn) n
191+process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t
192+ ctxt <- getContext
193+ ist <- get
194+ let tm' = simplify ctxt [] tm
195+ iputStrLn (show (delab ist tm'))
196+process fn TTShell = do ist <- get
197+ let shst = initState (tt_ctxt ist)
198+ shst' <- lift $ runShell shst
199+ return ()
200+process fn Execute = do (m, _) <- elabVal toplevel False
195201 (PApp fc
196202 (PRef fc (UN "run__IO"))
197203 [pexp $ PRef fc (NS (UN "main") ["main"])])
198204-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))
199− (tmpn, tmph) <- liftIO tempfile
200− liftIO $ hClose tmph
201− compile tmpn m
202− liftIO $ system tmpn
203− return ()
205+ (tmpn, tmph) <- liftIO tempfile
206+ liftIO $ hClose tmph
207+ compile tmpn m
208+ liftIO $ system tmpn
209+ return ()
204210 where fc = FC "main" 0
205−process (Compile f) = do (m, _) <- elabVal toplevel False
211+process fn (Compile f) = do (m, _) <- elabVal toplevel False
206212 (PApp fc
207213 (PRef fc (UN "run__IO"))
208214 [pexp $ PRef fc (NS (UN "main") ["main"])])
209− compile f m
215+ compile f m
210216 where fc = FC "main" 0
211−process (LogLvl i) = setLogLevel i
212−process Metavars = do ist <- get
217+process fn (LogLvl i) = setLogLevel i
218+process fn Metavars
219+ = do ist <- get
213220 let mvs = idris_metavars ist \\ primDefs
214221 case mvs of
215222 [] -> iputStrLn "No global metavariables to solve"
216223 _ -> iputStrLn $ "Global metavariables:\n\t" ++ show mvs
217−process NOP = return ()
224+process fn NOP = return ()
218225
219226displayHelp = let vstr = showVersion version in
220227 "\nIdris version " ++ vstr ++ "\n" ++