Skip to content
Snippets Groups Projects
Commit 56a17657 authored by ComFreek's avatar ComFreek
Browse files

add examples for Richard with JSON representations

parent f2e784ea
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
content/http..mathhub.info/FrameIT/frameworld/examples/$Examples.omdoc.xz 0 → 100644
+ 0
− 0
View file @ 56a17657
File added
errors/mmt-omdoc/examples/misc.mmt.err 0 → 100644
+ 159
− 0
View file @ 56a17657
<errors>
<error
target="structure-parser" sref="http://mathhub.info/FrameIT/frameworld/examples/misc.mmt#302.9.2:336.9.36" type="info.kwarc.mmt.api.SourceError" shortMsg="error while adding successfully parsed element http://mathhub.info/FrameIT/frameworld/examples?Examples?line_AB: variable point not declared in context http://mathhub.info/FrameIT/frameworld?ScrollMeta, http://mathhub.info/FrameIT/frameworld/examples?Examples" level="2">
source error (structure-parser) at http://mathhub.info/FrameIT/frameworld/examples/misc.mmt#302.9.2:336.9.36
<stacktrace>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.makeError(StructureParser.scala:202)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:134)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:497)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:688)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:477)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:768)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:768)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:416)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:93)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:93)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:83)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:94)</element>
<element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:45)</element>
<element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:159)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:564)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
<element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
</stacktrace>
<error type="info.kwarc.mmt.api.LookupError" shortMsg="variable point not declared in context http://mathhub.info/FrameIT/frameworld?ScrollMeta, http://mathhub.info/FrameIT/frameworld/examples?Examples" level="2">
<stacktrace>
<element>info.kwarc.mmt.api.objects.Context.$anonfun$apply$1(Context.scala:183)</element>
<element>scala.Option.getOrElse(Option.scala:138)</element>
<element>info.kwarc.mmt.api.objects.Context.apply(Context.scala:183)</element>
<element>info.kwarc.mmt.api.checking.Solver.getVar(Solver.scala:485)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms.$anonfun$inferType$3(SolverAlgorithms.scala:555)</element>
<element>info.kwarc.mmt.api.checking.History.indented(Constraints.scala:86)</element>
<element>info.kwarc.mmt.api.checking.Solver.$anonfun$logAndHistoryGroup$1(Solver.scala:345)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.checking.Solver.logGroup(Solver.scala:54)</element>
<element>info.kwarc.mmt.api.checking.Solver.logAndHistoryGroup(Solver.scala:344)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms.inferType(SolverAlgorithms.scala:545)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms.inferType$(SolverAlgorithms.scala:536)</element>
<element>info.kwarc.mmt.api.checking.Solver.inferType(Solver.scala:54)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms.coerceToType(SolverAlgorithms.scala:456)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms.checkSubtyping(SolverAlgorithms.scala:475)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms.$anonfun$check$5(SolverAlgorithms.scala:71)</element>
<element>scala.runtime.java8.JFunction0$mcZ$sp.apply(JFunction0$mcZ$sp.java:23)</element>
<element>info.kwarc.mmt.api.checking.History.indented(Constraints.scala:86)</element>
<element>info.kwarc.mmt.api.checking.Solver.$anonfun$logAndHistoryGroup$1(Solver.scala:345)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.checking.Solver.logGroup(Solver.scala:54)</element>
<element>info.kwarc.mmt.api.checking.Solver.logAndHistoryGroup(Solver.scala:344)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms.$anonfun$check$3(SolverAlgorithms.scala:68)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms$JudgementStore$.getOrElseUpdate(SolverAlgorithms.scala:94)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms.check(SolverAlgorithms.scala:65)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms.check$(SolverAlgorithms.scala:57)</element>
<element>info.kwarc.mmt.api.checking.Solver.check(Solver.scala:54)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms.checkTyping(SolverAlgorithms.scala:236)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms.$anonfun$check$5(SolverAlgorithms.scala:70)</element>
<element>scala.runtime.java8.JFunction0$mcZ$sp.apply(JFunction0$mcZ$sp.java:23)</element>
<element>info.kwarc.mmt.api.checking.History.indented(Constraints.scala:86)</element>
<element>info.kwarc.mmt.api.checking.Solver.$anonfun$logAndHistoryGroup$1(Solver.scala:345)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.checking.Solver.logGroup(Solver.scala:54)</element>
<element>info.kwarc.mmt.api.checking.Solver.logAndHistoryGroup(Solver.scala:344)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms.$anonfun$check$3(SolverAlgorithms.scala:68)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms$JudgementStore$.getOrElseUpdate(SolverAlgorithms.scala:94)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms.check(SolverAlgorithms.scala:65)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms.check$(SolverAlgorithms.scala:57)</element>
<element>info.kwarc.mmt.api.checking.Solver.check(Solver.scala:54)</element>
<element>info.kwarc.mmt.lf.StandardArgumentChecker$.$anonfun$apply$4(Rules.scala:118)</element>
<element>scala.runtime.java8.JFunction0$mcZ$sp.apply(JFunction0$mcZ$sp.java:23)</element>
<element>info.kwarc.mmt.api.checking.History.indented(Constraints.scala:86)</element>
<element>info.kwarc.mmt.lf.StandardArgumentChecker$.apply(Rules.scala:118)</element>
<element>info.kwarc.mmt.lf.GenericApplyTerm.$anonfun$apply$10(Rules.scala:189)</element>
<element>info.kwarc.mmt.lf.GenericApplyTerm.$anonfun$apply$10$adapted(Rules.scala:187)</element>
<element>scala.collection.LinearSeqOptimized.forall(LinearSeqOptimized.scala:85)</element>
<element>scala.collection.LinearSeqOptimized.forall$(LinearSeqOptimized.scala:82)</element>
<element>scala.collection.immutable.List.forall(List.scala:89)</element>
<element>info.kwarc.mmt.lf.GenericApplyTerm.apply(Rules.scala:187)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms.$anonfun$checkTyping$14(SolverAlgorithms.scala:260)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms.$anonfun$tryAllRules$2(SolverAlgorithms.scala:1183)</element>
<element>info.kwarc.mmt.api.utils.While$.apply(While.scala:14)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms.tryAllRules(SolverAlgorithms.scala:1179)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms.$anonfun$checkTyping$13(SolverAlgorithms.scala:258)</element>
<element>scala.runtime.java8.JFunction0$mcZ$sp.apply(JFunction0$mcZ$sp.java:23)</element>
<element>scala.Option.getOrElse(Option.scala:138)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms.$anonfun$checkTyping$7(SolverAlgorithms.scala:257)</element>
<element>scala.runtime.java8.JFunction0$mcZ$sp.apply(JFunction0$mcZ$sp.java:23)</element>
<element>info.kwarc.mmt.api.checking.History.indented(Constraints.scala:86)</element>
<element>info.kwarc.mmt.api.checking.Solver.$anonfun$logAndHistoryGroup$1(Solver.scala:345)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.checking.Solver.logGroup(Solver.scala:54)</element>
<element>info.kwarc.mmt.api.checking.Solver.logAndHistoryGroup(Solver.scala:344)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms.checkTyping(SolverAlgorithms.scala:243)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms.$anonfun$check$5(SolverAlgorithms.scala:70)</element>
<element>scala.runtime.java8.JFunction0$mcZ$sp.apply(JFunction0$mcZ$sp.java:23)</element>
<element>info.kwarc.mmt.api.checking.History.indented(Constraints.scala:86)</element>
<element>info.kwarc.mmt.api.checking.Solver.$anonfun$logAndHistoryGroup$1(Solver.scala:345)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.checking.Solver.logGroup(Solver.scala:54)</element>
<element>info.kwarc.mmt.api.checking.Solver.logAndHistoryGroup(Solver.scala:344)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms.$anonfun$check$3(SolverAlgorithms.scala:68)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms$JudgementStore$.getOrElseUpdate(SolverAlgorithms.scala:94)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms.check(SolverAlgorithms.scala:65)</element>
<element>info.kwarc.mmt.api.checking.SolverAlgorithms.check$(SolverAlgorithms.scala:57)</element>
<element>info.kwarc.mmt.api.checking.Solver.check(Solver.scala:54)</element>
<element>info.kwarc.mmt.api.checking.Solver.info$kwarc$mmt$api$checking$Solver$$activateRepeatedly(Solver.scala:820)</element>
<element>info.kwarc.mmt.api.checking.Solver.apply(Solver.scala:734)</element>
<element>info.kwarc.mmt.api.checking.Solver.applyMain(Solver.scala:718)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$7(RuleBasedChecker.scala:56)</element>
<element>scala.runtime.java8.JFunction0$mcZ$sp.apply(JFunction0$mcZ$sp.java:23)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:56)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$17(MMTStructureChecker.scala:313)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$17$adapted(MMTStructureChecker.scala:289)</element>
<element>scala.Option.foreach(Option.scala:274)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:289)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:73)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:88)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:131)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:497)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:688)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:477)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:768)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:768)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:416)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:93)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:93)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:83)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:94)</element>
<element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:45)</element>
<element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:159)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:564)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
<element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
</stacktrace>
</error>
</error>
</errors>
narration/examples/misc.omdoc 0 → 100644
+ 2
− 0
View file @ 56a17657
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/FrameIT/frameworld/examples/misc.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/examples/misc.mmt#0.0.0:1585.47.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld/examples"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?ScrollMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld/examples?Examples]" target="http://mathhub.info/FrameIT/frameworld/examples?Examples"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/examples/misc.mmt#122.4.0:136.4.14"/></metadata></mref></omdoc>
\ No newline at end of file
relational/examples/misc.rel 0 → 100644
+ 2
− 0
View file @ 56a17657
document http://mathhub.info/FrameIT/frameworld/examples/misc.omdoc
Declares http://mathhub.info/FrameIT/frameworld/examples/misc.omdoc http://mathhub.info/FrameIT/frameworld/examples?Examples
relational/http..mathhub.info/FrameIT/frameworld/examples/$Examples.rel 0 → 100644
+ 20
− 0
View file @ 56a17657
dataconstructor http://mathhub.info/FrameIT/frameworld/examples?Examples?A
dataconstructor http://mathhub.info/FrameIT/frameworld/examples?Examples?B
dataconstructor http://mathhub.info/FrameIT/frameworld/examples?Examples?line_AB
theory http://mathhub.info/FrameIT/frameworld/examples?Examples
HasMeta http://mathhub.info/FrameIT/frameworld/examples?Examples http://mathhub.info/FrameIT/frameworld?ScrollMeta
Declares http://mathhub.info/FrameIT/frameworld/examples?Examples http://mathhub.info/FrameIT/frameworld/examples?Examples?A
constant http://mathhub.info/FrameIT/frameworld/examples?Examples?A
DependsOn http://mathhub.info/FrameIT/frameworld/examples?Examples?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
DependsOn http://mathhub.info/FrameIT/frameworld/examples?Examples?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
DependsOn http://mathhub.info/FrameIT/frameworld/examples?Examples?A?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/FrameIT/frameworld/examples?Examples?A?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
Declares http://mathhub.info/FrameIT/frameworld/examples?Examples http://mathhub.info/FrameIT/frameworld/examples?Examples?B
constant http://mathhub.info/FrameIT/frameworld/examples?Examples?B
DependsOn http://mathhub.info/FrameIT/frameworld/examples?Examples?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
DependsOn http://mathhub.info/FrameIT/frameworld/examples?Examples?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
DependsOn http://mathhub.info/FrameIT/frameworld/examples?Examples?B?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/FrameIT/frameworld/examples?Examples?B?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
Declares http://mathhub.info/FrameIT/frameworld/examples?Examples http://mathhub.info/FrameIT/frameworld/examples?Examples?line_AB
constant http://mathhub.info/FrameIT/frameworld/examples?Examples?line_AB
DependsOn http://mathhub.info/FrameIT/frameworld/examples?Examples?line_AB?type http://mathhub.info/MitM/core/geometry?Geometry/Common?line_type?type
source/examples/misc.mmt 0 → 100644
+ 48
− 0
View file @ 56a17657
namespace http://mathhub.info/FrameIT/frameworld/examples ❚
fixmeta http://mathhub.info/FrameIT/frameworld?ScrollMeta ❚
theory Examples =
A: point ❘ = ⟨1.0, 2.0, 3.0⟩❙
B: point ❘ = ⟨4.0, 5.0, 6.0⟩❙
// this doesn't typecheck due to an MMT bug -- iirc not even Dennis knows what is going on ❙
line_AB: line_type ❘ = lineOf A B ❙
// JSON representation for A: {
"tp": {
"kind": "OMS",
"uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point"
},
"df": {
"kind": "OMA",
"applicant": {
"kind": "OMS",
"uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Tuple"
},
"arguments": [
{"kind": "OMF", "float": 1.0},
{"kind": "OMF", "float": 2.0},
{"kind": "OMF", "float": 3.0}
]
}
} ❙
// JSON representation of line_AB: {
"tp": {
"kind": "OMS",
"uri": "http://mathhub.info/MitM/core/geometry?Geometry/Common?line_type",
},
"df": {
"kind": "OMA",
"applicant": {
"kind": "OMS",
"uri": "http://mathhub.info/MitM/core/geometry?Geometry/Common?lineOf"
},
"arguments": [
{"kind": "OMS", "uri": "http://mathhub.info/FrameIT/frameworld/examples?Examples?A"},
{"kind": "OMS", "uri": "http://mathhub.info/FrameIT/frameworld/examples?Examples?B"},
]
}
} ❙
❚
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment