Datatypes.v

(*
    Boilerplate necessary for converting between OCaml types and extracted Coq
    types without using Obj.magic.
*)

Require Import String.
Require Import Parser.

Inductive token_ind :=
    | LPAREN'tok
    | RPAREN'tok
    | NUM'tok : nat -> token_ind
    | OP'tok : string -> token_ind
    | EOF'tok.

(*
    Helper function to make expressions in get_token more readable.
    Essentially, get_sst just takes a terminal and a value of its
    corresponding semantic type, returning a token. This should likely be
    generated by "menhir --coq", but isn't yet.
*)
Definition get_sst (t : Gram.terminal) (sst : Gram.symbol_semantic_type (Gram.T t)) : Gram.token :=
    existT (fun t' => Gram.symbol_semantic_type (Gram.T t')) t sst.

Definition get_token (ti : token_ind) : Aut.GramDefs.token :=
    match ti with
        | LPAREN'tok =>
            get_sst Gram.LPAREN't tt
        | RPAREN'tok =>
            get_sst Gram.RPAREN't tt
        | NUM'tok n =>
            get_sst Gram.NUM't n
        | OP'tok str =>
            get_sst Gram.OP't str
        | EOF'tok =>
            get_sst Gram.EOF't tt
    end.