mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-09-20 12:27:44 +03:00
Merge pull request #205 from abailly/syntax-highlight
first stab at syntax highlighting in Emacs
This commit is contained in:
Edwin Brady
GitHub
commit
bce7a5e747
@ -9,6 +9,8 @@ import Core.Normalise
|
||||
import Core.TT
|
||||
import Core.TTC
|
||||
|
||||
import Utils.Binary
|
||||
|
||||
-- Additional data we keep about the context to support interactive editing
|
||||
|
||||
public export
|
||||
@ -35,6 +37,15 @@ record Metadata where
|
||||
currentLHS : Maybe ClosedTerm
|
||||
holeLHS : List (Name, ClosedTerm)
|
||||
|
||||
Show Metadata where
|
||||
show (MkMetadata apps names tydecls currentLHS holeLHS)
|
||||
= "Metadata:\n" ++
|
||||
" lhsApps: " ++ show apps ++ "\n" ++
|
||||
" names: " ++ show names ++ "\n" ++
|
||||
" type declarations: " ++ show tydecls ++ "\n" ++
|
||||
" current LHS: " ++ show currentLHS ++ "\n" ++
|
||||
" holes: " ++ show holeLHS
|
||||
|
||||
export
|
||||
initMetadata : Metadata
|
||||
initMetadata = MkMetadata [] [] [] Nothing []
|
||||
@ -266,3 +277,19 @@ readFromTTM fname
|
||||
ttm <- fromBuf bin
|
||||
put MD (metadata ttm)
|
||||
|
||||
||| Read Metadata from given file
|
||||
export
|
||||
readMetadata : (fname : String) -> Core Metadata
|
||||
readMetadata fname
|
||||
= do Right buf <- coreLift $ readFromFile fname
|
||||
| Left err => throw (InternalError (fname ++ ": " ++ show err))
|
||||
bin <- newRef Bin buf
|
||||
MkTTMFile _ md <- fromBuf bin
|
||||
pure md
|
||||
|
||||
||| Dump content of a .ttm file in human-readable format
|
||||
export
|
||||
dumpTTM : (filename : String) -> Core ()
|
||||
dumpTTM fname
|
||||
= do md <- readMetadata fname
|
||||
coreLift $ putStrLn $ show md
|
||||
|
||||
@ -67,6 +67,8 @@ data CLOpt
|
||||
IdeModeSocket String |
|
||||
||| Run as a checker for the core language TTImp
|
||||
Yaffle String |
|
||||
||| Dump metadata from a .ttm file
|
||||
Metadata String |
|
||||
||| Run a REPL command then exit immediately
|
||||
RunREPL String |
|
||||
FindIPKG |
|
||||
@ -139,6 +141,8 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
|
||||
-- Internal debugging options
|
||||
MkOpt ["--yaffle", "--ttimp"] ["ttimp file"] (\f => [Yaffle f])
|
||||
Nothing, -- run ttimp REPL rather than full Idris
|
||||
MkOpt ["--ttm" ] ["ttimp file"] (\f => [Metadata f])
|
||||
Nothing, -- dump metadata information from the given ttm file
|
||||
MkOpt ["--debug-elab-check"] [] [DebugElabCheck]
|
||||
Nothing -- do more elaborator checks (currently conversion in LinearCheck)
|
||||
]
|
||||
|
||||
@ -26,6 +26,7 @@ import Idris.Version
|
||||
|
||||
import Idris.IDEMode.Parser
|
||||
import Idris.IDEMode.Commands
|
||||
import Idris.IDEMode.SyntaxHighlight
|
||||
|
||||
import TTImp.Interactive.CaseSplit
|
||||
import TTImp.Elab
|
||||
@ -115,6 +116,7 @@ getInput f
|
||||
do inp <- getNChars f (cast num)
|
||||
pure (pack inp)
|
||||
|
||||
|
||||
process : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto s : Ref Syn SyntaxInfo} ->
|
||||
@ -124,7 +126,7 @@ process : {auto c : Ref Ctxt Defs} ->
|
||||
process (Interpret cmd)
|
||||
= interpret cmd
|
||||
process (LoadFile fname _)
|
||||
= Idris.REPL.process (Load fname)
|
||||
= Idris.REPL.process (Load fname) >>= outputSyntaxHighlighting fname
|
||||
process (TypeOf n Nothing)
|
||||
= Idris.REPL.process (Check (PRef replFC (UN n)))
|
||||
process (TypeOf n (Just (l, c)))
|
||||
@ -177,18 +179,20 @@ idePutStrLn outf i msg
|
||||
= send outf (SExpList [SymbolAtom "write-string",
|
||||
toSExp msg, toSExp i])
|
||||
|
||||
printIDEWithStatus : File -> Integer -> String -> SExp -> Core ()
|
||||
printIDEWithStatus outf i status msg
|
||||
= do let m = SExpList [SymbolAtom status, toSExp msg,
|
||||
-- highlighting; currently blank
|
||||
SExpList []]
|
||||
send outf (SExpList [SymbolAtom "return", m, toSExp i])
|
||||
returnFromIDE : File -> Integer -> SExp -> Core ()
|
||||
returnFromIDE outf i msg
|
||||
= do send outf (SExpList [SymbolAtom "return", msg, toSExp i])
|
||||
|
||||
printIDEResult : File -> Integer -> SExp -> Core ()
|
||||
printIDEResult outf i msg = printIDEWithStatus outf i "ok" msg
|
||||
printIDEResult outf i msg = returnFromIDE outf i (SExpList [SymbolAtom "ok", toSExp msg])
|
||||
|
||||
printIDEResultWithHighlight : File -> Integer -> SExp -> Core ()
|
||||
printIDEResultWithHighlight outf i msg = returnFromIDE outf i (SExpList [SymbolAtom "ok", toSExp msg
|
||||
-- TODO return syntax highlighted result
|
||||
, SExpList []])
|
||||
|
||||
printIDEError : File -> Integer -> String -> Core ()
|
||||
printIDEError outf i msg = printIDEWithStatus outf i "error" (toSExp msg)
|
||||
printIDEError outf i msg = returnFromIDE outf i (SExpList [SymbolAtom "error", toSExp msg ])
|
||||
|
||||
SExpable REPLEval where
|
||||
toSExp EvalTC = SymbolAtom "typecheck"
|
||||
@ -214,10 +218,10 @@ displayIDEResult : {auto c : Ref Ctxt Defs} ->
|
||||
{auto o : Ref ROpts REPLOpts} ->
|
||||
File -> Integer -> REPLResult -> Core ()
|
||||
displayIDEResult outf i (REPLError err) = printIDEError outf i err
|
||||
displayIDEResult outf i (Evaluated x Nothing) = printIDEResult outf i $ StringAtom $ show x
|
||||
displayIDEResult outf i (Evaluated x (Just y)) = printIDEResult outf i $ StringAtom $ show x ++ " : " ++ show y
|
||||
displayIDEResult outf i (Printed xs) = printIDEResult outf i $ StringAtom $ showSep "\n" xs
|
||||
displayIDEResult outf i (TermChecked x y) = printIDEResult outf i $ StringAtom $ show x ++ " : " ++ show y
|
||||
displayIDEResult outf i (Evaluated x Nothing) = printIDEResultWithHighlight outf i $ StringAtom $ show x
|
||||
displayIDEResult outf i (Evaluated x (Just y)) = printIDEResultWithHighlight outf i $ StringAtom $ show x ++ " : " ++ show y
|
||||
displayIDEResult outf i (Printed xs) = printIDEResultWithHighlight outf i $ StringAtom $ showSep "\n" xs
|
||||
displayIDEResult outf i (TermChecked x y) = printIDEResultWithHighlight outf i $ StringAtom $ show x ++ " : " ++ show y
|
||||
displayIDEResult outf i (FileLoaded x) = printIDEResult outf i $ SExpList []
|
||||
displayIDEResult outf i (ErrorLoadingFile x err) = printIDEError outf i $ "Error loading file " ++ x ++ ": " ++ show err
|
||||
displayIDEResult outf i (ErrorsBuildingFile x errs) = printIDEError outf i $ "Error(s) building file " ++ x ++ ": " ++ (showSep "\n" $ map show errs)
|
||||
|
||||
125
src/Idris/IDEMode/SyntaxHighlight.idr
Normal file
125
src/Idris/IDEMode/SyntaxHighlight.idr
Normal file
@ -0,0 +1,125 @@
|
||||
module Idris.IDEMode.SyntaxHighlight
|
||||
|
||||
import Prelude.Functor as F
|
||||
import Core.Context
|
||||
import Core.InitPrimitives
|
||||
import Core.Metadata
|
||||
import Core.TT
|
||||
|
||||
import Idris.REPL
|
||||
import Idris.IDEMode.Commands
|
||||
|
||||
data Decoration : Type where
|
||||
Typ : Decoration
|
||||
Function : Decoration
|
||||
Data : Decoration
|
||||
Keyword : Decoration
|
||||
Bound : Decoration
|
||||
|
||||
SExpable Decoration where
|
||||
toSExp Typ = SymbolAtom "type"
|
||||
toSExp Function = SymbolAtom "function"
|
||||
toSExp Data = SymbolAtom "data"
|
||||
toSExp Keyword = SymbolAtom "keyword"
|
||||
toSExp Bound = SymbolAtom "bound"
|
||||
|
||||
record Highlight where
|
||||
constructor MkHighlight
|
||||
location : FC
|
||||
name : Name
|
||||
isImplicit : Bool
|
||||
key : String
|
||||
decor : Decoration
|
||||
docOverview : String
|
||||
typ : String
|
||||
ns : String
|
||||
|
||||
SExpable FC where
|
||||
toSExp (MkFC fname (startLine, startCol) (endLine, endCol))
|
||||
= SExpList [ SExpList [ SymbolAtom "filename", StringAtom fname ]
|
||||
, SExpList [ SymbolAtom "start", IntegerAtom (cast startLine + 1), IntegerAtom (cast startCol + 1) ]
|
||||
, SExpList [ SymbolAtom "end", IntegerAtom (cast endLine + 1), IntegerAtom (cast endCol + 1) ]
|
||||
]
|
||||
toSExp EmptyFC = SExpList []
|
||||
|
||||
SExpable Highlight where
|
||||
toSExp (MkHighlight loc nam impl k dec doc t ns)
|
||||
= SExpList [ toSExp loc
|
||||
, SExpList [ SExpList [ SymbolAtom "name", StringAtom (show nam) ]
|
||||
, SExpList [ SymbolAtom "namespace", StringAtom ns ]
|
||||
, SExpList [ SymbolAtom "decor", toSExp dec ]
|
||||
, SExpList [ SymbolAtom "implicit", toSExp impl ]
|
||||
, SExpList [ SymbolAtom "key", StringAtom k ]
|
||||
, SExpList [ SymbolAtom "doc-overview", StringAtom doc ]
|
||||
, SExpList [ SymbolAtom "type", StringAtom t ]
|
||||
]
|
||||
]
|
||||
|
||||
inFile : String -> (FC, (Name, Nat, ClosedTerm)) -> Bool
|
||||
inFile fname (MkFC file _ _, _) = file == fname
|
||||
|
||||
||| Output some data using current dialog index
|
||||
export
|
||||
printOutput : {auto o : Ref ROpts REPLOpts} ->
|
||||
SExp -> Core ()
|
||||
printOutput msg
|
||||
= do opts <- get ROpts
|
||||
case idemode opts of
|
||||
REPL _ => pure ()
|
||||
IDEMode i _ f =>
|
||||
send f (SExpList [SymbolAtom "output",
|
||||
msg, toSExp i])
|
||||
|
||||
|
||||
outputHighlight : {auto opts : Ref ROpts REPLOpts} ->
|
||||
Highlight -> Core ()
|
||||
outputHighlight h =
|
||||
printOutput $ SExpList [ SymbolAtom "ok"
|
||||
, SExpList [ SymbolAtom "highlight-source"
|
||||
, toSExp hlt
|
||||
]
|
||||
]
|
||||
where
|
||||
hlt : List Highlight
|
||||
hlt = [h]
|
||||
|
||||
outputNameSyntax : {auto opts : Ref ROpts REPLOpts} ->
|
||||
(FC, (Name, Nat, ClosedTerm)) -> Core ()
|
||||
outputNameSyntax (fc, (name, _, term)) =
|
||||
let dec = case term of
|
||||
(Local fc x idx y) => Just Bound
|
||||
|
||||
-- See definition of NameType in Core.TT for possible values of Ref's nametype field
|
||||
-- data NameType : Type where
|
||||
-- Bound : NameType
|
||||
-- Func : NameType
|
||||
-- DataCon : (tag : Int) -> (arity : Nat) -> NameType
|
||||
-- TyCon : (tag : Int) -> (arity : Nat) -> NameType
|
||||
(Ref fc Bound name) => Just Bound
|
||||
(Ref fc Func name) => Just Function
|
||||
(Ref fc (DataCon tag arity) name) => Just Data
|
||||
(Ref fc (TyCon tag arity) name) => Just Typ
|
||||
(Meta fc x y xs) => Just Bound
|
||||
(Bind fc x b scope) => Just Bound
|
||||
(App fc fn arg) => Just Bound
|
||||
(As fc x as pat) => Just Bound
|
||||
(TDelayed fc x y) => Nothing
|
||||
(TDelay fc x ty arg) => Nothing
|
||||
(TForce fc x y) => Nothing
|
||||
(PrimVal fc c) => Just Typ
|
||||
(Erased fc imp) => Just Bound
|
||||
(TType fc) => Just Typ
|
||||
hilite = F.map (\ d => MkHighlight fc name False "" d "" (show term) "") dec
|
||||
in maybe (pure ()) outputHighlight hilite
|
||||
|
||||
export
|
||||
outputSyntaxHighlighting : {auto m : Ref MD Metadata} ->
|
||||
{auto opts : Ref ROpts REPLOpts} ->
|
||||
String ->
|
||||
REPLResult ->
|
||||
Core REPLResult
|
||||
outputSyntaxHighlighting fname loadResult = do
|
||||
allNames <- filter (inFile fname) . names <$> get MD
|
||||
-- decls <- filter (inFile fname) . tydecls <$> get MD
|
||||
_ <- traverse outputNameSyntax allNames -- ++ decls)
|
||||
pure loadResult
|
||||
@ -104,6 +104,12 @@ tryYaffle (Yaffle f :: _) = do yaffleMain f []
|
||||
pure True
|
||||
tryYaffle (c :: cs) = tryYaffle cs
|
||||
|
||||
tryTTM : List CLOpt -> Core Bool
|
||||
tryTTM [] = pure False
|
||||
tryTTM (Metadata f :: _) = do dumpTTM f
|
||||
pure True
|
||||
tryTTM (c :: cs) = tryTTM cs
|
||||
|
||||
|
||||
banner : String
|
||||
banner = " ____ __ _ ___ \n" ++
|
||||
@ -119,6 +125,8 @@ stMain : List CLOpt -> Core ()
|
||||
stMain opts
|
||||
= do False <- tryYaffle opts
|
||||
| True => pure ()
|
||||
False <- tryTTM opts
|
||||
| True => pure ()
|
||||
defs <- initDefs
|
||||
c <- newRef Ctxt defs
|
||||
s <- newRef Syn initSyntax
|
||||
|
||||
@ -32,11 +32,7 @@ printWithStatus status msg
|
||||
= do opts <- get ROpts
|
||||
case idemode opts of
|
||||
REPL _ => coreLift $ putStrLn msg
|
||||
IDEMode i _ f =>
|
||||
do let m = SExpList [SymbolAtom status, toSExp msg,
|
||||
-- highlighting; currently blank
|
||||
SExpList []]
|
||||
send f (SExpList [SymbolAtom "return", m, toSExp i])
|
||||
_ => pure () -- this function should never be called in IDE Mode
|
||||
|
||||
export
|
||||
printResult : {auto o : Ref ROpts REPLOpts} ->
|
||||
|
||||
@ -94,7 +94,7 @@ chezTests
|
||||
|
||||
ideModeTests : List String
|
||||
ideModeTests
|
||||
= [ "ideMode001", "ideMode002" ]
|
||||
= [ "ideMode001", "ideMode002", "ideMode003" ]
|
||||
|
||||
chdir : String -> IO Bool
|
||||
chdir dir
|
||||
|
||||
@ -1,4 +1,26 @@
|
||||
000018(:protocol-version 2 0)
|
||||
000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
|
||||
000018(:return (:ok () ()) 1)
|
||||
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 8 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
|
||||
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:176} a)")))))) 1)
|
||||
0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 25)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
|
||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:176}_[] ?{_:177}_[])")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:177}_[]")))))) 1)
|
||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:178}_[] ?{_:177}_[])")))))) 1)
|
||||
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
|
||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:169}_[] ?{_:168}_[])")))))) 1)
|
||||
0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:159} : (Main.Vect n[0] a[1])) -> (({arg:160} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:630:1--637:1 n[2] m[4]) a[3])))")))))) 1)
|
||||
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
||||
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 29) (:end 5 31)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 27) (:end 5 29)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
||||
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 17) (:end 5 19)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 15) (:end 5 17)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
||||
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 41) (:end 5 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 38) (:end 3 39)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
||||
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 25) (:end 3 27)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 23) (:end 3 25)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
||||
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 13) (:end 3 15)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
|
||||
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 2 19) (:end 3 6)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
|
||||
000015(:return (:ok ()) 1)
|
||||
Alas the file is done, aborting
|
||||
|
||||
@ -9,7 +9,7 @@ MAJOR=`echo $VERSION | cut -d. -f1`
|
||||
MINOR=`echo $VERSION | cut -d. -f2`
|
||||
PATCH=`echo $VERSION | cut -d. -f3`
|
||||
|
||||
EXPECTED_LINE="(:return (:ok ((${MAJOR} ${MINOR} ${PATCH}) (\"${TAG}\")) ()) 1)"
|
||||
EXPECTED_LINE="(:return (:ok ((${MAJOR} ${MINOR} ${PATCH}) (\"${TAG}\"))) 1)"
|
||||
EXPECTED_LENGTH=$(expr ${#EXPECTED_LINE} + 1) # +LF
|
||||
|
||||
sed -e "s/__EXPECTED_LINE__/$(printf '%06x' ${EXPECTED_LENGTH})${EXPECTED_LINE}/g" expected.in > expected
|
||||
|
||||
7
tests/ideMode/ideMode003/LocType.idr
Normal file
7
tests/ideMode/ideMode003/LocType.idr
Normal file
@ -0,0 +1,7 @@
|
||||
data Vect : Nat -> Type -> Type where
|
||||
Nil : Vect Z a
|
||||
(::) : a -> Vect k a -> Vect (S k) a
|
||||
|
||||
append : Vect n a -> Vect m a -> Vect (n + m) a
|
||||
append [] ys = ys
|
||||
append (x :: xs) ys = x :: append xs ys
|
||||
27
tests/ideMode/ideMode003/expected
Normal file
27
tests/ideMode/ideMode003/expected
Normal file
@ -0,0 +1,27 @@
|
||||
000018(:protocol-version 2 0)
|
||||
000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
|
||||
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 8 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
|
||||
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:176} a)")))))) 1)
|
||||
0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 25)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
|
||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:176}_[] ?{_:177}_[])")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:177}_[]")))))) 1)
|
||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:178}_[] ?{_:177}_[])")))))) 1)
|
||||
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
|
||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:169}_[] ?{_:168}_[])")))))) 1)
|
||||
0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:159} : (Main.Vect n[0] a[1])) -> (({arg:160} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:630:1--637:1 n[2] m[4]) a[3])))")))))) 1)
|
||||
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
||||
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 29) (:end 5 31)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 27) (:end 5 29)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
||||
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 17) (:end 5 19)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 15) (:end 5 17)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
||||
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 41) (:end 5 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 38) (:end 3 39)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
||||
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 25) (:end 3 27)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 23) (:end 3 25)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
||||
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 13) (:end 3 15)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
|
||||
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 2 19) (:end 3 6)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
|
||||
000015(:return (:ok ()) 1)
|
||||
000037(:return (:ok "Main.Vect : Nat -> Type -> Type" ()) 2)
|
||||
Alas the file is done, aborting
|
||||
2
tests/ideMode/ideMode003/input
Normal file
2
tests/ideMode/ideMode003/input
Normal file
@ -0,0 +1,2 @@
|
||||
00001e((:load-file "LocType.idr") 1)
|
||||
((:type-of "Vect") 2)
|
||||
3
tests/ideMode/ideMode003/run
Executable file
3
tests/ideMode/ideMode003/run
Executable file
@ -0,0 +1,3 @@
|
||||
$1 --ide-mode < input
|
||||
|
||||
rm -rf build
|
||||
Loading…
Reference in New Issue
Block a user