Commit 5a468639 authored by Heiko Becker's avatar Heiko Becker

Fix stupid bug in Coq main function

parent a4ae8c3e
......@@ -5,12 +5,11 @@ open String;;
open Char;;
open Big_int;;
let str_join s1 s2 = String.concat "" [s1;s2];;
let explode s = let rec exp i l = if i < 0 then l else exp (i - 1) ((s.[i]) :: l) in exp (String.length s - 1) [];;
let rec implode sl =
match sl with
|c :: sl' -> str_join (String.make 1 c) (implode sl')
|c :: sl' -> (String.make 1 c)^(implode sl')
|[] -> "";;
(*
......@@ -23,7 +22,7 @@ let read_file filename =
let chan = open_in filename in
try
while true; do
text := str_join (!text)(input_line chan)
text := (!text) ^ (input_line chan) ^ "\n";
done; !text
with End_of_file ->
close_in chan;
......@@ -32,77 +31,3 @@ let read_file filename =
let input = read_file (Sys.argv.(1));;
let res = implode (CoqChecker.runChecker (explode (input)));;
let () = printf "%s\n" res;;
(* let rec pow a = function
| 0 -> 1
| 1 -> a
| n ->
let b = pow a (n / 2) in
b * b * (if n mod 2 = 0 then 1 else a);;
let calc n fac=
n - ((n / (pow 2 fac)) * (pow 2 fac));;
let char_to_ascii (c:char):CoqChecker.ascii =
let ord = code c in
let fst = if ord >= (pow 2 7) then CoqChecker.True else CoqChecker.False in
let ord = calc ord 7 in
let snd = if ord >= (pow 2 6) then CoqChecker.True else CoqChecker.False in
let ord = calc ord 6 in
let thd = if ord >= (pow 2 5) then CoqChecker.True else CoqChecker.False in
let ord = calc ord 5 in
let fth = if ord >= (pow 2 4) then CoqChecker.True else CoqChecker.False in
let ord = calc ord 4 in
let fft = if ord >= (pow 2 3) then CoqChecker.True else CoqChecker.False in
let ord = calc ord 3 in
let sxt = if ord >= (pow 2 2) then CoqChecker.True else CoqChecker.False in
let ord = calc ord 2 in
let svt = if ord >= (pow 2 1) then CoqChecker.True else CoqChecker.False in
let ord = calc ord 1 in
let eth = if ord = 1 then CoqChecker.True else CoqChecker.False in
Ascii (fst,snd,thd,fth,fft,sxt,svt,eth);;
let ascii_to_char (c:CoqChecker.ascii) =
match c with
|Ascii (fst,snd,thd,fth,fft,sxt,svt,eth) ->
let fst_val = if (fst = CoqChecker.True) then pow 2 7 else 0 in
let snd_val = if (snd = CoqChecker.True) then pow 2 6 else 0 in
let thd_val = if (thd = CoqChecker.True) then pow 2 5 else 0 in
let fth_val = if (fth = CoqChecker.True) then pow 2 4 else 0 in
let fft_val = if (fft = CoqChecker.True) then pow 2 3 else 0 in
let sxt_val = if (sxt = CoqChecker.True) then pow 2 2 else 0 in
let svt_val = if (svt = CoqChecker.True) then pow 2 1 else 0 in
let eth_val = if (eth = CoqChecker.True) then 1 else 0 in
chr (fst_val + snd_val + thd_val + fth_val + fft_val + sxt_val + svt_val + eth_val);; *)
(*
let explode s =
let rec exp i l =
if i < 0 then l else exp (i - 1) ((s.[i]) :: l) in
exp (String.length s - 1) [];;
*)
(*
let rec str_to_coq_str (s:char CoqChecker.list) :CoqChecker.string =
match s with
|CoqChecker.Cons (c,s2) -> CoqChecker.String ((char_to_ascii c), (str_to_coq_str s2))
|CoqChecker.Nil -> CoqChecker.EmptyString;;
let rec str_coq_to_str (s:CoqChecker.string) =
match s with
|CoqChecker.String (c, s') -> String.concat "" [(String.make 1 (ascii_to_char c)); str_coq_to_str s']
|CoqChecker.EmptyString -> "";; *)
(*let () = printf "%s@." Sys.argv.(1);; *)
(* let parse = dParse (lex (explode (Sys.argv.(1))) (big_int_of_int 1000)) (big_int_of_int 1000);; *)
(* let ( )= printf "%s\n" parse;; *)
(* let () = printf "Parsing done";; *)
(*t res = implode (CoqChecker.runChecker (explode (Array.get (Sys.argv) 1)));;*)
(* let () = printf "%s\n" res;; *)
(*
let () = printf "%s\n" (str_coq_to_str (str_to_coq_str (explode (Array.get (Sys.argv) 1))));;
let res = str_coq_to_str (CoqChecker.runChecker (str_to_coq_str (explode "1 Ret")));;
let res = CoqChecker.runChecker (str_to_coq_str (explode (Array.get (Sys.argv) 1)));;
let () = printf "%s\n" (str_coq_to_str res);;
let () = printf "%s\n" foo *)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment