add test

test/Isabelle.hs

@@ -0,0 +1,10 @@
+module Isabelle
+  ( allTests,
+  )
+where
+
+import Base
+import Isabelle.Positive qualified as P
+
+allTests :: TestTree
+allTests = testGroup "Isabelle tests" [P.allTests]

test/Isabelle/Positive.hs

@@ -0,0 +1,54 @@
+module Isabelle.Positive where
+
+import Base
+import Juvix.Compiler.Backend.Isabelle.Data.Result
+import Juvix.Compiler.Backend.Isabelle.Pretty
+
+data PosTest = PosTest
+  { _name :: String,
+    _dir :: Path Abs Dir,
+    _file :: Path Abs File,
+    _expectedFile :: Path Abs File
+  }
+
+makeLenses ''PosTest
+
+root :: Path Abs Dir
+root = relToProject $(mkRelDir "tests/positive/Isabelle")
+
+posTest :: String -> Path Rel Dir -> Path Rel File -> Path Rel File -> PosTest
+posTest _name rdir rfile efile =
+  let _dir = root <//> rdir
+      _file = _dir <//> rfile
+      _expectedFile = _dir <//> efile
+   in PosTest {..}
+
+testDescr :: PosTest -> TestDescr
+testDescr PosTest {..} =
+  TestDescr
+    { _testName = _name,
+      _testRoot = _dir,
+      _testAssertion = Steps $ \step -> do
+        entryPoint <- testDefaultEntryPointIO _dir _file
+        step "Translate"
+        PipelineResult {..} <- snd <$> testRunIO entryPoint upToIsabelle
+        let thy = _pipelineResult ^. resultTheory
+        step "Checking against expected output file"
+        expFile :: Text <- readFile _expectedFile
+        assertEqDiffText "Compare to expected output" (ppPrint thy <> "\n") expFile
+    }
+
+allTests :: TestTree
+allTests =
+  testGroup
+    "Isabelle positive tests"
+    (map (mkTest . testDescr) tests)
+
+tests :: [PosTest]
+tests =
+  [ posTest
+      "Test Isabelle translation"
+      $(mkRelDir ".")
+      $(mkRelFile "Program.juvix")
+      $(mkRelFile "isabelle/Program.thy")
+  ]

test/Main.hs

@@ -11,6 +11,7 @@ import Examples qualified
 import Format qualified
 import Formatter qualified
 import Internal qualified
+import Isabelle qualified
 import Nockma qualified
 import Package qualified
 import Parsing qualified
@@ -58,6 +59,7 @@ fastTests =
       Formatter.allTests,
       Package.allTests,
       BackendMarkdown.allTests,
+      Isabelle.allTests,
       Nockma.allTests
     ]
 

tests/positive/Isabelle/Package.juvix

@@ -0,0 +1,5 @@
+module Package;
+
+import PackageDescription.V2 open;
+
+package : Package := defaultPackage {name := "isabelle"};

tests/positive/Isabelle/Program.juvix

@@ -0,0 +1,97 @@
+module Program;
+
+import Stdlib.Prelude open;
+
+id0 : Nat -> Nat := id;
+
+id1 : List Nat -> List Nat := id;
+
+id2 {A : Type} : A -> A := id;
+
+add_one : List Nat -> List Nat
+  | [] := []
+  | (x :: xs) := (x + 1) :: add_one xs;
+
+sum : List Nat -> Nat
+  | [] := 0
+  | (x :: xs) := x + sum xs;
+
+f (x y : Nat) : Nat -> Nat
+  | z := (z + 1) * x + y;
+
+g (x y : Nat) : Bool :=
+  if
+    | x == y := false
+    | else := true;
+
+inc (x : Nat) : Nat := suc x;
+
+dec : Nat -> Nat
+  | zero := zero
+  | (suc x) := x;
+
+dec' (x : Nat) : Nat :=
+  case x of zero := zero | suc y := y;
+
+optmap {A} (f : A -> A) : Maybe A -> Maybe A
+  | nothing := nothing
+  | (just x) := just (f x);
+
+pboth {A B A' B'} (f : A -> A') (g : B -> B') : Pair A B -> Pair A' B'
+  | (x, y) := (f x, g y);
+
+bool_fun (x y z : Bool) : Bool := x && y || z;
+
+bool_fun' (x y z : Bool) : Bool := (x && y) || z;
+
+-- Queues
+
+--- A type of Queues
+type Queue (A : Type) := queue : List A -> List A -> Queue A;
+
+qfst : {A : Type} → Queue A → List A
+  | (queue x _) := x;
+
+qsnd : {A : Type} → Queue A → List A
+  | (queue _ x) := x;
+
+pop_front {A} (q : Queue A) : Queue A :=
+    let
+      q' : Queue A := queue (tail (qfst q)) (qsnd q);
+    in case qfst q' of
+         | nil := queue (reverse (qsnd q')) nil
+         | _ := q';
+
+push_back {A} (q : Queue A) (x : A) : Queue A :=
+    case qfst q of
+      | nil := queue (x :: nil) (qsnd q)
+      | q' := queue q' (x :: qsnd q);
+
+is_empty {A} (q : Queue A) : Bool :=
+    case qfst q of
+      | nil :=
+        case qsnd q of {
+          | nil := true
+          | _ := false
+        }
+      | _ := false;
+
+empty : {A : Type} → Queue A := queue nil nil;
+
+-- Multiple let expressions
+
+funkcja (n : Nat) : Nat :=
+  let
+    nat1 : Nat := 1;
+    nat2 : Nat := 2;
+    plusOne (n : Nat) : Nat := n + 1;
+  in plusOne n + nat1 + nat2;
+
+type Either' A B := Left' A | Right' B;
+
+-- Records
+
+type R := mkR {
+  r1 : Nat;
+  r2 : Nat;
+};

tests/positive/Isabelle/isabelle/Program.thy

@@ -0,0 +1,112 @@
+theory Program
+imports Main
+begin
+
+definition id0 :: "nat ⇒ nat" where
+  "id0 = id"
+
+definition id1 :: "nat list ⇒ nat list" where
+  "id1 = id"
+
+definition id2 :: "'A ⇒ 'A" where
+  "id2 = id"
+
+fun add_one :: "nat list ⇒ nat list" where
+  "add_one [] = []" |
+  "add_one (x # xs) = ((x + 1) # add_one xs)"
+
+fun sum :: "nat list ⇒ nat" where
+  "sum [] = 0" |
+  "sum (x # xs) = (x + sum xs)"
+
+fun f :: "nat ⇒ nat ⇒ nat ⇒ nat" where
+  "f x y z = ((z + 1) * x + y)"
+
+fun g :: "nat ⇒ nat ⇒ bool" where
+  "g x y = (if x = y then False else True)"
+
+fun inc :: "nat ⇒ nat" where
+  "inc x = (Suc x)"
+
+fun dec :: "nat ⇒ nat" where
+  "dec 0 = 0" |
+  "dec (Suc x) = x"
+
+fun dec' :: "nat ⇒ nat" where
+  "dec' x =
+    (case x of
+       0 ⇒ 0 |
+       (Suc y) ⇒ y)"
+
+fun optmap :: "('A ⇒ 'A) ⇒ 'A option ⇒ 'A option" where
+  "optmap f' None = None" |
+  "optmap f' (Some x) = (Some (f' x))"
+
+fun pboth :: "('A ⇒ 'A') ⇒ ('B ⇒ 'B') ⇒ 'A × 'B ⇒ 'A' × 'B'" where
+  "pboth f' g' (x, y) = (f' x, g' y)"
+
+fun bool_fun :: "bool ⇒ bool ⇒ bool ⇒ bool" where
+  "bool_fun x y z = (x ∧ (y ∨ z))"
+
+fun bool_fun' :: "bool ⇒ bool ⇒ bool ⇒ bool" where
+  "bool_fun' x y z = (x ∧ y ∨ z)"
+
+datatype 'A Queue
+  = queue "'A list" "'A list"
+
+fun qfst :: "'A Queue ⇒ 'A list" where
+  "qfst (queue x ω) = x"
+
+fun qsnd :: "'A Queue ⇒ 'A list" where
+  "qsnd (queue ω x) = x"
+
+fun pop_front :: "'A Queue ⇒ 'A Queue" where
+  "pop_front q =
+    (let
+       q' = queue (tl (qfst q)) (qsnd q)
+     in case qfst q' of
+          [] ⇒ queue (rev (qsnd q')) [] |
+          ω ⇒ q')"
+
+fun push_back :: "'A Queue ⇒ 'A ⇒ 'A Queue" where
+  "push_back q x =
+    (case qfst q of
+       [] ⇒ queue [x] (qsnd q) |
+       q' ⇒ queue q' (x # qsnd q))"
+
+fun is_empty :: "'A Queue ⇒ bool" where
+  "is_empty q =
+    (case qfst q of
+       [] ⇒
+         (case qsnd q of
+            [] ⇒ True |
+            ω ⇒ False) |
+       ω ⇒ False)"
+
+definition empty :: "'A Queue" where
+  "empty = queue [] []"
+
+fun funkcja :: "nat ⇒ nat" where
+  "funkcja n =
+    (let
+       nat1 = 1;
+       nat2 = 2;
+       plusOne = λ x0 . case x0 of
+                          n' ⇒ n' + 1
+     in plusOne n + nat1 + nat2)"
+
+datatype ('A, 'B) Either'
+  = Left' 'A |
+    Right' 'B
+
+record R =
+  r1 :: nat
+  r2 :: nat
+
+fun r1 :: "R ⇒ nat" where
+  "r1 (mkR a b) = a"
+
+fun r2 :: "R ⇒ nat" where
+  "r2 (mkR a b) = b"
+
+end