Commit 01aeda9e authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Get rid of some Obj.t in the interface of the extraction of Coq parsers.

parent 678f8ec7
Pipeline #65180 passed with stages
in 26 seconds
......@@ -386,13 +386,18 @@ Qed.
a failure (the automaton has rejected the input word), either a timeout
(the automaton has spent all the given [n_steps]), either a parsed semantic
value with a rest of the input buffer.
Note that we do not make parse_result depend on start_nt for the result
type, so that this inductive is extracted without the use of Obj.t in OCaml.
**)
Inductive parse_result :=
Inductive parse_result {A : Type} :=
| Fail_pr: parse_result
| Timeout_pr: parse_result
| Parsed_pr: symbol_semantic_type (NT (start_nt init)) -> Stream token -> parse_result.
| Parsed_pr: A -> Stream token -> parse_result.
Global Arguments parse_result _ : clear implicits.
Fixpoint parse_fix stk buffer n_steps (Hi : stack_invariant stk): parse_result:=
Fixpoint parse_fix stk buffer n_steps (Hi : stack_invariant stk):
parse_result (symbol_semantic_type (NT (start_nt init))) :=
match n_steps return _ with
| O => Timeout_pr
| S it =>
......@@ -406,7 +411,8 @@ Fixpoint parse_fix stk buffer n_steps (Hi : stack_invariant stk): parse_result:=
end (step_stack_invariant_preserved _ _ _)
end.
Definition parse (buffer : Stream token) (n_steps : nat): parse_result.
Definition parse (buffer : Stream token) (n_steps : nat):
parse_result (symbol_semantic_type (NT (start_nt init))).
refine (parse_fix [] buffer n_steps _).
Proof.
abstract (repeat constructor; intros; by destruct singleton_state_pred).
......@@ -414,13 +420,9 @@ Defined.
End Interpreter.
Arguments Fail_sr [init].
Arguments Accept_sr [init] _ _.
Arguments Progress_sr [init] _ _.
Arguments Fail_pr [init].
Arguments Timeout_pr [init].
Arguments Parsed_pr [init] _ _.
Arguments Fail_sr {init}.
Arguments Accept_sr {init} _ _.
Arguments Progress_sr {init} _ _.
End Make.
......
......@@ -24,7 +24,8 @@ Module Complete := Interpreter_complete.Make Aut Inter.
Definition complete_validator:unit->bool := Complete.Valid.is_complete.
Definition safe_validator:unit->bool := ValidSafe.is_safe.
Definition parse (safe:safe_validator ()=true) init n_steps buffer : parse_result init:=
Definition parse (safe:safe_validator ()=true) init n_steps buffer :
parse_result (symbol_semantic_type (NT (start_nt init))):=
parse (ValidSafe.is_safe_correct safe) init buffer n_steps.
(** Correction theorem. **)
......
......@@ -124,10 +124,10 @@ module Run (T: sig end) = struct
begin
let iteri f = ignore (List.fold_left (fun k x -> f k x; succ k) 1 constrs) in
fprintf f "Program Instance %sNum : %sAlphabet.Numbered %s :=\n" name menhirlib_path name;
fprintf f " { inj := fun x => match x return _ with ";
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";
fprintf f " surj := (fun n => match n return _ with ";
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);
fprintf f " inj_bound := %d%%positive }.\n" (List.length constrs);
......@@ -477,10 +477,8 @@ 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 := Parser.parse safe Aut.%s.\n\n"
funName (print_init node);
fprintf f "Definition %s : nat -> Streams.Stream token -> Parser.Inter.parse_result %s := Parser.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 " match %s iterator buffer with\n" funName;
......@@ -491,7 +489,7 @@ module Run (T: sig end) = struct
fprintf f " Gram.pt_sem tree = sem\n";
fprintf f " | _ => True\n";
fprintf f " end.\n";
fprintf f "Proof. apply Parser.parse_correct. Qed.\n\n";
fprintf f "Proof. apply Parser.parse_correct with (init:=Aut.%s). Qed.\n\n" (print_init node);
if not Settings.coq_no_complete then
begin
......
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