Module Main

Require Grammar.
Require Automaton.
Require Interpreter_safe.
Require Interpreter_correct.
Require Interpreter_complete.
Require Import Syntax.

Module Make(Export Aut:Automaton.T).
Export Aut.Gram.
Export Aut.GramDefs.

Module Import Inter := Interpreter.Make Aut.
Module Safe := Interpreter_safe.Make Aut Inter.
Module Correct := Interpreter_correct.Make Aut Inter.
Module Complete := Interpreter_complete.Make Aut Inter.

Definition complete_validator:unit->bool := Complete.Valid.is_complete.
Definition safe_validator:unit->bool := Safe.Valid.is_safe.
Definition parse (safe:safe_validator ()=true) init n_steps buffer : parse_result init:=
  Safe.parse_with_safe (Safe.Valid.is_safe_correct safe) init buffer n_steps.

Theorem parse_correct
  (safe:safe_validator ()= true) init n_steps buffer:
  match parse safe init n_steps buffer with
    | Parsed_pr sem buffer_new =>
      exists word,
        buffer = word ++ buffer_new /\ inhabited (parse_tree (NT (start_nt init)) word sem)
    | _ => True
  end.

Theorem parse_complete
  (safe:safe_validator () = true) init n_steps word buffer_end sem:
  complete_validator () = true ->
  forall tree:parse_tree (NT (start_nt init)) word sem,
  match parse safe init n_steps (word ++ buffer_end) with
    | Fail_pr => False
    | Parsed_pr sem_res buffer_end_res =>
      sem_res = sem /\ buffer_end_res = buffer_end /\ pt_size tree <= n_steps
    | Timeout_pr => n_steps < pt_size tree
  end.

Theorem unambiguity:
  safe_validator () = true -> complete_validator () = true -> inhabited token ->
  forall init word,
  forall sem1 (tree1:parse_tree (NT (start_nt init)) word sem1),
  forall sem2 (tree2:parse_tree (NT (start_nt init)) word sem2),
  sem1 = sem2.

End Make.