Source

calcoq / parser.ml

open Util
open CoqMain

(** lexer **)
type token =
  | MultOp
  | DivOp
  | AddOp
  | SubOp
  | Open
  | Close
  | Num of decimal
let stoken = function
  | MultOp -> "*"
  | DivOp -> "/"
  | AddOp -> "+"
  | SubOp -> "-"
  | Open -> "("
  | Close -> ")"
  | Num _ -> "Num_"


let rec tokens = function
  | [] -> []
  | '\t'::cs | '\n'::cs | ' '::cs | '\013'::cs -> tokens cs
  | '*' :: cs -> MultOp :: tokens cs
  | '/' :: cs -> DivOp :: tokens cs
  | '+' :: cs -> AddOp :: tokens cs
  | '-' :: cs -> SubOp :: tokens cs
  | '(' :: cs -> Open :: tokens cs
  | ')' :: cs -> Close :: tokens cs
  | ('0'..'9' as c1) :: cs -> num (Cons(deci_of_char c1, Nil)) cs
  | c :: cs -> failwith @@ "lexer: unknown token: ′" ^ string1 c ^ "′ " ^ char_concat cs
and num store = function
  | ('0'..'9' as c_i) :: cs -> num (Cons (deci_of_char c_i, store)) cs
  | cs -> Num store :: tokens cs
and deci_of_char = function
  | '0' -> D0
  | '1' -> D1
  | '2' -> D2
  | '3' -> D3
  | '4' -> D4
  | '5' -> D5
  | '6' -> D6
  | '7' -> D7
  | '8' -> D8
  | '9' -> D9
  | c -> failwith @@ "deci_of_char: " ^ string1 c


(** parser **)
type ('l, 'r) either = Inl of 'l | Inr of 'r

(* parser util----------------------*)
let (<|>) p1 p2 = fun code ->
  match p1 code, p2 code with
  | Inl (x1, ts), _ -> Inl (x1, ts)
  | _, Inl (x2, ts) -> Inl (x2, ts)
  | Inr (msg1), Inr (msg2) -> Inr (msg1 ^ " <|> " ^ msg2)

let (>>=) p f = fun code ->
  match p code with
  | Inl (x, ts) -> f x ts
  | Inr msg -> Inr msg

let return x = fun code -> Inl (x, code)

let (>>) p1 p2 = p1 >>= fun _ -> p2
let ( ** ) p1 p2 = p1 >>= fun x -> p2 >>= fun y -> return (x,y)
let ( *** ) p1 p2 = p1 >>= fun x -> p2 >>= fun y -> return (Pair(x,y))

let many p =
  let rec local store code = match p code with
    | Inl (x, ts) -> local (x::store) ts
    | Inr _ -> List.rev store, code
  in
  fun code -> Inl (local [] code)

(* for Coq list *)
let many' p =
  let rec local store code = match p code with
  | Inl (x, ts) -> local (Cons (x,store)) ts
  | Inr _ -> rev store, code
  in
  fun code -> Inl (local Nil code)

let opt p = fun code -> match p code with
  | Inl (x, ts) -> Inl (Some x, ts)
  | Inr _ ->  Inl (None, code)
(*-------------------------------*)

let vnum = function
  | Num cs :: ts -> Inl (VNum cs, ts)
  | _ -> Inr "vnum"
let prod_op = function
  | MultOp :: ts -> Inl (Mult, ts)
  | DivOp :: ts -> Inl (Div, ts)
  | _ -> Inr "prod_op"
let sum_op = function
  | AddOp :: ts -> Inl (Add, ts)
  | SubOp :: ts -> Inl (Sub, ts)
  | _ -> Inr "sum_op"
let token t = function
  | t1 :: ts when t = t1 -> Inl (t1, ts)
  | _ -> Inr "token"


let rec expr ts = (product() >>= fun p1 -> many' (sum_op *** product()) >>= fun op_p_list ->
  return (Expr (p1, op_p_list))) ts
and product () = value() >>= fun v1 -> many' (prod_op *** value()) >>= fun op_v_list ->
  return (Prod (v1, op_v_list))
and value () = vnum <|> (token Open >> expr >>= fun e -> token Close >> return (VExpr e))

let parse ts =
  match expr ts with
  | Inl (e, []) -> e
  | Inl (_, ts) -> failwith @@ "parse not end: " ^ Util.slist stoken ts
  | Inr msg -> failwith @@ "parse err: " ^ msg