From 32cebc3e76f682cc7299053b82f78d835f477efa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 14 Dec 2019 12:54:59 -0800
Subject: [PATCH] feat: add `getBaseStructurePath`

---
 src/Init/Lean/Structure.lean  | 17 +++++++++++++++++
 tests/lean/run/structure.lean |  2 ++
 2 files changed, 19 insertions(+)

diff --git a/src/Init/Lean/Structure.lean b/src/Init/Lean/Structure.lean
index 2f4dbb0041..57e0bc64d6 100644
--- a/src/Init/Lean/Structure.lean
+++ b/src/Init/Lean/Structure.lean
@@ -121,4 +121,21 @@ if isStructureLike env constName then
 else
   false
 
+partial def getPathToBaseStructureAux (env : Environment) (baseStructName : Name) : Name → List Name → Option (List Name)
+| structName, path =>
+  if baseStructName == structName then
+    some path.reverse
+  else
+    let fieldNames := getStructureFields env structName;
+    fieldNames.find? $ fun fieldName =>
+      match isSubobjectField? env structName fieldName with
+      | none                  => none
+      | some parentStructName => getPathToBaseStructureAux parentStructName ((structName ++ fieldName) :: path)
+
+/--
+  If `baseStructName` is an ancestor structure for `structName`, then return a sequence of projection functions
+  to go from `structName` to `baseStructName`. -/
+def getPathToBaseStructure? (env : Environment) (baseStructName : Name) (structName : Name) : Option (List Name) :=
+getPathToBaseStructureAux env baseStructName structName []
+
 end Lean
diff --git a/tests/lean/run/structure.lean b/tests/lean/run/structure.lean
index cd47b5509f..dd8206c333 100644
--- a/tests/lean/run/structure.lean
+++ b/tests/lean/run/structure.lean
@@ -40,6 +40,8 @@ do env ← MetaIO.getEnv;
    check $ !isStructure env `D;
    IO.println (getStructureFieldsFlattened env `S4);
    IO.println (getStructureFields env `D);
+   IO.println (getPathToBaseStructure? env `S1 `S4);
+   check $ getPathToBaseStructure? env `S1 `S4 == some [`S4.toS2, `S2.toS1];
    pure ()
 
 #eval tst