From 4646bb0d1c65249e1f0a318366735f83836cf2a9 Mon Sep 17 00:00:00 2001
From: Arnaud Bailly <arnaud.oqube@gmail.com>
Date: Wed, 28 Aug 2019 08:40:00 +0200
Subject: [PATCH] expose current Idris2 version as a proper type

---
 Makefile                       |  2 +-
 src/Idris/IDEMode/Commands.idr |  9 +++++----
 src/Idris/Version.idr          | 32 ++++++++++++++++++++++++++++++++
 tests/Main.idr                 |  7 ++++++-
 4 files changed, 44 insertions(+), 6 deletions(-)
 create mode 100644 src/Idris/Version.idr

diff --git a/Makefile b/Makefile
index 5f7e72b..df0d144 100644
--- a/Makefile
+++ b/Makefile
@@ -18,7 +18,7 @@ idris2: src/YafflePaths.idr check_version
 	idris --build idris2.ipkg
 
 src/YafflePaths.idr:
-	echo 'module YafflePaths; export yprefix : String; yprefix = "${PREFIX}"' > src/YafflePaths.idr
+	@echo 'module YafflePaths; export yprefix : String; yprefix = "${PREFIX}"; export yversion : ((Nat,Nat,Nat), String); yversion = ((2,0,0), "alpha")' > src/YafflePaths.idr
 
 prelude:
 	make -C libs/prelude IDRIS2=../../idris2
diff --git a/src/Idris/IDEMode/Commands.idr b/src/Idris/IDEMode/Commands.idr
index ac56125..b65430a 100644
--- a/src/Idris/IDEMode/Commands.idr
+++ b/src/Idris/IDEMode/Commands.idr
@@ -25,7 +25,8 @@ data IDECommand
      | MakeLemma Integer String
      | MakeCase Integer String
      | MakeWith Integer String
-    
+     | Version
+
 readHints : List SExp -> Maybe (List String)
 readHints [] = Just []
 readHints (StringAtom s :: rest)
@@ -46,7 +47,7 @@ getIDECommand (SExpList [SymbolAtom "type-of", StringAtom n])
 getIDECommand (SExpList [SymbolAtom "type-of", StringAtom n,
                          IntegerAtom l, IntegerAtom c])
     = Just $ TypeOf n (Just (l, c))
-getIDECommand (SExpList [SymbolAtom "case-split", IntegerAtom l, IntegerAtom c, 
+getIDECommand (SExpList [SymbolAtom "case-split", IntegerAtom l, IntegerAtom c,
                          StringAtom n])
     = Just $ CaseSplit l c n
 getIDECommand (SExpList [SymbolAtom "case-split", IntegerAtom l, StringAtom n])
@@ -129,7 +130,7 @@ SExpable Name where
 
 export
 (SExpable a, SExpable b) => SExpable (a, b) where
-  toSExp (x, y) 
+  toSExp (x, y)
       = case toSExp y of
              SExpList xs => SExpList (toSExp x :: xs)
              y' => SExpList [toSExp x, y']
@@ -151,7 +152,7 @@ hex : File -> Int -> IO ()
 hex (FHandle h) num = foreign FFI_C "fprintf" (Ptr -> String -> Int -> IO ()) h "%06x" num
 
 sendLine : File -> String -> IO ()
-sendLine (FHandle h) st = 
+sendLine (FHandle h) st =
   map (const ()) (prim_fwrite h st)
 
 export
diff --git a/src/Idris/Version.idr b/src/Idris/Version.idr
new file mode 100644
index 0000000..3cead36
--- /dev/null
+++ b/src/Idris/Version.idr
@@ -0,0 +1,32 @@
+||| Sets and display version of Idris 2
+module Idris.Version
+
+import YafflePaths
+
+||| Semantic versioning with optional tag
+||| See [semver](https://semver.org/) for proper definition of semantic versioning
+public export
+record Version where
+  constructor MkVersion
+  ||| Semantic version
+  ||| Should follow the (major, minor, patch) convention
+  semVer : (Nat, Nat, Nat)
+  ||| Optional tag
+  ||| Usually contains git sha1 of this software's build in between releases
+  versionTag : Maybe String
+
+export
+version : Version
+version with (yversion)
+  | (s,"") = MkVersion s Nothing
+  | (s,t) = MkVersion s (Just t)
+
+export
+showVersion : Version -> String
+showVersion (MkVersion (maj,min,patch) versionTag) =
+  concat (intersperse "." (map show [ maj, min, patch])) ++ showTag
+  where
+    showTag : String
+    showTag = case versionTag of
+                Nothing => ""
+                Just tag => "-" ++ tag
diff --git a/tests/Main.idr b/tests/Main.idr
index 862ce54..57a4ce5 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -64,6 +64,10 @@ chezTests
    = ["chez001", "chez002", "chez003", "chez004",
       "chez005", "chez006", "chez007"]
 
+ideModeTests : List String
+ideModeTests
+  =  [ "ideMode002" ]
+
 chdir : String -> IO Bool
 chdir dir
     = do ok <- foreign FFI_C "chdir" (String -> IO Int) dir
@@ -136,7 +140,8 @@ main
          let filteredNonCGTests =
               filterTests $ concat [testPaths "ttimp" ttimpTests,
                                     testPaths "idris2" idrisTests,
-                                    testPaths "typedd-book" typeddTests]
+                                    testPaths "typedd-book" typeddTests,
+                                    testPaths "ideMode" ideModeTests]
          let filteredChezTests = filterTests (testPaths "chez" chezTests)
          nonCGTestRes <- traverse (runTest idris2) filteredNonCGTests
          chezTestRes <- if length filteredChezTests > 0