git.iko.soy/Idris-dev
on master help sign in
Change disambiguation rules back
f9c3fd9Edwin Brady
src/Idris/Core/Elaborate.hs+1−4
compare with master
unifiedsplit
@@ -761,11 +761,8 @@ try' t1 t2 proofSearch
761 ulog <- getUnifyLog
761 ulog <- getUnifyLog
762 ivs <- get_instances
762 ivs <- get_instances
763 case prunStateT 999999 False ps t1 s of
763 case prunStateT 999999 False ps t1 s of
764− OK ((v, _, _), s')
764+ OK ((v, _, _), s') -> do put s'
765− | length (instances (proof s')) <= length ivs ->
766− do put s'
767 return $! v
765 return $! v
768− | otherwise -> t2
769 Error e1 -> traceWhen ulog ("try failed " ++ show e1) $
766 Error e1 -> traceWhen ulog ("try failed " ++ show e1) $
770 if recoverableErr e1 then
767 if recoverableErr e1 then
771 do case runStateT t2 s of
768 do case runStateT t2 s of
src/Idris/Elab/Value.hs+9−3
@@ -115,11 +115,17 @@ elabDocTerms info str = do typechecked <- Traversable.mapM decorate str
115 else Checked tm
115 else Checked tm
116 | otherwise = Unchecked
116 | otherwise = Unchecked
117
117
118+-- Try running the term directly (as IO ()), then printing it as an Integer
119+-- (as a default numeric tye), then printing it as any Showable thing
118elabExec :: FC -> PTerm -> PTerm
120elabExec :: FC -> PTerm -> PTerm
119elabExec fc tm = runtm (PAlternative False
121elabExec fc tm = runtm (PAlternative False
120− [PApp fc (PRef fc (sUN "printLn"))
122+ [printtm (PApp fc (PRef fc (sUN "the"))
121− [pimp (sUN "ffi") (PRef fc (sUN "FFI_C")) False, pexp tm],
123+ [pexp (PConstant (AType (ATInt ITBig))), pexp tm]),
122− tm])
124+ tm,
125+ printtm tm
126+ ])
123 where
127 where
124 runtm t = PApp fc (PRef fc (sUN "run__IO")) [pexp t]
128 runtm t = PApp fc (PRef fc (sUN "run__IO")) [pexp t]
129+ printtm t = PApp fc (PRef fc (sUN "printLn"))
130+ [pimp (sUN "ffi") (PRef fc (sUN "FFI_C")) False, pexp t]
125
131