Stefan pushed to branch master at Stefan / Typer

Commits: 133a2261 by Stefan Monnier at 2016-11-30T17:28:01-05:00 Streamline the integer binary ops slightly

* btl/builtins.typer (_+_, _*_): Adapt to new builtin names. (_-_, _/_): New builtins.

* src/eval.ml (add_binary_iop): Rename from _generic_binary_iop; Rewrite. Register the primitive into builtin_functions. (iadd_impl, isub_impl, imult_impl, idiv_impl): Don't give them names. (typer_builtins_impl): Remove. (<toplevel>): Don't manually add _+_ and _*_ to builtin_functions.

* src/lparse.ml (sform_built_in): Check builtin_functions to make sure the built-in actually exists.

- - - - -

3 changed files:

- btl/builtins.typer - src/eval.ml - src/lparse.ml

Changes:

===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -39,8 +39,10 @@ Unit = inductive_ Unit unit; unit = inductive-cons Unit unit;

% Basic operators -_+_ = Built-in "_+_" (Int -> Int -> Int); -_*_ = Built-in "_*_" (Int -> Int -> Int); +_+_ = Built-in "Int.+" (Int -> Int -> Int); +_-_ = Built-in "Int.-" (Int -> Int -> Int); +_*_ = Built-in "Int.*" (Int -> Int -> Int); +_/_ = Built-in "Int./" (Int -> Int -> Int);

Bool = inductive_ (Boolean) (True) (False); True = inductive-cons Bool True;

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -122,23 +122,19 @@ let elexp_fatal = debug_message fatal elexp_name elexp_string * Builtins *) (* Builtin of builtin * string * ltype *) -let _generic_binary_iop name f loc (depth : eval_debug_info) - (args_val: value_type list) = - - let l, r = match args_val with - | [l; r] -> l, r - | _ -> error loc (name ^ " expects 2 Integers arguments") in +let add_binary_iop name f = + let name = "Int." ^ name in + let f loc (depth : eval_debug_info) (args_val: value_type list) = + match args_val with + | [Vint(v); Vint(w)] -> Vint (f v w) + | _ -> error loc ("`" ^ name ^ "` expects 2 Integers arguments") in + add_builtin_function name f 2

- match l, r with - | Vint(v), Vint(w) -> Vint(f v w) - | _ -> - debug_messages fatal loc (name ^ " expects Integers as arguments") [ - "(" ^ name ^ " " ^ (value_string l) ^ " " ^ (value_string r) ^ ")";]

-let iadd_impl = _generic_binary_iop "Integer::add" (fun a b -> a + b) -let isub_impl = _generic_binary_iop "Integer::sub" (fun a b -> a - b) -let imult_impl = _generic_binary_iop "Integer::mult" (fun a b -> a * b) -let idiv_impl = _generic_binary_iop "Integer::div" (fun a b -> a / b) +let _ = add_binary_iop "+" (+); + add_binary_iop "-" (-); + add_binary_iop "*" ( * ); + add_binary_iop "/" (/)

let make_symbol loc depth args_val = (* symbol is a simple string *) @@ -311,12 +307,11 @@ and eval_call loc i f args = (* return result of eval *) | _, [] -> f

- | Vcons (n, fields), _ -> - let e = Vcons(n, List.append fields args) in - (* value_print e; print_string "\n"; *) e + | Vcons (n, fields), _ + -> Vcons (n, List.append fields args)

- | Closure (x, e, ctx), v::vs -> - let rec bindargs e vs ctx = match (vs, e) with + | Closure (x, e, ctx), v::vs + -> let rec bindargs e vs ctx = match (vs, e) with | (v::vs, Lambda ((_, x), e)) (* "Uncurry" on the fly. *) -> bindargs e vs (add_rte_variable (Some x) v ctx) @@ -324,44 +319,39 @@ and eval_call loc i f args = | _ -> eval_call loc i (_eval e ctx i) vs in bindargs e vs (add_rte_variable (Some x) v ctx)

- | Vbuiltin (name), args -> - (* FIXME: If there are fewer args, build a closure. - * FIXME: If there are too many args, pass it to the - * return value! *) - (* lookup the built-in implementation and call it *) - (try let (builtin, arity) = SMap.find name !builtin_functions in - let nargs = List.length args in - if nargs = arity then - builtin loc i args (* Fast common case. *) - else if nargs > arity then - let rec split n vs acc = match (n, vs) with - | 0, _ -> let v = eval_call loc i f (List.rev acc) in - eval_call loc i v vs - | _, (v::vs) -> split (n - 1) vs (v::acc) - | _ -> error loc "Impossible!" - in split nargs args [] - else - let rec buildctx args ctx = match args with - | [] -> ctx - | arg::args -> buildctx args (add_rte_variable None arg ctx) in - let rec buildargs n = - if n >= 0 - then (Var ((loc, "<dummy>"), n))::buildargs (n - 1) - else [] in - let rec buildbody n = - if n > 0 then - Lambda ((loc, "<dummy>"), buildbody (n - 1)) - else Call (Builtin (dloc, name), buildargs (arity - 1)) in - Closure ("<dummy>", - buildbody (arity - nargs - 1), - buildctx args Myers.nil) - - with Not_found -> - error loc ("Requested Built-in `" ^ name ^ "` does not exist") + | Vbuiltin (name), args + -> (try let (builtin, arity) = SMap.find name !builtin_functions in + let nargs = List.length args in + if nargs = arity then + builtin loc i args (* Fast common case. *) + else if nargs > arity then + let rec split n vs acc = match (n, vs) with + | 0, _ -> let v = eval_call loc i f (List.rev acc) in + eval_call loc i v vs + | _, (v::vs) -> split (n - 1) vs (v::acc) + | _ -> error loc "Impossible!" + in split nargs args [] + else + let rec buildctx args ctx = match args with + | [] -> ctx + | arg::args -> buildctx args (add_rte_variable None arg ctx) in + let rec buildargs n = + if n >= 0 + then (Var ((loc, "<dummy>"), n))::buildargs (n - 1) + else [] in + let rec buildbody n = + if n > 0 then + Lambda ((loc, "<dummy>"), buildbody (n - 1)) + else Call (Builtin (dloc, name), buildargs (arity - 1)) in + Closure ("<dummy>", + buildbody (arity - nargs - 1), + buildctx args Myers.nil) + + with Not_found -> + error loc ("Requested Built-in `" ^ name ^ "` does not exist") | e -> error loc ("Exception thrown from primitive `" ^ name ^"`"))

- | _ -> - value_fatal loc f "Trying to call a non-function!" + | _ -> value_fatal loc f "Trying to call a non-function!"

and eval_case ctx i loc target pat dflt = (* Eval target *) @@ -426,26 +416,6 @@ and _eval_decls (decls: (vdef * elexp) list) (* -------------------------------------------------------------------------- *) (* Builtin Implementation (Some require eval) *)

-and typer_builtins_impl = [ - ("_+_" , iadd_impl); - ("_*_" , imult_impl); - ("block_" , make_block); - ("symbol_" , make_symbol); - ("string_" , make_string); - ("integer_" , make_integer); - ("float_" , make_float); - ("node_" , make_node); - ("sexp_dispatch_", sexp_dispatch); - ("string_eq" , string_eq); - ("int_eq" , int_eq); - ("sexp_eq" , sexp_eq); - ("open" , open_impl); - ("bind" , bind_impl); - ("run-io" , run_io); - ("read" , read_impl); - ("write" , write_impl); -] - and bind_impl loc depth args_val = match args_val with | [Vcommand (cmd); callback] @@ -567,8 +537,6 @@ and print_eval_trace trace =

let _ = List.iter (fun (name, f, arity) -> add_builtin_function name f arity) [ - ("_+_" , iadd_impl, 2); - ("_*_" , imult_impl, 2); ("block_" , make_block, 1); ("symbol_" , make_symbol, 1); ("string_" , make_string, 1);

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -44,7 +44,7 @@ open Lexp open Env open Debruijn module DB = Debruijn -open Eval +module EV = Eval

open Grammar module BI = Builtin @@ -74,7 +74,7 @@ let fatal = msg_fatal "LPARSE"

(* Print Lexp name followed by the lexp in itself, finally throw an exception *) let debug_message error_type type_name type_string loc expr message = - debug_messages error_type loc + EV.debug_messages error_type loc message [ (type_name expr) ^ ": " ^ (type_string expr); ] @@ -165,7 +165,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = then elab_check_proper_type ctx ltype (Some var) else - (debug_messages fatal loc "Type check error: ¡¡ctx_define error!!" [ + (EV.debug_messages fatal loc "Type check error: ¡¡ctx_define error!!" [ lexp_string lxp ^ " !: " ^ lexp_string ltype; " because"; lexp_string ltype' ^ " != " ^ lexp_string ltype]) @@ -868,11 +868,11 @@ and lexp_expand_macro_ macro_funct sargs ctx expand_fun : value_type =

let macro = mkCall (macro_expand, args) in let emacro = OL.erase_type macro in - let rctx = from_lctx ctx in + let rctx = EV.from_lctx ctx in

(* eval macro *) - let vxp = try _eval emacro rctx ([], []) - with e -> print_eval_trace None; raise e in + let vxp = try EV._eval emacro rctx ([], []) + with e -> EV.print_eval_trace None; raise e in (* Return results *) (* Vint/Vstring/Vfloat might need to be converted to sexp *) vxp @@ -1089,6 +1089,8 @@ let sform_built_in ctx loc sargs = let meta_ctx, _ = !global_substitution in let ltp' = OL.lexp_close meta_ctx (ectx_to_lctx ctx) ltp in let bi = mkBuiltin ((loc, name), ltp', None) in + if not (SMap.mem name (!EV.builtin_functions)) then + sexp_error loc ("Unknown built-in `" ^ name ^ "`"); BI.add_builtin_cst name bi; bi

@@ -1175,7 +1177,7 @@ let default_lctx = lctx in lctx

-let default_rctx = from_lctx default_lctx +let default_rctx = EV.from_lctx default_lctx

(* String Parsing * --------------------------------------------------------- *) @@ -1211,12 +1213,12 @@ let lexp_decl_str str lctx = let _eval_expr_str str lctx rctx silent = let lxps = lexp_expr_str str lctx in let elxps = List.map OL.erase_type lxps in - (eval_all elxps rctx silent) + (EV.eval_all elxps rctx silent)

let eval_expr_str str lctx rctx = _eval_expr_str str lctx rctx false

let eval_decl_str str lctx rctx = let lxps, lctx = lexp_decl_str str lctx in let elxps = (List.map OL.clean_decls lxps) in - (eval_decls_toplevel elxps rctx), lctx + (EV.eval_decls_toplevel elxps rctx), lctx

View it on GitLab: https://gitlab.com/monnier/typer/commit/133a2261c1981cf4344a2be3ad47e6ee55b5...