Commit 9e3bca8f authored by Heiko Becker's avatar Heiko Becker

Simplify transScript by removing dead functions and add coq parser + extraction

parent afa4784f
Require Import CertificateChecker.
Require Import Daisy.CertificateChecker Daisy.daisyParser.
Require Import Coq.extraction.ExtrOcamlString Coq.extraction.ExtrOcamlBasic Coq.extraction.ExtrOcamlNatBigInt Coq.extraction.ExtrOcamlZBigInt.
Extraction Language Ocaml.
Extraction "CertificateChecker.ml" CertificateCheckerCmd.
\ No newline at end of file
Extraction "CoqChecker.ml" runChecker.
\ No newline at end of file
#load "CoqChecker.cmo";;
open Printf;;
open CoqChecker;;
open List;;
open String;;
open Char;;
(* 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 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')
|[] -> "";;
(*
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 -> "";; *)
implode (CoqChecker.runChecker dParse(lex (explode "1 Ret + 1657#5 Var 1 PRE ? Var 1 ~100#1 100#1 ABS ? + 1657#5 Var 1 1157#5 2157#5 7771411516990528329#81129638414606681695789005144064 ? 1657#5 1657#5 1657#5 1657#45035996273704960 ? Var 1 ~100#1 100#1 25#2251799813685248 ")) 1000);;
let () = printf "%s\n" Sys.argv.(1);;
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
This diff is collapsed.
......@@ -19,20 +19,9 @@ val _ = Datatype `
| DDIV
| DFRAC`;
val getChar_def = Define `
getChar input =
case input of
| "" => CHR 0
| STRING c input' => c`;
val getConst_def = Define `
getConst (c:char) = ORD c - 48`;
val suffix_def = Define `
suffix s = case s of
| STRING c s' => s'
| "" => ""`;
val lexConst_def = Define`
lexConst (input:tvarN) (akk:num) =
case input of
......
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