Commit 678f8ec7 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Coq backend : the token type is now an inductive.

parent fa91ef1b
......@@ -86,14 +86,18 @@ Module Type T.
arrows_right
(symbol_semantic_type (NT (prod_lhs p)))
(map symbol_semantic_type (prod_rhs_rev p)).
(** Tokens are the atomic elements of the input stream: they contain
a terminal and a semantic value of the type corresponding to this
terminal. *)
Parameter token : Type.
Parameter token_term : token -> terminal.
Parameter token_sem :
forall tok : token, symbol_semantic_type (T (token_term tok)).
End T.
Module Defs(Import G:T).
(** A token is a terminal and a semantic value for this terminal. **)
Definition token := {t:terminal & symbol_semantic_type (T t)}.
(** The semantics of a grammar is defined in two stages. First, we
define the notion of parse tree, which represents one way of
recognizing a word with a head symbol. Semantic values are stored
......@@ -106,8 +110,7 @@ Module Defs(Import G:T).
(** Parse tree for a terminal symbol. *)
| Terminal_pt:
forall (t:terminal) (sem:symbol_semantic_type (T t)),
parse_tree (T t) [existT (fun t => symbol_semantic_type (T t)) t sem]
forall (tok:token), parse_tree (T (token_term tok)) [tok]
(** Parse tree for a non-terminal symbol. *)
| Non_terminal_pt:
......@@ -135,7 +138,7 @@ Module Defs(Import G:T).
Fixpoint pt_sem {head_symbol word} (tree:parse_tree head_symbol word) :
symbol_semantic_type head_symbol :=
match tree with
| Terminal_pt _ sem => sem
| Terminal_pt tok => token_sem tok
| Non_terminal_pt prod ptl => ptl_sem ptl (prod_action prod)
end
with ptl_sem {A head_symbols word} (tree:parse_tree_list head_symbols word) :
......@@ -147,7 +150,7 @@ Module Defs(Import G:T).
Fixpoint pt_size {head_symbol word} (tree:parse_tree head_symbol word) :=
match tree with
| Terminal_pt _ _ => 1
| Terminal_pt _ => 1
| Non_terminal_pt _ l => S (ptl_size l)
end
with ptl_size {head_symbols word} (tree:parse_tree_list head_symbols word) :=
......
......@@ -331,26 +331,30 @@ Definition step stk buffer (Hi : stack_invariant stk): step_result :=
thunkP
match a return Prop with
| Default_reduce_act prod => _
| Lookahead_act awt => _
| Lookahead_act awt => forall t : terminal,
match awt t with
| Reduce_act p => _
| _ => True
end
end -> _
with
| Default_reduce_act prod => fun Hv =>
reduce_step stk prod buffer Hv Hi
| Lookahead_act awt => fun Hv =>
match Streams.hd buffer with
| existT _ term sem =>
match awt term as a return
| tok =>
match awt (token_term tok) as a return
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
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)
| Reduce_act prod => fun Hv =>
reduce_step stk prod buffer Hv Hi
| Fail_act => fun _ =>
Fail_sr
end (fun _ => Hv I term)
end (fun _ => Hv I (token_term tok))
end
end (fun _ => reduce_ok _).
......@@ -364,7 +368,7 @@ Proof.
assert (Hshift2 := shift_past_state (state_of_stack stk)).
destruct action_table as [prod|awt]=>/=.
- eauto using reduce_step_stack_invariant_preserved.
- destruct (Streams.hd buffer) as [term sem].
- set (term := token_term (Streams.hd buffer)).
generalize (Hred term). clear Hred. intros Hred.
specialize (Hshift1 term). specialize (Hshift2 term).
destruct (awt term) as [state_new e|prod|]=>//.
......@@ -403,8 +407,7 @@ Fixpoint parse_fix stk buffer n_steps (Hi : stack_invariant stk): parse_result:=
end.
Definition parse (buffer : Stream token) (n_steps : nat): parse_result.
refine
(parse_fix [] buffer n_steps _).
refine (parse_fix [] buffer n_steps _).
Proof.
abstract (repeat constructor; intros; by destruct singleton_state_pred).
Defined.
......
This diff is collapsed.
......@@ -117,16 +117,14 @@ Proof.
destruct reduce_step=>//.
+ destruct Hword_stk as (pt & <- & <-); eauto.
+ destruct Hword_stk as [<- ?]; eauto.
- destruct buffer as [[term sem] buffer]=>/=.
move=> /(_ term) Hv. destruct (awt term) as [st EQ|prod|]=>//.
- 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 := [_])|].
change sem with (pt_sem (Terminal_pt term sem)) at 2.
generalize (Terminal_pt term sem).
unfold token.
generalize [existT (fun t => symbol_semantic_type (T t)) term sem].
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 (existT _ term sem) buffer)) in Hword_stk.
(Cons tok buffer)) in Hword_stk.
destruct reduce_step=>//.
* destruct Hword_stk as (pt & <- & <-); eauto.
* destruct Hword_stk as [<- ?]; eauto.
......
......@@ -38,17 +38,13 @@ module Run (T: sig end) = struct
| Symbol.N nt -> sprintf "NT %s" (print_nterm nt)
| Symbol.T t -> sprintf "T %s" (print_term t)
exception No_type
let print_type ty =
if Settings.coq_no_actions then
"unit"
else
match ty with
| None -> raise No_type
| Some t -> match t with
| Stretch.Declared s -> s.Stretch.stretch_content
| Stretch.Inferred _ -> assert false (* We cannot infer coq types *)
if Settings.coq_no_actions then "unit"
else match ty with
| None -> "unit"
| Some t -> match t with
| Stretch.Declared s -> s.Stretch.stretch_content
| Stretch.Inferred _ -> assert false (* We cannot infer coq types *)
let is_final_state node =
match Default.has_default_reduction node with
......@@ -111,6 +107,14 @@ module Run (T: sig end) = struct
if Front.grammar.BasicSyntax.parameters <> [] then
Error.error [] "the Coq back-end does not support %%parameter."
let write_tokens f =
fprintf f "Inductive token : Type :=";
Terminal.iter_real (fun term ->
fprintf f "\n| %s : %s%%type -> token"
(Terminal.print term) (print_type (Terminal.ocamltype term))
);
fprintf f ".\n\n"
let write_inductive_alphabet f name constrs =
fprintf f "Inductive %s' : Set :=" name;
List.iter (fprintf f "\n| %s") constrs;
......@@ -123,8 +127,6 @@ module Run (T: sig end) = struct
fprintf f " { inj := fun x => match x return _ with ";
iteri (fun k constr -> fprintf f "\n | %s => %d%%positive" constr k);
fprintf f "\n end;\n";
(* Pattern matching on int31 litterals will disappear when
native 63 bits integers will be introduced in Coq. *)
fprintf f " surj := (fun n => match n return _ with ";
iteri (fprintf f "\n | %d%%positive => %s ");
fprintf f "\n | _ => %s\n end)%%Z;\n" (List.hd constrs);
......@@ -152,11 +154,9 @@ module Run (T: sig end) = struct
let write_symbol_semantic_type f =
fprintf f "Definition terminal_semantic_type (t:terminal) : Type:=\n";
fprintf f " match t with\n";
Terminal.iter (fun terminal ->
if not (Terminal.pseudo terminal) then
Terminal.iter_real (fun terminal ->
fprintf f " | %s => %s%%type\n"
(print_term terminal)
(try print_type (Terminal.ocamltype terminal) with No_type -> "unit")
(print_term terminal) (print_type (Terminal.ocamltype terminal))
);
fprintf f " end.\n\n";
......@@ -174,6 +174,20 @@ module Run (T: sig end) = struct
fprintf f " | NT nt => nonterminal_semantic_type nt\n";
fprintf f " end.\n\n"
let write_token_term f =
fprintf f "Definition token_term (tok : token) : terminal :=\n";
fprintf f " match tok with\n";
Terminal.iter_real (fun terminal ->
fprintf f " | %s _ => %s\n" (Terminal.print terminal) (print_term terminal));
fprintf f " end.\n\n"
let write_token_sem f =
fprintf f "Definition token_sem (tok : token) : symbol_semantic_type (T (token_term tok)) :=\n";
fprintf f " match tok with\n";
Terminal.iter_real (fun terminal ->
fprintf f " | %s x => x\n" (Terminal.print terminal));
fprintf f " end.\n\n"
let write_productions f =
write_inductive_alphabet f "production" (
Production.foldx (fun prod l -> (print_prod prod)::l) []);
......@@ -246,6 +260,9 @@ module Run (T: sig end) = struct
write_nonterminals f;
fprintf f "Include %sGrammar.Symbol.\n\n" menhirlib_path;
write_symbol_semantic_type f;
fprintf f "Definition token := token.\n\n";
write_token_term f;
write_token_sem f;
write_productions f;
write_productions_contents f;
fprintf f "Include %sGrammar.Defs.\n\n" menhirlib_path;
......@@ -282,20 +299,15 @@ module Run (T: sig end) = struct
fprintf f "Lookahead_act (fun terminal:terminal =>\n";
fprintf f " match terminal return lookahead_action terminal with\n";
let has_fail = ref false in
Terminal.iter (fun t ->
if not (Terminal.pseudo t) then
begin
try
let target = SymbolMap.find (Symbol.T t) (Lr1.transitions node) in
fprintf f " | %s => Shift_act %s (eq_refl _)\n" (print_term t) (print_nis target)
with Not_found ->
try
let prod =
Misc.single (TerminalMap.find t (Lr1.reductions node))
in
fprintf f " | %s => Reduce_act %s\n" (print_term t) (print_prod prod)
with Not_found -> has_fail := true
end);
Terminal.iter_real (fun t ->
try
let target = SymbolMap.find (Symbol.T t) (Lr1.transitions node) in
fprintf f " | %s => Shift_act %s (eq_refl _)\n" (print_term t) (print_nis target)
with Not_found ->
try
let prod = Misc.single (TerminalMap.find t (Lr1.reductions node)) in
fprintf f " | %s => Reduce_act %s\n" (print_term t) (print_prod prod)
with Not_found -> has_fail := true);
if !has_fail then
fprintf f " | _ => Fail_act\n";
fprintf f " end)\n"
......@@ -470,7 +482,7 @@ module Run (T: sig end) = struct
fprintf f "Theorem %s_correct iterator buffer:\n" funName;
fprintf f "Theorem %s_correct (iterator : nat) (buffer : Streams.Stream token):\n" funName;
fprintf f " match %s iterator buffer with\n" funName;
fprintf f " | Parser.Inter.Parsed_pr sem buffer_new =>\n";
fprintf f " exists word (tree : Gram.parse_tree (%s) word),\n"
......@@ -483,7 +495,7 @@ module Run (T: sig end) = struct
if not Settings.coq_no_complete then
begin
fprintf f "Theorem %s_complete (iterator:nat) word buffer_end:\n" funName;
fprintf f "Theorem %s_complete (iterator : nat) (word : list token) (buffer_end : Streams.Stream token) :\n" funName;
fprintf f " forall tree : Gram.parse_tree (%s) word,\n" (print_symbol (Symbol.N startnt));
fprintf f " match %s iterator (Parser.Inter.app_str word buffer_end) with\n" funName;
fprintf f " | Parser.Inter.Fail_pr => False\n";
......@@ -511,6 +523,7 @@ module Run (T: sig end) = struct
fprintf f "Unset Elimination Schemes.\n\n";
write_tokens f;
write_grammar f;
write_automaton f;
write_theorems 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