Source

calcoq / main.ml

open Util
open Reader
open Parser
open CoqMain

module Big = Big_int

let b1 = Big.unit_big_int
let double b = Big.mult_big_int (Big.big_int_of_int 2) b
let rec bint_of_positive = function
  | XI p -> Big.succ_big_int (double (bint_of_positive p))
  | XO p -> double (bint_of_positive p)
  | XH -> b1
let spositive p = Big.string_of_big_int (bint_of_positive p)

let sz = function
  | Z0 -> "O"
  | Zpos p -> spositive p
  | Zneg p -> "-" ^ spositive p
let sq q =
  if (q.qden = XH) then sz q.qnum
  else sz q.qnum ^ "/" ^ spositive q.qden

let input_all fname =
  Util.infile fname (fun ch ->
    let rec iter store =
      try iter (input_line ch :: store) with
      | End_of_file -> slist ~delim:"\n" id @@ List.rev store
    in iter [])

let main =
  let result, text =
    try
      let text = Reader.get_text () in
      try
	if text = "" then "",""
	else
	  match Parser.tokens (cs_string text) with
	  | [] -> "", text
	  | ts ->
	      let e = Parser.parse ts in
	      let rec eval = function
		| TVal q -> qred q
		| t -> eval (CoqMain.reduce t)
	      in
	      sq (eval (TExpr e)), text
      with
      | e -> "OCaml " ^ Printexc.to_string e, text
    with
    | e -> "Objective Caml " ^ Printexc.to_string e, ""
  in
  let templ = input_all "index.template" in
  let html = Str.global_replace (Str.regexp "::text::") text templ
      +> Str.global_replace (Str.regexp "::result::") result
  in
  print_string "Content-type: text/html\n";
  print_string "\n";
  print_string html