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

Cswb #591

Open
wants to merge 15 commits into
base: master
Choose a base branch
from
Open

Cswb #591

Changes from 1 commit
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
729a216
update hook (due to hook call update in coq)
Nov 2, 2023
edc76b4
add retyping after coercion (due to a modification in coq)
Nov 2, 2023
b204381
added tests
Nov 2, 2023
b333090
fixed naming
Nov 13, 2023
44b52f3
wip
Tragicus Jan 9, 2024
3725a99
add no-tc attribute support for typecheck and unification
Tragicus Jan 17, 2024
a58c201
Add of the expose grafting + test
FissoreD Jan 11, 2024
402b410
complete and compiles
Tragicus Feb 6, 2024
1d39142
new cs hook
Tragicus Feb 8, 2024
ea4f6d3
fix Elpi Typecheck program
gares Jan 9, 2024
e965d37
Merge branch 'master' into cswb
gares Feb 8, 2024
2ce9d16
add coq.reduction.lazy.whd_betaiota_deltazeta_for_iota_state
Tragicus Feb 21, 2024
0cda7be
fix evarconv
Tragicus Feb 21, 2024
bb0cd52
Enable loading db from files
proux01 Feb 21, 2024
38afaf3
Enable creating Db without initial code
proux01 Feb 21, 2024
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
15 changes: 15 additions & 0 deletions src/coq_elpi_builtins.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3382,6 +3382,21 @@ Supported attributes:
!: t)),
DocAbove);

MLCode(Pred("coq.reduction.lazy.whd_betaiota_deltazeta_for_iota_state",
CIn(term,"T",
COut(term,"Tred",
Read(proof_context, {|Puts T in weak head normal form.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have no clue what it does, but it does not do "just whd" ;-)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Indeed, thank you. Is there a difference between "weak head normal form" and "head normal form"? If so, the documentation of whd_betaiota_deltazeta_for_iota_state in reductionops.ml states "head normal form", while the function name starts with "whd", is that a typo?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Also, would you like for me to PR this commit (after fixing the doc) to coq-elpi now?

Supported attributes:
- @redflags! (default coq.redflags.all)|}))),
(fun t _ ~depth proof_context constraints state ->
let sigma = get_sigma state in
let flags = Option.default RedFlags.all proof_context.options.redflags in
let t, sk = EConstr.decompose_app sigma t in
let t, sk = Reductionops.whd_betaiota_deltazeta_for_iota_state (RedFlags.red_transparent flags) proof_context.env sigma (t, Reductionops.Stack.append_app sk Reductionops.Stack.empty) in
let t = Reductionops.Stack.zip sigma (t, sk) in
!: t)),
DocAbove);

MLCode(Pred("coq.reduction.lazy.norm",
CIn(term,"T",
COut(term,"Tred",
Expand Down
Loading