From a53b24b8a046d1620e9d74834f4bcbe43ac93e00 Mon Sep 17 00:00:00 2001
From: Iavor Diatchki <iavor.diatchki@gmail.com>
Date: Mon, 7 Feb 2022 10:19:47 -0800
Subject: [PATCH] Fix paths in nested relative includes

Fixes #1321
---
 src/Cryptol/Parser/NoInclude.hs                            | 4 +++-
 tests/modsys/relative-include/A/B/C.cry                    | 4 ++++
 tests/modsys/relative-include/A/B/D/E/F.cry                | 2 ++
 tests/modsys/relative-include/A/B/G/H.pcry                 | 2 ++
 tests/modsys/relative-include/A/B/G/I.pcry                 | 1 +
 tests/modsys/relative-include/relative-include.icry        | 1 +
 tests/modsys/relative-include/relative-include.icry.stdout | 4 ++++
 7 files changed, 17 insertions(+), 1 deletion(-)
 create mode 100644 tests/modsys/relative-include/A/B/C.cry
 create mode 100644 tests/modsys/relative-include/A/B/D/E/F.cry
 create mode 100644 tests/modsys/relative-include/A/B/G/H.pcry
 create mode 100644 tests/modsys/relative-include/A/B/G/I.pcry
 create mode 100644 tests/modsys/relative-include/relative-include.icry
 create mode 100644 tests/modsys/relative-include/relative-include.icry.stdout

diff --git a/src/Cryptol/Parser/NoInclude.hs b/src/Cryptol/Parser/NoInclude.hs
index 336f2e266..418fb86cb 100644
--- a/src/Cryptol/Parser/NoInclude.hs
+++ b/src/Cryptol/Parser/NoInclude.hs
@@ -196,7 +196,9 @@ resolveInclude lf = pushPath lf $ do
   case parseProgramWith (defaultConfig { cfgSource = thing lf, cfgPreProc = guessPreProc (thing lf) }) source of
 
     Right prog -> do
-      Program ds <- withIncPath (thing lf) (noIncludeProgram prog)
+      Program ds <-
+        do path <- fromIncPath (thing lf)
+           withIncPath path (noIncludeProgram prog)
       return ds
 
     Left err -> M (raise [IncludeParseError err])
diff --git a/tests/modsys/relative-include/A/B/C.cry b/tests/modsys/relative-include/A/B/C.cry
new file mode 100644
index 000000000..262792763
--- /dev/null
+++ b/tests/modsys/relative-include/A/B/C.cry
@@ -0,0 +1,4 @@
+module A::B::C where
+import A::B::D::E::F
+include "G/H.pcry"  // succeeds when run from `test/`
+
diff --git a/tests/modsys/relative-include/A/B/D/E/F.cry b/tests/modsys/relative-include/A/B/D/E/F.cry
new file mode 100644
index 000000000..f386e43c1
--- /dev/null
+++ b/tests/modsys/relative-include/A/B/D/E/F.cry
@@ -0,0 +1,2 @@
+module A::B::D::E::F where
+x = 1
diff --git a/tests/modsys/relative-include/A/B/G/H.pcry b/tests/modsys/relative-include/A/B/G/H.pcry
new file mode 100644
index 000000000..f528fb201
--- /dev/null
+++ b/tests/modsys/relative-include/A/B/G/H.pcry
@@ -0,0 +1,2 @@
+y = 2
+include "I.pcry"
diff --git a/tests/modsys/relative-include/A/B/G/I.pcry b/tests/modsys/relative-include/A/B/G/I.pcry
new file mode 100644
index 000000000..b67ca6a5d
--- /dev/null
+++ b/tests/modsys/relative-include/A/B/G/I.pcry
@@ -0,0 +1 @@
+z = 3
diff --git a/tests/modsys/relative-include/relative-include.icry b/tests/modsys/relative-include/relative-include.icry
new file mode 100644
index 000000000..2b64f2e39
--- /dev/null
+++ b/tests/modsys/relative-include/relative-include.icry
@@ -0,0 +1 @@
+:m A::B::C
diff --git a/tests/modsys/relative-include/relative-include.icry.stdout b/tests/modsys/relative-include/relative-include.icry.stdout
new file mode 100644
index 000000000..a2ed937d4
--- /dev/null
+++ b/tests/modsys/relative-include/relative-include.icry.stdout
@@ -0,0 +1,4 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module A::B::D::E::F
+Loading module A::B::C