From eb5cf15f41046829ae6d18abe5a8bb44746f1049 Mon Sep 17 00:00:00 2001 From: Pierre Chambart Date: Fri, 28 Jul 2023 03:20:05 +0200 Subject: [PATCH] test_kb --- test_kb_wasm/build.sh | 11 +++ test_kb_wasm/clean.sh | 2 + test_kb_wasm/equations.ml | 100 +++++++++++++++++++++ test_kb_wasm/equations.mli | 18 ++++ test_kb_wasm/kb.ml | 173 +++++++++++++++++++++++++++++++++++++ test_kb_wasm/kb.mli | 17 ++++ test_kb_wasm/kbmain.ml | 71 +++++++++++++++ test_kb_wasm/orderings.ml | 84 ++++++++++++++++++ test_kb_wasm/orderings.mli | 17 ++++ test_kb_wasm/terms.ml | 121 ++++++++++++++++++++++++++ test_kb_wasm/terms.mli | 17 ++++ test_kb_wasm/test.html | 37 ++++++++ test_kb_wasm/test.js | 63 ++++++++++++++ test_kb_wasm/test.sh | 3 + 14 files changed, 734 insertions(+) create mode 100755 test_kb_wasm/build.sh create mode 100755 test_kb_wasm/clean.sh create mode 100644 test_kb_wasm/equations.ml create mode 100644 test_kb_wasm/equations.mli create mode 100644 test_kb_wasm/kb.ml create mode 100644 test_kb_wasm/kb.mli create mode 100644 test_kb_wasm/kbmain.ml create mode 100644 test_kb_wasm/orderings.ml create mode 100644 test_kb_wasm/orderings.mli create mode 100644 test_kb_wasm/terms.ml create mode 100644 test_kb_wasm/terms.mli create mode 100644 test_kb_wasm/test.html create mode 100644 test_kb_wasm/test.js create mode 100755 test_kb_wasm/test.sh diff --git a/test_kb_wasm/build.sh b/test_kb_wasm/build.sh new file mode 100755 index 0000000000..1a97a38ded --- /dev/null +++ b/test_kb_wasm/build.sh @@ -0,0 +1,11 @@ + +../ocamlopt -c terms.mli +../ocamlopt -c terms.ml +../ocamlopt -c equations.mli +../ocamlopt -c equations.ml +../ocamlopt -c orderings.mli +../ocamlopt -c orderings.ml +../ocamlopt -c kb.mli +../ocamlopt -c kb.ml +../ocamlopt -c kbmain.ml +../ocamlopt terms.cmx equations.cmx orderings.cmx kb.cmx kbmain.cmx diff --git a/test_kb_wasm/clean.sh b/test_kb_wasm/clean.sh new file mode 100755 index 0000000000..5b43c46fc7 --- /dev/null +++ b/test_kb_wasm/clean.sh @@ -0,0 +1,2 @@ + +rm -f *.cmi *.cmx *.o a.out* diff --git a/test_kb_wasm/equations.ml b/test_kb_wasm/equations.ml new file mode 100644 index 0000000000..c8dbff0505 --- /dev/null +++ b/test_kb_wasm/equations.ml @@ -0,0 +1,100 @@ +(****************** Equation manipulations *************) + +open Terms + +type rule = + { number: int; + numvars: int; + lhs: term; + rhs: term } + +(* standardizes an equation so its variables are 1,2,... *) + +let mk_rule num m n = + let all_vars = union (vars m) (vars n) in + let counter = ref 0 in + let subst = + List.map (fun v -> incr counter; (v, Var !counter)) (List.rev all_vars) in + { number = num; + numvars = !counter; + lhs = substitute subst m; + rhs = substitute subst n } + + +(* checks that rules are numbered in sequence and returns their number *) + +let check_rules rules = + let counter = ref 0 in + List.iter (fun r -> incr counter; + if r.number <> !counter + then failwith "Rule numbers not in sequence") + rules; + !counter + + +let pretty_rule rule = + print_int rule.number; print_string " : "; + pretty_term rule.lhs; print_string " = "; pretty_term rule.rhs; + print_newline() + + +let pretty_rules rules = List.iter pretty_rule rules + +(****************** Rewriting **************************) + +(* Top-level rewriting. Let eq:L=R be an equation, M be a term such that L<=M. + With sigma = matching L M, we define the image of M by eq as sigma(R) *) +let reduce l m r = + substitute (matching l m) r + +(* Test whether m can be reduced by l, i.e. m contains an instance of l. *) + +let can_match l m = + try let _ = matching l m in true + with Failure _ -> false + +let rec reducible l m = + can_match l m || + (match m with + | Term(_,sons) -> List.exists (reducible l) sons + | _ -> false) + +(* Top-level rewriting with multiple rules. *) + +let rec mreduce rules m = + match rules with + [] -> failwith "mreduce" + | rule::rest -> + try + reduce rule.lhs m rule.rhs + with Failure _ -> + mreduce rest m + + +(* One step of rewriting in leftmost-outermost strategy, + with multiple rules. Fails if no redex is found *) + +let rec mrewrite1 rules m = + try + mreduce rules m + with Failure _ -> + match m with + Var n -> failwith "mrewrite1" + | Term(f, sons) -> Term(f, mrewrite1_sons rules sons) + +and mrewrite1_sons rules = function + [] -> failwith "mrewrite1" + | son::rest -> + try + mrewrite1 rules son :: rest + with Failure _ -> + son :: mrewrite1_sons rules rest + + +(* Iterating rewrite1. Returns a normal form. May loop forever *) + +let rec mrewrite_all rules m = + try + mrewrite_all rules (mrewrite1 rules m) + with Failure _ -> + m diff --git a/test_kb_wasm/equations.mli b/test_kb_wasm/equations.mli new file mode 100644 index 0000000000..99055ce22a --- /dev/null +++ b/test_kb_wasm/equations.mli @@ -0,0 +1,18 @@ +open Terms + +type rule = + { number: int; + numvars: int; + lhs: term; + rhs: term } + +val mk_rule: int -> term -> term -> rule +val check_rules: rule list -> int +val pretty_rule: rule -> unit +val pretty_rules: rule list -> unit +val reduce: term -> term -> term -> term +val reducible: term -> term -> bool +val mreduce: rule list -> term -> term +val mrewrite1: rule list -> term -> term +val mrewrite1_sons: rule list -> term list -> term list +val mrewrite_all: rule list -> term -> term diff --git a/test_kb_wasm/kb.ml b/test_kb_wasm/kb.ml new file mode 100644 index 0000000000..1e5fd2c714 --- /dev/null +++ b/test_kb_wasm/kb.ml @@ -0,0 +1,173 @@ +open Terms +open Equations + +(****************** Critical pairs *********************) + +(* All (u,subst) such that N/u (&var) unifies with M, + with principal unifier subst *) + +let rec super m = function + Term(_,sons) as n -> + let rec collate n = function + [] -> [] + | son::rest -> + List.map (fun (u, subst) -> (n::u, subst)) (super m son) + @ collate (n+1) rest in + let insides = collate 1 sons in + begin try + ([], unify m n) :: insides + with Failure _ -> + insides + end + | _ -> [] + + +(* Ex : +let (m,_) = <> +and (n,_) = <> in super m n +==> [[1],[2,Term ("B",[])]; x <- B + [2],[2,Term ("A",[]); 1,Term ("B",[])]] x <- A y <- B +*) + +(* All (u,subst), u&[], such that n/u unifies with m *) + +let super_strict m = function + Term(_,sons) -> + let rec collate n = function + [] -> [] + | son::rest -> + List.map (fun (u, subst) -> (n::u, subst)) (super m son) + @ collate (n+1) rest in + collate 1 sons + | _ -> [] + + +(* Critical pairs of l1=r1 with l2=r2 *) +(* critical_pairs : term_pair -> term_pair -> term_pair list *) +let critical_pairs (l1,r1) (l2,r2) = + let mk_pair (u,subst) = + substitute subst (replace l2 u r1), substitute subst r2 in + List.map mk_pair (super l1 l2) + +(* Strict critical pairs of l1=r1 with l2=r2 *) +(* strict_critical_pairs : term_pair -> term_pair -> term_pair list *) +let strict_critical_pairs (l1,r1) (l2,r2) = + let mk_pair (u,subst) = + substitute subst (replace l2 u r1), substitute subst r2 in + List.map mk_pair (super_strict l1 l2) + + +(* All critical pairs of eq1 with eq2 *) +let mutual_critical_pairs eq1 eq2 = + (strict_critical_pairs eq1 eq2) @ (critical_pairs eq2 eq1) + +(* Renaming of variables *) + +let rename n (t1,t2) = + let rec ren_rec = function + Var k -> Var(k+n) + | Term(op,sons) -> Term(op, List.map ren_rec sons) in + (ren_rec t1, ren_rec t2) + + +(************************ Completion ******************************) + +let deletion_message rule = + print_string "Rule ";print_int rule.number; print_string " deleted"; + print_newline() + + +(* Generate failure message *) +let non_orientable (m,n) = + pretty_term m; print_string " = "; pretty_term n; print_newline() + + +let rec partition p = function + [] -> ([], []) + | x::l -> let (l1, l2) = partition p l in + if p x then (x::l1, l2) else (l1, x::l2) + + +let rec get_rule n = function + [] -> raise Not_found + | r::l -> if n = r.number then r else get_rule n l + + +(* Improved Knuth-Bendix completion procedure *) + +let kb_completion greater = + let rec kbrec j rules = + let rec process failures (k,l) eqs = +(**** + print_string "***kb_completion "; print_int j; print_newline(); + pretty_rules rules; + List.iter non_orientable failures; + print_int k; print_string " "; print_int l; print_newline(); + List.iter non_orientable eqs; +***) + match eqs with + [] -> + if k rules (* successful completion *) + | _ -> print_string "Non-orientable equations :"; print_newline(); + List.iter non_orientable failures; + failwith "kb_completion" + end + | (m,n)::eqs -> + let m' = mrewrite_all rules m + and n' = mrewrite_all rules n + and enter_rule(left,right) = + let new_rule = mk_rule (j+1) left right in + pretty_rule new_rule; + let left_reducible rule = reducible left rule.lhs in + let (redl,irredl) = partition left_reducible rules in + List.iter deletion_message redl; + let right_reduce rule = + mk_rule rule.number rule.lhs + (mrewrite_all (new_rule::rules) rule.rhs) in + let irreds = List.map right_reduce irredl in + let eqs' = List.map (fun rule -> (rule.lhs, rule.rhs)) redl in + kbrec (j+1) (new_rule::irreds) [] (k,l) (eqs @ eqs' @ failures) in +(*** + print_string "--- Considering "; non_orientable (m', n'); +***) + if m' = n' then process failures (k,l) eqs else + if greater(m',n') then enter_rule(m',n') else + if greater(n',m') then enter_rule(n',m') else + process ((m',n')::failures) (k,l) eqs + + and next_criticals failures (k,l) = +(**** + print_string "***next_criticals "; + print_int k; print_string " "; print_int l ; print_newline(); +****) + try + let rl = get_rule l rules in + let el = (rl.lhs, rl.rhs) in + if k=l then + process failures (k,l) + (strict_critical_pairs el (rename rl.numvars el)) + else + try + let rk = get_rule k rules in + let ek = (rk.lhs, rk.rhs) in + process failures (k,l) + (mutual_critical_pairs el (rename rl.numvars ek)) + with Not_found -> next_criticals failures (k+1,l) + with Not_found -> next_criticals failures (1,l+1) + in process + in kbrec + + +(* complete_rules is assumed locally confluent, and checked Noetherian with + ordering greater, rules is any list of rules *) + +let kb_complete greater complete_rules rules = + let n = check_rules complete_rules + and eqs = List.map (fun rule -> (rule.lhs, rule.rhs)) rules in + let completed_rules = + kb_completion greater n complete_rules [] (n,n) eqs in + print_string "Canonical set found :"; print_newline(); + pretty_rules (List.rev completed_rules) diff --git a/test_kb_wasm/kb.mli b/test_kb_wasm/kb.mli new file mode 100644 index 0000000000..3276871656 --- /dev/null +++ b/test_kb_wasm/kb.mli @@ -0,0 +1,17 @@ +open Terms +open Equations + +val super: term -> term -> (int list * (int * term) list) list +val super_strict: term -> term -> (int list * (int * term) list) list +val critical_pairs: term * term -> term * term -> (term * term) list +val strict_critical_pairs: term * term -> term * term -> (term * term) list +val mutual_critical_pairs: term * term -> term * term -> (term * term) list +val rename: int -> term * term -> term * term +val deletion_message: rule -> unit +val non_orientable: term * term -> unit +val partition: ('a -> bool) -> 'a list -> 'a list * 'a list +val get_rule: int -> rule list -> rule +val kb_completion: + (term * term -> bool) -> int -> rule list -> (term * term) list + -> int * int -> (term * term) list -> rule list +val kb_complete: (term * term -> bool) -> rule list -> rule list -> unit diff --git a/test_kb_wasm/kbmain.ml b/test_kb_wasm/kbmain.ml new file mode 100644 index 0000000000..6e94ecd0a7 --- /dev/null +++ b/test_kb_wasm/kbmain.ml @@ -0,0 +1,71 @@ +(* TEST + modules = "terms.ml equations.ml orderings.ml kb.ml" +*) + +open Terms +open Equations +open Orderings +open Kb + +(**** +let group_rules = [ + { number = 1; numvars = 1; + lhs = Term("*", [Term("U",[]); Var 1]); rhs = Var 1 }; + { number = 2; numvars = 1; + lhs = Term("*", [Term("I",[Var 1]); Var 1]); rhs = Term("U",[]) }; + { number = 3; numvars = 3; + lhs = Term("*", [Term("*", [Var 1; Var 2]); Var 3]); + rhs = Term("*", [Var 1; Term("*", [Var 2; Var 3])]) } +] +****) + +let geom_rules = [ + { number = 1; numvars = 1; + lhs = Term ("*",[(Term ("U",[])); (Var 1)]); + rhs = Var 1 }; + { number = 2; numvars = 1; + lhs = Term ("*",[(Term ("I",[(Var 1)])); (Var 1)]); + rhs = Term ("U",[]) }; + { number = 3; numvars = 3; + lhs = Term ("*",[(Term ("*",[(Var 1); (Var 2)])); (Var 3)]); + rhs = Term ("*",[(Var 1); (Term ("*",[(Var 2); (Var 3)]))]) }; + { number = 4; numvars = 0; + lhs = Term ("*",[(Term ("A",[])); (Term ("B",[]))]); + rhs = Term ("*",[(Term ("B",[])); (Term ("A",[]))]) }; + { number = 5; numvars = 0; + lhs = Term ("*",[(Term ("C",[])); (Term ("C",[]))]); + rhs = Term ("U",[]) }; + { number = 6; numvars = 0; + lhs = Term("*", + [(Term ("C",[])); + (Term ("*",[(Term ("A",[])); (Term ("I",[(Term ("C",[]))]))]))]); + rhs = Term ("I",[(Term ("A",[]))]) }; + { number = 7; numvars = 0; + lhs = Term("*", + [(Term ("C",[])); + (Term ("*",[(Term ("B",[])); (Term ("I",[(Term ("C",[]))]))]))]); + rhs = Term ("B",[]) } +] + +let group_rank = function + "U" -> 0 + | "*" -> 1 + | "I" -> 2 + | "B" -> 3 + | "C" -> 4 + | "A" -> 5 + | _ -> assert false + +let group_precedence op1 op2 = + let r1 = group_rank op1 + and r2 = group_rank op2 in + if r1 = r2 then Equal else + if r1 > r2 then Greater else NotGE + +let group_order = rpo group_precedence lex_ext + +let greater pair = + match group_order pair with Greater -> true | _ -> false + +let _ = + kb_complete greater [] geom_rules diff --git a/test_kb_wasm/orderings.ml b/test_kb_wasm/orderings.ml new file mode 100644 index 0000000000..b6ef8abf59 --- /dev/null +++ b/test_kb_wasm/orderings.ml @@ -0,0 +1,84 @@ +(*********************** Recursive Path Ordering ****************************) + +open Terms + +type ordering = + Greater + | Equal + | NotGE + +let ge_ord order pair = match order pair with NotGE -> false | _ -> true +and gt_ord order pair = match order pair with Greater -> true | _ -> false +and eq_ord order pair = match order pair with Equal -> true | _ -> false + + +let rec rem_eq equiv x = function + [] -> failwith "rem_eq" + | y::l -> if equiv (x,y) then l else y :: rem_eq equiv x l + + +let diff_eq equiv (x,y) = + let rec diffrec = function + ([],_) as p -> p + | (h::t, y) -> try + diffrec (t, rem_eq equiv h y) + with Failure _ -> + let (x',y') = diffrec (t,y) in (h::x',y') in + if List.length x > List.length y then diffrec(y,x) else diffrec(x,y) + + +(* Multiset extension of order *) + +let mult_ext order = function + Term(_,sons1), Term(_,sons2) -> + begin match diff_eq (eq_ord order) (sons1,sons2) with + ([],[]) -> Equal + | (l1,l2) -> + if List.for_all + (fun n -> List.exists (fun m -> gt_ord order (m,n)) l1) l2 + then Greater else NotGE + end + | _ -> failwith "mult_ext" + + +(* Lexicographic extension of order *) + +let lex_ext order = function + (Term(_,sons1) as m), (Term(_,sons2) as n) -> + let rec lexrec = function + ([] , []) -> Equal + | ([] , _ ) -> NotGE + | ( _ , []) -> Greater + | (x1::l1, x2::l2) -> + match order (x1,x2) with + Greater -> if List.for_all (fun n' -> gt_ord order (m,n')) l2 + then Greater else NotGE + | Equal -> lexrec (l1,l2) + | NotGE -> if List.exists (fun m' -> ge_ord order (m',n)) l1 + then Greater else NotGE in + lexrec (sons1, sons2) + | _ -> failwith "lex_ext" + + +(* Recursive path ordering *) + +let rpo op_order ext = + let rec rporec (m,n) = + if m = n then Equal else + match m with + Var vm -> NotGE + | Term(op1,sons1) -> + match n with + Var vn -> + if occurs vn m then Greater else NotGE + | Term(op2,sons2) -> + match (op_order op1 op2) with + Greater -> + if List.for_all (fun n' -> gt_ord rporec (m,n')) sons2 + then Greater else NotGE + | Equal -> + ext rporec (m,n) + | NotGE -> + if List.exists (fun m' -> ge_ord rporec (m',n)) sons1 + then Greater else NotGE + in rporec diff --git a/test_kb_wasm/orderings.mli b/test_kb_wasm/orderings.mli new file mode 100644 index 0000000000..d0493c5228 --- /dev/null +++ b/test_kb_wasm/orderings.mli @@ -0,0 +1,17 @@ +open Terms + +type ordering = + Greater + | Equal + | NotGE + +val ge_ord: ('a -> ordering) -> 'a -> bool +val gt_ord: ('a -> ordering) -> 'a -> bool +val eq_ord: ('a -> ordering) -> 'a -> bool +val rem_eq: ('a * 'b -> bool) -> 'a -> 'b list -> 'b list +val diff_eq: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list * 'a list +val mult_ext: (term * term -> ordering) -> term * term -> ordering +val lex_ext: (term * term -> ordering) -> term * term -> ordering +val rpo: (string -> string -> ordering) -> + ((term * term -> ordering) -> term * term -> ordering) -> + term * term -> ordering diff --git a/test_kb_wasm/terms.ml b/test_kb_wasm/terms.ml new file mode 100644 index 0000000000..f66c86fab2 --- /dev/null +++ b/test_kb_wasm/terms.ml @@ -0,0 +1,121 @@ +(****************** Term manipulations *****************) + +type term = + Var of int + | Term of string * term list + +let rec union l1 l2 = + match l1 with + [] -> l2 + | a::r -> if List.mem a l2 then union r l2 else a :: union r l2 + + +let rec vars = function + Var n -> [n] + | Term(_,l) -> vars_of_list l +and vars_of_list = function + [] -> [] + | t::r -> union (vars t) (vars_of_list r) + + +let rec substitute subst = function + Term(oper,sons) -> Term(oper, List.map (substitute subst) sons) + | Var(n) as t -> try List.assoc n subst with Not_found -> t + + +(* Term replacement: replace M u N is M[u<-N]. *) + +let rec replace m u n = + match (u, m) with + [], _ -> n + | i::u, Term(oper, sons) -> Term(oper, replace_nth i sons u n) + | _ -> failwith "replace" + +and replace_nth i sons u n = + match sons with + s::r -> if i = 1 + then replace s u n :: r + else s :: replace_nth (i-1) r u n + | [] -> failwith "replace_nth" + + +(* Term matching. *) + +let matching term1 term2 = + let rec match_rec subst t1 t2 = + match (t1, t2) with + Var v, _ -> + if List.mem_assoc v subst then + if t2 = List.assoc v subst then subst else failwith "matching" + else + (v, t2) :: subst + | Term(op1,sons1), Term(op2,sons2) -> + if op1 = op2 + then List.fold_left2 match_rec subst sons1 sons2 + else failwith "matching" + | _ -> failwith "matching" in + match_rec [] term1 term2 + + +(* A naive unification algorithm. *) + +let compsubst subst1 subst2 = + (List.map (fun (v,t) -> (v, substitute subst1 t)) subst2) @ subst1 + + +let rec occurs n = function + Var m -> m = n + | Term(_,sons) -> List.exists (occurs n) sons + + +let rec unify term1 term2 = + match (term1, term2) with + Var n1, _ -> + if term1 = term2 then [] + else if occurs n1 term2 then failwith "unify" + else [n1, term2] + | term1, Var n2 -> + if occurs n2 term1 then failwith "unify" + else [n2, term1] + | Term(op1,sons1), Term(op2,sons2) -> + if op1 = op2 then + List.fold_left2 (fun s t1 t2 -> compsubst (unify (substitute s t1) + (substitute s t2)) s) + [] sons1 sons2 + else failwith "unify" + + +(* We need to print terms with variables independently from input terms + obtained by parsing. We give arbitrary names v1,v2,... to their variables. +*) + +let infixes = ["+";"*"] + +let rec pretty_term = function + Var n -> + print_string "v"; print_int n + | Term (oper,sons) -> + if List.mem oper infixes then begin + match sons with + [s1;s2] -> + pretty_close s1; print_string oper; pretty_close s2 + | _ -> + failwith "pretty_term : infix arity <> 2" + end else begin + print_string oper; + match sons with + [] -> () + | t::lt -> print_string "("; + pretty_term t; + List.iter (fun t -> print_string ","; pretty_term t) lt; + print_string ")" + end + +and pretty_close = function + Term(oper, _) as m -> + if List.mem oper infixes then begin + print_string "("; pretty_term m; print_string ")" + end else + pretty_term m + | m -> + pretty_term m diff --git a/test_kb_wasm/terms.mli b/test_kb_wasm/terms.mli new file mode 100644 index 0000000000..81ec58e726 --- /dev/null +++ b/test_kb_wasm/terms.mli @@ -0,0 +1,17 @@ +type term = + Var of int + | Term of string * term list + +val union: 'a list -> 'a list -> 'a list +val vars: term -> int list +val vars_of_list: term list -> int list +val substitute: (int * term) list -> term -> term +val replace: term -> int list -> term -> term +val replace_nth: int -> term list -> int list -> term -> term list +val matching: term -> term -> (int * term) list +val compsubst: (int * term) list -> (int * term) list -> (int * term) list +val occurs: int -> term -> bool +val unify: term -> term -> (int * term) list +val infixes: string list +val pretty_term: term -> unit +val pretty_close: term -> unit diff --git a/test_kb_wasm/test.html b/test_kb_wasm/test.html new file mode 100644 index 0000000000..8a8dca29f2 --- /dev/null +++ b/test_kb_wasm/test.html @@ -0,0 +1,37 @@ + + + + + Test + + + + + + diff --git a/test_kb_wasm/test.js b/test_kb_wasm/test.js new file mode 100644 index 0000000000..6b92f796f1 --- /dev/null +++ b/test_kb_wasm/test.js @@ -0,0 +1,63 @@ + +const memory = new WebAssembly.Memory({ + initial: 1, + maximum: 1, +}); + +function print_string(str) { + console.log('print_string'); + var res = ""; + for (i = 0; i < get_length(str); i++) { + res = res + String.fromCharCode(get_char(str, i)); + } + console.log(res); + }; +var str_buff = ""; +function print_string_mem(off, len) { + // console.log('print_string_mem'); + const buff = new Uint8Array(memory.buffer); + // console.log(buff); + var i = 0; + for (i = 0; i < len; i++) { + var char = String.fromCharCode(buff[i+off]); + str_buff = str_buff + char; + } + }; + +function print_i32(arg) { + str_buff = str_buff + arg.toString(); + }; +function print_f64(arg) { + console.log(arg); + }; + +function print_endline() { + console.log(str_buff); + str_buff = ""; +} + +function putchar(i_char) { + var char = String.fromCharCode(i_char); + str_buff = str_buff + char; +}; + +function flush() { + console.log(str_buff); + str_buff = ""; +} + +const bindings = { + "print_i32": print_i32, + "print_f64": print_f64, + "print_string": print_string, + "print_string_mem": print_string_mem, + "print_endline": print_endline, + "putchar": putchar, + "flush": flush, + "memory": memory +} + +const src = "./a.out.wasm" +const code = fetch(src) +const imports = {"js_runtime":bindings} +const wasmModule = await WebAssembly.instantiateStreaming(code,imports) diff --git a/test_kb_wasm/test.sh b/test_kb_wasm/test.sh new file mode 100755 index 0000000000..28ffc3f828 --- /dev/null +++ b/test_kb_wasm/test.sh @@ -0,0 +1,3 @@ + +../ocamlopt ./stuff.ml +python3 -m http.server 8000 --directory .