expr.mlog

module type INPUT = sig
  type index

  type token

  pred is_index : index

  pred token_at : index * token * index
end

module type GRAMMAR = sig
  type non_terminal
  type token
  type rhs

  constant start : non_terminal

  (* naturally gives regular right-hand sides!

     the 'rhs' is a state in some state machine where the transitions
     are non-terminals or tokens. If it is 'infinite' state, then we'd
     have data driven parsers? *)

  pred nt_to_rhs : non_terminal * rhs

  pred rhs_nt   : rhs * non_terminal * rhs
  pred rhs_tok  : rhs * token * rhs
  pred rhs_stop : rhs
end

module ExprGrammar = struct
  type non_terminal = { `E }

  constant start : non_terminal = `E

  type token = { `x | `plus }

  type rhs = { `E1_0 | `E1_1 | `E2_0 | `E2_1 | `E2_2 | `E2_3 }

  define nt_to_rhs : non_terminal * rhs
      nt_to_rhs (`E, `E1_0)
      nt_to_rhs (`E, `E2_0)

  define rhs_tok : rhs * token * rhs
      rhs_tok (`E1_0, `x, `E1_1)
      rhs_tok (`E2_1, `plus, `E2_2)

  define rhs_nt : rhs * non_terminal * rhs
      rhs_nt (`E2_0, `E, `E2_1)
      rhs_nt (`E2_2, `E, `E2_3)

  define rhs_stop : rhs
      rhs_stop (`E1_1)
      rhs_stop (`E2_3)
end

(* Basically computes the intersection of a CFG with a regular language... *)
module Recogniser (G : GRAMMAR) (I : INPUT with type token = G.token) =
struct

  (* parse (i, nt, j) if the symbol 'nt' is recognised between 'i' and
  'j' in the input. *)

  define
    parse : I.index * G.non_terminal * I.index
    parse (?i, ?nt, ?j) :-
      G.nt_to_rhs (?nt, ?rhs), parse_rhs (?i, ?rhs, ?j)

  and
    parse_rhs : I.index * G.rhs * I.index
    parse_rhs (?i, ?rhs, ?i) :-
       G.rhs_stop (?rhs), I.is_index (?i)
    parse_rhs (?i, ?rhs, ?j) :-
       G.rhs_tok (?rhs, ?tok, ?rhs'),
       I.token_at (?i, ?tok, ?i'),
       parse_rhs (?i', ?rhs', ?j)
    parse_rhs (?i, ?rhs, ?j) :-
       G.rhs_nt (?rhs, ?nt, ?rhs'),
       parse (?i, ?nt, ?i'), parse_rhs (?i', ?rhs', ?j)

  define
    parse_between : I.index * I.index
    parse_between (?i, ?j) :- parse (?i, G.start, ?j)

end

module TestInput = struct
  type index = int

  type token = { `x | `plus }

  define is_index : index
      is_index (0)
      is_index (1)
      is_index (2)
      is_index (3)

  define token_at : index * token * index
      token_at (0,`x,1)
      token_at (1,`plus,2)
      token_at (2,`x,3)
end

module R = Recogniser (ExprGrammar) (TestInput)