Commits

yoshihiro503  committed ec4b09d

import

  • Participants

Comments (0)

Files changed (6)

+#/bin/sh
+coqc main.v
+rm coqMain.mli
+ocamlopt nums.cmxa str.cmxa util.ml coqMain.ml reader.ml parser.ml main.ml -o index0.cgi
+rm *.cmx *.cmi *.o *.vo
+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>
+"
+Require Import QArith.
+Open Scope Q_scope.
+
+Require Import List.
+Inductive deci : Set :=
+  | D0 : deci | D1 : deci | D2 : deci | D3 : deci | D4 : deci
+  | D5 : deci | D6 : deci | D7 : deci | D8 : deci | D9 : deci.
+Definition decimal := list deci.
+
+Inductive prod_op : Set :=
+  | Mult : prod_op | Div : prod_op.
+Inductive sum_op : Set :=
+  | Add : sum_op | Sub : sum_op.
+
+Inductive value : Set := VNum : decimal -> value | VExpr : expr -> value
+with product : Set := Prod : value -> list (prod_op * value) -> product
+with expr : Set := Expr : product -> list (sum_op * product) -> expr.
+
+Definition q_of_deci d := match d with
+  | D0 => 0 # 1
+  | D1 => 1 # 1
+  | D2 => 2 # 1
+  | D3 => 3 # 1
+  | D4 => 4 # 1
+  | D5 => 5 # 1
+  | D6 => 6 # 1
+  | D7 => 7 # 1
+  | D8 => 8 # 1
+  | D9 => 9 # 1
+  end.
+Definition q10 := 10 # 1.
+Fixpoint q_of_decimal ds := match ds with
+  | nil => 0
+  | cons d_i ds => q_of_deci d_i + q10 * q_of_decimal ds
+  end.
+
+Inductive term : Set :=
+  | TVal : Q -> term
+  | TExpr : expr -> term
+  | TProd : prod_op -> term -> term -> term
+  | TSum  : sum_op  -> term -> term -> term.
+
+Definition term_of_val v := match v with
+  | VNum n  => TVal (q_of_decimal n)
+  | VExpr e => TExpr e
+  end.
+Fixpoint reduce t := match t with
+  | TVal q => TVal q
+  | TExpr (Expr (Prod v nil) nil) => term_of_val v
+  | TExpr (Expr (Prod v1 (cons (Mult, v2) tl)) nil) =>
+      TProd Mult (term_of_val v1) (TExpr (Expr (Prod v2 tl) nil))
+  | TExpr (Expr (Prod v1 (cons (Div,  v2) tl)) nil) =>
+      TProd Div  (term_of_val v1) (TExpr (Expr (Prod v2 tl) nil))
+  | TExpr (Expr p1 (cons (Add, p2) tl)) =>
+      TSum Add (TExpr (Expr p1 nil)) (TExpr (Expr p2 tl))
+  | TExpr (Expr p1 (cons (Sub, p2) tl)) =>
+      TSum Sub (TExpr (Expr p1 nil)) (TExpr (Expr p2 tl))
+  | TProd Mult (TVal q1) (TVal q2) => TVal (q1 * q2)
+  | TProd Div  (TVal q1) (TVal q2) => TVal (q1 / q2)
+  | TProd op t1 t2 => TProd op (reduce t1) (reduce t2)
+  | TSum Add (TVal q1) (TVal q2) => TVal (q1 + q2)
+  | TSum Sub (TVal q1) (TVal q2) => TVal (q1 - q2)
+  | TSum op t1 t2 => TSum op (reduce t1) (reduce t2)
+  end.
+
+
+Extraction "coqMain.ml" rev reduce Qred.
+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: &prime;" ^ string1 c ^ "&prime; " ^ 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
+open Str
+open Util
+
+(** decode : string -> string **)
+let decode text =
+  let parce_char c = match c with
+    | '0'..'9' -> int_of_char c - int_of_char '0'
+    | 'a'..'f' -> 10 + int_of_char c - int_of_char 'a'
+    | 'A'..'F' -> 10 + int_of_char c - int_of_char 'A'
+    | _ -> failwith ("decode parce_char: " ^ String.make 1 c)
+  in
+  let rec aux i s =
+    if i < String.length s then
+      match s.[i] with
+      | '+' -> (s.[i] <- ' '; aux (i+1) s)
+      | '%' -> String.sub s 0 i
+          ^ String.make 1 (char_of_int (16 * parce_char s.[i+1] + parce_char s.[i+2]))
+          ^ aux 0 (String.sub s (i+3) (String.length s - i - 3))
+      | _ -> aux (i+1) s
+    else s
+  in aux 0 text
+
+(* TODO
+let get_input () =
+  let parse_16char = function
+    | '0'..'9' -> int_of_char c - int_of_char '0'
+    | 'a'..'f' -> 10 + int_of_char c - int_of_char 'a'
+    | 'A'..'F' -> 10 + int_of_char c - int_of_char 'A'
+    | _ -> failwith ("decode parse_16char: " ^ String.make 1 c)
+	try
+	  begin match read_char () with
+	  | '+' -> (' '::)
+*)
+
+let read_all () =
+  let rec iter store =
+    try iter (read_line () :: store) with
+    | End_of_file -> String.concat "" (List.rev store)
+  in iter []
+
+let get_text () =
+  let input = decode (read_all ()) in
+  if input = "" then ""
+  else
+    try
+    let ps = List.map (split (regexp "=")) (split (regexp "&") input) in
+    match List.find (function | "formula"::_ -> true | _ -> false) ps with
+    | [formula] -> ""
+    | [formula; t] -> t
+    | _ -> failwith @@ "Reader.get_text: " ^ input
+    with
+    | e -> Printexc.to_string e ^ ": " ^ input
+let ( @@ ) f x = f x
+let ( $ ) g f x = g (f x)
+
+let slist ?(delim="; ") f l = (String.concat delim @@ List.map f l)
+
+let string1 c = String.make 1 c
+
+let char_concat = slist ~delim:"" (String.make 1)
+let cs_string s =
+  let rec iter store i =
+    if i < 0 then store
+    else iter (s.[i]::store) (i-1)
+  in
+  iter [] (String.length s - 1)