From f2d9337123e473a315d72c0875a6154b011b4656 Mon Sep 17 00:00:00 2001 From: VooDooS Date: Tue, 24 Sep 2019 17:20:04 +0200 Subject: [PATCH] Some cleanup --- docs/js/elpi-worker.js | 7 +++-- docs/js/main.js | 18 +---------- lib/data.mli | 2 ++ lib/elpi_string.ml | 42 -------------------------- lib/elpi_string.mli | 1 - lib/js/type_parser.pegjs | 1 - lib/main.ml | 14 ++++++--- lib/mlts_api/mlts_API.mli | 1 + lib/mlts_api/prologAst.ml | 11 ++++--- lib/mlts_api/prologPrinter.ml | 3 +- lib/mlts_api/translator.ml | 57 ++++++++++++++++++++--------------- 11 files changed, 59 insertions(+), 98 deletions(-) delete mode 100644 lib/elpi_string.ml delete mode 100644 lib/elpi_string.mli diff --git a/docs/js/elpi-worker.js b/docs/js/elpi-worker.js index 9c37cd9..c2c69e8 100644 --- a/docs/js/elpi-worker.js +++ b/docs/js/elpi-worker.js @@ -1,7 +1,10 @@ - +/** + * Code for the Elpi Worker + * - works in separate thread + * - load mlts.js to work with elpi + */ console.log('[Elpi-worker] ' + "Starting Elpi..."); -//importScripts('mlts.runtime.js'); importScripts('mlts.js'); console.log('[Elpi-worker] ' + "Elpi started"); diff --git a/docs/js/main.js b/docs/js/main.js index eb4b3b2..e0a3765 100644 --- a/docs/js/main.js +++ b/docs/js/main.js @@ -39,9 +39,6 @@ $(function () { $(document).ready(function(){ $.get("readme.html", function(data) { $("#readme").html(data); - /*$('#readme pre').each(function(i, block) { - hljs.highlightBlock(block); - });*/ }); load(window.location.hash.substring(1)); @@ -104,14 +101,6 @@ function useFile(corr, instr, name) { else { res = "(* Failed to load file " + name + "*)"; } - /*$.ajax({ - url: name,//"examples/" + name + ".mlts", - success: function (result) { - if (result.isOk == false) res = (result.message); - else res = ("(* unknown file " + name + " *)"); - }, - async: false - });*/ console.log(res); return res } @@ -153,11 +142,7 @@ function onMessageCB(event) { unlock(); } else if(event.data.type == 'log') { - $('#log') - //.append("[") - //.append((new Date()).toLocaleTimeString()) - //.append("]") - .append((event.data.text).replace(/arobase/g, '@')); + $('#log').append((event.data.text).replace(/arobase/g, '@')); } else if (event.data.type == 'error') { unlock(); @@ -207,7 +192,6 @@ function run() { lock('Running'); var mltsCode = editor.getValue(); mltsCode = mltsCode.replace(/(use "(.*)";;)/g, useFile); - //console.log(mltsCode); elpi.postMessage(mltsCode); } diff --git a/lib/data.mli b/lib/data.mli index 3437823..6179e4f 100644 --- a/lib/data.mli +++ b/lib/data.mli @@ -1,3 +1,5 @@ +(* Packed data for the js_of_ocaml pseudo-file system *) + type file = { name: string; text: string } val files : file list diff --git a/lib/elpi_string.ml b/lib/elpi_string.ml deleted file mode 100644 index ab42824..0000000 --- a/lib/elpi_string.ml +++ /dev/null @@ -1,42 +0,0 @@ -exception Query_failed - -(* Tools for priting Elpi results - * These results have the type Elpi_API.Data.solution - * - * type solution = { - * assignments : term StrMap.t; - * constraints : syntactic_constraints; - * custom_constraints : custom_constraints; - *} - * - *) -let string_of_assignments ass = - Elpi_API.Data.StrMap.fold - (fun name term acc -> - Elpi_API.Pp.term (Format.str_formatter) term; - let str = Format.flush_str_formatter () in - (* LP strings are surrounded by quotes, we remove them *) - acc ^ name ^ " := " ^ str) - ass "" - -let string_of_constraints cons = - Elpi_API.Pp.constraints (Format.str_formatter) cons; - Format.flush_str_formatter () - -let string_of_cconstraints cons = - Elpi_API.Pp.custom_constraints (Format.str_formatter) cons; - Format.flush_str_formatter () - -let string_of_sol (s : Elpi_API.Data.solution) = - "Assignments : " ^ (string_of_assignments (s.assignments)) - ^ "\nConstraints : " ^ (string_of_constraints (s.constraints)) - ^ "\nCustom constraints : " - ^ (string_of_cconstraints (s.custom_constraints)) - ^ "\n" - -let loop_printer f (out : Elpi_API.Execute.outcome) = - print_string ("\nIter "^ (string_of_float f) ^ ":\n"); - match out with - | Success(data) -> print_string (string_of_sol data) - | NoMoreSteps -> print_string "Finished (no more).\n" - | Failure -> print_string "Finished (fail).\n" diff --git a/lib/elpi_string.mli b/lib/elpi_string.mli deleted file mode 100644 index d47c041..0000000 --- a/lib/elpi_string.mli +++ /dev/null @@ -1 +0,0 @@ -val loop_printer : float -> Elpi_API.Execute.outcome -> unit diff --git a/lib/js/type_parser.pegjs b/lib/js/type_parser.pegjs index a4f886f..4e7852e 100644 --- a/lib/js/type_parser.pegjs +++ b/lib/js/type_parser.pegjs @@ -32,6 +32,5 @@ Ident TIdent = t:("t_" [_0-9a-z]i+) { return (strip(text())) } - _ "whitespace" = [ \t\n\r]* {return ""} diff --git a/lib/main.ml b/lib/main.ml index 157604f..3b86654 100644 --- a/lib/main.ml +++ b/lib/main.ml @@ -2,10 +2,13 @@ open Js_of_ocaml exception Query_failed exception No_kernel +(* TryMLTS version *) let version = "0.4" +(* Reference to the Elpi kernel *) let kernel = ref None +(* Tools for printing to the browser console *) let escape s = Js.to_string (Js.escape (Js.string s)) @@ -21,6 +24,7 @@ let consoleError ?pref:(p = "") (str : string) = let wrapConsole ?pref:(p = "") ?loc str = console str let wrapConsoleErr ?pref:(p = "") ?loc str = consoleError str +(* Translate and compile MLTS code *) let compile header code = try (* First mlts => lprolog *) @@ -29,15 +33,14 @@ let compile header code = (* updating the pseudo files *) Sys_js.update_file ~name:"core/progs.elpi" ~content:lpcode; - (*Sys_js.update_file "core/datatypes.sig" typsig; - Sys_js.update_file "core/datatypes.mod" typmod;*) (* recompiling lprolog code *) let parsed = Elpi.API.Parse.program - [(*"core/datatypes.mod";*) + [ "core/progs.elpi"; - "core/run.elpi";] in + "core/run.elpi"; + ] in kernel := Some(Elpi.API.Compile.program Elpi.API.Compile.default_flags header [parsed]); (* We return the lprolog code for reference *) @@ -54,6 +57,7 @@ let q_prog = "Prog" let q_value = "Value" let q_type = "Type" +(* Handler for Elpi output *) let handle_out res iter _f (out : unit Elpi.API.Execute.outcome) = match out with | Success(data) -> @@ -112,7 +116,7 @@ let _ = ignore (Js.Unsafe.eval_string ("sendVersion('" ^ (version) ^"')")); - (* Loading data folder in the pseudo-filesystem *) + (* Load data folder in the pseudo-filesystem *) Data.load (); (* Initialize Elpi *) diff --git a/lib/mlts_api/mlts_API.mli b/lib/mlts_api/mlts_API.mli index d3d42e7..a53aaf8 100644 --- a/lib/mlts_api/mlts_API.mli +++ b/lib/mlts_api/mlts_API.mli @@ -4,5 +4,6 @@ val parse_and_translate : string -> val pp_prog : Format.formatter -> PrologAst.clause list -> unit +(* Parses, translates and print the resulting AST *) val prologify : string -> ( string * (string * int) list) diff --git a/lib/mlts_api/prologAst.ml b/lib/mlts_api/prologAst.ml index 663ced0..85386c0 100644 --- a/lib/mlts_api/prologAst.ml +++ b/lib/mlts_api/prologAst.ml @@ -1,3 +1,6 @@ +(* This module contians function taht builds +correct prolog asts *) + type global_name = string type local_name = string * int type name = @@ -74,7 +77,7 @@ let make_bool ?(is_pat = false) b = let make_string ?(is_pat = false) s = make_lit is_pat (make_app "s" [Lit (String s)]) -let make_unit ?(is_pat = false) i = +let make_unit ?(is_pat = false) _i = make_lit is_pat (make_app "unit" []) let make_global n = @@ -85,11 +88,11 @@ let make_local n i = let make_localp p = make_local (fst p) (snd p) -let make_select name (mutual_name, mutual_n) index = +let make_select _name (mutual_name, mutual_n) index = make_app "select" [Lit (Int index); App(Local(mutual_name, mutual_n), [])] -let make_select_g name mutual_name index = +let make_select_g _name mutual_name index = make_app "select" [Lit (Int index); App(Global(mutual_name), [])] @@ -186,6 +189,6 @@ let make_constr ?(pattern=false) name tms = (if pattern then "pvariant" else "variant") [make_global name; List tms] -let make_row name lambdas projs = +let make_row name lambdas _projs = make_app "rowfix" [Abs(name, make_app "row" [List(lambdas)])] \ No newline at end of file diff --git a/lib/mlts_api/prologPrinter.ml b/lib/mlts_api/prologPrinter.ml index 9cfe1ab..0b6c38e 100644 --- a/lib/mlts_api/prologPrinter.ml +++ b/lib/mlts_api/prologPrinter.ml @@ -1,5 +1,6 @@ -open Format +(* Pretty printer for the prolog AST *) +open Format open PrologAst let pp_global_name ppf s = fprintf ppf "%s" s diff --git a/lib/mlts_api/translator.ml b/lib/mlts_api/translator.ml index b8e6bc3..a06490f 100644 --- a/lib/mlts_api/translator.ml +++ b/lib/mlts_api/translator.ml @@ -1,12 +1,13 @@ open MltsAst -module P = PrologAst +module P = PrologAst +type def = { name: string; pos: Lexing.position } + +(* Exceptions *) exception TranslatorError of string * (Lexing.position option) exception StaticCheckError of string * (Lexing.position option) -type def = { name: string; pos: Lexing.position } - let strip name = String.sub name 2 (String.length name - 2) let make_exception message def pos = @@ -33,12 +34,12 @@ type context = { mutable global_vars : string list; mutable global_constrs : string list; mutable global_mutuals : (string * (string * int)) list; - mutable actual_def: def list; + mutable actual_def: def list; (* Used to track error position *) mutable wanabeeRigidNoms: P.local_name list; } let incr_expr c = c.nb_expr <- c.nb_expr + 1 -(* (local) Environments *) +(* (local) Environments and tools *) type env = { local_vars: P.local_name list; free_vars: P.global_name list; @@ -63,7 +64,7 @@ let add_nom_to_env v env = let add_mutual_to_env v row n env = let res = (v, row, n) in match List.find_opt - (fun ((n, _, _), i) -> n = v) + (fun ((n, _, _), _i) -> n = v) env.local_rows with | None -> let res = (res, 0) in @@ -88,9 +89,15 @@ let string_of_env env = ) let print_env env = print_endline (string_of_env env) -(* env are used to pass is used to carry different kind of information. Some, such as local variables should be erased when leaving scope, some like the list of "free variables" needed by an expr should not. +(* env are used used to carry different kind of information. Some, such as local +variables should be erased when leaving scope, some like the list of "free +variables" needed by an expr should not. + +This may be bad design (todo split envs in two ?) but for now the revert_locals +function can be use to strip newly declared locals using an "Original" +environement without the new locals and the "deeper" env with maybe new locals +and informations *) - This may be bad design (todo ?) but for now the revert_locals function can be use to strip newly declared locals using an "Original" environement without the new locals and the "deeper" env with maybe new locals and infos *) let revert_locals envBefore envAfter = { envAfter with local_vars = envBefore.local_vars } @@ -113,13 +120,15 @@ type tdef = { kind: k; name: string; body: P.term; env: env } (* PROGRAM TRANSLATION *) let mlts_to_prolog p = - let ctx = { nb_expr = 0; - global_vars = ["list_hd"; "list_tl"; "print"; "failwith"]; - global_constrs = ["pair"; "list_empty"; "list_cons"]; - global_mutuals = []; - actual_def = []; - wanabeeRigidNoms = [] - } + let ctx = { + nb_expr = 0; + (* Builtin functions *) + global_vars = ["list_hd"; "list_tl"; "print"; "failwith"]; + global_constrs = ["pair"; "list_empty"; "list_cons"]; + global_mutuals = []; + actual_def = []; + wanabeeRigidNoms = [] + } in let add_global v = ctx.global_vars <- v::ctx.global_vars in let add_constr c = ctx.global_constrs <- c::ctx.global_constrs in @@ -202,7 +211,7 @@ let mlts_to_prolog p = snd row_local_name in (* Adding all mutually defined functions to env *) - let local_names, selects, env, _ = List.fold_left + let _local_names, selects, env, _ = List.fold_left (fun (locals, selects, env, i) (LBVal(name, _, _)) -> let ln, env = add_mutual_to_env name row_local_name i env in let select = P.make_select name cap_row_local_name i in @@ -212,7 +221,7 @@ let mlts_to_prolog p = (* A row is a list of lambda expressions and a matching sequence of projections *) let lambdas, projs, env = List.fold_left - (fun (l, p, env) (LBVal(name, params, expr)) -> + (fun (l, _p, env) (LBVal(_name, params, expr)) -> let body, env = make_lam env params expr in body::l, [](*todo*), env) ([],[],env) mutuals in @@ -222,7 +231,7 @@ let mlts_to_prolog p = (* Creating let-expressions for all mutual functions and adding them to the global env *) - let lets = List.map (fun (name, row_name, select) -> + let tlets = List.map (fun (name, row_name, select) -> add_global name; P.Definition({ name = "prog"; @@ -238,10 +247,7 @@ let mlts_to_prolog p = args = [P.Lit(P.String(row_name)); P.make_row row_local_name (List.rev lambdas) projs ]; body = P.make_deps (env.free_vars); - }))::lets - - - (*failwith "Mutual rec not implemented"*) + }))::tlets | DType(name, decls) -> set_actual_def ctx name pos; @@ -252,7 +258,7 @@ let mlts_to_prolog p = | Sum(_, _) as s -> P.List (List.rev (list_of_sum s)) | Arrow(ty1, ty2) -> P.make_app "arr" [t_typ ty1; t_typ ty2] | Bind(ty1, ty2) -> P.make_app "bigarr" [t_typ ty1; t_typ ty2] - | List(ty) -> P.make_app "t_list" [t_typ ty](*failwith "List (type) not implemented"*) + | List(ty) -> P.make_app "t_list" [t_typ ty] in match ty with | Sum(ty1, ty2) -> (t_typ ty2)::(list_of_sum ty1) @@ -307,9 +313,9 @@ let mlts_to_prolog p = | ELetRecin(LBVal(name, params, e), body) -> (*let name = ((fst ln) ^ "_" ^ (string_of_int (snd ln))) in*) let ln, env = add_to_env name envIn in - let letbody, env = make_lam env params e in + let tletbody, env = make_lam env params e in let body, env = t_expr env body in - P.make_letrecin ln letbody body, revert_locals envIn env + P.make_letrecin ln tletbody body, revert_locals envIn env | EMatch(e, rules) -> let e, env = t_expr envIn e in @@ -515,6 +521,7 @@ let mlts_to_prolog p = let tm, env = aux envInitial params e in tm, revert_locals envInitial env in + let make_death_list (l : def list) : (string * int) list = List.map (fun (d : def) -> (d.name, d.pos.pos_lnum)) l in