Novembre 2016 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer][master] Streamline the integer binary ops slightly
by Stefan 30 Nov '16

30 Nov '16

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/133a2261c1981cf4344a2be3ad47e6ee55b…

1 0

[Git][monnier/typer][master] Fix partial application of builtins
by Stefan 30 Nov '16

30 Nov '16

Stefan pushed to branch master at Stefan / Typer Commits: cda68e29 by Stefan Monnier at 2016-11-30T13:43:14-05:00 Fix partial application of builtins * src/eval.ml (builtin_functions): Rename from _builtin_lookup. Add arity info for each primitive. (add_builtin_function): New function. (_eval): Eval `Call` args before calling eval_call. (get_predef_eval): Remove unused. (eval_call): Rewrite. Signal an error if a builtin throws an exception: since Typer's language is total this should only happen if there's a bug in Typer's own code. (bind_impl): Use eval_call; simplify. (get_builtin_impl): Remove. Pre-fill builtin_functions instead. * src/elexp.ml (elexp_string): Add deb-indices in output. * tests/eval_test.ml ("Partial Application"): Also test partial application of builtins. - - - - - 3 changed files: - src/elexp.ml - src/eval.ml - tests/eval_test.ml Changes: ===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -118,7 +118,7 @@ and elexp_string lxp = match lxp with | Imm(s) -> sexp_string s | Builtin((_, s)) -> s - | Var((_, s), _) -> s + | Var((_, s), i) -> s ^ "[" ^ string_of_int i ^ "]" | Cons((_, s)) -> s | Lambda((_, s), b) -> "lambda " ^ s ^ " -> " ^ (elexp_string b) ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -52,8 +52,15 @@ let dloc = dummy_location let _global_eval_trace = ref ([], []) let _global_eval_ctx = ref make_runtime_ctx let _eval_max_recursion_depth = ref 255 -let _builtin_lookup = ref (SMap.empty : (location -> eval_debug_info - -> value_type list -> value_type) SMap.t) + +let builtin_functions + = ref (SMap.empty : ((location -> eval_debug_info + -> value_type list -> value_type) + (* The primitive's arity. *) + * int) SMap.t) + +let add_builtin_function name f arity = + builtin_functions := SMap.add name (f, arity) (!builtin_functions) let append_eval_trace trace (expr : elexp) = let (a, b) = trace in @@ -278,8 +285,12 @@ let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type eval inst nctx (* Function call *) - | Call (lname, args) -> - eval_call ctx (append_typer_trace trace lxp) lname args + | Call (f, args) + (* FIXME: Add the trace only once we enter the function? *) + -> let ntrace = append_typer_trace trace lxp in + eval_call (elexp_location f) ntrace + (_eval f ctx ntrace) + (List.map (fun e -> _eval e ctx ntrace) args) (* Case *) | Case (loc, target, pat, dflt) @@ -288,11 +299,6 @@ let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type | Type -> Vcons((tloc, "Unit"), []) -and get_predef_eval name ctx = - let r = (get_rte_size ctx) - !builtin_size in - let v = mkSusp (get_predef_raw name) (S.shift r) in - _eval (OL.erase_type v) ctx ([], []) - and eval_var ctx lxp v = let ((loc, name), idx) = v in try get_rte_variable (Some name) (idx) ctx @@ -300,36 +306,62 @@ and eval_var ctx lxp v = elexp_fatal loc lxp ("Variable: " ^ name ^ (str_idx idx) ^ " was not found ") -and eval_call ctx i lname eargs = - let loc = elexp_location lname in - let f = _eval lname ctx i in - - (* standard function *) - let rec eval_call f args ctx = - match f, args with - | Vcons (n, []), _ -> - let e = Vcons(n, args) in - (* value_print e; print_string "\n"; *) e - - (* we add an argument to the closure *) - | Closure (n, lxp, ctx), hd::tl -> - let nctx = add_rte_variable (Some n) hd ctx in - let ret = _eval lxp nctx i in - eval_call ret tl nctx - - | Vbuiltin (str), args -> - (* lookup the built-in implementation and call it *) - (get_builtin_impl str loc) loc i args - - (* return result of eval *) - | _, [] -> f - - | _ -> - value_fatal loc f "Cannot eval function" in - - (* eval function here *) - let args = List.map (fun e -> _eval e ctx i) eargs in - eval_call f args ctx +and eval_call loc i f args = + match f, args with + (* return result of eval *) + | _, [] -> f + + | Vcons (n, fields), _ -> + let e = Vcons(n, List.append fields args) in + (* value_print e; print_string "\n"; *) e + + | 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) + | ([], _) -> _eval e ctx i + | _ -> 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") + | e -> error loc ("Exception thrown from primitive `" ^ name ^"`")) + + | _ -> + value_fatal loc f "Trying to call a non-function!" and eval_case ctx i loc target pat dflt = (* Eval target *) @@ -415,31 +447,11 @@ and typer_builtins_impl = [ ] and bind_impl loc depth args_val = - - let io, cb = match args_val with - | [io; callback] -> io, callback - | _ -> error loc "bind expects two arguments" in - - (* build Vcommand from io function *) - let cmd = match io with - | Vcommand (cmd) -> cmd - | _ -> error loc "bind first arguments must be a monad" in - - (* bind returns another Vcommand *) - Vcommand (fun () -> - (* get callback *) - let body, ctx = match cb with - | Closure(_, body, ctx) -> body, ctx - | _ -> error loc "A Closure was expected" in - - (* run given command *) - let underlying = cmd () in - - (* add evaluated IO to arg list *) - let nctx = add_rte_variable None underlying ctx in - - (* eval callback *) - _eval body nctx depth) + match args_val with + | [Vcommand (cmd); callback] + -> (* bind returns another Vcommand *) + Vcommand (fun () -> eval_call loc depth callback [cmd ()]) + | _ -> error loc "Wrong number of args or wrong first arg value in `bind`" and run_io loc depth args_val = @@ -457,18 +469,6 @@ and run_io loc depth args_val = (* return given type *) ltp -and get_builtin_impl str loc = - (* Make built-in lookup table *) - (match (SMap.is_empty !_builtin_lookup) with - | true -> - _builtin_lookup := (List.fold_left (fun lkup (name, f) -> - SMap.add name f lkup) SMap.empty typer_builtins_impl) - | _ -> ()); - - try SMap.find str !_builtin_lookup - with Not_found -> - error loc ("Requested Built-in \"" ^ str ^ "\" does not exist") - (* Sexp -> (Sexp -> List Sexp -> Sexp) -> (String -> Sexp) -> (String -> Sexp) -> (Int -> Sexp) -> (Float -> Sexp) -> (List Sexp -> Sexp) -> Sexp *) @@ -565,6 +565,27 @@ and print_eval_trace trace = let (a, b) = !_global_eval_trace in print_trace " EVAL TRACE " trace a +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); + ("integer_" , make_integer, 1); + ("float_" , make_float, 1); + ("node_" , make_node, 2); + ("sexp_dispatch_", sexp_dispatch, 7); + ("string_eq" , string_eq, 2); + ("int_eq" , int_eq, 2); + ("sexp_eq" , sexp_eq, 2); + ("open" , open_impl, 2); + ("bind" , bind_impl, 2); + ("run-io" , run_io, 2); + ("read" , read_impl, 2); + ("write" , write_impl, 2); + ] + let eval lxp ctx = _eval lxp ctx ([], []) let debug_eval lxp ctx = ===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -230,12 +230,12 @@ let _ = test_eval_eqv_named "add : Int -> Int -> Int; add = lambda x y -> (x + y); - inc : Int -> Int; - inc = add 1;" + inc1 = add 1; + inc2 = _+_ 2;" - "inc 1; inc 2; inc 3;" + "inc1 1; inc2 2; inc1 3;" - "2; 3; 4" + "2; 4; 4" (* * Lists View it on GitLab: https://gitlab.com/monnier/typer/commit/cda68e292e4c6d2c7b1b9e0a37a9f0154fd…

1 0

[Git][monnier/typer][master] * src/eval.ml: Don't pass `ctx` to builtins
by Stefan 30 Nov '16

30 Nov '16

Stefan pushed to branch master at Stefan / Typer Commits: 96d9936b by Stefan Monnier at 2016-11-30T12:11:59-05:00 * src/eval.ml: Don't pass `ctx` to builtins (none_fun): Remove, unused. (typer_eval): Remove function and corresponding builtin. (_builtin_lookup): Change type. - - - - - 1 changed file: - src/eval.ml Changes: ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -52,7 +52,8 @@ let dloc = dummy_location let _global_eval_trace = ref ([], []) let _global_eval_ctx = ref make_runtime_ctx let _eval_max_recursion_depth = ref 255 -let _builtin_lookup = ref SMap.empty +let _builtin_lookup = ref (SMap.empty : (location -> eval_debug_info + -> value_type list -> value_type) SMap.t) let append_eval_trace trace (expr : elexp) = let (a, b) = trace in @@ -113,12 +114,9 @@ let elexp_fatal = debug_message fatal elexp_name elexp_string (* * Builtins *) -let none_fun : (location -> eval_debug_info -> value_type list -> runtime_env -> value_type) - = (fun loc args_val ctx -> error loc "Requested Built-in was not implemented") - (* Builtin of builtin * string * ltype *) let _generic_binary_iop name f loc (depth : eval_debug_info) - (args_val: value_type list) (ctx: runtime_env) = + (args_val: value_type list) = let l, r = match args_val with | [l; r] -> l, r @@ -135,7 +133,7 @@ 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 make_symbol loc depth args_val ctx = +let make_symbol loc depth args_val = (* symbol is a simple string *) let lxp = match args_val with | [r] -> r @@ -145,7 +143,7 @@ let make_symbol loc depth args_val ctx = | Vstring(str) -> Vsexp(Symbol(loc, str)) | _ -> value_error loc lxp "symbol_ expects one string as argument" -let make_node loc depth args_val ctx = +let make_node loc depth args_val = let op, tlist = match args_val with | [Vsexp(op); lst] -> op, lst @@ -162,12 +160,12 @@ let make_node loc depth args_val ctx = | Vint (i) -> Integer(dloc, i) | Vstring (s) -> String(dloc, s) | _ -> - print_rte_ctx ctx; + (* print_rte_ctx ctx; *) value_error loc g "node_ expects 'List Sexp' second as arguments") args in Vsexp(Node(op, s)) -let make_string loc depth args_val ctx = +let make_string loc depth args_val = let lxp = match args_val with | [r] -> r | _ -> error loc "string_ expects 1 argument" in @@ -176,7 +174,7 @@ let make_string loc depth args_val ctx = | Vstring(str) -> Vsexp(String(loc, str)) | _ -> value_error loc lxp "string_ expects one string as argument" -let make_integer loc depth args_val ctx = +let make_integer loc depth args_val = let lxp = match args_val with | [r] -> r | _ -> error loc "integer_ expects 1 argument" in @@ -185,29 +183,29 @@ let make_integer loc depth args_val ctx = | Vint(str) -> Vsexp(Integer(loc, str)) | _ -> value_error loc lxp "integer_ expects one string as argument" -let make_float loc depth args_val ctx = Vdummy -let make_block loc depth args_val ctx = Vdummy +let make_float loc depth args_val = Vdummy +let make_block loc depth args_val = Vdummy let ttrue = Vcons((dloc, "True"), []) let tfalse = Vcons((dloc, "False"), []) let btyper b = if b then ttrue else tfalse -let string_eq loc depth args_val ctx = +let string_eq loc depth args_val = match args_val with | [Vstring(s1); Vstring(s2)] -> btyper (s1 = s2) | _ -> error loc "string_eq expects 2 strings" -let int_eq loc depth args_val ctx = +let int_eq loc depth args_val = match args_val with | [Vint(s1); Vint(s2)] -> btyper (s1 = s2) | _ -> error loc "int_eq expects 2 integer" -let sexp_eq loc depth args_val ctx = +let sexp_eq loc depth args_val = match args_val with | [Vsexp (s1); Vsexp (s2)] -> btyper (sexp_equal s1 s2) | _ -> error loc "sexp_eq expects 2 sexp" -let open_impl loc depth args_val ctx = +let open_impl loc depth args_val = let file, mode = match args_val with | [Vstring(file_name); Vstring(mode)] -> file_name, mode @@ -220,7 +218,7 @@ let open_impl loc depth args_val ctx = | "w" -> Vout(open_out file) | _ -> error loc "wrong open mode") -let read_impl loc depth args_val ctx = +let read_impl loc depth args_val = let channel = match args_val with | [Vin(c); _] -> c @@ -231,7 +229,7 @@ let read_impl loc depth args_val ctx = let line = input_line channel in Vstring(line) -let write_impl loc depth args_val ctx = +let write_impl loc depth args_val = let channel, msg = match args_val with | [Vout(c); Vstring(msg)] -> c, msg @@ -321,7 +319,7 @@ and eval_call ctx i lname eargs = | Vbuiltin (str), args -> (* lookup the built-in implementation and call it *) - (get_builtin_impl str loc) loc i args ctx + (get_builtin_impl str loc) loc i args (* return result of eval *) | _, [] -> f @@ -409,7 +407,6 @@ and typer_builtins_impl = [ ("string_eq" , string_eq); ("int_eq" , int_eq); ("sexp_eq" , sexp_eq); - ("eval_" , typer_eval); ("open" , open_impl); ("bind" , bind_impl); ("run-io" , run_io); @@ -417,7 +414,7 @@ and typer_builtins_impl = [ ("write" , write_impl); ] -and bind_impl loc depth args_val ctx = +and bind_impl loc depth args_val = let io, cb = match args_val with | [io; callback] -> io, callback @@ -444,7 +441,7 @@ and bind_impl loc depth args_val ctx = (* eval callback *) _eval body nctx depth) -and run_io loc depth args_val ctx = +and run_io loc depth args_val = let io, ltp = match args_val with | [io; ltp] -> io, ltp @@ -460,17 +457,6 @@ and run_io loc depth args_val ctx = (* return given type *) ltp -and typer_eval loc depth args ctx = - let arg = match args with - | [a] -> a - | _ -> error loc "eval_ expects a single argument" in - (* I need to be able to lexp sexp but I don't have lexp ctx *) - match arg with - (* Nodes that can be evaluated *) - | Closure (_, body, ctx) -> _eval body ctx depth - (* Leaf *) - | _ -> arg - and get_builtin_impl str loc = (* Make built-in lookup table *) (match (SMap.is_empty !_builtin_lookup) with @@ -486,7 +472,7 @@ and get_builtin_impl str loc = (* Sexp -> (Sexp -> List Sexp -> Sexp) -> (String -> Sexp) -> (String -> Sexp) -> (Int -> Sexp) -> (Float -> Sexp) -> (List Sexp -> Sexp) -> Sexp *) -and sexp_dispatch loc depth args ctx = +and sexp_dispatch loc depth args = let eval a b = _eval a b depth in let sxp, nd, sym, str, it, flt, blk, rctx = match args with | [sxp; Closure(_, nd, rctx); Closure(_, sym, _); View it on GitLab: https://gitlab.com/monnier/typer/commit/96d9936b1029c1f07e29bd0696596ef1b74…

1 0

[Git][monnier/typer][master] Make `Builtin`s be closed and available via ##... syntax
by Stefan 29 Nov '16

29 Nov '16

Stefan pushed to branch master at Stefan / Typer Commits: 8396dc22 by Stefan Monnier at 2016-11-29T13:31:20-05:00 Make `Builtin`s be closed and available via ##... syntax * src/builtin.ml (type_eq, olist2tlist_lexp): Add missing hashconsing. * src/lexp.ml (mkSusp): Don't make a susp for Builtins. (push_susp): Builtins are closed, so there's nothing to push anything. (eq, subst_eq): New functions. * src/lparse.ml (newMetalevel): Add missing hashconsing. (sform_built_in, sform_new_attribute): Close type of builtin. (sform_built_in): Add to BI.lmap so it's available via the ##... syntax. (sform_add_attribute): Close attr before adding it to table. * src/opslexp.ml (lctx_to_subst, lexp_close): New functions. (set_plexp): Rename from set_lexp, change it to hold pairs. (set_member_p, set_add): Rewrite. (conv_p'): Use a set of hypothetical equalities to break inf-loops. Add missing hashconsing. * src/unification.ml (unify'): Mirror change in OL.conv_p'. - - - - - 6 changed files: - DESIGN - src/builtin.ml - src/lexp.ml - src/lparse.ml - src/opslexp.ml - src/unification.ml Changes: ===================================== DESIGN ===================================== --- a/DESIGN +++ b/DESIGN @@ -998,26 +998,6 @@ the recursive calls. (e.g. that need to know the set of freevars in one of its arguments) are "impossible" unless Typer provides extra support for them. * Syntax -** Lexical rules -Tokens will be made of any sequence of letters other than blanks/comments. - - blanks = LF, CR, TAB, SPC - comments = %...\n - strings = "...\?..." - numbers = as standard as possible - maybe handle \ specially not only in strings but anywhere else as well - special token = sequence of chars which is always treated as a single - token even if it's not surrounded by blanks. The set of special tokens - can be extended by the programmer. - magic token = the _ char is magical in that it forcefully connects even - special tokens: a(b are 3 tokens if ( is special, but a_(_b is a single - (magic) token. - -** Structured identifiers -We want to support identifiers with inner structure, such as "foo.bar.baz". - -This could be lexed into a Node identical to that of ( __.__ foo bar baz) - ** Provide syntax for backquote&unquote Since "," is to be used as separator, maybe (,e) and (`e) could be used? ** Macros ===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -118,17 +118,19 @@ let dump_predef () = (* Builtin types *) let dloc = DB.dloc -let op_binary t = Arrow (Aexplicit, None, t, dloc, - Arrow (Aexplicit, None, t, dloc, t)) +let op_binary t = mkArrow (Aexplicit, None, t, dloc, + mkArrow (Aexplicit, None, t, dloc, t)) let type_eq = let lv = (dloc, "l") in let tv = (dloc, "t") in - Arrow (Aerasable, Some lv, DB.type_level, dloc, - Arrow (Aerasable, Some tv, - Sort (dloc, Stype (Var (lv, 0))), dloc, - Arrow (Aexplicit, None, Var (tv, 0), dloc, - Arrow (Aexplicit, None, Var (tv, 1), dloc, - DB.type0)))) + mkArrow (Aerasable, Some lv, + DB.type_level, dloc, + mkArrow (Aerasable, Some tv, + mkSort (dloc, Stype (Var (lv, 0))), dloc, + mkArrow (Aexplicit, None, Var (tv, 0), dloc, + mkArrow (Aexplicit, None, + mkVar (tv, 1), dloc, + DB.type0)))) (* lexp Imm list *) @@ -138,8 +140,8 @@ let olist2tlist_lexp lst ctx = let rlst = List.rev lst in List.fold_left (fun tail elem -> - Call(tcons, [(Aexplicit, (Imm(elem))); - (Aexplicit, tail)])) tnil rlst + mkCall(tcons, [(Aexplicit, (Imm(elem))); + (Aexplicit, tail)])) tnil rlst (* typer list as seen during runtime *) let olist2tlist_rte lst = @@ -193,5 +195,5 @@ let builtins = let _ = new_builtin_type "Sexp" DB.type0 let _ = new_builtin_type - "IO" (Arrow (Aexplicit, None, DB.type0, dloc, DB.type0)) + "IO" (mkArrow (Aexplicit, None, DB.type0, dloc, DB.type0)) let _ = new_builtin_type "FileHandle" DB.type0 ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -168,6 +168,7 @@ let rec mkSusp e s = match e with (* FIXME: `Builtin` shouuld be treated like `Imm`. *) | Imm _ -> e + | Builtin _ -> e | Susp (e, s') -> mkSusp e (scompose s' s) | Var (l,v) -> slookup s l v | Metavar (vn, s', vd, t) -> mkMetavar (vn, scompose s' s, vd, mkSusp t s) @@ -211,11 +212,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) | SortLevel (SLsucc e') -> mkSortLevel (SLsucc (mkSusp e' s)) | Sort (l, Stype e) -> mkSort (l, Stype (mkSusp e s)) | Sort (l, _) -> e - | Builtin (l, ltp, otable) - -> let otable' = match otable with - | Some table -> Some (AttributeMap.map (fun lxp -> mkSusp lxp s) table) - | _ -> None in - mkBuiltin (l, (mkSusp ltp s), otable') + | Builtin _ -> e | Let (l, defs, e) -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in @@ -693,3 +690,73 @@ and _lexp_str_decls ctx decls = (name ^ " = " ^ (lexp_to_str lxp) ^ ";" ^ sepdecl)::str) [] decls in List.rev ret + +(** Syntactic equality (i.e. without β). *******) + +let rec eq meta_ctx e1 e2 = + e1 == e2 || + let eq = eq meta_ctx in + match (e1, e2) with + | (Imm (Integer (_, i1)), Imm (Integer (_, i2))) -> i1 = i2 + | (Imm (Float (_, x1)), Imm (Float (_, x2))) -> x1 = x2 + | (Imm (String (_, s1)), Imm (String (_, s2))) -> s1 = s2 + | (Imm s1, Imm s2) -> s1 = s2 + | (SortLevel SLz, SortLevel SLz) -> true + | (SortLevel (SLsucc e1), SortLevel (SLsucc e2)) -> eq e1 e2 + | (Sort (_, StypeOmega), Sort (_, StypeOmega)) -> true + | (Sort (_, StypeLevel), Sort (_, StypeLevel)) -> true + | (Sort (_, Stype e1), Sort (_, Stype e2)) -> eq e1 e2 + | (Builtin ((_, name1), _, _), Builtin ((_, name2), _, _)) -> name1 = name2 + | (Var (_, i1), Var (_, i2)) -> i1 = i2 + | (Susp (e1, s1), e2) -> eq (push_susp e1 s1) e2 + | (e1, Susp (e2, s2)) -> eq e1 (push_susp e2 s2) + | (Let (_, defs1, e1), Let (_, defs2, e2)) + -> eq e1 e2 && List.for_all2 (fun (_, e1, t1) (_, e2, t2) + -> eq t1 t2 && eq e1 e2) + defs1 defs2 + | (Arrow (ak1, _, t11, _, t21), Arrow (ak2, _, t12, _, t22)) + -> ak1 = ak2 && eq t11 t12 && eq t21 t22 + | (Lambda (ak1, _, t1, e1), Lambda (ak2, _, t2, e2)) + -> ak1 = ak2 && eq t1 t2 && eq e1 e2 + | (Call (e1, as1), Call (e2, as2)) + -> eq e1 e2 && List.for_all2 (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && eq e1 e2) + as1 as2 + | (Inductive (_, l1, as1, cases1), Inductive (_, l2, as2, cases2)) + -> l1 = l2 + && List.for_all2 (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && eq e1 e2) + as1 as2 + && SMap.equal (List.for_all2 (fun (ak1, _, e1) (ak2, _, e2) + -> ak1 = ak2 && eq e1 e2)) + cases1 cases2 + | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> eq t1 t2 && l1 = l2 + | (Case (_, e1, r1, cases1, def1), Case (_, e2, r2, cases2, def2)) + -> eq e1 e2 && eq r1 r2 + && SMap.equal (fun (_, fields1, e1) (_, fields2, e2) + -> eq e1 e2 && List.for_all2 (fun (ak1, _) (ak2, _) + -> ak1 = ak2) + fields1 fields2) + cases1 cases2 + && (match (def1, def2) with + | (Some (_, e1), Some (_, e2)) -> eq e1 e2 + | _ -> def1 = def2) + | (Metavar (i1, s1, _, t1), Metavar (i2, s2, _, t2)) + -> i1 = i2 && eq t1 t2 && subst_eq meta_ctx s1 s2 + | _ -> false + +and subst_eq meta_ctx s1 s2 = + s1 == s2 || + match (s1, s2) with + | (S.Identity, S.Identity) -> true + | (S.Cons (e1, s1), S.Cons (e2, s2)) + -> eq meta_ctx e1 e2 && subst_eq meta_ctx s1 s2 + | (S.Shift (s1, o1), S.Shift (s2, o2)) + -> let o = min o1 o2 in + subst_eq meta_ctx (S.mkShift s1 (o1 - o)) (S.mkShift s2 (o2 - o)) + | (S.Shift (S.Cons (e1, s1), o1), S.Cons (e2, s2)) + -> eq meta_ctx (mkSusp e1 (S.shift o1)) e2 + && subst_eq meta_ctx (S.mkShift s1 o1) s2 + | (S.Cons (e1, s1), S.Shift (S.Cons (e2, s2), o2)) + -> eq meta_ctx e1 (mkSusp e2 (S.shift o2)) + && subst_eq meta_ctx s1 (S.mkShift s2 o2) + | _ -> false + ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -237,7 +237,7 @@ let newMetavar l name t = mkMetavar (meta, S.Identity, (l, name), t) let newMetalevel () = - newMetavar Util.dummy_location "l" (Sort (dummy_location, StypeLevel)) + newMetavar Util.dummy_location "l" (mkSort (dummy_location, StypeLevel)) let newMetatype () = newMetavar Util.dummy_location "t" (newMetalevel ()) @@ -770,21 +770,21 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = let parg = pexp_parse lsarg in let larg = check parg arg_type ctx in - handle_fun_args ((Aimplicit, larg) :: largs) (sarg::sargs) pending - (L.mkSusp ret_type (S.substitute larg))) + handle_fun_args ((Aimplicit, larg) :: largs) (sarg::sargs) pending + (L.mkSusp ret_type (S.substitute larg))) (* Aerasable *) | sarg :: sargs, Arrow (Aerasable, v, arg_type, _, ret_type) -> let larg = newMetavar (sexp_location sarg) - (match v with Some (_, name) -> name | _ -> "v") - arg_type in - handle_fun_args ((Aerasable, larg) :: largs) (sarg::sargs) pending - (L.mkSusp ret_type (S.substitute larg)) + (match v with Some (_, name) -> name | _ -> "v") + arg_type in + handle_fun_args ((Aerasable, larg) :: largs) (sarg::sargs) pending + (L.mkSusp ret_type (S.substitute larg)) - | sarg :: sargs, t -> - print_lexp_ctx (ectx_to_lctx ctx); - lexp_fatal (sexp_location sarg) t - ("Explicit arg `" ^ sexp_string sarg - ^ "` to non-function (type = " ^ lexp_string ltp ^ ")") in + | sarg :: sargs, t + -> print_lexp_ctx (ectx_to_lctx ctx); + lexp_fatal (sexp_location sarg) t + ("Explicit arg `" ^ sexp_string sarg + ^ "` to non-function (type = " ^ lexp_string ltp ^ ")") in let handle_funcall () = let largs, ret_type = handle_fun_args [] sargs SMap.empty ltp in @@ -1002,14 +1002,17 @@ and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp = * -------------------------------------------------------------------------- *) and sform_new_attribute ctx loc sargs = - let ltp = match sargs with - | [t] -> lexp_parse_sexp ctx t - | _ -> fatal loc "new-attribute expects a single Type argument" in - - (* FIXME: This creates new values for type `ltp` (very wrong if `ltp` - * is False, for example): Should be a type like `AttributeMap t` - * instead. *) - Builtin ((loc, "new-attribute"), ltp, Some AttributeMap.empty) + match sargs with + | [t] -> let ptp = pexp_parse t in + let ltp = infer_type ptp ctx None in + let meta_ctx, _ = !global_substitution in + (* FIXME: This creates new values for type `ltp` (very wrong if `ltp` + * is False, for example): Should be a type like `AttributeMap t` + * instead. *) + mkBuiltin ((loc, "new-attribute"), + OL.lexp_close meta_ctx (ectx_to_lctx ctx) ltp, + Some AttributeMap.empty) + | _ -> fatal loc "new-attribute expects a single Type argument" and sform_add_attribute ctx loc (sargs : sexp list) = let n = get_size ctx in @@ -1018,13 +1021,14 @@ and sform_add_attribute ctx loc (sargs : sexp list) = | _ -> fatal loc "add-attribute expects 3 arguments (table; var; attr)" in let meta_ctx, _ = !global_substitution in - let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) meta_ctx with - | Builtin (_, attr_type, Some map)-> map, attr_type + let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) meta_ctx with + | Builtin (_, attr_type, Some map) -> map, attr_type | _ -> fatal loc "add-attribute expects a table as first argument" in - (* FIXME: Type check (attr: type == attr_type) *) - let table = AttributeMap.add var attr map in - Builtin ((loc, "add-attribute"), attr_type, Some table) + (* FIXME: Type check (attr: type == attr_type) *) + let attr' = OL.lexp_close meta_ctx (ectx_to_lctx ctx) attr in + let table = AttributeMap.add var attr' map in + mkBuiltin ((loc, "add-attribute"), attr_type, Some table) and get_attribute ctx loc largs = let ctx_n = get_size ctx in @@ -1079,10 +1083,14 @@ let sform_decltype ctx loc sargs = let sform_built_in ctx loc sargs = match !_parsing_internals, sargs with - | true, [String (_, str); stp] -> - let ptp = pexp_parse stp in - let ltp, _ = infer ptp ctx in - mkBuiltin((loc, str), ltp, None) + | true, [String (_, name); stp] + -> let ptp = pexp_parse stp in + let ltp = infer_type ptp ctx None in + 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 + BI.add_builtin_cst name bi; + bi | true, _ -> error loc "Wrong Usage of `Built-in`"; dlxp ===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -69,7 +69,49 @@ let rec lexp_defs_subst l s defs = match defs with | (_, lexp, _) :: defs' -> lexp_defs_subst l (S.cons (mkLet (l, defs, lexp)) s) defs' -(* Reduce to weak head normal form. +(** Convert a lexp_context into a substitution. *) + +let rec lctx_to_subst lctx = + match lctx with + | Myers.Mnil -> Subst.identity + | Myers.Mcons ((0, _, LetDef e, _), lctx, _, _) + -> let s = lctx_to_subst lctx in + L.scompose (S.substitute e) s + | Myers.Mcons ((0, ov, _, _), lctx, _, _) + -> let s = lctx_to_subst lctx in + (* Here we decide to keep those vars in the target domain. + * Another option would be to map them to `L.impossible`, + * hence making the target domain be empty (i.e. making the substitution + * generate closed results). *) + L.ssink (maybev ov) s + | Myers.Mcons ((1, ov, LetDef e, t), lctx, _, _) + -> let rec getdefs i lctx rdefs = + match lctx with + | Myers.Mcons ((o, ov, LetDef e, t), lctx, _, _) + when o = i + -> getdefs (i + 1) lctx ((maybev ov, e, t) :: rdefs) + | _ -> (lctx, List.rev rdefs) in + let (lctx, defs) = getdefs 2 lctx [(maybev ov, e, t)] in + let s1 = lctx_to_subst lctx in + let s2 = lexp_defs_subst DB.dloc S.identity defs in + L.scompose s2 s1 + | _ -> U.internal_error "Unexpected lexp_context shape!" + +(* Take an expression `e` that is "closed" relatively to context lctx + * and return an equivalent expression valid in the empty context. + * By "closed" I mean that it only refers to elements of the context which + * are LetDef. *) +let lexp_close meta_ctx lctx e = + (* There are many different ways to skin this cat. + * This is definitely not the best one: + * - it inlines all the definitions everywhere they're used + * - It turns the lctx (of O(log N) access time) into a subst + * (of O(N) access time) + * Oh well! *) + L.clean meta_ctx (mkSusp e (lctx_to_subst lctx)) + + +(** Reduce to weak head normal form. * WHNF implies: * - Not a Let. * - Not a let-bound variable. @@ -146,38 +188,39 @@ let lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = in lexp_whnf e ctx -(** A very naive implementation of sets of lexps. *) -type set_lexp = lexp list -let set_empty : set_lexp = [] -let set_member_p (s : set_lexp) (e : lexp) : bool - = if not (e == Lexp.hc e) then - (print_string "Not hashcons'd: "; - lexp_print e; - print_string "\n"); - assert (e == Lexp.hc e); - List.mem e s -let set_add (s : set_lexp) (e : lexp) : set_lexp - = assert (not (set_member_p s e)); - e :: s -let set_shift_n (s : set_lexp) (n : U.db_offset) - = List.map (fun e -> Lexp.push_susp e (S.shift n)) s -let set_shift s : set_lexp = set_shift_n s 1 +(** A very naive implementation of sets of pairs of lexps. *) +type set_plexp = (lexp * lexp) list +let set_empty : set_plexp = [] +let set_member_p meta_ctx (s : set_plexp) (e1 : lexp) (e2 : lexp) : bool + = assert (e1 == Lexp.hc e1); + assert (e2 == Lexp.hc e2); + try let _ = List.find (fun (e1', e2') + -> L.eq meta_ctx e1 e1' && L.eq meta_ctx e2 e2') + s + in true + with Not_found -> false +let set_add (s : set_plexp) (e1 : lexp) (e2 : lexp) : set_plexp + = (* assert (not (set_member_p meta_ctx s e1 e2)); *) + ((e1, e2) :: s) +let set_shift_n (s : set_plexp) (n : U.db_offset) + = List.map (let s = S.shift n in + fun (e1, e2) -> (Lexp.push_susp e1 s, Lexp.push_susp e2 s)) + s +let set_shift s : set_plexp = set_shift_n s 1 (********* Testing if two types are "convertible" aka "equivalent" *********) (* Returns true if e₁ and e₂ are equal (upto alpha/beta/...). *) -let rec conv_p' meta_ctx (ctx : DB.lexp_context) (vs : set_lexp) e1 e2 : bool = +let rec conv_p' meta_ctx (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let conv_p' = conv_p' meta_ctx in let e1' = lexp_whnf e1 ctx meta_ctx in let e2' = lexp_whnf e2 ctx meta_ctx in e1' == e2' || - let stop1 = not (e1 == e1') && set_member_p vs e1' in - let stop2 = not (e2 == e2') && set_member_p vs e2' in - let vs' = if not (e1 == e1') && not stop1 then set_add vs e1' - else if not (e2 == e2') && not stop2 then set_add vs e2' - else vs in + let changed = not (e1 == e1' && e2 == e2') in + if changed && set_member_p meta_ctx vs e1' e2' then true else + let vs' = if changed then set_add vs e1' e2' else vs in let conv_p = conv_p' ctx vs' in - match if stop1 || stop2 then (e1, e2) else (e1', e2') with + match (e1', e2') with | (Imm (Integer (_, i1)), Imm (Integer (_, i2))) -> i1 = i2 | (Imm (Float (_, i1)), Imm (Float (_, i2))) -> i1 = i2 | (Imm (String (_, i1)), Imm (String (_, i2))) -> i1 = i2 @@ -301,14 +344,15 @@ let rec check' meta_ctx erased ctx e = | Sort (l, Stype e) -> let t = check erased ctx e in assert_type ctx e t DB.type_level; - Sort (l, Stype (SortLevel (SLsucc e))) + mkSort (l, Stype (mkSortLevel (SLsucc e))) | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) -> (U.msg_error "TC" (lexp_location e) "Reached unreachable sort!"; (* U.internal_error "Reached unreachable sort!"; *) DB.sort_omega) | Builtin (_, t, _) - -> check_type DB.set_empty ctx t; (* FIXME: Use an empty ctx? *) + -> let _ = check_type DB.set_empty Myers.nil t in + (* FIXME: Check the attributemap as well! *) t (* FIXME: Check recursive references. *) | Var (((_, name), idx) as v) @@ -347,22 +391,22 @@ let rec check' meta_ctx erased ctx e = (* FIXME: fix scoping of `k2` and `s2`. *) -> if ak == P.Aerasable && impredicative_erase && s1 != StypeLevel then k2 - else Sort (l, sort_compose l s1 s2) + else mkSort (l, sort_compose l s1 s2) | (Sort (_, _), _) -> (U.msg_error "TC" (lexp_location t2) "Not a proper type"; - Sort (l, StypeOmega)) + mkSort (l, StypeOmega)) | (_, _) -> (U.msg_error "TC" (lexp_location t1) "Not a proper type"; - Sort (l, StypeOmega))) + mkSort (l, StypeOmega))) | Lambda (ak, ((l,_) as v), t, e) -> ((match lexp_whnf (check_type DB.set_empty ctx t) ctx meta_ctx with | Sort _ -> () | _ -> (U.msg_error "TC" (lexp_location t) "Formal arg type is not a type!"; ())); - Arrow (ak, Some v, t, l, - check (dbset_push ak erased) - (DB.lctx_extend ctx (Some v) Variable t) - e)) + mkArrow (ak, Some v, t, l, + check (dbset_push ak erased) + (DB.lctx_extend ctx (Some v) Variable t) + e)) | Call (f, args) -> let ft = check erased ctx f in List.fold_left @@ -414,10 +458,10 @@ let rec check' meta_ctx erased ctx e = case in level) cases (mkSortLevel SLz) in - Sort (l, Stype level) + mkSort (l, Stype level) | (ak, v, t)::args - -> Arrow (ak, Some v, t, lexp_location t, - arg_loop args (DB.lctx_extend ctx (Some v) Variable t)) in + -> mkArrow (ak, Some v, t, lexp_location t, + arg_loop args (DB.lctx_extend ctx (Some v) Variable t)) in let tct = arg_loop args ctx in tct | Case (l, e, ret, branches, default) @@ -489,15 +533,15 @@ let rec check' meta_ctx erased ctx e = let rec fieldargs ftypes = match ftypes with | [] -> let nargs = List.length fieldtypes + List.length fargs in - Call (mkSusp t (S.shift nargs), indtype fargs (nargs - 1)) + mkCall (mkSusp t (S.shift nargs), indtype fargs (nargs - 1)) | (ak, vd, ftype) :: ftypes - -> Arrow (ak, vd, ftype, lexp_location ftype, - fieldargs ftypes) in + -> mkArrow (ak, vd, ftype, lexp_location ftype, + fieldargs ftypes) in let rec buildtype fargs = match fargs with | [] -> fieldargs fieldtypes | (ak, ((l,_) as vd), atype) :: fargs - -> Arrow (P.Aerasable, Some vd, atype, l, + -> mkArrow (P.Aerasable, Some vd, atype, l, buildtype fargs) in buildtype fargs | _ -> (U.msg_error "TC" (lexp_location e) ===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -87,16 +87,14 @@ let rec unify (e1: lexp) (e2: lexp) unify' e1 e2 ctx OL.set_empty subst and unify' (e1: lexp) (e2: lexp) - (ctx : DB.lexp_context) (vs : OL.set_lexp) (subst: meta_subst) + (ctx : DB.lexp_context) (vs : OL.set_plexp) (subst: meta_subst) : return_type = let e1' = OL.lexp_whnf e1 ctx subst in let e2' = OL.lexp_whnf e2 ctx subst in - let stop1 = not (e1 == e1') && OL.set_member_p vs e1' in - let stop2 = not (e2 == e2') && OL.set_member_p vs e2' in - let vs' = if not (e1 == e1') && not stop1 then OL.set_add vs e1' - else if not (e2 == e2') && not stop2 then OL.set_add vs e2' - else vs in - match if stop1 || stop2 then (e1, e2) else (e1', e2') with + let changed = not (e1 == e1' && e2 == e2') in + if changed && OL.set_member_p subst vs e1' e2' then Some (subst, []) else + let vs' = if changed then OL.set_add vs e1' e2' else vs in + match (e1', e2') with | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _) | (Var _, Var _) | (Inductive _, Inductive _)) -> if OL.conv_p subst ctx e1' e2' then Some (subst, []) else None View it on GitLab: https://gitlab.com/monnier/typer/commit/8396dc22616f8cb9b6aa501a5a5d6ebfaa4…

1 0

[Git][monnier/typer][master] * src/lparse.ml: Rewrite "Built-in" as a special form
by Stefan 28 Nov '16

28 Nov '16

Stefan pushed to branch master at Stefan / Typer Commits: 43ddd912 by Stefan Monnier at 2016-11-28T13:31:18-05:00 * src/lparse.ml: Rewrite "Built-in" as a special form * src/lparse.ml (handle_funcall): Don't treat `Built-in` specially. (sform_built_in): New function. (special_forms): Use it. (default_lctx): Remove manual construction of "Built-in" builtin. - - - - - 1 changed file: - src/lparse.ml Changes: ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -787,28 +787,8 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = ^ "` to non-function (type = " ^ lexp_string ltp ^ ")") in let handle_funcall () = - (* Here we use lexp_whnf on actual code, but it's OK - * because we only use the result when it's a "predefined constant". *) - match OL.lexp_whnf body (ectx_to_lctx ctx) meta_ctx with - | Builtin((_, "Built-in"), _, _) (* FIXME: Should be a Special-Form! *) - -> ( - (* ------ SPECIAL ------ *) - match !_parsing_internals, sargs with - | true, [String (_, str); stp] -> - let ptp = pexp_parse stp in - let ltp, _ = infer ptp ctx in - mkBuiltin((loc, str), ltp, None), ltp - - | true, _ -> error loc "Wrong Usage of `Built-in`"; - dlxp, dltype - - | false, _ -> error loc "Use of `Built-in` in user code"; - dlxp, dltype) - - | e -> - (* Process Arguments. *) - let largs, ret_type = handle_fun_args [] sargs SMap.empty ltp in - mkCall (body, List.rev largs), ret_type in + let largs, ret_type = handle_fun_args [] sargs SMap.empty ltp in + mkCall (body, List.rev largs), ret_type in let handle_macro_call () = let sxp = match lexp_expand_macro body sargs ctx with @@ -1097,6 +1077,20 @@ let sform_decltype ctx loc sargs = | _ -> error loc "decltype expects one argument"; dlxp +let sform_built_in ctx loc sargs = + match !_parsing_internals, sargs with + | true, [String (_, str); stp] -> + let ptp = pexp_parse stp in + let ltp, _ = infer ptp ctx in + mkBuiltin((loc, str), ltp, None) + + | true, _ -> error loc "Wrong Usage of `Built-in`"; + dlxp + + | false, _ -> error loc "Use of `Built-in` in user code"; + dlxp + + (* Only print var info *) and lexp_print_var_info ctx = let ((m, _), env, _) = ctx in @@ -1118,6 +1112,7 @@ and lexp_print_var_info ctx = (* Register special forms. *) let _ = List.iter add_special_form [ + ("Built-in", sform_built_in); (* FIXME: We should add here `let_in_`, `case_`, etc... *) ("get-attribute", sform_get_attribute); ("new-attribute", sform_new_attribute); @@ -1140,9 +1135,6 @@ let default_lctx = -> if String.get key 0 = '-' then ctx else ctx_define ctx (dloc, key) e t) (!BI.lmap) lctx in - (* FIXME: Add builtins directly here. *) - let lxp = mkBuiltin((dloc, "Built-in"), DB.type0, None) in - let lctx = ctx_define lctx (dloc, "Built-in") lxp DB.type0 in (* Read BTL files *) let pres = prelex_file (!btl_folder ^ "builtins.typer") in View it on GitLab: https://gitlab.com/monnier/typer/commit/43ddd912b822ca553efc5ccdd2e59ea7aa9…

1 0

[Git][monnier/typer][master] * src/lparse.ml (special_forms): Remove last arg, move context 1st
by Stefan 28 Nov '16

28 Nov '16

Stefan pushed to branch master at Stefan / Typer Commits: 7535ecf7 by Stefan Monnier at 2016-11-28T13:23:40-05:00 * src/lparse.ml (special_forms): Remove last arg, move context 1st - - - - - 1 changed file: - src/lparse.ml Changes: ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -91,7 +91,7 @@ let global_substitution = ref (empty_meta_subst, []) (** Builtin Macros i.e, special forms. *) type special_forms_map = - (location -> sexp list -> elab_context -> lexp -> lexp) SMap.t + (elab_context -> location -> sexp list -> lexp) SMap.t let special_forms : special_forms_map ref = ref SMap.empty let type_special_form = BI.new_builtin_type "Special-Form" type0 @@ -749,7 +749,7 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = let default = Var((dloc, pname), pidx) in (* lookup default attribute of ltp *) - let attr = get_attribute loc [default; arg_type] ctx arg_type in + let attr = get_attribute ctx loc [default; arg_type] in (* FIXME: The `default` attribute table shouldn't contain elements of * type `Macro` but elements of type `something -> Sexp`. * The point of the `Macro` type is to be able to distinguish @@ -834,7 +834,7 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = match OL.lexp_whnf body (ectx_to_lctx ctx) meta_ctx with | Builtin ((_, name), _, _) -> (* Special form. *) - let e = (get_special_form loc name) loc sargs ctx ltp in + let e = (get_special_form loc name) ctx loc sargs in let meta_ctx, _ = !global_substitution in (* FIXME: We don't actually need to typecheck `e`, we just need * to find its type. *) @@ -1018,9 +1018,10 @@ and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp = let e, _ = infer (pexp_parse e) ctx in e (* -------------------------------------------------------------------------- - * Special form implementation + * Special forms implementation * -------------------------------------------------------------------------- *) -and new_attribute_impl loc sargs ctx ftype = + +and sform_new_attribute ctx loc sargs = let ltp = match sargs with | [t] -> lexp_parse_sexp ctx t | _ -> fatal loc "new-attribute expects a single Type argument" in @@ -1030,7 +1031,7 @@ and new_attribute_impl loc sargs ctx ftype = * instead. *) Builtin ((loc, "new-attribute"), ltp, Some AttributeMap.empty) -and add_attribute_impl loc (sargs : sexp list) ctx ftype = +and sform_add_attribute ctx loc (sargs : sexp list) = let n = get_size ctx in let table, var, attr = match List.map (lexp_parse_sexp ctx) sargs with | [table; Var((_, name), idx); attr] -> table, (n - idx, name), attr @@ -1045,7 +1046,7 @@ and add_attribute_impl loc (sargs : sexp list) ctx ftype = let table = AttributeMap.add var attr map in Builtin ((loc, "add-attribute"), attr_type, Some table) -and get_attribute loc largs ctx ftype = +and get_attribute ctx loc largs = let ctx_n = get_size ctx in let table, var = match largs with | [table; Var((_, name), idx)] -> table, (ctx_n - idx, name) @@ -1059,10 +1060,10 @@ and get_attribute loc largs ctx ftype = let lxp = AttributeMap.find var map in (lxp : lexp) -and get_attribute_impl loc (sargs : sexp list) ctx ftype = - get_attribute loc (List.map (lexp_parse_sexp ctx) sargs) ctx ftype +and sform_get_attribute ctx loc (sargs : sexp list) = + get_attribute ctx loc (List.map (lexp_parse_sexp ctx) sargs) -and has_attribute_impl loc (sargs : sexp list) ctx ftype = +and sform_has_attribute ctx loc (sargs : sexp list) = let n = get_size ctx in let table, var = match List.map (lexp_parse_sexp ctx) sargs with | [table; Var((_, name), idx)] -> table, (n - idx, name) @@ -1078,7 +1079,7 @@ and has_attribute_impl loc (sargs : sexp list) ctx ftype = with Not_found -> BI.get_predef "False" ctx -and declexpr_impl loc sargs ctx ftype = +and sform_declexpr ctx loc sargs = match List.map (lexp_parse_sexp ctx) sargs with | [Var((_, vn), vi)] -> (match DB.env_lookup_expr ctx ((loc, vn), vi) with @@ -1089,7 +1090,7 @@ and declexpr_impl loc sargs ctx ftype = dlxp -let decltype_impl loc sargs ctx ftype = +let sform_decltype ctx loc sargs = match List.map (lexp_parse_sexp ctx) sargs with | [Var((_, vn), vi)] -> DB.env_lookup_type ctx ((loc, vn), vi) @@ -1118,13 +1119,13 @@ and lexp_print_var_info ctx = let _ = List.iter add_special_form [ (* FIXME: We should add here `let_in_`, `case_`, etc... *) - ("get-attribute", get_attribute_impl); - ("new-attribute", new_attribute_impl); - ("has-attribute", has_attribute_impl); - ("add-attribute", add_attribute_impl); + ("get-attribute", sform_get_attribute); + ("new-attribute", sform_new_attribute); + ("has-attribute", sform_has_attribute); + ("add-attribute", sform_add_attribute); (* FIXME: These should be functions! *) - ("decltype", decltype_impl); - ("declexpr", declexpr_impl); + ("decltype", sform_decltype); + ("declexpr", sform_declexpr); ] (* Default context with builtin types View it on GitLab: https://gitlab.com/monnier/typer/commit/7535ecf78f40ddd3f69110531b41fb95a77…

1 0

[Git][monnier/typer][master] Change special forms's args to be sexps rather than lexps
by Stefan 28 Nov '16

28 Nov '16

Stefan pushed to branch master at Stefan / Typer Commits: 7443ad30 by Stefan Monnier at 2016-11-28T13:14:13-05:00 Change special forms's args to be sexps rather than lexps * src/builtin.ml (declexpr_impl, decltype_impl): Move to lparse.ml. * src/lparse.ml (special_forms_map): Rename from macromap. Change special forms's args to be sexps rather than lexps. Adjust all users accordingly. (lexp_parse_all): Rewrite using List.map. (lexp_parse_sexp): New function. - - - - - 2 changed files: - src/builtin.ml - src/lparse.ml Changes: ===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -168,30 +168,6 @@ let is_lbuiltin idx ctx = else false -let declexpr_impl loc largs ctx ftype = - - let (vi, vn) = match largs with - | [Var((_, vn), vi)] -> (vi, vn) - | _ -> error loc "declexpr expects one argument" in - - let lxp = match DB.env_lookup_expr ctx ((loc, vn), vi) with - | Some lxp -> lxp - | None -> error loc "no expr available" in - (* ltp and ftype should be the same - let ltp = env_lookup_type ctx ((loc, vn), vi) in *) - lxp - - -let decltype_impl loc largs ctx ftype = - - let (vi, vn) = match largs with - | [Var((_, vn), vi)] -> (vi, vn) - | _ -> error loc "decltype expects one argument" in - - let ltype = DB.env_lookup_type ctx ((loc, vn), vi) in - (* mkSusp prop (S.shift (var_i + 1)) *) - ltype - (* Map of lexp builtin elements accessible via (## <name>). *) let lmap = ref (SMap.empty : (L.lexp * L.ltype) SMap.t) ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -90,10 +90,10 @@ let value_fatal = debug_message fatal value_name value_string let global_substitution = ref (empty_meta_subst, []) (** Builtin Macros i.e, special forms. *) -type macromap = - (location -> lexp list -> elab_context -> lexp -> lexp) SMap.t +type special_forms_map = + (location -> sexp list -> elab_context -> lexp -> lexp) SMap.t -let special_forms : macromap ref = ref SMap.empty +let special_forms : special_forms_map ref = ref SMap.empty let type_special_form = BI.new_builtin_type "Special-Form" type0 let add_special_form (name, func) = @@ -749,7 +749,7 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = let default = Var((dloc, pname), pidx) in (* lookup default attribute of ltp *) - let attr = get_attribute_impl loc [default; arg_type] ctx arg_type in + let attr = get_attribute loc [default; arg_type] ctx arg_type in (* FIXME: The `default` attribute table shouldn't contain elements of * type `Macro` but elements of type `something -> Sexp`. * The point of the `Macro` type is to be able to distinguish @@ -834,9 +834,7 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = match OL.lexp_whnf body (ectx_to_lctx ctx) meta_ctx with | Builtin ((_, name), _, _) -> (* Special form. *) - let pargs = List.map pexp_parse sargs in - let largs = lexp_parse_all pargs ctx in - let e = (get_special_form loc name) loc largs ctx ltp in + let e = (get_special_form loc name) loc sargs ctx ltp in let meta_ctx, _ = !global_substitution in (* FIXME: We don't actually need to typecheck `e`, we just need * to find its type. *) @@ -1014,32 +1012,31 @@ and lexp_p_decls pdecls ctx: ((vdef * lexp * ltype) list list * elab_context) = decls :: declss, nnctx and lexp_parse_all (p: pexp list) (ctx: elab_context) : lexp list = + List.map (fun pe -> let e, _ = infer pe ctx in e) p - let rec loop (plst: pexp list) ctx (acc: lexp list) = - match plst with - | [] -> (List.rev acc) - | pe :: plst -> let lxp, _ = infer pe ctx in - (loop plst ctx (lxp::acc)) in - - (loop p ctx []) +and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp = + let e, _ = infer (pexp_parse e) ctx in e (* -------------------------------------------------------------------------- * Special form implementation * -------------------------------------------------------------------------- *) -and new_attribute_impl loc largs ctx ftype = - let ltp = match largs with - | [ltp] -> ltp +and new_attribute_impl loc sargs ctx ftype = + let ltp = match sargs with + | [t] -> lexp_parse_sexp ctx t | _ -> fatal loc "new-attribute expects a single Type argument" in + (* FIXME: This creates new values for type `ltp` (very wrong if `ltp` + * is False, for example): Should be a type like `AttributeMap t` + * instead. *) Builtin ((loc, "new-attribute"), ltp, Some AttributeMap.empty) -and add_attribute_impl loc largs ctx ftype = - let meta_ctx, _ = !global_substitution in +and add_attribute_impl loc (sargs : sexp list) ctx ftype = let n = get_size ctx in - let table, var, attr = match largs with + let table, var, attr = match List.map (lexp_parse_sexp ctx) sargs with | [table; Var((_, name), idx); attr] -> table, (n - idx, name), attr | _ -> fatal loc "add-attribute expects 3 arguments (table; var; attr)" in + let meta_ctx, _ = !global_substitution in let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) meta_ctx with | Builtin (_, attr_type, Some map)-> map, attr_type | _ -> fatal loc "add-attribute expects a table as first argument" in @@ -1048,13 +1045,13 @@ and add_attribute_impl loc largs ctx ftype = let table = AttributeMap.add var attr map in Builtin ((loc, "add-attribute"), attr_type, Some table) -and get_attribute_impl loc largs ctx ftype = - let meta_ctx, _ = !global_substitution in +and get_attribute loc largs ctx ftype = let ctx_n = get_size ctx in let table, var = match largs with | [table; Var((_, name), idx)] -> table, (ctx_n - idx, name) | _ -> fatal loc "get-attribute expects 2 arguments (table; var)" in + let meta_ctx, _ = !global_substitution in let map = match OL.lexp_whnf table (ectx_to_lctx ctx) meta_ctx with | Builtin (_, attr_type, Some map) -> map | _ -> fatal loc "get-attribute expects a table as first argument" in @@ -1062,13 +1059,16 @@ and get_attribute_impl loc largs ctx ftype = let lxp = AttributeMap.find var map in (lxp : lexp) -and has_attribute_impl loc largs ctx ftype = - let meta_ctx, _ = !global_substitution in +and get_attribute_impl loc (sargs : sexp list) ctx ftype = + get_attribute loc (List.map (lexp_parse_sexp ctx) sargs) ctx ftype + +and has_attribute_impl loc (sargs : sexp list) ctx ftype = let n = get_size ctx in - let table, var = match largs with + let table, var = match List.map (lexp_parse_sexp ctx) sargs with | [table; Var((_, name), idx)] -> table, (n - idx, name) | _ -> fatal loc "get-attribute expects 2 arguments (table; var)" in + let meta_ctx, _ = !global_substitution in let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) meta_ctx with | Builtin (_, attr_type, Some map) -> map, attr_type | lxp -> lexp_fatal loc lxp "get-attribute expects a table as first argument" in @@ -1078,6 +1078,24 @@ and has_attribute_impl loc largs ctx ftype = with Not_found -> BI.get_predef "False" ctx +and declexpr_impl loc sargs ctx ftype = + match List.map (lexp_parse_sexp ctx) sargs with + | [Var((_, vn), vi)] + -> (match DB.env_lookup_expr ctx ((loc, vn), vi) with + | Some lxp -> lxp + | None -> error loc "no expr available"; + dlxp) + | _ -> error loc "declexpr expects one argument"; + dlxp + + +let decltype_impl loc sargs ctx ftype = + match List.map (lexp_parse_sexp ctx) sargs with + | [Var((_, vn), vi)] + -> DB.env_lookup_type ctx ((loc, vn), vi) + | _ -> error loc "decltype expects one argument"; + dlxp + (* Only print var info *) and lexp_print_var_info ctx = let ((m, _), env, _) = ctx in @@ -1105,8 +1123,8 @@ let _ = List.iter add_special_form ("has-attribute", has_attribute_impl); ("add-attribute", add_attribute_impl); (* FIXME: These should be functions! *) - ("decltype", BI.decltype_impl); - ("declexpr", BI.declexpr_impl); + ("decltype", decltype_impl); + ("declexpr", declexpr_impl); ] (* Default context with builtin types View it on GitLab: https://gitlab.com/monnier/typer/commit/7443ad300f394133b6bcb8ca6544cb59892…

1 0

[Git][monnier/typer][master] Fix WHNF of Let and recognize negative integers
by Stefan 28 Nov '16

28 Nov '16

Stefan pushed to branch master at Stefan / Typer Commits: 1e05e7c1 by Stefan Monnier at 2016-11-28T11:42:57-05:00 Fix WHNF of Let and recognize negative integers * src/lexer.ml (nexttoken): Recognize negative integer. * src/opslexp.ml (lexp_whnf): Really return WHNF for `Let`. * tests/eval_test.ml ("Let"): Use negative integer, to test them. ("Lists"): Add tests using a different definition of List. - - - - - 3 changed files: - src/lexer.ml - src/opslexp.ml - tests/eval_test.ml Changes: ===================================== src/lexer.ml ===================================== --- a/src/lexer.ml +++ b/src/lexer.ml @@ -49,7 +49,11 @@ let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos | (Preblock (sl, bpts, el) :: pts) -> (Block (sl, bpts, el), pts, 0, 0) | (Prestring (loc, str) :: pts) -> (String (loc, str), pts, 0, 0) | (Pretoken ({file;line;column}, name) :: pts') - -> if digit_p name.[bpos] then + -> let char = name.[bpos] in + if digit_p char + || (char = '-' (* FIXME: Handle '+' as well! *) + && bpos + 1 < String.length name + && digit_p (name.[bpos + 1])) then let rec lexnum bp cp (np : num_part) = if bp >= String.length name then ((if np == NPint then ===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -63,6 +63,7 @@ let lookup_value = DB.lctx_lookup_value * `let x₂ = e₂ in e₂`) will be interpreted in the remaining context, * which already provides "x₁". *) +(* FXIME: This creates an O(N^2) tree from an O(N) `let`! *) let rec lexp_defs_subst l s defs = match defs with | [] -> s | (_, lexp, _) :: defs' @@ -138,7 +139,7 @@ let lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = (* FIXME: I'd really prefer to use "native" recursive substitutions, using * ideally a trick similar to the db_offsets in lexp_context! *) | Let (l, defs, body) - -> push_susp body (lexp_defs_subst l S.identity defs) + -> lexp_whnf (push_susp body (lexp_defs_subst l S.identity defs)) ctx | e -> e ===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -79,8 +79,8 @@ let _ = test_eval_eqv_named "c = 3; e = 1; f = 2; d = 4;" - "let a = 10; x = 50; y = 60; b = 20; - in a + b;" (* == *) "30" + "let a = -5; x = 50; y = 60; b = 20; + in a + b;" (* == *) "15" let _ = test_eval_eqv_named "Let2" @@ -246,7 +246,13 @@ let _ = test_eval_eqv_named "my_list = cons 1 (cons 2 (cons 3 - (cons 4 nil)))" + (cons 4 nil))); + List' = let L : Type -> Type; + L = inductive_ (L (a : Type)) (nil) (cons a (L a)) + in L; + cons' = inductive-cons List' cons; + nil' = inductive-cons List' nil; + my_list' = (cons' 1 nil');" "length my_list; head my_list; View it on GitLab: https://gitlab.com/monnier/typer/commit/1e05e7c18a4dd35979426187a063f82fdcd…

1 0

[Git][monnier/typer][master] Use ##... for types. Don't use `Macro` for special forms
by Stefan 28 Nov '16

28 Nov '16

Stefan pushed to branch master at Stefan / Typer Commits: 02dabd43 by Stefan Monnier at 2016-11-28T10:01:45-05:00 Use ##... for types. Don't use `Macro` for special forms * btl/unit.typer, btl/list.typer, btl/macro.typer: Remove, unused. * btl/builtins.typer: Rename from types.typer. (Unit): Define as inductive, rather than builtin. (unit): New predefined constant. (Int, Float, String, Sexp, Context, IO, FileHandle, Attribute): Remove built-in types, now declared in OCaml. (new-attribute, get-attribute, has-attribute, add-attribute, decltype) (declexpr): Remove special forms, now declared in OCaml. * src/builtin.ml (predef_name): Remove "Attribute", unused. (add_builtin_type): New function. Add all builtin sorts and types. * src/debruijn.ml (sort_level): Rename from type_level. (sort_omega): Rename from type_omega. (type_level): New type. * src/lparse.ml (macromap): Move. (special_forms): Rename from make_macro_map; make it a ref cell rather than a function of no arguments. (type_special_form): New built-in type. (add_special_form): New function. (get_special_form): Rename from get_macro_impl, rewrite. (infer_call.handle_funcall): Use mkBuiltin. Remove the single-arg form of `Built-in`. (infer_call): Don't use the `Macro` to indicate a special form. (builtin_macro, is_builtin_macro): Remove. (<toplevel>): Register special forms. (default_lctx): Add entries predefined in BI.lmap. before loading types.typer. * src/opslexp.ml (conv_p) <Inductive>: Fix scoping of fields. (sort_level_max): Hash-cons return value. (check'): Check the type provided to `Builtin`. Hash cons the sorts as well. (erase_type): Silence compiler warning. - - - - - 9 changed files: - btl/types.typer → btl/builtins.typer - − btl/list.typer - − btl/macro.typer - − btl/unit.typer - src/builtin.ml - src/debruijn.ml - src/lexp.ml - src/lparse.ml - src/opslexp.ml Changes: ===================================== btl/types.typer → btl/builtins.typer ===================================== --- a/btl/types.typer +++ b/btl/builtins.typer @@ -35,13 +35,8 @@ % Base Types % ----------------------------------------------------- -Int = Built-in "Int"; -Float = Built-in "Float"; -String = Built-in "String"; -Sexp = Built-in "Sexp"; - -Unit = Built-in "Unit"; % Nothing -Context = Built-in "Context"; % Lexp Context +Unit = inductive_ Unit unit; +unit = inductive-cons Unit unit; % Basic operators _+_ = Built-in "_+_" (Int -> Int -> Int); @@ -145,8 +140,6 @@ sexp_dispatch_ = Built-in "sexp_dispatch_" ( % Monads % ----------------------------------------------------- -IO = Built-in "IO" (Type -> Type); - % Builtin bind bind = Built-in "bind" ( (a : Type) ≡> @@ -157,9 +150,6 @@ bind = Built-in "bind" ( % File monad -% define a dummy type that supposed to represent a file -FileHandle = Built-in "FileHandle"; - %% `runIO` should have type IO Unit -> b -> b %% or IO a -> b -> b, which means "run the IO, throw away the result, %% and then return the second argument unchanged". The "dummy" b argument @@ -172,29 +162,3 @@ run-io = Built-in "run-io" ((a : Type) ≡> IO Unit -> a -> a); open = Built-in "open" (String -> String -> IO FileHandle); write = Built-in "write" (FileHandle -> String -> IO Unit); read = Built-in "read" (FileHandle -> Int -> IO String); - -% ----------------------------------------------------- -% Attributes -% ----------------------------------------------------- - -% Despite being typed as macro those actually returns lexp. -% not that it matters for the end user -Attribute = Built-in "Attribute"; -new-attribute = Built-in "new-attribute" Macro; -get-attribute = Built-in "get-attribute" Macro; -has-attribute = Built-in "has-attribute" Macro; -add-attribute = Built-in "add-attribute" Macro; - -% attribute = Macro_ add-attribute; - -% ----------------------------------------------------- -% Context Accessors -% ----------------------------------------------------- - -%% FIXME: These should be functions! -decltype = Built-in "decltype" Macro; -declexpr = Built-in "declexpr" Macro; - - - - ===================================== btl/list.typer deleted ===================================== --- a/btl/list.typer +++ /dev/null @@ -1,26 +0,0 @@ -List : Type -> Type; -List = inductive_ (dList (a : Type)) (nil) (cons a (List a)); - -nil = inductive-cons List nil; -cons = inductive-cons List cons; - -length : (a : Type) => List a -> Int; -length = lambda a => - lambda xs -> - case xs - | nil => 0 - | cons hd tl => (1 + length tl); - -head : (a : Type) => List a -> a; -head = lambda a => - lambda xs -> - case xs - | nil => nil - | cons hd tl => hd; - -tail : (a : Type) => List a -> List a; -tail = lambda a => - lambda xs -> - case xs - | nil => nil - | cons hd tl => tl; ===================================== btl/macro.typer deleted ===================================== --- a/btl/macro.typer +++ /dev/null @@ -1,36 +0,0 @@ - - -block_ : (List Sexp) -> Sexp; -block_ = Built-in block_; - -symbol_ : String -> Sexp; -symbol_ = Built-in symbol_; - -string_ : String -> Sexp; -string_ = Built-in string_; - -node_ : (List Sexp) -> Sexp; -node_ = Built-in node_; - -integer_ : Int -> Sexp; -integer_ = Built-in integer_; - -Macro : Type; -Macro = inductive_ (dMacro) (Macro_ Type); -Macro_ = inductive-cons Macro Macro_; - - -%% Basic usage -% -% sqr = (Macro_ -% (node_ (symbol_ "lambda_->_") (symbol "x") -% (node_ "_*_" (symbol "x") (symbol "x")))); -% -% (sqr 4); % <=> 4 * 4 -% -% -%% Using Quasi Quote ` -% -% sqr = (Macro_ (qq (lambda x -> ,x * ,x))); -% -% (sqr 4); % <=> 4 * 4 ===================================== btl/unit.typer deleted ===================================== --- a/btl/unit.typer +++ /dev/null @@ -1,5 +0,0 @@ - -% Declare a dummy Type -Unit : Type; -Unit = inductive_ (Unit) (unit); -unit = inductive-cons Unit unit; ===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -79,7 +79,6 @@ let predef_name = [ "Macro"; "expand_macro_"; "expand_dmacro_"; - "Attribute"; ] let default_predef_map : predef_table = @@ -201,3 +200,22 @@ let add_builtin_cst (name : string) (e : lexp) assert (not (SMap.mem name map)); let t = OL.check VMap.empty Myers.nil e in lmap := SMap.add name (e, t) map + +let new_builtin_type name kind = + let t = mkBuiltin ((dloc, name), kind, None) in + add_builtin_cst name t; + t + +let builtins = + add_builtin_cst "TypeLevel" DB.type_level; + add_builtin_cst "TypeLevel.z" DB.level0; + add_builtin_cst "Type" DB.type0; + add_builtin_cst "Type1" DB.type1; + add_builtin_cst "Int" DB.type_int; + add_builtin_cst "Float" DB.type_float; + add_builtin_cst "String" DB.type_string + +let _ = new_builtin_type "Sexp" DB.type0 +let _ = new_builtin_type + "IO" (Arrow (Aexplicit, None, DB.type0, dloc, DB.type0)) +let _ = new_builtin_type "FileHandle" DB.type0 ===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -79,14 +79,15 @@ let warning = msg_warning "DEBRUIJN" * ---------------------------------- *) let dloc = dummy_location +let sort_level = mkSort (dloc, StypeLevel) +let sort_omega = mkSort (dloc, StypeOmega) +let type_level = mkBuiltin ((dloc, "TypeLevel"), sort_level, None) let level0 = mkSortLevel SLz let level1 = mkSortLevel (SLsucc level0) let level2 = mkSortLevel (SLsucc level1) let type0 = mkSort (dloc, Stype level0) let type1 = mkSort (dloc, Stype level1) let type2 = mkSort (dloc, Stype level2) -let type_level = mkSort (dloc, StypeLevel) -let type_omega = mkSort (dloc, StypeOmega) let type_int = mkBuiltin ((dloc, "Int"), type0, None) let type_float = mkBuiltin ((dloc, "Float"), type0, None) let type_string = mkBuiltin ((dloc, "String"), type0, None) @@ -291,7 +292,8 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = ret) with Not_found -> error loc ("DeBruijn index " - ^ string_of_int dbi ^ " out of bounds!") + ^ string_of_int dbi ^ " of `" ^ ename + ^ "` out of bounds!") ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -658,9 +658,9 @@ and _lexp_to_str ctx exp = | Sort (_, Stype (SortLevel SLz)) -> "##Type" | Sort (_, Stype (SortLevel (SLsucc (SortLevel SLz)))) -> "##Type1" - | Sort (_, StypeLevel) -> "##TypeLevel" + | Sort (_, StypeLevel) -> "##Type_ℓ" | Sort (_, Stype _) -> "##Type_?" (* FIXME! *) - | Sort (_, StypeOmega) -> "##Type_ω" (* FIXME: Should never happen! *) + | Sort (_, StypeOmega) -> "##Type_ω" | SortLevel (SLz) -> "##TypeLevel.z" | SortLevel (SLsucc e) -> "##TypeLevel.succ" ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -89,6 +89,22 @@ let value_fatal = debug_message fatal value_name value_string (* :-( *) let global_substitution = ref (empty_meta_subst, []) +(** Builtin Macros i.e, special forms. *) +type macromap = + (location -> lexp list -> elab_context -> lexp -> lexp) SMap.t + +let special_forms : macromap ref = ref SMap.empty +let type_special_form = BI.new_builtin_type "Special-Form" type0 + +let add_special_form (name, func) = + BI.add_builtin_cst name (mkBuiltin ((dloc, name), type_special_form, None)); + special_forms := SMap.add name func (!special_forms) + +let get_special_form loc name = + try SMap.find name (!special_forms) + with Not_found -> fatal loc ("Special form `" ^ name ^ "` not found!") + + (* The prefix `elab_check_` is used for functions which do internal checking * (i.e. errors signalled here correspond to internal errors rather than * to errors in the user's code). *) @@ -112,10 +128,6 @@ let elab_check_sort (ctx : elab_context) lsort var ltp = ("Type of `" ^ name ^ "` is not a proper type: " ^ typestr) -(* Builtin Macro i.e, special forms *) -type macromap = - (location -> lexp list -> elab_context -> lexp -> lexp) SMap.t - let elab_check_proper_type (ctx : elab_context) ltp var = let meta_ctx, _ = !global_substitution in try elab_check_sort ctx (OL.check meta_ctx (ectx_to_lctx ctx) ltp) var ltp @@ -778,17 +790,14 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = (* Here we use lexp_whnf on actual code, but it's OK * because we only use the result when it's a "predefined constant". *) match OL.lexp_whnf body (ectx_to_lctx ctx) meta_ctx with - | Builtin((_, "Built-in"), _, _) + | Builtin((_, "Built-in"), _, _) (* FIXME: Should be a Special-Form! *) -> ( (* ------ SPECIAL ------ *) match !_parsing_internals, sargs with - | true, [String (_, str)] -> - Builtin((loc, str), ltp, None), ltp - | true, [String (_, str); stp] -> let ptp = pexp_parse stp in let ltp, _ = infer ptp ctx in - Builtin((loc, str), ltp, None), ltp + mkBuiltin((loc, str), ltp, None), ltp | true, _ -> error loc "Wrong Usage of `Built-in`"; dlxp, dltype @@ -815,31 +824,32 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = infer pxp ctx in (* This is the builtin Macro type *) - let macro_type, macro_disp = match BI.get_predef_option "Macro" ctx with - | Some lxp -> OL.lexp_whnf lxp (ectx_to_lctx ctx) meta_ctx, true + let macro_type = match BI.get_predef_option "Macro" ctx with + | Some lxp -> OL.lexp_whnf lxp (ectx_to_lctx ctx) meta_ctx (* When type.typer is being parsed and the predef is not yet available *) - | None -> dltype, false in + | None -> impossible in (* determine function type *) - match func, ltp with - | macro, _ when (macro_disp - && OL.conv_p meta_ctx (ectx_to_lctx ctx) - ltp macro_type) -> ( - match macro with - | Pvar(l, name) when is_builtin_macro name -> - let pargs = List.map pexp_parse sargs in - let largs = lexp_parse_all pargs ctx in - let e = (get_macro_impl loc name) loc largs ctx ltp in - let meta_ctx, _ = !global_substitution in - (* FIXME: We don't actually need to typecheck `e`, we just need - * to find its type. *) - (e, OL.check meta_ctx (ectx_to_lctx ctx) e) - - (* true macro *) - | _ -> handle_macro_call ()) - - (* FIXME: Handle special-forms here as well! *) - | _ -> handle_funcall () + if (OL.conv_p meta_ctx (ectx_to_lctx ctx) ltp type_special_form) then + match OL.lexp_whnf body (ectx_to_lctx ctx) meta_ctx with + | Builtin ((_, name), _, _) -> + (* Special form. *) + let pargs = List.map pexp_parse sargs in + let largs = lexp_parse_all pargs ctx in + let e = (get_special_form loc name) loc largs ctx ltp in + let meta_ctx, _ = !global_substitution in + (* FIXME: We don't actually need to typecheck `e`, we just need + * to find its type. *) + (e, OL.check meta_ctx (ectx_to_lctx ctx) e) + + | _ -> lexp_error loc body ("Unknown special-form: " + ^ lexp_string body); + let t = newMetatype () in + (newMetavar loc "<dummy>" t, t) + else if (OL.conv_p meta_ctx (ectx_to_lctx ctx) ltp macro_type) then + handle_macro_call () + else + handle_funcall () (* Parse inductive type definition. *) and lexp_parse_inductive ctors ctx = @@ -890,22 +900,10 @@ and lexp_expand_macro_ macro_funct sargs ctx expand_fun : value_type = vxp and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = - try (* Lookup macro declaration *) - let idx = senv_lookup mname ctx in - (* FIXME: We should only check that `ltp` is Macro, and not look - * at `lxp` here (just like we do for expression macros). *) - let ltp = env_lookup_type ctx ((loc, mname), idx) in - let lxp = env_lookup_expr ctx ((loc, mname), idx) in - - (* lxp has the form (Call (Var(_, "Macro_"), [(_, function)])) - * We need the function so we can call it later *) - let body, mfun = match lxp with - | Some (Call(_, [(_, lxp)]) as e) -> e, lxp - | Some lxp -> lxp, lxp - | None -> fatal loc "expression does not exist" in - - (* Special Form *) - let ret = lexp_expand_dmacro body sargs ctx in + try let lxp, ltp = infer (Pvar (loc, mname)) ctx in + + (* FIXME: Check that (conv_p ltp Macro)! *) + let ret = lexp_expand_dmacro lxp sargs ctx in (* convert typer list to ocaml *) let decls = BI.tlist2olist [] ret in @@ -1017,39 +1015,13 @@ and lexp_p_decls pdecls ctx: ((vdef * lexp * ltype) list list * elab_context) = and lexp_parse_all (p: pexp list) (ctx: elab_context) : lexp list = - let rec loop (plst: pexp list) ctx (acc: lexp list) = - match plst with - | [] -> (List.rev acc) - | pe :: plst -> let lxp, _ = infer pe ctx in + let rec loop (plst: pexp list) ctx (acc: lexp list) = + match plst with + | [] -> (List.rev acc) + | pe :: plst -> let lxp, _ = infer pe ctx in (loop plst ctx (lxp::acc)) in - - (loop p ctx []) - -(* -------------------------------------------------------------------------- - * Built-in Macro: i.e special forms - * -------------------------------------------------------------------------- *) -and builtin_macro = [ - (* FIXME: These should be functions! *) - ("decltype", BI.decltype_impl); - ("declexpr", BI.declexpr_impl); - (* FIXME: These are not macros but `special-forms`. - * We should add here `let_in_`, `case_`, etc... *) - ("get-attribute", get_attribute_impl); - ("new-attribute", new_attribute_impl); - ("has-attribute", has_attribute_impl); - ("add-attribute", add_attribute_impl); -] - -and make_macro_map unit : macromap = - List.fold_left (fun map (name, funct) -> - SMap.add name funct map) SMap.empty builtin_macro - -and get_macro_impl loc name = - try SMap.find name (make_macro_map ()) - with Not_found -> fatal loc ("Builtin macro" ^ name ^ " not found") - -and is_builtin_macro name = - SMap.mem name (make_macro_map ()) + + (loop p ctx []) (* -------------------------------------------------------------------------- * Special form implementation @@ -1124,22 +1096,37 @@ and lexp_print_var_info ctx = print_string "\n") done +(* Register special forms. *) +let _ = List.iter add_special_form + [ + (* FIXME: We should add here `let_in_`, `case_`, etc... *) + ("get-attribute", get_attribute_impl); + ("new-attribute", new_attribute_impl); + ("has-attribute", has_attribute_impl); + ("add-attribute", add_attribute_impl); + (* FIXME: These should be functions! *) + ("decltype", BI.decltype_impl); + ("declexpr", BI.declexpr_impl); + ] + (* Default context with builtin types * --------------------------------------------------------- *) (* Make lxp context with built-in types *) -let default_lctx, default_rctx = +let default_lctx = (* Empty context *) let lctx = make_elab_context in - let lctx = ctx_define lctx (dloc, "Type1") DB.type1 DB.type2 in - let lctx = ctx_define lctx (dloc, "Type") DB.type0 DB.type1 in + let lctx = SMap.fold (fun key (e, t) ctx + -> if String.get key 0 = '-' then ctx + else ctx_define ctx (dloc, key) e t) + (!BI.lmap) lctx in (* FIXME: Add builtins directly here. *) - let lxp = Builtin((dloc, "Built-in"), DB.type0, None) in + let lxp = mkBuiltin((dloc, "Built-in"), DB.type0, None) in let lctx = ctx_define lctx (dloc, "Built-in") lxp DB.type0 in (* Read BTL files *) - let pres = prelex_file (!btl_folder ^ "types.typer") in + let pres = prelex_file (!btl_folder ^ "builtins.typer") in let sxps = lex default_stt pres in let nods = sexp_parse_all_to_list default_grammar sxps (Some ";") in let pxps = pexp_decls_all nods in @@ -1167,7 +1154,9 @@ let default_lctx, default_rctx = with e -> warning dloc "Predef not found"; lctx in - lctx, from_lctx lctx + lctx + +let default_rctx = from_lctx default_lctx (* String Parsing * --------------------------------------------------------- *) ===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -207,16 +207,7 @@ let rec conv_p' meta_ctx (ctx : DB.lexp_context) (vs : set_lexp) e1 e2 : bool = true args1 args2 in conv_p f1 f2 && conv_arglist_p args1 args2 | (Inductive (_, l1, args1, cases1), Inductive (_, l2, args2, cases2)) - -> let rec conv_args ctx vs args1 args2 = - match args1, args2 with - | ([], []) -> true - | ((ak1,l1,t1)::args1, (ak2,l2,t2)::args2) - -> ak1 == ak2 && conv_p' ctx vs t1 t2 - && conv_args (DB.lexp_ctx_cons ctx 0 (Some l1) Variable t1) - (set_shift vs) - args1 args2 - | _,_ -> false in - let rec conv_fields ctx vs fields1 fields2 = + -> let rec conv_fields ctx vs fields1 fields2 = match fields1, fields2 with | ([], []) -> true | ((ak1,vd1,t1)::fields1, (ak2,vd2,t2)::fields2) @@ -225,8 +216,19 @@ let rec conv_p' meta_ctx (ctx : DB.lexp_context) (vs : set_lexp) e1 e2 : bool = (set_shift vs) fields1 fields2 | _,_ -> false in + let rec conv_args ctx vs args1 args2 = + match args1, args2 with + | ([], []) -> + (* Args checked alright, now go on with the fields, + * using the new context. *) + SMap.equal (conv_fields ctx vs) cases1 cases2 + | ((ak1,l1,t1)::args1, (ak2,l2,t2)::args2) + -> ak1 == ak2 && conv_p' ctx vs t1 t2 + && conv_args (DB.lexp_ctx_cons ctx 0 (Some l1) Variable t1) + (set_shift vs) + args1 args2 + | _,_ -> false in l1 == l2 && conv_args ctx vs' args1 args2 - && SMap.equal (conv_fields ctx vs') cases1 cases2 | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> l1 = l2 && conv_p t1 t2 (* FIXME: Various missing cases, such as Case. *) | (_, _) -> false @@ -237,18 +239,17 @@ let conv_p meta_ctx (ctx : DB.lexp_context) e1 e2 (********* Testing if a lexp is properly typed *********) - let rec sort_level_max l1 l2 = match nosusp l1, nosusp l2 with | SortLevel SLz, l2 -> l2 | l1, SortLevel SLz -> l1 | SortLevel (SLsucc l1), SortLevel (SLsucc l2) - -> SortLevel (SLsucc (sort_level_max l1 l2)) + -> mkSortLevel (SLsucc (sort_level_max l1 l2)) | _, _ (* FIXME: This requires s.th. like `SLmax of lexp * lexp`! *) -> U.msg_error "TC" (lexp_location l1) ("Can't compute the max of levels `" ^ lexp_string l1 ^ "` and `" ^ lexp_string l2 ^ "`"); - SortLevel SLz + mkSortLevel SLz let sort_compose l s1 s2 = match s1, s2 with @@ -295,25 +296,25 @@ let rec check' meta_ctx erased ctx e = | SortLevel (SLsucc e) -> let t = check erased ctx e in assert_type ctx e t DB.type_level; - (* FIXME: typelevel vs typelevelsort !? *) DB.type_level | Sort (l, Stype e) -> let t = check erased ctx e in assert_type ctx e t DB.type_level; Sort (l, Stype (SortLevel (SLsucc e))) - | Sort (_, StypeLevel) -> DB.type_omega + | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) - -> (U.msg_error "TC" (lexp_location e) "Reached Unreachable sort!"; - U.internal_error "Reached Unreachable sort!"; - DB.type_omega) - | Builtin (_, t, _) -> t + -> (U.msg_error "TC" (lexp_location e) "Reached unreachable sort!"; + (* U.internal_error "Reached unreachable sort!"; *) + DB.sort_omega) + | Builtin (_, t, _) + -> check_type DB.set_empty ctx t; (* FIXME: Use an empty ctx? *) + t (* FIXME: Check recursive references. *) | Var (((_, name), idx) as v) -> if DB.set_mem idx erased then U.msg_error "TC" (lexp_location e) ("Var `" ^ name ^ "`" - ^ " can't be used here, because it's `erasable`") - else if name = "erased" then U.internal_error "WOWO!"; + ^ " can't be used here, because it's `erasable`"); lookup_type ctx v | Susp (e, s) -> check erased ctx (push_susp e s) | Let (l, defs, e) @@ -411,7 +412,7 @@ let rec check' meta_ctx erased ctx e = (level, ctx) case in level) - cases (SortLevel SLz) in + cases (mkSortLevel SLz) in Sort (l, Stype level) | (ak, v, t)::args -> Arrow (ak, Some v, t, lexp_location t, @@ -477,7 +478,7 @@ let rec check' meta_ctx erased ctx e = ret | Cons (t, (_, name)) -> (match lexp_whnf t ctx meta_ctx with - | Inductive (l, _, fargs, constructors) as it + | Inductive (l, _, fargs, constructors) -> let fieldtypes = SMap.find name constructors in let rec indtype fargs start_index = match fargs with @@ -541,6 +542,7 @@ let rec erase_type (lxp: L.lexp): E.elexp = | L.Sort _ -> E.Type (* Still useful to some extent. *) | L.Inductive(l, label, _, _) -> E.Inductive(l, label) + | L.Metavar _ -> U.internal_error "Metavar in erase_type" and filter_arg_list lst = let rec filter_arg_list lst acc = View it on GitLab: https://gitlab.com/monnier/typer/commit/02dabd43b7f858775ac587cfdca1d71298f…

1 0

[Git][monnier/typer][master] Add new ##... syntax to refer to existing builtins
by Stefan 26 Nov '16

26 Nov '16

Stefan pushed to branch master at Stefan / Typer Commits: f9a5b2f2 by Stefan Monnier at 2016-11-26T11:23:49-05:00 Add new ##... syntax to refer to existing builtins * src/builtin.ml (lmap): New var. (add_builtin_cst): New function. * src/lexp.ml (mkSusp): Don't bother suspending immediates. (lexp_unparse): Use Pbuiltin. (_lexp_to_str): Use the ##... syntax. * src/lparse.ml (macromap): Adjust to earlier change. (make_macro_map): Use it. (infer): Handle Pbuiltin. * src/pexp.ml (pexp): Add Pbuiltin constructor. (pexp_parse): Recognize new ##... syntax. (pexp_location, pexp_unparse): Handle it. * src/prelexer.ml (string_sub): Move to util.ml. - - - - - 8 changed files: - DESIGN - src/builtin.ml - src/lexp.ml - src/lparse.ml - src/pexp.ml - src/prelexer.ml - src/util.ml - tests/eval_test.ml Changes: ===================================== DESIGN ===================================== --- a/DESIGN +++ b/DESIGN @@ -1219,22 +1219,30 @@ For IO the macro would return "bind e1 e2", whereas for "a * b" it would use Here's an example of a use of partial functions: - type Exp (e : Env) := - Var i (t : lookup i e) + type Exp (e : Env) + | Var i (t : lookup i e) where "lookup" might fail. Without partial functions, we have to use a relational style, as in: - type Exp (e : Env) := - Var i (_: lookup i e t) t + type Exp (e : Env) + | Var i (_: lookup i e t) t In the present case, we could make "lookup" return False, but if we change it to: - type Exp (e : Env) (τ : EType) := - SetVar i (v : Exp Env (lookup i e)) + type Exp (e : Env) (τ : EType) + | SetVar i (v : Exp Env (lookup i e)) -Suddenly, this doesn't work any more. +Suddenly, this doesn't work any more. We would then have to do something +like, have `lookup` return an `Option` and then do: + + type Exp (e : Env) (τ : EType) + | SetVar i (v : (case lookup i e + | Some t => Exp Env t + | None -> False)) + +It would be neat to have some way to "automate" this. * Erasable constructors ===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -1,9 +1,6 @@ -(* - * Typer Compiler +(* builtin.ml --- Infrastructure to define built-in primitives * - * --------------------------------------------------------------------------- - * - * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * Copyright (C) 2016 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -25,8 +22,34 @@ * * --------------------------------------------------------------------------- * - * Description: - * Hold built-in types definition and built-in functions implementation + * There are several different issues with how to make the compiler's code + * interact with code defined in Typer: + * + * ** Exporting primitives + * + * I.e. how to give a name and a type to a primitive implemented in OCaml + * + * There are several conflicting desires, here: we'd generally want the name, + * the type (and the association) to be close to the primitive's definition, so + * that adding a new primitive doesn't require changes in many files. + * + * But it's also good to have the type written in some Typer file, both for + * the convenience of writing the code in Typer syntax with typer-mode support, + * and also because error messages can easily refer to that file, so it can be + * used for user-documentation. + * + * ** Importing definitions + * + * Sometimes we want some part of the core to be defined in Typer and used + * from OCaml. Examples are the type `Macro` along with the `expand-macro` + * function or the type Bool/true/false used with various primitives. + * + * ** Intertwined dependencies + * + * The various importing/exporting might need to be interlaced. Some exported + * functions's types will want to refer to imported types, while some imported + * definitions may want to refer to exported definitions. So we'd like to be + * able to do them in "any" order. * * ---------------------------------------------------------------------------*) @@ -34,6 +57,8 @@ open Util open Sexp (* Integer/Float *) open Pexp (* arg_kind *) +module L = Lexp +module OL = Opslexp open Lexp module DB = Debruijn @@ -168,9 +193,11 @@ let decltype_impl loc largs ctx ftype = (* mkSusp prop (S.shift (var_i + 1)) *) ltype +(* Map of lexp builtin elements accessible via (## <name>). *) +let lmap = ref (SMap.empty : (L.lexp * L.ltype) SMap.t) - - - - - +let add_builtin_cst (name : string) (e : lexp) + = let map = !lmap in + assert (not (SMap.mem name map)); + let t = OL.check VMap.empty Myers.nil e in + lmap := SMap.add name (e, t) map ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -166,6 +166,8 @@ let rec mkSusp e s = * There's no deep technical rason for that: * it just seemed like a good idea to do it eagerly when it's easy. *) match e with + (* FIXME: `Builtin` shouuld be treated like `Imm`. *) + | Imm _ -> e | Susp (e, s') -> mkSusp e (scompose s' s) | Var (l,v) -> slookup s l v | Metavar (vn, s', vd, t) -> mkMetavar (vn, scompose s' s, vd, mkSusp t s) @@ -349,10 +351,7 @@ let rec lexp_unparse lxp = match lxp with | Susp _ as e -> lexp_unparse (nosusp e) | Imm (sexp) -> Pimm (sexp) - | Builtin ((loc, name), _, None) -> Pvar((loc, name)) - | Builtin ((loc, name), ltp, _ ) - -> Pcall(Pvar((loc, name)), [pexp_unparse (lexp_unparse ltp)]) - + | Builtin (s, _, _) -> Pbuiltin s | Var ((loc, name), _) -> Pvar((loc, name)) | Cons (t, ctor) -> Pcons (lexp_unparse t, ctor) | Lambda (kind, vdef, ltp, body) -> @@ -655,15 +654,16 @@ and _lexp_to_str ctx exp = ^ "| " ^ (match v with None -> "_" | Some (_,name) -> name) ^ " => " ^ (lexp_to_stri 1 df)) - | Builtin ((_, name), _, _) -> name + | Builtin ((_, name), _, _) -> "##" ^ name - | Sort (_, Stype (SortLevel SLz)) -> "Type_0" - | Sort (_, Stype _) -> "Type_?" - | Sort (_, StypeOmega) -> "Type_ω" - | Sort (_, StypeLevel) -> "Type_Level" + | Sort (_, Stype (SortLevel SLz)) -> "##Type" + | Sort (_, Stype (SortLevel (SLsucc (SortLevel SLz)))) -> "##Type1" + | Sort (_, StypeLevel) -> "##TypeLevel" + | Sort (_, Stype _) -> "##Type_?" (* FIXME! *) + | Sort (_, StypeOmega) -> "##Type_ω" (* FIXME: Should never happen! *) - | SortLevel (SLz) -> "<Level0>" - | SortLevel (SLsucc e) -> "<LevelS?>" + | SortLevel (SLz) -> "##TypeLevel.z" + | SortLevel (SLsucc e) -> "##TypeLevel.succ" and lexp_str_ctor ctx ctors = SMap.fold (fun key value str ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -43,10 +43,11 @@ open Lexp open Env open Debruijn +module DB = Debruijn open Eval open Grammar -open Builtin +module BI = Builtin module Unif = Unification @@ -113,7 +114,7 @@ let elab_check_sort (ctx : elab_context) lsort var ltp = (* Builtin Macro i.e, special forms *) type macromap = - (location -> lexp list -> elab_context -> lexp -> (lexp * lexp)) SMap.t + (location -> lexp list -> elab_context -> lexp -> lexp) SMap.t let elab_check_proper_type (ctx : elab_context) ltp var = let meta_ctx, _ = !global_substitution in @@ -247,6 +248,12 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = | _ -> pexp_error tloc p "Could not find type"; dltype) + | Pbuiltin (l,name) + -> (try SMap.find name (! BI.lmap) + with Not_found + -> pexp_error l p ("Unknown builtin `" ^ name ^ "`"); + dlxp, dltype) + (* Symbol i.e identifier. *) | Pvar (loc, name) -> (try @@ -808,7 +815,7 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = infer pxp ctx in (* This is the builtin Macro type *) - let macro_type, macro_disp = match get_predef_option "Macro" ctx with + let macro_type, macro_disp = match BI.get_predef_option "Macro" ctx with | Some lxp -> OL.lexp_whnf lxp (ectx_to_lctx ctx) meta_ctx, true (* When type.typer is being parsed and the predef is not yet available *) | None -> dltype, false in @@ -867,9 +874,9 @@ and lexp_expand_dmacro macro_funct sargs ctx and lexp_expand_macro_ macro_funct sargs ctx expand_fun : value_type = (* Build the function to be called *) - let macro_expand = get_predef expand_fun ctx in + let macro_expand = BI.get_predef expand_fun ctx in let args = [(Aexplicit, macro_funct); - (Aexplicit, (olist2tlist_lexp sargs ctx))] in + (Aexplicit, (BI.olist2tlist_lexp sargs ctx))] in let macro = mkCall (macro_expand, args) in let emacro = OL.erase_type macro in @@ -901,7 +908,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = let ret = lexp_expand_dmacro body sargs ctx in (* convert typer list to ocaml *) - let decls = tlist2olist [] ret in + let decls = BI.tlist2olist [] ret in (* extract sexp from result *) let decls = List.map (fun g -> @@ -1023,8 +1030,8 @@ and lexp_parse_all (p: pexp list) (ctx: elab_context) : lexp list = * -------------------------------------------------------------------------- *) and builtin_macro = [ (* FIXME: These should be functions! *) - ("decltype", decltype_impl); - ("declexpr", declexpr_impl); + ("decltype", BI.decltype_impl); + ("declexpr", BI.declexpr_impl); (* FIXME: These are not macros but `special-forms`. * We should add here `let_in_`, `case_`, etc... *) ("get-attribute", get_attribute_impl); @@ -1033,7 +1040,7 @@ and builtin_macro = [ ("add-attribute", add_attribute_impl); ] -and make_macro_map unit = +and make_macro_map unit : macromap = List.fold_left (fun map (name, funct) -> SMap.add name funct map) SMap.empty builtin_macro @@ -1095,9 +1102,9 @@ and has_attribute_impl loc largs ctx ftype = | lxp -> lexp_fatal loc lxp "get-attribute expects a table as first argument" in try let _ = AttributeMap.find var map in - (get_predef "True" ctx) + BI.get_predef "True" ctx with Not_found -> - (get_predef "False" ctx) + BI.get_predef "False" ctx (* Only print var info *) and lexp_print_var_info ctx = @@ -1154,7 +1161,7 @@ let default_lctx, default_rctx = List.iter (fun name -> let idx = senv_lookup name lctx in let v = Var((dloc, name), idx) in - set_predef name (Some v)) predef_name; + BI.set_predef name (Some v)) BI.predef_name; (* -- DONE -- *) lctx with e -> ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -39,6 +39,7 @@ type pvar = symbol type pexp = (* | Psort of location * sort *) | Pimm of sexp (* Used for strings, ... *) + | Pbuiltin of symbol | Pvar of pvar | Phastype of location * pexp * pexp | Pmetavar of pvar @@ -70,6 +71,7 @@ let rec pexp_location e = match e with (* | Psort (l,_) -> l *) | Pimm s -> sexp_location s + | Pbuiltin (l,_) -> l | Pvar (l,_) -> l | Phastype (l,_,_) -> l | Pmetavar (l, _) -> l @@ -97,6 +99,18 @@ let rec pexp_parse (s : sexp) : pexp = (* | Symbol (l, "Type") -> Psort (l, Type) *) | Symbol (l, name) when String.length name > 0 && String.get name 0 == '?' -> Pmetavar (l, String.sub name 1 (String.length name - 1)) + | Symbol (l, name) when String.length name > 2 + && String.get name 0 == '#' + && String.get name 1 == '#' + -> Pbuiltin (l, string_sub name 2 (String.length name)) + (* | Node (Symbol (start, "##"), [Symbol s]) + * -> Pbuiltin s + * | Node (Symbol (start, "##"), [e]) + * -> pexp_error (sexp_location e) "Non-symbol argument to `##`"; + * Pmetavar (start, "") + * | Node (Symbol (start, "##"), _) + * -> pexp_error start "`##` takes exactly one argument"; + * Pmetavar (start, "") *) | Symbol s -> Pvar s | Node (Symbol (start, "_:_"), [e; t]) -> Phastype (start, pexp_parse e, pexp_parse t) @@ -297,8 +311,10 @@ and pexp_unparse (e : pexp) : sexp = (* | Psort (l,Ext) -> Symbol (l, "%Ext%") *) (* | Psort (l,Type) -> Symbol (l, "%Type%") *) | Pimm s -> s + | Pbuiltin (l,name) -> Symbol (l, "##" ^ name) + (* | Pbuiltin ((l,_) as s) -> Node (Symbol (l, "##"), [Symbol s]) *) | Pvar v -> Symbol v - | Pmetavar (l,name) -> Symbol (l,"?"^name) + | Pmetavar (l,name) -> Symbol (l, "?" ^ name) | Phastype (l,e,t) -> Node (Symbol (l, "_:_"), [pexp_unparse e; pexp_unparse t]) | Plet (start, decls, body) -> @@ -406,6 +422,7 @@ let pexp_print e = print_string (pexp_string e) let pexp_name e = match e with | Pimm _ -> "Pimm" + | Pbuiltin _ -> "Pbuiltin" | Pvar (_,_) -> "Pvar" | Phastype (_,_,_) -> "Phastype" | Pmetavar (_, _) -> "Pmetavar" ===================================== src/prelexer.ml ===================================== --- a/src/prelexer.ml +++ b/src/prelexer.ml @@ -46,8 +46,6 @@ type pretoken = (* FIXME: Add syntax for char constants (maybe 'c'). *) (* FIXME: Handle multiline strings. *) -let string_sub str b e = String.sub str b (e - b) - let inc_cp (cp:charpos) (c:char) = (* Count char positions in utf-8: don't count the non-leading bytes. *) if utf8_head_p c then cp+1 else cp ===================================== src/util.ml ===================================== --- a/src/util.ml +++ b/src/util.ml @@ -90,6 +90,7 @@ let debug_msg expr = let not_implemented_error () = internal_error "not implemented" let string_implode chars = String.concat "" (List.map (String.make 1) chars) +let string_sub str b e = String.sub str b (e - b) let opt_map f x = match x with None -> None | Some x -> Some (f x) ===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -190,7 +190,7 @@ let _ = test_eval_eqv_named three = succ two; plus : Nat -> Nat -> Nat; - plus = lambda (x : Nat) -> lambda (y : Nat) -> case x + plus x y = case x | zero => y | succ z => succ (plus z y);") View it on GitLab: https://gitlab.com/monnier/typer/commit/f9a5b2f2efe0fa1028e95035146e88e137d…

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Novembre 2016