bigInt: javascript

5f008456 · MARCHE Claude · bd050c46 · 5f008456 · 5f008456 · 5f008456
Commit 5f008456 authored Apr 26, 2014 by MARCHE Claude
5 changed files
--- a/.gitignore
+++ b/.gitignore
@@ -222,8 +222,10 @@ pvsbin/
 /examples/euler001/*__*.ml
 /examples/sudoku/*__*.ml
 /examples/defunctionalization/*__*.ml
-examples/vstte12_combinators/jsmain.js
-examples/vstte12_combinators/*__*.ml
+/examples/vstte12_combinators/jsmain.js
+/examples/vstte12_combinators/*__*.ml
+/examples/in_progress/bigInt/jsmain.js
+/examples/in_progress/bigInt/*__*.ml


 # modules

--- a/examples/in_progress/bigInt/Makefile
+++ b/examples/in_progress/bigInt/Makefile
+
+BENCH ?= no
+
+ifeq ($(BENCH),yes)
+  WHY3=../../bin/why3
+  WHY3SHARE=../../share
+else
+  ifeq ($(BINDIR),)
+    WHY3=why3
+  else
+    WHY3=$(BINDIR)/why3
+  endif
+  WHY3SHARE=$(shell $(WHY3) --print-datadir)
+endif
+
+include $(WHY3SHARE)/Makefile.config
+
+ifeq ($(BENCH),yes)
+  INCLUDE += -I ../../lib/why3
+endif
+
+MAIN=main
+GEN=bigInt__N
+OBJ=$(GEN) 
+
+GENML = $(addsuffix .ml, $(GEN))
+ML = $(addsuffix .ml, $(OBJ))
+CMO = $(addsuffix .cmo, $(OBJ))
+CMX = $(addsuffix .cmx, $(OBJ))
+
+OCAMLOPT=ocamlopt -noassert -inline 1000
+
+all: $(MAIN).$(OCAMLBEST)
+
+extract: $(ML)
+
+$(MAIN).byte: $(CMO)  $(MAIN).cmo
+	ocamlc $(INCLUDE) $(BIGINTLIB).cma why3extract.cma -o $@ $^
+
+$(MAIN).opt: $(CMX)  $(MAIN).cmx
+	$(OCAMLOPT) $(INCLUDE) $(BIGINTLIB).cmxa why3extract.cmxa -o $@ $^
+
+$(MAIN).cmx: $(CMX)
+
+$(ML): ../bigInt.mlw
+	$(WHY3) -E ocaml32 $< -o .
+
+%.cmx: %.ml
+	$(OCAMLOPT) $(INCLUDE) -annot -c $<
+
+%.cmo: %.ml
+	ocamlc $(INCLUDE) -annot -c $<
+
+%.cmi: %.mli
+	ocamlc $(INCLUDE) -annot -c $<
+
+clean::
+	rm -f $(GENML) *.cm[xio] *.o *.annot $(MAIN).opt $(MAIN).byte
+	rm -f why3__*.ml* bigInt__*.ml* int__*.ml*
+
+
+# javascript
+
+
+JSMAIN=jsmain
+
+JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
+          -syntax camlp4o
+
+$(JSMAIN).js: $(JSMAIN).byte 
+	js_of_ocaml -pretty -noinline $(JSMAIN).byte
+
+
+$(JSMAIN).byte: $(ML) jsmain.ml
+	$(JSOCAMLC) $(INCLUDE) -o $@ -linkpkg $^
+
+
+%.cmo: %.ml
+	$(JSOCAMLC) $(INCLUDE) -annot -c $<
+
+%.cmi: %.mli
+	$(JSOCAMLC) $(INCLUDE) -annot -c $<
+
--- a/examples/in_progress/bigInt/index.html
+++ b/examples/in_progress/bigInt/index.html
+<?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>
--- a/examples/in_progress/bigInt/jsmain.ml
+++ b/examples/in_progress/bigInt/jsmain.ml
+
+
+(* computation part  *)
+
+open BigInt__N
+
+let compute_result text =
+  try
+    let t = from_small_int (int_of_string text) in
+    let a = add t t in
+    let a = add a t in
+    for i=0 to Array.length a.digits - 1 do
+      Format.fprintf Format.str_formatter "a[%d] = %d@." i a.digits.(i)
+    done;
+    Format.flush_str_formatter ()
+  with _ -> "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
--- a/examples/in_progress/bigInt/main.ml
+++ b/examples/in_progress/bigInt/main.ml
+
+open Why3extract
+open Format
+
+let usage () =
+  eprintf "Usage: %s <decimal number>@." Sys.argv.(0);
+  exit 2
+
+let input =
+  if Array.length Sys.argv <> 2 then usage ();
+  Sys.argv.(1)
+
+open BigInt__N
+
+let input_num =
+  try from_small_int (int_of_string input)
+  with _ -> usage ()
+
+let () =
+  let a = BigInt__N.add input_num input_num in
+  let a = BigInt__N.add a input_num in
+  for i=0 to Array.length a.digits - 1 do
+    printf "a[%d] = %d@." i a.digits.(i)
+  done