diff --git a/libASL/dune b/libASL/dune index c34ac1a2..b37cb1b6 100644 --- a/libASL/dune +++ b/libASL/dune @@ -35,5 +35,4 @@ ) (preprocessor_deps (alias ../asl_files)) (preprocess (pps ppx_blob)) - (libraries libASL_support (re_export libASL_ast) str))) - + (libraries libASL_support (re_export libASL_ast) str)) diff --git a/libASL/tcheck.ml b/libASL/tcheck.ml index 381f733c..2493efa2 100644 --- a/libASL/tcheck.ml +++ b/libASL/tcheck.ml @@ -19,7 +19,7 @@ open Utils open Asl_utils open Printf -let verbose = false +let verbose = true (****************************************************************) @@ -718,7 +718,6 @@ let simplify_type (x: AST.ty): AST.ty = let check_constraints (bs: expr list) (cs: expr list): bool = LibASL_support.Solver.check_constraints bs cs - (****************************************************************) (** {3 Unification support code} *) (****************************************************************) @@ -2465,7 +2464,7 @@ let tc_declarations (isPrelude: bool) (ds: AST.declaration list): AST.declaratio if verbose then Printf.printf " - Typechecking %d phase 1 declarations\n" (List.length pre); let pre' = List.map (tc_declaration env0) pre in let post' = List.map (tc_declaration env0) post in - if verbose then List.iter (fun ds -> List.iter (fun d -> Printf.printf "\nTypechecked %s\n" (Utils.to_string (PP.pp_declaration d))) ds) post'; + (* if verbose then List.iter (fun ds -> List.iter (fun d -> Printf.printf "\nTypechecked %s\n" (Utils.to_string (PP.pp_declaration d))) ds) post'; *) if verbose then Printf.printf " - Typechecking %d phase 2 declarations\n" (List.length post); List.append (List.concat pre') (List.concat post') diff --git a/web/dune b/web/dune index 0c1ced8f..9da554e0 100644 --- a/web/dune +++ b/web/dune @@ -2,10 +2,15 @@ (name js) (modes js) (modules js) - (libraries z3 libASLResources dune-site str zarith pprint zarith_stubs_js) + (libraries boopimpl libASL dune-site str zarith pprint zarith_stubs_js) (js_of_ocaml (flags --debug-info --no-inline :standard \ --source-map-inline)) ) +(library + (name virtual) + (modules v) + (virtual_modules v)) + (alias (name default) (deps js.bc.js index.html)) diff --git a/web/impl/dune b/web/impl/dune new file mode 100644 index 00000000..043e4890 --- /dev/null +++ b/web/impl/dune @@ -0,0 +1,5 @@ + +(library + (name boopimpl) + (implements virtual)) + diff --git a/web/impl/v.ml b/web/impl/v.ml new file mode 100644 index 00000000..518c53ef --- /dev/null +++ b/web/impl/v.ml @@ -0,0 +1,3 @@ + +let read x = x ^ x +let write _ _ = () diff --git a/web/js.ml b/web/js.ml index 8e5deaa9..60cdb36b 100644 --- a/web/js.ml +++ b/web/js.ml @@ -1,4 +1,5 @@ let () = print_endline "hello from js"; - print_endline @@ Int.to_string @@ List.length LibASLResources.Res.Sites.aslfiles - (* print_endline @@ LibASL.Value.(pp_value @@ from_bitsLit "100") *) + (* print_endline @@ Int.to_string @@ List.length LibASLResources.Res.Sites.aslfiles; *) + print_endline @@ LibASL.Value.(pp_value @@ from_bitsLit "100"); + print_endline @@ Virtual.V.read "boop" diff --git a/web/v.mli b/web/v.mli new file mode 100644 index 00000000..6b0df950 --- /dev/null +++ b/web/v.mli @@ -0,0 +1,2 @@ +val read : string -> string +val write : string -> string -> unit