idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-16 07:34:45 +03:00
Code Issues Projects Releases Wiki Activity
b192be32b8
Idris2/tests/idris2/reflection001/expected
Ruslan Feizerakhmanov 7aee7c9b7c
[ new ] --install-with-src; refactoring around FCs (#1450) 
Why:

* To implement robust cross-project go-to-definition in LSP
  i.e you can jump to definition of any global name coming
  from library dependencies, as well as from the local project files.

What it does:

*  Modify `FC`s to carry `ModuleIdent` for .idr sources,
   file name for .ipkg sources or nothing for interactive runs.

*  Add `--install-with-src` to install the source code alongside
   the ttc binaries. The source is installed into the same directory
   as the corresponding ttc file. Installed sources are made read-only.

*  As we install the sources pinned to the related ttc files we gain
   the versioning of sources for free.
2021-06-05 12:53:22 +01:00

39 lines
5.2 KiB
Plaintext
Raw Blame History

1/1: Building quote (quote.idr)
Error: While processing right hand side of bad. When unifying Int and TTImp.
Mismatch between: Int and TTImp.
quote:25:19--25:22
21 | bad : Int -> TTImp
22 | bad val
23 | = `(let xfn : Int -> Int
24 | xfn var = var * 2 in
25 | xfn ~(val))
^^^
Error: %language ElabReflection not enabled
quote:33:1--33:21
29 |
30 | noExtension : Elab ()
31 | noExtension = fail "Should not print this message"
32 |
33 | %runElab noExtension
^^^^^^^^^^^^^^^^^^^^
Error: Error during reflection: Should not print this message
quote:37:1--37:21
33 | %runElab noExtension
34 |
35 | %language ElabReflection
36 |
37 | %runElab noExtension
^^^^^^^^^^^^^^^^^^^^
Main> IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 12) (3, 23)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 12) (3, 23)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 17) (3, 18)) (UN "+")) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 13) (6, 14)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 13) (6, 14)) (UN "fromInteger")) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 13) (6, 14)) (BI 3)))) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 18) (6, 19)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 18) (6, 19)) (UN "fromInteger")) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 18) (6, 19)) (BI 4)))
Main> IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 12) (3, 23)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 12) (3, 23)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 17) (3, 18)) (UN "+")) (IVar (MkFC (Virtual Interactive) (0, 6) (0, 10)) (UN "True"))) (IVar (MkFC (Virtual Interactive) (0, 14) (0, 19)) (UN "False"))
Main> ILocal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 12) (11, 29)) [IClaim (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 12) (10, 28)) MW Private [] (MkTy (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 12) (10, 15)) (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 12) (10, 15)) (UN "xfn") (IPi (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 18) (10, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 18) (10, 21)) IntType) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 25) (10, 28)) IntType))), IDef (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 29)) (UN "xfn") [PatClause (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 19)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 15)) (UN "xfn")) (IBindVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 16) (11, 19)) "var")) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 22) (11, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 22) (11, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 26) (11, 27)) (UN "*")) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 22) (11, 25)) (UN "var"))) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 28) (11, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 28) (11, 29)) (UN "fromInteger")) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 28) (11, 29)) (BI 2))))]] (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (12, 12) (12, 22)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (12, 12) (12, 15)) (UN "xfn")) (IApp (MkFC (Virtual Interactive) (0, 9) (0, 22)) (IApp (MkFC (Virtual Interactive) (0, 9) (0, 22)) (IVar (MkFC (Virtual Interactive) (0, 9) (0, 12)) (UN "the")) (IPrimVal (MkFC (Virtual Interactive) (0, 13) (0, 16)) IntType)) (IApp (MkFC (Virtual Interactive) (0, 17) (0, 22)) (IVar (MkFC (Virtual Interactive) (0, 17) (0, 22)) (UN "fromInteger")) (IPrimVal (MkFC (Virtual Interactive) (0, 17) (0, 22)) (BI 99994)))))
Main> ILocal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 12) (17, 29)) [IClaim (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 12) (16, 28)) MW Private [] (MkTy (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 12) (16, 15)) (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 12) (16, 15)) (UN "xfn") (IPi (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 18) (16, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 18) (16, 21)) IntType) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 25) (16, 28)) IntType))), IDef (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 29)) (UN "xfn") [PatClause (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 19)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 15)) (UN "xfn")) (IBindVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 16) (17, 19)) "var")) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 22) (17, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 22) (17, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 26) (17, 27)) (UN "*")) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 22) (17, 25)) (UN "var"))) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 28) (17, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 28) (17, 29)) (UN "fromInteger")) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 28) (17, 29)) (BI 2))))]] (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (18, 12) (18, 43)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (18, 12) (18, 15)) (UN "xfn")) (IPrimVal EmptyFC (I 99994)))
Main> [UN "names", NS (MkNS ["Prelude"]) (UN "+")]
Main> Bye for now!
Reference in New Issue View Git Blame Copy Permalink