Commit 76292c83 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Coq backend : do no longer use Stdlib's Stream library, which is likely to be...

Coq backend : do no longer use Stdlib's Stream library, which is likely to be deprecated because it is using positive coinductive types.
parent d0593e9a
Pipeline #67923 passed with stages
in 29 seconds
......@@ -11,7 +11,7 @@
(* *)
(****************************************************************************)
From Coq Require Import Streams List Syntax.
From Coq Require Import List Syntax.
From Coq.ssr Require Import ssreflect.
Require Automaton.
Require Import Alphabet Grammar Validator_safe.
......@@ -78,19 +78,25 @@ Lemma cast_eq T F (x : T) (eq : thunkP (x = x)) `{forall x y, Decidable (x = y)}
cast F eq a = a.
Proof. by rewrite /cast -Eqdep_dec.eq_rect_eq_dec. Qed.
(** Some operations on streams **)
(** Input buffers and operations on them. **)
CoInductive buffer : Type :=
Buf_cons { buf_head : token; buf_tail : buffer }.
(** Concatenation of a list and a stream **)
Fixpoint app_str {A:Type} (l:list A) (s:Stream A) :=
Delimit Scope buffer_scope with buf.
Bind Scope buffer_scope with buffer.
Infix "::" := Buf_cons (at level 60, right associativity) : buffer_scope.
(** Concatenation of a list and an input buffer **)
Fixpoint app_buf (l:list token) (buf:buffer) :=
match l with
| nil => s
| cons t q => Cons t (app_str q s)
| nil => buf
| cons t q => (t :: app_buf q buf)%buf
end.
Infix "++" := app_buf (at level 60, right associativity) : buffer_scope.
Infix "++" := app_str (right associativity, at level 60).
Lemma app_str_app_assoc {A:Type} (l1 l2:list A) (s:Stream A) :
l1 ++ (l2 ++ s) = (l1 ++ l2) ++ s.
Lemma app_buf_assoc (l1 l2:list token) (buf:buffer) :
(l1 ++ (l2 ++ buf) = (l1 ++ l2) ++ buf)%buf.
Proof. induction l1 as [|?? IH]=>//=. rewrite IH //. Qed.
(** The type of a non initial state: the type of semantic values associated
......@@ -268,14 +274,14 @@ Qed.
bogus and has perfomed a forbidden action. **)
Inductive step_result :=
| Fail_sr: step_result
| Accept_sr: symbol_semantic_type (NT (start_nt init)) -> Stream token -> step_result
| Progress_sr: stack -> Stream token -> step_result.
| Accept_sr: symbol_semantic_type (NT (start_nt init)) -> buffer -> step_result
| Progress_sr: stack -> buffer -> step_result.
(** [reduce_step] does a reduce action :
- pops some elements from the stack
- execute the action of the production
- follows the goto for the produced non terminal symbol **)
Definition reduce_step stk prod (buffer : Stream token)
Definition reduce_step stk prod (buffer : buffer)
(Hval : thunkP (valid_for_reduce (state_of_stack stk) prod))
(Hi : stack_invariant stk)
: step_result.
......@@ -341,7 +347,7 @@ Definition step stk buffer (Hi : stack_invariant stk): step_result :=
| Default_reduce_act prod => fun Hv =>
reduce_step stk prod buffer Hv Hi
| Lookahead_act awt => fun Hv =>
match Streams.hd buffer with
match buf_head buffer with
| tok =>
match awt (token_term tok) as a return
thunkP match a return Prop with Reduce_act p => _ | _ => _ end -> _
......@@ -349,7 +355,7 @@ Definition step stk buffer (Hi : stack_invariant stk): step_result :=
| Shift_act state_new e => fun _ =>
let sem_conv := eq_rect _ symbol_semantic_type (token_sem tok) _ e in
Progress_sr (existT noninitstate_type state_new sem_conv::stk)
(Streams.tl buffer)
(buf_tail buffer)
| Reduce_act prod => fun Hv =>
reduce_step stk prod buffer Hv Hi
| Fail_act => fun _ =>
......@@ -368,7 +374,7 @@ Proof.
assert (Hshift2 := shift_past_state (state_of_stack stk)).
destruct action_table as [prod|awt]=>/=.
- eauto using reduce_step_stack_invariant_preserved.
- set (term := token_term (Streams.hd buffer)).
- set (term := token_term (buf_head buffer)).
generalize (Hred term). clear Hred. intros Hred.
specialize (Hshift1 term). specialize (Hshift2 term).
destruct (awt term) as [state_new e|prod|]=>//.
......@@ -393,7 +399,7 @@ Qed.
Inductive parse_result {A : Type} :=
| Fail_pr: parse_result
| Timeout_pr: parse_result
| Parsed_pr: A -> Stream token -> parse_result.
| Parsed_pr: A -> buffer -> parse_result.
Global Arguments parse_result _ : clear implicits.
Fixpoint parse_fix stk buffer n_steps (Hi : stack_invariant stk):
......@@ -402,7 +408,7 @@ Fixpoint parse_fix stk buffer n_steps (Hi : stack_invariant stk):
| O => Timeout_pr
| S it =>
match step stk buffer Hi as r
return (forall stk' (buffer' : Stream token), r = _ -> _) -> _
return (forall stk' buffer', r = _ -> _) -> _
with
| Fail_sr => fun _ => Fail_pr
| Accept_sr t buffer_new => fun _ => Parsed_pr t buffer_new
......@@ -411,7 +417,7 @@ Fixpoint parse_fix stk buffer n_steps (Hi : stack_invariant stk):
end (step_stack_invariant_preserved _ _ _)
end.
Definition parse (buffer : Stream token) (n_steps : nat):
Definition parse (buffer : buffer) (n_steps : nat):
parse_result (symbol_semantic_type (NT (start_nt init))).
refine (parse_fix [] buffer n_steps _).
Proof.
......
......@@ -11,7 +11,7 @@
(* *)
(****************************************************************************)
From Coq Require Import Streams List Syntax Arith.
From Coq Require Import List Syntax Arith.
From Coq.ssr Require Import ssreflect.
Require Import Alphabet Grammar.
Require Automaton Interpreter Validator_complete.
......@@ -128,7 +128,7 @@ Variable init: initstate.
(** In order to prove compleness, we first fix a word to be parsed
together with the content of the parser at the end of the parsing. *)
Variable full_word: list token.
Variable buffer_end: Stream token.
Variable buffer_end: buffer.
(** Completeness is proved by following the traversal of the parse
tree which is performed by the parser. Each step of parsing
......@@ -222,7 +222,7 @@ Definition ptd_sem (ptd : pt_dot) :=
buffer left to be read by the parser when at the state represented
by the dotted parse tree. *)
Fixpoint ptlz_buffer {hole_symbs hole_word}
(ptlz:ptl_zipper hole_symbs hole_word): Stream token :=
(ptlz:ptl_zipper hole_symbs hole_word): buffer :=
match ptlz with
| Non_terminal_pt_ptlz ptz =>
ptz_buffer ptz
......@@ -230,7 +230,7 @@ Fixpoint ptlz_buffer {hole_symbs hole_word}
wordt ++ ptlz_buffer ptlz'
end
with ptz_buffer {hole_symb hole_word}
(ptz:pt_zipper hole_symb hole_word): Stream token :=
(ptz:pt_zipper hole_symb hole_word): buffer :=
match ptz with
| Top_ptz => buffer_end
| Cons_ptl_ptz _ ptlz =>
......@@ -240,7 +240,7 @@ with ptz_buffer {hole_symb hole_word}
Definition ptd_buffer (ptd:pt_dot) :=
match ptd with
| Reduce_ptd _ ptz => ptz_buffer ptz
| @Shift_ptd tok _ wordq _ ptlz => Cons tok (ptlz_buffer ptlz)
| @Shift_ptd tok _ wordq _ ptlz => (tok::ptlz_buffer ptlz)%buf
end.
(** We are now ready to define the main invariant of the proof of
......@@ -271,7 +271,7 @@ Fixpoint ptlz_future {hole_symbs hole_word}
Fixpoint ptlz_lookahead {hole_symbs hole_word}
(ptlz:ptl_zipper hole_symbs hole_word) : terminal :=
match ptlz with
| Non_terminal_pt_ptlz ptz => token_term (Streams.hd (ptz_buffer ptz))
| Non_terminal_pt_ptlz ptz => token_term (buf_head (ptz_buffer ptz))
| Cons_ptl_ptlz _ ptlz' => ptlz_lookahead ptlz'
end.
......@@ -298,7 +298,7 @@ Definition ptd_stack_compat (ptd:pt_dot) (stk:stack): Prop :=
| @Reduce_ptd prod _ ptl ptz =>
exists stk0,
state_has_future (state_of_stack init stk) prod []
(token_term (Streams.hd (ptz_buffer ptz))) /\
(token_term (buf_head (ptz_buffer ptz))) /\
ptl_stack_compat stk0 ptl stk /\
ptz_stack_compat stk0 ptz
| Shift_ptd tok ptl ptlz =>
......@@ -323,9 +323,9 @@ Lemma ptlz_future_ptlz_prod hole_symbs hole_word
Proof. induction ptlz=>//=. Qed.
Lemma ptlz_future_first {symbs word} (ptlz : ptl_zipper symbs word) :
TerminalSet.In (token_term (Streams.hd (ptlz_buffer ptlz)))
TerminalSet.In (token_term (buf_head (ptlz_buffer ptlz)))
(first_word_set (ptlz_future ptlz)) \/
token_term (Streams.hd (ptlz_buffer ptlz)) = ptlz_lookahead ptlz /\
token_term (buf_head (ptlz_buffer ptlz)) = ptlz_lookahead ptlz /\
nullable_word (ptlz_future ptlz) = true.
Proof.
induction ptlz as [|??? [|tok] pt ptlz IH]; [by auto| |]=>/=.
......@@ -475,11 +475,11 @@ Qed.
(** We prove that these functions behave well w.r.t. xxx_buffer. *)
Lemma ptd_buffer_build_from_pt {symb word}
(pt : parse_tree symb word) (ptz : pt_zipper symb word) :
word ++ ptz_buffer ptz = ptd_buffer (build_pt_dot_from_pt pt ptz)
(word ++ ptz_buffer ptz)%buf = ptd_buffer (build_pt_dot_from_pt pt ptz)
with ptd_buffer_build_from_pt_rec {symbs word}
(ptl : parse_tree_list symbs word) (ptlz : ptl_zipper symbs word)
Hsymbs :
word ++ ptlz_buffer ptlz = ptd_buffer (build_pt_dot_from_pt_rec ptl Hsymbs ptlz).
(word ++ ptlz_buffer ptlz)%buf = ptd_buffer (build_pt_dot_from_pt_rec ptl Hsymbs ptlz).
Proof.
- destruct pt as [tok|prod word ptl]=>/=.
+ f_equal. revert ptz. generalize [tok].
......@@ -490,12 +490,12 @@ Proof.
| |- context [match ?X with Some H => _ | None => _ end] => destruct X eqn:EQ
end.
* by rewrite -ptd_buffer_build_from_pt_rec.
* rewrite [X in X ++_](_ : word = []) //. clear -EQ. by destruct ptl.
* rewrite [X in (X ++ _)%buf](_ : word = []) //. clear -EQ. by destruct ptl.
- destruct ptl as [|?? ptl ?? pt]; [contradiction|].
specialize (ptd_buffer_build_from_pt_rec _ _ ptl).
destruct ptl.
+ by rewrite /= -ptd_buffer_build_from_pt.
+ by rewrite -ptd_buffer_build_from_pt_rec //= app_str_app_assoc.
+ by rewrite -ptd_buffer_build_from_pt_rec //= app_buf_assoc.
Qed.
Lemma ptd_buffer_build_from_ptl {symbs word}
......@@ -524,7 +524,7 @@ Proof.
change True with (match T (token_term tok) with T _ => True | NT _ => False end) at 1.
generalize (T (token_term tok)) => symb HT sem word ptz. by destruct ptz.
+ assert (state_has_future (state_of_stack init stk) prod
(rev' (prod_rhs_rev prod)) (token_term (Streams.hd (ptz_buffer ptz)))).
(rev' (prod_rhs_rev prod)) (token_term (buf_head (ptz_buffer ptz)))).
{ revert ptz Hstk. remember (NT (prod_lhs prod)) eqn:EQ=>ptz.
destruct ptz as [|?? ptl0 ?? ptlz0].
- intros ->. apply start_future. congruence.
......@@ -641,12 +641,12 @@ Proof.
generalize (reduce_ok safe (state_of_stack init stk)).
destruct ptd as [prod word ptl ptz|tok symbs word ptl ptlz].
- assert (Hfut : state_has_future (state_of_stack init stk) prod []
(token_term (Streams.hd (ptz_buffer ptz)))).
(token_term (buf_head (ptz_buffer ptz)))).
{ destruct Hstk as (? & ? & ?)=>//. }
assert (Hact := end_reduce _ _ _ _ Hfut eq_refl).
destruct action_table as [?|awt]=>Hval /=.
+ subst. by apply reduce_step_next_ptd.
+ set (term := token_term (Streams.hd (ptz_buffer ptz))) in *.
+ set (term := token_term (buf_head (ptz_buffer ptz))) in *.
generalize (Hval term). clear Hval. destruct (awt term)=>//. subst.
intros Hval. by apply reduce_step_next_ptd.
- destruct Hstk as (stk0 & Hfut & Hstk & Hstk0).
......
......@@ -11,7 +11,7 @@
(* *)
(****************************************************************************)
From Coq Require Import Streams List Syntax.
From Coq Require Import List Syntax.
Require Import Alphabet.
Require Grammar Automaton Interpreter.
From Coq.ssr Require Import ssreflect.
......@@ -95,16 +95,16 @@ Proof.
Qed.
(** [step] preserves the invariant **)
Lemma step_invariant stk word (buffer:Stream token) safe Hi :
Lemma step_invariant stk word buffer safe Hi :
word_has_stack_semantics word stk ->
match step safe init stk buffer Hi with
| Accept_sr sem buffer_new =>
exists word_new (pt:parse_tree (NT (start_nt init)) word_new),
word ++ buffer = word_new ++ buffer_new /\
(word ++ buffer = word_new ++ buffer_new)%buf /\
pt_sem pt = sem
| Progress_sr stk_new buffer_new =>
exists word_new,
word ++ buffer = word_new ++ buffer_new /\
(word ++ buffer = word_new ++ buffer_new)%buf /\
word_has_stack_semantics word_new stk_new
| Fail_sr => True
end.
......@@ -119,12 +119,12 @@ Proof.
+ destruct Hword_stk as [<- ?]; eauto.
- destruct buffer as [tok buffer]=>/=.
move=> /(_ (token_term tok)) Hv. destruct (awt (token_term tok)) as [st EQ|prod|]=>//.
+ eexists _. split; [by apply app_str_app_assoc with (l2 := [_])|].
+ eexists _. split; [by apply app_buf_assoc with (l2 := [_])|].
change (token_sem tok) with (pt_sem (Terminal_pt tok)).
generalize (Terminal_pt tok). generalize [tok].
rewrite -> EQ=>word' pt /=. by constructor.
+ apply (reduce_step_invariant stk prod (fun _ => Hv) Hi word
(Cons tok buffer)) in Hword_stk.
+ apply (reduce_step_invariant stk prod (fun _ => Hv) Hi word (tok::buffer))
in Hword_stk.
destruct reduce_step=>//.
* destruct Hword_stk as (pt & <- & <-); eauto.
* destruct Hword_stk as [<- ?]; eauto.
......@@ -137,18 +137,18 @@ Theorem parse_correct safe buffer n_steps:
match parse safe init buffer n_steps with
| Parsed_pr sem buffer_new =>
exists word_new (pt:parse_tree (NT (start_nt init)) word_new),
buffer = word_new ++ buffer_new /\
buffer = (word_new ++ buffer_new)%buf /\
pt_sem pt = sem
| _ => True
end.
Proof.
unfold parse.
change buffer with ([] ++ buffer) at 2. revert buffer. generalize Nil_stack_whss.
change buffer with ([] ++ buffer)%buf at 2. revert buffer. generalize Nil_stack_whss.
generalize (parse_subproof init).
generalize (@nil token). generalize (@nil (sigT noninitstate_type)).
induction n_steps as [|n_steps IH]=>//= stk word Hi Hword_stk buffer.
apply step_invariant with (buffer := buffer) (safe := safe) (Hi := Hi) in Hword_stk.
generalize (step_stack_invariant_preserved safe init stk (buffer) Hi).
apply (step_invariant _ _ buffer safe Hi) in Hword_stk.
generalize (step_stack_invariant_preserved safe init stk buffer Hi).
destruct step as [| |stk' buffer']=>//. clear Hi. move=> /(_ _ _ eq_refl) Hi.
destruct Hword_stk as (word' & -> & Hword'). by eapply IH.
Qed.
......
......@@ -34,7 +34,7 @@ Theorem parse_correct
match parse safe init n_steps buffer with
| Parsed_pr sem buffer_new =>
exists word (pt : parse_tree (NT (start_nt init)) word),
buffer = word ++ buffer_new /\
buffer = (word ++ buffer_new)%buf /\
pt_sem pt = sem
| _ => True
end.
......@@ -63,10 +63,11 @@ Theorem unambiguity:
pt_sem tree1 = pt_sem tree2.
Proof.
intros Hsafe Hcomp [tok] init word tree1 tree2.
assert (Hcomp1 := parse_complete Hsafe init (pt_size tree1) word (Streams.const tok)
Hcomp tree1).
assert (Hcomp2 := parse_complete Hsafe init (pt_size tree1) word (Streams.const tok)
Hcomp tree2).
pose (buf_end := cofix buf_end := (tok :: buf_end)%buf).
assert (Hcomp1 := parse_complete Hsafe init (pt_size tree1) word buf_end
Hcomp tree1).
assert (Hcomp2 := parse_complete Hsafe init (pt_size tree1) word buf_end
Hcomp tree2).
destruct parse.
- destruct Hcomp1.
- exfalso. eapply PeanoNat.Nat.lt_irrefl, Hcomp1.
......
......@@ -6,6 +6,8 @@ export
.PHONY: all clean install uninstall
all:
_CoqProject:
@ $(MAKE) -f Makefile.coq --no-print-directory _CoqProject
......
......@@ -477,15 +477,15 @@ module Run (T: sig end) = struct
Lr1.fold_entry (fun _prod node startnt _t () ->
let funName = Nonterminal.print true startnt in
fprintf f "Definition %s : nat -> Streams.Stream token -> MenhirLibParser.Inter.parse_result %s := MenhirLibParser.parse safe Aut.%s.\n\n"
fprintf f "Definition %s : nat -> MenhirLibParser.Inter.buffer -> MenhirLibParser.Inter.parse_result %s := MenhirLibParser.parse safe Aut.%s.\n\n"
funName (print_type (Nonterminal.ocamltype startnt)) (print_init node);
fprintf f "Theorem %s_correct (iterator : nat) (buffer : Streams.Stream token):\n" funName;
fprintf f "Theorem %s_correct (iterator : nat) (buffer : MenhirLibParser.Inter.buffer):\n" funName;
fprintf f " match %s iterator buffer with\n" funName;
fprintf f " | MenhirLibParser.Inter.Parsed_pr sem buffer_new =>\n";
fprintf f " exists word (tree : Gram.parse_tree (%s) word),\n"
(print_symbol (Symbol.N startnt));
fprintf f " buffer = MenhirLibParser.Inter.app_str word buffer_new /\\\n";
fprintf f " buffer = MenhirLibParser.Inter.app_buf word buffer_new /\\\n";
fprintf f " Gram.pt_sem tree = sem\n";
fprintf f " | _ => True\n";
fprintf f " end.\n";
......@@ -493,9 +493,9 @@ module Run (T: sig end) = struct
if not Settings.coq_no_complete then
begin
fprintf f "Theorem %s_complete (iterator : nat) (word : list token) (buffer_end : Streams.Stream token) :\n" funName;
fprintf f "Theorem %s_complete (iterator : nat) (word : list token) (buffer_end : MenhirLibParser.Inter.buffer) :\n" funName;
fprintf f " forall tree : Gram.parse_tree (%s) word,\n" (print_symbol (Symbol.N startnt));
fprintf f " match %s iterator (MenhirLibParser.Inter.app_str word buffer_end) with\n" funName;
fprintf f " match %s iterator (MenhirLibParser.Inter.app_buf word buffer_end) with\n" funName;
fprintf f " | MenhirLibParser.Inter.Fail_pr => False\n";
fprintf f " | MenhirLibParser.Inter.Parsed_pr output_res buffer_end_res =>\n";
fprintf f " output_res = Gram.pt_sem tree /\\\n";
......
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