max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add getBaseStructurePath

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-14 12:54:59 -08:00
parent a80c5c8339
commit 32cebc3e76
2 changed files with 19 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/Init/Lean/Structure.lean
View file

@ -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

2
tests/lean/run/structure.lean
View file

@ -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