Partially solve 1494 parse dol standard examples by gnn · Pull Request #1540 · spechub/Hets

gnn · 2015-11-03T21:40:38Z

The commits on this branch solve some of the parsing issues hets has with the DOL standard.
Two outstanding issues still remain:

issues with language serialization CURIES (so don't use those yet when you're testing)
select and reject can not handle SymbolLists

which is why the ticket can not be fully closed yet. The fixes for those issues will follow soon.
I'm creating this pull request before fully solving this issue because one can still use the parser on quite a few things, so it might be of some help already.

I tested for conflicts. There shouldn't be any.

gnn · 2015-11-04T18:11:57Z

Please don't merge the pull request yet. There a are a few more commits to come.

cmaeder · 2015-11-05T08:51:27Z

The policy is that (only) the creator of a PR merges after an OK by another reviewer

cmaeder · 2015-11-17T12:32:55Z

Common/AnnoParser.hs

I'm not sure if you really need endOfLine. I suspect that spaces also skips crlf. If you really need to check for the end of a line, then newline (from Text.ParserCombinators.Parsec.Char) should do, too.

Furthermore, comment lines should not be skipped but kept as part of the global annotations

Thanks for suggesting spaces. It worked and also enabled me to get rid of a line that I wanted to be gone from the get go. See 868229b below.
The reason I'm skipping the comments is that prefixAnno is already parsing a %prefix( ... )% annotation block and it needs to return a Prefix_anno. Since I wasn't able to figure out where to put the Unparsed_anno returned from commentLine I decided to skip those comments.

tillmo · 2016-03-11T13:29:47Z

The problem that select and reject can not handle SymbolLists is solved by branch filtering_with_symbol_lists

mcodescu · 2016-08-16T06:11:07Z

The change suggested by Christian (newline instead of endOfLine) is enough to make the compilation go through (and probably the tests green). I have tried the files from https://ontohub.org/dol-examples. There are some that can't go through because of missing translations or logics. For some we would need more of the static analysis for DOL that has been implemented in the meanwhile in HETS (probably via a rebase). The only problem I could find so far is for https://ontohub.org/dol-examples/sorting.dol

./hets ~/repos/dol-examples/sorting.dol 
### file name '/home/mcodescu/repos/dol-examples/sorting.dol' does not match library name 'Sorting'
Analyzing library Sorting
logic CASL
Analyzing spec Sorting?TotalOrder
Analyzing spec Sorting?Nat
Analyzing spec Sorting?List
Analyzing spec Sorting?Sorting
/home/mcodescu/repos/dol-examples/sorting.dol:48.1-48.4: *** Error:
attempt to hide the following symbols from the local environment:
{pred is_ordered : List, pred permutation : List * List}
hets: user error (Stopped due to errors)

Hiding from a named specification works though. This seems to be a parsing error.

gnn · 2016-08-18T17:03:23Z

I tested this and it seems that the problem is the second then of the spec Sorting. I think it creates a nested scope and the hide is_ordered, permutation only affects that scope, which doesn't work, as the symbols it attempts to hide also appear outside of that scope. Adding curly braces, see this diff, to explicitly scope the hide over the complete spec squelches the error. As a second option, removing the then has the same effect.
I don't know whether this behaviour of hide is intended though, so I'd like to ask whether I should change the example according to the linked gist or modify how hide behaves.

tillmo · 2017-05-07T17:13:50Z

@mcodescu, could you please have a look at the last two commits? Can we at least merge this pull request now, even if not all problems have been solved? (The pull request should of course not break existing functionality.)

mcodescu · 2017-08-17T12:41:13Z

I have parsed again the specifications in the repository mentioned above. Now the sorting specification is parsed correctly. It might be a good idea to run more tests before merging, though, but I don't have more inputs. Also, when compiling this branch on my machine, I had to take care of some ambiguous occurrences of methods, especially involving Data.Graph.Inductive.Graph, which is usually not imported using qualified. So if you do merge, please make sure that you don't introduce compilation errors.

tillmo · 2017-09-18T09:22:21Z

please rebase this branch on master (git rebase master, solve problems, then git push -f) in order to see if it works with the recently added tests.

ghost · 2017-09-18T09:22:23Z

Can one of the admins verify this patch?

It's no longer part of the standard, so there's no need to parse it anymore. 'library' is sufficient.

See the comments in the file for an explanation. In short: those parts make the parser choke, but not because of DOL related problems. So they have to go until those unrelated problems have been fixed.

It's not part of the DOL grammar and that's how it should be as it's also not part of the alignment API.

The DOL Standard doesn't allow those. Should be plain text keywords instead.

The standard says they should simply be doubles, not enclosed in parentheses.

If the `= ...` part is omitted it now defaults to the empty specification/oms/network.

It's a minuscule change but that way, it stays in line with how the rest of Hets is organized.

Don't know whether that's the correct way, but it's my stab at getting `OMS Extraction` to work. From what I gathered by reading the code this should be the right way to do it.

For some reason Hets leaves the angular brackets in there, when parsing IRIs at least in this small code sample. This prevents logic lookup from working properly. I opted for this short hack, as it I don't know whether other code relies on the brackets being there and removing them just before looking up the logic is the option that is least likely to break other code.

Since only one function is used in the importing module, I'd like to make that explicit.

Logic `OWL`, sublogic `NP-sROIQ-D|-|` should be correct but Hets errors out saying it doesn't know the logic `NP-sROIQ-D|-|`. For now simply using `OWL` seems to work, but it's a hack that should be corrected at some point.

Same (maybe) problem as in `lookupLogicName`. The IRI passed in as a parameter is still enclosed in angular brackets which is not expected by those functions. Filtering the brackets might only address the symptom of a bigger issue but it fixes the problem at hand and has the least effects on the remaining codebase.

This reverts commit 17aa52c and instead applies the fix closer to logic name lookup inside the function doing the lookup. That way both fixes for serialization and logic name lookup (which are identical) are grouped in one file.

As the comments says, theres a proper way to do it by using the information stored in the `LanguageQual` that is the result of parsing the `language` declaration. But this would entail expanding a possible prefix of the `LanguageQual` and I don't have time to implement this right now. I'll open an issue for this so that I can work on it later. For now, parsing the DOL examples is more important so I added this hack to get an intermediate working solution.

Now it also adds support for more logics/languages and various translations.

@cmaeder

Thanks @cmaeder for the suggestion. Using `spaces` has two benefits. It gets rid of a dependency issue resulting in a compilation error and it allows me to be consistent and only eat up whitespace at the end of lines.

gnn · 2017-09-21T00:55:55Z

I rebased the branch onto the current master. There are no compilation errors and I tried parsing all the DOL examples in the repository. There are still quite a few errors, most of which stem from missing logics or comorphisms, but some also have other reasons.

These are the categories of parsing errors, encountered when trying hets -p on the contents of the current dol-examples repository, missing .env files excluded and in order of decreasing frequency.
The errors are links to gists containing the error messages:

Missing comorphisms

Pretty simple. Hets doesn't seem to know the comorphisms uses in these examples, so the parser complains.

Unknown logics

Similar to the above. Hets doesn't seem to know one of the logics used in the examples. Note that the purl.net prefix is not the culprit in the first instance. Hets doesn't know the logic, even if this prefix is removed. Also beware: the second example is mentioned here only because this is the first type of error encountered. There probably is a missing comorphism in this example too.

Unknown keyword `distributed-ontology`

It seems, that hets either can't handle the keyword distributed-ontology yet, or it is not used correctly in the example.

Errors caused by unicode symbols which `hets` doesn't to be able to handle

I actually have a fix for this replacing the unicode symbols by their ASCII counterparts prepared locally. I just have to push the proposal to the examples repository.

Unknown cause

This is only one file and the error is caused by the select x where... construct. Even if I change the construct to select x . where... there are errors after that one too. So I don't really know how the select x where... construct should be used.

gnn · 2017-09-21T00:56:36Z

Closed by accident when commenting. Sorry.

ghost · 2017-09-21T00:56:38Z

Can one of the admins verify this patch?

tillmo · 2017-09-21T08:11:32Z

distributed-ontology should be replaced by library. Where does the select problem occur exactly?

tillmo · 2023-07-27T09:11:34Z

continued in #2154

cmaeder reviewed Nov 17, 2015
View reviewed changes

Stephan Günther and others added 20 commits September 21, 2017 00:44

Remove keyword 'distributed-ontology'

69e6eaf

It's no longer part of the standard, so there's no need to parse it anymore. 'library' is sufficient.

Remove 'CommonLogic' parts from DOL test

4fd2ecb

See the comments in the file for an explanation. In short: those parts make the parser choke, but not because of DOL related problems. So they have to go until those unrelated problems have been fixed.

Remove 'mapsto' alignment relation from DOL test

d1f1f84

It's not part of the DOL grammar and that's how it should be as it's also not part of the alignment API.

Fix LaTex'isms in DOL test

6fce3e8

The DOL Standard doesn't allow those. Should be plain text keywords instead.

Fix confidence declarations in DOL test

77cd3cf

The standard says they should simply be doubles, not enclosed in parentheses.

Add "AlignmentSemantics" test case

0ada092

Add oms keyword

0c63db2

Make = OMSOrNetwork optional in equivalence

7877253

If the `= ...` part is omitted it now defaults to the empty specification/oms/network.

Make "extract" and "remove" proper keywords

4eb2e3a

It's a minuscule change but that way, it stays in line with how the rest of Hets is organized.

Add extractS/removeS to terminatingKeywords

1e54913

Don't know whether that's the correct way, but it's my stab at getting `OMS Extraction` to work. From what I gathered by reading the code this should be the right way to do it.

Change casing of DOL in known prefixes

dee2df5

Use explicit import list for Logic.KnownIris

53e80ad

Since only one function is used in the importing module, I'd like to make that explicit.

Allow comment lines in prefix annotations

0624400

Shim for parsing SROIQ when prefixed

82ccbe9

Logic `OWL`, sublogic `NP-sROIQ-D|-|` should be correct but Hets errors out saying it doesn't know the logic `NP-sROIQ-D|-|`. For now simply using `OWL` seems to work, but it's a hack that should be corrected at some point.

Move the '<>' fix into lookupLogicName

92bedc9

This reverts commit 17aa52c and instead applies the fix closer to logic name lookup inside the function doing the lookup. That way both fixes for serialization and logic name lookup (which are identical) are grouped in one file.

Expand comment

fe4e851

Add languageS as a proper keyword

d779d24

gnn added 2 commits September 21, 2017 01:29

Expand language declaration hack

2381fb3

Now it also adds support for more logics/languages and various translations.

Use spaces instead of endOfLine

c49913b

Thanks @cmaeder for the suggestion. Using `spaces` has two benefits. It gets rid of a dependency issue resulting in a compilation error and it allows me to be consistent and only eat up whitespace at the end of lines.

gnn force-pushed the 1494-parse-DOL-standard-examples branch from ecc2936 to c49913b Compare September 21, 2017 00:33

gnn closed this Sep 21, 2017

gnn reopened this Sep 21, 2017

tillmo mentioned this pull request Jul 27, 2023

1494 parse dol standard examples #2154

Open

tillmo closed this Jul 27, 2023

Conversation

gnn commented Nov 3, 2015

Uh oh!

gnn commented Nov 4, 2015

Uh oh!

cmaeder commented Nov 5, 2015

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tillmo commented Mar 11, 2016

Uh oh!

mcodescu commented Aug 16, 2016

Uh oh!

gnn commented Aug 18, 2016

Uh oh!

tillmo commented May 7, 2017

Uh oh!

mcodescu commented Aug 17, 2017

Uh oh!

tillmo commented Sep 18, 2017

Uh oh!

ghost commented Sep 18, 2017

Uh oh!

gnn commented Sep 21, 2017

Uh oh!

gnn commented Sep 21, 2017

Uh oh!

ghost commented Sep 21, 2017

Uh oh!

tillmo commented Sep 21, 2017

Uh oh!

tillmo commented Jul 27, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants