Commit dd28dd61 authored by MARCHE Claude's avatar MARCHE Claude

Extraction of VSTTE12_Combinators to Javascript

parent c67a3b49
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=vstte12_combinators__Combinators
OBJ=$(GEN) parse
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: $(GENML)
$(MAIN).opt: $(CMX) $(MAIN).cmx
$(OCAMLOPT) $(INCLUDE) $(BIGINTLIB).cmxa why3extract.cmxa -o $@ $^
$(MAIN).cmx: $(CMX)
$(GENML): ../vstte12_combinators.mlw
$(WHY3) -E ocaml32 ../vstte12_combinators.mlw -o .
%.cmx: %.ml
$(OCAMLOPT) $(INCLUDE) -annot -c $<
clean::
rm -f $(GENML) *.cm[xio] *.o *.annot $(MAIN).opt $(MAIN).byte
rm -f vstte12_combinators__*.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 $<
clean::
rm -f *.cm[io] $(NAME).byte $(NAME).js
<?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>Interpreter for combinator terms</title>
</head>
<body id="test">
<h1>Interpreter for combinator terms</h1>
<p>Enter a combinator term in the text area below</p>
<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 t = Parse.parse_term text in
let u = Vstte12_combinators__Combinators.reduction t in
Format.fprintf Format.str_formatter
"the normal form is %a" Parse.pr u;
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
open Why3extract
open Format
let usage () =
eprintf "Reduction of combinator terms@.";
eprintf "Usage: %s <combinator term>@." Sys.argv.(0);
exit 2
let input =
if Array.length Sys.argv <> 2 then usage ();
Sys.argv.(1)
let input_term =
if input = "go" then
let i = Vstte12_combinators__Combinators.i in
Vstte12_combinators__Combinators.App(i,i)
else
try Parse.parse_term input
with _ ->
begin
eprintf "syntax error@.";
usage ()
end
let () =
let a = Vstte12_combinators__Combinators.reduction input_term in
printf "The normal form of %a is %a@."
Parse.pr input_term Parse.pr a
open Format
open Vstte12_combinators__Combinators
let rec pr fmt t =
match t with
| S -> fprintf fmt "S"
| K -> fprintf fmt "K"
| App(t1,t2) -> fprintf fmt "(%a %a)" pr t1 pr t2
exception SyntaxError
let rec parse_term s i =
match String.get s i with
| 'S' -> S, i+1
| 'K' -> K, i+1
| 'I' -> Vstte12_combinators__Combinators.i, i+1
| '(' ->
let t1,i1 = parse_term s (i+1) in
begin
match String.get s i1 with
| ' ' ->
let t2,i2 = parse_term s (i1+1) in
begin
match String.get s i2 with
| ')' -> App(t1,t2),i2+1
| _ -> raise SyntaxError
end
| _ -> raise SyntaxError
end
| _ -> raise SyntaxError
let parse_term s =
try
let t,i = parse_term s 0 in
if i <> String.length s then raise SyntaxError;
t
with _ -> raise SyntaxError
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