b2017d2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Pattern variables should be lifted to top level

...since pattern variables scope across the whole expression. If we don't lift them, mysterious unification errors can happen for implicit arguments.

commitb2017d2625a01abd9cdc7badadd394a25dc614ff authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 27 Nov 2014, 11:35 (12 years ago) parentc87ea77

5 files changed+20−3

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+3−1 src/Idris/ElabTerm.hs+1−1 src/Idris/REPL.hs+8 src/Idris/REPLParser.hs+7 test/error003/expected+1−1

src/Idris/AbsSyntaxTree.hs+3−1

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

345345 | DynamicLink FilePath

346346 | ListDynamic

347347 | Pattelab PTerm

348− | DebugInfo Name

349348 | Search PTerm

350349 | CaseSplitAt Bool Int Name

351350 | AddClauseFrom Bool Int Name

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

372371 | PrintDef Name

373372 | PPrint OutputFmt Int PTerm

374373 | TransformInfo Name

374+ -- Debugging commands

375+ | DebugInfo Name

376+ | DebugUnify PTerm PTerm

375377

376378data OutputFmt = HTMLOutput | LaTeXOutput

377379

src/Idris/ElabTerm.hs+1−1

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

351351 else if (defined && not guarded)

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

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

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

354+ (do patvar n; update_term liftPats)

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

356356 [] -> False

357357 _ -> True

src/Idris/REPL.hs+8

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

4848import Idris.Core.Evaluate

4949import Idris.Core.Execute (execute)

5050import Idris.Core.TT

51+import Idris.Core.Unify

5152import Idris.Core.Constraints

5253

5354import IRTS.Compiler

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

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

930931 ts

931932

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)

932940

933941process fn (DebugInfo n)

934942 = do i <- getIState

src/Idris/REPLParser.hs+7

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

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

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

9191

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+

9299 , unrecognized

93100 , nop

94101 ]

test/error003/expected+1−1

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

11ErrorReflection.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 ()