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

Feat: Add getAllParentStructures

Browse source
This commit is contained in:
Leonardo de Moura 2021-04-07 17:14:15 -07:00
parent 6c0f3c277f
commit 6d361b91b5
2 changed files with 30 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Lean/Structure.lean
View file

@ -82,6 +82,15 @@ def getParentStructures (env : Environment) (structName : Name) : Array Name :=
| some parentStructName => acc.push parentStructName
| none => acc
/-- Return all parent structures -/
partial def getAllParentStructures (env : Environment) (structName : Name) : Array Name :=
visit structName |>.run #[] |>.2
where
visit (structName : Name) : StateT (Array Name) Id Unit := do
for p in getParentStructures env structName do
modify fun s => s.push p
visit p
/-- `findField? env S fname`. If `fname` is defined in a parent `S'` of `S`, return `S'` -/
partial def findField? (env : Environment) (structName : Name) (fieldName : Name) : Option Name :=
if (getStructureFields env structName).contains fieldName then

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

@ -24,25 +24,27 @@ inductive D
| mk (x y z : Nat) : D
def tst : CoreM Unit :=
do let env ← getEnv;
IO.println (getStructureFields env `Lean.Environment);
check $ getStructureFields env `S4 == #[`toS2, `toS3, `s];
check $ getStructureFields env `S1 == #[`x, `y];
check $ isSubobjectField? env `S4 `toS2 == some `S2;
check $ getParentStructures env `S4 == #[`S2, `S3];
check $ findField? env `S4 `x == some `S1;
check $ findField? env `S4 `x1 == none;
check $ isStructure env `S1;
check $ isStructure env `S2;
check $ isStructure env `S3;
check $ isStructure env `S4;
check $ isStructure env `S5;
check $ !isStructure env `Nat;
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];
do let env ← getEnv
IO.println (getStructureFields env `Lean.Environment)
check $ getStructureFields env `S4 == #[`toS2, `toS3, `s]
check $ getStructureFields env `S1 == #[`x, `y]
check $ isSubobjectField? env `S4 `toS2 == some `S2
check $ getParentStructures env `S4 == #[`S2, `S3]
check $ findField? env `S4 `x == some `S1
check $ findField? env `S4 `x1 == none
check $ isStructure env `S1
check $ isStructure env `S2
check $ isStructure env `S3
check $ isStructure env `S4
check $ isStructure env `S5
check $ !isStructure env `Nat
check $ !isStructure env `D
IO.println (getStructureFieldsFlattened env `S4)
IO.println (getStructureFields env `D)
IO.println (getPathToBaseStructure? env `S1 `S4)
IO.println (getParentStructures env `S4)
IO.println (getAllParentStructures env `S4)
check $ getPathToBaseStructure? env `S1 `S4 == some [`S4.toS2, `S2.toS1]
pure ()
#eval tst