b2017d2 · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+3−1

compare with master

unifiedsplit

@@ -345,7 +345,6 @@ data Command = Quit

345 | DynamicLink FilePath

346 | ListDynamic

347 | Pattelab PTerm

348− | DebugInfo Name

349 | Search PTerm

348 | Search PTerm

350 | CaseSplitAt Bool Int Name

349 | CaseSplitAt Bool Int Name

351 | AddClauseFrom Bool Int Name

350 | AddClauseFrom Bool Int Name

@@ -372,6 +371,9 @@ data Command = Quit

372 | PrintDef Name

371 | PrintDef Name

373 | PPrint OutputFmt Int PTerm

372 | PPrint OutputFmt Int PTerm

374 | TransformInfo Name

373 | TransformInfo Name

374+ -- Debugging commands

375+ | DebugInfo Name

376+ | DebugUnify PTerm PTerm

375

377

376data OutputFmt = HTMLOutput | LaTeXOutput

378data OutputFmt = HTMLOutput | LaTeXOutput

377

379

src/Idris/ElabTerm.hs+1−1

@@ -351,7 +351,7 @@ elab ist info emode opts fn tm

351 else if (defined && not guarded)

352 then do apply (Var n) []; solve

353 else try (do apply (Var n) []; solve)

354− (do patvar n; ) -- update_term liftPats)

354+ (do patvar n; update_term liftPats)

355 where inparamBlock n = case lookupCtxtName n (inblock info) of

356 [] -> False

357 _ -> True

src/Idris/REPL.hs+8

@@ -48,6 +48,7 @@ import Util.Pretty hiding ((</>))

48import Idris.Core.Evaluate

49import Idris.Core.Execute (execute)

50import Idris.Core.TT

51+import Idris.Core.Unify

51import Idris.Core.Constraints

52import Idris.Core.Constraints

52

53

53import IRTS.Compiler

54import IRTS.Compiler

@@ -929,6 +930,13 @@ process fn (TotCheck n)

929 map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $

930 map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $

930 ts

931 ts

931

932

933+process fn (DebugUnify l r)

934+ = do (ltm, _) <- elabVal recinfo ERHS l

935+ (rtm, _) <- elabVal recinfo ERHS r

936+ ctxt <- getContext

937+ case unify ctxt [] ltm rtm [] [] [] [] of

938+ OK ans -> iputStrLn (show ans)

939+ Error e -> iputStrLn (show e)

932

940

933process fn (DebugInfo n)

941process fn (DebugInfo n)

934 = do i <- getIState

942 = do i <- getIState

src/Idris/REPLParser.hs+7

@@ -89,6 +89,13 @@ pCmd = choice [ do c <- cmd ["q", "quit"]; noArgs c Quit

89 , do c <- cmd ["ps", "proofsearch"]; cmd_proofsearch c

90 , do c <- cmd ["ref", "refine"]; cmd_refine c

91

92+ , do c <- cmd ["debugunify"];

93+ P.whiteSpace

94+ l <- P.simpleExpr defaultSyntax

95+ r <- P.simpleExpr defaultSyntax

96+ eof

97+ return (Right (DebugUnify l r))

98+

92 , unrecognized

99 , unrecognized

93 , nop

100 , nop

94 ]

101 ]

test/error003/expected+1−1

@@ -1,2 +1,2 @@

1ErrorReflection.idr:67:5:When elaborating right hand side of bad:

2−DSL type error: (t(502) => t'(503)) doesn't match ()

2+DSL type error: (t(503) => t'(504)) doesn't match ()