Commit fa91ef1b authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Coq backend : Make generated parsers executable.

parent 1eaae61e
Pipeline #65063 passed with stages
in 20 seconds
......@@ -111,8 +111,8 @@ try assumption.
apply (compare_trans _ _ _ _ H H0).
Qed.
(** Special case of comparable, where equality is usual equality. **)
Class ComparableUsualEq {A:Type} (C: Comparable A) :=
(** Special case of comparable, where equality is Leibniz equality. **)
Class ComparableLeibnizEq {A:Type} (C: Comparable A) :=
compare_eq : forall x y, compare x y = Eq -> x = y.
(** Boolean equality for a [Comparable]. **)
......@@ -122,7 +122,7 @@ Definition compare_eqb {A:Type} {C:Comparable A} (x y:A) :=
| _ => false
end.
Theorem compare_eqb_iff {A:Type} {C:Comparable A} {U:ComparableUsualEq C} :
Theorem compare_eqb_iff {A:Type} {C:Comparable A} {U:ComparableLeibnizEq C} :
forall x y, compare_eqb x y = true <-> x = y.
Proof.
unfold compare_eqb.
......@@ -133,13 +133,13 @@ destruct H.
rewrite compare_refl; intuition.
Qed.
Instance NComparableUsualEq : ComparableUsualEq natComparable := Nat.compare_eq.
Instance NComparableLeibnizEq : ComparableLeibnizEq natComparable := Nat.compare_eq.
(** A pair of ComparableUsualEq is ComparableUsualEq **)
Instance PairComparableUsualEq
{A:Type} {CA:Comparable A} (UA:ComparableUsualEq CA)
{B:Type} {CB:Comparable B} (UB:ComparableUsualEq CB) :
ComparableUsualEq (PairComparable CA CB).
(** A pair of ComparableLeibnizEq is ComparableLeibnizEq **)
Instance PairComparableLeibnizEq
{A:Type} {CA:Comparable A} (UA:ComparableLeibnizEq CA)
{B:Type} {CB:Comparable B} (UB:ComparableLeibnizEq CB) :
ComparableLeibnizEq (PairComparable CA CB).
Proof.
intros x y; destruct x, y; simpl.
pose proof (compare_eq a a0); pose proof (compare_eq b b0).
......@@ -155,10 +155,10 @@ Class Finite (A:Type) := {
all_list_forall : forall x:A, In x all_list
}.
(** An alphabet is both [ComparableUsualEq] and [Finite]. **)
(** An alphabet is both [ComparableLeibnizEq] and [Finite]. **)
Class Alphabet (A:Type) := {
AlphabetComparable :> Comparable A;
AlphabetComparableUsualEq :> ComparableUsualEq AlphabetComparable;
AlphabetComparableLeibnizEq :> ComparableLeibnizEq AlphabetComparable;
AlphabetFinite :> Finite A
}.
......@@ -187,9 +187,19 @@ Next Obligation.
- rewrite Pos.compare_gt_iff in *. eauto using Pos.lt_trans.
Qed.
Next Obligation.
intros x y. unfold compare. rewrite Pos.compare_eq_iff. intros Hxy.
rewrite <-(surj_inj_compat x), <-(surj_inj_compat y). congruence.
Qed.
intros x y. unfold compare. intros Hxy.
assert (Hxy' : inj x = inj y).
(* We do not use [Pos.compare_eq_iff] directly to make sure the
proof is executable. *)
{ destruct (Pos.eq_dec (inj x) (inj y)) as [|[]]; [now auto|].
now apply Pos.compare_eq_iff. }
(* Using rewrite here leads to non-executable proofs. *)
transitivity (surj (inj x)).
{ apply eq_sym, surj_inj_compat. }
transitivity (surj (inj y)); cycle 1.
{ apply surj_inj_compat. }
apply f_equal, Hxy'.
Defined.
Next Obligation.
rewrite <-(surj_inj_compat x).
generalize (inj_bound_spec x). generalize (inj x). clear x. intros x.
......@@ -205,38 +215,6 @@ Next Obligation.
- rewrite Pos.iter_succ. destruct Pos.iter. simpl in IH2. subst. reflexivity.
Qed.
(** Previous class instances for [option A] **)
Program Instance OptionComparable {A:Type} (C:Comparable A) : Comparable (option A) :=
{ compare := fun x y =>
match x, y return comparison with
| None, None => Eq
| None, Some _ => Lt
| Some _, None => Gt
| Some x, Some y => compare x y
end }.
Next Obligation. destruct x, y; intuition. apply compare_antisym. Qed.
Next Obligation.
destruct x, y, z; try now intuition;
try (rewrite <- H in H0; discriminate).
apply (compare_trans _ _ _ _ H H0).
Qed.
Instance OptionComparableUsualEq {A:Type} {C:Comparable A} (U:ComparableUsualEq C) :
ComparableUsualEq (OptionComparable C).
Proof.
intros [] []; simpl; try reflexivity; try discriminate.
intros ->%compare_eq. reflexivity.
Qed.
Program Instance OptionFinite {A:Type} (E:Finite A) : Finite (option A) :=
{ all_list := None :: map Some all_list }.
Next Obligation.
destruct x; intuition.
right.
apply in_map.
apply all_list_forall.
Defined.
(** Definitions of [FSet]/[FMap] from [Comparable] **)
Require Import OrderedTypeAlt.
Require FSetAVL.
......
......@@ -40,22 +40,22 @@ Module Symbol(Import A:Alphs).
AlphabetFinite := {| all_list :=
map T all_list++map NT all_list |} }.
Next Obligation.
destruct x; destruct y; intuition; apply compare_antisym.
destruct x; destruct y; intuition; apply compare_antisym.
Qed.
Next Obligation.
destruct x; destruct y; destruct z; intuition; try discriminate.
apply (compare_trans _ t0); intuition.
apply (compare_trans _ n0); intuition.
destruct x; destruct y; destruct z; intuition; try discriminate.
apply (compare_trans _ t0); intuition.
apply (compare_trans _ n0); intuition.
Qed.
Next Obligation.
intros x y.
destruct x; destruct y; try discriminate; intros.
rewrite (compare_eq t t0); intuition.
rewrite (compare_eq n n0); intuition.
Qed.
intros x y.
destruct x; destruct y; try discriminate; intros.
rewrite (compare_eq t t0); now intuition.
rewrite (compare_eq n n0); now intuition.
Defined.
Next Obligation.
rewrite in_app_iff.
destruct x; [left | right]; apply in_map; apply all_list_forall.
rewrite in_app_iff.
destruct x; [left | right]; apply in_map; apply all_list_forall.
Qed.
End Symbol.
......
......@@ -26,7 +26,7 @@ Class Decidable (P : Prop) := decide : {P} + {~P}.
Arguments decide _ {_}.
(** A [Comparable] type has decidable equality. *)
Instance comparable_decidable_eq T `{ComparableUsualEq T} (x y : T) :
Instance comparable_decidable_eq T `{ComparableLeibnizEq T} (x y : T) :
Decidable (x = y).
Proof.
unfold Decidable.
......
......@@ -135,7 +135,7 @@ module Run (T: sig end) = struct
fprintf f "Program Instance %sAlph : %sAlphabet.Alphabet %s :=\n" name menhirlib_path name;
fprintf f " { AlphabetComparable := {| compare := fun x y =>\n";
fprintf f " match x, y return comparison with end |};\n";
fprintf f " AlphabetEnumerable := {| all_list := [] |} }.";
fprintf f " AlphabetEnumerable := {| all_list := []%%list |} }.";
end
let write_terminals f =
......@@ -184,17 +184,17 @@ module Run (T: sig end) = struct
fprintf f " { p:nonterminal * list symbol &\n";
fprintf f " %sGrammar.arrows_right\n" menhirlib_path;
fprintf f " (symbol_semantic_type (NT (fst p)))\n";
fprintf f " (map symbol_semantic_type (snd p)) }\n";
fprintf f " (List.map symbol_semantic_type (snd p)) }\n";
fprintf f " :=\n";
fprintf f " let box := existT (fun p =>\n";
fprintf f " %sGrammar.arrows_right\n" menhirlib_path;
fprintf f " (symbol_semantic_type (NT (fst p)))\n";
fprintf f " (map symbol_semantic_type (snd p)) )\n";
fprintf f " (List.map symbol_semantic_type (snd p)) )\n";
fprintf f " in\n";
fprintf f " match p with\n";
Production.iterx (fun prod ->
fprintf f " | %s => box\n" (print_prod prod);
fprintf f " (%s, [%s])\n"
fprintf f " (%s, [%s]%%list)\n"
(print_nterm (Production.nt prod))
(String.concat "; "
(List.map print_symbol (List.rev (Array.to_list (Production.rhs prod)))));
......@@ -236,7 +236,7 @@ module Run (T: sig end) = struct
if !first then first := false else fprintf f "; ";
fprintf f "%s" (print_term t)
) firstSet;
fprintf f "]\n");
fprintf f "]%%list\n");
fprintf f " end.\n\n"
let write_grammar f =
......@@ -335,7 +335,7 @@ module Run (T: sig end) = struct
(Invariant.fold (fun l _ symb _ -> print_symbol symb::l)
[] (Invariant.stack node)))
in
fprintf f " | %s => [%s]\n" (print_nis node) s);
fprintf f " | %s => [%s]%%list\n" (print_nis node) s);
fprintf f " end.\n";
fprintf f "Extract Constant past_symb_of_non_init_state => \"fun _ -> assert false\".\n\n"
......@@ -370,7 +370,7 @@ module Run (T: sig end) = struct
(Invariant.fold (fun accu _ _ states -> get_stateset_id states::accu)
[] (Invariant.stack node))
in
bprintf b " | %s => [ %s ]\n" (print_nis node) s);
bprintf b " | %s => [ %s ]%%list\n" (print_nis node) s);
bprintf b " end.\n";
Buffer.output_buffer f b;
fprintf f "Extract Constant past_state_of_non_init_state => \"fun _ -> assert false\".\n\n"
......@@ -399,7 +399,7 @@ module Run (T: sig end) = struct
else fprintf f "; ";
fprintf f "%s" (print_term lookahead)
) lookaheadset;
fprintf f "].\nExtract Inlined Constant %s => \"assert false\".\n\n" id;
fprintf f "]%%list.\nExtract Inlined Constant %s => \"assert false\".\n\n" id;
id
in
let b = Buffer.create 256 in
......@@ -416,7 +416,7 @@ module Run (T: sig end) = struct
(print_prod prod) pos (get_lookaheadset_id lookaheads);
end
) (Lr0.closure (Lr0.export (Lr1.state node)));
bprintf b " ].\n";
bprintf b " ]%%list.\n";
bprintf b "Extract Inlined Constant items_of_state_%d => \"assert false\".\n\n" (Lr1.number node)
);
Buffer.output_buffer f b;
......@@ -428,7 +428,7 @@ module Run (T: sig end) = struct
fprintf f " end.\n";
end
else
fprintf f "Definition items_of_state (s:state): list item := [].\n";
fprintf f "Definition items_of_state (s:state): list item := []%%list.\n";
fprintf f "Extract Constant items_of_state => \"fun _ -> assert false\".\n\n"
let write_automaton f =
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment