Skip to content

Commit

Permalink
Merge pull request #8 from proux01/coq_elpi_2
Browse files Browse the repository at this point in the history 
Adapt to coq-elpi 2.0.0
  • Loading branch information
@ecranceMERCE
ecranceMERCE authored Jan 11, 2024
2 parents ca25c04 + 608b564 commit d909d02
Show file tree
Hide file tree
Showing 2 changed files with 41 additions and 26 deletions.
10 changes: 7 additions & 3 deletions theories/Commands.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,13 +13,17 @@ From elpi Require Import elpi.

From Trakt Require Import InternalProofs.

From Trakt.Elpi Extra Dependency "types.elpi" as types.
From Trakt.Elpi Extra Dependency "common.elpi" as common.
From Trakt.Elpi Extra Dependency "commands.elpi" as commands.

Elpi Command Trakt.

Elpi Query lp:{{
coq.option.add ["trakt.verbosity"] (coq.option.int (some 0)) ff.
}}.

Elpi Accumulate File "types.elpi" From Trakt.Elpi.
Elpi Accumulate File types.
Elpi Typecheck.

From Trakt Require Export Database.
Expand All @@ -28,10 +32,10 @@ Elpi Accumulate Db symbols.db.
Elpi Accumulate Db relations.db.
Elpi Accumulate Db conversion.db.

Elpi Accumulate File "common.elpi" From Trakt.Elpi.
Elpi Accumulate File common.
Elpi Typecheck.

Elpi Accumulate File "commands.elpi" From Trakt.Elpi.
Elpi Accumulate File commands.
Elpi Typecheck.

Elpi Accumulate lp:{{
Expand Down
57 changes: 34 additions & 23 deletions theories/Tactic.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,21 +14,32 @@ From elpi Require Import elpi.
From Trakt Require Import InternalProofs.
From Trakt Require Export Database.

From Trakt.Elpi Extra Dependency "types.elpi" as types.
From Trakt.Elpi Extra Dependency "common.elpi" as common.
From Trakt.Elpi Extra Dependency "proof.elpi" as proof.
From Trakt.Elpi Extra Dependency "rewrite-identities.elpi" as rewrite_identities.
From Trakt.Elpi Extra Dependency "preprocess.elpi" as preprocess.
From Trakt.Elpi Extra Dependency "generalise-free-variables.elpi" as generalise_free_variables.
From Trakt.Elpi Extra Dependency "bool-to-prop.elpi" as bool_to_prop.
From Trakt.Elpi Extra Dependency "tactic.elpi" as tactic.
From Trakt.Elpi Extra Dependency "boolify-arrows.elpi" as boolify_arrows.
From Trakt.Elpi Extra Dependency "reorder-quantifiers.elpi" as reorder_quantifiers.

Elpi Tactic trakt.

Elpi Accumulate File "types.elpi" From Trakt.Elpi.
Elpi Accumulate File types.
Elpi Accumulate Db embeddings.db.
Elpi Accumulate Db logic.db.
Elpi Accumulate Db symbols.db.
Elpi Accumulate Db relations.db.
Elpi Accumulate Db conversion.db.
Elpi Accumulate File "common.elpi" From Trakt.Elpi.
Elpi Accumulate File "proof.elpi" From Trakt.Elpi.
Elpi Accumulate File "rewrite-identities.elpi" From Trakt.Elpi.
Elpi Accumulate File "preprocess.elpi" From Trakt.Elpi.
Elpi Accumulate File "generalise-free-variables.elpi" From Trakt.Elpi.
Elpi Accumulate File "bool-to-prop.elpi" From Trakt.Elpi.
Elpi Accumulate File "tactic.elpi" From Trakt.Elpi.
Elpi Accumulate File common.
Elpi Accumulate File proof.
Elpi Accumulate File rewrite_identities.
Elpi Accumulate File preprocess.
Elpi Accumulate File generalise_free_variables.
Elpi Accumulate File bool_to_prop.
Elpi Accumulate File tactic.
Elpi Accumulate lp:{{
solve InitialGoal NewGoals :-
InitialGoal = goal Context _ InitialGoalTy _ [trm ETarget, trm LTarget, trm RuntimeRelData],
Expand Down Expand Up @@ -81,19 +92,19 @@ Tactic Notation "trakt" constr(logic_target) :=

Elpi Tactic trakt_pose.

Elpi Accumulate File "types.elpi" From Trakt.Elpi.
Elpi Accumulate File types.
Elpi Accumulate Db embeddings.db.
Elpi Accumulate Db logic.db.
Elpi Accumulate Db symbols.db.
Elpi Accumulate Db relations.db.
Elpi Accumulate Db conversion.db.
Elpi Accumulate File "common.elpi" From Trakt.Elpi.
Elpi Accumulate File "proof.elpi" From Trakt.Elpi.
Elpi Accumulate File "rewrite-identities.elpi" From Trakt.Elpi.
Elpi Accumulate File "preprocess.elpi" From Trakt.Elpi.
Elpi Accumulate File "generalise-free-variables.elpi" From Trakt.Elpi.
Elpi Accumulate File "bool-to-prop.elpi" From Trakt.Elpi.
Elpi Accumulate File "tactic.elpi" From Trakt.Elpi.
Elpi Accumulate File common.
Elpi Accumulate File proof.
Elpi Accumulate File rewrite_identities.
Elpi Accumulate File preprocess.
Elpi Accumulate File generalise_free_variables.
Elpi Accumulate File bool_to_prop.
Elpi Accumulate File tactic.
Elpi Accumulate lp:{{
solve Goal NewGoals :-
Goal = goal _ _ GoalTy _ [trm ETarget, trm LTarget, trm H, str S, trm RuntimeRelData],
Expand Down Expand Up @@ -165,11 +176,11 @@ Tactic Notation "trakt_pose"

Elpi Tactic trakt_boolify_arrows.

Elpi Accumulate File "types.elpi" From Trakt.Elpi.
Elpi Accumulate File types.
Elpi Accumulate Db logic.db.
Elpi Accumulate File "common.elpi" From Trakt.Elpi.
Elpi Accumulate File "proof.elpi" From Trakt.Elpi.
Elpi Accumulate File "boolify-arrows.elpi" From Trakt.Elpi.
Elpi Accumulate File common.
Elpi Accumulate File proof.
Elpi Accumulate File boolify_arrows.
Elpi Accumulate lp:{{
solve ((goal _ _ GoalTy _ []) as InitialGoal) NewGoals :- !, std.do! [
coq.elaborate-skeleton GoalTy _ EGoalTy ok,
Expand All @@ -187,9 +198,9 @@ Tactic Notation "trakt_boolify_arrows" := elpi trakt_boolify_arrows.

Elpi Tactic trakt_reorder_quantifiers.

Elpi Accumulate File "types.elpi" From Trakt.Elpi.
Elpi Accumulate File "common.elpi" From Trakt.Elpi.
Elpi Accumulate File "reorder-quantifiers.elpi" From Trakt.Elpi.
Elpi Accumulate File types.
Elpi Accumulate File common.
Elpi Accumulate File reorder_quantifiers.
Elpi Accumulate lp:{{
solve ((goal _ _ GoalTy _ []) as InitialGoal) NewGoals :- !, std.do! [
coq.elaborate-skeleton GoalTy _ EGoalTy ok,
Expand Down

0 comments on commit d909d02

Please sign in to comment.