Ontology

definition theorem
legend
Concept : Type
Show details 
| Concept.mk : String → Concept

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

Relation : Type
Show details 
| Relation.mk : String → Concept → Concept → Relation

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

Ontology : Type
Show details 
| Ontology.mk : List Concept → List Relation → Ontology

Outer dependencies: (none)

Inner dependencies: Concept, Relation

Lean core dependencies: Eq, List, Nat

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

Ontology.wellFormed (o : Ontology) : Prop
Show details 
fun o => ∀ 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

Ontology.decidableWellFormed (o : Ontology) : Decidable o.wellFormed
Show details 
fun o => 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

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

Complexity: 9 (size of the value term)

Outer dependencies: Ontology

Inner dependencies: Concept, Relation

Used by: Ontology.empty_wellFormed

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)

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

Complexity: 3 (size of the value term)

Outer dependencies: Concept

Used by: partOfRelation

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

Complexity: 3 (size of the value term)

Outer dependencies: Concept

Used by: partOfRelation

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

Complexity: 7 (size of the value term)

Outer dependencies: Relation

Inner dependencies: componentConcept, systemConcept

Used by: (none)

RawRelation : Type
Show details 
| RawRelation.mk : String → String → String → RawRelation

Outer dependencies: (none)

Lean core dependencies: Eq, Nat, String

Used by: Ontology.readFile, instDecodeTomlRawRelation, resolveRelation

instDecodeTomlConcept : Lake.DecodeToml Concept
Show details 
{
  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

instDecodeTomlRawRelation : Lake.DecodeToml RawRelation
Show details 
{
  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

resolveRelation (concepts : List Concept) (r : RawRelation) : Except String Relation
Show details 
fun 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

Ontology.readFile (path : System.FilePath) : IO Ontology
Show details 
fun 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)

concept : ParserDescr
Show details 
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)

allConceptAnnotations (env : Environment) : Array (Name × String)
Show details 
fun 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

getConceptsOf (env : Environment) (declName : Name) : List String
Show details 
fun 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)

lemmaTag : ParserDescr
Show details 
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)

allLemmaTags (env : Environment) : Array Name
Show details 
fun 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

isLemma (env : Environment) (n : Name) : Bool
Show details 
fun 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)

ignoreTag : ParserDescr
Show details 
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)

allIgnoreTags (env : Environment) : Array Name
Show details 
fun 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

isIgnored (env : Environment) (n : Name) : Bool
Show details 
fun 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)

exampleTag : ParserDescr
Show details 
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)

allExampleTags (env : Environment) : Array Name
Show details 
fun 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

isExample (env : Environment) (n : Name) : Bool
Show details 
fun 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)

Difficulty : Type
Show details 
| Difficulty.easy : Difficulty
| Difficulty.moderate : Difficulty
| Difficulty.hard : Difficulty
| Difficulty.optional : Difficulty

Outer dependencies: (none)

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

Used by: Difficulty.ofString?

Difficulty.ofString? : String → Option Difficulty
Show details 
fun x =>
  match x with
  | "easy" => some Difficulty.easy
  | "moderate" => some Difficulty.moderate
  | "hard" => some Difficulty.hard
  | "optional" => some Difficulty.optional
  | 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)

difficultyTag : ParserDescr
Show details 
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)

allDifficultyAnnotations (env : Environment) : Array (Name × String)
Show details 
fun 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)

Quality : Type
Show details 
| Quality.generated : Quality
| Quality.preliminary : Quality
| Quality.settled : Quality

Outer dependencies: (none)

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

Used by: Quality.ofString?, qualityOf

Quality.ofString? : String → Option Quality
Show details 
fun x =>
  match x with
  | "generated" => some Quality.generated
  | "preliminary" => some Quality.preliminary
  | "settled" => some Quality.settled
  | x => none

Complexity: 41 (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

qualityTag : ParserDescr
Show details 
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)

allQualityAnnotations (env : Environment) : Array (Name × String)
Show details 
fun 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

qualityOf (env : Environment) (n : Name) : Quality
Show details 
fun 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)

moduleOf (env : Environment) (n : Name) : Option Name
Show details 
fun 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