Commit e3332a88 authored by MARCHE Claude's avatar MARCHE Claude

mp: extract to javascript

parent 77c67856
......@@ -178,7 +178,7 @@ module N
= let limb_zero = Limb.of_int 0 in
let zero = Int31.of_int 0 in
let one = Int31.of_int 1 in
let minus_one = Int31.of_int (-1) in
let minus_one = Int31.(-_) one in
let i = ref x2 in
let x3 = Int31.(+) x1 (Int31.(-) y2 y1) in
try
......
......@@ -20,9 +20,11 @@ ifeq ($(BENCH),yes)
endif
MAIN=main
GEN=map__Map mach__int__UInt32 mp__N
GEN=map__Map mp__N
OBJ=$(GEN) parse
parse.cmo: mp__N.cmi
GENML = $(addsuffix .ml, $(GEN))
ML = $(addsuffix .ml, $(OBJ))
CMO = $(addsuffix .cmo, $(OBJ))
......@@ -32,7 +34,7 @@ OCAMLOPT=ocamlopt -noassert -inline 1000
all: $(MAIN).$(OCAMLBEST)
extract: $(ML)
extract: $(GENML)
$(MAIN).byte: $(CMO) $(MAIN).cmo
ocamlc $(INCLUDE) $(BIGINTLIB).cma why3extract.cma -g -o $@ $^
......@@ -42,7 +44,7 @@ $(MAIN).opt: $(CMX) $(MAIN).cmx
$(MAIN).cmx: $(CMX)
$(ML): ../mp.mlw
$(GENML): ../mp.mlw
$(WHY3) -E ocaml32 $< -o .
%.cmx: %.ml
......@@ -71,7 +73,7 @@ $(JSMAIN).js: $(JSMAIN).byte
js_of_ocaml -pretty -noinline $(JSMAIN).byte
$(JSMAIN).byte: $(ML) jsmain.ml
$(JSMAIN).byte: $(CMO) jsmain.ml
$(JSOCAMLC) $(INCLUDE) -o $@ -linkpkg $^
......
<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN"
"http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title>Javascript test for bigInt</title>
</head>
<body id="test">
<h1>Javascript test for bigInt</h1>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<script type="text/javascript" src="jsmain.js"></script>
</body>
</html>
(* computation part *)
let compute_result text =
try
let a,i = Parse.parse_dec text 0 in
let i = Parse.parse_sep_star text i in
let b,i = Parse.parse_dec text i in
let c = Mp__N.add a b in
Parse.pr Format.str_formatter c;
Format.flush_str_formatter ()
with Parse.SyntaxError -> "syntax error"
(* HTML rendering *)
module Html = Dom_html
let node x = (x : #Dom.node Js.t :> Dom.node Js.t)
let (<|) e l = List.iter (fun c -> Dom.appendChild e c) l; node e
let html_of_string (d : Html.document Js.t) (s:string) =
d##createElement (Js.string "p") <|
[node (d##createTextNode (Js.string s))]
let replace_child p n =
Js.Opt.iter (p##firstChild) (fun c -> Dom.removeChild p c);
Dom.appendChild p n
let onload (_event : #Html.event Js.t) : bool Js.t =
let d = Html.document in
let body =
Js.Opt.get (d##getElementById(Js.string "test"))
(fun () -> assert false) in
let textbox = Html.createTextarea d in
textbox##rows <- 20; textbox##cols <- 100;
let preview = Html.createDiv d in
preview##style##border <- Js.string "1px black";
preview##style##padding <- Js.string "5px";
Dom.appendChild body textbox;
Dom.appendChild body (Html.createBr d);
Dom.appendChild body preview;
let rec dyn_preview old_text n =
let text = Js.to_string (textbox##value) in
let n =
if text <> old_text then
begin
begin try
let rendered =
html_of_string d (compute_result text)
in
replace_child preview rendered
with _ -> ()
end;
20
end
else
max 0 (n - 1)
in
Lwt.bind
(Lwt_js.sleep (if n = 0 then 0.5 else 0.1))
(fun () -> dyn_preview text n)
in
let (_ : 'a Lwt.t) = dyn_preview "" 0 in Js._false
let (_ : unit) = Html.window##onload <- Html.handler onload
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