idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-17 08:11:45 +03:00
Code Issues Projects Releases Wiki Activity
2ac4bea220
Idris2/tests/idris2/reflection001/expected

39 lines
4.0 KiB
Plaintext
Raw Normal View History

Make a start on reflection Don't get too excited yet - I want this in so that it doesn't get too out of sync, but I still have to think about exactly how it's going to work in practice.
2020-05-30 00:40:29 +03:00
1/1: Building quote (quote.idr)
Implementations and errors - Added initial implementations for terms and values - Error messages converted to pretty printer - Colorization for error messages - Color and console width option both as command line and repl command
2020-07-28 15:11:42 +03:00
Error: While processing right hand side of bad. When unifying Int and TTImp.
Mismatch between: Int and TTImp.
quote.idr:25:19--25:22
Show more codes in error report
2021-02-11 20:24:26 +03:00
21 | bad : Int -> TTImp
22 | bad val
23 | = `(let xfn : Int -> Int
24 | xfn var = var * 2 in
PTerm and error intial prettyprinting
2020-07-22 22:16:43 +03:00
25 | xfn ~(val))
Show more codes in error report
2021-02-11 20:24:26 +03:00
^^^
Implementations and errors - Added initial implementations for terms and values - Error messages converted to pretty printer - Colorization for error messages - Color and console width option both as command line and repl command
2020-07-28 15:11:42 +03:00
Missing runElab decl check
2020-09-16 00:29:48 +03:00
Error: %language ElabReflection not enabled
quote.idr:33:1--33:21
Show more codes in error report
2021-02-11 20:24:26 +03:00
29 |
30 | noExtension : Elab ()
31 | noExtension = fail "Should not print this message"
32 |
Missing runElab decl check
2020-09-16 00:29:48 +03:00
33 | %runElab noExtension
Show more codes in error report
2021-02-11 20:24:26 +03:00
^^^^^^^^^^^^^^^^^^^^
Missing runElab decl check
2020-09-16 00:29:48 +03:00
Error: Error during reflection: Should not print this message
quote.idr:37:1--37:21
Show more codes in error report
2021-02-11 20:24:26 +03:00
33 | %runElab noExtension
34 |
35 | %language ElabReflection
36 |
Missing runElab decl check
2020-09-16 00:29:48 +03:00
37 | %runElab noExtension
Show more codes in error report
2021-02-11 20:24:26 +03:00
^^^^^^^^^^^^^^^^^^^^
Missing runElab decl check
2020-09-16 00:29:48 +03:00
Make a start on reflection Don't get too excited yet - I want this in so that it doesn't get too out of sync, but I still have to think about exactly how it's going to work in practice.
2020-05-30 00:40:29 +03:00
Main> IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IVar (MkFC "quote.idr" (3, 12) (3, 23)) (UN "+")) (IApp (MkFC "quote.idr" (6, 13) (6, 14)) (IVar (MkFC "quote.idr" (6, 13) (6, 14)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (6, 13) (6, 14)) (BI 3)))) (IApp (MkFC "quote.idr" (6, 18) (6, 19)) (IVar (MkFC "quote.idr" (6, 18) (6, 19)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (6, 18) (6, 19)) (BI 4)))
Main> IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IVar (MkFC "quote.idr" (3, 12) (3, 23)) (UN "+")) (IVar (MkFC "(interactive)" (0, 6) (0, 10)) (UN "True"))) (IVar (MkFC "(interactive)" (0, 14) (0, 19)) (UN "False"))
Make :typeat a useful command (#998) Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-02-05 19:15:40 +03:00
Main> ILocal (MkFC "quote.idr" (10, 12) (11, 29)) [IClaim (MkFC "quote.idr" (10, 12) (10, 28)) MW Private [] (MkTy (MkFC "quote.idr" (10, 12) (10, 28)) (MkFC "quote.idr" (10, 12) (10, 15)) (UN "xfn") (IPi (MkFC "quote.idr" (10, 18) (10, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC "quote.idr" (10, 18) (10, 21)) IntType) (IPrimVal (MkFC "quote.idr" (10, 25) (10, 28)) IntType))), IDef (MkFC "quote.idr" (11, 12) (11, 29)) (UN "xfn") [PatClause (MkFC "quote.idr" (11, 12) (11, 29)) (IApp (MkFC "quote.idr" (11, 12) (11, 19)) (IVar (MkFC "quote.idr" (11, 12) (11, 15)) (UN "xfn")) (IBindVar (MkFC "quote.idr" (11, 16) (11, 19)) "var")) (IApp (MkFC "quote.idr" (11, 22) (11, 29)) (IApp (MkFC "quote.idr" (11, 22) (11, 29)) (IVar (MkFC "quote.idr" (11, 22) (11, 29)) (UN "*")) (IVar (MkFC "quote.idr" (11, 22) (11, 25)) (UN "var"))) (IApp (MkFC "quote.idr" (11, 28) (11, 29)) (IVar (MkFC "quote.idr" (11, 28) (11, 29)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (11, 28) (11, 29)) (BI 2))))]] (IApp (MkFC "quote.idr" (12, 12) (12, 22)) (IVar (MkFC "quote.idr" (12, 12) (12, 15)) (UN "xfn")) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IVar (MkFC "(interactive)" (0, 9) (0, 12)) (UN "the")) (IPrimVal (MkFC "(interactive)" (0, 13) (0, 16)) IntType)) (IApp (MkFC "(interactive)" (0, 17) (0, 22)) (IVar (MkFC "(interactive)" (0, 17) (0, 22)) (UN "fromInteger")) (IPrimVal (MkFC "(interactive)" (0, 17) (0, 22)) (BI 99994)))))
Main> ILocal (MkFC "quote.idr" (16, 12) (17, 29)) [IClaim (MkFC "quote.idr" (16, 12) (16, 28)) MW Private [] (MkTy (MkFC "quote.idr" (16, 12) (16, 28)) (MkFC "quote.idr" (16, 12) (16, 15)) (UN "xfn") (IPi (MkFC "quote.idr" (16, 18) (16, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC "quote.idr" (16, 18) (16, 21)) IntType) (IPrimVal (MkFC "quote.idr" (16, 25) (16, 28)) IntType))), IDef (MkFC "quote.idr" (17, 12) (17, 29)) (UN "xfn") [PatClause (MkFC "quote.idr" (17, 12) (17, 29)) (IApp (MkFC "quote.idr" (17, 12) (17, 19)) (IVar (MkFC "quote.idr" (17, 12) (17, 15)) (UN "xfn")) (IBindVar (MkFC "quote.idr" (17, 16) (17, 19)) "var")) (IApp (MkFC "quote.idr" (17, 22) (17, 29)) (IApp (MkFC "quote.idr" (17, 22) (17, 29)) (IVar (MkFC "quote.idr" (17, 22) (17, 29)) (UN "*")) (IVar (MkFC "quote.idr" (17, 22) (17, 25)) (UN "var"))) (IApp (MkFC "quote.idr" (17, 28) (17, 29)) (IVar (MkFC "quote.idr" (17, 28) (17, 29)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (17, 28) (17, 29)) (BI 2))))]] (IApp (MkFC "quote.idr" (18, 12) (18, 43)) (IVar (MkFC "quote.idr" (18, 12) (18, 15)) (UN "xfn")) (IPrimVal EmptyFC (I 99994)))
[ refactor ] introducing Namespace (#638) Until now namespaces were stored as (reversed) lists of strings. It led to: * confusing code where we work on the underlying representation of namespaces rather than say what we mean (using `isSuffixOf` to mean `isParentOf`) * potentially introducing errors by not respecting the invariant cf. bug report #616 (but also name generation in the scheme backend although that did not lead to bugs as it was self-consistent AFAICT) * ad-hoc code to circumvent overlapping interface implementation when showing / pretty-printing namespaces This PR introduces a `Namespace` newtype containing a list of strings. Nested namespaces are still stored in reverse order but the exposed interface aims to support programming by saying what we mean (`isParentOf`, `isApproximationOf`, `X <.> Y` computes to `X.Y`, etc.) irrespective of the underlying representation.
2020-09-05 11:41:31 +03:00
Main> [UN "names", NS (MkNS ["Prelude"]) (UN "+")]
Make a start on reflection Don't get too excited yet - I want this in so that it doesn't get too out of sync, but I still have to think about exactly how it's going to work in practice.
2020-05-30 00:40:29 +03:00
Main> Bye for now!
Reference in New Issue Copy Permalink