Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

adapt to elpi 2.0 #15

Merged
merged 1 commit into from
Nov 29, 2024
Merged

adapt to elpi 2.0 #15

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion elpi/commands.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -107,7 +107,7 @@ add-embedding Args :-
"expected: ", {coq.term->string ExpectedEmbedThenInvIdT},
"\ngot: ", {coq.term->string EmbedThenInvIdT}, "\n\n"
]},
pi y\ pi z\ copy (app [Embed, y]) z => copy (CondF y) (CondFE z),
pi y\ pi z\ (copy (app [Embed, y]) z => copy (CondF y) (CondFE z)),
ExpectedInvThenEmbedCondIdT =
{{ forall (x' : lp:T'), lp:(CondFE x') -> @eq lp:T' (lp:Embed (lp:EmbedInv x')) x' }},
pi x'\
Expand Down
2 changes: 1 addition & 1 deletion elpi/generalise_free_variables.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ find-free-variables.aux {{ lp:A -> lp:B }} ETargetOpt Context FVInfoSet :- !,
set-merge FVInfoSetA FVInfoSetB FVInfoSet.

find-free-variables.aux (prod _ T F) ETargetOpt Context FVInfoSet' :- !,
pi x\ decl x _ T => find-free-variables.aux (F x) ETargetOpt Context (FVInfoSet x),
pi x\ (decl x _ T => find-free-variables.aux (F x) ETargetOpt Context (FVInfoSet x)),
std.set.remove (pr x _) (FVInfoSet x) FVInfoSet'.

find-free-variables.aux (app [F|Args]) ETargetOpt Context FVInfoSet' :- !,
Expand Down
6 changes: 3 additions & 3 deletions elpi/preprocess.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -113,11 +113,11 @@ preprocess (prod N T F) ETargetOpt LTarget TVar _ OutTerm Proof :- !,
% inverse lemmas, but some embedding identities must be removed
make-reverse-embedding-context FunT ETarget REF,
std.map.make cmp_term EmptyMap,
pi x'\ decl x' _ T' => (
pi x'\ (decl x' _ T' ==>
beta-reduce (F' (REF x')) (BF x'),
if (CondFOpt = some CondF) (
% there will be a condition in the final proof
pi c\ decl c _ (CondF x') => (
pi c\ (decl c _ (CondF x') ==>
std.map.add x' c EmptyMap (CondProofs x' c),
rewrite-identities (BF x') ETarget LTarget (CondProofs x' c) (RwProofC x' c),
clear-custom-terms-in-proof (RwProofC x' c) (RwProofC' x' c),
Expand Down Expand Up @@ -725,7 +725,7 @@ pred generalise
generalise X Term FT ETarget F' :-
pi x\
% first replace X with a fresh variable
copy X x => copy Term (F x),
(copy X x => copy Term (F x)),
% then remove embedding functions around this variable everywhere in the term
remove-embeddings-around x (F x) FT ETarget (F' x).

Expand Down
6 changes: 3 additions & 3 deletions elpi/proof.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ build.aux (proof.none T) {{ @id lp:T }}.
build.aux (proof.of-term Term) Term.

build.aux (proof.forall T PF CoqProofF) CoqProof :-
pi x\ decl x _ T =>
pi x\ decl x _ T ==>
build.aux (PF x) (CoqPF x),
if (CoqPF x = {{ id }}) (
copy (app [{{ id }}, X]) X => copy (CoqProofF CoqPF) CoqProof
Expand All @@ -68,8 +68,8 @@ build.aux (proof.forall T PF CoqProofF) CoqProof :-
).

build.aux (proof.forall2 T U PF CoqProofF) CoqProof :-
pi x\ decl x _ T =>
pi y\ decl y _ (U x) =>
pi x\ decl x _ T ==>
pi y\ decl y _ (U x) ==>
build.aux (PF x y) (CoqPF x y),
if (CoqPF x y = {{ id }}) (
copy (app [{{ id }}, X]) X => copy (CoqProofF CoqPF) CoqProof
Expand Down
2 changes: 1 addition & 1 deletion elpi/reorder_quantifiers.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ pred bind-back i:list term, i:term, o:term.
bind-back [] Term Term.

bind-back [X|Xs] Term Term' :-
pi x\ copy X x => copy Term (F x), !,
(pi x\ copy X x => copy Term (F x)), !,
bind-back Xs (fun _ _ F) Term'.

% pop a list of hypotheses in front of a type
Expand Down
4 changes: 0 additions & 4 deletions theories/Commands.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,6 @@ Elpi Query lp:{{
}}.

Elpi Accumulate File types.
Elpi Typecheck.

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

Elpi Accumulate File common.
Elpi Typecheck.

Elpi Accumulate File commands.
Elpi Typecheck.

Elpi Accumulate lp:{{
pred elaborate-argument i:argument, o:argument.
Expand Down Expand Up @@ -68,5 +65,4 @@ Elpi Accumulate lp:{{
" | Trakt Set Verbosity (0|1|2)", "", ""
]}.
}}.
Elpi Typecheck.
Elpi Export Trakt.
15 changes: 13 additions & 2 deletions theories/Database.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,11 @@
intros []; cbv [negb]; auto.
Qed.

Elpi Db logic.db lp:{{
From Trakt.Elpi Extra Dependency "types.elpi" as types.

Elpi Db logic.db lp:{{ }}.
Elpi Accumulate logic.db File Signature types.

Check failure on line 78 in theories/Database.v

View workflow job for this annotation

GitHub Actions / master (8.19) / from-sources 

Anomaly "wtf" Please report at http://coq.inria.fr/bugs/.
Elpi Accumulate logic.db lp:{{
logical-connector
{{ and }} {{ andb }} [covariant, covariant]
{{ and_impl_morphism }} {{ andb_and_impl }} {{ and_andb_impl }}.
Expand Down Expand Up @@ -106,6 +110,13 @@
Qed.

Elpi Db embeddings.db lp:{{ }}.
Elpi Accumulate embeddings.db File Signature types.

Elpi Db symbols.db lp:{{ }}.
Elpi Accumulate symbols.db File Signature types.

Elpi Db relations.db lp:{{ }}.
Elpi Db conversion.db lp:{{ }}.
Elpi Accumulate relations.db File Signature types.

Elpi Db conversion.db lp:{{ }}.
Elpi Accumulate conversion.db File Signature types.
36 changes: 16 additions & 20 deletions theories/Tactic.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,36 +47,35 @@ Elpi Accumulate lp:{{
std.assert! (format-runtime-relation-data RuntimeRelData RuntimeRelCtx)
"wrong runtime relations format",
RuntimeRelCtx =>
preprocess-extra InitialGoalTy Context (some ETarget) LTarget covariant true EndGoalTy Proof,
refine {{ lp:Proof (_ : lp:EndGoalTy) }} InitialGoal NewGoals.
(preprocess-extra InitialGoalTy Context (some ETarget) LTarget covariant true EndGoalTy Proof,
refine {{ lp:Proof (_ : lp:EndGoalTy) }} InitialGoal NewGoals).

solve InitialGoal NewGoals :-
InitialGoal = goal Context _ InitialGoalTy _ [trm ETarget, trm LTarget],
(LTarget = {{ Prop }} ; LTarget = {{ bool }}), !,
[] =>
preprocess-extra InitialGoalTy Context (some ETarget) LTarget covariant true EndGoalTy Proof,
refine {{ lp:Proof (_ : lp:EndGoalTy) }} InitialGoal NewGoals.
(preprocess-extra InitialGoalTy Context (some ETarget) LTarget covariant true EndGoalTy Proof,
refine {{ lp:Proof (_ : lp:EndGoalTy) }} InitialGoal NewGoals).

solve InitialGoal NewGoals :-
InitialGoal = goal Context _ InitialGoalTy _ [trm LTarget, trm RuntimeRelData],
(LTarget = {{ Prop }} ; LTarget = {{ bool }}), !,
std.assert! (format-runtime-relation-data RuntimeRelData RuntimeRelCtx)
"wrong runtime relations format",
RuntimeRelCtx =>
preprocess-extra InitialGoalTy Context none LTarget covariant true EndGoalTy Proof,
refine {{ lp:Proof (_ : lp:EndGoalTy) }} InitialGoal NewGoals.
(preprocess-extra InitialGoalTy Context none LTarget covariant true EndGoalTy Proof,
refine {{ lp:Proof (_ : lp:EndGoalTy) }} InitialGoal NewGoals).

solve InitialGoal NewGoals :-
InitialGoal = goal Context _ InitialGoalTy _ [trm LTarget],
(LTarget = {{ Prop }} ; LTarget = {{ bool }}), !,
[] =>
preprocess-extra InitialGoalTy Context none LTarget covariant true EndGoalTy Proof,
refine {{ lp:Proof (_ : lp:EndGoalTy) }} InitialGoal NewGoals.
(preprocess-extra InitialGoalTy Context none LTarget covariant true EndGoalTy Proof,
refine {{ lp:Proof (_ : lp:EndGoalTy) }} InitialGoal NewGoals).

solve _ _ :-
coq.error "usage: trakt [target embedding type] <bool|Prop> [with rel <relations>]".
}}.
Elpi Typecheck.

Tactic Notation "trakt" constr(target) constr(logic_target) "with" "rel" constr(l) :=
elpi trakt ltac_term:(target) ltac_term:(logic_target) ltac_term:(l).
Expand Down Expand Up @@ -115,8 +114,8 @@ Elpi Accumulate lp:{{
"wrong runtime relations format",
coq.typecheck H T ok,
RuntimeRelCtx =>
preprocess-extra T [] (some ETarget) LTarget contravariant false T' P,
refine (let Name T' (app [P, H]) (t\ {{ _ : lp:GoalTy }})) Goal NewGoals.
(preprocess-extra T [] (some ETarget) LTarget contravariant false T' P,
refine (let Name T' (app [P, H]) (t\ {{ _ : lp:GoalTy }})) Goal NewGoals).

solve Goal NewGoals :-
Goal = goal _ _ GoalTy _ [trm ETarget, trm LTarget, trm H, str S],
Expand All @@ -125,8 +124,8 @@ Elpi Accumulate lp:{{
coq.string->name S Name,
coq.typecheck H T ok,
[] =>
preprocess-extra T [] (some ETarget) LTarget contravariant false T' P,
refine (let Name T' (app [P, H]) (t\ {{ _ : lp:GoalTy }})) Goal NewGoals.
(preprocess-extra T [] (some ETarget) LTarget contravariant false T' P,
refine (let Name T' (app [P, H]) (t\ {{ _ : lp:GoalTy }})) Goal NewGoals).

solve Goal NewGoals :-
Goal = goal _ _ GoalTy _ [trm LTarget, trm H, str S, trm RuntimeRelData],
Expand All @@ -137,8 +136,8 @@ Elpi Accumulate lp:{{
"wrong runtime relations format",
coq.typecheck H T ok,
RuntimeRelCtx =>
preprocess-extra T [] none LTarget contravariant false T' P,
refine (let Name T' (app [P, H]) (t\ {{ _ : lp:GoalTy }})) Goal NewGoals.
(preprocess-extra T [] none LTarget contravariant false T' P,
refine (let Name T' (app [P, H]) (t\ {{ _ : lp:GoalTy }})) Goal NewGoals).

solve Goal NewGoals :-
Goal = goal _ _ GoalTy _ [trm LTarget, trm H, str S],
Expand All @@ -147,8 +146,8 @@ Elpi Accumulate lp:{{
coq.string->name S Name,
coq.typecheck H T ok,
[] =>
preprocess-extra T [] none LTarget contravariant false T' P,
refine (let Name T' (app [P, H]) (t\ {{ _ : lp:GoalTy }})) Goal NewGoals.
(preprocess-extra T [] none LTarget contravariant false T' P,
refine (let Name T' (app [P, H]) (t\ {{ _ : lp:GoalTy }})) Goal NewGoals).

solve _ _ :-
coq.error {std.string.concat "\n" [
Expand All @@ -158,7 +157,6 @@ Elpi Accumulate lp:{{
" [with rel <relations>]"
]}.
}}.
Elpi Typecheck.

Tactic Notation "trakt_pose" constr(et) constr(lt) ":" constr(h) "as" ident(s) :=
elpi trakt_pose ltac_term:(et) ltac_term:(lt) ltac_term:(h) ltac_string:(s).
Expand Down Expand Up @@ -192,7 +190,6 @@ Elpi Accumulate lp:{{
solve _ _ :-
coq.error "usage: trakt_boolify_arrows.".
}}.
Elpi Typecheck.

Tactic Notation "trakt_boolify_arrows" := elpi trakt_boolify_arrows.

Expand All @@ -212,6 +209,5 @@ Elpi Accumulate lp:{{
solve _ _ :-
coq.error "usage: trakt_reorder_quantifiers.".
}}.
Elpi Typecheck.

Tactic Notation "trakt_reorder_quantifiers" := elpi trakt_reorder_quantifiers.
Loading