Store the closedness of a term on its leave in unification matchrec. #14253
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
Bench https://gitlab.com/coq/coq/-/jobs/1237769695 |
|
Funny experiment but not really conclusive. Some single lines show important differences but it doesn't stand out it the whole bench, and they are rather small in absolute values. |
ppedrot
force-pushed
the
cache-constr-annotation-unfication-matchrec
branch
from
90c2774
to
830a5c7
Compare
|
Reopening because it actually fixes a reported bug. |
ppedrot
force-pushed
the
cache-constr-annotation-unfication-matchrec
branch
from
830a5c7
to
ec55829
Compare
|
Hey, I have detected that there were CI failures at commit ec55829 without any failure in the test-suite. |
2 similar comments
|
Hey, I have detected that there were CI failures at commit ec55829 without any failure in the test-suite. |
|
Hey, I have detected that there were CI failures at commit ec55829 without any failure in the test-suite. |
|
@coqbot ci minimize |
|
I have initiated minimization at commit ec55829 for the suggested target ci-fiat_parsers as requested. |
|
Hey, I have detected that there were CI failures at commit ec55829 without any failure in the test-suite. |
|
Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/fiat_parsers/src/Parsers/Refinement/PossibleTerminalsSets.v (from ci-fiat_parsers) (interrupted by timeout) (full log on GitHub Actions) Minimized Coq File (truncated to 32KiB; full 60KiB file on GitHub Actions Artifacts under
|
|
@JasonGross minimization is incomplete, is there an easy way to relaunch it? |
|
Not yet. I'm hopeful @Zimmi48 will manage to implement the coqbot side of relaunching as per coq/bot#143 (comment) within the next couple of days, and then minimization will automatically be relaunched when interrupted by timeout. @Zimmi48, if you don't have time, I can try to implement it. Alternatively, @ppedrot , if you want to do it manually, there's a printout of a curl request in the log that contains the relevant information for making a new branch on the minimizer as per the instructions at coq/bot#143 (comment), and if you're really in a hurry you could create that branch manually. Otherwise I'd suggest just waiting a couple of days until we have the coqbot side implemented and then we can relaunch minimization here. |
|
@JasonGross Unfortunately, I've underestimated the time that some other tasks would take and now I need to delay work on the bot to after the Coq workshop 😖 So if you do have time to implement this feature in the next couple of days, feel free to go ahead. |
|
Resumption should now work, I'm testing it at #14328 (comment) |
|
Now that resumption works and I've adjusted fiat to be a bit more minimizable and with some help from manual minimization to work around #14529, minimization has finished! I'll post the full bug file in the next comment. Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/fiat_parsers/src/Parsers/Refinement/PossibleTerminalsSets.v (from ci-fiat_parsers) (full log on GitHub Actions) Minimized Coq File (truncated to 32KiB; full 45KiB file on GitHub Actions Artifacts under
|
Minimized Coq File(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-deprecated-native-compiler-option" "-w" "-deprecated-appcontext -notation-overridden" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_parsers/src" "Fiat" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_parsers/Bedrock" "Bedrock" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_parsers/src/Common/Tactics" "-top" "bug_01" "-native-compiler" "no" "-require-import" "Coq.Compat.AdmitAxiom" "-native-compiler" "no") -*- *)
(* File reduced by coq-bug-finder from original input, then from 916 lines to 386 lines, then from 507 lines to 948 lines, then from 951 lines to 417 lines, then from 538 lines to 916 lines, then from 919 lines to 447 lines, then from 567 lines to 917 lines, then from 921 lines to 475 lines, then from 595 lines to 831 lines, then from 834 lines to 516 lines, then from 634 lines to 1027 lines, then from 1031 lines to 795 lines, then from 910 lines to 2027 lines, then from 2031 lines to 1799 lines, then from 1801 lines to 806 lines, then from 918 lines to 1029 lines, then from 1033 lines to 887 lines, then from 999 lines to 1506 lines, then from 1510 lines to 1022 lines, then from 1110 lines to 1322 lines, then from 1325 lines to 1054 lines, then from 1142 lines to 1195 lines, then from 1199 lines to 1173 lines, then from 1176 lines to 1076 lines, then from 1161 lines to 1456 lines, then from 1459 lines to 1237 lines, then from 1310 lines to 1462 lines, then from 1466 lines to 1257 lines, then from 1325 lines to 1458 lines, then from 1462 lines to 1287 lines, then from 1353 lines to 1483 lines, then from 1487 lines to 1294 lines, then from 1360 lines to 1530 lines, then from 1534 lines to 1530 lines, then from 1530 lines to 1370 lines, then from 1435 lines to 1479 lines, then from 1483 lines to 1382 lines, then from 1447 lines to 1598 lines, then from 1602 lines to 1400 lines, then from 1461 lines to 2272 lines, then from 2275 lines to 1688 lines, then from 1691 lines to 1498 lines, then from 1556 lines to 1843 lines, then from 1847 lines to 1527 lines, then from 1585 lines to 1869 lines, then from 1873 lines to 1659 lines, then from 1712 lines to 1965 lines, then from 1969 lines to 1785 lines, then from 1807 lines to 1755 lines, then from 1808 lines to 2104 lines, then from 2108 lines to 1790 lines, then from 1841 lines to 2002 lines, then from 2006 lines to 1809 lines, then from 1859 lines to 2559 lines, then from 2563 lines to 2189 lines, then from 2192 lines to 1844 lines, then from 1892 lines to 1929 lines, then from 1932 lines to 1845 lines, then from 1892 lines to 1916 lines, then from 1920 lines to 1845 lines, then from 1892 lines to 1949 lines, then from 1953 lines to 1861 lines, then from 1908 lines to 1950 lines, then from 1954 lines to 1942 lines, then from 1944 lines to 1860 lines, then from 1908 lines to 1945 lines, then from 1948 lines to 1861 lines, then from 1908 lines to 1932 lines, then from 1936 lines to 1861 lines, then from 1908 lines to 1965 lines, then from 1969 lines to 1861 lines, then from 1908 lines to 1950 lines, then from 1954 lines to 1877 lines, then from 1924 lines to 1861 lines, then from 1908 lines to 1945 lines, then from 1948 lines to 1861 lines, then from 1908 lines to 1932 lines, then from 1936 lines to 1861 lines, then from 1908 lines to 1965 lines, then from 1969 lines to 1861 lines, then from 1908 lines to 1950 lines, then from 1954 lines to 1878 lines, then from 1925 lines to 1860 lines, then from 1908 lines to 1945 lines, then from 1948 lines to 1861 lines, then from 1908 lines to 1932 lines, then from 1936 lines to 1861 lines, then from 1908 lines to 1965 lines, then from 1969 lines to 1861 lines, then from 1908 lines to 1950 lines, then from 1954 lines to 1942 lines, then from 1944 lines to 1860 lines, then from 1908 lines to 1945 lines, then from 1948 lines to 1861 lines, then from 1908 lines to 1932 lines, then from 1936 lines to 1861 lines, then from 1908 lines to 1965 lines, then from 1969 lines to 1861 lines, then from 1908 lines to 1950 lines, then from 1954 lines to 1879 lines, then from 1925 lines to 1860 lines, then from 1864 lines to 1860 lines, then from 1840 lines to 1179 lines, then from 2974 lines to 1443 lines, then from 1438 lines to 1065 lines, then from 1090 lines to 1150 lines, then from 1154 lines to 1077 lines, then from 1081 lines to 1077 lines *)
(* coqc version 8.15+alpha compiled with OCaml 4.05.0
coqtop version 8.15+alpha *)
Require Coq.MSets.MSetPositive.
Require Coq.Sets.Ensembles.
Module Export Fiat_DOT_Common_DOT_Coq__8_4__8_5__Compat.
Module Export Fiat.
Module Export Common.
Module Export Coq__8_4__8_5__Compat.
Global Set Instance Generalized Output.
End Coq__8_4__8_5__Compat.
End Common.
End Fiat.
End Fiat_DOT_Common_DOT_Coq__8_4__8_5__Compat.
Module Export Fiat_DOT_Common.
Module Export Fiat.
Module Common.
Global Set Implicit Arguments.
Global Generalizable All Variables.
Global Coercion is_true : bool >-> Sortclass.
End Common.
End Fiat.
End Fiat_DOT_Common.
Module Export Fiat_DOT_Common_DOT_Equality.
Module Export Fiat.
Module Export Common.
Module Export Equality.
Import Coq.Lists.List.
Import Coq.Strings.String.
Scheme Equality for string.
Section In.
Section list_bin.
Context {A} (eq_A : A -> A -> bool) (a : A).
Fixpoint list_bin (ls : list A) : bool
:= match ls with
| nil => false
| x::xs => orb (list_bin xs) (eq_A x a)
end.
End list_bin.
End In.
End Equality.
End Common.
End Fiat.
End Fiat_DOT_Common_DOT_Equality.
Module Export Fiat_DOT_Common_DOT_Instances.
Module Export Fiat.
Module Export Common.
Module Export Instances.
Import Coq.Classes.Morphisms.
Global Instance drop_0_Proper {A B RA RB} {f : B}
{H : Proper RB f}
: Proper (RA ==> RB) (fun _ : A => f).
admit.
Defined.
End Instances.
End Common.
End Fiat.
End Fiat_DOT_Common_DOT_Instances.
Module Export Fiat_DOT_Common_DOT_List_DOT_Operations.
Module Export Fiat.
Module Export Common.
Module Export List.
Module Export Operations.
Import Coq.Lists.List.
Module Export List.
Definition uniquize {A} (beq : A -> A -> bool) (ls : list A) : list A
:= fold_right
(fun x xs => if list_bin beq x xs then xs else x::xs)
nil
ls.
Fixpoint up_to (n : nat) : list nat :=
match n with
| 0 => nil
| S n' => n'::up_to n'
end.
End List.
End Operations.
End List.
End Common.
End Fiat.
End Fiat_DOT_Common_DOT_List_DOT_Operations.
Module Export Fiat_DOT_Common_DOT_MSetExtensions.
Module Export Fiat.
Module Export Common.
Module Export MSetExtensions.
Export Coq.MSets.MSetInterface.
End MSetExtensions.
End Common.
End Fiat.
End Fiat_DOT_Common_DOT_MSetExtensions.
Module Export Fiat_DOT_Common_DOT_Notations.
Module Export Fiat.
Module Export Common.
Module Export Notations.
Reserved Infix "⊔" (at level 80).
End Notations.
End Common.
End Fiat.
End Fiat_DOT_Common_DOT_Notations.
Module Export Fiat_DOT_Parsers_DOT_StringLike_DOT_Core.
Module Export Fiat.
Module Export Parsers.
Module Export StringLike.
Module Export Core.
Local Coercion is_true : bool >-> Sortclass.
Module Export StringLike.
Class StringLikeMin {Char : Type} :=
{
String :> Type;
char_at_matches : nat -> String -> (Char -> bool) -> bool;
unsafe_get : nat -> String -> Char;
length : String -> nat
}.
Class StringLike {Char : Type} {HSLM : @StringLikeMin Char} :=
{
is_char : String -> Char -> bool;
take : nat -> String -> String;
drop : nat -> String -> String;
get : nat -> String -> option Char;
bool_eq : String -> String -> bool;
beq : relation String := fun x y => bool_eq x y
}.
Arguments StringLikeMin : clear implicits.
Arguments StringLike Char {HSLM}.
Delimit Scope string_like_scope with string_like.
Infix "=s" := (@beq _ _ _) (at level 70, no associativity) : type_scope.
Notation "s ~= [ ch ]" := (is_char s ch) (at level 70, no associativity) : string_like_scope.
Local Open Scope string_like_scope.
Class StringLikeProperties (Char : Type) `{StringLike Char} :=
{
singleton_unique : forall s ch ch', s ~= [ ch ] -> s ~= [ ch' ] -> ch = ch';
singleton_exists : forall s, length s = 1 -> exists ch, s ~= [ ch ];
char_at_matches_correct : forall s n P ch, get n s = Some ch -> (char_at_matches n s P = P ch);
get_0 : forall s ch, take 1 s ~= [ ch ] <-> get 0 s = Some ch;
get_S : forall n s, get (S n) s = get n (drop 1 s);
unsafe_get_correct : forall n s ch, get n s = Some ch -> unsafe_get n s = ch;
length_singleton : forall s ch, s ~= [ ch ] -> length s = 1;
bool_eq_char : forall s s' ch, s ~= [ ch ] -> s' ~= [ ch ] -> s =s s';
is_char_Proper :> Proper (beq ==> eq ==> eq) is_char;
length_Proper :> Proper (beq ==> eq) length;
take_Proper :> Proper (eq ==> beq ==> beq) take;
drop_Proper :> Proper (eq ==> beq ==> beq) drop;
bool_eq_Equivalence :> Equivalence beq;
bool_eq_empty : forall str str', length str = 0 -> length str' = 0 -> str =s str';
take_short_length : forall str n, n <= length str -> length (take n str) = n;
take_long : forall str n, length str <= n -> take n str =s str;
take_take : forall str n m, take n (take m str) =s take (min n m) str;
drop_length : forall str n, length (drop n str) = length str - n;
drop_0 : forall str, drop 0 str =s str;
drop_drop : forall str n m, drop n (drop m str) =s drop (n + m) str;
drop_take : forall str n m, drop n (take m str) =s take (m - n) (drop n str);
take_drop : forall str n m, take n (drop m str) =s drop m (take (n + m) str);
bool_eq_from_get : forall str str', (forall n, get n str = get n str') -> str =s str';
strings_nontrivial : forall n, exists str, length str = n
}.
Arguments StringLikeProperties Char {_ _}.
End StringLike.
End Core.
End StringLike.
End Parsers.
End Fiat.
End Fiat_DOT_Parsers_DOT_StringLike_DOT_Core.
Module Export Fiat.
Module Export Parsers.
Module Export ContextFreeGrammar.
Module Export Core.
Export Fiat.Parsers.StringLike.Core.
End Core.
Section syntax.
Context {Char : Type}.
Inductive RCharExpr :=
| rbeq (ch : Char)
| ror (_ _ : RCharExpr)
| rand (_ _ : RCharExpr)
| rneg (_ : RCharExpr)
| rcode_le_than (code : BinNums.N)
| rcode_ge_than (code : BinNums.N).
Inductive ritem :=
| RTerminal (_ : RCharExpr)
| RNonTerminal (_ : String.string).
Definition rproduction := list ritem.
Definition rproductions := list rproduction.
End syntax.
Global Arguments rproductions : clear implicits.
Section semantics.
Context {Char : Type}.
Class interp_RCharExpr_data :=
{ irbeq : Char -> Char -> bool;
irN_of : Char -> BinNums.N }.
End semantics.
Global Arguments interp_RCharExpr_data : clear implicits.
Import Coq.Strings.String.
Class NoDupR {T} beq (ls : list T) := nodupr : uniquize beq ls = ls.
Record pregrammar Char :=
{
pregrammar_rproductions : list (string * rproductions Char);
pregrammar_idata : interp_RCharExpr_data Char;
pregrammar_rnonterminals : list string
:= map fst pregrammar_rproductions;
rnonterminals_unique
: NoDupR string_beq pregrammar_rnonterminals;
RLookup_idx : nat -> rproductions Char
:= fun n => nth n (map snd pregrammar_rproductions) nil
}.
Module Export Definitions.
Local Coercion is_true : bool >-> Sortclass.
Delimit Scope grammar_fixedpoint_scope with fixedpoint.
Local Open Scope grammar_fixedpoint_scope.
Inductive lattice_for T := top | constant (_ : T) | bottom.
Scheme Equality for lattice_for.
Arguments bottom {_}.
Arguments top {_}.
Notation "'⊥'" := bottom : grammar_fixedpoint_scope.
Notation "'⊤'" := top : grammar_fixedpoint_scope.
Global Instance lattice_for_Equivalence {T} {beq : T -> T -> bool}
{H : Equivalence beq}
: Equivalence (lattice_for_beq beq).
admit.
Defined.
Definition lattice_for_lt {T} (lt : T -> T -> bool) (x y : lattice_for T)
:= match x, y with
| ⊤, ⊤ => false
| constant x', constant y' => lt x' y'
| ⊥, ⊥ => false
| _, ⊤ => true
| ⊤, _ => false
| _, constant _ => true
| constant _, _ => false
end.
Global Instance lattice_for_lt_Proper {T} {beq lt : T -> T -> bool}
{H : Proper (beq ==> beq ==> eq) lt}
: Proper (lattice_for_beq beq ==> lattice_for_beq beq ==> eq) (lattice_for_lt lt).
admit.
Defined.
Definition lattice_for_lub {T} (lub : T -> T -> lattice_for T) (x y : lattice_for T)
:= match x, y with
| ⊤, ⊤ => ⊤
| constant x', constant y' => lub x' y'
| ⊥, ⊥ => ⊥
| ⊤, _
| _, ⊤
=> ⊤
| ⊥, v
| v, ⊥
=> v
end.
Section lub_correct.
Context {T} (beq : T -> T -> bool) (lt : T -> T -> bool) (lub : T -> T -> lattice_for T).
Local Notation "x <= y" := (orb (lattice_for_beq beq x y) (lattice_for_lt lt x y)).
Context (lub_correct_l : forall x y, constant x <= lub x y)
(lub_correct_r : forall x y, constant y <= lub x y)
(beq_Reflexive : Reflexive beq).
Lemma lattice_for_lub_correct_l x y
: x <= lattice_for_lub lub x y.
Proof using beq_Reflexive lub_correct_l.
admit.
Qed.
Lemma lattice_for_lub_correct_r x y
: y <= lattice_for_lub lub x y.
Proof using beq_Reflexive lub_correct_r.
admit.
Qed.
Global Instance lattice_for_lub_Proper
{lub_Proper : Proper (beq ==> beq ==> lattice_for_beq beq) lub}
: Proper (lattice_for_beq beq ==> lattice_for_beq beq ==> lattice_for_beq beq) (lattice_for_lub lub).
admit.
Defined.
End lub_correct.
Definition lattice_for_gt_well_founded {T} {lt : T -> T -> bool}
(gt_wf : well_founded (Basics.flip lt))
: well_founded (Basics.flip (lattice_for_lt lt)).
admit.
Defined.
Global Instance lattice_for_lt_Transitive {T} {lt : T -> T -> bool} {_ : Transitive lt}
: Transitive (lattice_for_lt lt).
admit.
Defined.
Class grammar_fixedpoint_lattice_data prestate :=
{ state :> _ := lattice_for prestate;
prestate_lt : prestate -> prestate -> bool;
state_lt : state -> state -> bool
:= lattice_for_lt prestate_lt;
prestate_beq : prestate -> prestate -> bool;
state_beq : state -> state -> bool
:= lattice_for_beq prestate_beq;
prestate_le s1 s2 := (prestate_beq s1 s2 || prestate_lt s1 s2)%bool;
state_le s1 s2 := (state_beq s1 s2 || state_lt s1 s2)%bool;
prestate_beq_Equivalence : Equivalence prestate_beq;
state_beq_Equivalence : Equivalence state_beq
:= lattice_for_Equivalence;
preleast_upper_bound : prestate -> prestate -> state;
least_upper_bound : state -> state -> state
:= lattice_for_lub preleast_upper_bound;
preleast_upper_bound_correct_l
: forall a b, state_le (constant a) (preleast_upper_bound a b);
preleast_upper_bound_correct_r
: forall a b, state_le (constant b) (preleast_upper_bound a b);
least_upper_bound_correct_l
: forall a b, state_le a (least_upper_bound a b)
:= lattice_for_lub_correct_l prestate_beq prestate_lt preleast_upper_bound preleast_upper_bound_correct_l _;
least_upper_bound_correct_r
: forall a b, state_le b (least_upper_bound a b)
:= lattice_for_lub_correct_r prestate_beq prestate_lt preleast_upper_bound preleast_upper_bound_correct_r _;
prestate_gt_wf : well_founded (Basics.flip prestate_lt);
state_gt_wf : well_founded (Basics.flip state_lt)
:= lattice_for_gt_well_founded prestate_gt_wf;
preleast_upper_bound_Proper : Proper (prestate_beq ==> prestate_beq ==> state_beq) preleast_upper_bound;
least_upper_bound_Proper : Proper (state_beq ==> state_beq ==> state_beq) least_upper_bound
:= @lattice_for_lub_Proper _ _ _ _;
prestate_lt_Proper : Proper (prestate_beq ==> prestate_beq ==> eq) prestate_lt;
state_lt_Proper : Proper (state_beq ==> state_beq ==> eq) state_lt
:= lattice_for_lt_Proper;
prestate_lt_Transitive : Transitive prestate_lt;
state_lt_Transitive : Transitive state_lt
:= lattice_for_lt_Transitive }.
Infix "<=" := (@state_le _ _) : grammar_fixedpoint_scope.
Infix "⊔" := (@least_upper_bound _ _) : grammar_fixedpoint_scope.
Global Instance lattice_for_rect_Proper_85 {A}
: Proper (eq ==> forall_relation (fun _ => eq) ==> eq ==> eq ==> Basics.flip Basics.impl)
(@lattice_for_rect A (fun _ => Prop)) | 3.
admit.
Defined.
Lemma lattice_for_rect_pull {A B C} f t c b v
: f (@lattice_for_rect A (fun _ => B) t c b v)
= @lattice_for_rect A (fun _ => C) (f t) (fun x => f (c x)) (f b) v.
admit.
Defined.
End Definitions.
Module Export AsciiLattice.
Import Coq.Strings.Ascii.
Import Coq.MSets.MSetPositive.
Section gen.
Global Instance positive_set_fpdata
: grammar_fixedpoint_lattice_data PositiveSet.t.
admit.
Defined.
End gen.
Definition max_ascii := Eval compute in BinPos.Pos.of_nat (S (nat_of_ascii (Ascii true true true true true true true true))).
End AsciiLattice.
Module Export FromAbstractInterpretationDefinitions.
Import Coq.Sets.Ensembles.
Import Fiat.Parsers.ContextFreeGrammar.Core.
Local Coercion is_true : bool >-> Sortclass.
Local Open Scope grammar_fixedpoint_scope.
Section general_fold.
Context {Char : Type}
{T : Type}.
Definition lattice_for_combine_production combine_production
: lattice_for T -> lattice_for T -> lattice_for T
:= fun x y => match x, y with
| ⊥, _
| _, ⊥
=> ⊥
| ⊤, _
| _, ⊤
=> ⊤
| constant x', constant y'
=> combine_production x' y'
end.
Global Instance lattice_for_combine_production_Proper
{prestate_beq : T -> T -> bool}
{precombine_production}
{H : Proper (prestate_beq ==> prestate_beq ==> lattice_for_beq prestate_beq) precombine_production}
: Proper (lattice_for_beq prestate_beq ==> lattice_for_beq prestate_beq ==> lattice_for_beq prestate_beq) (lattice_for_combine_production precombine_production).
admit.
Defined.
Context {fpdata : @grammar_fixedpoint_lattice_data T}.
Class AbstractInterpretation :=
{ on_terminal : (Char -> bool) -> lattice_for T;
on_nil_production : lattice_for T;
precombine_production : T -> T -> lattice_for T;
combine_production : lattice_for T -> lattice_for T -> lattice_for T
:= lattice_for_combine_production precombine_production;
precombine_production_Proper : Proper (prestate_beq ==> prestate_beq ==> state_beq) precombine_production;
combine_production_Proper : Proper (state_beq ==> state_beq ==> state_beq) combine_production
:= lattice_for_combine_production_Proper }.
Global Existing Instance precombine_production_Proper.
End general_fold.
Section on_ensembles.
Context {Char : Type} {HSLM : StringLikeMin Char} {HSL : StringLike Char}.
Definition ensemble_on_terminal (P : Char -> bool) : Ensemble String
:= (fun str => exists ch, is_true (P ch) /\ str ~= [ ch ])%string_like.
Definition ensemble_on_nil_production : Ensemble String
:= (fun str => length str = 0).
Definition ensemble_combine_production : Ensemble String -> Ensemble String -> Ensemble String
:= fun P1 P2 => fun str => exists n, P1 (take n str) /\ P2 (drop n str).
Definition ensemble_least_upper_bound : Ensemble String -> Ensemble String -> Ensemble String
:= fun P1 P2 => fun str => P1 str \/ P2 str.
End on_ensembles.
Section fold_correctness.
Context {Char : Type} {HSLM : StringLikeMin Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char}.
Context {T : Type}.
Context {fpdata : @grammar_fixedpoint_lattice_data T}
{aidata : @AbstractInterpretation Char T fpdata}.
Context (G : pregrammar Char)
(prerelated : Ensemble String -> T -> Prop).
Definition lattice_for_related (P : Ensemble String) (st : lattice_for T) : Prop
:= match st with
| ⊤ => True
| ⊥ => forall str, ~P str
| constant n => prerelated P n
end.
Section related.
Global Instance lattice_for_related_ext {_ : Proper ((beq ==> iff) ==> prestate_beq ==> iff) prerelated}
: Proper ((beq ==> iff) ==> state_beq ==> iff) related | 2.
Proof using HSLP.
admit.
Qed.
Global Instance lattice_for_combine_production_Proper_le
{precombine_production'}
{H : Proper (prestate_le ==> prestate_le ==> state_le) precombine_production'}
: Proper (state_le ==> state_le ==> state_le) (lattice_for_combine_production precombine_production').
admit.
Defined.
End related.
Class AbstractInterpretationCorrectness :=
{ prerelated_ext : Proper ((beq ==> iff) ==> prestate_beq ==> iff) prerelated;
related : Ensemble String -> state -> Prop
:= lattice_for_related;
related_ext : Proper ((beq ==> iff) ==> state_beq ==> iff) related
:= lattice_for_related_ext;
related_monotonic : forall s0 s1, s0 <= s1 -> (forall v, related v s0 -> related v s1);
lub_correct
: forall P1 st1,
related P1 st1
-> forall P2 st2,
related P2 st2
-> related (ensemble_least_upper_bound P1 P2) (least_upper_bound st1 st2);
on_terminal_correct
: forall P,
related (ensemble_on_terminal P) (on_terminal P);
on_nil_production_correct
: related ensemble_on_nil_production on_nil_production;
precombine_production_Proper_le
: Proper (prestate_le ==> prestate_le ==> state_le) precombine_production;
combine_production_Proper_le
: Proper (state_le ==> state_le ==> state_le) combine_production
:= _;
combine_production_correct
: forall P1 st1,
related P1 st1
-> forall P2 st2,
related P2 st2
-> related (ensemble_combine_production P1 P2) (combine_production st1 st2)
}.
End fold_correctness.
End FromAbstractInterpretationDefinitions.
Import Fiat_DOT_Common.Fiat.Common.
Global Instance prod_fixedpoint_lattice {prestate0 prestate1}
{fpldata0 : grammar_fixedpoint_lattice_data prestate0}
{fpldata1 : grammar_fixedpoint_lattice_data prestate1}
: grammar_fixedpoint_lattice_data (@state _ fpldata0 * @state _ fpldata1).
admit.
Defined.
Global Instance prod_fixedpoint_lattice' {prestate0 prestate1}
{fpldata0 : grammar_fixedpoint_lattice_data prestate0}
{fpldata1 : grammar_fixedpoint_lattice_data prestate1}
: grammar_fixedpoint_lattice_data (lattice_for prestate0 * lattice_for prestate1)
:= prod_fixedpoint_lattice.
Import Fiat.Parsers.StringLike.Core.
Module Export ProdAbstractInterpretationDefinitions.
Import Coq.Sets.Ensembles.
Section aidata.
Context {Char : Type} {T T0 T1}
{fpldata : grammar_fixedpoint_lattice_data T}
{fpldata0 : grammar_fixedpoint_lattice_data T0}
{fpldata1 : grammar_fixedpoint_lattice_data T1}.
Definition prod_on_terminal
(on_terminal0 : (Char -> bool) -> lattice_for T0)
(on_terminal1 : (Char -> bool) -> lattice_for T1)
: (Char -> bool) -> lattice_for (lattice_for T0 * lattice_for T1)
:= fun P => constant (on_terminal0 P, on_terminal1 P).
Definition prod_on_nil_production
(on_nil_production0 : lattice_for T0)
(on_nil_production1 : lattice_for T1)
: lattice_for (lattice_for T0 * lattice_for T1)
:= constant (on_nil_production0, on_nil_production1).
Definition prod_precombine_production_dep
(precombine_production0 : T0 -> T0 -> lattice_for T0)
(precombine_production1 : lattice_for T0 -> lattice_for T0 -> T1 -> T1 -> lattice_for T1)
: (lattice_for T0 * lattice_for T1) -> (lattice_for T0 * lattice_for T1) -> lattice_for (lattice_for T0 * lattice_for T1)
:= fun x y => constant (lattice_for_combine_production precombine_production0 (fst x) (fst y),
lattice_for_combine_production (precombine_production1 (fst x) (fst y)) (snd x) (snd y)).
Definition prod_precombine_production_nondep
(precombine_production0 : T0 -> T0 -> lattice_for T0)
(precombine_production1 : T1 -> T1 -> lattice_for T1)
: (lattice_for T0 * lattice_for T1) -> (lattice_for T0 * lattice_for T1) -> lattice_for (lattice_for T0 * lattice_for T1)
:= fun x y => constant (lattice_for_combine_production precombine_production0 (fst x) (fst y),
lattice_for_combine_production precombine_production1 (snd x) (snd y)).
Global Instance prod_precombine_production_dep_Proper
{precombine_production0 : T0 -> T0 -> lattice_for T0}
{precombine_production1 : lattice_for T0 -> lattice_for T0 -> T1 -> T1 -> lattice_for T1}
{HP0 : Proper (prestate_beq ==> prestate_beq ==> state_beq) precombine_production0}
{HP1 : Proper (state_beq ==> state_beq ==> prestate_beq ==> prestate_beq ==> state_beq) precombine_production1}
: Proper (prestate_beq ==> prestate_beq ==> state_beq) (prod_precombine_production_dep precombine_production0 precombine_production1).
admit.
Defined.
Definition prod_aidata_dep
(on_terminal0 : (Char -> bool) -> lattice_for T0)
(on_nil_production0 : lattice_for T0)
(precombine_production0 : T0 -> T0 -> lattice_for T0)
(on_terminal1 : (Char -> bool) -> lattice_for T1)
(on_nil_production1 : lattice_for T1)
(precombine_production1 : lattice_for T0 -> lattice_for T0 -> T1 -> T1 -> lattice_for T1)
(precombine_production0_Proper
: Proper (prestate_beq ==> prestate_beq ==> state_beq) precombine_production0)
(precombine_production1_Proper
: Proper (state_beq ==> state_beq ==> prestate_beq ==> prestate_beq ==> state_beq) precombine_production1)
: @AbstractInterpretation Char (lattice_for T0 * lattice_for T1) prod_fixedpoint_lattice'.
Proof.
refine {| on_terminal := prod_on_terminal on_terminal0 on_terminal1;
on_nil_production := prod_on_nil_production on_nil_production0 on_nil_production1;
precombine_production := prod_precombine_production_dep precombine_production0 precombine_production1 |}.
Defined.
Global Instance prod_precombine_production_dep_Proper_le
{precombine_production0 : T0 -> T0 -> lattice_for T0}
{precombine_production1 : lattice_for T0 -> lattice_for T0 -> T1 -> T1 -> lattice_for T1}
{HP0 : Proper (prestate_le ==> prestate_le ==> state_le) precombine_production0}
{HP1 : Proper (state_le ==> state_le ==> prestate_le ==> prestate_le ==> state_le) precombine_production1}
: Proper (prestate_le ==> prestate_le ==> state_le) (prod_precombine_production_dep precombine_production0 precombine_production1).
admit.
Defined.
Global Instance prod_precombine_production_nondep_dep_Proper_le
{precombine_production0 : lattice_for T -> lattice_for T -> T0 -> T0 -> lattice_for T0}
{precombine_production1 : lattice_for T -> lattice_for T -> T1 -> T1 -> lattice_for T1}
{HP0 : Proper (state_le ==> state_le ==> prestate_le ==> prestate_le ==> state_le) precombine_production0}
{HP1 : Proper (state_le ==> state_le ==> prestate_le ==> prestate_le ==> state_le) precombine_production1}
: Proper (state_le ==> state_le ==> prestate_le ==> prestate_le ==> state_le) (fun x y => prod_precombine_production_nondep (precombine_production0 x y) (precombine_production1 x y)).
admit.
Defined.
End aidata.
Section aicdata.
Context {Char} {HSLM : StringLikeMin Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char}
{T0 T1}
{fpldata0 : grammar_fixedpoint_lattice_data T0}
{fpldata1 : grammar_fixedpoint_lattice_data T1}
(prerelated0 : Ensemble String -> T0 -> Prop)
(prerelated1 : Ensemble String -> T1 -> Prop).
Definition prod_prerelated : Ensemble String -> (lattice_for T0 * lattice_for T1) -> Prop
:= fun P st
=> lattice_for_related prerelated0 P (fst st)
/\ lattice_for_related prerelated1 P (snd st).
Global Instance prod_prerelated_ext
{prerelated0_ext : Proper ((beq ==> iff) ==> prestate_beq ==> iff) prerelated0}
{prerelated1_ext : Proper ((beq ==> iff) ==> prestate_beq ==> iff) prerelated1}
: Proper ((beq ==> iff) ==> prestate_beq ==> iff) prod_prerelated.
Proof using HSLP.
admit.
Qed.
Lemma prod_related_monotonic
{related0_monotonic : forall s0 s1, (s0 <= s1)%fixedpoint -> forall v, lattice_for_related prerelated0 v s0 -> lattice_for_related prerelated0 v s1}
{related1_monotonic : forall s0 s1, (s0 <= s1)%fixedpoint -> forall v, lattice_for_related prerelated1 v s0 -> lattice_for_related prerelated1 v s1}
: forall s0 s1, (s0 <= s1)%fixedpoint -> forall v, lattice_for_related prod_prerelated v s0 -> lattice_for_related prod_prerelated v s1.
admit.
Defined.
Lemma prod_lub_correct
(lub0_correct : forall P1 st1,
lattice_for_related prerelated0 P1 st1
-> forall P2 st2,
lattice_for_related prerelated0 P2 st2
-> lattice_for_related prerelated0 (ensemble_least_upper_bound P1 P2) (st1 ⊔ st2)%fixedpoint)
(lub1_correct : forall P1 st1,
lattice_for_related prerelated1 P1 st1
-> forall P2 st2,
lattice_for_related prerelated1 P2 st2
-> lattice_for_related prerelated1 (ensemble_least_upper_bound P1 P2) (st1 ⊔ st2)%fixedpoint)
: forall P1 st1,
lattice_for_related prod_prerelated P1 st1
-> forall P2 st2,
lattice_for_related prod_prerelated P2 st2
-> lattice_for_related prod_prerelated (ensemble_least_upper_bound P1 P2) (st1 ⊔ st2)%fixedpoint.
admit.
Defined.
Lemma prod_on_terminal_correct
(on_terminal0 : (Char -> bool) -> lattice_for T0)
(on_terminal1 : (Char -> bool) -> lattice_for T1)
(on_terminal0_correct : forall P, lattice_for_related prerelated0 (ensemble_on_terminal P) (on_terminal0 P))
(on_terminal1_correct : forall P, lattice_for_related prerelated1 (ensemble_on_terminal P) (on_terminal1 P))
: forall P, lattice_for_related prod_prerelated (ensemble_on_terminal P) (prod_on_terminal on_terminal0 on_terminal1 P).
admit.
Defined.
Lemma prod_on_nil_production_correct
(on_nil_production0 : lattice_for T0)
(on_nil_production1 : lattice_for T1)
(on_nil_production0_correct : lattice_for_related prerelated0 ensemble_on_nil_production on_nil_production0)
(on_nil_production1_correct : lattice_for_related prerelated1 ensemble_on_nil_production on_nil_production1)
: lattice_for_related prod_prerelated ensemble_on_nil_production (prod_on_nil_production on_nil_production0 on_nil_production1).
admit.
Defined.
Lemma prod_combine_production_dep_correct
(precombine_production0 : T0 -> T0 -> lattice_for T0)
(precombine_production1 : lattice_for T0 -> lattice_for T0 -> T1 -> T1 -> lattice_for T1)
(combine_production0_correct : forall P1 st1,
lattice_for_related prerelated0 P1 st1
-> forall P2 st2,
lattice_for_related prerelated0 P2 st2
-> lattice_for_related prerelated0 (ensemble_combine_production P1 P2) (lattice_for_combine_production precombine_production0 st1 st2))
(combine_production1_correct : forall P1 st1 st10,
lattice_for_related prerelated0 P1 st10
-> lattice_for_related prerelated1 P1 st1
-> forall P2 st2 st20,
lattice_for_related prerelated0 P2 st20
-> lattice_for_related prerelated1 P2 st2
-> lattice_for_related prerelated1 (ensemble_combine_production P1 P2) (lattice_for_combine_production (precombine_production1 st10 st20) st1 st2))
: forall P1 st1,
lattice_for_related prod_prerelated P1 st1
-> forall P2 st2,
lattice_for_related prod_prerelated P2 st2
-> lattice_for_related prod_prerelated (ensemble_combine_production P1 P2) (lattice_for_combine_production (prod_precombine_production_dep precombine_production0 precombine_production1) st1 st2).
admit.
Defined.
Lemma prod_combine_production_nondep_correct_specific
(precombine_production0 : T0 -> T0 -> lattice_for T0)
(precombine_production1 : T1 -> T1 -> lattice_for T1)
P1 st1
(Hrel1 : lattice_for_related prod_prerelated P1 st1)
P2 st2
(Hrel2 : lattice_for_related prod_prerelated P2 st2)
(combine_production0_correct
: forall st1v,
st1 = constant st1v
-> forall st2v,
st2 = constant st2v
-> lattice_for_related prerelated0 (ensemble_combine_production P1 P2) (lattice_for_combine_production precombine_production0 (fst st1v) (fst st2v)))
(combine_production1_correct
: forall st1v,
st1 = constant st1v
-> forall st2v,
st2 = constant st2v
-> lattice_for_related prerelated1 (ensemble_combine_production P1 P2) (lattice_for_combine_production precombine_production1 (snd st1v) (snd st2v)))
: lattice_for_related prod_prerelated (ensemble_combine_production P1 P2) (lattice_for_combine_production (prod_precombine_production_nondep precombine_production0 precombine_production1) st1 st2).
admit.
Defined.
End aicdata.
Global Arguments prod_prerelated_ext {_ _ _ _ T0 T1 _ _ prerelated0 prerelated1} _ _ _ _ _ _ _ _.
Global Arguments prod_related_monotonic {_ _ T0 T1 _ _ prerelated0 prerelated1} _ _ _ _ _ _ _.
Global Arguments prod_lub_correct {_ _ T0 T1 _ _ prerelated0 prerelated1} _ _ _ _ _ _ _ _.
Global Arguments prod_on_terminal_correct {_ _ _ T0 T1 prerelated0 prerelated1 on_terminal0 on_terminal1} _ _ _.
Global Arguments prod_on_nil_production_correct {_ _ T0 T1 prerelated0 prerelated1 on_nil_production0 on_nil_production1} _ _.
Global Arguments prod_precombine_production_dep_Proper_le {T0 T1 _ _ precombine_production0 precombine_production1} _ _ _ _ _ _ _ _.
Global Arguments prod_combine_production_dep_correct {_ _ _ T0 T1 prerelated0 prerelated1 precombine_production0 precombine_production1} _ _ _ _ _ _ _ _.
Global Arguments prod_precombine_production_nondep_dep_Proper_le {T T0 T1 _ _ _ precombine_production0 precombine_production1} _ _ _ _ _ _ _ _ _ _ _ _ _ _.
End ProdAbstractInterpretationDefinitions.
Local Open Scope grammar_fixedpoint_scope.
Inductive nonemptyT := nonempty | could_be_empty.
Global Instance might_be_empty_lattice : grammar_fixedpoint_lattice_data nonemptyT.
admit.
Defined.
Global Instance might_be_empty_aidata {Char} : @AbstractInterpretation Char nonemptyT _.
admit.
Defined.
Section correctness.
Context {Char} {HSLM : StringLikeMin Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char}.
Definition might_be_empty_accurate
(P : String -> Prop) (nonemptyv : nonemptyT)
: Prop
:= nonemptyv = nonempty -> forall str, P str -> length str <> 0.
Global Instance might_be_empty_aicdata
: AbstractInterpretationCorrectness might_be_empty_accurate.
admit.
Defined.
End correctness.
Definition might_be_emptyT := lattice_for nonemptyT.
Coercion collapse_might_be_empty (x : might_be_emptyT) : bool
:= match x with
| ⊤ => true
| constant could_be_empty => true
| constant nonempty => false
| ⊥ => false
end.
Local Open Scope string_like_scope.
Section forall_chars.
Context {Char} {HSLM : StringLikeMin Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char}.
Definition forall_chars (str : String) (P : Char -> Prop)
:= forall n ch,
take 1 (drop n str) ~= [ ch ]
-> P ch.
End forall_chars.
Section for_first_char.
Context {Char} {HSLM : StringLikeMin Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char}.
Definition for_first_char (str : String) (P : Char -> Prop)
:= forall ch,
take 1 str ~= [ ch ]
-> P ch.
End for_first_char.
Section for_last_char.
Context {Char} {HSLM : StringLikeMin Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char}.
Definition for_last_char (str : String) (P : Char -> Prop)
:= forall ch,
drop (pred (length str)) str ~= [ ch ]
-> P ch.
End for_last_char.
Import Coq.MSets.MSetPositive.
Definition all_possible_ascii' : PositiveSet.t
:= List.fold_right
PositiveSet.add
PositiveSet.empty
(List.map (fun x => BinPos.Pos.of_nat (S x))
(Operations.List.up_to (S (Ascii.nat_of_ascii (Ascii.Ascii true true true true true true true true))))).
Definition all_possible_ascii : PositiveSet.t
:= Eval compute in all_possible_ascii'.
Definition pos_of_ascii (x : Ascii.ascii) : BinNums.positive
:= match Ascii.N_of_ascii x with
| BinNums.N0 => max_ascii
| BinNums.Npos x => x
end.
Definition all_but (P : Ascii.ascii -> bool) : PositiveSet.t
:= PositiveSet.filter (fun n => negb (P (Ascii.ascii_of_pos n))) all_possible_ascii.
Definition possible_terminals_prestate
:= (@state _ might_be_empty_lattice
* lattice_for
(lattice_for
(@state _ positive_set_fpdata
* @state _ positive_set_fpdata )
* @state _ positive_set_fpdata ))%type.
Global Instance possible_terminals_aidata : @AbstractInterpretation Ascii.ascii possible_terminals_prestate _.
Proof.
refine (@prod_aidata_dep
_ _ _ _ _
on_terminal
(@on_nil_production Ascii.ascii _ _ might_be_empty_aidata)
(@precombine_production Ascii.ascii _ _ might_be_empty_aidata)
(prod_on_terminal
(prod_on_terminal
(fun P => constant (all_but P))
(fun P => constant (all_but P)))
(fun P => constant (all_but P)))
(prod_on_nil_production
(prod_on_nil_production
(constant all_possible_ascii)
(constant all_possible_ascii))
(constant all_possible_ascii))
(fun xmbe ymbe
=> prod_precombine_production_nondep
(prod_precombine_production_nondep
(fun x' y'
=> constant (if collapse_might_be_empty xmbe
then PositiveSet.inter x' y'
else x'))
(fun x' y'
=> constant (if collapse_might_be_empty ymbe
then PositiveSet.inter x' y'
else y')))
(fun x' y'
=> constant (PositiveSet.inter x' y')))
_ _).
intros x0 y0 H0 x1 y1 H1 x2 y2 H2 x3 y3 H3.
repeat match goal with
| [ H : is_true (state_beq ?x ?y) |- context[collapse_might_be_empty ?x] ]
=> replace (collapse_might_be_empty x)
with (collapse_might_be_empty y)
by (rewrite H; reflexivity);
clear x H
end.
repeat first [ eapply @prod_precombine_production_nondep_Proper
| eassumption
| match goal with
| [ |- context[collapse_might_be_empty ?v] ]
=> destruct (collapse_might_be_empty v)
end ];
clear; admit.
Defined.
Section correctness.
Context {HSLM : StringLikeMin Ascii.ascii} {HSL : StringLike Ascii.ascii} {HSLP : StringLikeProperties Ascii.ascii}.
Definition possible_accurate
: forall (P : String -> Prop) (st : possible_terminals_prestate), Prop
:= prod_prerelated
might_be_empty_accurate
(prod_prerelated
(prod_prerelated
(fun P st
=> forall str, P str -> for_first_char str (fun ch => ~PositiveSet.In (pos_of_ascii ch) st))
(fun P st
=> forall str, P str -> for_last_char str (fun ch => ~PositiveSet.In (pos_of_ascii ch) st)))
(fun P st
=> forall str, P str -> forall_chars str (fun ch => ~PositiveSet.In (pos_of_ascii ch) st))).
Local Ltac pull_lattice_for_rect :=
repeat lazymatch goal with
| [ |- context G[match ?v with ⊤ => ?T | ⊥ => ?B | constant x => @?C x end] ]
=> let RT := type of T in
let G' := context G[lattice_for_rect (fun _ => RT) T C B v] in
change G'
| [ |- context G[fun k : ?KT => match @?v k with ⊤ => @?T k | ⊥ => @?B k | constant x => @?C k x end] ]
=> let RT := match type of T with forall k, @?RT k => RT end in
let G' := context G[fun k : KT => lattice_for_rect (fun _ => RT k) (T k) (C k) (B k) (v k)] in
change G'; cbv beta
| [ |- context G[fun k : ?KT => ?f match @?v k with ⊤ => @?T k | ⊥ => @?B k | constant x => @?C k x end (@?arg k)] ]
=> let RT := match type of T with forall k, @?RT k => RT end in
let G' := context G[fun k : KT => f (lattice_for_rect (fun _ => RT k) (T k) (C k) (B k) (v k)) (arg k)] in
change G'; cbv beta
| [ |- context G[fun k : ?KT => ?f (@?arg k) match @?v k with ⊤ => @?T k | ⊥ => @?B k | constant x => @?C k x end] ]
=> let RT := match type of T with forall k, @?RT k => RT end in
let G' := context G[fun k : KT => f (arg k) (lattice_for_rect (fun _ => RT k) (T k) (C k) (B k) (v k))] in
change G'; cbv beta
end;
rewrite !(fun A T T' x y z => lattice_for_rect_pull (A := A) (lattice_for_rect (T := T) (fun _ => T') x y z));
setoid_rewrite (fun A T T' x y z => lattice_for_rect_pull (A := A) (lattice_for_rect (T := T) (fun _ => T') x y z)).
Global Instance constant_inter_Proper
: Proper (prestate_le ==> prestate_le ==> state_le) (fun x' y' => constant (PositiveSet.inter x' y')).
admit.
Defined.
Local Ltac t_combine_pre :=
repeat first [ assumption
| progress intros
| progress subst
| progress cbv [prod_prerelated ensemble_combine_production lattice_for_related might_be_empty_accurate lattice_for_combine_production] in *
| progress simpl in *
| match goal with H : and _ _ |- _ => destruct H | H : prod _ _ |- _ => destruct H end ].
Local Ltac t_combine :=
t_combine_pre;
pull_lattice_for_rect.
Local Obligation Tactic := intros.
Global Program Instance possible_aicdata
: AbstractInterpretationCorrectness possible_accurate
:= { prerelated_ext
:= prod_prerelated_ext
(@prerelated_ext Ascii.ascii _ _ _ _ _ _ _ might_be_empty_aicdata)
(prod_prerelated_ext (prod_prerelated_ext _ _) _);
related_monotonic
:= prod_related_monotonic
(@related_monotonic Ascii.ascii _ _ _ _ _ _ _ might_be_empty_aicdata)
(prod_related_monotonic (prod_related_monotonic _ _) _);
lub_correct
:= prod_lub_correct
(@lub_correct Ascii.ascii _ _ _ _ _ _ _ might_be_empty_aicdata)
(prod_lub_correct (prod_lub_correct _ _) _);
on_terminal_correct
:= prod_on_terminal_correct
(@on_terminal_correct Ascii.ascii _ _ _ _ _ _ _ might_be_empty_aicdata)
(prod_on_terminal_correct (prod_on_terminal_correct _ _) _);
on_nil_production_correct
:= prod_on_nil_production_correct
(@on_nil_production_correct Ascii.ascii _ _ _ _ _ _ _ might_be_empty_aicdata)
(prod_on_nil_production_correct (prod_on_nil_production_correct _ _) _);
precombine_production_Proper_le
:= prod_precombine_production_dep_Proper_le
(@precombine_production_Proper_le Ascii.ascii _ _ _ _ _ _ _ might_be_empty_aicdata)
(prod_precombine_production_nondep_dep_Proper_le (prod_precombine_production_nondep_dep_Proper_le _ _) _);
combine_production_correct
:= prod_combine_production_dep_correct
(@combine_production_correct Ascii.ascii _ _ _ _ _ _ _ might_be_empty_aicdata)
(fun P1 st1 st10 R10 R1 P2 st2 st20 R20 R2
=> prod_combine_production_nondep_correct_specific
_ _ _ _ _ _ _ _
(fun st1v Hst1v st2v Hst2v
=> prod_combine_production_nondep_correct_specific
_ _ _ _ _ _ _ _ _ _)
_)
}.
Next Obligation.
admit.
Defined.
Next Obligation.
admit.
Defined.
Next Obligation.
admit.
Defined.
Next Obligation.
admit.
Defined.
Next Obligation.
admit.
Defined.
Next Obligation.
admit.
Defined.
Next Obligation.
admit.
Defined.
Next Obligation.
admit.
Defined.
Next Obligation.
admit.
Defined.
Next Obligation.
admit.
Defined.
Next Obligation.
admit.
Defined.
Next Obligation.
admit.
Defined.
Next Obligation.
admit.
Defined.
Next Obligation.
admit.
Defined.
Next Obligation.
admit.
Defined.
Next Obligation.
admit.
Defined.
Next Obligation.
admit.
Defined.
Next Obligation.
admit.
Defined.
Next Obligation.
admit.
Defined.
Next Obligation.
admit.
Defined.
Next Obligation.
admit.
Defined.
Next Obligation.
admit.
Defined.
Next Obligation.
{
t_combine.
The error message occurs in |
|
@ppedrot, I hope this is helpful! |
|
@JasonGross yes, thanks a lot. I'll try to understand what's going on now. |
|
Here is a much smaller test: From Coq Require Import Setoid Morphisms.
Axiom lattice_for : Type -> Type.
Axiom constant : forall {T : Type}, T -> lattice_for T.
Axiom lattice_for_rect :
forall [T : Type] (P : Type), (forall t : T, P) -> forall l : lattice_for T, P.
#[local]
Declare Instance lattice_for_rect_Proper_85 : forall {A},
Proper (forall_relation (fun _ => eq) ==> eq ==> Basics.flip Basics.impl)
(@lattice_for_rect A Prop) | 3.
Axiom lattice_rewrite :
forall (A T T' : Type) (x : T -> T') (c : A -> lattice_for T)
(v : lattice_for A),
lattice_for_rect T' x (lattice_for_rect (lattice_for T) c v) =
lattice_for_rect T' (fun x0 : A => lattice_for_rect T' x (c x0)) v.
Axiom collapse_might_be_empty : bool.
Axiom PosSet : Type.
Axiom PosSet_inter : PosSet -> PosSet -> PosSet.
Goal
forall
(l2 : lattice_for PosSet)
(l0 : lattice_for PosSet),
lattice_for_rect Prop
(fun x : PosSet =>
lattice_for_rect Prop
(fun _ : PosSet => True)
(lattice_for_rect (lattice_for PosSet)
(fun y' : PosSet =>
constant
(if collapse_might_be_empty then PosSet_inter x y' else y')) l0)) l2
.
Proof.
intros.
rewrite lattice_rewrite.
(* Unbound rel in the goal *)
match goal with [ |- ?T ] => let _ := type of T in idtac end. |
ppedrot
added a commit
to ppedrot/coq
that referenced
this pull request
Jun 21, 2021
ppedrot
force-pushed
the
cache-constr-annotation-unfication-matchrec
branch
from
ec55829
to
74b37f2
Compare
|
OK, this should be working now. I stupidly forgot to accumulate the highest free variable in the branches of a case. I added the minimized test for good measure. |
|
Hey, I have detected that there were CI failures at commit 74b37f2 without any failure in the test-suite. |
|
@coqbot CI minimize |
|
I have initiated minimization at commit 74b37f2 for the suggested target ci-metacoq as requested. |
|
Error: Could not minimize file (from ci-metacoq) (full log on GitHub Actions) build log (truncated to last 26KiB; full 1.8MiB file on GitHub Actions Artifacts under
|
ppedrot
added a commit
to ppedrot/coq
that referenced
this pull request
Jun 21, 2021
ppedrot
force-pushed
the
cache-constr-annotation-unfication-matchrec
branch
from
74b37f2
to
cafc76b
Compare
|
@JasonGross done. This is what I call bleeding edge... |
|
@JasonGross looks like metacoq is broken on master, this is unrelated to this PR. |
|
Hey, I have detected that there were CI failures at commit cafc76b without any failure in the test-suite. |
The reason for the failure was that the |
Hum, that's weird because the corresponding job for the base commit failed in this case: https://gitlab.com/coq/coq/-/jobs/1364637965 |
We introduce a new internal type of annotated terms which are essentially a pair of a term and an annotation, in a recursive way. The annotation is a boolean standing for the closedness of the term. This guarantees a O(1) access to the underlying term, as well as a O(1) access to closedness. Building the annotation is O(n) in the term and is an upfront cost payed before entering the recursion. This trick could be generalized to any annotation which is local, i.e. only depends on the data of the direct subterms of a term. There are various places that could benefit from it, but for the time being I do not want to introduce yet another generic term API.
ppedrot
force-pushed
the
cache-constr-annotation-unfication-matchrec
branch
from
cafc76b
to
226c823
Compare
|
This is ready and needs an assignee. @SkySkimmer ? |
SkySkimmer
approved these changes
Jun 24, 2021
|
@coqbot: merge now |
jfehrle
pushed a commit
to jfehrle/coq
that referenced
this pull request
Sep 21, 2021
This was referenced Oct 26, 2021
Open
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
We introduce a new internal type of annotated terms which are essentially a pair of a term and an annotation, in a recursive way. The annotation is a boolean standing for the closedness of the term. This guarantees a O(1) access to the underlying term, as well as a O(1) access to closedness. Building the annotation is O(n) in the term and is an upfront cost payed before entering the recursion.
This trick could be generalized to any annotation which is local, i.e. only depends on the data of the direct subterms of a term. There are various places that could benefit from it, but for the time being I do not want to introduce yet another generic term API.
Fixes #12600.