diff --git a/examples/in_progress/mp.mlw b/examples/in_progress/mp.mlw index 8e32606d680911bec6aa0d857f4bda69977d0ff4..005ab59ce0a814d75c3a85026f8e735cea5956fb 100644 --- a/examples/in_progress/mp.mlw +++ b/examples/in_progress/mp.mlw @@ -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 diff --git a/examples/in_progress/mp/Makefile b/examples/in_progress/mp/Makefile index cf385b12a0c7d1705a6ccd829934449502c325e9..09db9c807d8b62d9f669ee98f32ad49d1db8cd01 100644 --- a/examples/in_progress/mp/Makefile +++ b/examples/in_progress/mp/Makefile @@ -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 $^ diff --git a/examples/in_progress/mp/index.html b/examples/in_progress/mp/index.html new file mode 100644 index 0000000000000000000000000000000000000000..ce70dae8203d62cc6da11c97456fc94f0045d7be --- /dev/null +++ b/examples/in_progress/mp/index.html @@ -0,0 +1,13 @@ + + + + + Javascript test for bigInt + + +

Javascript test for bigInt

+ + + + diff --git a/examples/in_progress/mp/jsmain.ml b/examples/in_progress/mp/jsmain.ml new file mode 100644 index 0000000000000000000000000000000000000000..57e4a0ef8085d97f15e9f77e2268a0e294eead34 --- /dev/null +++ b/examples/in_progress/mp/jsmain.ml @@ -0,0 +1,68 @@ + + +(* 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