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

Axiom-free development, the interpreter should evaluate inside Coq with reasonnable performance.

parent ec31fb4f
......@@ -12,8 +12,7 @@
(* *)
(* *********************************************************************)
From Coq Require Import Int31 Cyclic31 Omega List Syntax
Relations RelationClasses.
From Coq Require Import Int31 Cyclic31 Omega List Syntax Relations RelationClasses.
Local Obligation Tactic := intros.
......@@ -135,14 +134,6 @@ destruct H.
rewrite compare_refl; intuition.
Qed.
(** [Comparable] provides a decidable equality. **)
Definition compare_eqdec {A:Type} {C:Comparable A} {U:ComparableUsualEq C} (x y:A):
{x = y} + {x <> y}.
Proof.
destruct (compare x y) as [] eqn:?; [left; apply compare_eq; intuition | ..];
right; intro; destruct H; rewrite compare_refl in Heqc; discriminate.
Defined.
Instance NComparableUsualEq : ComparableUsualEq natComparable := Nat.compare_eq.
(** A pair of ComparableUsualEq is ComparableUsualEq **)
......
......@@ -13,7 +13,7 @@
(* *********************************************************************)
From Coq Require Import List Syntax Orders.
From MenhirLib Require Import Alphabet Tuples.
From MenhirLib Require Import Alphabet.
(** The terminal non-terminal alphabets of the grammar. **)
Module Type Alphs.
......@@ -61,9 +61,11 @@ Module Symbol(Import A:Alphs).
End Symbol.
Module Type T.
Export Tuples.
(** A curryfied function with multiple parameters **)
Definition arrows_right: Type -> list Type -> Type :=
fold_right (fun A B => A -> B).
Module Type T.
Include Alphs <+ Symbol.
(** [symbol_semantic_type] maps a symbols to the type of its semantic
......
......@@ -13,15 +13,73 @@
(* *********************************************************************)
From Coq Require Import Streams List Syntax.
From Coq.Program Require Import Equality.
From Coq.ssr Require Import ssreflect.
From MenhirLib Require Automaton.
From MenhirLib Require Import Alphabet.
From MenhirLib Require Import Alphabet Grammar.
From MenhirLib Require Import Validator_safe.
Module Make(Import A:Automaton.T).
Module Import ValidSafe := Validator_safe.Make A.
(** A few helpers for dependent types. *)
(** Decidable propositions. *)
Class Decidable (P : Prop) := decide : {P} + {~P}.
Arguments decide _ {_}.
(** A [Comparable] type has decidable equality. *)
Instance comparable_decidable_eq T `{Comparable T, ComparableUsualEq T} (x y : T) :
Decidable (x = y).
Proof.
unfold Decidable.
destruct (compare x y) eqn:EQ; [left; apply compare_eq; intuition | ..];
right; intros ->; by rewrite compare_refl in EQ.
Defined.
Instance list_decidable_eq T :
(forall x y : T, Decidable (x = y)) ->
(forall l1 l2 : list T, Decidable (l1 = l2)).
Proof. unfold Decidable. decide equality. Defined.
Ltac subst_existT :=
repeat
match goal with
| _ => progress subst
| H : @existT ?A ?P ?x ?y1 = @existT ?A ?P ?x ?y2 |- _ =>
let DEC := fresh in
assert (DEC : forall u1 u2 : A, Decidable (u1 = u2)) by apply _;
apply Eqdep_dec.inj_pair2_eq_dec in H; [|by apply DEC];
clear DEC
end.
(** The interpreter is written using dependent types. In order to
avoid reducing proof terms while executing the parser, we thunk all
the propositions behind an arrow.
Note that thunkP is still in Prop so that it is erased by
extraction.
*)
Definition thunkP (P : Prop) : Prop := True -> P.
(** Sometimes, we actually need a reduced proof in a program (for
example when using an equality to cast a value). In that case,
instead of reducing the proof we already have, we reprove the
assertion by using decidability. *)
Definition reprove {P} `{Decidable P} (p : thunkP P) : P :=
match decide P with
| left p => p
| right np => False_ind _ (np (p I))
end.
(** Combination of reprove with eq_rect. *)
Definition cast {T : Type} (F : T -> Type) {x y : T} (eq : thunkP (x = y))
`{Decidable (x = y)}:
F x -> F y :=
fun a => eq_rect x F a y (reprove eq).
Lemma cast_eq T F (x : T) (eq : thunkP (x = x)) `{forall x y, Decidable (x = y)} a :
cast F eq a = a.
Proof. by rewrite /cast -Eqdep_dec.eq_rect_eq_dec. Qed.
(** Some operations on streams **)
(** Concatenation of a list and a stream **)
......@@ -107,30 +165,30 @@ with stack_invariant_next: stack -> Prop :=
values using [sem_popped] as an accumulator and discards the popped
states.**)
Fixpoint pop (symbols_to_pop:list symbol) {A:Type} (stk:stack) :
prefix symbols_to_pop (symb_stack_of_stack stk) ->
thunkP (prefix symbols_to_pop (symb_stack_of_stack stk)) ->
forall (action:arrows_right A (map symbol_semantic_type symbols_to_pop)),
stack * A.
unshelve refine
(match symbols_to_pop
return
prefix symbols_to_pop (symb_stack_of_stack stk) ->
(thunkP (prefix symbols_to_pop (symb_stack_of_stack stk))) ->
forall (action:arrows_right A (map _ symbols_to_pop)), stack * A
with
| [] => fun _ action => (stk, action)
| t::q => fun Hp action =>
match stk
return prefix (t::q) (symb_stack_of_stack stk) -> stack * A
return thunkP (prefix (t::q) (symb_stack_of_stack stk)) -> stack * A
with
| existT _ state_cur sem::stack_rec => fun Hp =>
let sem_conv := eq_rect _ symbol_semantic_type sem _ _ in
let sem_conv := cast symbol_semantic_type _ sem in
pop q _ stack_rec _ (action sem_conv)
| [] => fun Hp => False_rect _ _
end Hp
end).
Proof.
- simpl in Hp. clear -Hp. abstract now inversion Hp.
- simpl in Hp. clear -Hp. abstract now inversion Hp.
- simpl in Hp. clear -Hp. abstract now inversion Hp.
- simpl in Hp. clear -Hp. abstract (intros _ ; specialize (Hp I); now inversion Hp).
- clear -Hp. abstract (specialize (Hp I); now inversion Hp).
- simpl in Hp. clear -Hp. abstract (intros _ ; specialize (Hp I); now inversion Hp).
Defined.
(* Equivalent declarative specification for pop, so that we avoid
......@@ -154,11 +212,13 @@ Proof.
induction symbols_to_pop as [|t symbols_to_pop IH]=>stk Hp action /=.
- split.
+ intros [= <- <-]. constructor.
+ intros H. inversion H. simpl_existTs. by subst.
+ intros H. inversion H. by subst_existT.
- destruct stk as [|[st sem]]=>/=; [by destruct pop_subproof0|].
destruct pop_subproof=>/=. rewrite IH. split.
remember (pop_subproof t symbols_to_pop stk st Hp) as EQ eqn:eq. clear eq.
generalize EQ. revert Hp action. rewrite <-(EQ I)=>Hp action ?.
rewrite cast_eq. rewrite IH. split.
+ intros. by constructor.
+ intros H. inversion H. simpl_existTs. by subst.
+ intros H. inversion H. by subst_existT.
Qed.
......@@ -218,28 +278,29 @@ Inductive step_result :=
- execute the action of the production
- follows the goto for the produced non terminal symbol **)
Definition reduce_step stk prod (buffer : Stream token)
(Hval : valid_for_reduce (state_of_stack stk) prod)
(Hval : thunkP (valid_for_reduce (state_of_stack stk) prod))
(Hi : stack_invariant stk)
: step_result.
refine
((let '(stk', sem) as ss := pop (prod_rhs_rev prod) stk _ (prod_action prod)
return state_valid_after_pop (state_of_stack (fst ss)) _ _ -> _
return thunkP (state_valid_after_pop (state_of_stack (fst ss)) _ _) -> _
in fun Hval' =>
match goto_table (state_of_stack stk') (prod_lhs prod) as goto
return (goto = _ -> _) -> _
return (thunkP (goto = _ -> _ : Prop)) -> _
with
| Some (exist _ state_new e) => fun _ =>
let sem := eq_rect _ _ sem _ e in
Progress_sr (existT noninitstate_type state_new sem::stk') buffer
| None => fun Hval =>
let sem := eq_rect _ (fun symb => symbol_semantic_type symb) sem _ _ in
let sem := cast symbol_semantic_type _ sem in
Accept_sr sem buffer
end (proj2 Hval _ Hval'))
(pop_state_valid _ _ _ _ _ _ _)).
end (fun _ => proj2 (Hval I) _ (Hval' I)))
(fun _ => pop_state_valid _ _ _ _ _ _ _)).
Proof.
- clear -Hi Hval.
abstract (destruct Hi; eapply prefix_ass; [apply Hval|eassumption]).
- clear -Hval. abstract (f_equal; specialize (Hval eq_refl); destruct stk' as [|[]]=>//).
abstract (intros _; destruct Hi; eapply prefix_ass; [by apply Hval|eassumption]).
- clear -Hval.
abstract (intros _; f_equal; specialize (Hval I eq_refl); destruct stk' as [|[]]=>//).
- clear -Hi. abstract by destruct Hi.
Defined.
......@@ -256,7 +317,7 @@ Proof.
destruct pop as [stk0 sem]=>/=. simpl in Hi'. intros Hv'.
assert (Hgoto1:=goto_head_symbs (state_of_stack stk0) (prod_lhs prod)).
assert (Hgoto2:=goto_past_state (state_of_stack stk0) (prod_lhs prod)).
match goal with | |- context [proj2 Hv ?s ?H] => generalize (proj2 Hv s H) end.
match goal with | |- context [fun _ : True => ?X] => generalize X end.
destruct goto_table as [[state_new e]|] eqn:EQgoto=>//.
intros _ [= <- <-]. constructor=>/=.
- constructor. eapply prefix_ass. apply Hgoto1. by destruct Hi'.
......@@ -269,10 +330,11 @@ Qed.
(** One step of parsing. **)
Definition step stk buffer (Hi : stack_invariant stk): step_result :=
match action_table (state_of_stack stk) as a return
match a return Prop with
| Default_reduce_act prod => _
| Lookahead_act awt => _
end -> _
thunkP
match a return Prop with
| Default_reduce_act prod => _
| Lookahead_act awt => _
end -> _
with
| Default_reduce_act prod => fun Hv =>
reduce_step stk prod buffer Hv Hi
......@@ -280,7 +342,7 @@ Definition step stk buffer (Hi : stack_invariant stk): step_result :=
match Streams.hd buffer with
| existT _ term sem =>
match awt term as a return
match a return Prop with Reduce_act p => _ | _ => _ end -> _
thunkP match a return Prop with Reduce_act p => _ | _ => _ end -> _
with
| Shift_act state_new e => fun _ =>
let sem_conv := eq_rect _ symbol_semantic_type sem _ e in
......@@ -290,9 +352,9 @@ Definition step stk buffer (Hi : stack_invariant stk): step_result :=
reduce_step stk prod buffer Hv Hi
| Fail_act => fun _ =>
Fail_sr
end (Hv term)
end (fun _ => Hv I term)
end
end (reduce_ok _).
end (fun _ => reduce_ok _).
Lemma step_stack_invariant_preserved stk buffer Hi stk' buffer':
step stk buffer Hi = Progress_sr stk' buffer' ->
......
......@@ -12,10 +12,10 @@
(* *)
(* *********************************************************************)
From Coq Require Import Streams Equality List Syntax Arith.
From Coq Require Import Streams List Syntax Arith.
From Coq.ssr Require Import ssreflect.
From MenhirLib Require Import Alphabet.
From MenhirLib Require Grammar Automaton Interpreter Validator_complete.
From MenhirLib Require Import Alphabet Grammar.
From MenhirLib Require Automaton Interpreter Validator_complete.
Module Make(Import A:Automaton.T) (Import Inter:Interpreter.T A).
Module Import Valid := Validator_complete.Make A.
......@@ -72,7 +72,7 @@ Proof.
* destruct IH.
move=>[/TerminalSet.union_1 [?|?]|[??]];
auto using TerminalSet.union_2, TerminalSet.union_3.
+ rewrite Bool.andb_false_r. intuition.
+ rewrite Bool.andb_false_r. by intuition.
Qed.
(** If the first predicate has been validated, then it is correct. **)
......@@ -595,7 +595,7 @@ Proof.
| |- context [pop_state_valid init ?A stk ?B ?C ?D ?E ?F] =>
generalize (pop_state_valid init A stk B C D E F)
end.
rewrite Hstk /=. intros Hv. generalize (proj2 Hval (state_of_stack init stk0) Hv).
rewrite Hstk /=. intros Hv. generalize (proj2 (Hval I) (state_of_stack init stk0) Hv).
clear Hval Hstk Hi Hv stk.
assert (Hgoto := fun fut prod' =>
non_terminal_goto (state_of_stack init stk0) prod' (NT (prod_lhs prod)::fut)).
......@@ -621,13 +621,13 @@ Proof.
apply (ptd_stack_compat_build_from_ptl _ _ _ stk0'); auto; [].
split=>//. by exists eq_refl.
- intros Hv.
generalize (reduce_step_subproof0 _ prod _ (ptl_sem ptl (prod_action _)) Hv).
generalize (reduce_step_subproof0 _ prod _ (ptl_sem ptl (prod_action _)) (fun _ => Hv)).
intros EQnt. clear Hv Hgoto'.
change (ptl_sem ptl (prod_action prod))
with (pt_sem (Non_terminal_pt prod ptl)).
generalize (Non_terminal_pt prod ptl). clear ptl. destruct ptz.
+ intros pt. f_equal. rewrite -Eqdep.Eq_rect_eq.eq_rect_eq //.
+ intros pt. f_equal. by rewrite cast_eq.
+ edestruct Hgoto. eapply ptz_stack_compat_cons_state_has_future, Hstk0.
Qed.
......
......@@ -12,7 +12,7 @@
(* *)
(* *********************************************************************)
From Coq Require Import Streams List Syntax Equality.
From Coq Require Import Streams List Syntax.
From MenhirLib Require Import Alphabet.
From MenhirLib Require Grammar Automaton Interpreter.
From Coq.ssr Require Import ssreflect.
......@@ -57,7 +57,7 @@ Proof.
induction Hspec as [stk sem|symbols_to_pop st stk action sem stk' res Hspec IH];
intros word_stk Hword_stk.
- exists word_stk, [], Nil_ptl. rewrite -app_nil_end. eauto.
- inversion Hword_stk. simpl_existTs. subst.
- inversion Hword_stk. subst_existT.
edestruct IH as (word_stk' & word_res & ptl & ? & Hword_stk'' & ?); [eassumption|].
subst. eexists word_stk', (word_res ++ _)%list, (Cons_ptl ptl _).
split; [|split]=>//. rewrite app_assoc //.
......@@ -83,13 +83,16 @@ Proof.
destruct pop as [stk' sem] eqn:Hpop=>/= Hv'.
apply pop_spec_ok in Hpop. apply pop_spec_ptl with (word_stk := word) in Hpop=>//.
destruct Hpop as (word1 & word2 & ptl & <- & Hword1 & <-).
match goal with | |- context [proj2 Hv ?x1 ?x2] => generalize (proj2 Hv x1 x2) end.
match goal with | |- context [proj2 (Hv I) ?x1 ?x2] => generalize (proj2 (Hv I) x1 x2) end.
destruct goto_table as [[st' EQ]|].
- intros _. split=>//.
change (ptl_sem ptl (prod_action prod)) with (pt_sem (Non_terminal_pt prod ptl)).
generalize (Non_terminal_pt prod ptl). rewrite ->EQ. intros pt. by constructor.
- intros Hstk'. destruct Hword1; [|by destruct Hstk'].
destruct reduce_step_subproof0. exists (Non_terminal_pt prod ptl). by split.
generalize (reduce_step_subproof0 init prod [] (ptl_sem ptl (prod_action prod))
(fun _ : True => Hstk')).
simpl in Hstk'. rewrite -Hstk' // => EQ. rewrite cast_eq.
exists (Non_terminal_pt prod ptl). by split.
Qed.
(** [step] preserves the invariant **)
......@@ -110,7 +113,8 @@ Proof.
intros Hword_stk. unfold step.
generalize (reduce_ok safe (state_of_stack init stk)).
destruct action_table as [prod|awt].
- intros Hv. apply (reduce_step_invariant stk prod Hv Hi word buffer) in Hword_stk.
- intros Hv.
apply (reduce_step_invariant stk prod (fun _ => Hv) Hi word buffer) in Hword_stk.
destruct reduce_step=>//.
+ destruct Hword_stk as (pt & <- & <-); eauto.
+ destruct Hword_stk as [<- ?]; eauto.
......@@ -122,7 +126,7 @@ Proof.
unfold token.
generalize [existT (fun t => symbol_semantic_type (T t)) term sem].
rewrite -> EQ=>word' pt /=. by constructor.
+ apply (reduce_step_invariant stk prod Hv Hi word
+ apply (reduce_step_invariant stk prod (fun _ => Hv) Hi word
(Cons (existT _ term sem) buffer)) in Hword_stk.
destruct reduce_step=>//.
* destruct Hword_stk as (pt & <- & <-); eauto.
......
......@@ -67,8 +67,10 @@ Proof.
Hcomp tree1).
assert (Hcomp2 := parse_complete Hsafe init (pt_size tree1) word (Streams.const tok)
Hcomp tree2).
destruct parse; auto with exfalso zarith.
destruct Hcomp1 as [-> _], Hcomp2 as [-> _]. reflexivity.
destruct parse.
- destruct Hcomp1.
- exfalso. eapply PeanoNat.Nat.lt_irrefl, Hcomp1.
- destruct Hcomp1 as [-> _], Hcomp2 as [-> _]. reflexivity.
Qed.
End Make.
(* *********************************************************************)
(* *)
(* Menhir *)
(* *)
(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation, either version 3 of *)
(* the License, or (at your option) any later version. *)
(* *)
(* *********************************************************************)
From Coq Require Import List Syntax Equality.
(** A curryfied function with multiple parameters **)
Definition arrows_left: list Type -> Type -> Type :=
fold_left (fun A B => B -> A).
(** A curryfied function with multiple parameters **)
Definition arrows_right: Type -> list Type -> Type :=
fold_right (fun A B => A -> B).
(** A tuple is a heterogeneous list. For convenience, we use pairs. **)
Fixpoint tuple (types : list Type) : Type :=
match types with
| nil => unit
| t::q => prod t (tuple q)
end.
Fixpoint uncurry {args:list Type} {res:Type}:
arrows_left args res -> tuple args -> res :=
match args return forall res, arrows_left args res -> tuple args -> res with
| [] => fun _ f _ => f
| t::q => fun res f p => let (d, t) := p in
(@uncurry q _ f t) d
end res.
Lemma arrows_left_right_map_rev_append A B l1 l2 (f : B -> Type) :
arrows_left (map f (rev_append l1 l2)) A =
arrows_left (map f l2) (arrows_right A (map f l1)).
Proof.
revert l2. induction l1 as [|C l1 IH]; intros l2; [|simpl; rewrite IH]; reflexivity.
Qed.
Lemma JMeq_eqrect:
forall (U:Type) (a b:U) (P:U -> Type) (x:P a) (e:a=b),
eq_rect a P x b e ~= x.
Proof.
destruct e.
reflexivity.
Qed.
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