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 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
  print_string "Content-type: text/html\n";
  print_string "\n";
  print_string
"<html>
<meta http-equiv='Content-Type' content='text/html; charset=EUC_JP'>
<head>
 <title>Free Calculator</title>
</head>

<body>
<a href='lambdavn/'>Lambda Vn</a>, 
<a href='http://d.hatena.ne.jp/yoshihiro503/'>Coq blog</a><br>

<h2>Free Calculator</h2>
<center>
<br>
<form action='index.cgi' method='post' name='calc'>
<table border=0 cellspacing=0 cellpadding=0>
 <tr><td valign=top>
  <table border=1 cellpadding=1 cellspacing=1 bgcolor=#7597dd id='free' width=650>
   <tr style='background-color: #e5ecf9;'>
    <td rowspan=2 valign=middle nowrap width=200>&nbsp;<b>Expression</b>&nbsp;</td>
    <td nowrap width=200>&nbsp;Digit number<select name='precision'>
     <option value='inf' selected>��</option>
    </select></td>
    <td nowrap width=200>&nbsp;</td>
    <td rowspan=2 nowrap align=center valign=middle >&nbsp;</td>
   </tr>
   <tr style='background-color: #e5ecf9;'>
    <td nowrap>&nbsp;</td>
    <td>&nbsp;</td>
   </tr>
   <tr style='background-color: #ffffff;'>
    <td colspan=4 valign=top><textarea style='border-style:none;' cols=73 rows=12 name='formula'>
";
  print_string text;
  print_string
"</textarea>
    </td>
   </tr>
   <tr><td height=35 valign=middle style='background-color:#e5ecf9;' colspan=4>
     &nbsp;&nbsp;<input type='submit' value='Execution'>
   </td></tr>
   <tr><td bgcolor='#e5ecf9' colspan=4>&nbsp;Answer
   </td></tr>
   <tr style='background-color: #ffffff;'><td nowrap valign='top' colspan=4><input size='79' style=' border-style: none;' type='text' id='ans' class='text' value='";
   print_string result;
   print_string "'>
   </td></tr>
  </table>
 </td></tr>
</table>
</form>
</center>
<br>
<div align=right>
Powered by <a href='http://caml.inria.fr/'><img src='caml.128x58.gif' alt='powered by OCaml' border='0' height='30'/></a>
and <a href='http://coq.inria.fr/'><img src='barron_logo.png' alt='powered by Coq' border='0' height='40'/></a>.
</div><br>
origin <a href='http://keisan.casio.jp/has10/Free.cgi'>�����ٷ׻�������</a><br>
Free CGI server: <a href='http://0web.cjb.net'>Zero Web Server</a><br>


</body>
</html>
"