From 391cb48a4569174f52b0074615128042c9a19952 Mon Sep 17 00:00:00 2001 From: pcarrott Date: Tue, 31 Oct 2023 22:08:49 +0000 Subject: [PATCH 01/28] Create coqpyt folder --- .github/workflows/test.yml | 2 +- README.md | 11 ++++++----- {coq => coqpyt}/__init__.py | 0 {coq/lsp => coqpyt/coq}/__init__.py | 0 {coq => coqpyt/coq}/base_file.py | 14 +++++++------- {coq => coqpyt/coq}/changes.py | 0 {coq => coqpyt/coq}/exceptions.py | 0 {tests => coqpyt/coq/lsp}/__init__.py | 0 {coq => coqpyt/coq}/lsp/client.py | 10 +++++----- {coq => coqpyt/coq}/lsp/structs.py | 2 +- {coq => coqpyt/coq}/proof_file.py | 14 +++++++------- {coq => coqpyt/coq}/structs.py | 4 ++-- coqpyt/lsp/__init__.py | 8 ++++++++ {lsp => coqpyt/lsp}/client.py | 4 ++-- {lsp => coqpyt/lsp}/endpoint.py | 2 +- {lsp => coqpyt/lsp}/json_rpc_endpoint.py | 2 +- {lsp => coqpyt/lsp}/structs.py | 0 coqpyt/tests/__init__.py | 0 {tests => coqpyt/tests}/resources/.gitignore | 0 {tests => coqpyt/tests}/resources/test_bug.v | 0 {tests => coqpyt/tests}/resources/test_bullets.v | 0 .../tests}/resources/test_change_empty.v | 0 {tests => coqpyt/tests}/resources/test_derive.v | 0 .../tests}/resources/test_exists_notation.v | 0 .../tests}/resources/test_get_notation.v | 0 {tests => coqpyt/tests}/resources/test_goal.v | 0 .../tests}/resources/test_imports/.gitignore | 0 .../tests}/resources/test_imports/Makefile | 0 .../tests}/resources/test_imports/Makefile.conf | 0 .../tests}/resources/test_imports/_CoqProject | 0 .../tests}/resources/test_imports/test_import.v | 0 .../tests}/resources/test_imports/test_import2.v | 0 {tests => coqpyt/tests}/resources/test_invalid_1.v | 0 {tests => coqpyt/tests}/resources/test_invalid_2.v | 0 .../tests}/resources/test_list_notation.v | 0 .../tests}/resources/test_module_type.v | 0 .../tests}/resources/test_nested_proofs.v | 0 .../tests}/resources/test_non_ending_proof.v | 0 .../tests}/resources/test_obligation.v | 0 .../tests}/resources/test_simple_file.v | 0 .../tests}/resources/test_theorem_tokens.v | 0 .../tests}/resources/test_type_class.v | 0 .../tests}/resources/test_unknown_notation.v | 0 {tests => coqpyt/tests}/resources/test_valid.v | 0 .../tests}/resources/test_where_notation.v | 0 {tests => coqpyt/tests}/test_coq_file.py | 6 +++--- {tests => coqpyt/tests}/test_coq_lsp_client.py | 6 +++--- {tests => coqpyt/tests}/test_json_rpc_endpoint.py | 2 +- {tests => coqpyt/tests}/test_proof_file.py | 10 +++++----- {tests => coqpyt/tests}/test_readme.py | 5 +++-- lsp/__init__.py | 8 -------- setup.py | 4 ++-- 52 files changed, 58 insertions(+), 56 deletions(-) rename {coq => coqpyt}/__init__.py (100%) rename {coq/lsp => coqpyt/coq}/__init__.py (100%) rename {coq => coqpyt/coq}/base_file.py (98%) rename {coq => coqpyt/coq}/changes.py (100%) rename {coq => coqpyt/coq}/exceptions.py (100%) rename {tests => coqpyt/coq/lsp}/__init__.py (100%) rename {coq => coqpyt/coq}/lsp/client.py (97%) rename {coq => coqpyt/coq}/lsp/structs.py (98%) rename {coq => coqpyt/coq}/proof_file.py (98%) rename {coq => coqpyt/coq}/structs.py (98%) create mode 100644 coqpyt/lsp/__init__.py rename {lsp => coqpyt/lsp}/client.py (99%) rename {lsp => coqpyt/lsp}/endpoint.py (99%) rename {lsp => coqpyt/lsp}/json_rpc_endpoint.py (99%) rename {lsp => coqpyt/lsp}/structs.py (100%) create mode 100644 coqpyt/tests/__init__.py rename {tests => coqpyt/tests}/resources/.gitignore (100%) rename {tests => coqpyt/tests}/resources/test_bug.v (100%) rename {tests => coqpyt/tests}/resources/test_bullets.v (100%) rename {tests => coqpyt/tests}/resources/test_change_empty.v (100%) rename {tests => coqpyt/tests}/resources/test_derive.v (100%) rename {tests => coqpyt/tests}/resources/test_exists_notation.v (100%) rename {tests => coqpyt/tests}/resources/test_get_notation.v (100%) rename {tests => coqpyt/tests}/resources/test_goal.v (100%) rename {tests => coqpyt/tests}/resources/test_imports/.gitignore (100%) rename {tests => coqpyt/tests}/resources/test_imports/Makefile (100%) rename {tests => coqpyt/tests}/resources/test_imports/Makefile.conf (100%) rename {tests => coqpyt/tests}/resources/test_imports/_CoqProject (100%) rename {tests => coqpyt/tests}/resources/test_imports/test_import.v (100%) rename {tests => coqpyt/tests}/resources/test_imports/test_import2.v (100%) rename {tests => coqpyt/tests}/resources/test_invalid_1.v (100%) rename {tests => coqpyt/tests}/resources/test_invalid_2.v (100%) rename {tests => coqpyt/tests}/resources/test_list_notation.v (100%) rename {tests => coqpyt/tests}/resources/test_module_type.v (100%) rename {tests => coqpyt/tests}/resources/test_nested_proofs.v (100%) rename {tests => coqpyt/tests}/resources/test_non_ending_proof.v (100%) rename {tests => coqpyt/tests}/resources/test_obligation.v (100%) rename {tests => coqpyt/tests}/resources/test_simple_file.v (100%) rename {tests => coqpyt/tests}/resources/test_theorem_tokens.v (100%) rename {tests => coqpyt/tests}/resources/test_type_class.v (100%) rename {tests => coqpyt/tests}/resources/test_unknown_notation.v (100%) rename {tests => coqpyt/tests}/resources/test_valid.v (100%) rename {tests => coqpyt/tests}/resources/test_where_notation.v (100%) rename {tests => coqpyt/tests}/test_coq_file.py (98%) rename {tests => coqpyt/tests}/test_coq_lsp_client.py (81%) rename {tests => coqpyt/tests}/test_json_rpc_endpoint.py (99%) rename {tests => coqpyt/tests}/test_proof_file.py (99%) rename {tests => coqpyt/tests}/test_readme.py (75%) delete mode 100644 lsp/__init__.py diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 943fd4e..a89d537 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -37,7 +37,7 @@ jobs: run: | opam install coq-lsp - - name: Install coq-lsp-pyclient + - name: Install coqpyt run: | pip install -e . diff --git a/README.md b/README.md index 9cf306d..71f1429 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,7 @@ Interact with Coq files and navigate through your proofs using our Python client for [coq-lsp](https://github.com/ejgallego/coq-lsp). -Execute Coq files, retrieve the generated context and edit proofs through addition and removal of steps. +Execute Coq files, retrieve the generated context and edit proofs through insertion and removal of steps. ## Installation @@ -19,9 +19,9 @@ python -m pip install -e . ## Usage ```python import os -from coq.base_file import CoqFile -from coq.proof_file import ProofFile -from coq.structs import TermType +from coqpyt.coq.base_file import CoqFile +from coqpyt.coq.proof_file import ProofFile +from coqpyt.coq.structs import TermType # Open Coq file with CoqFile(os.path.join(os.getcwd(), "examples/example.v")) as coq_file: @@ -83,8 +83,9 @@ with ProofFile(os.path.join(os.getcwd(), "examples/example.v")) as proof_file: ) ``` -### Run tests +## Tests +To run the tests for CoqPyt go to the folder ```coqpyt``` and run: ```bash pytest tests -s ``` diff --git a/coq/__init__.py b/coqpyt/__init__.py similarity index 100% rename from coq/__init__.py rename to coqpyt/__init__.py diff --git a/coq/lsp/__init__.py b/coqpyt/coq/__init__.py similarity index 100% rename from coq/lsp/__init__.py rename to coqpyt/coq/__init__.py diff --git a/coq/base_file.py b/coqpyt/coq/base_file.py similarity index 98% rename from coq/base_file.py rename to coqpyt/coq/base_file.py index 1d68879..722d2f9 100644 --- a/coq/base_file.py +++ b/coqpyt/coq/base_file.py @@ -3,18 +3,18 @@ import uuid import tempfile import subprocess -from lsp.structs import ( +from coqpyt.lsp.structs import ( TextDocumentItem, TextDocumentIdentifier, VersionedTextDocumentIdentifier, TextDocumentContentChangeEvent, ) -from lsp.structs import ResponseError, ErrorCodes, Diagnostic -from coq.lsp.structs import Position, GoalAnswer, RangedSpan -from coq.structs import Step, FileContext, Term, TermType, SegmentType -from coq.lsp.client import CoqLspClient -from coq.exceptions import * -from coq.changes import * +from coqpyt.lsp.structs import ResponseError, ErrorCodes, Diagnostic +from coqpyt.coq.lsp.structs import Position, GoalAnswer, RangedSpan +from coqpyt.coq.structs import Step, FileContext, Term, TermType, SegmentType +from coqpyt.coq.lsp.client import CoqLspClient +from coqpyt.coq.exceptions import * +from coqpyt.coq.changes import * from typing import List, Optional from packaging import version diff --git a/coq/changes.py b/coqpyt/coq/changes.py similarity index 100% rename from coq/changes.py rename to coqpyt/coq/changes.py diff --git a/coq/exceptions.py b/coqpyt/coq/exceptions.py similarity index 100% rename from coq/exceptions.py rename to coqpyt/coq/exceptions.py diff --git a/tests/__init__.py b/coqpyt/coq/lsp/__init__.py similarity index 100% rename from tests/__init__.py rename to coqpyt/coq/lsp/__init__.py diff --git a/coq/lsp/client.py b/coqpyt/coq/lsp/client.py similarity index 97% rename from coq/lsp/client.py rename to coqpyt/coq/lsp/client.py index 465750e..a18cd40 100644 --- a/coq/lsp/client.py +++ b/coqpyt/coq/lsp/client.py @@ -1,10 +1,10 @@ import time import subprocess -from lsp.json_rpc_endpoint import JsonRpcEndpoint -from lsp.endpoint import LspEndpoint -from lsp.client import LspClient -from lsp.structs import * -from coq.lsp.structs import * +from coqpyt.lsp.json_rpc_endpoint import JsonRpcEndpoint +from coqpyt.lsp.endpoint import LspEndpoint +from coqpyt.lsp.client import LspClient +from coqpyt.lsp.structs import * +from coqpyt.coq.lsp.structs import * class CoqLspClient(LspClient): diff --git a/coq/lsp/structs.py b/coqpyt/coq/lsp/structs.py similarity index 98% rename from coq/lsp/structs.py rename to coqpyt/coq/lsp/structs.py index b6788b5..c301560 100644 --- a/coq/lsp/structs.py +++ b/coqpyt/coq/lsp/structs.py @@ -1,6 +1,6 @@ from enum import Enum from typing import Dict, Optional, Any, List, Tuple -from lsp.structs import Range, VersionedTextDocumentIdentifier, Position +from coqpyt.lsp.structs import Range, VersionedTextDocumentIdentifier, Position class Hyp(object): diff --git a/coq/proof_file.py b/coqpyt/coq/proof_file.py similarity index 98% rename from coq/proof_file.py rename to coqpyt/coq/proof_file.py index 56a3c54..aae942f 100644 --- a/coq/proof_file.py +++ b/coqpyt/coq/proof_file.py @@ -3,14 +3,14 @@ import shutil import uuid import tempfile -from lsp.structs import ( +from coqpyt.lsp.structs import ( TextDocumentItem, VersionedTextDocumentIdentifier, TextDocumentContentChangeEvent, ResponseError, ErrorCodes, ) -from coq.structs import ( +from coqpyt.coq.structs import ( TermType, Step, Term, @@ -18,11 +18,11 @@ ProofTerm, FileContext, ) -from coq.lsp.structs import Result, Query, GoalAnswer, Range -from coq.base_file import CoqFile -from coq.lsp.client import CoqLspClient -from coq.changes import * -from coq.exceptions import * +from coqpyt.coq.lsp.structs import Result, Query, GoalAnswer, Range +from coqpyt.coq.base_file import CoqFile +from coqpyt.coq.lsp.client import CoqLspClient +from coqpyt.coq.changes import * +from coqpyt.coq.exceptions import * from typing import List, Dict, Optional, Tuple diff --git a/coq/structs.py b/coqpyt/coq/structs.py similarity index 98% rename from coq/structs.py rename to coqpyt/coq/structs.py index 21322fa..6c3c009 100644 --- a/coq/structs.py +++ b/coqpyt/coq/structs.py @@ -1,8 +1,8 @@ import re from enum import Enum from typing import Dict, List, Union, Callable -from coq.lsp.structs import RangedSpan, GoalAnswer -from lsp.structs import Diagnostic, Position +from coqpyt.coq.lsp.structs import RangedSpan, GoalAnswer +from coqpyt.lsp.structs import Diagnostic, Position class SegmentType(Enum): diff --git a/coqpyt/lsp/__init__.py b/coqpyt/lsp/__init__.py new file mode 100644 index 0000000..d385c45 --- /dev/null +++ b/coqpyt/lsp/__init__.py @@ -0,0 +1,8 @@ +# from __future__ import absolute_import + +__all__ = [] + +from coqpyt.lsp.json_rpc_endpoint import JsonRpcEndpoint +from coqpyt.lsp.client import LspClient +from coqpyt.lsp.endpoint import LspEndpoint +from coqpyt.lsp import structs diff --git a/lsp/client.py b/coqpyt/lsp/client.py similarity index 99% rename from lsp/client.py rename to coqpyt/lsp/client.py index 7202632..77bfc97 100644 --- a/lsp/client.py +++ b/coqpyt/lsp/client.py @@ -1,5 +1,5 @@ -from lsp import structs -from lsp.endpoint import LspEndpoint +from coqpyt.lsp import structs +from coqpyt.lsp.endpoint import LspEndpoint class LspClient(object): diff --git a/lsp/endpoint.py b/coqpyt/lsp/endpoint.py similarity index 99% rename from lsp/endpoint.py rename to coqpyt/lsp/endpoint.py index 6d019d0..2b5102a 100644 --- a/lsp/endpoint.py +++ b/coqpyt/lsp/endpoint.py @@ -1,7 +1,7 @@ from __future__ import print_function import threading import logging -from lsp import structs +from coqpyt.lsp import structs from typing import Dict, List diff --git a/lsp/json_rpc_endpoint.py b/coqpyt/lsp/json_rpc_endpoint.py similarity index 99% rename from lsp/json_rpc_endpoint.py rename to coqpyt/lsp/json_rpc_endpoint.py index 3aea26e..778a5dd 100644 --- a/lsp/json_rpc_endpoint.py +++ b/coqpyt/lsp/json_rpc_endpoint.py @@ -1,7 +1,7 @@ from __future__ import print_function import json import logging -from lsp import structs +from coqpyt.lsp import structs import threading JSON_RPC_REQ_FORMAT = "Content-Length: {json_string_len}\r\n\r\n{json_string}" diff --git a/lsp/structs.py b/coqpyt/lsp/structs.py similarity index 100% rename from lsp/structs.py rename to coqpyt/lsp/structs.py diff --git a/coqpyt/tests/__init__.py b/coqpyt/tests/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/tests/resources/.gitignore b/coqpyt/tests/resources/.gitignore similarity index 100% rename from tests/resources/.gitignore rename to coqpyt/tests/resources/.gitignore diff --git a/tests/resources/test_bug.v b/coqpyt/tests/resources/test_bug.v similarity index 100% rename from tests/resources/test_bug.v rename to coqpyt/tests/resources/test_bug.v diff --git a/tests/resources/test_bullets.v b/coqpyt/tests/resources/test_bullets.v similarity index 100% rename from tests/resources/test_bullets.v rename to coqpyt/tests/resources/test_bullets.v diff --git a/tests/resources/test_change_empty.v b/coqpyt/tests/resources/test_change_empty.v similarity index 100% rename from tests/resources/test_change_empty.v rename to coqpyt/tests/resources/test_change_empty.v diff --git a/tests/resources/test_derive.v b/coqpyt/tests/resources/test_derive.v similarity index 100% rename from tests/resources/test_derive.v rename to coqpyt/tests/resources/test_derive.v diff --git a/tests/resources/test_exists_notation.v b/coqpyt/tests/resources/test_exists_notation.v similarity index 100% rename from tests/resources/test_exists_notation.v rename to coqpyt/tests/resources/test_exists_notation.v diff --git a/tests/resources/test_get_notation.v b/coqpyt/tests/resources/test_get_notation.v similarity index 100% rename from tests/resources/test_get_notation.v rename to coqpyt/tests/resources/test_get_notation.v diff --git a/tests/resources/test_goal.v b/coqpyt/tests/resources/test_goal.v similarity index 100% rename from tests/resources/test_goal.v rename to coqpyt/tests/resources/test_goal.v diff --git a/tests/resources/test_imports/.gitignore b/coqpyt/tests/resources/test_imports/.gitignore similarity index 100% rename from tests/resources/test_imports/.gitignore rename to coqpyt/tests/resources/test_imports/.gitignore diff --git a/tests/resources/test_imports/Makefile b/coqpyt/tests/resources/test_imports/Makefile similarity index 100% rename from tests/resources/test_imports/Makefile rename to coqpyt/tests/resources/test_imports/Makefile diff --git a/tests/resources/test_imports/Makefile.conf b/coqpyt/tests/resources/test_imports/Makefile.conf similarity index 100% rename from tests/resources/test_imports/Makefile.conf rename to coqpyt/tests/resources/test_imports/Makefile.conf diff --git a/tests/resources/test_imports/_CoqProject b/coqpyt/tests/resources/test_imports/_CoqProject similarity index 100% rename from tests/resources/test_imports/_CoqProject rename to coqpyt/tests/resources/test_imports/_CoqProject diff --git a/tests/resources/test_imports/test_import.v b/coqpyt/tests/resources/test_imports/test_import.v similarity index 100% rename from tests/resources/test_imports/test_import.v rename to coqpyt/tests/resources/test_imports/test_import.v diff --git a/tests/resources/test_imports/test_import2.v b/coqpyt/tests/resources/test_imports/test_import2.v similarity index 100% rename from tests/resources/test_imports/test_import2.v rename to coqpyt/tests/resources/test_imports/test_import2.v diff --git a/tests/resources/test_invalid_1.v b/coqpyt/tests/resources/test_invalid_1.v similarity index 100% rename from tests/resources/test_invalid_1.v rename to coqpyt/tests/resources/test_invalid_1.v diff --git a/tests/resources/test_invalid_2.v b/coqpyt/tests/resources/test_invalid_2.v similarity index 100% rename from tests/resources/test_invalid_2.v rename to coqpyt/tests/resources/test_invalid_2.v diff --git a/tests/resources/test_list_notation.v b/coqpyt/tests/resources/test_list_notation.v similarity index 100% rename from tests/resources/test_list_notation.v rename to coqpyt/tests/resources/test_list_notation.v diff --git a/tests/resources/test_module_type.v b/coqpyt/tests/resources/test_module_type.v similarity index 100% rename from tests/resources/test_module_type.v rename to coqpyt/tests/resources/test_module_type.v diff --git a/tests/resources/test_nested_proofs.v b/coqpyt/tests/resources/test_nested_proofs.v similarity index 100% rename from tests/resources/test_nested_proofs.v rename to coqpyt/tests/resources/test_nested_proofs.v diff --git a/tests/resources/test_non_ending_proof.v b/coqpyt/tests/resources/test_non_ending_proof.v similarity index 100% rename from tests/resources/test_non_ending_proof.v rename to coqpyt/tests/resources/test_non_ending_proof.v diff --git a/tests/resources/test_obligation.v b/coqpyt/tests/resources/test_obligation.v similarity index 100% rename from tests/resources/test_obligation.v rename to coqpyt/tests/resources/test_obligation.v diff --git a/tests/resources/test_simple_file.v b/coqpyt/tests/resources/test_simple_file.v similarity index 100% rename from tests/resources/test_simple_file.v rename to coqpyt/tests/resources/test_simple_file.v diff --git a/tests/resources/test_theorem_tokens.v b/coqpyt/tests/resources/test_theorem_tokens.v similarity index 100% rename from tests/resources/test_theorem_tokens.v rename to coqpyt/tests/resources/test_theorem_tokens.v diff --git a/tests/resources/test_type_class.v b/coqpyt/tests/resources/test_type_class.v similarity index 100% rename from tests/resources/test_type_class.v rename to coqpyt/tests/resources/test_type_class.v diff --git a/tests/resources/test_unknown_notation.v b/coqpyt/tests/resources/test_unknown_notation.v similarity index 100% rename from tests/resources/test_unknown_notation.v rename to coqpyt/tests/resources/test_unknown_notation.v diff --git a/tests/resources/test_valid.v b/coqpyt/tests/resources/test_valid.v similarity index 100% rename from tests/resources/test_valid.v rename to coqpyt/tests/resources/test_valid.v diff --git a/tests/resources/test_where_notation.v b/coqpyt/tests/resources/test_where_notation.v similarity index 100% rename from tests/resources/test_where_notation.v rename to coqpyt/tests/resources/test_where_notation.v diff --git a/tests/test_coq_file.py b/coqpyt/tests/test_coq_file.py similarity index 98% rename from tests/test_coq_file.py rename to coqpyt/tests/test_coq_file.py index 04cc9b3..1573213 100644 --- a/tests/test_coq_file.py +++ b/coqpyt/tests/test_coq_file.py @@ -1,9 +1,9 @@ import os import shutil import pytest -from coq.base_file import CoqFile -from coq.changes import * -from coq.exceptions import * +from coqpyt.coq.base_file import CoqFile +from coqpyt.coq.changes import * +from coqpyt.coq.exceptions import * coq_file: CoqFile = None diff --git a/tests/test_coq_lsp_client.py b/coqpyt/tests/test_coq_lsp_client.py similarity index 81% rename from tests/test_coq_lsp_client.py rename to coqpyt/tests/test_coq_lsp_client.py index f90f90c..7c5bf38 100644 --- a/tests/test_coq_lsp_client.py +++ b/coqpyt/tests/test_coq_lsp_client.py @@ -1,7 +1,7 @@ import os -from coq.lsp.client import CoqLspClient -from lsp.structs import * -from coq.lsp.structs import * +from coqpyt.coq.lsp.client import CoqLspClient +from coqpyt.lsp.structs import * +from coqpyt.coq.lsp.structs import * def test_save_vo(): diff --git a/tests/test_json_rpc_endpoint.py b/coqpyt/tests/test_json_rpc_endpoint.py similarity index 99% rename from tests/test_json_rpc_endpoint.py rename to coqpyt/tests/test_json_rpc_endpoint.py index 23f31f9..354c9f7 100644 --- a/tests/test_json_rpc_endpoint.py +++ b/coqpyt/tests/test_json_rpc_endpoint.py @@ -1,6 +1,6 @@ import os -import lsp import pytest +from coqpyt import lsp JSON_RPC_RESULT_LIST = [ 'Content-Length: 40\r\n\r\n{"key_str": "some_string", "key_num": 1}'.encode( diff --git a/tests/test_proof_file.py b/coqpyt/tests/test_proof_file.py similarity index 99% rename from tests/test_proof_file.py rename to coqpyt/tests/test_proof_file.py index 3a4bfb0..bd50908 100644 --- a/tests/test_proof_file.py +++ b/coqpyt/tests/test_proof_file.py @@ -5,11 +5,11 @@ import pytest import tempfile from typing import List, Tuple -from coq.lsp.structs import * -from coq.structs import TermType, Term, CoqError, CoqErrorCodes -from coq.proof_file import ProofFile -from coq.exceptions import * -from coq.changes import * +from coqpyt.coq.lsp.structs import * +from coqpyt.coq.structs import TermType, Term, CoqError, CoqErrorCodes +from coqpyt.coq.proof_file import ProofFile +from coqpyt.coq.exceptions import * +from coqpyt.coq.changes import * versionId: VersionedTextDocumentIdentifier = None state: ProofFile = None diff --git a/tests/test_readme.py b/coqpyt/tests/test_readme.py similarity index 75% rename from tests/test_readme.py rename to coqpyt/tests/test_readme.py index 3327393..0f997e1 100644 --- a/tests/test_readme.py +++ b/coqpyt/tests/test_readme.py @@ -15,9 +15,10 @@ def teardown_aux(): def test_if_readme_runs(teardown_aux): - with open("README.md", "r") as f: - text = f.read() + with open("../README.md", "r") as f: + text, example_path = f.read(), "../examples/example.v" script = text.split("```python")[1].split("```")[0] + script = example_path.join(script.split(example_path[3:])) with open(temp_path, "w") as f2: f2.write(script) run = subprocess.run(f"python3 {temp_path}", shell=True, capture_output=True) diff --git a/lsp/__init__.py b/lsp/__init__.py deleted file mode 100644 index 9ef13ef..0000000 --- a/lsp/__init__.py +++ /dev/null @@ -1,8 +0,0 @@ -# from __future__ import absolute_import - -__all__ = [] - -from lsp.json_rpc_endpoint import JsonRpcEndpoint -from lsp.client import LspClient -from lsp.endpoint import LspEndpoint -from lsp import structs diff --git a/setup.py b/setup.py index 1750321..35199a0 100644 --- a/setup.py +++ b/setup.py @@ -24,14 +24,14 @@ def run_tests(self): setup( - name="coq-lsp-pyclient", + name="coqpyt", version="0.0.1", author="Pedro Carrott, Nuno Saavedra, Avi Yeger", author_email="pedro.carrott@imperial.ac.uk", description="CoqPyt: a Python client for coq-lsp", long_description=long_description, long_description_content_type="text/markdown", - url="https://github.com/sr-lab/coq-lsp-pyclient", + url="https://github.com/sr-lab/CoqPyt", packages=find_packages(), tests_require=["pytest", "pytest_mock"], cmdclass={"test": PyTest}, From 5575c534f6cd113d3b6f727f7addfbd528eb7fbd Mon Sep 17 00:00:00 2001 From: pcarrott Date: Wed, 1 Nov 2023 14:47:32 +0000 Subject: [PATCH 02/28] Add workflow for embedding code in readme --- .github/workflows/readme.yml | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 .github/workflows/readme.yml diff --git a/.github/workflows/readme.yml b/.github/workflows/readme.yml new file mode 100644 index 0000000..b8b736d --- /dev/null +++ b/.github/workflows/readme.yml @@ -0,0 +1,31 @@ +name: Embed code in README + +on: + pull_request_target: + types: + - opened + +jobs: + embed: + runs-on: ubuntu-latest + + steps: + - name: Checkout + uses: actions/checkout@v3.5.2 + + - name: Set up node + uses: actions/setup-node@v3 + with: + node-version: 14 + + - name: Install embedme + run: npm install -g embedme + + - name: Embed code + run: embedme README.md + + - name: Commit changes + uses: EndBug/add-and-commit@v9 + with: + add: "README.md" + push: origin ${{ github.head_ref }} \ No newline at end of file From 053feb6e101c6b426a577ced24d4b052ac7112e5 Mon Sep 17 00:00:00 2001 From: pcarrott Date: Wed, 1 Nov 2023 15:19:13 +0000 Subject: [PATCH 03/28] Extract example to python file and embed file in readme --- README.md | 83 +++++++------------------------- coqpyt/tests/test_readme.py | 10 ++-- examples/readme.py | 70 +++++++++++++++++++++++++++ examples/{example.v => readme.v} | 0 4 files changed, 93 insertions(+), 70 deletions(-) create mode 100644 examples/readme.py rename examples/{example.v => readme.v} (100%) diff --git a/README.md b/README.md index 71f1429..bd2d0c3 100644 --- a/README.md +++ b/README.md @@ -17,75 +17,28 @@ python -m pip install -e . ``` ## Usage -```python -import os -from coqpyt.coq.base_file import CoqFile -from coqpyt.coq.proof_file import ProofFile -from coqpyt.coq.structs import TermType - -# Open Coq file -with CoqFile(os.path.join(os.getcwd(), "examples/example.v")) as coq_file: - coq_file.exec(nsteps=2) - # Get all terms defined until now - print("Number of terms:", len(coq_file.context.terms)) - # Filter by Tactics - print("Number of tactics:", - len( - list(filter( - lambda term: term.type == TermType.TACTIC, - coq_file.context.terms.values(), - )) - ) - ) - - # Enter proof - coq_file.exec(nsteps=4) - print("In proof:", coq_file.in_proof) - # Get current goals - print(coq_file.current_goals()) - - # Save compiled file - coq_file.save_vo() - print("Compiled file exists:", os.path.exists("examples/example.vo")) - os.remove("examples/example.vo") - - # Run remaining file - coq_file.run() - print("Checked:", coq_file.checked) - # Get all terms defined until now - print("Number of terms:", len(coq_file.context.terms)) - -with ProofFile(os.path.join(os.getcwd(), "examples/example.v")) as proof_file: - # Number of proofs in the file - print("Number of proofs:", len(proof_file.proofs)) - print("Proof:", proof_file.proofs[0].text) - - # Print steps of proof - for step in proof_file.proofs[0].steps: - print(step.text, end="") - print() - - # Get the context used in the third step - print(proof_file.proofs[0].steps[2].context) - # Print the goals in the third step - print(proof_file.proofs[0].steps[2].goals) - - # Print number of terms in context - print("Number of terms:", len(proof_file.context.terms)) - # Filter for Notations only - print("Number of notations:", - len( - list(filter( - lambda term: term.type == TermType.NOTATION, - proof_file.context.terms.values(), - )) - ) - ) + +Import classes from the ``coqpyt`` package. + + +```py +``` + +Create a CoqFile object, execute the file and extract the generated context. + + +```py +``` + +Create a ProofFile object (a CoqFile instance) and interact with the proofs. + + +```py ``` ## Tests -To run the tests for CoqPyt go to the folder ```coqpyt``` and run: +To run the tests for CoqPyt go to the folder ``coqpyt`` and run: ```bash pytest tests -s ``` diff --git a/coqpyt/tests/test_readme.py b/coqpyt/tests/test_readme.py index 0f997e1..741d652 100644 --- a/coqpyt/tests/test_readme.py +++ b/coqpyt/tests/test_readme.py @@ -14,11 +14,11 @@ def teardown_aux(): os.remove(temp_path) -def test_if_readme_runs(teardown_aux): - with open("../README.md", "r") as f: - text, example_path = f.read(), "../examples/example.v" - script = text.split("```python")[1].split("```")[0] - script = example_path.join(script.split(example_path[3:])) +def test_readme_example(teardown_aux): + readme_path = "../examples/readme" + with open(f"{readme_path}.py", "r") as f: + script, vfile = f.read(), f"{readme_path}.v" + script = vfile.join(script.split(vfile[3:])) with open(temp_path, "w") as f2: f2.write(script) run = subprocess.run(f"python3 {temp_path}", shell=True, capture_output=True) diff --git a/examples/readme.py b/examples/readme.py new file mode 100644 index 0000000..40fd613 --- /dev/null +++ b/examples/readme.py @@ -0,0 +1,70 @@ +import os +from coqpyt.coq.base_file import CoqFile +from coqpyt.coq.proof_file import ProofFile +from coqpyt.coq.structs import TermType + +# Open Coq file +with CoqFile(os.path.join(os.getcwd(), "examples/readme.v")) as coq_file: + coq_file.exec(nsteps=2) + # Get all terms defined until now + print("Number of terms:", len(coq_file.context.terms)) + # Filter by Tactics + print( + "Number of tactics:", + len( + list( + filter( + lambda term: term.type == TermType.TACTIC, + coq_file.context.terms.values(), + ) + ) + ), + ) + + # Enter proof + coq_file.exec(nsteps=4) + print("In proof:", coq_file.in_proof) + # Get current goals + print(coq_file.current_goals()) + + # Save compiled file + coq_file.save_vo() + print("Compiled file exists:", os.path.exists("examples/readme.vo")) + os.remove("examples/readme.vo") + + # Run remaining file + coq_file.run() + print("Checked:", coq_file.checked) + # Get all terms defined until now + print("Number of terms:", len(coq_file.context.terms)) + +# Create Proof file +with ProofFile(os.path.join(os.getcwd(), "examples/readme.v")) as proof_file: + # Number of proofs in the file + print("Number of proofs:", len(proof_file.proofs)) + print("Proof:", proof_file.proofs[0].text) + + # Print steps of proof + for step in proof_file.proofs[0].steps: + print(step.text, end="") + print() + + # Get the context used in the third step + print(proof_file.proofs[0].steps[2].context) + # Print the goals in the third step + print(proof_file.proofs[0].steps[2].goals) + + # Print number of terms in context + print("Number of terms:", len(proof_file.context.terms)) + # Filter for Notations only + print( + "Number of notations:", + len( + list( + filter( + lambda term: term.type == TermType.NOTATION, + proof_file.context.terms.values(), + ) + ) + ), + ) diff --git a/examples/example.v b/examples/readme.v similarity index 100% rename from examples/example.v rename to examples/readme.v From f37791408f1185a1b089fa7fff4628b529f5283a Mon Sep 17 00:00:00 2001 From: pcarrott Date: Wed, 1 Nov 2023 15:22:50 +0000 Subject: [PATCH 04/28] Update node versions in embed workflow --- .github/workflows/readme.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/readme.yml b/.github/workflows/readme.yml index b8b736d..4fc9d2c 100644 --- a/.github/workflows/readme.yml +++ b/.github/workflows/readme.yml @@ -14,9 +14,9 @@ jobs: uses: actions/checkout@v3.5.2 - name: Set up node - uses: actions/setup-node@v3 + uses: actions/setup-node@v4 with: - node-version: 14 + node-version: 20 - name: Install embedme run: npm install -g embedme From 6cfdbf789cb1ff9aeb3d3ff07b5ed8ffce7376df Mon Sep 17 00:00:00 2001 From: Pedro Carrott <43729507+pcarrott@users.noreply.github.com> Date: Wed, 1 Nov 2023 15:29:33 +0000 Subject: [PATCH 05/28] Embed README when changes are pushed to Python file --- .github/workflows/readme.yml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/readme.yml b/.github/workflows/readme.yml index 4fc9d2c..dc363cd 100644 --- a/.github/workflows/readme.yml +++ b/.github/workflows/readme.yml @@ -1,9 +1,9 @@ name: Embed code in README on: - pull_request_target: - types: - - opened + push: + paths: + - "examples/readme.py" jobs: embed: @@ -28,4 +28,4 @@ jobs: uses: EndBug/add-and-commit@v9 with: add: "README.md" - push: origin ${{ github.head_ref }} \ No newline at end of file + push: origin ${{ github.head_ref }} From bffc41878b204a2b5b216107a837e2cbd0a930f4 Mon Sep 17 00:00:00 2001 From: pcarrott Date: Wed, 1 Nov 2023 15:35:19 +0000 Subject: [PATCH 06/28] Trigger readme embedding --- examples/readme.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/readme.py b/examples/readme.py index 40fd613..f5c79d7 100644 --- a/examples/readme.py +++ b/examples/readme.py @@ -38,7 +38,7 @@ # Get all terms defined until now print("Number of terms:", len(coq_file.context.terms)) -# Create Proof file +# Open Proof file with ProofFile(os.path.join(os.getcwd(), "examples/readme.v")) as proof_file: # Number of proofs in the file print("Number of proofs:", len(proof_file.proofs)) From 25f5d2f23679503acddbf03d4107b8cd0d8a71f3 Mon Sep 17 00:00:00 2001 From: pcarrott Date: Wed, 1 Nov 2023 15:32:55 +0000 Subject: [PATCH 07/28] Commit from GitHub Actions (Embed code in README) --- README.md | 65 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 65 insertions(+) diff --git a/README.md b/README.md index bd2d0c3..d38b956 100644 --- a/README.md +++ b/README.md @@ -22,18 +22,83 @@ Import classes from the ``coqpyt`` package. ```py +from coqpyt.coq.base_file import CoqFile +from coqpyt.coq.proof_file import ProofFile +from coqpyt.coq.structs import TermType ``` Create a CoqFile object, execute the file and extract the generated context. ```py +with CoqFile(os.path.join(os.getcwd(), "examples/readme.v")) as coq_file: + coq_file.exec(nsteps=2) + # Get all terms defined until now + print("Number of terms:", len(coq_file.context.terms)) + # Filter by Tactics + print( + "Number of tactics:", + len( + list( + filter( + lambda term: term.type == TermType.TACTIC, + coq_file.context.terms.values(), + ) + ) + ), + ) + + # Enter proof + coq_file.exec(nsteps=4) + print("In proof:", coq_file.in_proof) + # Get current goals + print(coq_file.current_goals()) + + # Save compiled file + coq_file.save_vo() + print("Compiled file exists:", os.path.exists("examples/readme.vo")) + os.remove("examples/readme.vo") + + # Run remaining file + coq_file.run() + print("Checked:", coq_file.checked) + # Get all terms defined until now + print("Number of terms:", len(coq_file.context.terms)) ``` Create a ProofFile object (a CoqFile instance) and interact with the proofs. ```py +with ProofFile(os.path.join(os.getcwd(), "examples/readme.v")) as proof_file: + # Number of proofs in the file + print("Number of proofs:", len(proof_file.proofs)) + print("Proof:", proof_file.proofs[0].text) + + # Print steps of proof + for step in proof_file.proofs[0].steps: + print(step.text, end="") + print() + + # Get the context used in the third step + print(proof_file.proofs[0].steps[2].context) + # Print the goals in the third step + print(proof_file.proofs[0].steps[2].goals) + + # Print number of terms in context + print("Number of terms:", len(proof_file.context.terms)) + # Filter for Notations only + print( + "Number of notations:", + len( + list( + filter( + lambda term: term.type == TermType.NOTATION, + proof_file.context.terms.values(), + ) + ) + ), + ) ``` ## Tests From 10ea0ceb8b3c18233b5270d17dfc0d19daecfef7 Mon Sep 17 00:00:00 2001 From: Pedro Carrott <43729507+pcarrott@users.noreply.github.com> Date: Wed, 1 Nov 2023 15:39:32 +0000 Subject: [PATCH 08/28] Changes to README trigger embed workflow --- .github/workflows/readme.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/readme.yml b/.github/workflows/readme.yml index dc363cd..6947988 100644 --- a/.github/workflows/readme.yml +++ b/.github/workflows/readme.yml @@ -4,6 +4,7 @@ on: push: paths: - "examples/readme.py" + - "README.md" jobs: embed: From c4e8174a4c6b64f4f1b262d15d87b2173a85303c Mon Sep 17 00:00:00 2001 From: pcarrott Date: Wed, 8 Nov 2023 19:22:48 +0000 Subject: [PATCH 09/28] Refactor ProofTerm for obligations --- coq/base_file.py | 4 ++++ coq/proof_file.py | 19 +++++++++++-------- coq/structs.py | 11 +++++++++-- tests/test_proof_file.py | 17 ++++++++++++++++- 4 files changed, 40 insertions(+), 11 deletions(-) diff --git a/coq/base_file.py b/coq/base_file.py index 5bef267..846e939 100644 --- a/coq/base_file.py +++ b/coq/base_file.py @@ -476,6 +476,10 @@ def traverse_expr(expr): if expr[1][0] == "Derive": prop = CoqFile.get_ident(expr[2][2]) self.__add_term(prop, self.curr_step, term_type) + elif term_type == TermType.OBLIGATION: + self._last_term = Term( + self.curr_step, term_type, self.path, self.curr_module[:] + ) else: names = traverse_expr(expr) for name in names: diff --git a/coq/proof_file.py b/coq/proof_file.py index 9884769..96eb290 100644 --- a/coq/proof_file.py +++ b/coq/proof_file.py @@ -383,17 +383,16 @@ def __get_steps( return steps def __get_proof(self, proofs): - term, statement_context = None, None + program, statement_context = None, None if self.get_term_type(self.prev_step.ast) == TermType.OBLIGATION: - term, statement_context = self.__get_program_context() + program, statement_context = self.__get_program_context() elif self.get_term_type(self.prev_step.ast) != TermType.OTHER: - term = self._last_term statement_context = self.__step_context(self.prev_step) # HACK: We ignore proofs inside a Module Type since they can't be used outside # and should be overriden. if self.in_proof and len(self.curr_module_type) == 0: steps = self.__get_steps(proofs) - proofs.append((term, statement_context, steps)) + proofs.append((self._last_term, statement_context, steps, program)) def __call_context(self, calls: List[Tuple]): context, calls = [], [call[0](*call[1:]) for call in calls] @@ -418,11 +417,15 @@ def get_proof_step(step: Tuple[Step, Optional[GoalAnswer], List[Tuple]]): self.close() raise e - proof_steps = [ - (term, self.__call_context(calls), list(map(get_proof_step, steps))) - for term, calls, steps in proofs + return [ + ProofTerm( + term, + self.__call_context(calls), + list(map(get_proof_step, steps)), + program, + ) + for term, calls, steps, program in proofs ] - return list(map(lambda t: ProofTerm(*t), proof_steps)) def __find_step(self, range: Range) -> Optional[Tuple[ProofTerm, int]]: for proof in self.proofs: diff --git a/coq/structs.py b/coq/structs.py index 21322fa..a314fd7 100644 --- a/coq/structs.py +++ b/coq/structs.py @@ -1,6 +1,6 @@ import re from enum import Enum -from typing import Dict, List, Union, Callable +from typing import Dict, List, Union, Callable, Optional from coq.lsp.structs import RangedSpan, GoalAnswer from lsp.structs import Diagnostic, Position @@ -132,10 +132,17 @@ def diagnostics(self) -> List[Diagnostic]: class ProofTerm(Term): - def __init__(self, term: Term, context: List[Term], steps: List[ProofStep]): + def __init__( + self, + term: Term, + context: List[Term], + steps: List[ProofStep], + program: Optional[Term] = None, + ): super().__init__(term.step, term.type, term.file_path, term.module) self.steps = steps self.context = context + self.program = program class FileContext: diff --git a/tests/test_proof_file.py b/tests/test_proof_file.py index 2617d6b..59f9243 100644 --- a/tests/test_proof_file.py +++ b/tests/test_proof_file.py @@ -910,6 +910,19 @@ def test_obligation(setup, teardown): ), ('Notation "x = y" := (eq x y) : type_scope.', TermType.NOTATION, []), ] + texts = [ + "Obligation 2 of id1.", + "Next Obligation of id1.", + "Obligation 2 of id2 : type with reflexivity.", + "Next Obligation of id2 with reflexivity.", + "Next Obligation.", + "Next Obligation with reflexivity.", + "Obligation 1.", + "Obligation 2 : type with reflexivity.", + "Obligation 1 of id with reflexivity.", + "Obligation 1 of id : type.", + "Obligation 2 : type.", + ] programs = [ ("id1", "S (pred n)"), ("id1", "S (pred n)"), @@ -926,8 +939,10 @@ def test_obligation(setup, teardown): for i, proof in enumerate(proofs): compare_context(statement_context, proof.context) + assert proof.text == texts[i] + assert proof.program is not None assert ( - proof.text + proof.program.text == "Program Definition " + programs[i][0] + " (n : nat) : { x : nat | x = n } := if dec (leb n 0) then 0%nat else " From 1e277b79d470b35179e9faf7838cc5601fab8f7f Mon Sep 17 00:00:00 2001 From: pcarrott Date: Wed, 8 Nov 2023 20:35:19 +0000 Subject: [PATCH 10/28] Ignore term types to avoid incorrect nested proofs and unnecessary steps --- coq/proof_file.py | 12 ++++++++++++ tests/resources/test_nested_proofs.v | 2 ++ 2 files changed, 14 insertions(+) diff --git a/coq/proof_file.py b/coq/proof_file.py index 96eb290..552a767 100644 --- a/coq/proof_file.py +++ b/coq/proof_file.py @@ -357,6 +357,18 @@ def __get_steps( raise e self.__step() + if self.get_term_type(self.prev_step.ast) in [ + TermType.TACTIC, + TermType.NOTATION, + TermType.INDUCTIVE, + TermType.COINDUCTIVE, + TermType.RECORD, + TermType.CLASS, + TermType.SCHEME, + TermType.VARIANT, + ]: + continue + # Nested proofs if self.get_term_type(self.prev_step.ast) != TermType.OTHER: self.__get_proof(proofs) diff --git a/tests/resources/test_nested_proofs.v b/tests/resources/test_nested_proofs.v index 3ee4bb0..5e0bd3c 100644 --- a/tests/resources/test_nested_proofs.v +++ b/tests/resources/test_nested_proofs.v @@ -5,6 +5,8 @@ S n * m = 0 + (S n * m). Proof. intros n m. + Ltac reduce_eq := simpl; reflexivity. + Theorem plus_O_n : forall n:nat, n = 0 + n. intros n. simpl; reflexivity. From fbfd9c019accb4900f0607c15f1360810b978ed9 Mon Sep 17 00:00:00 2001 From: pcarrott Date: Thu, 9 Nov 2023 02:18:15 +0000 Subject: [PATCH 11/28] Fix ProofTerm by keeping last term before get_steps --- coq/proof_file.py | 3 ++- tests/test_proof_file.py | 2 ++ 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/coq/proof_file.py b/coq/proof_file.py index 552a767..d340b81 100644 --- a/coq/proof_file.py +++ b/coq/proof_file.py @@ -403,8 +403,9 @@ def __get_proof(self, proofs): # HACK: We ignore proofs inside a Module Type since they can't be used outside # and should be overriden. if self.in_proof and len(self.curr_module_type) == 0: + term = self._last_term # Keep the term before rewrite steps = self.__get_steps(proofs) - proofs.append((self._last_term, statement_context, steps, program)) + proofs.append((term, statement_context, steps, program)) def __call_context(self, calls: List[Tuple]): context, calls = [], [call[0](*call[1:]) for call in calls] diff --git a/tests/test_proof_file.py b/tests/test_proof_file.py index 59f9243..cd7ba66 100644 --- a/tests/test_proof_file.py +++ b/tests/test_proof_file.py @@ -833,6 +833,7 @@ def test_nested_proofs(setup, teardown): for i, step in enumerate(proofs[0].steps): assert step.text == steps[i] + theorem = "Theorem mult_0_plus : forall n m : nat, S n * m = 0 + (S n * m)." steps = [ "\nProof.", "\nintros n m.", @@ -840,6 +841,7 @@ def test_nested_proofs(setup, teardown): "\nreflexivity.", "\nQed.", ] + assert proofs[1].text == theorem assert len(proofs[1].steps) == len(steps) for i, step in enumerate(proofs[1].steps): assert step.text == steps[i] From e84513bdda2a5d7a359b1c6f2e40e9ddac3acaa9 Mon Sep 17 00:00:00 2001 From: pcarrott Date: Fri, 10 Nov 2023 00:00:25 +0000 Subject: [PATCH 12/28] Make current_goals property --- coqpyt/coq/base_file.py | 35 ++++++++++++++++++----------------- coqpyt/coq/proof_file.py | 8 ++++---- examples/readme.py | 2 +- 3 files changed, 23 insertions(+), 22 deletions(-) diff --git a/coqpyt/coq/base_file.py b/coqpyt/coq/base_file.py index 722d2f9..6e06821 100644 --- a/coqpyt/coq/base_file.py +++ b/coqpyt/coq/base_file.py @@ -679,13 +679,30 @@ def checked(self) -> bool: """ return self.steps_taken == len(self.steps) + @property + def current_goals(self) -> Optional[GoalAnswer]: + """Get goals in current position. + + Returns: + Optional[GoalAnswer]: Goals in the current position if there are goals + """ + end_pos = ( + Position(0, 0) if self.steps_taken == 0 else self.prev_step.ast.range.end + ) + + if end_pos != self.__last_end_pos: + self.__current_goals = self._goals(end_pos) + self.__last_end_pos = end_pos + + return self.__current_goals + @property def in_proof(self) -> bool: """ Returns: bool: True if the current step is inside a proof """ - return self.__in_proof(self.current_goals()) + return self.__in_proof(self.current_goals) @property def terms(self) -> List[Term]: @@ -795,22 +812,6 @@ def run(self) -> List[Step]: """ return self.exec(len(self.steps)) - def current_goals(self) -> Optional[GoalAnswer]: - """Get goals in current position. - - Returns: - Optional[GoalAnswer]: Goals in the current position if there are goals - """ - end_pos = ( - Position(0, 0) if self.steps_taken == 0 else self.prev_step.ast.range.end - ) - - if end_pos != self.__last_end_pos: - self.__current_goals = self._goals(end_pos) - self.__last_end_pos = end_pos - - return self.__current_goals - def save_vo(self): """Compiles the vo file for this Coq file.""" uri = f"file://{self.__path}" diff --git a/coqpyt/coq/proof_file.py b/coqpyt/coq/proof_file.py index aae942f..b979383 100644 --- a/coqpyt/coq/proof_file.py +++ b/coqpyt/coq/proof_file.py @@ -327,7 +327,7 @@ def traverse_expr(expr): id = ".".join(self.curr_module + [id]) return self.__program_context[id] elif tag in [2, 3, 5]: - id = self.current_goals().program[0][0][1] + id = self.current_goals.program[0][0][1] # This works because the obligation must be in the # same module as the program id = ".".join(self.curr_module + [id]) @@ -336,7 +336,7 @@ def traverse_expr(expr): raise RuntimeError(f"Unknown obligation command with tag number {tag}: {text}") def __check_program(self): - goals = self.current_goals() + goals = self.current_goals if len(goals.program) == 0: return id = ".".join(self.curr_module + [goals.program[-1][0][1]]) @@ -358,7 +358,7 @@ def __get_steps( steps = [] while self.in_proof and not self.checked: try: - goals = self.current_goals() + goals = self.current_goals except Exception as e: self.__aux_file.close() raise e @@ -377,7 +377,7 @@ def __get_steps( steps.append((self.prev_step, goals, context_calls)) try: - goals = self.current_goals() + goals = self.current_goals except Exception as e: self.__aux_file.close() raise e diff --git a/examples/readme.py b/examples/readme.py index f5c79d7..39246be 100644 --- a/examples/readme.py +++ b/examples/readme.py @@ -25,7 +25,7 @@ coq_file.exec(nsteps=4) print("In proof:", coq_file.in_proof) # Get current goals - print(coq_file.current_goals()) + print(coq_file.current_goals) # Save compiled file coq_file.save_vo() From 777eda5c24bf27e67c96c21dc742e079576e8187 Mon Sep 17 00:00:00 2001 From: pcarrott Date: Fri, 10 Nov 2023 00:06:21 +0000 Subject: [PATCH 13/28] Fix DeprecationWarning from tests --- coqpyt/tests/test_proof_file.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/coqpyt/tests/test_proof_file.py b/coqpyt/tests/test_proof_file.py index bd50908..b7ccbc0 100644 --- a/coqpyt/tests/test_proof_file.py +++ b/coqpyt/tests/test_proof_file.py @@ -209,7 +209,7 @@ def test_get_proofs(setup, teardown): ], [ ( - 'Inductive and (A B:Prop) : Prop := conj : A -> B -> A /\ B where "A /\ B" := (and A B) : type_scope.', + 'Inductive and (A B:Prop) : Prop := conj : A -> B -> A /\\ B where "A /\\ B" := (and A B) : type_scope.', TermType.NOTATION, [], ), From 9d469589cfb8790098ba34fa0431695302269664 Mon Sep 17 00:00:00 2001 From: pcarrott Date: Fri, 10 Nov 2023 00:17:35 +0000 Subject: [PATCH 14/28] Change argument order in add_step --- coqpyt/coq/base_file.py | 10 +++++----- coqpyt/coq/proof_file.py | 8 ++++---- coqpyt/tests/test_coq_file.py | 6 +++--- coqpyt/tests/test_proof_file.py | 24 ++++++++++++------------ 4 files changed, 24 insertions(+), 24 deletions(-) diff --git a/coqpyt/coq/base_file.py b/coqpyt/coq/base_file.py index 6e06821..ed18422 100644 --- a/coqpyt/coq/base_file.py +++ b/coqpyt/coq/base_file.py @@ -590,8 +590,8 @@ def _delete_step( def _add_step( self, - step_text: str, previous_step_index: int, + step_text: str, in_proof: bool = False, validate_file: bool = True, ) -> None: @@ -648,8 +648,8 @@ def _change_steps(self, changes: List[CoqChange]): for i, change in enumerate(changes): if isinstance(change, CoqAddStep): self._add_step( - change.step_text, change.previous_step_index, + change.step_text, validate_file=False, ) offset_steps += 1 @@ -778,23 +778,23 @@ def delete_step(self, step_index: int) -> None: def add_step( self, - step_text: str, previous_step_index: int, + step_text: str, ) -> None: """Adds a step to the file. The step must be inside a proof. This function will change the original file. If an exception is thrown the file will not be changed. Args: - step_text (str): The text of the step to add. previous_step_index (int): The index of the previous step of the new step. + step_text (str): The text of the step to add. Raises: NotImplementedError: If the step added is not on a proof. InvalidFileException: If the file being changed is not valid. InvalidStepException: If the step added is not valid """ - self._make_change(self._add_step, step_text, previous_step_index) + self._make_change(self._add_step, previous_step_index, step_text) def change_steps(self, changes: List[CoqChange]): """Changes the steps of the Coq file transactionally. diff --git a/coqpyt/coq/proof_file.py b/coqpyt/coq/proof_file.py index b979383..f5e3ac0 100644 --- a/coqpyt/coq/proof_file.py +++ b/coqpyt/coq/proof_file.py @@ -476,12 +476,12 @@ def proofs(self) -> List[ProofTerm]: """ return self.__proofs - def add_step(self, step_text: str, previous_step_index: int): + def add_step(self, previous_step_index: int, step_text: str): proof, prev = self.__find_prev(self.steps[previous_step_index].ast.range) if prev == -1: - self._make_change(self._add_step, step_text, previous_step_index) + self._make_change(self._add_step, previous_step_index, step_text) else: - self._make_change(self._add_step, step_text, previous_step_index, True) + self._make_change(self._add_step, previous_step_index, step_text, True) proof.steps.insert(prev + 1, self.__get_step(previous_step_index + 1)) # We should change the goals of all the steps in the same proof # after the one that was changed @@ -515,8 +515,8 @@ def change_steps(self, changes: List[CoqChange]): self.steps[change.previous_step_index].ast.range ) self._add_step( - change.step_text, change.previous_step_index, + change.step_text, in_proof=True, validate_file=False, ) diff --git a/coqpyt/tests/test_coq_file.py b/coqpyt/tests/test_coq_file.py index 1573213..97f7158 100644 --- a/coqpyt/tests/test_coq_file.py +++ b/coqpyt/tests/test_coq_file.py @@ -74,16 +74,16 @@ def test_add_step(): try: steps = coq_file.exec(nsteps=8) assert steps[-1].text == "\n Print plus." - coq_file.add_step("\n Print minus.", 7) + coq_file.add_step(7, "\n Print minus.") steps = coq_file.exec(nsteps=1) assert steps[-1].text == "\n Print minus." - coq_file.add_step("\n Print minus.", 6) + coq_file.add_step(6, "\n Print minus.") steps = coq_file.exec(nsteps=1) assert steps[-1].text == "\n Print Nat.add." assert steps[-1].ast.range.start.line == 14 with pytest.raises(NotImplementedError): - coq_file.add_step("\n Print minus.", 0) + coq_file.add_step(0, "\n Print minus.") finally: coq_file.close() if os.path.exists(new_file_path): diff --git a/coqpyt/tests/test_proof_file.py b/coqpyt/tests/test_proof_file.py index b7ccbc0..de179d2 100644 --- a/coqpyt/tests/test_proof_file.py +++ b/coqpyt/tests/test_proof_file.py @@ -494,7 +494,7 @@ def test_get_proofs_valid_change(setup, teardown): assert step.text == texts[i] assert str(proofs[0].steps[i].goals) == str(goals[i]) - state.add_step("\n intros n.", 5) + state.add_step(5, "\n intros n.") versionId.version += 1 proofs = state.proofs @@ -549,7 +549,7 @@ def test_get_proofs_valid_change(setup, teardown): assert str(proofs[0].steps[i].goals) == str(goals[i]) # Check if context is changed correctly - state.add_step("\n Print minus.", 7) + state.add_step(7, "\n Print minus.") texts = [ "\n Proof.", "\n intros n.", @@ -580,10 +580,10 @@ def test_get_proofs_valid_change(setup, teardown): # Add outside of proof with pytest.raises(NotImplementedError): - state.add_step("\n Print plus.", 25) + state.add_step(25, "\n Print plus.") # Add step in beginning of proof - state.add_step("\n Print plus.", 26) + state.add_step(26, "\n Print plus.") assert state.steps[27].text == "\n Print plus." # Delete outside of proof @@ -591,7 +591,7 @@ def test_get_proofs_valid_change(setup, teardown): state.delete_step(33) # Add step to end of proof - state.add_step("\n Print plus.", 31) + state.add_step(31, "\n Print plus.") assert state.steps[32].text == "\n Print plus." # Delete step in beginning of proof @@ -699,16 +699,16 @@ def check_rollback(): state.delete_step(16) check_rollback() with pytest.raises(InvalidStepException): - state.add_step("invalid_tactic", 7) + state.add_step(7, "invalid_tactic") check_rollback() with pytest.raises(InvalidStepException): - state.add_step("invalid_tactic.", 7) + state.add_step(7, "invalid_tactic.") check_rollback() with pytest.raises(InvalidStepException): - state.add_step("\n invalid_tactic.", 7) + state.add_step(7, "\n invalid_tactic.") check_rollback() with pytest.raises(InvalidStepException): - state.add_step("\n invalid_tactic x $$$ y.", 7) + state.add_step(7, "\n invalid_tactic x $$$ y.") check_rollback() @@ -716,20 +716,20 @@ def check_rollback(): @pytest.mark.parametrize("teardown", [(True,)], indirect=True) def test_get_proofs_change_notation(setup, teardown): # Just checking if the program does not crash - state.add_step(" destruct (a Date: Fri, 10 Nov 2023 00:15:09 +0000 Subject: [PATCH 15/28] Commit from GitHub Actions (Embed code in README) --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index d38b956..36b8c3e 100644 --- a/README.md +++ b/README.md @@ -52,7 +52,7 @@ with CoqFile(os.path.join(os.getcwd(), "examples/readme.v")) as coq_file: coq_file.exec(nsteps=4) print("In proof:", coq_file.in_proof) # Get current goals - print(coq_file.current_goals()) + print(coq_file.current_goals) # Save compiled file coq_file.save_vo() From e40c83388fe2641beae1e9a346c09f264adb25f6 Mon Sep 17 00:00:00 2001 From: pcarrott Date: Fri, 10 Nov 2023 01:04:54 +0000 Subject: [PATCH 16/28] Simplify Makefile in test_imports --- .../tests/resources/test_imports/.gitignore | 4 +- coqpyt/tests/resources/test_imports/Makefile | 997 +----------------- .../resources/test_imports/Makefile.conf | 71 -- 3 files changed, 25 insertions(+), 1047 deletions(-) delete mode 100644 coqpyt/tests/resources/test_imports/Makefile.conf diff --git a/coqpyt/tests/resources/test_imports/.gitignore b/coqpyt/tests/resources/test_imports/.gitignore index 633871c..58ad313 100644 --- a/coqpyt/tests/resources/test_imports/.gitignore +++ b/coqpyt/tests/resources/test_imports/.gitignore @@ -2,4 +2,6 @@ *.vos *.vo *.glob -*.aux +.*.aux +Makefile.* +.Makefile.* diff --git a/coqpyt/tests/resources/test_imports/Makefile b/coqpyt/tests/resources/test_imports/Makefile index 7012dfb..a3e1bf3 100644 --- a/coqpyt/tests/resources/test_imports/Makefile +++ b/coqpyt/tests/resources/test_imports/Makefile @@ -1,981 +1,28 @@ -########################################################################## -## # The Coq Proof Assistant / The Coq Development Team ## -## v # Copyright INRIA, CNRS and contributors ## -## /dev/null 2>/dev/null; echo $$?)) -STDTIME?=command time -f $(TIMEFMT) -else -ifeq (0,$(shell gtime -f "" true >/dev/null 2>/dev/null; echo $$?)) -STDTIME?=gtime -f $(TIMEFMT) -else -STDTIME?=command time -endif -endif -else -STDTIME?=command time -f $(TIMEFMT) -endif - -COQBIN?= -ifneq (,$(COQBIN)) -# add an ending / -COQBIN:=$(COQBIN)/ -endif - -# Coq binaries -COQC ?= "$(COQBIN)coqc" -COQTOP ?= "$(COQBIN)coqtop" -COQCHK ?= "$(COQBIN)coqchk" -COQNATIVE ?= "$(COQBIN)coqnative" -COQDEP ?= "$(COQBIN)coqdep" -COQDOC ?= "$(COQBIN)coqdoc" -COQPP ?= "$(COQBIN)coqpp" -COQMKFILE ?= "$(COQBIN)coq_makefile" -OCAMLLIBDEP ?= "$(COQBIN)ocamllibdep" - -# Timing scripts -COQMAKE_ONE_TIME_FILE ?= "$(COQCORELIB)/tools/make-one-time-file.py" -COQMAKE_BOTH_TIME_FILES ?= "$(COQCORELIB)/tools/make-both-time-files.py" -COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQCORELIB)/tools/make-both-single-timing-files.py" -BEFORE ?= -AFTER ?= - -# OCaml binaries -CAMLC ?= "$(OCAMLFIND)" ocamlc -c -CAMLOPTC ?= "$(OCAMLFIND)" opt -c -CAMLLINK ?= "$(OCAMLFIND)" ocamlc -linkall -CAMLOPTLINK ?= "$(OCAMLFIND)" opt -linkall -CAMLDOC ?= "$(OCAMLFIND)" ocamldoc -CAMLDEP ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .mlpack - -# DESTDIR is prepended to all installation paths -DESTDIR ?= - -# Debug builds, typically -g to OCaml, -debug to Coq. -CAMLDEBUG ?= -COQDEBUG ?= - -# Extra packages to be linked in (as in findlib -package) -CAMLPKGS ?= -FINDLIBPKGS = -package coq-core.plugins.ltac $(CAMLPKGS) - -# Option for making timing files -TIMING?= -# Option for changing sorting of timing output file -TIMING_SORT_BY ?= auto -# Option for changing the fuzz parameter on the output file -TIMING_FUZZ ?= 0 -# Option for changing whether to use real or user time for timing tables -TIMING_REAL?= -# Option for including the memory column(s) -TIMING_INCLUDE_MEM?= -# Option for sorting by the memory column -TIMING_SORT_BY_MEM?= -# Output file names for timed builds -TIME_OF_BUILD_FILE ?= time-of-build.log -TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log -TIME_OF_BUILD_AFTER_FILE ?= time-of-build-after.log -TIME_OF_PRETTY_BUILD_FILE ?= time-of-build-pretty.log -TIME_OF_PRETTY_BOTH_BUILD_FILE ?= time-of-build-both.log -TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line - -TGTS ?= - -# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not) -ifdef DSTROOT -DESTDIR := $(DSTROOT) -endif - -# Substitution of the path by appending $(DESTDIR) if needed. -# The variable $(COQMF_WINDRIVE) can be needed for Cygwin environments. -windrive_path = $(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(1)),$(1)) -destination_path = $(if $(DESTDIR),$(DESTDIR)/$(call windrive_path,$(1)),$(1)) - -# Installation paths of libraries and documentation. -COQLIBINSTALL ?= $(call destination_path,$(COQLIB)/user-contrib) -COQDOCINSTALL ?= $(call destination_path,$(DOCDIR)/coq/user-contrib) -COQPLUGININSTALL ?= $(call destination_path,$(COQCORELIB)/..) -COQTOPINSTALL ?= $(call destination_path,$(COQLIB)/toploop) # FIXME: Unused variable? - -# findlib files installation -FINDLIBPREINST= mkdir -p "$(COQPLUGININSTALL)/" -FINDLIBDESTDIR= -destdir "$(COQPLUGININSTALL)/" - -# we need to move out of sight $(METAFILE) otherwise findlib thinks the -# package is already installed -findlib_install = \ - $(HIDE)if [ "$(METAFILE)" ]; then \ - $(FINDLIBPREINST) && \ - mv "$(METAFILE)" "$(METAFILE).skip" ; \ - "$(OCAMLFIND)" install $(2) $(FINDLIBDESTDIR) $(FINDLIBPACKAGE) $(1); \ - rc=$$?; \ - mv "$(METAFILE).skip" "$(METAFILE)"; \ - exit $$rc; \ - fi -findlib_remove = \ - $(HIDE)if [ ! -z "$(METAFILE)" ]; then\ - "$(OCAMLFIND)" remove $(FINDLIBDESTDIR) $(FINDLIBPACKAGE); \ - fi - - -########## End of parameters ################################################## -# What follows may be relevant to you only if you need to -# extend this Makefile. If so, look for 'Extension point' here and -# put in Makefile.local double colon rules accordingly. -# E.g. to perform some work after the all target completes you can write -# -# post-all:: -# echo "All done!" -# -# in Makefile.local -# -############################################################################### - - - - -# Flags ####################################################################### -# -# We define a bunch of variables combining the parameters. -# To add additional flags to coq, coqchk or coqdoc, set the -# {COQ,COQCHK,COQDOC}EXTRAFLAGS variable to whatever you want to add. -# To overwrite the default choice and set your own flags entirely, set the -# {COQ,COQCHK,COQDOC}FLAGS variable. - -SHOW := $(if $(VERBOSE),@true "",@echo "") -HIDE := $(if $(VERBOSE),,@) - -TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) - -OPT?= - -# The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d -ifeq '$(OPT)' '-byte' -USEBYTE:=true -DYNOBJ:=.cma -DYNLIB:=.cma -else -USEBYTE:= -DYNOBJ:=.cmxs -DYNLIB:=.cmxs -endif - -# these variables are meant to be overridden if you want to add *extra* flags -COQEXTRAFLAGS?= -COQCHKEXTRAFLAGS?= -COQDOCEXTRAFLAGS?= - -# Find the last argument of the form "-native-compiler FLAG" -COQUSERNATIVEFLAG:=$(strip \ -$(subst -native-compiler-,,\ -$(lastword \ -$(filter -native-compiler-%,\ -$(subst -native-compiler ,-native-compiler-,\ -$(strip $(COQEXTRAFLAGS))))))) - -COQFILTEREDEXTRAFLAGS:=$(strip \ -$(filter-out -native-compiler-%,\ -$(subst -native-compiler ,-native-compiler-,\ -$(strip $(COQEXTRAFLAGS))))) - -COQACTUALNATIVEFLAG:=$(lastword $(COQMF_COQ_NATIVE_COMPILER_DEFAULT) $(COQMF_COQPROJECTNATIVEFLAG) $(COQUSERNATIVEFLAG)) - -ifeq '$(COQACTUALNATIVEFLAG)' 'yes' - COQNATIVEFLAG="-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" - COQDONATIVE="yes" -else -ifeq '$(COQACTUALNATIVEFLAG)' 'ondemand' - COQNATIVEFLAG="-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" - COQDONATIVE="no" -else - COQNATIVEFLAG="-w" "-deprecated-native-compiler-option" "-native-compiler" "no" - COQDONATIVE="no" -endif -endif - -# these flags do NOT contain the libraries, to make them easier to overwrite -COQFLAGS?=-q $(OTHERFLAGS) $(COQFILTEREDEXTRAFLAGS) $(COQNATIVEFLAG) -COQCHKFLAGS?=-silent -o $(COQCHKEXTRAFLAGS) -COQDOCFLAGS?=-interpolate -utf8 $(COQDOCEXTRAFLAGS) - -COQDOCLIBS?=$(COQLIBS_NOML) - -# The version of Coq being run and the version of coq_makefile that -# generated this makefile -COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1) -COQMAKEFILE_VERSION:=8.17.0 - -# COQ_SRC_SUBDIRS is for user-overriding, usually to add -# `user-contrib/Foo` to the includes, we keep COQCORE_SRC_SUBDIRS for -# Coq's own core libraries, which should be replaced by ocamlfind -# options at some point. -COQ_SRC_SUBDIRS?= -COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)") - -CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -# ocamldoc fails with unknown argument otherwise -CAMLDOCFLAGS:=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) -CAMLFLAGS+=$(OCAMLWARN) - -ifneq (,$(TIMING)) -TIMING_ARG=-time -ifeq (after,$(TIMING)) -TIMING_EXT=after-timing -else -ifeq (before,$(TIMING)) -TIMING_EXT=before-timing -else -TIMING_EXT=timing -endif -endif -else -TIMING_ARG= -endif - -# Files ####################################################################### -# -# We here define a bunch of variables about the files being part of the -# Coq project in order to ease the writing of build target and build rules - -VDFILE := .Makefile.d - -ALLSRCFILES := \ - $(MLGFILES) \ - $(MLFILES) \ - $(MLPACKFILES) \ - $(MLLIBFILES) \ - $(MLIFILES) - -# helpers -vo_to_obj = $(addsuffix .o,\ - $(filter-out Warning: Error:,\ - $(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1)))) -strip_dotslash = $(patsubst ./%,%,$(1)) - -# without this we get undefined variables in the expansion for the -# targets of the [deprecated,use-mllib-or-mlpack] rule -with_undef = $(if $(filter-out undefined, $(origin $(1))),$($(1))) - -VO = vo -VOS = vos - -VOFILES = $(VFILES:.v=.$(VO)) -GLOBFILES = $(VFILES:.v=.glob) -HTMLFILES = $(VFILES:.v=.html) -GHTMLFILES = $(VFILES:.v=.g.html) -BEAUTYFILES = $(addsuffix .beautified,$(VFILES)) -TEXFILES = $(VFILES:.v=.tex) -GTEXFILES = $(VFILES:.v=.g.tex) -CMOFILES = \ - $(MLGFILES:.mlg=.cmo) \ - $(MLFILES:.ml=.cmo) \ - $(MLPACKFILES:.mlpack=.cmo) -CMXFILES = $(CMOFILES:.cmo=.cmx) -OFILES = $(CMXFILES:.cmx=.o) -CMAFILES = $(MLLIBFILES:.mllib=.cma) $(MLPACKFILES:.mlpack=.cma) -CMXAFILES = $(CMAFILES:.cma=.cmxa) -CMIFILES = \ - $(CMOFILES:.cmo=.cmi) \ - $(MLIFILES:.mli=.cmi) -# the /if/ is because old _CoqProject did not list a .ml(pack|lib) but just -# a .mlg file -CMXSFILES = \ - $(MLPACKFILES:.mlpack=.cmxs) \ - $(CMXAFILES:.cmxa=.cmxs) \ - $(if $(MLPACKFILES)$(CMXAFILES),,\ - $(MLGFILES:.mlg=.cmxs) $(MLFILES:.ml=.cmxs)) - -# files that are packed into a plugin (no extension) -PACKEDFILES = \ - $(call strip_dotslash, \ - $(foreach lib, \ - $(call strip_dotslash, \ - $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$(call with_undef,$(lib)))) -# files that are archived into a .cma (mllib) -LIBEDFILES = \ - $(call strip_dotslash, \ - $(foreach lib, \ - $(call strip_dotslash, \ - $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$(call with_undef,$(lib)))) -CMIFILESTOINSTALL = $(filter-out $(addsuffix .cmi,$(PACKEDFILES)),$(CMIFILES)) -CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES)) -OBJFILES = $(call vo_to_obj,$(VOFILES)) -ALLNATIVEFILES = \ - $(OBJFILES:.o=.cmi) \ - $(OBJFILES:.o=.cmx) \ - $(OBJFILES:.o=.cmxs) -FINDLIBPACKAGE=$(patsubst .%,%,$(suffix $(METAFILE))) - -# trick: wildcard filters out non-existing files, so that `install` doesn't show -# warnings and `clean` doesn't pass to rm a list of files that is too long for -# the shell. -NATIVEFILES = $(wildcard $(ALLNATIVEFILES)) -FILESTOINSTALL = \ - $(VOFILES) \ - $(VFILES) \ - $(GLOBFILES) \ - $(NATIVEFILES) \ - $(CMXSFILES) # to be removed when we remove legacy loading -FINDLIBFILESTOINSTALL = \ - $(CMIFILESTOINSTALL) -ifeq '$(HASNATDYNLINK)' 'true' -DO_NATDYNLINK = yes -FINDLIBFILESTOINSTALL += $(CMXSFILES) $(CMXAFILES) $(CMOFILESTOINSTALL:.cmo=.cmx) -else -DO_NATDYNLINK = -endif - -ALLDFILES = $(addsuffix .d,$(ALLSRCFILES)) $(VDFILE) - -# Compilation targets ######################################################### - -all: - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all +# Default target +all: Makefile.coq + +@$(MAKE) -f Makefile.coq all .PHONY: all -all.timing.diff: - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all.timing.diff TIME_OF_PRETTY_BUILD_EXTRA_FILES="" - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all -.PHONY: all.timing.diff - -ifeq (0,$(TIMING_REAL)) -TIMING_REAL_ARG := -TIMING_USER_ARG := --user -else -ifeq (1,$(TIMING_REAL)) -TIMING_REAL_ARG := --real -TIMING_USER_ARG := -else -TIMING_REAL_ARG := -TIMING_USER_ARG := -endif -endif - -ifeq (0,$(TIMING_INCLUDE_MEM)) -TIMING_INCLUDE_MEM_ARG := --no-include-mem -else -TIMING_INCLUDE_MEM_ARG := -endif - -ifeq (1,$(TIMING_SORT_BY_MEM)) -TIMING_SORT_BY_MEM_ARG := --sort-by-mem -else -TIMING_SORT_BY_MEM_ARG := -endif - -make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE) -make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE) -make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: - $(HIDE)rm -f pretty-timed-success.ok - $(HIDE)($(MAKE) --no-print-directory -f "$(PARENT)" $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE) - $(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed -print-pretty-timed:: - $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) -print-pretty-timed-diff:: - $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) -ifeq (,$(BEFORE)) -print-pretty-single-time-diff:: - @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' - $(HIDE)false -else -ifeq (,$(AFTER)) -print-pretty-single-time-diff:: - @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' - $(HIDE)false -else -print-pretty-single-time-diff:: - $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --fuzz=$(TIMING_FUZZ) --sort-by=$(TIMING_SORT_BY) $(TIMING_USER_ARG) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) -endif -endif -pretty-timed: - $(HIDE)$(MAKE) --no-print-directory -f "$(PARENT)" make-pretty-timed - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-timed -.PHONY: pretty-timed make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff - -# Extension points for actions to be performed before/after the all target -pre-all:: - @# Extension point - $(HIDE)if [ "$(COQMAKEFILE_VERSION)" != "$(COQ_VERSION)" ]; then\ - echo "W: This Makefile was generated by Coq $(COQMAKEFILE_VERSION)";\ - echo "W: while the current Coq version is $(COQ_VERSION)";\ - fi -.PHONY: pre-all - -post-all:: - @# Extension point -.PHONY: post-all - -real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles) -.PHONY: real-all - -real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff) -.PHONY: real-all.timing.diff - -bytefiles: $(CMOFILES) $(CMAFILES) -.PHONY: bytefiles - -optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) -.PHONY: optfiles - -# FIXME, see Ralf's bugreport -# quick is deprecated, now renamed vio -vio: $(VOFILES:.vo=.vio) -.PHONY: vio -quick: vio - $(warning "'make quick' is deprecated, use 'make vio' or consider using 'vos' files") -.PHONY: quick - -vio2vo: - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \ - -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) -.PHONY: vio2vo - -# quick2vo is undocumented -quick2vo: - $(HIDE)make -j $(J) vio - $(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \ - viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \ - if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \ - done); \ - echo "VIO2VO: $$VIOFILES"; \ - if [ -n "$$VIOFILES" ]; then \ - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -schedule-vio2vo $(J) $$VIOFILES; \ - fi -.PHONY: quick2vo - -checkproofs: - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \ - -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) -.PHONY: checkproofs - -vos: $(VOFILES:%.vo=%.vos) -.PHONY: vos - -vok: $(VOFILES:%.vo=%.vok) -.PHONY: vok - -validate: $(VOFILES) - $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS_NOML) $^ -.PHONY: validate - -only: $(TGTS) -.PHONY: only - -# Documentation targets ####################################################### - -html: $(GLOBFILES) $(VFILES) - $(SHOW)'COQDOC -d html $(GAL)' - $(HIDE)mkdir -p html - $(HIDE)$(COQDOC) \ - -toc $(COQDOCFLAGS) -html $(GAL) $(COQDOCLIBS) -d html $(VFILES) - -mlihtml: $(MLIFILES:.mli=.cmi) - $(SHOW)'CAMLDOC -d $@' - $(HIDE)mkdir $@ || rm -rf $@/* - $(HIDE)$(CAMLDOC) -html \ - -d $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) $(FINDLIBPKGS) - -all-mli.tex: $(MLIFILES:.mli=.cmi) - $(SHOW)'CAMLDOC -latex $@' - $(HIDE)$(CAMLDOC) -latex \ - -o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) $(FINDLIBPKGS) - -all.ps: $(VFILES) - $(SHOW)'COQDOC -ps $(GAL)' - $(HIDE)$(COQDOC) \ - -toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \ - -o $@ `$(COQDEP) -sort $(VFILES)` - -all.pdf: $(VFILES) - $(SHOW)'COQDOC -pdf $(GAL)' - $(HIDE)$(COQDOC) \ - -toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \ - -o $@ `$(COQDEP) -sort $(VFILES)` - -# FIXME: not quite right, since the output name is different -gallinahtml: GAL=-g -gallinahtml: html - -all-gal.ps: GAL=-g -all-gal.ps: all.ps - -all-gal.pdf: GAL=-g -all-gal.pdf: all.pdf - -# ? -beautify: $(BEAUTYFILES) - for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done - @echo 'Do not do "make clean" until you are sure that everything went well!' - @echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/' -.PHONY: beautify - -# Installation targets ######################################################## -# -# There rules can be extended in Makefile.local -# Extensions can't assume when they run. - -# findlib needs the package to not be installed, so we remove it before -# installing it (see the call to findlib_remove) -install: META - $(HIDE)code=0; for f in $(FILESTOINSTALL); do\ - if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \ - done; exit $$code - $(HIDE)for f in $(FILESTOINSTALL); do\ - df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ - if [ "$$?" != "0" -o -z "$$df" ]; then\ - echo SKIP "$$f" since it has no logical path;\ - else\ - install -d "$(COQLIBINSTALL)/$$df" &&\ - install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\ - echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\ - fi;\ - done - $(call findlib_remove) - $(call findlib_install, META $(FINDLIBFILESTOINSTALL)) - $(HIDE)$(MAKE) install-extra -f "$(SELF)" -install-extra:: - @# Extension point -.PHONY: install install-extra - -META: $(METAFILE) - $(HIDE)if [ "$(METAFILE)" ]; then \ - cat "$(METAFILE)" | grep -v 'directory.*=.*' > META; \ - fi - -install-byte: - $(call findlib_install, $(CMAFILES) $(CMOFILESTOINSTALL), -add) - -install-doc:: html mlihtml - @# Extension point - $(HIDE)install -d "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" - $(HIDE)for i in html/*; do \ - dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ - install -m 0644 "$$i" "$$dest";\ - echo INSTALL "$$i" "$$dest";\ - done - $(HIDE)install -d \ - "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" - $(HIDE)for i in mlihtml/*; do \ - dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ - install -m 0644 "$$i" "$$dest";\ - echo INSTALL "$$i" "$$dest";\ - done -.PHONY: install-doc - -uninstall:: - @# Extension point - $(call findlib_remove) - $(HIDE)for f in $(FILESTOINSTALL); do \ - df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ - instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ - rm -f "$$instf" &&\ - echo RM "$$instf" ;\ - done - $(HIDE)for f in $(FILESTOINSTALL); do \ - df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ - echo RMDIR "$(COQLIBINSTALL)/$$df/" &&\ - (rmdir "$(COQLIBINSTALL)/$$df/" 2>/dev/null || true); \ - done - -.PHONY: uninstall - -uninstall-doc:: - @# Extension point - $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html' - $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" - $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml' - $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" - $(HIDE) rmdir "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true -.PHONY: uninstall-doc - -# Cleaning #################################################################### -# -# There rules can be extended in Makefile.local -# Extensions can't assume when they run. +# Permit local customization +-include Makefile.local -clean:: - @# Extension point - $(SHOW)'CLEAN' - $(HIDE)rm -f $(CMOFILES) - $(HIDE)rm -f $(CMIFILES) - $(HIDE)rm -f $(CMAFILES) - $(HIDE)rm -f $(CMXFILES) - $(HIDE)rm -f $(CMXAFILES) - $(HIDE)rm -f $(CMXSFILES) - $(HIDE)rm -f $(OFILES) - $(HIDE)rm -f $(CMXAFILES:.cmxa=.a) - $(HIDE)rm -f $(MLGFILES:.mlg=.ml) - $(HIDE)rm -f $(CMXFILES:.cmx=.cmt) - $(HIDE)rm -f $(MLIFILES:.mli=.cmti) - $(HIDE)rm -f $(ALLDFILES) - $(HIDE)rm -f $(NATIVEFILES) - $(HIDE)find . -name .coq-native -type d -empty -delete - $(HIDE)rm -f $(VOFILES) - $(HIDE)rm -f $(VOFILES:.vo=.vio) - $(HIDE)rm -f $(VOFILES:.vo=.vos) - $(HIDE)rm -f $(VOFILES:.vo=.vok) - $(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old) - $(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex - $(HIDE)rm -f $(VFILES:.v=.glob) - $(HIDE)rm -f $(VFILES:.v=.tex) - $(HIDE)rm -f $(VFILES:.v=.g.tex) - $(HIDE)rm -f pretty-timed-success.ok - $(HIDE)rm -f META - $(HIDE)rm -rf html mlihtml +# Forward most targets to Coq makefile (with some trick to make this phony) +%: Makefile.coq phony + @#echo "Forwarding $@" + +@$(MAKE) -f Makefile.coq $@ +phony: ; +.PHONY: phony + +clean: Makefile.coq + +@$(MAKE) -f Makefile.coq clean + @# Make sure not to enter the `_opam` folder. + rm .*.aux Makefile.* .PHONY: clean -cleanall:: clean - @# Extension point - $(SHOW)'CLEAN *.aux *.timing' - $(HIDE)rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux) - $(HIDE)rm -f $(TIME_OF_BUILD_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) - $(HIDE)rm -f $(VOFILES:.vo=.v.timing) - $(HIDE)rm -f $(VOFILES:.vo=.v.before-timing) - $(HIDE)rm -f $(VOFILES:.vo=.v.after-timing) - $(HIDE)rm -f $(VOFILES:.vo=.v.timing.diff) - $(HIDE)rm -f .lia.cache .nia.cache -.PHONY: cleanall - -archclean:: - @# Extension point - $(SHOW)'CLEAN *.cmx *.o' - $(HIDE)rm -f $(NATIVEFILES) - $(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx) -.PHONY: archclean - - -# Compilation rules ########################################################### - -$(MLIFILES:.mli=.cmi): %.cmi: %.mli - $(SHOW)'CAMLC -c $<' - $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $< - -$(MLGFILES:.mlg=.ml): %.ml: %.mlg - $(SHOW)'COQPP $<' - $(HIDE)$(COQPP) $< - -# Stupid hack around a deficient syntax: we cannot concatenate two expansions -$(filter %.cmo, $(MLFILES:.ml=.cmo) $(MLGFILES:.mlg=.cmo)): %.cmo: %.ml - $(SHOW)'CAMLC -c $<' - $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $< - -# Same hack -$(filter %.cmx, $(MLFILES:.ml=.cmx) $(MLGFILES:.mlg=.cmx)): %.cmx: %.ml - $(SHOW)'CAMLOPT -c $(FOR_PACK) $<' - $(HIDE)$(TIMER) $(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $(FOR_PACK) $< - - -$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa - $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \ - -shared -o $@ $< - -$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib - $(SHOW)'CAMLC -a -o $@' - $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^ - -$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib - $(SHOW)'CAMLOPT -a -o $@' - $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^ - - -$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa - $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \ - -shared -o $@ $< - -$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx | %.mlpack - $(SHOW)'CAMLOPT -a -o $@' - $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $< - -$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack - $(SHOW)'CAMLC -a -o $@' - $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^ - -$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack - $(SHOW)'CAMLC -pack -o $@' - $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -pack -o $@ $^ - -$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack - $(SHOW)'CAMLOPT -pack -o $@' - $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -pack -o $@ $^ - -# This rule is for _CoqProject with no .mllib nor .mlpack -$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx - $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' - $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \ - -shared -o $@ $< - -ifneq (,$(TIMING)) -TIMING_EXTRA = > $<.$(TIMING_EXT) -else -TIMING_EXTRA = -endif - -# can't make -# https://www.gnu.org/software/make/manual/make.html#Static-Pattern -# work with multiple target rules -# so use eval in a loop instead -# with grouped targets https://www.gnu.org/software/make/manual/make.html#Multiple-Targets -# if available (GNU Make >= 4.3) -ifneq (,$(filter grouped-target,$(.FEATURES))) -define globvorule= - -# take care to $$ variables using $< etc - $(1).vo $(1).glob &: $(1).v | $(VDFILE) - $(SHOW)COQC $(1).v - $(HIDE)$$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $(1).v $$(TIMING_EXTRA) -ifeq ($(COQDONATIVE), "yes") - $(SHOW)COQNATIVE $(1).vo - $(HIDE)$(call TIMER,$(1).vo.native) $(COQNATIVE) $(COQLIBS) $(1).vo -endif - -endef -else - -$(VOFILES): %.vo: %.v | $(VDFILE) - $(SHOW)COQC $< - $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< $(TIMING_EXTRA) -ifeq ($(COQDONATIVE), "yes") - $(SHOW)COQNATIVE $@ - $(HIDE)$(call TIMER,$@.native) $(COQNATIVE) $(COQLIBS) $@ -endif - -# this is broken :( todo fix if we ever find a solution that doesn't need grouped targets -$(GLOBFILES): %.glob: %.v - $(SHOW)'COQC $< (for .glob)' - $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< - -endif - -$(foreach vfile,$(VFILES:.v=),$(eval $(call globvorule,$(vfile)))) - -$(VFILES:.v=.vio): %.vio: %.v - $(SHOW)COQC -vio $< - $(HIDE)$(TIMER) $(COQC) -vio $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< - -$(VFILES:.v=.vos): %.vos: %.v - $(SHOW)COQC -vos $< - $(HIDE)$(TIMER) $(COQC) -vos $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< - -$(VFILES:.v=.vok): %.vok: %.v - $(SHOW)COQC -vok $< - $(HIDE)$(TIMER) $(COQC) -vok $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< - -$(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing - $(SHOW)PYTHON TIMING-DIFF $*.{before,after}-timing - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" - -$(BEAUTYFILES): %.v.beautified: %.v - $(SHOW)'BEAUTIFY $<' - $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -beautify $< - -$(TEXFILES): %.tex: %.v - $(SHOW)'COQDOC -latex $<' - $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ - -$(GTEXFILES): %.g.tex: %.v - $(SHOW)'COQDOC -latex -g $<' - $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@ - -$(HTMLFILES): %.html: %.v %.glob - $(SHOW)'COQDOC -html $<' - $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html $< -o $@ - -$(GHTMLFILES): %.g.html: %.v %.glob - $(SHOW)'COQDOC -html -g $<' - $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@ - -# Dependency files ############################################################ - -ifndef MAKECMDGOALS - -include $(ALLDFILES) -else - ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),) - -include $(ALLDFILES) - endif -endif - -.SECONDARY: $(ALLDFILES) - -redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV ) - -GENMLFILES:=$(MLGFILES:.mlg=.ml) -$(addsuffix .d,$(ALLSRCFILES)): $(GENMLFILES) - -$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli - $(SHOW)'CAMLDEP $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) - -$(addsuffix .d,$(MLGFILES)): %.mlg.d: %.ml - $(SHOW)'CAMLDEP $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) - -$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml - $(SHOW)'CAMLDEP $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) - -$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib - $(SHOW)'OCAMLLIBDEP $<' - $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) - -$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack - $(SHOW)'OCAMLLIBDEP $<' - $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) - -# If this makefile is created using a _CoqProject we have coqdep get -# options from it. This avoids argument length limits for pathological -# projects. Note that extra options might be on the command line. -VDFILE_FLAGS:=$(if _CoqProject,-f _CoqProject,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES) - -$(VDFILE): _CoqProject $(VFILES) - $(SHOW)'COQDEP VFILES' - $(HIDE)$(COQDEP) $(if $(strip $(METAFILE)),-m "$(METAFILE)") -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok) - -# Misc ######################################################################## - -byte: - $(HIDE)$(MAKE) all "OPT:=-byte" -f "$(SELF)" -.PHONY: byte - -opt: - $(HIDE)$(MAKE) all "OPT:=-opt" -f "$(SELF)" -.PHONY: opt - -# This is deprecated. To extend this makefile use -# extension points and Makefile.local -printenv:: - $(warning printenv is deprecated) - $(warning write extensions in Makefile.local or include Makefile.conf) - @echo 'COQLIB = $(COQLIB)' - @echo 'COQCORELIB = $(COQCORELIB)' - @echo 'DOCDIR = $(DOCDIR)' - @echo 'OCAMLFIND = $(OCAMLFIND)' - @echo 'HASNATDYNLINK = $(HASNATDYNLINK)' - @echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)' - @echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)' - @echo 'COQCORE_SRC_SUBDIRS = $(COQCORE_SRC_SUBDIRS)' - @echo 'OCAMLFIND = $(OCAMLFIND)' - @echo 'PP = $(PP)' - @echo 'COQFLAGS = $(COQFLAGS)' - @echo 'COQLIB = $(COQLIBS)' - @echo 'COQLIBINSTALL = $(COQLIBINSTALL)' - @echo 'COQDOCINSTALL = $(COQDOCINSTALL)' -.PHONY: printenv - -# Generate a .merlin file. If you need to append directives to this -# file you can extend the merlin-hook target in Makefile.local -.merlin: - $(SHOW)'FILL .merlin' - $(HIDE)echo 'FLG $(COQMF_CAMLFLAGS)' > .merlin - $(HIDE)echo 'B $(COQCORELIB)' >> .merlin - $(HIDE)echo 'S $(COQCORELIB)' >> .merlin - $(HIDE)$(foreach d,$(COQCORE_SRC_SUBDIRS), \ - echo 'B $(COQCORELIB)$(d)' >> .merlin;) - $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ - echo 'S $(COQLIB)$(d)' >> .merlin;) - $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'B $(d)' >> .merlin;) - $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'S $(d)' >> .merlin;) - $(HIDE)$(MAKE) merlin-hook -f "$(SELF)" -.PHONY: merlin - -merlin-hook:: - @# Extension point -.PHONY: merlin-hook - -# prints all variables -debug: - $(foreach v,\ - $(sort $(filter-out $(INITIAL_VARS) INITIAL_VARS,\ - $(.VARIABLES))),\ - $(info $(v) = $($(v)))) -.PHONY: debug - -.DEFAULT_GOAL := all - -# Users can create Makefile.local-late to hook into double-colon rules -# or add other needed Makefile code, using defined -# variables if necessary. --include Makefile.local-late +# Create Coq Makefile. +Makefile.coq: _CoqProject Makefile + "$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES) -# Local Variables: -# mode: makefile-gmake -# End: +# Some files that do *not* need to be forwarded to Makefile.coq. +# ("::" lets Makefile.local overwrite this.) +Makefile Makefile.local _CoqProject $(OPAMFILES):: ; \ No newline at end of file diff --git a/coqpyt/tests/resources/test_imports/Makefile.conf b/coqpyt/tests/resources/test_imports/Makefile.conf deleted file mode 100644 index 666b8e3..0000000 --- a/coqpyt/tests/resources/test_imports/Makefile.conf +++ /dev/null @@ -1,71 +0,0 @@ -# This configuration file was generated by running: -# coq_makefile -f _CoqProject -o Makefile - -COQBIN?= -ifneq (,$(COQBIN)) -# add an ending / -COQBIN:=$(COQBIN)/ -endif -COQMKFILE ?= "$(COQBIN)coq_makefile" - -############################################################################### -# # -# Project files. # -# # -############################################################################### - -COQMF_CMDLINE_VFILES := -COQMF_SOURCES := $(shell $(COQMKFILE) -sources-of -f _CoqProject $(COQMF_CMDLINE_VFILES)) -COQMF_VFILES := $(filter %.v, $(COQMF_SOURCES)) -COQMF_MLIFILES := $(filter %.mli, $(COQMF_SOURCES)) -COQMF_MLFILES := $(filter %.ml, $(COQMF_SOURCES)) -COQMF_MLGFILES := $(filter %.mlg, $(COQMF_SOURCES)) -COQMF_MLPACKFILES := $(filter %.mlpack, $(COQMF_SOURCES)) -COQMF_MLLIBFILES := $(filter %.mllib, $(COQMF_SOURCES)) -COQMF_METAFILE = - -############################################################################### -# # -# Path directives (-I, -R, -Q). # -# # -############################################################################### - -COQMF_OCAMLLIBS = -COQMF_SRC_SUBDIRS = -COQMF_COQLIBS = -R . TestImport -COQMF_COQLIBS_NOML = -R . TestImport -COQMF_CMDLINE_COQLIBS = - -############################################################################### -# # -# Coq configuration. # -# # -############################################################################### - -COQMF_COQLIB=/home/nfsaavedra/.opam/default/lib/coq/ -COQMF_COQCORELIB=/home/nfsaavedra/.opam/default/lib/coq/../coq-core/ -COQMF_DOCDIR=/home/nfsaavedra/.opam/default/share/doc/ -COQMF_OCAMLFIND=/home/nfsaavedra/.opam/default/bin/ocamlfind -COQMF_CAMLFLAGS=-thread -rectypes -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -COQMF_WARN=-warn-error +a-3 -COQMF_HASNATDYNLINK=true -COQMF_COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax -COQMF_COQ_NATIVE_COMPILER_DEFAULT=no -COQMF_WINDRIVE= - -############################################################################### -# # -# Native compiler. # -# # -############################################################################### - -COQMF_COQPROJECTNATIVEFLAG = - -############################################################################### -# # -# Extra variables. # -# # -############################################################################### - -COQMF_OTHERFLAGS = -COQMF_INSTALLCOQDOCROOT = TestImport From a4bb4a266b3d092204e5f3067b8323b335b713a8 Mon Sep 17 00:00:00 2001 From: pcarrott Date: Fri, 10 Nov 2023 22:39:55 +0000 Subject: [PATCH 17/28] Merge changes from master --- coqpyt/coq/base_file.py | 29 ++++++++++++++------- coqpyt/coq/proof_file.py | 21 +++++---------- coqpyt/tests/resources/test_proof_cmd.v | 26 ++++++++++++++++++ coqpyt/tests/resources/test_section_terms.v | 4 +++ coqpyt/tests/test_proof_file.py | 25 ++++++++++++++++++ 5 files changed, 82 insertions(+), 23 deletions(-) create mode 100644 coqpyt/tests/resources/test_proof_cmd.v create mode 100644 coqpyt/tests/resources/test_section_terms.v diff --git a/coqpyt/coq/base_file.py b/coqpyt/coq/base_file.py index ed18422..8ea48dc 100644 --- a/coqpyt/coq/base_file.py +++ b/coqpyt/coq/base_file.py @@ -88,6 +88,7 @@ def __init__( self.version = 1 self.__last_end_pos: Optional[Position] = None self.__current_goals = None + self._last_term: Optional[Term] = None def __enter__(self): return self @@ -253,6 +254,7 @@ def __short_text( def __add_term(self, name: str, step: Step, term_type: TermType): term = Term(step, term_type, self.path, self.curr_module[:]) + self._last_term = term if term.type == TermType.NOTATION: self.context.update(terms={name: term}) return @@ -390,11 +392,20 @@ def traverse_expr(expr): # - names should be removed from the context # - curr_module should change as you leave or re-enter modules + expr = self.expr(self.curr_step.ast) + if ( + expr == [None] + or expr[0] == "VernacProof" + or (expr[0] == "VernacExtend" and expr[1][0] == "VernacSolve") + ): + return + term_type = CoqFile.__get_term_type(expr) text = self.curr_step.short_text - # FIXME Let (and maybe Variable) should be handled. However, - # I think we can't handle them as normal Locals since they are - # specific to a section. + # FIXME: Section-local terms are ignored. We do this to avoid + # overwriting global terms with section-local terms after the section + # is closed. Regardless, these should be handled given that they might + # be used within the section. for keyword in [ "Variable", "Let", @@ -403,13 +414,13 @@ def traverse_expr(expr): "Hypotheses", ]: if text.startswith(keyword): + # NOTE: We update the last term so as to obtain proofs even for + # section-local terms. This is safe, because the attribute is + # meant to be overwritten every time a new term is found. + self._last_term = Term( + self.curr_step, term_type, self.path, self.curr_module[:] + ) return - expr = self.expr(self.curr_step.ast) - if expr == [None]: - return - if expr[0] == "VernacExtend" and expr[1][0] == "VernacSolve": - return - term_type = CoqFile.__get_term_type(expr) if expr[0] == "VernacEndSegment": if len(self.__segment_stack) == 0: diff --git a/coqpyt/coq/proof_file.py b/coqpyt/coq/proof_file.py index f5e3ac0..f2cf75d 100644 --- a/coqpyt/coq/proof_file.py +++ b/coqpyt/coq/proof_file.py @@ -175,9 +175,12 @@ def get_context(file_path: str, timeout: int): _AuxFile.__CACHE[(v_file, hash)] = aux_context coq_file.close() - # FIXME: we ignore the usage of Local from imported files to + # FIXME: we ignore the usage of "Local" from imported files to # simplify the implementation. However, they can be used: # https://coq.inria.fr/refman/language/core/modules.html?highlight=local#coq:attr.local + # NOTE: We handle "Local" separately from section-local keywords + # due to the aforementioned reason. The handling should be different + # for both types of keywords. for term in list(aux_context.terms.keys()): if aux_context.terms[term].text.startswith("Local"): aux_context.terms.pop(term) @@ -287,16 +290,6 @@ def __search_notation(call): return traverse_expr(self.expr(step.ast)) - def __get_last_term(self): - terms = self.terms - if len(terms) == 0: - return None - last_term = terms[0] - for term in terms[1:]: - if last_term.ast.range.end < term.ast.range.end: - last_term = term - return last_term - def __get_program_context(self): def traverse_expr(expr): stack = expr[:0:-1] @@ -332,7 +325,7 @@ def traverse_expr(expr): # same module as the program id = ".".join(self.curr_module + [id]) return self.__program_context[id] - text = self.__get_last_term().text + text = self._last_term.text raise RuntimeError(f"Unknown obligation command with tag number {tag}: {text}") def __check_program(self): @@ -343,7 +336,7 @@ def __check_program(self): if id in self.__program_context: return self.__program_context[id] = ( - self.__get_last_term(), + self._last_term, self.__step_context(self.prev_step), ) @@ -394,7 +387,7 @@ def __get_proof(self, proofs): if self.get_term_type(self.prev_step.ast) == TermType.OBLIGATION: term, statement_context = self.__get_program_context() elif self.get_term_type(self.prev_step.ast) != TermType.OTHER: - term = self.__get_last_term() + term = self._last_term statement_context = self.__step_context(self.prev_step) # HACK: We ignore proofs inside a Module Type since they can't be used outside # and should be overriden. diff --git a/coqpyt/tests/resources/test_proof_cmd.v b/coqpyt/tests/resources/test_proof_cmd.v new file mode 100644 index 0000000..fcdc5a0 --- /dev/null +++ b/coqpyt/tests/resources/test_proof_cmd.v @@ -0,0 +1,26 @@ +Require Import Coq.Unicode.Utf8. + +Section Random. + Variable (n : nat) (Hn : n <> 0). + + Definition x := 1. + + Goal ∃ (m : nat), + S m = n. + Proof using Hn. + destruct n. + + exfalso. auto. + + eexists. auto. + Defined. + + Goal ∃ (m : nat), + S m = n. + Proof with auto. + destruct n. + + exfalso... + + eexists... + Qed. + + Goal nat. + Proof 0. +End Random. \ No newline at end of file diff --git a/coqpyt/tests/resources/test_section_terms.v b/coqpyt/tests/resources/test_section_terms.v new file mode 100644 index 0000000..a554846 --- /dev/null +++ b/coqpyt/tests/resources/test_section_terms.v @@ -0,0 +1,4 @@ +Section Random. + Let ignored : nat. + Proof. exact 0. Defined. +End Random. \ No newline at end of file diff --git a/coqpyt/tests/test_proof_file.py b/coqpyt/tests/test_proof_file.py index de179d2..1c4e296 100644 --- a/coqpyt/tests/test_proof_file.py +++ b/coqpyt/tests/test_proof_file.py @@ -1042,3 +1042,28 @@ def test_simple_file_changes(setup, teardown): assert state.proofs[0].steps[0].text == steps[1] assert state.proofs[1].text == steps[2].strip() assert state.proofs[1].steps[0].text == steps[3] + + +@pytest.mark.parametrize("setup", [("test_proof_cmd.v", None)], indirect=True) +def test_proof_cmd(setup, teardown): + assert len(state.proofs) == 3 + goals = [ + "Goal ∃ (m : nat), S m = n.", + "Goal ∃ (m : nat), S m = n.", + "Goal nat.", + ] + proofs = [ + "\n Proof using Hn.", + "\n Proof with auto.", + "\n Proof 0.", + ] + for i, proof in enumerate(state.proofs): + assert proof.text == goals[i] + assert proof.steps[0].text == proofs[i] + + +@pytest.mark.parametrize("setup", [("test_section_terms.v", None)], indirect=True) +def test_section_terms(setup, teardown): + assert len(state.proofs) == 1 + assert state.proofs[0].text == "Let ignored : nat." + assert len(state.terms) == 0 From 12e8a2f090afddc890bab9b1a340b59049bf3417 Mon Sep 17 00:00:00 2001 From: pcarrott Date: Fri, 10 Nov 2023 23:12:48 +0000 Subject: [PATCH 18/28] Fetch context immediately and call didChange instead of calling didOpen at the end --- coqpyt/coq/proof_file.py | 79 ++++++++++++++-------------------------- 1 file changed, 27 insertions(+), 52 deletions(-) diff --git a/coqpyt/coq/proof_file.py b/coqpyt/coq/proof_file.py index f2cf75d..e090d7f 100644 --- a/coqpyt/coq/proof_file.py +++ b/coqpyt/coq/proof_file.py @@ -221,12 +221,13 @@ def __init__( """ super().__init__(file_path, library, timeout, workspace, coq_lsp, coqtop) self.__aux_file = _AuxFile(timeout=self.timeout) + self.__aux_file.didOpen() try: # We need to update the context already defined in the CoqFile self.context.update(_AuxFile.get_context(self.path, self.timeout).terms) - self.__program_context: Dict[str, Tuple[Term, List]] = {} - self.__proofs = self.__get_proofs() + self.__program_context: Dict[str, Tuple[Term, List[Term]]] = {} + self.__proofs: List[ProofTerm] = self.__get_proofs() except Exception as e: self.close() raise e @@ -251,32 +252,30 @@ def __locate(self, search, line): fun = lambda x: x.endswith("(default interpretation)") return nots[0][:-25] if fun(nots[0]) else nots[0] - def __step_context(self, step: Step): + def __step_context(self, step: Step) -> List[Term]: def traverse_expr(expr): stack, res = expr[:0:-1], [] while len(stack) > 0: el = stack.pop() if isinstance(el, list) and len(el) == 3 and el[0] == "Ser_Qualid": term = self.__get_term(CoqFile.get_id(el)) - if term is not None: - res.append((lambda x: x, term)) + if term is not None and term not in res: + res.append(term) elif isinstance(el, list) and len(el) == 4 and el[0] == "CNotation": line = len(self.__aux_file.read().split("\n")) self.__aux_file.append(f'\nLocate "{el[2][1]}".') + self.__aux_file.didChange() + + notation_name, scope = el[2][1], "" + notation = self.__locate(notation_name, line) + if notation.split(":")[-1].endswith("_scope"): + scope = notation.split(":")[-1].strip() + + if notation != "Unknown notation": + term = self.context.get_notation(notation_name, scope) + if term not in res: + res.append(term) - def __search_notation(call): - notation_name = call[0] - scope = "" - notation = call[1](*call[2:]) - if notation == "Unknown notation": - return None - if notation.split(":")[-1].endswith("_scope"): - scope = notation.split(":")[-1].strip() - return self.context.get_notation(notation_name, scope) - - res.append( - (__search_notation, (el[2][1], self.__locate, el[2][1], line)) - ) stack.append(el[1:]) elif isinstance(el, list): for v in reversed(el): @@ -290,7 +289,7 @@ def __search_notation(call): return traverse_expr(self.expr(step.ast)) - def __get_program_context(self): + def __get_program_context(self) -> Tuple[Term, List[Term]]: def traverse_expr(expr): stack = expr[:0:-1] while len(stack) > 0: @@ -345,9 +344,7 @@ def __step(self): self.__aux_file.append(self.prev_step.text) self.__check_program() - def __get_steps( - self, proofs - ) -> List[Tuple[Step, Optional[GoalAnswer], List[Tuple]]]: + def __get_steps(self, proofs: List[ProofTerm]) -> List[ProofStep]: steps = [] while self.in_proof and not self.checked: try: @@ -364,10 +361,10 @@ def __get_steps( while not self.in_proof and not self.checked: self.__step() continue - context_calls = self.__step_context(self.prev_step) + context = self.__step_context(self.prev_step) if self.prev_step.text.strip() == "": continue - steps.append((self.prev_step, goals, context_calls)) + steps.append(ProofStep(self.prev_step, goals, context)) try: goals = self.current_goals @@ -378,11 +375,11 @@ def __get_steps( self.steps_taken < len(self.steps) and self.expr(self.curr_step.ast)[0] == "VernacEndProof" ): - steps.append((self.curr_step, goals, [])) + steps.append(ProofStep(self.curr_step, goals, [])) return steps - def __get_proof(self, proofs): + def __get_proof(self, proofs: List[ProofTerm]): term, statement_context = None, None if self.get_term_type(self.prev_step.ast) == TermType.OBLIGATION: term, statement_context = self.__get_program_context() @@ -393,36 +390,15 @@ def __get_proof(self, proofs): # and should be overriden. if self.in_proof and len(self.curr_module_type) == 0: steps = self.__get_steps(proofs) - proofs.append((term, statement_context, steps)) - - def __call_context(self, calls: List[Tuple]): - context, calls = [], [call[0](*call[1:]) for call in calls] - [context.append(call) for call in calls if call not in context] - return list(filter(lambda term: term is not None, context)) + proofs.append(ProofTerm(term, statement_context, steps)) def __get_proofs(self) -> List[ProofTerm]: - def get_proof_step(step: Tuple[Step, Optional[GoalAnswer], List[Tuple]]): - return ProofStep(step[0], step[1], self.__call_context(step[2])) - - proofs: List[ - Tuple[Term, List[Tuple[Step, Optional[GoalAnswer], List[Tuple]]]] - ] = [] + proofs: List[ProofTerm] = [] while not self.checked: self.__step() # Get context from initial statement self.__get_proof(proofs) - - try: - self.__aux_file.didOpen() - except Exception as e: - self.close() - raise e - - proof_steps = [ - (term, self.__call_context(calls), list(map(get_proof_step, steps))) - for term, calls, steps in proofs - ] - return list(map(lambda t: ProofTerm(*t), proof_steps)) + return proofs def __find_step(self, range: Range) -> Optional[Tuple[ProofTerm, int]]: for proof in self.proofs: @@ -449,10 +425,9 @@ def __get_step(self, step_index): self.__aux_file.write("") for step in self.steps[: step_index + 1]: self.__aux_file.append(step.text) - call = self.__step_context(self.steps[step_index]) self.__aux_file.didChange() + context = self.__step_context(self.steps[step_index]) - context = self.__call_context(call) # The goals will be loaded if used (Lazy Loading) goals = self._goals return ProofStep(self.steps[step_index], goals, context) From c3eb6cb8da301173ac45a75d60f8d10c6b58359f Mon Sep 17 00:00:00 2001 From: pcarrott Date: Sat, 11 Nov 2023 00:02:11 +0000 Subject: [PATCH 19/28] Extract FileContext to separate file and standardize imports --- README.md | 2 +- coqpyt/coq/base_file.py | 102 ++++++------- coqpyt/coq/context.py | 82 ++++++++++ coqpyt/coq/lsp/client.py | 3 +- coqpyt/coq/lsp/structs.py | 3 +- coqpyt/coq/proof_file.py | 23 ++- coqpyt/coq/structs.py | 73 +-------- coqpyt/lsp/endpoint.py | 3 +- coqpyt/lsp/json_rpc_endpoint.py | 3 +- coqpyt/tests/test_coq_file.py | 5 +- coqpyt/tests/test_coq_lsp_client.py | 4 +- coqpyt/tests/test_json_rpc_endpoint.py | 1 + coqpyt/tests/test_proof_file.py | 203 +++++++++++++------------ examples/readme.py | 3 +- 14 files changed, 260 insertions(+), 250 deletions(-) create mode 100644 coqpyt/coq/context.py diff --git a/README.md b/README.md index 36b8c3e..e81f63d 100644 --- a/README.md +++ b/README.md @@ -20,7 +20,7 @@ python -m pip install -e . Import classes from the ``coqpyt`` package. - + ```py from coqpyt.coq.base_file import CoqFile from coqpyt.coq.proof_file import ProofFile diff --git a/coqpyt/coq/base_file.py b/coqpyt/coq/base_file.py index 8ea48dc..e538ad0 100644 --- a/coqpyt/coq/base_file.py +++ b/coqpyt/coq/base_file.py @@ -3,20 +3,24 @@ import uuid import tempfile import subprocess +from typing import Optional, List +from packaging import version + from coqpyt.lsp.structs import ( TextDocumentItem, TextDocumentIdentifier, VersionedTextDocumentIdentifier, TextDocumentContentChangeEvent, + ResponseError, + ErrorCodes, + Diagnostic, ) -from coqpyt.lsp.structs import ResponseError, ErrorCodes, Diagnostic from coqpyt.coq.lsp.structs import Position, GoalAnswer, RangedSpan -from coqpyt.coq.structs import Step, FileContext, Term, TermType, SegmentType from coqpyt.coq.lsp.client import CoqLspClient from coqpyt.coq.exceptions import * from coqpyt.coq.changes import * -from typing import List, Optional -from packaging import version +from coqpyt.coq.structs import Step, Term, TermType, SegmentType +from coqpyt.coq.context import FileContext class CoqFile(object): @@ -83,7 +87,7 @@ def __init__( self.curr_module_type: List[str] = [] self.curr_section: List[str] = [] self.__segment_stack: List[SegmentType] = [] - self.context = FileContext() + self.context = FileContext(self.path) self.__anonymous_id: Optional[int] = None self.version = 1 self.__last_end_pos: Optional[Position] = None @@ -184,44 +188,6 @@ def __init_coq_version(self, coqtop): self.__expr = lambda e: e if outdated else e[1] self.__where_notation_key = "decl_ntn" if outdated else "ntn_decl" - @property - def curr_step(self): - return self.steps[self.steps_taken] - - @property - def prev_step(self): - return self.steps[self.steps_taken - 1] - - @staticmethod - def get_id(id: List) -> str: - if id[0] == "Ser_Qualid": - return ".".join([l[1] for l in reversed(id[1][1])] + [id[2][1]]) - elif id[0] == "Id": - return id[1] - return None - - @staticmethod - def get_ident(el: List) -> Optional[str]: - if ( - len(el) == 3 - and el[0] == "GenArg" - and el[1][0] == "Rawwit" - and el[1][1][0] == "ExtraArg" - ): - if el[1][1][1] == "identref": - return el[2][0][1][1] - elif el[1][1][1] == "ident": - return el[2][1] - return None - - @staticmethod - def get_v(el): - if isinstance(el, dict) and "v" in el: - return el["v"] - elif isinstance(el, list) and len(el) == 2 and el[0] == "v": - return el[1] - return None - def expr(self, step: RangedSpan) -> Optional[List]: if ( step.span is not None @@ -673,6 +639,14 @@ def _change_steps(self, changes: List[CoqChange]): if len(self.steps) != previous_steps_size + offset_steps or not self.is_valid: raise InvalidChangeException() + @property + def curr_step(self): + return self.steps[self.steps_taken] + + @property + def prev_step(self): + return self.steps[self.steps_taken - 1] + @property def timeout(self) -> int: """The timeout of the coq-lsp client. @@ -715,18 +689,6 @@ def in_proof(self) -> bool: """ return self.__in_proof(self.current_goals) - @property - def terms(self) -> List[Term]: - """ - Returns: - List[Term]: The terms of the file already executed - """ - return list( - filter( - lambda term: term.file_path == self.path, self.context.terms.values() - ) - ) - @property def diagnostics(self) -> List[Diagnostic]: """ @@ -838,3 +800,33 @@ def close(self): self.coq_lsp_client.exit() if self.__from_lib: os.remove(self.__path) + + @staticmethod + def get_id(id: List) -> str: + if id[0] == "Ser_Qualid": + return ".".join([l[1] for l in reversed(id[1][1])] + [id[2][1]]) + elif id[0] == "Id": + return id[1] + return None + + @staticmethod + def get_ident(el: List) -> Optional[str]: + if ( + len(el) == 3 + and el[0] == "GenArg" + and el[1][0] == "Rawwit" + and el[1][1][0] == "ExtraArg" + ): + if el[1][1][1] == "identref": + return el[2][0][1][1] + elif el[1][1][1] == "ident": + return el[2][1] + return None + + @staticmethod + def get_v(el): + if isinstance(el, dict) and "v" in el: + return el["v"] + elif isinstance(el, list) and len(el) == 2 and el[0] == "v": + return el[1] + return None diff --git a/coqpyt/coq/context.py b/coqpyt/coq/context.py new file mode 100644 index 0000000..e72a63a --- /dev/null +++ b/coqpyt/coq/context.py @@ -0,0 +1,82 @@ +import re +from typing import List, Dict + +from coqpyt.coq.structs import Term, CoqError, CoqErrorCodes + + +class FileContext: + def __init__(self, path: str, terms: Dict[str, Term] = None): + self.path = path + self.terms = {} if terms is None else terms + + @property + def local_terms(self) -> List[Term]: + """ + Returns: + List[Term]: The executed terms defined in the current file. + """ + return list( + filter(lambda term: term.file_path == self.path, self.terms.values()) + ) + + def update( + self, + terms: Dict[str, Term] = {}, + ): + self.terms.update(terms) + + def get_notation(self, notation: str, scope: str) -> Term: + """Get a notation from the context. + + Args: + notation (str): Id of the notation. E.g. "_ + _" + scope (str): Scope of the notation. E.g. "nat_scope" + + Raises: + RuntimeError: If the notation is not found in the context. + + Returns: + Term: Term that corresponds to the notation. + """ + notation_id = FileContext.get_notation_key(notation, scope) + regex = f"{re.escape(notation_id)}".split("\\ ") + for i, sub in enumerate(regex): + if sub == "_": + # We match the wildcard with the description from here: + # https://coq.inria.fr/distrib/current/refman/language/core/basic.html#grammar-token-ident + # Coq accepts more characters, but no one should need more than these... + chars = "A-Za-zÀ-ÖØ-öø-ˁˆ-ˑˠ-ˤˬˮͰ-ʹͶͷͺ-ͽͿΆΈ-ΊΌΎ-ΡΣ-ϵϷ-ҁҊ-ԯԱ-Ֆՙա-և" + regex[i] = f"([{chars}][{chars}0-9_']*|_[{chars}0-9_']+)" + else: + # Handle '_' + regex[i] = f"({sub}|('{sub}'))" + regex = "^" + "\\ ".join(regex) + "$" + + # Search notations + unscoped = None + for term in self.terms.keys(): + if re.match(regex, term): + return self.terms[term] + if re.match(regex, term.split(":")[0].strip()): + unscoped = term + # In case the stored id contains the scope but no scope is provided + if unscoped is not None: + return self.terms[unscoped] + + # Search Infix + if re.match("^_ ([^ ]*) _$", notation): + op = notation[2:-2] + key = FileContext.get_notation_key(op, scope) + if key in self.terms: + return self.terms[key] + + raise CoqError( + CoqErrorCodes.NotationNotFound, + f"Notation not found in context: {notation_id}", + ) + + @staticmethod + def get_notation_key(notation: str, scope: str): + if scope != "" and scope is not None: + notation += " : " + scope + return notation diff --git a/coqpyt/coq/lsp/client.py b/coqpyt/coq/lsp/client.py index a18cd40..a7be716 100644 --- a/coqpyt/coq/lsp/client.py +++ b/coqpyt/coq/lsp/client.py @@ -1,9 +1,10 @@ import time import subprocess + +from coqpyt.lsp.structs import * from coqpyt.lsp.json_rpc_endpoint import JsonRpcEndpoint from coqpyt.lsp.endpoint import LspEndpoint from coqpyt.lsp.client import LspClient -from coqpyt.lsp.structs import * from coqpyt.coq.lsp.structs import * diff --git a/coqpyt/coq/lsp/structs.py b/coqpyt/coq/lsp/structs.py index c301560..25884bf 100644 --- a/coqpyt/coq/lsp/structs.py +++ b/coqpyt/coq/lsp/structs.py @@ -1,5 +1,6 @@ from enum import Enum -from typing import Dict, Optional, Any, List, Tuple +from typing import Any, Optional, Tuple, List, Dict + from coqpyt.lsp.structs import Range, VersionedTextDocumentIdentifier, Position diff --git a/coqpyt/coq/proof_file.py b/coqpyt/coq/proof_file.py index e090d7f..0bc8107 100644 --- a/coqpyt/coq/proof_file.py +++ b/coqpyt/coq/proof_file.py @@ -3,6 +3,8 @@ import shutil import uuid import tempfile +from typing import Optional, Tuple, List, Dict + from coqpyt.lsp.structs import ( TextDocumentItem, VersionedTextDocumentIdentifier, @@ -10,20 +12,13 @@ ResponseError, ErrorCodes, ) -from coqpyt.coq.structs import ( - TermType, - Step, - Term, - ProofStep, - ProofTerm, - FileContext, -) -from coqpyt.coq.lsp.structs import Result, Query, GoalAnswer, Range -from coqpyt.coq.base_file import CoqFile +from coqpyt.coq.lsp.structs import Result, Query, Range from coqpyt.coq.lsp.client import CoqLspClient -from coqpyt.coq.changes import * +from coqpyt.coq.structs import TermType, Step, Term, ProofStep, ProofTerm from coqpyt.coq.exceptions import * -from typing import List, Dict, Optional, Tuple +from coqpyt.coq.changes import * +from coqpyt.coq.context import FileContext +from coqpyt.coq.base_file import CoqFile class _AuxFile(object): @@ -158,7 +153,7 @@ def get_context(file_path: str, timeout: int): aux_file.append(f"\nLocate Library {library}.") aux_file.didChange() - context = FileContext() + context = FileContext(file_path) for i, library in enumerate(libraries): v_file = aux_file.get_diagnostics( "Locate Library", library, last_line + i + 1 @@ -184,7 +179,7 @@ def get_context(file_path: str, timeout: int): for term in list(aux_context.terms.keys()): if aux_context.terms[term].text.startswith("Local"): aux_context.terms.pop(term) - context.update(**vars(aux_context)) + context.update(aux_context.terms) return context diff --git a/coqpyt/coq/structs.py b/coqpyt/coq/structs.py index 6c3c009..ce596d9 100644 --- a/coqpyt/coq/structs.py +++ b/coqpyt/coq/structs.py @@ -1,8 +1,8 @@ -import re from enum import Enum -from typing import Dict, List, Union, Callable -from coqpyt.coq.lsp.structs import RangedSpan, GoalAnswer +from typing import List, Union, Callable + from coqpyt.lsp.structs import Diagnostic, Position +from coqpyt.coq.lsp.structs import RangedSpan, GoalAnswer class SegmentType(Enum): @@ -136,70 +136,3 @@ def __init__(self, term: Term, context: List[Term], steps: List[ProofStep]): super().__init__(term.step, term.type, term.file_path, term.module) self.steps = steps self.context = context - - -class FileContext: - def __init__(self, terms: Dict[str, Term] = None): - self.terms = {} if terms is None else terms - - def update( - self, - terms: Dict[str, Term] = {}, - ): - self.terms.update(terms) - - def get_notation(self, notation: str, scope: str) -> Term: - """Get a notation from the context. - - Args: - notation (str): Id of the notation. E.g. "_ + _" - scope (str): Scope of the notation. E.g. "nat_scope" - - Raises: - RuntimeError: If the notation is not found in the context. - - Returns: - Term: Term that corresponds to the notation. - """ - notation_id = FileContext.get_notation_key(notation, scope) - regex = f"{re.escape(notation_id)}".split("\\ ") - for i, sub in enumerate(regex): - if sub == "_": - # We match the wildcard with the description from here: - # https://coq.inria.fr/distrib/current/refman/language/core/basic.html#grammar-token-ident - # Coq accepts more characters, but no one should need more than these... - chars = "A-Za-zÀ-ÖØ-öø-ˁˆ-ˑˠ-ˤˬˮͰ-ʹͶͷͺ-ͽͿΆΈ-ΊΌΎ-ΡΣ-ϵϷ-ҁҊ-ԯԱ-Ֆՙա-և" - regex[i] = f"([{chars}][{chars}0-9_']*|_[{chars}0-9_']+)" - else: - # Handle '_' - regex[i] = f"({sub}|('{sub}'))" - regex = "^" + "\\ ".join(regex) + "$" - - # Search notations - unscoped = None - for term in self.terms.keys(): - if re.match(regex, term): - return self.terms[term] - if re.match(regex, term.split(":")[0].strip()): - unscoped = term - # In case the stored id contains the scope but no scope is provided - if unscoped is not None: - return self.terms[unscoped] - - # Search Infix - if re.match("^_ ([^ ]*) _$", notation): - op = notation[2:-2] - key = FileContext.get_notation_key(op, scope) - if key in self.terms: - return self.terms[key] - - raise CoqError( - CoqErrorCodes.NotationNotFound, - f"Notation not found in context: {notation_id}", - ) - - @staticmethod - def get_notation_key(notation: str, scope: str): - if scope != "" and scope is not None: - notation += " : " + scope - return notation diff --git a/coqpyt/lsp/endpoint.py b/coqpyt/lsp/endpoint.py index 2b5102a..9164836 100644 --- a/coqpyt/lsp/endpoint.py +++ b/coqpyt/lsp/endpoint.py @@ -1,8 +1,9 @@ from __future__ import print_function import threading import logging +from typing import List, Dict + from coqpyt.lsp import structs -from typing import Dict, List class LspEndpoint(threading.Thread): diff --git a/coqpyt/lsp/json_rpc_endpoint.py b/coqpyt/lsp/json_rpc_endpoint.py index 778a5dd..06a20ed 100644 --- a/coqpyt/lsp/json_rpc_endpoint.py +++ b/coqpyt/lsp/json_rpc_endpoint.py @@ -1,9 +1,10 @@ from __future__ import print_function import json import logging -from coqpyt.lsp import structs import threading +from coqpyt.lsp import structs + JSON_RPC_REQ_FORMAT = "Content-Length: {json_string_len}\r\n\r\n{json_string}" LEN_HEADER = "Content-Length: " TYPE_HEADER = "Content-Type: " diff --git a/coqpyt/tests/test_coq_file.py b/coqpyt/tests/test_coq_file.py index 97f7158..c21f6ea 100644 --- a/coqpyt/tests/test_coq_file.py +++ b/coqpyt/tests/test_coq_file.py @@ -1,9 +1,10 @@ import os import shutil import pytest -from coqpyt.coq.base_file import CoqFile -from coqpyt.coq.changes import * + from coqpyt.coq.exceptions import * +from coqpyt.coq.changes import * +from coqpyt.coq.base_file import CoqFile coq_file: CoqFile = None diff --git a/coqpyt/tests/test_coq_lsp_client.py b/coqpyt/tests/test_coq_lsp_client.py index 7c5bf38..e5c32bf 100644 --- a/coqpyt/tests/test_coq_lsp_client.py +++ b/coqpyt/tests/test_coq_lsp_client.py @@ -1,7 +1,7 @@ import os -from coqpyt.coq.lsp.client import CoqLspClient + from coqpyt.lsp.structs import * -from coqpyt.coq.lsp.structs import * +from coqpyt.coq.lsp.client import CoqLspClient def test_save_vo(): diff --git a/coqpyt/tests/test_json_rpc_endpoint.py b/coqpyt/tests/test_json_rpc_endpoint.py index 354c9f7..24c6019 100644 --- a/coqpyt/tests/test_json_rpc_endpoint.py +++ b/coqpyt/tests/test_json_rpc_endpoint.py @@ -1,5 +1,6 @@ import os import pytest + from coqpyt import lsp JSON_RPC_RESULT_LIST = [ diff --git a/coqpyt/tests/test_proof_file.py b/coqpyt/tests/test_proof_file.py index 1c4e296..a8a8422 100644 --- a/coqpyt/tests/test_proof_file.py +++ b/coqpyt/tests/test_proof_file.py @@ -4,15 +4,16 @@ import subprocess import pytest import tempfile -from typing import List, Tuple +from typing import Tuple, List + from coqpyt.coq.lsp.structs import * -from coqpyt.coq.structs import TermType, Term, CoqError, CoqErrorCodes -from coqpyt.coq.proof_file import ProofFile from coqpyt.coq.exceptions import * from coqpyt.coq.changes import * +from coqpyt.coq.structs import TermType, Term, CoqError, CoqErrorCodes +from coqpyt.coq.proof_file import ProofFile versionId: VersionedTextDocumentIdentifier = None -state: ProofFile = None +proof_file: ProofFile = None workspace: str = None file_path: str = "" @@ -29,7 +30,7 @@ def compare_context( @pytest.fixture def setup(request): - global state, versionId, workspace, file_path + global proof_file, versionId, workspace, file_path file_path, workspace = request.param[0], request.param[1] if len(request.param) == 3 and request.param[2]: new_path = os.path.join( @@ -43,7 +44,7 @@ def setup(request): workspace = os.path.join(os.getcwd(), "tests/resources", workspace) subprocess.run(f"cd {workspace} && make", shell=True, capture_output=True) uri = "file://" + file_path - state = ProofFile(file_path, timeout=60, workspace=workspace) + proof_file = ProofFile(file_path, timeout=60, workspace=workspace) versionId = VersionedTextDocumentIdentifier(uri, 1) yield @@ -53,7 +54,7 @@ def teardown(request): yield if workspace is not None: subprocess.run(f"cd {workspace} && make clean", shell=True, capture_output=True) - state.close() + proof_file.close() if ( hasattr(request, "param") and len(request.param) == 1 @@ -65,7 +66,7 @@ def teardown(request): @pytest.mark.parametrize("setup", [("test_valid.v", None)], indirect=True) def test_get_proofs(setup, teardown): - proofs = state.proofs + proofs = proof_file.proofs assert len(proofs) == 4 texts = [ @@ -120,7 +121,7 @@ def test_get_proofs(setup, teardown): ], [("Ltac reduce_eq := simpl; reflexivity.", TermType.TACTIC, [])], ] - statement_context = [ + proof_filement_context = [ ("Inductive nat : Set := | O : nat | S : nat -> nat.", TermType.INDUCTIVE, []), ('Notation "x = y" := (eq x y) : type_scope.', TermType.NOTATION, []), ( @@ -130,7 +131,7 @@ def test_get_proofs(setup, teardown): ), ] - compare_context(statement_context, proofs[0].context) + compare_context(proof_filement_context, proofs[0].context) assert proofs[0].text == "Theorem plus_O_n : forall n:nat, 0 + n = n." for i in range(4): assert proofs[0].steps[i].text == texts[i] @@ -224,7 +225,7 @@ def test_get_proofs(setup, teardown): (24, 4, 24, 25), (25, 4, 25, 16), ] - statement_context = [ + proof_filement_context = [ ( "Notation \"∀ x .. y , P\" := (forall x, .. (forall y, P) ..) (at level 200, x binder, y binder, right associativity, format \"'[ ' '[ ' ∀ x .. y ']' , " + "'/' P ']'\") : type_scope.", @@ -245,7 +246,7 @@ def test_get_proofs(setup, teardown): ("Inductive nat : Set := | O : nat | S : nat -> nat.", TermType.INDUCTIVE, []), ] - compare_context(statement_context, proofs[1].context) + compare_context(proof_filement_context, proofs[1].context) assert ( proofs[1].text == "Definition mult_0_plus : ∀ n m : nat, 0 + (S n * m) = S n * m." @@ -309,7 +310,7 @@ def test_get_proofs(setup, teardown): ], [("Ltac reduce_eq := simpl; reflexivity.", TermType.TACTIC, [])], ] - statement_context = [ + proof_filement_context = [ ("Inductive nat : Set := | O : nat | S : nat -> nat.", TermType.INDUCTIVE, []), ('Notation "x = y" := (eq x y) : type_scope.', TermType.NOTATION, []), ( @@ -319,7 +320,7 @@ def test_get_proofs(setup, teardown): ), ] - compare_context(statement_context, proofs[2].context) + compare_context(proof_filement_context, proofs[2].context) assert proofs[2].text == "Theorem plus_O_n : forall n:nat, n = 0 + n." for i in range(4): assert proofs[2].steps[i].text == texts[i] @@ -413,7 +414,7 @@ def test_get_proofs(setup, teardown): ], [], ] - statement_context = [ + proof_filement_context = [ ( "Notation \"∀ x .. y , P\" := (forall x, .. (forall y, P) ..) (at level 200, x binder, y binder, right associativity, format \"'[ ' '[ ' ∀ x .. y ']' , " + "'/' P ']'\") : type_scope.", @@ -434,7 +435,7 @@ def test_get_proofs(setup, teardown): ), ] - compare_context(statement_context, proofs[3].context) + compare_context(proof_filement_context, proofs[3].context) assert ( proofs[3].text == "Theorem mult_0_plus : ∀ n m : nat, S n * m = 0 + (S n * m)." ) @@ -447,10 +448,10 @@ def test_get_proofs(setup, teardown): @pytest.mark.parametrize("setup", [("test_valid.v", None, True)], indirect=True) @pytest.mark.parametrize("teardown", [(True,)], indirect=True) def test_get_proofs_valid_change(setup, teardown): - state.delete_step(6) + proof_file.delete_step(6) versionId.version += 1 - proofs = state.proofs + proofs = proof_file.proofs texts = [ "\n Proof.", "\n Print plus.", @@ -494,10 +495,10 @@ def test_get_proofs_valid_change(setup, teardown): assert step.text == texts[i] assert str(proofs[0].steps[i].goals) == str(goals[i]) - state.add_step(5, "\n intros n.") + proof_file.add_step(5, "\n intros n.") versionId.version += 1 - proofs = state.proofs + proofs = proof_file.proofs texts = [ "\n Proof.", "\n intros n.", @@ -549,7 +550,7 @@ def test_get_proofs_valid_change(setup, teardown): assert str(proofs[0].steps[i].goals) == str(goals[i]) # Check if context is changed correctly - state.add_step(7, "\n Print minus.") + proof_file.add_step(7, "\n Print minus.") texts = [ "\n Proof.", "\n intros n.", @@ -580,36 +581,36 @@ def test_get_proofs_valid_change(setup, teardown): # Add outside of proof with pytest.raises(NotImplementedError): - state.add_step(25, "\n Print plus.") + proof_file.add_step(25, "\n Print plus.") # Add step in beginning of proof - state.add_step(26, "\n Print plus.") - assert state.steps[27].text == "\n Print plus." + proof_file.add_step(26, "\n Print plus.") + assert proof_file.steps[27].text == "\n Print plus." # Delete outside of proof with pytest.raises(NotImplementedError): - state.delete_step(33) + proof_file.delete_step(33) # Add step to end of proof - state.add_step(31, "\n Print plus.") - assert state.steps[32].text == "\n Print plus." + proof_file.add_step(31, "\n Print plus.") + assert proof_file.steps[32].text == "\n Print plus." # Delete step in beginning of proof - state.delete_step(27) - assert state.steps[27].text == "\n intros n." + proof_file.delete_step(27) + assert proof_file.steps[27].text == "\n intros n." # Delete step in end of proof - state.delete_step(41) - assert state.steps[41].text == "\n Admitted." + proof_file.delete_step(41) + assert proof_file.steps[41].text == "\n Admitted." @pytest.mark.parametrize("setup", [("test_valid.v", None, True)], indirect=True) @pytest.mark.parametrize("teardown", [(True,)], indirect=True) def test_get_proofs_change_steps(setup, teardown): versionId.version += 1 - proofs = state.proofs + proofs = proof_file.proofs - state.change_steps( + proof_file.change_steps( [ CoqDeleteStep(6), CoqAddStep("\n intros n.", 5), @@ -647,68 +648,68 @@ def test_get_proofs_change_steps(setup, teardown): # Add outside of proof with pytest.raises(NotImplementedError): - state.change_steps([CoqAddStep("\n Print plus.", 25)]) + proof_file.change_steps([CoqAddStep("\n Print plus.", 25)]) # Add step in beginning of proof - state.change_steps([CoqAddStep("\n Print plus.", 26)]) - assert state.steps[27].text == "\n Print plus." + proof_file.change_steps([CoqAddStep("\n Print plus.", 26)]) + assert proof_file.steps[27].text == "\n Print plus." # # Delete outside of proof with pytest.raises(NotImplementedError): - state.change_steps([CoqDeleteStep(33)]) + proof_file.change_steps([CoqDeleteStep(33)]) # # Add step to end of proof - state.change_steps([CoqAddStep("\n Print plus.", 31)]) - assert state.steps[32].text == "\n Print plus." + proof_file.change_steps([CoqAddStep("\n Print plus.", 31)]) + assert proof_file.steps[32].text == "\n Print plus." # # Delete step in beginning of proof - state.change_steps([CoqDeleteStep(27)]) - assert state.steps[27].text == "\n intros n." + proof_file.change_steps([CoqDeleteStep(27)]) + assert proof_file.steps[27].text == "\n intros n." # # Delete step in end of proof - state.change_steps([CoqDeleteStep(41)]) - assert state.steps[41].text == "\n Admitted." + proof_file.change_steps([CoqDeleteStep(41)]) + assert proof_file.steps[41].text == "\n Admitted." @pytest.mark.parametrize("setup", [("test_valid.v", None, True)], indirect=True) @pytest.mark.parametrize("teardown", [(True,)], indirect=True) def test_get_proofs_invalid_change(setup, teardown): - n_old_steps = len(state.steps) - old_diagnostics = state.diagnostics + n_old_steps = len(proof_file.steps) + old_diagnostics = proof_file.diagnostics old_goals = [] - for proof in state.proofs: + for proof in proof_file.proofs: for step in proof.steps: old_goals.append(step.goals) def check_rollback(): - with open(state.path, "r") as f: - assert n_old_steps == len(state.steps) - assert old_diagnostics == state.diagnostics - assert state.is_valid + with open(proof_file.path, "r") as f: + assert n_old_steps == len(proof_file.steps) + assert old_diagnostics == proof_file.diagnostics + assert proof_file.is_valid assert "invalid_tactic" not in f.read() i = 0 - for proof in state.proofs: + for proof in proof_file.proofs: for step in proof.steps: assert step.goals == old_goals[i] i += 1 with pytest.raises(InvalidDeleteException): - state.delete_step(9) + proof_file.delete_step(9) check_rollback() with pytest.raises(InvalidDeleteException): - state.delete_step(16) + proof_file.delete_step(16) check_rollback() with pytest.raises(InvalidStepException): - state.add_step(7, "invalid_tactic") + proof_file.add_step(7, "invalid_tactic") check_rollback() with pytest.raises(InvalidStepException): - state.add_step(7, "invalid_tactic.") + proof_file.add_step(7, "invalid_tactic.") check_rollback() with pytest.raises(InvalidStepException): - state.add_step(7, "\n invalid_tactic.") + proof_file.add_step(7, "\n invalid_tactic.") check_rollback() with pytest.raises(InvalidStepException): - state.add_step(7, "\n invalid_tactic x $$$ y.") + proof_file.add_step(7, "\n invalid_tactic x $$$ y.") check_rollback() @@ -716,34 +717,34 @@ def check_rollback(): @pytest.mark.parametrize("teardown", [(True,)], indirect=True) def test_get_proofs_change_notation(setup, teardown): # Just checking if the program does not crash - state.add_step(len(state.steps) - 3, " destruct (a .. (ex (fun y => p)) ..)) (at level 200, x binder, right associativity, format \"'[' 'exists' '/ ' x .. y , '/ ' p ']'\") : type_scope." ) @pytest.mark.parametrize("setup", [("test_list_notation.v", None)], indirect=True) def test_list_notation(setup, teardown): - assert len(state.proofs) == 1 + assert len(proof_file.proofs) == 1 context = [ ('Notation "x = y" := (eq x y) : type_scope.', TermType.NOTATION, []), ( @@ -810,7 +811,7 @@ def test_list_notation(setup, teardown): ["ListNotations"], ), ] - compare_context(context, state.proofs[0].context) + compare_context(context, proof_file.proofs[0].context) @pytest.mark.parametrize("setup", [("test_unknown_notation.v", None)], indirect=True) @@ -819,13 +820,13 @@ def test_unknown_notation(setup, teardown): Locate command because it is a default notation. """ with pytest.raises(CoqError) as e_info: - assert state.context.get_notation("{ _ }", "") + assert proof_file.context.get_notation("{ _ }", "") assert e_info.value.code == CoqErrorCodes.NotationNotFound @pytest.mark.parametrize("setup", [("test_nested_proofs.v", None)], indirect=True) def test_nested_proofs(setup, teardown): - proofs = state.proofs + proofs = proof_file.proofs assert len(proofs) == 4 steps = ["\n intros n.", "\n simpl; reflexivity.", "\n Qed."] @@ -863,7 +864,7 @@ def test_nested_proofs(setup, teardown): @pytest.mark.parametrize("setup", [("test_theorem_tokens.v", None)], indirect=True) def test_theorem_tokens(setup, teardown): - proofs = state.proofs + proofs = proof_file.proofs assert len(proofs) == 7 assert proofs[0].type == TermType.REMARK assert proofs[1].type == TermType.FACT @@ -876,7 +877,7 @@ def test_theorem_tokens(setup, teardown): @pytest.mark.parametrize("setup", [("test_bullets.v", None)], indirect=True) def test_bullets(setup, teardown): - proofs = state.proofs + proofs = proof_file.proofs assert len(proofs) == 1 steps = [ "\nProof.", @@ -895,10 +896,10 @@ def test_bullets(setup, teardown): @pytest.mark.parametrize("setup", [("test_obligation.v", None)], indirect=True) def test_obligation(setup, teardown): - proofs = state.proofs + proofs = proof_file.proofs assert len(proofs) == 11 - statement_context = [ + proof_filement_context = [ ("Inductive nat : Set := | O : nat | S : nat -> nat.", TermType.INDUCTIVE, []), ("Notation dec := sumbool_of_bool.", TermType.NOTATION, []), ("Notation leb := Nat.leb (only parsing).", TermType.NOTATION, []), @@ -925,7 +926,7 @@ def test_obligation(setup, teardown): ] for i, proof in enumerate(proofs): - compare_context(statement_context, proof.context) + compare_context(proof_filement_context, proof.context) assert ( proof.text == "Program Definition " @@ -942,15 +943,15 @@ def test_obligation(setup, teardown): def test_module_type(setup, teardown): # We ignore proofs inside a Module Type since they can't be used outside # and should be overriden. - assert len(state.proofs) == 1 + assert len(proof_file.proofs) == 1 @pytest.mark.parametrize("setup", [("test_type_class.v", None)], indirect=True) def test_type_class(setup, teardown): - assert len(state.proofs) == 2 - assert len(state.proofs[0].steps) == 4 + assert len(proof_file.proofs) == 2 + assert len(proof_file.proofs[0].steps) == 4 assert ( - state.proofs[0].text + proof_file.proofs[0].text == "#[refine] Global Instance unit_EqDec : TypeClass.EqDecNew unit := { eqb_new x y := true }." ) @@ -967,10 +968,10 @@ def test_type_class(setup, teardown): [], ), ] - compare_context(context, state.proofs[0].context) + compare_context(context, proof_file.proofs[0].context) assert ( - state.proofs[1].text + proof_file.proofs[1].text == "Instance test : TypeClass.EqDecNew unit -> TypeClass.EqDecNew unit." ) @@ -987,18 +988,18 @@ def test_type_class(setup, teardown): ), ("Inductive unit : Set := tt : unit.", TermType.INDUCTIVE, []), ] - compare_context(context, state.proofs[1].context) + compare_context(context, proof_file.proofs[1].context) @pytest.mark.parametrize("setup", [("test_goal.v", None)], indirect=True) def test_goal(setup, teardown): - assert len(state.proofs) == 3 + assert len(proof_file.proofs) == 3 goals = [ "Definition ignored : forall P Q: Prop, (P -> Q) -> P -> Q.", "Goal forall P Q: Prop, (P -> Q) -> P -> Q.", "Goal forall P Q: Prop, (P -> Q) -> P -> Q.", ] - for i, proof in enumerate(state.proofs): + for i, proof in enumerate(proof_file.proofs): assert proof.text == goals[i] compare_context( [ @@ -1015,7 +1016,7 @@ def test_goal(setup, teardown): @pytest.mark.parametrize("setup", [("test_simple_file.v", None, True)], indirect=True) @pytest.mark.parametrize("teardown", [(True,)], indirect=True) def test_simple_file_changes(setup, teardown): - state.change_steps( + proof_file.change_steps( [ CoqDeleteStep(1), CoqDeleteStep(1), @@ -1026,8 +1027,8 @@ def test_simple_file_changes(setup, teardown): CoqAddStep("\nAdmitted.", 2), ] ) - assert len(state.steps) == 5 - assert len(state.proofs) == 2 + assert len(proof_file.steps) == 5 + assert len(proof_file.proofs) == 2 steps = [ "Example test1: 1 + 1 = 2.", @@ -1036,17 +1037,17 @@ def test_simple_file_changes(setup, teardown): "\nAdmitted.", ] for i, step in enumerate(steps): - assert step == state.steps[i].text + assert step == proof_file.steps[i].text - assert state.proofs[0].text == steps[0] - assert state.proofs[0].steps[0].text == steps[1] - assert state.proofs[1].text == steps[2].strip() - assert state.proofs[1].steps[0].text == steps[3] + assert proof_file.proofs[0].text == steps[0] + assert proof_file.proofs[0].steps[0].text == steps[1] + assert proof_file.proofs[1].text == steps[2].strip() + assert proof_file.proofs[1].steps[0].text == steps[3] @pytest.mark.parametrize("setup", [("test_proof_cmd.v", None)], indirect=True) def test_proof_cmd(setup, teardown): - assert len(state.proofs) == 3 + assert len(proof_file.proofs) == 3 goals = [ "Goal ∃ (m : nat), S m = n.", "Goal ∃ (m : nat), S m = n.", @@ -1057,13 +1058,13 @@ def test_proof_cmd(setup, teardown): "\n Proof with auto.", "\n Proof 0.", ] - for i, proof in enumerate(state.proofs): + for i, proof in enumerate(proof_file.proofs): assert proof.text == goals[i] assert proof.steps[0].text == proofs[i] @pytest.mark.parametrize("setup", [("test_section_terms.v", None)], indirect=True) def test_section_terms(setup, teardown): - assert len(state.proofs) == 1 - assert state.proofs[0].text == "Let ignored : nat." - assert len(state.terms) == 0 + assert len(proof_file.proofs) == 1 + assert proof_file.proofs[0].text == "Let ignored : nat." + assert len(proof_file.context.local_terms) == 0 diff --git a/examples/readme.py b/examples/readme.py index 39246be..b7ed243 100644 --- a/examples/readme.py +++ b/examples/readme.py @@ -1,7 +1,8 @@ import os + +from coqpyt.coq.structs import TermType from coqpyt.coq.base_file import CoqFile from coqpyt.coq.proof_file import ProofFile -from coqpyt.coq.structs import TermType # Open Coq file with CoqFile(os.path.join(os.getcwd(), "examples/readme.v")) as coq_file: From 5da5ab22fa2fb06bdf46cbb2ce39287697df4d19 Mon Sep 17 00:00:00 2001 From: pcarrott Date: Sun, 12 Nov 2023 00:05:40 +0000 Subject: [PATCH 20/28] Extract term logic from CoqFile to FileContext --- coqpyt/coq/base_file.py | 344 ++------------------------------ coqpyt/coq/context.py | 319 +++++++++++++++++++++++++++-- coqpyt/coq/exceptions.py | 8 + coqpyt/coq/proof_file.py | 194 +++++++++--------- coqpyt/coq/structs.py | 34 +++- coqpyt/tests/test_coq_file.py | 1 + coqpyt/tests/test_proof_file.py | 5 +- 7 files changed, 452 insertions(+), 453 deletions(-) diff --git a/coqpyt/coq/base_file.py b/coqpyt/coq/base_file.py index e538ad0..a8159a6 100644 --- a/coqpyt/coq/base_file.py +++ b/coqpyt/coq/base_file.py @@ -2,9 +2,7 @@ import shutil import uuid import tempfile -import subprocess from typing import Optional, List -from packaging import version from coqpyt.lsp.structs import ( TextDocumentItem, @@ -19,7 +17,7 @@ from coqpyt.coq.lsp.client import CoqLspClient from coqpyt.coq.exceptions import * from coqpyt.coq.changes import * -from coqpyt.coq.structs import Step, Term, TermType, SegmentType +from coqpyt.coq.structs import Step from coqpyt.coq.context import FileContext @@ -31,9 +29,6 @@ class CoqFile(object): ast (List[RangedSpan]): AST of the Coq file. Each element is a step of execution in the Coq file. steps_taken (int): The number of steps already executed - curr_module (List[str]): A list correspondent to the module path in the - current step. For instance, if the current module is `Ex.Test`, the - list will be ['Ex', 'Test']. context (FileContext): The context defined in the file. path (str): Path of the file. If the file is from the Coq library, a temporary file will be used. @@ -64,6 +59,7 @@ def __init__( simply used to check the Coq version in use. Defaults to "coqtop". """ self.__init_path(file_path, library) + if workspace is not None: uri = f"file://{workspace}" else: @@ -82,17 +78,10 @@ def __init__( self.steps_taken: int = 0 self.__init_steps(text, ast) self.__validate() - self.__init_coq_version(coqtop) - self.curr_module: List[str] = [] - self.curr_module_type: List[str] = [] - self.curr_section: List[str] = [] - self.__segment_stack: List[SegmentType] = [] - self.context = FileContext(self.path) - self.__anonymous_id: Optional[int] = None + self.context = FileContext(self.path, module=self.file_module, coqtop=coqtop) self.version = 1 self.__last_end_pos: Optional[Position] = None self.__current_goals = None - self._last_term: Optional[Term] = None def __enter__(self): return self @@ -175,31 +164,6 @@ def __validate(self): step.diagnostics.append(diagnostic) break - def __init_coq_version(self, coqtop): - output = subprocess.check_output(f"{coqtop} -v", shell=True) - coq_version = output.decode("utf-8").split("\n")[0].split()[-1] - outdated = version.parse(coq_version) < version.parse("8.18") - - # For version 8.18, we ignore the tags [VernacSynterp] and [VernacSynPure] - # and use the "ntn_decl" prefix when handling where notations - # For older versions, we only tested 8.17, so we provide no claims about - # versions prior to that. - - self.__expr = lambda e: e if outdated else e[1] - self.__where_notation_key = "decl_ntn" if outdated else "ntn_decl" - - def expr(self, step: RangedSpan) -> Optional[List]: - if ( - step.span is not None - and isinstance(step.span, dict) - and "v" in step.span - and isinstance(step.span["v"], dict) - and "expr" in step.span["v"] - ): - return self.__expr(step.span["v"]["expr"]) - - return [None] - def __short_text( self, text: str, curr_step: RangedSpan, prev_step: Optional[RangedSpan] = None ): @@ -207,250 +171,15 @@ def __short_text( nlines = curr_range.end.line - curr_range.start.line + 1 lines = text.split("\n")[-nlines:] - prev_range = None if prev_step is None else prev_step.range - if prev_range is None or prev_range.end.line < curr_range.start.line: - start = curr_range.start.character - else: - start = curr_range.start.character - prev_range.end.character + start = curr_range.start.character + if prev_step is not None and prev_step.range.end.line >= curr_range.start.line: + start -= prev_step.range.end.character lines[-1] = lines[-1][: curr_range.end.character] lines[0] = lines[0][start:] return " ".join(" ".join(lines).split()) - def __add_term(self, name: str, step: Step, term_type: TermType): - term = Term(step, term_type, self.path, self.curr_module[:]) - self._last_term = term - if term.type == TermType.NOTATION: - self.context.update(terms={name: term}) - return - - full_name = lambda name: ".".join(self.curr_module + [name]) - self.context.update(terms={full_name(name): term}) - - curr_file_module = "" - for module in reversed(self.file_module): - curr_file_module = module + "." + curr_file_module - self.context.update(terms={curr_file_module + name: term}) - - @staticmethod - def __get_term_type(expr: List) -> TermType: - if expr[0] == "VernacStartTheoremProof": - return getattr(TermType, expr[1][0].upper()) - elif expr[0] == "VernacDefinition": - return TermType.DEFINITION - elif expr[0] in ["VernacNotation", "VernacSyntacticDefinition"]: - return TermType.NOTATION - elif expr[0] == "VernacExtend" and expr[1][0] == "Obligations": - return TermType.OBLIGATION - elif expr[0] == "VernacInductive" and expr[1][0] == "Class": - return TermType.CLASS - elif expr[0] == "VernacInductive" and expr[1][0] in ["Record", "Structure"]: - return TermType.RECORD - elif expr[0] == "VernacInductive" and expr[1][0] == "Variant": - return TermType.VARIANT - elif expr[0] == "VernacInductive" and expr[1][0] == "CoInductive": - return TermType.COINDUCTIVE - elif expr[0] == "VernacInductive": - return TermType.INDUCTIVE - elif expr[0] == "VernacInstance": - return TermType.INSTANCE - elif expr[0] == "VernacCoFixpoint": - return TermType.COFIXPOINT - elif expr[0] == "VernacFixpoint": - return TermType.FIXPOINT - elif expr[0] == "VernacScheme": - return TermType.SCHEME - elif expr[0] == "VernacExtend" and expr[1][0].startswith("Derive"): - return TermType.DERIVE - elif expr[0] == "VernacExtend" and expr[1][0].startswith("AddSetoid"): - return TermType.SETOID - elif expr[0] == "VernacExtend" and expr[1][0].startswith( - ("AddRelation", "AddParametricRelation") - ): - return TermType.RELATION - elif ( - expr[0] == "VernacExtend" and expr[1][0] == "VernacDeclareTacticDefinition" - ): - return TermType.TACTIC - elif expr[0] == "VernacExtend" and expr[1][0] == "Function": - return TermType.FUNCTION - else: - return TermType.OTHER - - # Simultaneous definition of terms and notations (where clause) - # https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#simultaneous-definition-of-terms-and-notations - def __handle_where_notations(self, expr: List, term_type: TermType): - spans = [] - if ( - term_type - in [ - TermType.VARIANT, - TermType.INDUCTIVE, - ] - and len(expr) > 2 - and isinstance(expr[2], list) - and len(expr[2]) > 0 - and isinstance(expr[2][0], list) - and len(expr[2][0]) > 1 - and isinstance(expr[2][0][1], list) - and len(expr[2][0][1]) > 0 - ): - spans = expr[2][0][1] - elif ( - term_type == TermType.FIXPOINT - and len(expr) > 2 - and isinstance(expr[2], list) - and len(expr[2]) > 0 - and isinstance(expr[2][0], dict) - and "notations" in expr[2][0] - and isinstance(expr[2][0]["notations"], list) - and len(expr[2][0]["notations"]) > 0 - ): - spans = expr[2][0]["notations"] - - # handles when multiple notations are defined - for span in spans: - name = FileContext.get_notation_key( - span[f"{self.__where_notation_key}_string"]["v"], - span[f"{self.__where_notation_key}_scope"], - ) - self.__add_term(name, self.curr_step, TermType.NOTATION) - - def __process_step(self, sign): - def traverse_expr(expr): - inductive = expr[0] == "VernacInductive" - extend = expr[0] == "VernacExtend" - stack, res = expr[:0:-1], [] - while len(stack) > 0: - el = stack.pop() - v = CoqFile.get_v(el) - if v is not None and isinstance(v, list) and len(v) == 2: - id = CoqFile.get_id(v) - if id is not None: - if not inductive: - return [id] - res.append(id) - elif v[0] == "Name": - if not inductive: - return [v[1][1]] - res.append(v[1][1]) - - elif isinstance(el, dict): - for v in reversed(el.values()): - if isinstance(v, (dict, list)): - stack.append(v) - elif isinstance(el, list): - if len(el) > 0 and el[0] == "CLocalAssum": - continue - - ident = CoqFile.get_ident(el) - if ident is not None and extend: - return [ident] - - for v in reversed(el): - if isinstance(v, (dict, list)): - stack.append(v) - return res - - try: - # TODO: A negative sign should handle things differently. For example: - # - names should be removed from the context - # - curr_module should change as you leave or re-enter modules - - expr = self.expr(self.curr_step.ast) - if ( - expr == [None] - or expr[0] == "VernacProof" - or (expr[0] == "VernacExtend" and expr[1][0] == "VernacSolve") - ): - return - term_type = CoqFile.__get_term_type(expr) - text = self.curr_step.short_text - - # FIXME: Section-local terms are ignored. We do this to avoid - # overwriting global terms with section-local terms after the section - # is closed. Regardless, these should be handled given that they might - # be used within the section. - for keyword in [ - "Variable", - "Let", - "Context", - "Hypothesis", - "Hypotheses", - ]: - if text.startswith(keyword): - # NOTE: We update the last term so as to obtain proofs even for - # section-local terms. This is safe, because the attribute is - # meant to be overwritten every time a new term is found. - self._last_term = Term( - self.curr_step, term_type, self.path, self.curr_module[:] - ) - return - - if expr[0] == "VernacEndSegment": - if len(self.__segment_stack) == 0: - return - match self.__segment_stack.pop(): - case SegmentType.MODULE: - self.curr_module.pop() - case SegmentType.MODULE_TYPE: - self.curr_module_type.pop() - case SegmentType.SECTION: - self.curr_section.pop() - elif expr[0] == "VernacDefineModule": - self.curr_module.append(expr[2]["v"][1]) - self.__segment_stack.append(SegmentType.MODULE) - elif expr[0] == "VernacDeclareModuleType": - self.curr_module_type.append(expr[1]["v"][1]) - self.__segment_stack.append(SegmentType.MODULE_TYPE) - elif expr[0] == "VernacBeginSection": - self.curr_section.append(expr[1]["v"][1]) - self.__segment_stack.append(SegmentType.SECTION) - - # HACK: We ignore terms inside a Module Type since they can't be used outside - # and should be overriden. - elif len(self.curr_module_type) > 0: - return - elif expr[0] == "VernacExtend" and expr[1][0] == "VernacTacticNotation": - # FIXME: Handle this case - return - elif expr[0] == "VernacNotation": - name = text.split('"')[1].strip() - if text[:-1].split(":")[-1].endswith("_scope"): - name += " : " + text[:-1].split(":")[-1].strip() - self.__add_term(name, self.curr_step, TermType.NOTATION) - elif expr[0] == "VernacSyntacticDefinition": - name = text.split(" ")[1] - if text[:-1].split(":")[-1].endswith("_scope"): - name += " : " + text[:-1].split(":")[-1].strip() - self.__add_term(name, self.curr_step, TermType.NOTATION) - elif expr[0] == "VernacInstance" and expr[1][0]["v"][0] == "Anonymous": - # FIXME: The name should be "_instance_N" - self.__add_term("_anonymous", self.curr_step, term_type) - elif expr[0] == "VernacDefinition" and expr[2][0]["v"][0] == "Anonymous": - # We associate the anonymous term to the same name used internally by Coq - if self.__anonymous_id is None: - name, self.__anonymous_id = "Unnamed_thm", 0 - else: - name = f"Unnamed_thm{self.__anonymous_id}" - self.__anonymous_id += 1 - self.__add_term(name, self.curr_step, term_type) - elif term_type == TermType.DERIVE: - name = CoqFile.get_ident(expr[2][0]) - self.__add_term(name, self.curr_step, term_type) - if expr[1][0] == "Derive": - prop = CoqFile.get_ident(expr[2][2]) - self.__add_term(prop, self.curr_step, term_type) - else: - names = traverse_expr(expr) - for name in names: - self.__add_term(name, self.curr_step, term_type) - - self.__handle_where_notations(expr, term_type) - finally: - self.steps_taken += sign - def __read(self): with open(self.path, "r") as f: return f.read() @@ -699,12 +428,6 @@ def diagnostics(self) -> List[Diagnostic]: uri = f"file://{self.__path}" return self.coq_lsp_client.lsp_endpoint.diagnostics[uri] - def get_term_type(self, ast: RangedSpan) -> TermType: - expr = self.expr(ast) - if expr is not None: - return CoqFile.__get_term_type(expr) - return TermType.OTHER - def exec(self, nsteps=1) -> List[Step]: """Execute steps in the file. @@ -721,21 +444,22 @@ def exec(self, nsteps=1) -> List[Step]: len(self.steps) - self.steps_taken if sign > 0 else self.steps_taken, ) - # FIXME: for now we ignore the terms in the context when going backwards - # on the file if sign == 1: for _ in range(nsteps): - self.__process_step(sign) + self.context.process_step(self.curr_step) + self.steps_taken += 1 return self.steps[initial_steps_taken : self.steps_taken] - else: - for _ in range(nsteps): - self.steps_taken -= 1 - if not self.in_proof: - self.steps_taken = initial_steps_taken - raise NotImplementedError( - "Going backwards outside of a proof is not implemented yet" - ) - return self.steps[self.steps_taken - 1 : initial_steps_taken] + + # FIXME: for now we ignore the terms in the context when going backwards + # on the file + for _ in range(nsteps): + self.steps_taken -= 1 + if not self.in_proof: + self.steps_taken = initial_steps_taken + raise NotImplementedError( + "Going backwards outside of a proof is not implemented yet" + ) + return self.steps[self.steps_taken - 1 : initial_steps_taken] def delete_step(self, step_index: int) -> None: """Deletes a step from the file. The step must be inside a proof. @@ -800,33 +524,3 @@ def close(self): self.coq_lsp_client.exit() if self.__from_lib: os.remove(self.__path) - - @staticmethod - def get_id(id: List) -> str: - if id[0] == "Ser_Qualid": - return ".".join([l[1] for l in reversed(id[1][1])] + [id[2][1]]) - elif id[0] == "Id": - return id[1] - return None - - @staticmethod - def get_ident(el: List) -> Optional[str]: - if ( - len(el) == 3 - and el[0] == "GenArg" - and el[1][0] == "Rawwit" - and el[1][1][0] == "ExtraArg" - ): - if el[1][1][1] == "identref": - return el[2][0][1][1] - elif el[1][1][1] == "ident": - return el[2][1] - return None - - @staticmethod - def get_v(el): - if isinstance(el, dict) and "v" in el: - return el["v"] - elif isinstance(el, list) and len(el) == 2 and el[0] == "v": - return el[1] - return None diff --git a/coqpyt/coq/context.py b/coqpyt/coq/context.py index e72a63a..7718042 100644 --- a/coqpyt/coq/context.py +++ b/coqpyt/coq/context.py @@ -1,13 +1,233 @@ import re -from typing import List, Dict +import subprocess +from packaging import version +from typing import Optional, List, Dict -from coqpyt.coq.structs import Term, CoqError, CoqErrorCodes +from coqpyt.coq.exceptions import NotationNotFoundException +from coqpyt.coq.structs import SegmentType, SegmentStack, Step, TermType, Term class FileContext: - def __init__(self, path: str, terms: Dict[str, Term] = None): + def __init__( + self, + path: str, + module: Optional[List[str]] = None, + coqtop: str = "coqtop", + terms: Optional[Dict[str, Term]] = None, + ): self.path = path + self.module = [] if module is None else module + self.__init_coq_version(coqtop) self.terms = {} if terms is None else terms + self.last_term: Optional[Term] = None + self.__segments = SegmentStack() + self.__anonymous_id: Optional[int] = None + + def __init_coq_version(self, coqtop): + output = subprocess.check_output(f"{coqtop} -v", shell=True) + coq_version = output.decode("utf-8").split("\n")[0].split()[-1] + outdated = version.parse(coq_version) < version.parse("8.18") + + # For version 8.18, we ignore the tags [VernacSynterp] and [VernacSynPure] + # and use the "ntn_decl" prefix when handling where notations + # For older versions, we only tested 8.17, so we provide no claims about + # versions prior to that. + + self.__expr = lambda e: e if outdated else e[1] + self.__where_notation_key = "decl_ntn" if outdated else "ntn_decl" + + def __add_terms(self, step: Step, expr: List): + term_type = FileContext.__term_type(expr) + text = step.short_text + + # FIXME: Section-local terms are ignored. We do this to avoid + # overwriting global terms with section-local terms after the section + # is closed. Regardless, these should be handled given that they might + # be used within the section. + for keyword in [ + "Variable", + "Let", + "Context", + "Hypothesis", + "Hypotheses", + ]: + if text.startswith(keyword): + # NOTE: We update the last term so as to obtain proofs even for + # section-local terms. This is safe, because the attribute is + # meant to be overwritten every time a new term is found. + self.last_term = Term( + step, term_type, self.path, self.__segments.modules[:] + ) + return + + if expr[0] == "VernacExtend" and expr[1][0] == "VernacTacticNotation": + # FIXME: Handle this case + return + elif expr[0] == "VernacNotation": + name = text.split('"')[1].strip() + if text[:-1].split(":")[-1].endswith("_scope"): + name += " : " + text[:-1].split(":")[-1].strip() + self.__add_term(name, step, TermType.NOTATION) + elif expr[0] == "VernacSyntacticDefinition": + name = text.split(" ")[1] + if text[:-1].split(":")[-1].endswith("_scope"): + name += " : " + text[:-1].split(":")[-1].strip() + self.__add_term(name, step, TermType.NOTATION) + elif expr[0] == "VernacInstance" and expr[1][0]["v"][0] == "Anonymous": + # FIXME: The name should be "_instance_N" + self.__add_term("_anonymous", step, term_type) + elif expr[0] == "VernacDefinition" and expr[2][0]["v"][0] == "Anonymous": + # We associate the anonymous term to the same name used internally by Coq + if self.__anonymous_id is None: + name, self.__anonymous_id = "Unnamed_thm", 0 + else: + name = f"Unnamed_thm{self.__anonymous_id}" + self.__anonymous_id += 1 + self.__add_term(name, step, term_type) + elif term_type == TermType.DERIVE: + name = FileContext.get_ident(expr[2][0]) + self.__add_term(name, step, term_type) + if expr[1][0] == "Derive": + prop = FileContext.get_ident(expr[2][2]) + self.__add_term(prop, step, term_type) + else: + names = FileContext.__get_names(expr) + for name in names: + self.__add_term(name, step, term_type) + + self.__handle_where_notations(step, expr, term_type) + + def __add_term(self, name: str, step: Step, term_type: TermType): + modules = self.__segments.modules[:] + term = Term(step, term_type, self.path, modules) + self.last_term = term + if term.type == TermType.NOTATION: + self.terms[name] = term + return + + self.terms[".".join(modules + [name])] = term + + curr_module = "" + for module in reversed(self.module): + curr_module = module + "." + curr_module + self.terms[curr_module + name] = term + + # Simultaneous definition of terms and notations (where clause) + # https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#simultaneous-definition-of-terms-and-notations + def __handle_where_notations(self, step: Step, expr: List, term_type: TermType): + spans = [] + if ( + term_type + in [ + TermType.VARIANT, + TermType.INDUCTIVE, + ] + and len(expr) > 2 + and isinstance(expr[2], list) + and len(expr[2]) > 0 + and isinstance(expr[2][0], list) + and len(expr[2][0]) > 1 + and isinstance(expr[2][0][1], list) + and len(expr[2][0][1]) > 0 + ): + spans = expr[2][0][1] + elif ( + term_type == TermType.FIXPOINT + and len(expr) > 2 + and isinstance(expr[2], list) + and len(expr[2]) > 0 + and isinstance(expr[2][0], dict) + and "notations" in expr[2][0] + and isinstance(expr[2][0]["notations"], list) + and len(expr[2][0]["notations"]) > 0 + ): + spans = expr[2][0]["notations"] + + # handles when multiple notations are defined + for span in spans: + name = FileContext.get_notation_key( + span[f"{self.__where_notation_key}_string"]["v"], + span[f"{self.__where_notation_key}_scope"], + ) + self.__add_term(name, step, TermType.NOTATION) + + @staticmethod + def __get_names(expr: List) -> List[str]: + inductive = expr[0] == "VernacInductive" + extend = expr[0] == "VernacExtend" + stack, res = expr[:0:-1], [] + while len(stack) > 0: + el = stack.pop() + v = FileContext.get_v(el) + if v is not None and isinstance(v, list) and len(v) == 2: + id = FileContext.get_id(v) + if id is not None: + if not inductive: + return [id] + res.append(id) + elif v[0] == "Name": + if not inductive: + return [v[1][1]] + res.append(v[1][1]) + + elif isinstance(el, dict): + for v in reversed(el.values()): + if isinstance(v, (dict, list)): + stack.append(v) + elif isinstance(el, list): + if len(el) > 0 and el[0] == "CLocalAssum": + continue + + ident = FileContext.get_ident(el) + if ident is not None and extend: + return [ident] + + for v in reversed(el): + if isinstance(v, (dict, list)): + stack.append(v) + return res + + @staticmethod + def __term_type(expr: List) -> TermType: + if expr[0] == "VernacStartTheoremProof": + return getattr(TermType, expr[1][0].upper()) + if expr[0] == "VernacDefinition": + return TermType.DEFINITION + if expr[0] in ["VernacNotation", "VernacSyntacticDefinition"]: + return TermType.NOTATION + if expr[0] == "VernacExtend" and expr[1][0] == "Obligations": + return TermType.OBLIGATION + if expr[0] == "VernacInductive" and expr[1][0] == "Class": + return TermType.CLASS + if expr[0] == "VernacInductive" and expr[1][0] in ["Record", "Structure"]: + return TermType.RECORD + if expr[0] == "VernacInductive" and expr[1][0] == "Variant": + return TermType.VARIANT + if expr[0] == "VernacInductive" and expr[1][0] == "CoInductive": + return TermType.COINDUCTIVE + if expr[0] == "VernacInductive": + return TermType.INDUCTIVE + if expr[0] == "VernacInstance": + return TermType.INSTANCE + if expr[0] == "VernacCoFixpoint": + return TermType.COFIXPOINT + if expr[0] == "VernacFixpoint": + return TermType.FIXPOINT + if expr[0] == "VernacScheme": + return TermType.SCHEME + if expr[0] == "VernacExtend" and expr[1][0].startswith("Derive"): + return TermType.DERIVE + if expr[0] == "VernacExtend" and expr[1][0].startswith("AddSetoid"): + return TermType.SETOID + if expr[0] == "VernacExtend" and expr[1][0].startswith( + ("AddRelation", "AddParametricRelation") + ): + return TermType.RELATION + if expr[0] == "VernacExtend" and expr[1][0] == "VernacDeclareTacticDefinition": + return TermType.TACTIC + if expr[0] == "VernacExtend" and expr[1][0] == "Function": + return TermType.FUNCTION + return TermType.OTHER @property def local_terms(self) -> List[Term]: @@ -19,12 +239,60 @@ def local_terms(self) -> List[Term]: filter(lambda term: term.file_path == self.path, self.terms.values()) ) - def update( - self, - terms: Dict[str, Term] = {}, - ): + @property + def in_module_type(self) -> bool: + return len(self.__segments.module_types) > 0 + + def process_step(self, step: Step): + expr = self.expr(step) + if ( + expr == [None] + or expr[0] == "VernacProof" + or (expr[0] == "VernacExtend" and expr[1][0] == "VernacSolve") + ): + return + + # Keep track of current segments + if expr[0] == "VernacEndSegment": + self.__segments.pop() + elif expr[0] == "VernacDefineModule": + self.__segments.push(expr[2]["v"][1], SegmentType.MODULE) + elif expr[0] == "VernacDeclareModuleType": + self.__segments.push(expr[1]["v"][1], SegmentType.MODULE_TYPE) + elif expr[0] == "VernacBeginSection": + self.__segments.push(expr[1]["v"][1], SegmentType.SECTION) + # HACK: We ignore terms inside a Module Type since they can't be used outside + # and should be overriden. + elif not self.in_module_type: + self.__add_terms(step, expr) + + def expr(self, step: Step) -> Optional[List]: + if ( + step.ast.span is not None + and isinstance(step.ast.span, dict) + and "v" in step.ast.span + and isinstance(step.ast.span["v"], dict) + and "expr" in step.ast.span["v"] + ): + return self.__expr(step.ast.span["v"]["expr"]) + return [None] + + def term_type(self, step: Step) -> TermType: + return FileContext.__term_type(self.expr(step)) + + def update(self, terms: Dict[str, Term] = {}): self.terms.update(terms) + def append_module_prefix(self, name: str) -> str: + return ".".join(self.__segments.modules + [name]) + + def get_term(self, name: str) -> Optional[Term]: + for i in range(len(self.__segments.modules), -1, -1): + curr_name = ".".join(self.__segments.modules[:i] + [name]) + if curr_name in self.terms: + return self.terms[curr_name] + return None + def get_notation(self, notation: str, scope: str) -> Term: """Get a notation from the context. @@ -70,13 +338,40 @@ def get_notation(self, notation: str, scope: str) -> Term: if key in self.terms: return self.terms[key] - raise CoqError( - CoqErrorCodes.NotationNotFound, - f"Notation not found in context: {notation_id}", - ) + raise NotationNotFoundException(notation_id) @staticmethod - def get_notation_key(notation: str, scope: str): + def get_notation_key(notation: str, scope: str) -> str: if scope != "" and scope is not None: notation += " : " + scope return notation + + @staticmethod + def get_id(id: List) -> Optional[str]: + if id[0] == "Ser_Qualid": + return ".".join([l[1] for l in reversed(id[1][1])] + [id[2][1]]) + elif id[0] == "Id": + return id[1] + return None + + @staticmethod + def get_ident(el: List) -> Optional[str]: + if ( + len(el) == 3 + and el[0] == "GenArg" + and el[1][0] == "Rawwit" + and el[1][1][0] == "ExtraArg" + ): + if el[1][1][1] == "identref": + return el[2][0][1][1] + elif el[1][1][1] == "ident": + return el[2][1] + return None + + @staticmethod + def get_v(el: List) -> Optional[str]: + if isinstance(el, dict) and "v" in el: + return el["v"] + elif isinstance(el, list) and len(el) == 2 and el[0] == "v": + return el[1] + return None diff --git a/coqpyt/coq/exceptions.py b/coqpyt/coq/exceptions.py index f37d408..6694782 100644 --- a/coqpyt/coq/exceptions.py +++ b/coqpyt/coq/exceptions.py @@ -24,3 +24,11 @@ def __init__(self, file: str): def __str__(self): return "The file {} is not valid.".format(self.file) + + +class NotationNotFoundException(Exception): + def __init__(self, notation: str): + self.notation: str = notation + + def __str__(self): + return 'Notation "{}" not found in context.'.format(self.notation) diff --git a/coqpyt/coq/proof_file.py b/coqpyt/coq/proof_file.py index 0bc8107..0336281 100644 --- a/coqpyt/coq/proof_file.py +++ b/coqpyt/coq/proof_file.py @@ -50,18 +50,6 @@ def __init_path(self, file_path): self.path = new_path self.version = 1 - def read(self): - with open(self.path, "r") as f: - return f.read() - - def write(self, text): - with open(self.path, "w") as f: - f.write(text) - - def append(self, text): - with open(self.path, "a") as f: - f.write(text) - def __handle_exception(self, e): if not isinstance(e, ResponseError) or e.code not in [ ErrorCodes.ServerQuit.value, @@ -71,26 +59,6 @@ def __handle_exception(self, e): self.coq_lsp_client.exit() os.remove(self.path) - def didOpen(self): - uri = f"file://{self.path}" - try: - self.coq_lsp_client.didOpen(TextDocumentItem(uri, "coq", 1, self.read())) - except Exception as e: - self.__handle_exception(e) - raise e - - def didChange(self): - uri = f"file://{self.path}" - self.version += 1 - try: - self.coq_lsp_client.didChange( - VersionedTextDocumentIdentifier(uri, self.version), - [TextDocumentContentChangeEvent(None, None, self.read())], - ) - except Exception as e: - self.__handle_exception(e) - raise e - def __get_queries(self, keyword): uri = f"file://{self.path}" if uri not in self.coq_lsp_client.lsp_endpoint.diagnostics: @@ -133,6 +101,38 @@ def get_diagnostics(self, keyword, search, line): break return None + def read(self): + with open(self.path, "r") as f: + return f.read() + + def write(self, text): + with open(self.path, "w") as f: + f.write(text) + + def append(self, text): + with open(self.path, "a") as f: + f.write(text) + + def didOpen(self): + uri = f"file://{self.path}" + try: + self.coq_lsp_client.didOpen(TextDocumentItem(uri, "coq", 1, self.read())) + except Exception as e: + self.__handle_exception(e) + raise e + + def didChange(self): + uri = f"file://{self.path}" + self.version += 1 + try: + self.coq_lsp_client.didChange( + VersionedTextDocumentIdentifier(uri, self.version), + [TextDocumentContentChangeEvent(None, None, self.read())], + ) + except Exception as e: + self.__handle_exception(e) + raise e + def close(self): self.coq_lsp_client.shutdown() self.coq_lsp_client.exit() @@ -233,13 +233,6 @@ def __enter__(self): def __exit__(self, exc_type, exc_value, traceback): self.close() - def __get_term(self, name): - for i in range(len(self.curr_module), -1, -1): - curr_name = ".".join(self.curr_module[:i] + [name]) - if curr_name in self.context.terms: - return self.context.terms[curr_name] - return None - def __locate(self, search, line): nots = self.__aux_file.get_diagnostics("Locate", f'"{search}"', line).split( "\n" @@ -248,57 +241,41 @@ def __locate(self, search, line): return nots[0][:-25] if fun(nots[0]) else nots[0] def __step_context(self, step: Step) -> List[Term]: - def traverse_expr(expr): - stack, res = expr[:0:-1], [] - while len(stack) > 0: - el = stack.pop() - if isinstance(el, list) and len(el) == 3 and el[0] == "Ser_Qualid": - term = self.__get_term(CoqFile.get_id(el)) - if term is not None and term not in res: + stack, res = self.context.expr(step)[:0:-1], [] + while len(stack) > 0: + el = stack.pop() + if isinstance(el, list) and len(el) == 3 and el[0] == "Ser_Qualid": + term = self.context.get_term(FileContext.get_id(el)) + if term is not None and term not in res: + res.append(term) + elif isinstance(el, list) and len(el) == 4 and el[0] == "CNotation": + line = len(self.__aux_file.read().split("\n")) + self.__aux_file.append(f'\nLocate "{el[2][1]}".') + self.__aux_file.didChange() + + notation_name, scope = el[2][1], "" + notation = self.__locate(notation_name, line) + if notation.split(":")[-1].endswith("_scope"): + scope = notation.split(":")[-1].strip() + + if notation != "Unknown notation": + term = self.context.get_notation(notation_name, scope) + if term not in res: res.append(term) - elif isinstance(el, list) and len(el) == 4 and el[0] == "CNotation": - line = len(self.__aux_file.read().split("\n")) - self.__aux_file.append(f'\nLocate "{el[2][1]}".') - self.__aux_file.didChange() - - notation_name, scope = el[2][1], "" - notation = self.__locate(notation_name, line) - if notation.split(":")[-1].endswith("_scope"): - scope = notation.split(":")[-1].strip() - - if notation != "Unknown notation": - term = self.context.get_notation(notation_name, scope) - if term not in res: - res.append(term) - - stack.append(el[1:]) - elif isinstance(el, list): - for v in reversed(el): - if isinstance(v, (dict, list)): - stack.append(v) - elif isinstance(el, dict): - for v in reversed(el.values()): - if isinstance(v, (dict, list)): - stack.append(v) - return res - - return traverse_expr(self.expr(step.ast)) - - def __get_program_context(self) -> Tuple[Term, List[Term]]: - def traverse_expr(expr): - stack = expr[:0:-1] - while len(stack) > 0: - el = stack.pop() - if isinstance(el, list): - ident = CoqFile.get_ident(el) - if ident is not None: - return ident - for v in reversed(el): - if isinstance(v, list): - stack.append(v) - return None + stack.append(el[1:]) + elif isinstance(el, list): + for v in reversed(el): + if isinstance(v, (dict, list)): + stack.append(v) + elif isinstance(el, dict): + for v in reversed(el.values()): + if isinstance(v, (dict, list)): + stack.append(v) + return res + def __get_program_context(self) -> Tuple[Term, List[Term]]: + expr = self.context.expr(self.prev_step) # Tags: # 0 - Obligation N of id : type # 1 - Obligation N of id @@ -306,31 +283,42 @@ def traverse_expr(expr): # 3 - Obligation N # 4 - Next Obligation of id # 5 - Next Obligation - tag = self.expr(self.prev_step.ast)[1][1] + tag = expr[1][1] if tag in [0, 1, 4]: - id = traverse_expr(self.expr(self.prev_step.ast)) - # This works because the obligation must be in the - # same module as the program - id = ".".join(self.curr_module + [id]) - return self.__program_context[id] + stack = expr[:0:-1] + while len(stack) > 0: + el = stack.pop() + if not isinstance(el, list): + continue + + ident = FileContext.get_ident(el) + if ident is not None: + # This works because the obligation must be in the + # same module as the program + id = self.context.append_module_prefix(ident) + return self.__program_context[id] + + for v in reversed(el): + if isinstance(v, list): + stack.append(v) elif tag in [2, 3, 5]: id = self.current_goals.program[0][0][1] # This works because the obligation must be in the # same module as the program - id = ".".join(self.curr_module + [id]) + id = self.context.append_module_prefix(id) return self.__program_context[id] - text = self._last_term.text + text = self.context.last_term.text raise RuntimeError(f"Unknown obligation command with tag number {tag}: {text}") def __check_program(self): goals = self.current_goals if len(goals.program) == 0: return - id = ".".join(self.curr_module + [goals.program[-1][0][1]]) + id = self.context.append_module_prefix(goals.program[-1][0][1]) if id in self.__program_context: return self.__program_context[id] = ( - self._last_term, + self.context.last_term, self.__step_context(self.prev_step), ) @@ -350,7 +338,7 @@ def __get_steps(self, proofs: List[ProofTerm]) -> List[ProofStep]: self.__step() # Nested proofs - if self.get_term_type(self.prev_step.ast) != TermType.OTHER: + if self.context.term_type(self.prev_step) != TermType.OTHER: self.__get_proof(proofs) # Pass Qed if it exists while not self.in_proof and not self.checked: @@ -368,7 +356,7 @@ def __get_steps(self, proofs: List[ProofTerm]) -> List[ProofStep]: raise e if ( self.steps_taken < len(self.steps) - and self.expr(self.curr_step.ast)[0] == "VernacEndProof" + and self.context.expr(self.curr_step)[0] == "VernacEndProof" ): steps.append(ProofStep(self.curr_step, goals, [])) @@ -376,14 +364,14 @@ def __get_steps(self, proofs: List[ProofTerm]) -> List[ProofStep]: def __get_proof(self, proofs: List[ProofTerm]): term, statement_context = None, None - if self.get_term_type(self.prev_step.ast) == TermType.OBLIGATION: + if self.context.term_type(self.prev_step) == TermType.OBLIGATION: term, statement_context = self.__get_program_context() - elif self.get_term_type(self.prev_step.ast) != TermType.OTHER: - term = self._last_term + elif self.context.term_type(self.prev_step) != TermType.OTHER: + term = self.context.last_term statement_context = self.__step_context(self.prev_step) # HACK: We ignore proofs inside a Module Type since they can't be used outside # and should be overriden. - if self.in_proof and len(self.curr_module_type) == 0: + if self.in_proof and not self.context.in_module_type: steps = self.__get_steps(proofs) proofs.append(ProofTerm(term, statement_context, steps)) diff --git a/coqpyt/coq/structs.py b/coqpyt/coq/structs.py index ce596d9..72ffe1a 100644 --- a/coqpyt/coq/structs.py +++ b/coqpyt/coq/structs.py @@ -1,5 +1,5 @@ from enum import Enum -from typing import List, Union, Callable +from typing import Any, List, Union, Callable from coqpyt.lsp.structs import Diagnostic, Position from coqpyt.coq.lsp.structs import RangedSpan, GoalAnswer @@ -39,15 +39,29 @@ class TermType(Enum): OTHER = 100 -class CoqErrorCodes(Enum): - InvalidFile = 0 - NotationNotFound = 1 - - -class CoqError(Exception): - def __init__(self, code: CoqErrorCodes, message: str): - self.code = code - self.message = message +class SegmentStack: + def __init__(self): + self.modules: List[str] = [] + self.module_types: List[str] = [] + self.sections: List[str] = [] + self.stack: List[SegmentType] = [] + + def __match_apply(self, type: SegmentType, operation: Callable, *args: Any): + match type: + case SegmentType.MODULE: + operation(self.modules, *args) + case SegmentType.MODULE_TYPE: + operation(self.module_types, *args) + case SegmentType.SECTION: + operation(self.sections, *args) + + def push(self, name: str, type: SegmentType): + self.stack.append(type) + self.__match_apply(type, list.append, name) + + def pop(self): + if len(self.stack) > 0: + self.__match_apply(self.stack.pop(), list.pop) class Step(object): diff --git a/coqpyt/tests/test_coq_file.py b/coqpyt/tests/test_coq_file.py index c21f6ea..eae7072 100644 --- a/coqpyt/tests/test_coq_file.py +++ b/coqpyt/tests/test_coq_file.py @@ -207,6 +207,7 @@ def test_module_type(setup, teardown): # We ignore terms inside a Module Type since they can't be used outside # and should be overriden. assert len(coq_file.context.terms) == 1 + assert "plus_O_n" in coq_file.context.terms @pytest.mark.parametrize("setup", ["test_derive.v"], indirect=True) diff --git a/coqpyt/tests/test_proof_file.py b/coqpyt/tests/test_proof_file.py index a8a8422..6adbfed 100644 --- a/coqpyt/tests/test_proof_file.py +++ b/coqpyt/tests/test_proof_file.py @@ -9,7 +9,7 @@ from coqpyt.coq.lsp.structs import * from coqpyt.coq.exceptions import * from coqpyt.coq.changes import * -from coqpyt.coq.structs import TermType, Term, CoqError, CoqErrorCodes +from coqpyt.coq.structs import TermType, Term from coqpyt.coq.proof_file import ProofFile versionId: VersionedTextDocumentIdentifier = None @@ -819,9 +819,8 @@ def test_unknown_notation(setup, teardown): """Checks if it is able to handle the notation { _ } that is unknown for the Locate command because it is a default notation. """ - with pytest.raises(CoqError) as e_info: + with pytest.raises(NotationNotFoundException): assert proof_file.context.get_notation("{ _ }", "") - assert e_info.value.code == CoqErrorCodes.NotationNotFound @pytest.mark.parametrize("setup", [("test_nested_proofs.v", None)], indirect=True) From dae49ec971a5dfabbad84d9816b6c25395e11c87 Mon Sep 17 00:00:00 2001 From: pcarrott Date: Mon, 13 Nov 2023 04:11:48 +0000 Subject: [PATCH 21/28] Implement (forward) exec for ProofFile --- README.md | 4 +- coqpyt/coq/base_file.py | 70 ++++++++------ coqpyt/coq/proof_file.py | 165 ++++++++++++++++++-------------- coqpyt/tests/test_coq_file.py | 2 +- coqpyt/tests/test_proof_file.py | 27 ++++-- examples/readme.py | 1 + 6 files changed, 156 insertions(+), 113 deletions(-) diff --git a/README.md b/README.md index e81f63d..42efd0c 100644 --- a/README.md +++ b/README.md @@ -29,7 +29,7 @@ from coqpyt.coq.structs import TermType Create a CoqFile object, execute the file and extract the generated context. - + ```py with CoqFile(os.path.join(os.getcwd(), "examples/readme.v")) as coq_file: coq_file.exec(nsteps=2) @@ -68,7 +68,7 @@ with CoqFile(os.path.join(os.getcwd(), "examples/readme.v")) as coq_file: Create a ProofFile object (a CoqFile instance) and interact with the proofs. - + ```py with ProofFile(os.path.join(os.getcwd(), "examples/readme.v")) as proof_file: # Number of proofs in the file diff --git a/coqpyt/coq/base_file.py b/coqpyt/coq/base_file.py index a8159a6..57800ca 100644 --- a/coqpyt/coq/base_file.py +++ b/coqpyt/coq/base_file.py @@ -192,7 +192,7 @@ def _goals(self, end_pos: Position): self.__handle_exception(e) raise e - def __in_proof(self, goals: Optional[GoalAnswer]): + def _can_close_proof(self, goals: Optional[GoalAnswer]): def empty_stack(stack): # e.g. [([], [])] for tuple in stack: @@ -201,13 +201,19 @@ def empty_stack(stack): return True goals = goals.goals - return goals is not None and ( - len(goals.goals) > 0 - or not empty_stack(goals.stack) - or len(goals.shelf) > 0 - or goals.bullet is not None + if goals is None: + return False + + return ( + len(goals.goals) == 0 + and empty_stack(goals.stack) + and len(goals.shelf) == 0 + and goals.bullet is None ) + def __in_proof(self, goals: Optional[GoalAnswer]): + return goals is not None and goals.goals is not None + def __update_steps(self): uri = f"file://{self.path}" text = self.__read() @@ -417,6 +423,10 @@ def in_proof(self) -> bool: bool: True if the current step is inside a proof """ return self.__in_proof(self.current_goals) + + @property + def can_close_proof(self): + return self._can_close_proof(self.current_goals) @property def diagnostics(self) -> List[Diagnostic]: @@ -428,6 +438,17 @@ def diagnostics(self) -> List[Diagnostic]: uri = f"file://{self.__path}" return self.coq_lsp_client.lsp_endpoint.diagnostics[uri] + def _step(self, sign): + self.steps_taken += sign + if sign == 1: + self.context.process_step(self.prev_step) + # FIXME: for now we ignore the terms in the context when going backwards + # on the file + elif not self.in_proof: + raise NotImplementedError( + "Going backwards outside of a proof is not implemented yet" + ) + def exec(self, nsteps=1) -> List[Step]: """Execute steps in the file. @@ -444,22 +465,23 @@ def exec(self, nsteps=1) -> List[Step]: len(self.steps) - self.steps_taken if sign > 0 else self.steps_taken, ) - if sign == 1: - for _ in range(nsteps): - self.context.process_step(self.curr_step) - self.steps_taken += 1 - return self.steps[initial_steps_taken : self.steps_taken] - - # FIXME: for now we ignore the terms in the context when going backwards - # on the file for _ in range(nsteps): - self.steps_taken -= 1 - if not self.in_proof: + try: + self._step(sign) + except NotImplementedError as e: self.steps_taken = initial_steps_taken - raise NotImplementedError( - "Going backwards outside of a proof is not implemented yet" - ) - return self.steps[self.steps_taken - 1 : initial_steps_taken] + raise e + + last, slice = sign == 1, (initial_steps_taken, self.steps_taken) + return self.steps[slice[1 - last] : slice[last]] + + def run(self) -> List[Step]: + """Executes the remaining steps in the file. + + Returns: + List[Step]: List of the remaining steps in the file. + """ + return self.exec(len(self.steps) - self.steps_taken) def delete_step(self, step_index: int) -> None: """Deletes a step from the file. The step must be inside a proof. @@ -501,14 +523,6 @@ def change_steps(self, changes: List[CoqChange]): """ self._make_change(self._change_steps, changes) - def run(self) -> List[Step]: - """Executes all the steps in the file. - - Returns: - List[Step]: List of all the steps in the file. - """ - return self.exec(len(self.steps)) - def save_vo(self): """Compiles the vo file for this Coq file.""" uri = f"file://{self.__path}" diff --git a/coqpyt/coq/proof_file.py b/coqpyt/coq/proof_file.py index ccf025e..19c938c 100644 --- a/coqpyt/coq/proof_file.py +++ b/coqpyt/coq/proof_file.py @@ -12,7 +12,7 @@ ResponseError, ErrorCodes, ) -from coqpyt.coq.lsp.structs import Result, Query, Range +from coqpyt.coq.lsp.structs import Result, Query, Range, GoalAnswer from coqpyt.coq.lsp.client import CoqLspClient from coqpyt.coq.structs import TermType, Step, Term, ProofStep, ProofTerm from coqpyt.coq.exceptions import * @@ -221,12 +221,14 @@ def __init__( try: # We need to update the context already defined in the CoqFile self.context.update(_AuxFile.get_context(self.path, self.timeout).terms) - self.__program_context: Dict[str, Tuple[Term, List[Term]]] = {} - self.__proofs: List[ProofTerm] = self.__get_proofs() except Exception as e: self.close() raise e + self.__program_context: Dict[str, Tuple[Term, List[Term]]] = {} + self.__proofs: List[ProofTerm] = [] + self.__open_proofs: List[Tuple[Term, List[Term], List[ProofStep], Optional[Term]]] = [] + def __enter__(self): return self @@ -322,84 +324,50 @@ def __check_program(self): self.__step_context(self.prev_step), ) - def __step(self): - self.exec() - self.__aux_file.append(self.prev_step.text) - self.__check_program() - - def __get_steps(self, proofs: List[ProofTerm]) -> List[ProofStep]: - steps = [] - while self.in_proof and not self.checked: - try: - goals = self.current_goals - except Exception as e: - self.__aux_file.close() - raise e - - self.__step() - if self.context.term_type(self.prev_step) in [ - TermType.TACTIC, - TermType.NOTATION, - TermType.INDUCTIVE, - TermType.COINDUCTIVE, - TermType.RECORD, - TermType.CLASS, - TermType.SCHEME, - TermType.VARIANT, - ]: - continue + def __check_proof_step(self, goals: GoalAnswer): + # HACK: We ignore proofs inside a Module Type since they can't be used outside + # and should be overriden. + if self.context.in_module_type: + return + if self.prev_step.text.strip() == "": + return + # Steps outside of proofs are ignored + if not self.in_proof and goals.goals is None: + return + # Create proof term when Qed is found + if self.context.expr(self.prev_step)[0] in ["VernacEndProof", "VernacExactProof"]: + open_proof = self.__open_proofs.pop() + open_proof[2].append(ProofStep(self.prev_step, goals, [])) + self.__proofs.append(ProofTerm(*open_proof)) + return - # Nested proofs - if self.context.term_type(self.prev_step) != TermType.OTHER: - self.__get_proof(proofs) - # Pass Qed if it exists - while not self.in_proof and not self.checked: - self.__step() - continue + term_type = self.context.term_type(self.prev_step) + # Regular proof steps are added to the last open proof + if term_type == TermType.OTHER: context = self.__step_context(self.prev_step) - if self.prev_step.text.strip() == "": - continue - steps.append(ProofStep(self.prev_step, goals, context)) - - try: - goals = self.current_goals - except Exception as e: - self.__aux_file.close() - raise e - if ( - self.steps_taken < len(self.steps) - and self.context.expr(self.curr_step)[0] == "VernacEndProof" - ): - steps.append(ProofStep(self.curr_step, goals, [])) - - return steps + self.__open_proofs[-1][2].append(ProofStep(self.prev_step, goals, context)) + return + # Assume that terms of the following types do not introduce new proofs + if term_type in [TermType.TACTIC, TermType.NOTATION, TermType.INDUCTIVE, TermType.COINDUCTIVE, TermType.RECORD, TermType.CLASS, TermType.SCHEME, TermType.VARIANT]: + return - def __get_proof(self, proofs): - program, statement_context = None, None - if self.context.term_type(self.prev_step) == TermType.OBLIGATION: + # New proof terms can be either obligations or regular proofs + proof_term, program = self.context.last_term, None + if term_type == TermType.OBLIGATION: program, statement_context = self.__get_program_context() - elif self.context.term_type(self.prev_step) != TermType.OTHER: + else: statement_context = self.__step_context(self.prev_step) - # HACK: We ignore proofs inside a Module Type since they can't be used outside - # and should be overriden. - if self.in_proof and not self.context.in_module_type: - term = self.context.last_term # Keep the term before rewrite - steps = self.__get_steps(proofs) - proofs.append(ProofTerm(term, statement_context, steps, program)) - - def __get_proofs(self) -> List[ProofTerm]: - proofs: List[ProofTerm] = [] - while not self.checked: - self.__step() - # Get context from initial statement - self.__get_proof(proofs) - return proofs + self.__open_proofs.append((proof_term, statement_context, [], program)) def __find_step(self, range: Range) -> Optional[Tuple[ProofTerm, int]]: - for proof in self.proofs: + for proof in self.__proofs: for i, proof_step in enumerate(proof.steps): if proof_step.ast.range == range: return (proof, i) + for proof in self.__open_proofs: + for i, proof_step in enumerate(proof[2]): + if proof_step.ast.range == range: + return (ProofTerm(*proof), i) return None def __find_prev(self, range: Range) -> Tuple[ProofTerm, Optional[int]]: @@ -408,9 +376,12 @@ def __find_prev(self, range: Range) -> Tuple[ProofTerm, Optional[int]]: return optional # Previous step may be the definition of the proof - for proof in self.proofs: + for proof in self.__proofs: if proof.ast.range == range: return (proof, -1) + for proof in self.__open_proofs: + if proof[0].ast.range == range: + return (ProofTerm(*proof), -1) raise NotImplementedError( "Adding steps outside of a proof is not implemented yet" @@ -439,6 +410,56 @@ def proofs(self) -> List[ProofTerm]: """ return self.__proofs + @property + def open_proofs(self) -> List[ProofTerm]: + """Gets all the proofs in the file and their corresponding steps. + + Returns: + List[ProofStep]: Each element has the list of steps for a single + proof of the Coq file. The proofs are ordered by the order + they are written on the file. The steps include the context + used for each step and the goals in that step. + """ + return [ProofTerm(*proof) for proof in self.__open_proofs] + + def exec(self, nsteps=1) -> List[Step]: + """Execute steps in the file. + + Args: + nsteps (int, optional): Number of steps to execute. Defaults to 1. + + Returns: + List[Step]: List of steps executed. + """ + sign = 1 if nsteps > 0 else -1 + initial_steps_taken = self.steps_taken + nsteps = min( + nsteps * sign, + len(self.steps) - self.steps_taken if sign > 0 else self.steps_taken, + ) + + for _ in range(nsteps): + try: + goals = self.current_goals + except Exception as e: + self.__aux_file.close() + raise e + + try: + self._step(sign) + except NotImplementedError as e: + self.steps_taken = initial_steps_taken + raise e + + # FIXME: Handle proof terms and aux_file for negative steps + if sign == 1: + self.__aux_file.append(self.prev_step.text) + self.__check_program() + self.__check_proof_step(goals) + + last, slice = sign == 1, (initial_steps_taken, self.steps_taken) + return self.steps[slice[1 - last] : slice[last]] + def add_step(self, previous_step_index: int, step_text: str): proof, prev = self.__find_prev(self.steps[previous_step_index].ast.range) if prev == -1: diff --git a/coqpyt/tests/test_coq_file.py b/coqpyt/tests/test_coq_file.py index eae7072..0c9255b 100644 --- a/coqpyt/tests/test_coq_file.py +++ b/coqpyt/tests/test_coq_file.py @@ -33,7 +33,7 @@ def test_negative_step(setup, teardown): steps = coq_file.exec(nsteps=8) assert steps[-1].text == "\n Print plus." steps = coq_file.exec(nsteps=-1) - assert steps[0].text == "\n intros n." + assert steps[0].text == "\n Print plus." steps = coq_file.exec(nsteps=-2) with pytest.raises(NotImplementedError): coq_file.exec(nsteps=-1) diff --git a/coqpyt/tests/test_proof_file.py b/coqpyt/tests/test_proof_file.py index 05ecc0b..d0e44dd 100644 --- a/coqpyt/tests/test_proof_file.py +++ b/coqpyt/tests/test_proof_file.py @@ -45,6 +45,7 @@ def setup(request): subprocess.run(f"cd {workspace} && make", shell=True, capture_output=True) uri = "file://" + file_path proof_file = ProofFile(file_path, timeout=60, workspace=workspace) + proof_file.run() versionId = VersionedTextDocumentIdentifier(uri, 1) yield @@ -730,14 +731,17 @@ def test_get_proofs_change_invalid(setup, teardown): @pytest.mark.parametrize("setup", [("test_change_empty.v", None, True)], indirect=True) @pytest.mark.parametrize("teardown", [(True,)], indirect=True) def test_get_proofs_change_empty(setup, teardown): + assert len(proof_file.proofs) == 0 + assert len(proof_file.open_proofs) == 1 + proof_file.add_step(len(proof_file.steps) - 2, "\nAdmitted.") assert proof_file.steps[-2].text == "\nAdmitted." - assert len(proof_file.proofs[0].steps) == 2 - assert proof_file.proofs[0].steps[-1].text == "\nAdmitted." + assert len(proof_file.open_proofs[0].steps) == 2 + assert proof_file.open_proofs[0].steps[-1].text == "\nAdmitted." proof_file.delete_step(len(proof_file.steps) - 2) assert len(proof_file.steps) == 3 - assert len(proof_file.proofs[0].steps) == 1 + assert len(proof_file.open_proofs[0].steps) == 1 @pytest.mark.parametrize( @@ -775,8 +779,8 @@ def test_imports(setup, teardown): @pytest.mark.parametrize("setup", [("test_non_ending_proof.v", None)], indirect=True) def test_non_ending_proof(setup, teardown): - assert len(proof_file.proofs) == 1 - assert len(proof_file.proofs[0].steps) == 3 + assert len(proof_file.open_proofs) == 1 + assert len(proof_file.open_proofs[0].steps) == 3 @pytest.mark.parametrize("setup", [("test_exists_notation.v", None)], indirect=True) @@ -826,7 +830,7 @@ def test_unknown_notation(setup, teardown): @pytest.mark.parametrize("setup", [("test_nested_proofs.v", None)], indirect=True) def test_nested_proofs(setup, teardown): proofs = proof_file.proofs - assert len(proofs) == 4 + assert len(proofs) == 2 steps = ["\n intros n.", "\n simpl; reflexivity.", "\n Qed."] assert len(proofs[0].steps) == len(steps) @@ -846,20 +850,23 @@ def test_nested_proofs(setup, teardown): for i, step in enumerate(proofs[1].steps): assert step.text == steps[i] + proofs = proof_file.open_proofs + assert len(proofs) == 2 + steps = [ "\n intros n.", "\n simpl; reflexivity.", ] - assert len(proofs[2].steps) == 2 - for i, step in enumerate(proofs[2].steps): + assert len(proofs[0].steps) == 2 + for i, step in enumerate(proofs[0].steps): assert step.text == steps[i] steps = [ "\n intros n.", "\n simpl; reflexivity.", ] - assert len(proofs[3].steps) == 2 - for i, step in enumerate(proofs[3].steps): + assert len(proofs[1].steps) == 2 + for i, step in enumerate(proofs[1].steps): assert step.text == steps[i] diff --git a/examples/readme.py b/examples/readme.py index b7ed243..414c349 100644 --- a/examples/readme.py +++ b/examples/readme.py @@ -41,6 +41,7 @@ # Open Proof file with ProofFile(os.path.join(os.getcwd(), "examples/readme.v")) as proof_file: + proof_file.run() # Number of proofs in the file print("Number of proofs:", len(proof_file.proofs)) print("Proof:", proof_file.proofs[0].text) From 71b0a976fe2005f72ade7d5e903edd3474130cc0 Mon Sep 17 00:00:00 2001 From: pcarrott Date: Mon, 13 Nov 2023 04:09:38 +0000 Subject: [PATCH 22/28] Commit from GitHub Actions (Embed code in README) --- README.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 42efd0c..af9bf29 100644 --- a/README.md +++ b/README.md @@ -22,15 +22,16 @@ Import classes from the ``coqpyt`` package. ```py +from coqpyt.coq.structs import TermType from coqpyt.coq.base_file import CoqFile from coqpyt.coq.proof_file import ProofFile -from coqpyt.coq.structs import TermType ``` Create a CoqFile object, execute the file and extract the generated context. ```py +# Open Coq file with CoqFile(os.path.join(os.getcwd(), "examples/readme.v")) as coq_file: coq_file.exec(nsteps=2) # Get all terms defined until now @@ -70,7 +71,9 @@ Create a ProofFile object (a CoqFile instance) and interact with the proofs. ```py +# Open Proof file with ProofFile(os.path.join(os.getcwd(), "examples/readme.v")) as proof_file: + proof_file.run() # Number of proofs in the file print("Number of proofs:", len(proof_file.proofs)) print("Proof:", proof_file.proofs[0].text) From f79887f29c382f59ae5e5a59f9cd03f3a7a6f58e Mon Sep 17 00:00:00 2001 From: pcarrott Date: Mon, 13 Nov 2023 20:55:15 +0000 Subject: [PATCH 23/28] Partial support for backwards steps in ProofFile --- coqpyt/coq/base_file.py | 29 +++---- coqpyt/coq/context.py | 4 +- coqpyt/coq/proof_file.py | 131 +++++++++++++++++++++++--------- coqpyt/coq/structs.py | 4 +- coqpyt/tests/test_proof_file.py | 26 ++++++- 5 files changed, 138 insertions(+), 56 deletions(-) diff --git a/coqpyt/coq/base_file.py b/coqpyt/coq/base_file.py index 57800ca..640c6fb 100644 --- a/coqpyt/coq/base_file.py +++ b/coqpyt/coq/base_file.py @@ -230,6 +230,17 @@ def __update_steps(self): self.__init_steps(text, ast) self.__validate() + def _step(self, sign): + self.steps_taken += sign + # FIXME: for now we ignore the terms in the context when going backwards + # on the file + if sign == 1: + self.context.process_step(self.prev_step) + elif not self.in_proof: + raise NotImplementedError( + "Going backwards outside of a proof is not implemented yet" + ) + def _make_change(self, change_function, *args): previous_steps = self.steps old_steps_taken = self.steps_taken @@ -423,7 +434,7 @@ def in_proof(self) -> bool: bool: True if the current step is inside a proof """ return self.__in_proof(self.current_goals) - + @property def can_close_proof(self): return self._can_close_proof(self.current_goals) @@ -438,17 +449,6 @@ def diagnostics(self) -> List[Diagnostic]: uri = f"file://{self.__path}" return self.coq_lsp_client.lsp_endpoint.diagnostics[uri] - def _step(self, sign): - self.steps_taken += sign - if sign == 1: - self.context.process_step(self.prev_step) - # FIXME: for now we ignore the terms in the context when going backwards - # on the file - elif not self.in_proof: - raise NotImplementedError( - "Going backwards outside of a proof is not implemented yet" - ) - def exec(self, nsteps=1) -> List[Step]: """Execute steps in the file. @@ -465,11 +465,12 @@ def exec(self, nsteps=1) -> List[Step]: len(self.steps) - self.steps_taken if sign > 0 else self.steps_taken, ) - for _ in range(nsteps): + for i in range(nsteps): try: self._step(sign) except NotImplementedError as e: - self.steps_taken = initial_steps_taken + self.steps_taken -= sign # Take back the faulty step + self.exec(nsteps=-sign * i) # Re-take the steps in inverse order raise e last, slice = sign == 1, (initial_steps_taken, self.steps_taken) diff --git a/coqpyt/coq/context.py b/coqpyt/coq/context.py index 8bd97dd..6195380 100644 --- a/coqpyt/coq/context.py +++ b/coqpyt/coq/context.py @@ -91,7 +91,9 @@ def __add_terms(self, step: Step, expr: List): prop = FileContext.get_ident(expr[2][2]) self.__add_term(prop, step, term_type) elif term_type == TermType.OBLIGATION: - self.last_term = Term(step, term_type, self.path, self.__segments.modules[:]) + self.last_term = Term( + step, term_type, self.path, self.__segments.modules[:] + ) else: names = FileContext.__get_names(expr) for name in names: diff --git a/coqpyt/coq/proof_file.py b/coqpyt/coq/proof_file.py index 19c938c..936b9e6 100644 --- a/coqpyt/coq/proof_file.py +++ b/coqpyt/coq/proof_file.py @@ -113,6 +113,12 @@ def append(self, text): with open(self.path, "a") as f: f.write(text) + def truncate(self, text): + text = text.encode("utf-8") + with open(self.path, "rb+") as f: + f.seek(-len(text), os.SEEK_END) + f.truncate() + def didOpen(self): uri = f"file://{self.path}" try: @@ -227,7 +233,9 @@ def __init__( self.__program_context: Dict[str, Tuple[Term, List[Term]]] = {} self.__proofs: List[ProofTerm] = [] - self.__open_proofs: List[Tuple[Term, List[Term], List[ProofStep], Optional[Term]]] = [] + self.__open_proofs: List[ + Tuple[Term, List[Term], List[ProofStep], Optional[Term]] + ] = [] def __enter__(self): return self @@ -324,40 +332,85 @@ def __check_program(self): self.__step_context(self.prev_step), ) - def __check_proof_step(self, goals: GoalAnswer): - # HACK: We ignore proofs inside a Module Type since they can't be used outside - # and should be overriden. - if self.context.in_module_type: - return - if self.prev_step.text.strip() == "": - return - # Steps outside of proofs are ignored - if not self.in_proof and goals.goals is None: - return - # Create proof term when Qed is found - if self.context.expr(self.prev_step)[0] in ["VernacEndProof", "VernacExactProof"]: + def __handle_end_proof(self, step: Step, goals: Optional[GoalAnswer]): + if goals is None: + proof = self.__proofs.pop() + term = Term(proof.step, proof.type, proof.file_path, proof.module) + self.__open_proofs.append( + (term, proof.context, proof.steps[:-1], proof.program) + ) + else: open_proof = self.__open_proofs.pop() - open_proof[2].append(ProofStep(self.prev_step, goals, [])) + open_proof[2].append(ProofStep(step, goals, [])) self.__proofs.append(ProofTerm(*open_proof)) - return - term_type = self.context.term_type(self.prev_step) - # Regular proof steps are added to the last open proof - if term_type == TermType.OTHER: - context = self.__step_context(self.prev_step) - self.__open_proofs[-1][2].append(ProofStep(self.prev_step, goals, context)) - return + def __handle_proof_step(self, step: Step, goals: Optional[GoalAnswer]): + if goals is None: + self.__open_proofs[-1][2].pop() + else: + context = self.__step_context(step) + self.__open_proofs[-1][2].append(ProofStep(step, goals, context)) + + def __handle_proof_term(self, step: Step, goals: Optional[GoalAnswer]): + if goals is None: + self.__open_proofs.pop() + else: + # New proof terms can be either obligations or regular proofs + proof_term, program = self.context.last_term, None + if self.context.term_type(step) == TermType.OBLIGATION: + program, statement_context = self.__get_program_context() + else: + statement_context = self.__step_context(step) + self.__open_proofs.append((proof_term, statement_context, [], program)) + + def __is_proof_term(self, step: Step): + term_type = self.context.term_type(step) # Assume that terms of the following types do not introduce new proofs - if term_type in [TermType.TACTIC, TermType.NOTATION, TermType.INDUCTIVE, TermType.COINDUCTIVE, TermType.RECORD, TermType.CLASS, TermType.SCHEME, TermType.VARIANT]: + # FIXME: Should probably check if [type != OTHER] and if goals were changed + return term_type not in [ + TermType.TACTIC, + TermType.NOTATION, + TermType.INDUCTIVE, + TermType.COINDUCTIVE, + TermType.RECORD, + TermType.CLASS, + TermType.SCHEME, + TermType.VARIANT, + ] + + def __check_proof_step(self, step: Step, goals: Optional[GoalAnswer] = None): + # Last step of the file + if step.text.strip() == "": + return + # FIXME: Forward steps outside of proofs are ignored + # NOTE: CoqFile raises an exception for backward steps + if not self.in_proof and (goals is None or goals.goals is None): return - # New proof terms can be either obligations or regular proofs - proof_term, program = self.context.last_term, None - if term_type == TermType.OBLIGATION: - program, statement_context = self.__get_program_context() - else: - statement_context = self.__step_context(self.prev_step) - self.__open_proofs.append((proof_term, statement_context, [], program)) + # Found [Qed]/[Defined]/[Admitted] or [Proof .] + if self.context.expr(step)[0] in ["VernacEndProof", "VernacExactProof"]: + self.__handle_end_proof(step, goals) + # Regular proof steps for the last open proof + elif self.context.term_type(step) == TermType.OTHER: + self.__handle_proof_step(step, goals) + # FIXME: An exception is raised because we found a term definition + # and CoqFile does not remove the term when stepping backwards + elif goals is None: + raise NotImplementedError( + "Found term definition while going backwards in proof" + ) + # Ignore term definitions that do not generate new proof goals + elif self.__is_proof_term(step): + self.__handle_proof_term(step, goals) + + def __forward_step(self, goals: GoalAnswer): + self.__aux_file.append(self.prev_step.text) + self.__check_program() + self.__check_proof_step(self.prev_step, goals) + + def __backward_step(self): + self.__aux_file.truncate(self.curr_step.text) + self.__check_proof_step(self.curr_step) def __find_step(self, range: Range) -> Optional[Tuple[ProofTerm, int]]: for proof in self.__proofs: @@ -421,7 +474,7 @@ def open_proofs(self) -> List[ProofTerm]: used for each step and the goals in that step. """ return [ProofTerm(*proof) for proof in self.__open_proofs] - + def exec(self, nsteps=1) -> List[Step]: """Execute steps in the file. @@ -437,8 +490,9 @@ def exec(self, nsteps=1) -> List[Step]: nsteps * sign, len(self.steps) - self.steps_taken if sign > 0 else self.steps_taken, ) + step = self.__forward_step if sign == 1 else lambda _: self.__backward_step() - for _ in range(nsteps): + for i in range(nsteps): try: goals = self.current_goals except Exception as e: @@ -446,17 +500,18 @@ def exec(self, nsteps=1) -> List[Step]: raise e try: + # HACK: We ignore steps inside a Module Type since they can't + # be used outside and should be overriden. + in_module_type = self.context.in_module_type self._step(sign) + if in_module_type or self.context.in_module_type: + continue + step(goals) except NotImplementedError as e: - self.steps_taken = initial_steps_taken + self.steps_taken -= sign # Take back the faulty step + self.exec(nsteps=-sign * i) # Re-take the steps in inverse order raise e - # FIXME: Handle proof terms and aux_file for negative steps - if sign == 1: - self.__aux_file.append(self.prev_step.text) - self.__check_program() - self.__check_proof_step(goals) - last, slice = sign == 1, (initial_steps_taken, self.steps_taken) return self.steps[slice[1 - last] : slice[last]] diff --git a/coqpyt/coq/structs.py b/coqpyt/coq/structs.py index 15d1b0c..ae46fda 100644 --- a/coqpyt/coq/structs.py +++ b/coqpyt/coq/structs.py @@ -76,7 +76,7 @@ class Term: def __init__( self, step: Step, - term_type: TermType, + type: TermType, file_path: str, module: List[str], ): @@ -90,7 +90,7 @@ def __init__( module (str): The module where the term is. """ self.step = step - self.type = term_type + self.type = type self.file_path = file_path self.module = module diff --git a/coqpyt/tests/test_proof_file.py b/coqpyt/tests/test_proof_file.py index d0e44dd..e1c77f8 100644 --- a/coqpyt/tests/test_proof_file.py +++ b/coqpyt/tests/test_proof_file.py @@ -827,7 +827,7 @@ def test_unknown_notation(setup, teardown): assert proof_file.context.get_notation("{ _ }", "") -@pytest.mark.parametrize("setup", [("test_nested_proofs.v", None)], indirect=True) +@pytest.mark.parametrize("setup", [("test_nested_proofs.v", None, True)], indirect=True) def test_nested_proofs(setup, teardown): proofs = proof_file.proofs assert len(proofs) == 2 @@ -869,6 +869,30 @@ def test_nested_proofs(setup, teardown): for i, step in enumerate(proofs[1].steps): assert step.text == steps[i] + # Close proofs + proof_file.exec(-1) + proof_file.add_step(proof_file.steps_taken - 1, "\nQed.") + proof_file.add_step(proof_file.steps_taken - 1, "\nQed.") + proof_file.exec(2) + assert len(proof_file.proofs) == 4 + assert len(proof_file.open_proofs) == 0 + + # Re-open proofs + proof_file.exec(-2) + assert len(proof_file.proofs) == 2 + assert len(proof_file.open_proofs) == 2 + + # Attempt to leave proof + with pytest.raises(NotImplementedError): + proof_file.exec(-3) + + # Check rollback + assert len(proof_file.proofs) == 2 + assert len(proof_file.open_proofs) == 2 + proof_file.exec(2) + assert len(proof_file.proofs) == 4 + assert len(proof_file.open_proofs) == 0 + @pytest.mark.parametrize("setup", [("test_theorem_tokens.v", None)], indirect=True) def test_theorem_tokens(setup, teardown): From bf88daf91c3826267786619f930280610c221d0b Mon Sep 17 00:00:00 2001 From: pcarrott Date: Tue, 14 Nov 2023 12:37:47 +0000 Subject: [PATCH 24/28] minor fix to repo name --- setup.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/setup.py b/setup.py index 35199a0..c6436f4 100644 --- a/setup.py +++ b/setup.py @@ -31,7 +31,7 @@ def run_tests(self): description="CoqPyt: a Python client for coq-lsp", long_description=long_description, long_description_content_type="text/markdown", - url="https://github.com/sr-lab/CoqPyt", + url="https://github.com/sr-lab/coqpyt", packages=find_packages(), tests_require=["pytest", "pytest_mock"], cmdclass={"test": PyTest}, From ec298d6d71bb09cef010e6a519857bc3ecd000a3 Mon Sep 17 00:00:00 2001 From: pcarrott Date: Tue, 14 Nov 2023 13:27:31 +0000 Subject: [PATCH 25/28] Update tests.yml --- .github/workflows/test.yml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index a89d537..1e400f7 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -43,4 +43,6 @@ jobs: - name: Run tests run: | - eval $(opam env) && pytest -s \ No newline at end of file + eval $(opam env) + cd coqpyt + pytest tests -s \ No newline at end of file From 6966197ff97b8d998534bf00c82c7641cdf7e8d8 Mon Sep 17 00:00:00 2001 From: pcarrott Date: Tue, 14 Nov 2023 16:24:08 +0000 Subject: [PATCH 26/28] Update readme workflow to run on PR or push to main --- .github/workflows/readme.yml | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/.github/workflows/readme.yml b/.github/workflows/readme.yml index 6947988..1e0b3b7 100644 --- a/.github/workflows/readme.yml +++ b/.github/workflows/readme.yml @@ -2,6 +2,15 @@ name: Embed code in README on: push: + branches: + - master + paths: + - "examples/readme.py" + - "README.md" + pull_request_target: + types: + - opened + - edited paths: - "examples/readme.py" - "README.md" From ec626feda19f7e0ed8e73184571e1a8d7333cd51 Mon Sep 17 00:00:00 2001 From: pcarrott Date: Tue, 14 Nov 2023 17:11:20 +0000 Subject: [PATCH 27/28] Add docstrings --- coqpyt/coq/base_file.py | 18 +++++- coqpyt/coq/context.py | 135 ++++++++++++++++++++++++++------------- coqpyt/coq/proof_file.py | 29 +++------ 3 files changed, 117 insertions(+), 65 deletions(-) diff --git a/coqpyt/coq/base_file.py b/coqpyt/coq/base_file.py index 640c6fb..123a0e2 100644 --- a/coqpyt/coq/base_file.py +++ b/coqpyt/coq/base_file.py @@ -387,10 +387,18 @@ def _change_steps(self, changes: List[CoqChange]): @property def curr_step(self): + """ + Returns: + Step: The next step to be executed. + """ return self.steps[self.steps_taken] @property def prev_step(self): + """ + Returns: + Step: The previously executed step. + """ return self.steps[self.steps_taken - 1] @property @@ -415,7 +423,7 @@ def current_goals(self) -> Optional[GoalAnswer]: """Get goals in current position. Returns: - Optional[GoalAnswer]: Goals in the current position if there are goals + Optional[GoalAnswer]: Goals in the current position if there are goals. """ end_pos = ( Position(0, 0) if self.steps_taken == 0 else self.prev_step.ast.range.end @@ -431,12 +439,16 @@ def current_goals(self) -> Optional[GoalAnswer]: def in_proof(self) -> bool: """ Returns: - bool: True if the current step is inside a proof + bool: True if the current step is inside a proof. """ return self.__in_proof(self.current_goals) @property def can_close_proof(self): + """ + Returns: + bool: True if the next step can be a [Qed]. + """ return self._can_close_proof(self.current_goals) @property @@ -512,7 +524,7 @@ def add_step( Raises: NotImplementedError: If the step added is not on a proof. InvalidFileException: If the file being changed is not valid. - InvalidStepException: If the step added is not valid + InvalidStepException: If the step added is not valid. """ self._make_change(self._add_step, previous_step_index, step_text) diff --git a/coqpyt/coq/context.py b/coqpyt/coq/context.py index 6195380..d552643 100644 --- a/coqpyt/coq/context.py +++ b/coqpyt/coq/context.py @@ -149,7 +149,7 @@ def __handle_where_notations(self, step: Step, expr: List, term_type: TermType): # handles when multiple notations are defined for span in spans: - name = FileContext.get_notation_key( + name = FileContext.__get_notation_key( span[f"{self.__where_notation_key}_string"]["v"], span[f"{self.__where_notation_key}_scope"], ) @@ -162,7 +162,7 @@ def __get_names(expr: List) -> List[str]: stack, res = expr[:0:-1], [] while len(stack) > 0: el = stack.pop() - v = FileContext.get_v(el) + v = FileContext.__get_v(el) if v is not None and isinstance(v, list) and len(v) == 2: id = FileContext.get_id(v) if id is not None: @@ -191,6 +191,40 @@ def __get_names(expr: List) -> List[str]: stack.append(v) return res + @staticmethod + def get_id(id: List) -> Optional[str]: + # FIXME: This should be made private once [__step_context] is extracted + # from ProofFile to here. + if id[0] == "Ser_Qualid": + return ".".join([l[1] for l in reversed(id[1][1])] + [id[2][1]]) + elif id[0] == "Id": + return id[1] + return None + + @staticmethod + def get_ident(el: List) -> Optional[str]: + # FIXME: This should be made private once [__get_program_context] is extracted + # from ProofFile to here. + if ( + len(el) == 3 + and el[0] == "GenArg" + and el[1][0] == "Rawwit" + and el[1][1][0] == "ExtraArg" + ): + if el[1][1][1] == "identref": + return el[2][0][1][1] + elif el[1][1][1] == "ident": + return el[2][1] + return None + + @staticmethod + def __get_v(el: List) -> Optional[str]: + if isinstance(el, dict) and "v" in el: + return el["v"] + elif isinstance(el, list) and len(el) == 2 and el[0] == "v": + return el[1] + return None + @staticmethod def __term_type(expr: List) -> TermType: if expr[0] == "VernacStartTheoremProof": @@ -233,6 +267,12 @@ def __term_type(expr: List) -> TermType: return TermType.FUNCTION return TermType.OTHER + @staticmethod + def __get_notation_key(notation: str, scope: str) -> str: + if scope != "" and scope is not None: + notation += " : " + scope + return notation + @property def local_terms(self) -> List[Term]: """ @@ -245,9 +285,19 @@ def local_terms(self) -> List[Term]: @property def in_module_type(self) -> bool: + """ + Returns: + bool: True if currently inside a module type. + """ return len(self.__segments.module_types) > 0 def process_step(self, step: Step): + """Extracts the identifiers from a step and updates the context with + new terms defined by the step. + + Args: + step (Step): The step to be processed. + """ expr = self.expr(step) if ( expr == [None] @@ -270,7 +320,14 @@ def process_step(self, step: Step): elif not self.in_module_type: self.__add_terms(step, expr) - def expr(self, step: Step) -> Optional[List]: + def expr(self, step: Step) -> List: + """ + Args: + step (Step): The step to be processed. + + Returns: + List: 'expr' field from the AST of a step. + """ if ( step.ast.span is not None and isinstance(step.ast.span, dict) @@ -282,15 +339,43 @@ def expr(self, step: Step) -> Optional[List]: return [None] def term_type(self, step: Step) -> TermType: + """ + Args: + step (Step): The step to be processed. + + Returns: + List: The term type of the step. + """ return FileContext.__term_type(self.expr(step)) def update(self, terms: Dict[str, Term] = {}): + """Updates the context with new terms. + + Args: + terms (Dict[str, Term]): The new terms to be added. + """ self.terms.update(terms) def append_module_prefix(self, name: str) -> str: + """Attaches the current module path to the start of a name. + + Args: + name (str): The name. + + Returns: + str: The full name with the module path. + """ return ".".join(self.__segments.modules + [name]) def get_term(self, name: str) -> Optional[Term]: + """Get a notation from the context. + + Args: + name (str): The term name. + + Returns: + Optional[Term]: The term mapped to the name, if it exists. + """ for i in range(len(self.__segments.modules), -1, -1): curr_name = ".".join(self.__segments.modules[:i] + [name]) if curr_name in self.terms: @@ -301,8 +386,8 @@ def get_notation(self, notation: str, scope: str) -> Term: """Get a notation from the context. Args: - notation (str): Id of the notation. E.g. "_ + _" - scope (str): Scope of the notation. E.g. "nat_scope" + notation (str): Id of the notation. E.g. "_ + _". + scope (str): Scope of the notation. E.g. "nat_scope". Raises: RuntimeError: If the notation is not found in the context. @@ -310,7 +395,7 @@ def get_notation(self, notation: str, scope: str) -> Term: Returns: Term: Term that corresponds to the notation. """ - notation_id = FileContext.get_notation_key(notation, scope) + notation_id = FileContext.__get_notation_key(notation, scope) regex = f"{re.escape(notation_id)}".split("\\ ") for i, sub in enumerate(regex): if sub == "_": @@ -338,44 +423,8 @@ def get_notation(self, notation: str, scope: str) -> Term: # Search Infix if re.match("^_ ([^ ]*) _$", notation): op = notation[2:-2] - key = FileContext.get_notation_key(op, scope) + key = FileContext.__get_notation_key(op, scope) if key in self.terms: return self.terms[key] raise NotationNotFoundException(notation_id) - - @staticmethod - def get_notation_key(notation: str, scope: str) -> str: - if scope != "" and scope is not None: - notation += " : " + scope - return notation - - @staticmethod - def get_id(id: List) -> Optional[str]: - if id[0] == "Ser_Qualid": - return ".".join([l[1] for l in reversed(id[1][1])] + [id[2][1]]) - elif id[0] == "Id": - return id[1] - return None - - @staticmethod - def get_ident(el: List) -> Optional[str]: - if ( - len(el) == 3 - and el[0] == "GenArg" - and el[1][0] == "Rawwit" - and el[1][1][0] == "ExtraArg" - ): - if el[1][1][1] == "identref": - return el[2][0][1][1] - elif el[1][1][1] == "ident": - return el[2][1] - return None - - @staticmethod - def get_v(el: List) -> Optional[str]: - if isinstance(el, dict) and "v" in el: - return el["v"] - elif isinstance(el, list) and len(el) == 2 and el[0] == "v": - return el[1] - return None diff --git a/coqpyt/coq/proof_file.py b/coqpyt/coq/proof_file.py index 936b9e6..8922c90 100644 --- a/coqpyt/coq/proof_file.py +++ b/coqpyt/coq/proof_file.py @@ -453,37 +453,29 @@ def __get_step(self, step_index): @property def proofs(self) -> List[ProofTerm]: - """Gets all the proofs in the file and their corresponding steps. + """Gets all the closed proofs in the file and their corresponding steps. Returns: - List[ProofStep]: Each element has the list of steps for a single - proof of the Coq file. The proofs are ordered by the order - they are written on the file. The steps include the context - used for each step and the goals in that step. + List[ProofTerm]: Each element has the list of steps for a single + closed proof of the Coq file. The proofs are ordered by the + order they are closed on the file. The steps include the + context used for each step and the goals in that step. """ return self.__proofs @property def open_proofs(self) -> List[ProofTerm]: - """Gets all the proofs in the file and their corresponding steps. + """Gets all the open proofs in the file and their corresponding steps. Returns: - List[ProofStep]: Each element has the list of steps for a single - proof of the Coq file. The proofs are ordered by the order - they are written on the file. The steps include the context - used for each step and the goals in that step. + List[ProofTerm]: Each element has the list of steps for a single + open proof of the Coq file. The proofs are ordered by the + order they are opened on the file. The steps include the + context used for each step and the goals in that step. """ return [ProofTerm(*proof) for proof in self.__open_proofs] def exec(self, nsteps=1) -> List[Step]: - """Execute steps in the file. - - Args: - nsteps (int, optional): Number of steps to execute. Defaults to 1. - - Returns: - List[Step]: List of steps executed. - """ sign = 1 if nsteps > 0 else -1 initial_steps_taken = self.steps_taken nsteps = min( @@ -586,6 +578,5 @@ def change_steps(self, changes: List[CoqChange]): raise InvalidChangeException() def close(self): - """Closes all resources used by this object.""" super().close() self.__aux_file.close() From 7e2248621d38564f4ba6b42d830860c8c3d87977 Mon Sep 17 00:00:00 2001 From: pcarrott Date: Tue, 14 Nov 2023 17:33:28 +0000 Subject: [PATCH 28/28] Pre-ProofTerm alias --- coqpyt/coq/proof_file.py | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/coqpyt/coq/proof_file.py b/coqpyt/coq/proof_file.py index 8922c90..1097749 100644 --- a/coqpyt/coq/proof_file.py +++ b/coqpyt/coq/proof_file.py @@ -21,6 +21,9 @@ from coqpyt.coq.base_file import CoqFile +_ProofTerm: Tuple[Term, List[Term], List[ProofStep], Optional[Term]] + + class _AuxFile(object): __CACHE: Dict[Tuple[str, str], FileContext] = {} @@ -233,9 +236,7 @@ def __init__( self.__program_context: Dict[str, Tuple[Term, List[Term]]] = {} self.__proofs: List[ProofTerm] = [] - self.__open_proofs: List[ - Tuple[Term, List[Term], List[ProofStep], Optional[Term]] - ] = [] + self.__open_proofs: List[_ProofTerm] = [] def __enter__(self): return self @@ -335,9 +336,8 @@ def __check_program(self): def __handle_end_proof(self, step: Step, goals: Optional[GoalAnswer]): if goals is None: proof = self.__proofs.pop() - term = Term(proof.step, proof.type, proof.file_path, proof.module) self.__open_proofs.append( - (term, proof.context, proof.steps[:-1], proof.program) + (proof, proof.context, proof.steps[:-1], proof.program) ) else: open_proof = self.__open_proofs.pop() @@ -382,7 +382,7 @@ def __check_proof_step(self, step: Step, goals: Optional[GoalAnswer] = None): # Last step of the file if step.text.strip() == "": return - # FIXME: Forward steps outside of proofs are ignored + # Forward steps outside of proofs are ignored # NOTE: CoqFile raises an exception for backward steps if not self.in_proof and (goals is None or goals.goals is None): return