From d47bbd7c1dec4c202a4611273a8bfb33803e1308 Mon Sep 17 00:00:00 2001 From: Patrick Nicodemus Date: Wed, 21 Aug 2024 16:16:23 -0400 Subject: [PATCH 1/3] Removed dependency on stdlib --- builtin-doc/coq-builtin.elpi | 4 ++-- builtin-doc/elpi-builtin.elpi | 3 +++ elpi/dune | 5 ++++- 3 files changed, 9 insertions(+), 3 deletions(-) diff --git a/builtin-doc/coq-builtin.elpi b/builtin-doc/coq-builtin.elpi index e3d07ce69..a5d9b2b81 100644 --- a/builtin-doc/coq-builtin.elpi +++ b/builtin-doc/coq-builtin.elpi @@ -558,8 +558,8 @@ external pred coq.version o:string, o:int, o:int, o:int. % To make the API more precise we use different data types for the names % of global objects. -% Note: [ctype \"bla\"] is an opaque data type and by convention it is -% written [@bla]. +% Note: [ctype "bla"] is an opaque data type and by convention it is written +% [@bla]. % Global constant name typeabbrev constant (ctype "constant"). diff --git a/builtin-doc/elpi-builtin.elpi b/builtin-doc/elpi-builtin.elpi index c59c1dc1f..2b32eedae 100644 --- a/builtin-doc/elpi-builtin.elpi +++ b/builtin-doc/elpi-builtin.elpi @@ -449,6 +449,9 @@ pred ignore-failure! i:prop. ignore-failure! P :- P, !. ignore-failure! _. +pred once i:prop. +once P :- P, !. + % [assert! C M] takes the first success of C or fails with message M pred assert! i:prop, i:string. assert! Cond Msg :- (Cond ; fatal-error-w-data Msg Cond), !. diff --git a/elpi/dune b/elpi/dune index 7c74d7fbc..57a668cb1 100644 --- a/elpi/dune +++ b/elpi/dune @@ -1,6 +1,9 @@ (coq.theory (name elpi_elpi) ; FIXME - (package coq-elpi)) + (package coq-elpi) + (stdlib no) + (theories Coq) + ) (rule (target dummy.v) From 1359ed2502b48074639bba561f6ff0627b6657fd Mon Sep 17 00:00:00 2001 From: Patrick Nicodemus Date: Wed, 21 Aug 2024 17:16:22 -0400 Subject: [PATCH 2/3] Removed stdlib --- examples/dune | 4 +++- examples/example_abs_evars.v | 1 + examples/example_curry_howard_tactics.v | 1 + examples/example_fuzzer.v | 3 ++- examples/example_generalize.v | 1 + examples/example_import_projections.v | 1 + examples/example_record_expansion.v | 1 + examples/example_record_to_sigma.v | 1 + examples/example_reduction_surgery.v | 1 + examples/example_reflexive_tactic.v | 1 + examples/tutorial_coq_elpi_HOAS.v | 1 + examples/tutorial_coq_elpi_command.v | 1 + examples/tutorial_coq_elpi_tactic.v | 1 + 13 files changed, 16 insertions(+), 2 deletions(-) diff --git a/examples/dune b/examples/dune index 9a7bee3cd..a5d785173 100644 --- a/examples/dune +++ b/examples/dune @@ -2,6 +2,8 @@ (package coq-elpi) (name elpi_examples) (plugins coq-elpi.elpi) - (theories elpi)) + (theories elpi Coq) + (stdlib no) + ) ; (include_subdirs qualified) diff --git a/examples/example_abs_evars.v b/examples/example_abs_evars.v index f9879ee37..626681329 100644 --- a/examples/example_abs_evars.v +++ b/examples/example_abs_evars.v @@ -1,3 +1,4 @@ +From Coq Require Import Prelude. From elpi Require Import elpi. (** Closing a term with holes with binders *) diff --git a/examples/example_curry_howard_tactics.v b/examples/example_curry_howard_tactics.v index 7e984143b..793261251 100644 --- a/examples/example_curry_howard_tactics.v +++ b/examples/example_curry_howard_tactics.v @@ -1,3 +1,4 @@ +From Coq Require Import Prelude. From elpi Require Import elpi. (* Tactics diff --git a/examples/example_fuzzer.v b/examples/example_fuzzer.v index 0c4b010e4..2593ef012 100644 --- a/examples/example_fuzzer.v +++ b/examples/example_fuzzer.v @@ -1,3 +1,4 @@ +From Coq Require Import Prelude. From elpi Require Import elpi. (** Intrinsically typed data type and semantics, from software foundations. @@ -96,4 +97,4 @@ Elpi Typecheck. Elpi fuzz eval eval1. (* let's print our new, broken, semantics ;-) *) -Print eval1. \ No newline at end of file +Print eval1. diff --git a/examples/example_generalize.v b/examples/example_generalize.v index 158f9baa5..ae1348ce5 100644 --- a/examples/example_generalize.v +++ b/examples/example_generalize.v @@ -1,3 +1,4 @@ +From Coq Require Import Prelude. From elpi Require Import elpi. (** Abstract a term over something, like the generalize tactic *) diff --git a/examples/example_import_projections.v b/examples/example_import_projections.v index 5f44e339f..d5d10bfb3 100644 --- a/examples/example_import_projections.v +++ b/examples/example_import_projections.v @@ -1,3 +1,4 @@ +From Coq Require Import Prelude. From elpi Require Import elpi. (* "import" a record instance by naming it's applied projections *) diff --git a/examples/example_record_expansion.v b/examples/example_record_expansion.v index 64e192b3b..a17dcc7ce 100644 --- a/examples/example_record_expansion.v +++ b/examples/example_record_expansion.v @@ -1,3 +1,4 @@ +From Coq Require Import Datatypes Logic. From elpi Require Import elpi. (** diff --git a/examples/example_record_to_sigma.v b/examples/example_record_to_sigma.v index ac968ea9e..435683192 100644 --- a/examples/example_record_to_sigma.v +++ b/examples/example_record_to_sigma.v @@ -1,3 +1,4 @@ +From Coq Require Import Datatypes Logic Specif. From elpi Require Import elpi. (* Define a command to turn records into nested sigma types, suggested diff --git a/examples/example_reduction_surgery.v b/examples/example_reduction_surgery.v index 94ac3b0b6..15b810dad 100644 --- a/examples/example_reduction_surgery.v +++ b/examples/example_reduction_surgery.v @@ -3,6 +3,7 @@ from a given module. *) +From Coq Require Import Prelude. From elpi Require Import elpi. Elpi Tactic reduce. diff --git a/examples/example_reflexive_tactic.v b/examples/example_reflexive_tactic.v index b2ca18694..9051e893e 100644 --- a/examples/example_reflexive_tactic.v +++ b/examples/example_reflexive_tactic.v @@ -9,6 +9,7 @@ *) +From Coq Require Import Prelude. From elpi Require elpi. Require Arith ZArith Psatz List ssreflect. diff --git a/examples/tutorial_coq_elpi_HOAS.v b/examples/tutorial_coq_elpi_HOAS.v index 8ce682784..3d64427b1 100644 --- a/examples/tutorial_coq_elpi_HOAS.v +++ b/examples/tutorial_coq_elpi_HOAS.v @@ -45,6 +45,7 @@ HOAS for Gallina |*) +From Coq Require Import Prelude. (* .none *) From elpi Require Import elpi. (* .none *) Elpi Command tutorial_HOAS. (* .none *) diff --git a/examples/tutorial_coq_elpi_command.v b/examples/tutorial_coq_elpi_command.v index 98ab50093..f6a89b49c 100644 --- a/examples/tutorial_coq_elpi_command.v +++ b/examples/tutorial_coq_elpi_command.v @@ -44,6 +44,7 @@ Let's create a simple command, called "hello", which prints :e:`"Hello"` followed by the arguments we pass to it: |*) +From Coq Require Import Prelude. From elpi Require Import elpi. Elpi Command hello. diff --git a/examples/tutorial_coq_elpi_tactic.v b/examples/tutorial_coq_elpi_tactic.v index 57f057ed1..5d54c9ef4 100644 --- a/examples/tutorial_coq_elpi_tactic.v +++ b/examples/tutorial_coq_elpi_tactic.v @@ -55,6 +55,7 @@ Let's define a simple tactic that prints the current goal. |*) +From Coq Require Import Prelude. From elpi Require Import elpi. Elpi Tactic show. From 6932ab65e43513bdab79091c24ed7cd772035f6b Mon Sep 17 00:00:00 2001 From: Patrick Nicodemus Date: Wed, 21 Aug 2024 18:35:48 -0400 Subject: [PATCH 3/3] Removed stdlib dependency in a few more pieces --- elpi/coq-elaborator.elpi | 6 +++--- theories/dune | 4 +++- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/elpi/coq-elaborator.elpi b/elpi/coq-elaborator.elpi index 5f2dea227..fc2f97b1a 100644 --- a/elpi/coq-elaborator.elpi +++ b/elpi/coq-elaborator.elpi @@ -37,13 +37,13 @@ pred propagate-Prop-constraint-inward i:term. propagate-Prop-constraint-inward {{ forall x : lp:Ty, lp:(F x) }} :- !, @pi-decl `x` Ty x\ propagate-Prop-constraint-inward (F x). -propagate-Prop-constraint-inward {{ lp:A /\ lp:B }} :- !, +propagate-Prop-constraint-inward {{ Logic.and lp:A lp:B }} :- !, propagate-Prop-constraint-inward A, propagate-Prop-constraint-inward B. -propagate-Prop-constraint-inward {{ lp:A \/ lp:B }} :- !, +propagate-Prop-constraint-inward {{ Logic.or lp:A lp:B }} :- !, propagate-Prop-constraint-inward A, propagate-Prop-constraint-inward B. -propagate-Prop-constraint-inward {{ ~ lp:A }} :- !, +propagate-Prop-constraint-inward {{ Logic.not lp:A }} :- !, propagate-Prop-constraint-inward A. propagate-Prop-constraint-inward (uvar as X) :- !, coq.typecheck X {{ Prop }} ok. diff --git a/theories/dune b/theories/dune index 4f3a60a6e..d2afd6012 100644 --- a/theories/dune +++ b/theories/dune @@ -2,7 +2,9 @@ (name elpi) (package coq-elpi) (plugins coq-elpi.elpi) - (theories elpi_elpi)) + (theories elpi_elpi Coq) + (stdlib no) + ) (rule (target elpi.v)