Require Import String ZArith.
Require micheline_lexer micheline_parser.
Require micheline2michelson typer.
Require Import syntax.
Require Import syntax_type.
Require error_pp.
Import error.Notations.
Require main.

Section ParserHelpers.
  Variable input : String.string.
  Variable fuel : Datatypes.nat.

  Definition parsed_M :=
    let! x := main.lexed_M input in
    main.wrap_parser_result (micheline_parser.file fuel x).

  Definition michelson_seq_M :=
    let! x := parsed_M in
    micheline2michelson.micheline2michelson_instruction x.

  Definition michelson_typed_seq_M self_type ty :=
    let! x := michelson_seq_M in
    typer.type_instruction_seq (self_type := self_type) typer.Any x ty.

  Definition michelson_type_checked_seq_M self_type A B :=
    let! i := michelson_seq_M in
    typer.type_check_instruction_seq
      (self_type := self_type)
      (typer.type_instruction_seq typer.Any) i A B.

  Definition michelson_type_checked_M self_type A B :=
    let! i := michelson_seq_M in
    typer.type_check_instruction
      (self_type := self_type)
      (typer.type_instruction typer.Any)
      (untyped_syntax.Instruction_seq i) A B.

  Definition is_lexed := error_pp.m_pp (main.lexed_M input).

  Definition is_parsed := error_pp.m_pp parsed_M.

  Definition is_michelson := error_pp.m_pp michelson_seq_M.

  Definition type_check self_type ty := error_pp.m_pp (michelson_typed_seq_M self_type ty).

  Definition lf := micheline_pp.lf.

  Definition print_info self_type ty :=
    ("Lexing: " ++ is_lexed ++ lf ++
                "Parsing: " ++ is_parsed ++ lf ++
                "Expansion: " ++ is_michelson ++ lf ++
                "Type checking: " ++ type_check self_type ty ++ lf)%string.
End ParserHelpers.