Ontology

definition theorem
legend
structure Concept : Type
  • name : String
Show details

Outer dependencies: (none)

Lean core dependencies: Eq, Nat, String

Used by: Ontology, Ontology.decidableWellFormed, Ontology.empty, Ontology.empty_wellFormed, Ontology.readFile, Ontology.wellFormed, Relation, componentConcept, instDecodeTomlConcept, resolveRelation, systemConcept

structure Relation : Type
  • label : String
  • source : Concept
  • target : Concept
Show details

Outer dependencies: (none)

Inner dependencies: Concept

Lean core dependencies: Eq, Nat, String

Used by: Ontology, Ontology.decidableWellFormed, Ontology.empty, Ontology.empty_wellFormed, Ontology.readFile, Ontology.wellFormed, partOfRelation, resolveRelation

structure Ontology : Type
  • concepts : List Concept
  • relations : List Relation
Show details

Outer dependencies: (none)

Inner dependencies: Concept, Relation

Lean core dependencies: Eq, List, Nat

Used by: Ontology.decidableWellFormed, Ontology.empty, Ontology.readFile, Ontology.wellFormed

def Ontology.wellFormed (o : Ontology) : Prop
Show details 
| o.wellFormed = ∀ r ∈ o.relations, r.source ∈ o.concepts ∧ r.target ∈ o.concepts

Complexity: 63 (size of the value term)

Outer dependencies: Ontology

Inner dependencies: Concept, Relation

Lean core dependencies: And, List

Used by: Ontology.decidableWellFormed, Ontology.empty_wellFormed, Ontology.readFile

instance Ontology.decidableWellFormed (o : Ontology) : Decidable o.wellFormed
Show details 
| o.decidableWellFormed = Ontology.decidableWellFormed._aux_1 o

Complexity: 5 (size of the value term)

Outer dependencies: Ontology, Ontology.wellFormed

Inner dependencies: Concept, Relation

Lean core dependencies: And, Decidable, List

Used by: Ontology.readFile

def Ontology.empty : Ontology
Show details 
| Ontology.empty = { concepts := [], relations := [] }

Complexity: 9 (size of the value term)

Outer dependencies: Ontology

Inner dependencies: Concept, Relation

Used by: Ontology.empty_wellFormed

theorem Ontology.empty_wellFormed : Ontology.empty.wellFormed
Show details 
fun r hr =>
  List.Mem.casesOn (motive := fun a t =>
    Ontology.empty.relations = a →
      hr ≍ t → r.source ∈ Ontology.empty.concepts ∧ r.target ∈ Ontology.empty.concepts)
    hr (fun as h => False.elim (noConfusion_of_Nat List.ctorIdx h))
    (fun b {as} a h => False.elim (noConfusion_of_Nat List.ctorIdx h))
    (Eq.refl Ontology.empty.relations) (HEq.refl hr)

Complexity: 443 (size of the value term)

Dependencies: Ontology.empty, Ontology.wellFormed

Proof dependencies: Concept, Relation

Lean core dependencies: And, Eq, False.elim, HEq, List, List.Mem, noConfusion_of_Nat

Used by: (none)

def componentConcept : Concept
Show details 
| componentConcept = { name := "component" }

Complexity: 3 (size of the value term)

Outer dependencies: Concept

Used by: partOfRelation

def systemConcept : Concept
Show details 
| systemConcept = { name := "system" }

Complexity: 3 (size of the value term)

Outer dependencies: Concept

Used by: partOfRelation

def partOfRelation : Relation
Show details 
| partOfRelation = { label := "part-of", source := componentConcept, target := systemConcept }

Complexity: 7 (size of the value term)

Outer dependencies: Relation

Inner dependencies: componentConcept, systemConcept

Used by: (none)

structure RawRelation : Type
  • label : String
  • source : String
  • target : String
Show details

Outer dependencies: (none)

Lean core dependencies: Eq, Nat, String

Used by: Ontology.readFile, instDecodeTomlRawRelation, resolveRelation

instance instDecodeTomlConcept : Lake.DecodeToml Concept
Show details 
| instDecodeTomlConcept =
  {
    decode := fun v => do
      let t ← v.decodeTable
      let name ← t.decode `name
      pure { name := name } }

Complexity: 93 (size of the value term)

Outer dependencies: Concept

Lean core dependencies: Array, Lean.Name.mkStr1, String, Unit

Used by: Ontology.readFile

instance instDecodeTomlRawRelation : Lake.DecodeToml RawRelation
Show details 
| instDecodeTomlRawRelation =
  {
    decode := fun v => do
      let t ← v.decodeTable
      let label ← t.decode `label
      let source ← t.decode `source
      let target ← t.decode `target
      pure { label := label, source := source, target := target } }

Complexity: 169 (size of the value term)

Outer dependencies: RawRelation

Lean core dependencies: Array, Lean.Name.mkStr1, String, Unit

Used by: Ontology.readFile

def resolveRelation (concepts : List Concept) (r : RawRelation) : Except String Relation
Show details 
| resolveRelation concepts r =
  match List.find? (fun x => x.name == r.source) concepts,
    List.find? (fun x => x.name == r.target) concepts with
  | some s, some t => Except.ok { label := r.label, source := s, target := t }
  | none, x =>
    Except.error
      (toString "relation '" ++ toString r.label ++ toString "': no witness for concept '" ++
          toString r.source ++
        toString "'")
  | x, none =>
    Except.error
      (toString "relation '" ++ toString r.label ++ toString "': no witness for concept '" ++
          toString r.target ++
        toString "'")

Complexity: 313 (size of the value term)

Outer dependencies: Concept, RawRelation, Relation

Lean core dependencies: Except, List, List.find?, Option, String

Used by: Ontology.readFile

def Ontology.readFile (path : System.FilePath) : IO Ontology
Show details 
| Ontology.readFile path = do
  let input ← IO.FS.readFile path
  have ictx : Parser.InputContext :=
    Parser.mkInputContext input path.toString true input.rawEndPos ⋯
  let __do_lift ← liftM (Lake.Toml.loadToml ictx).toBaseIO
  match __do_lift with
    | Except.error a => throw (IO.userError (toString "failed to parse TOML: " ++ toString path))
    | Except.ok table =>
      match
        EStateM.run
          (Lake.Toml.mergeErrors (table.decode `concepts) (table.decode `relations) Prod.mk)
          #[] with
      | EStateM.Result.error a a_1 =>
        throw (IO.userError (toString "failed to decode ontology: " ++ toString path))
      | EStateM.Result.ok (concepts, rawRelations) a =>
        have concepts := concepts.toList;
        match List.mapM (resolveRelation concepts) rawRelations.toList with
        | Except.error msg =>
          throw
            (IO.userError
              (toString "failed to resolve ontology in " ++ toString path ++ toString ": " ++
                toString msg))
        | Except.ok relations =>
          have o := { concepts := concepts, relations := relations };
          if h : o.wellFormed then pure o
          else
            throw
              (IO.userError
                (toString "ontology in " ++ toString path ++ toString " is not well-formed"))

Complexity: 636 (size of the value term)

Outer dependencies: Ontology

Inner dependencies: Concept, Ontology.decidableWellFormed, Ontology.wellFormed, RawRelation, Relation, instDecodeTomlConcept, instDecodeTomlRawRelation, resolveRelation

Lean core dependencies: Array, BaseIO, EIO, EIO.toBaseIO, EStateM.Result, EStateM.run, Except, IO, IO.Error, IO.FS.readFile, IO.userError, Lean.Name.mkStr1, List, List.mapM, List.toArray, Not, Prod, String, String.Pos.Raw, String.rawEndPos, System.FilePath, Unit, dite, liftM, of_eq_true, optParam

Used by: (none)

def concept : ParserDescr
Show details 
| concept =
  ParserDescr.node `concept 1022
    (ParserDescr.binary `andthen
      (ParserDescr.binary `andthen (ParserDescr.nonReservedSymbol "concept" false)
        (ParserDescr.const `ppSpace))
      (ParserDescr.const `str))

Complexity: 45 (size of the value term)

Outer dependencies: (none)

Lean core dependencies: Lean.Name.mkStr1, Lean.ParserDescr, Nat

Used by: (none)

def allConceptAnnotations (env : Environment) : Array (Name × String)
Show details 
| allConceptAnnotations env =
  (have acc := conceptExt.getState env;
    do
    let __s ←
      forIn [:env.allImportedModuleNames.size] acc fun i __s =>
          have acc := __s;
          have acc := acc ++ conceptExt.getModuleEntries env i;
          pure (ForInStep.yield acc)
    have acc : Array (Name × String) := __s
    pure acc).run

Complexity: 383 (size of the value term)

Outer dependencies: (none)

Lean core dependencies: Array, Array.size, ForInStep, Id, Id.run, Lean.Name, Membership, Nat, Nat.zero_lt_one, Prod, Std.Legacy.Range, String, inferInstance

Used by: getConceptsOf

def getConceptsOf (env : Environment) (declName : Name) : List String
Show details 
| getConceptsOf env declName =
  List.filterMap
    (fun x =>
      match x with
      | (n, c) => if (n == declName) = true then some c else none)
    (allConceptAnnotations env).toList

Complexity: 95 (size of the value term)

Outer dependencies: (none)

Inner dependencies: allConceptAnnotations

Lean core dependencies: Bool, Eq, Lean.Name, List, List.filterMap, Option, Prod, String, ite

Used by: (none)

def lemmaTag : ParserDescr
Show details 
| lemmaTag = ParserDescr.node `lemmaTag 1024 (ParserDescr.nonReservedSymbol "lemma" false)

Complexity: 21 (size of the value term)

Outer dependencies: (none)

Lean core dependencies: Lean.Name.mkStr1, Lean.ParserDescr, Nat

Used by: (none)

def allLemmaTags (env : Environment) : Array Name
Show details 
| allLemmaTags env =
  (have acc := lemmaExt.getState env;
    do
    let __s ←
      forIn [:env.allImportedModuleNames.size] acc fun i __s =>
          have acc := __s;
          have acc := acc ++ lemmaExt.getModuleEntries env i;
          pure (ForInStep.yield acc)
    have acc : Array Name := __s
    pure acc).run

Complexity: 259 (size of the value term)

Outer dependencies: (none)

Lean core dependencies: Array, Array.size, ForInStep, Id, Id.run, Lean.Name, Membership, Nat, Nat.zero_lt_one, Std.Legacy.Range, inferInstance

Used by: isLemma

def isLemma (env : Environment) (n : Name) : Bool
Show details 
| isLemma env n = (allLemmaTags env).contains n

Complexity: 15 (size of the value term)

Outer dependencies: (none)

Inner dependencies: allLemmaTags

Lean core dependencies: Array.contains, Bool, Lean.Name

Used by: (none)

def ignoreTag : ParserDescr
Show details 
| ignoreTag = ParserDescr.node `ignoreTag 1024 (ParserDescr.nonReservedSymbol "ignore" false)

Complexity: 21 (size of the value term)

Outer dependencies: (none)

Lean core dependencies: Lean.Name.mkStr1, Lean.ParserDescr, Nat

Used by: (none)

def allIgnoreTags (env : Environment) : Array Name
Show details 
| allIgnoreTags env =
  (have acc := ignoreExt.getState env;
    do
    let __s ←
      forIn [:env.allImportedModuleNames.size] acc fun i __s =>
          have acc := __s;
          have acc := acc ++ ignoreExt.getModuleEntries env i;
          pure (ForInStep.yield acc)
    have acc : Array Name := __s
    pure acc).run

Complexity: 259 (size of the value term)

Outer dependencies: (none)

Lean core dependencies: Array, Array.size, ForInStep, Id, Id.run, Lean.Name, Membership, Nat, Nat.zero_lt_one, Std.Legacy.Range, inferInstance

Used by: isIgnored

def isIgnored (env : Environment) (n : Name) : Bool
Show details 
| isIgnored env n = (allIgnoreTags env).contains n

Complexity: 15 (size of the value term)

Outer dependencies: (none)

Inner dependencies: allIgnoreTags

Lean core dependencies: Array.contains, Bool, Lean.Name

Used by: (none)

def forwardReferencingTag : ParserDescr
Show details 
| forwardReferencingTag =
  ParserDescr.node `forwardReferencingTag 1024
    (ParserDescr.nonReservedSymbol "forward_referencing" false)

Complexity: 21 (size of the value term)

Outer dependencies: (none)

Lean core dependencies: Lean.Name.mkStr1, Lean.ParserDescr, Nat

Used by: (none)

def allForwardReferencingTags (env : Environment) : Array Name
Show details 
| allForwardReferencingTags env =
  (have acc := forwardReferencingExt.getState env;
    do
    let __s ←
      forIn [:env.allImportedModuleNames.size] acc fun i __s =>
          have acc := __s;
          have acc := acc ++ forwardReferencingExt.getModuleEntries env i;
          pure (ForInStep.yield acc)
    have acc : Array Name := __s
    pure acc).run

Complexity: 259 (size of the value term)

Outer dependencies: (none)

Lean core dependencies: Array, Array.size, ForInStep, Id, Id.run, Lean.Name, Membership, Nat, Nat.zero_lt_one, Std.Legacy.Range, inferInstance

Used by: (none)

def exampleTag : ParserDescr
Show details 
| exampleTag = ParserDescr.node `exampleTag 1024 (ParserDescr.nonReservedSymbol "example" false)

Complexity: 21 (size of the value term)

Outer dependencies: (none)

Lean core dependencies: Lean.Name.mkStr1, Lean.ParserDescr, Nat

Used by: (none)

def allExampleTags (env : Environment) : Array Name
Show details 
| allExampleTags env =
  (have acc := exampleExt.getState env;
    do
    let __s ←
      forIn [:env.allImportedModuleNames.size] acc fun i __s =>
          have acc := __s;
          have acc := acc ++ exampleExt.getModuleEntries env i;
          pure (ForInStep.yield acc)
    have acc : Array Name := __s
    pure acc).run

Complexity: 259 (size of the value term)

Outer dependencies: (none)

Lean core dependencies: Array, Array.size, ForInStep, Id, Id.run, Lean.Name, Membership, Nat, Nat.zero_lt_one, Std.Legacy.Range, inferInstance

Used by: isExample

def isExample (env : Environment) (n : Name) : Bool
Show details 
| isExample env n = (allExampleTags env).contains n

Complexity: 15 (size of the value term)

Outer dependencies: (none)

Inner dependencies: allExampleTags

Lean core dependencies: Array.contains, Bool, Lean.Name

Used by: (none)

inductive Difficulty : Type
  • easy : Difficulty
  • moderate : Difficulty
  • hard : Difficulty
  • optional : Difficulty
Show details

Outer dependencies: (none)

Lean core dependencies: Eq, Nat, Nat.ble, PULift, cond, noConfusionEnum, noConfusionTypeEnum

Used by: Difficulty.ofString?

def Difficulty.ofString? : String → Option Difficulty
Show details 
| Difficulty.ofString? "easy" = some Difficulty.easy
| Difficulty.ofString? "moderate" = some Difficulty.moderate
| Difficulty.ofString? "hard" = some Difficulty.hard
| Difficulty.ofString? "optional" = some Difficulty.optional
| Difficulty.ofString? x✝ = none

Complexity: 49 (size of the value term)

Outer dependencies: Difficulty

Lean core dependencies: Eq, Eq.ndrec_symm, Not, Option, String, Unit, Unit.unit, dite

Used by: (none)

def difficultyTag : ParserDescr
Show details 
| difficultyTag =
  ParserDescr.node `difficultyTag 1022
    (ParserDescr.binary `andthen
      (ParserDescr.binary `andthen (ParserDescr.nonReservedSymbol "difficulty" false)
        (ParserDescr.const `ppSpace))
      (ParserDescr.const `str))

Complexity: 45 (size of the value term)

Outer dependencies: (none)

Lean core dependencies: Lean.Name.mkStr1, Lean.ParserDescr, Nat

Used by: (none)

def allDifficultyAnnotations (env : Environment) : Array (Name × String)
Show details 
| allDifficultyAnnotations env =
  (have acc := difficultyExt.getState env;
    do
    let __s ←
      forIn [:env.allImportedModuleNames.size] acc fun i __s =>
          have acc := __s;
          have acc := acc ++ difficultyExt.getModuleEntries env i;
          pure (ForInStep.yield acc)
    have acc : Array (Name × String) := __s
    pure acc).run

Complexity: 383 (size of the value term)

Outer dependencies: (none)

Lean core dependencies: Array, Array.size, ForInStep, Id, Id.run, Lean.Name, Membership, Nat, Nat.zero_lt_one, Prod, Std.Legacy.Range, String, inferInstance

Used by: (none)

inductive Quality : Type
  • generated : Quality
  • preliminary : Quality
  • settled : Quality
  • special : Quality
Show details

Outer dependencies: (none)

Lean core dependencies: Eq, Nat, Nat.ble, PULift, cond, noConfusionEnum, noConfusionTypeEnum

Used by: Quality.ofString?, qualityOf

def Quality.ofString? : String → Option Quality
Show details 
| Quality.ofString? "generated" = some Quality.generated
| Quality.ofString? "preliminary" = some Quality.preliminary
| Quality.ofString? "settled" = some Quality.settled
| Quality.ofString? "special" = some Quality.special
| Quality.ofString? x✝ = none

Complexity: 49 (size of the value term)

Outer dependencies: Quality

Lean core dependencies: Eq, Eq.ndrec_symm, Not, Option, String, Unit, Unit.unit, dite

Used by: qualityOf

def qualityTag : ParserDescr
Show details 
| qualityTag =
  ParserDescr.node `qualityTag 1022
    (ParserDescr.binary `andthen
      (ParserDescr.binary `andthen (ParserDescr.nonReservedSymbol "quality" false)
        (ParserDescr.const `ppSpace))
      (ParserDescr.const `str))

Complexity: 45 (size of the value term)

Outer dependencies: (none)

Lean core dependencies: Lean.Name.mkStr1, Lean.ParserDescr, Nat

Used by: (none)

def allQualityAnnotations (env : Environment) : Array (Name × String)
Show details 
| allQualityAnnotations env =
  (have acc := qualityExt.getState env;
    do
    let __s ←
      forIn [:env.allImportedModuleNames.size] acc fun i __s =>
          have acc := __s;
          have acc := acc ++ qualityExt.getModuleEntries env i;
          pure (ForInStep.yield acc)
    have acc : Array (Name × String) := __s
    pure acc).run

Complexity: 383 (size of the value term)

Outer dependencies: (none)

Lean core dependencies: Array, Array.size, ForInStep, Id, Id.run, Lean.Name, Membership, Nat, Nat.zero_lt_one, Prod, Std.Legacy.Range, String, inferInstance

Used by: qualityOf

def qualityOf (env : Environment) (n : Name) : Quality
Show details 
| qualityOf env n =
  match List.filter (fun x => x.1 == n) (allQualityAnnotations env).toList with
  | [] => Quality.generated
  | l => (Quality.ofString? l.getLast!.2).getD Quality.generated

Complexity: 103 (size of the value term)

Outer dependencies: Quality

Inner dependencies: Quality.ofString?, allQualityAnnotations

Lean core dependencies: Bool, Lean.Name, List, List.filter, List.getLast!, Nat, Nat.hasNotBit, Nat.land, Nat.ne_of_beq_eq_false, Nat.shiftRight, Option.getD, Prod, String, Unit, Unit.unit

Used by: (none)

def moduleOf (env : Environment) (n : Name) : Option Name
Show details 
| moduleOf env n = do
  let idx ← env.getModuleIdxFor? n
  env.allImportedModuleNames[idx.toNat]?

Complexity: 67 (size of the value term)

Outer dependencies: (none)

Lean core dependencies: Array, Array.size, Lean.Name, Nat, Option

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitiontheoremdeclared elsewheredependencyproof dependency
legend