Setepenre pushed to branch master at Stefan / Typer Commits: 0c893907 by Pierre Delaunay at 2016-05-07T08:51:03-04:00 Modified Builtin Changes to be committed: * src/util.ml Added `typer_unreachable` for impossible case branch raise an error if the branch is used * src/lexp.ml: New definition of builtin - - - - - 26948fc1 by Pierre Delaunay at 2016-05-07T11:16:32-04:00 New builtin system Builtin definition file everything is in a single file because we can't force file eval order yet (module system required) Changes to be committed: * btl/types.typer: - - - - - 227524e9 by Pierre Delaunay at 2016-05-07T11:20:05-04:00 merging - - - - - 16 changed files: - btl/list.typer - btl/macro.typer - + btl/types.typer - + btl/unit.typer - + samples/empty.typer - samples/macro.typer - src/builtin.ml - src/env.ml - src/eval.ml - src/lexp.ml - src/lparse.ml - src/pexp.ml - src/util.ml - tests/env_test.ml - tests/eval_test.ml - tests/lexp_test.ml Changes: ===================================== btl/list.typer ===================================== --- a/btl/list.typer +++ b/btl/list.typer @@ -1,6 +1,4 @@ - - -List : Type; +List : Type -> Type; List = inductive_ (dList (a : Type)) (nil) (cons a (List a)); nil = inductive-cons List nil; @@ -26,5 +24,3 @@ tail = lambda a => case xs | nil => nil | cons hd tl => tl; - - ===================================== btl/macro.typer ===================================== --- a/btl/macro.typer +++ b/btl/macro.typer @@ -1,12 +1,24 @@ -% define Sexp constructor -Sexp : Type; -Sexp = inductive_ (built-in) (block_ Sexp) - (symbol_ string) (string_ string) (integer_ Int) (float_ Float) - (node_ Sexp List Sexp); + +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_ (built-in) (Macro_ sexp); +Macro = inductive_ (dMacro) (Macro_ Type); +Macro_ = inductive-cons Macro Macro_; + %% Basic usage % ===================================== btl/types.typer ===================================== --- /dev/null +++ b/btl/types.typer @@ -0,0 +1,68 @@ +% Base Types +% ----------------------------------------------------- + +Type = Built-in "Type"; +Int = Built-in "Int"; +Float = Built-in "Float"; +String = Built-in "String"; +Sexp = Built-in "Sexp"; + +% Basic operators +_+_ : Int -> Int -> Int; +_+_ = Built-in "_+_"; + +_*_ : Int -> Int -> Int; +_*_ = Built-in "_*_"; + +% List +% ----------------------------------------------------- + +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 a 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; + +% Macro +% ----------------------------------------------------- + +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_ ; + ===================================== btl/unit.typer ===================================== --- /dev/null +++ b/btl/unit.typer @@ -0,0 +1,5 @@ + +% Declare a dummy Type +Unit : Type; +Unit = inductive_ (Unit) (unit); +unit = inductive-cons Unit unit; ===================================== samples/empty.typer ===================================== --- /dev/null +++ b/samples/empty.typer ===================================== samples/macro.typer ===================================== --- a/samples/macro.typer +++ b/samples/macro.typer @@ -20,8 +20,12 @@ m1 = (sqr 2); % The easy way % +%Type List a = +% | Nil +% | Cons a (list a); -sqr = Macro_ (qq (lambda (x : Int) -> x * x)); + +sqr = Macro_ (qquote (lambda (x : Int) -> x * x)); m2 = (sqr 2); @@ -30,6 +34,46 @@ m2 = (sqr 2); % my_fun = let a = 2 in - Macro_ (qquote lambda (x : Int) -> x * (uquote a)); + Macro_ lambda (x : Sexp) -> qquote ((uquote x) * (uquote (integer_ a)))); + +my_fun = + Macro_ lambda (x : Sexp) -> qquote (lambda (y : Int) -> (uquote x) * (uquote y))); + + +quote = Maocr_ quote +quote e = case early + | Node () + +main = (my_fun 3); 3 * 2 + + +% +% Hygiene +% + +fun1 = lambda (x : Int) -> x * 2; +fun2 = Macro_ (lambda (x : Int) -> (qquote x * (fun1 x))); +fun1 = lambda (x : Int) -> x * 3; + +m3 = (fun2 2); % if Hygienic == 8 + % else == 12 + +% +% Depends when the macro is lexp and evaluated... +% lexp_parsing the macro early would fix its index +% and prevent the presented issue +% + +% We can force function inlining + +%sqr_inline = lambda (x : Int) -> +% let a = x in +% Macro_ (qquote ((uquote x) * ((uquote x)))); + + +% Macro_ (qquote (lambda (x : Int) -> x * x)); +% sqr2 = (inline (lambda (x : Int) -> x * x)); + + + -main = (my_fun 3); \ No newline at end of file ===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -54,17 +54,11 @@ let type0 = Sort (dloc, Stype slevel0) let type1 = Sort (dloc, Stype slevel1) let type_omega = Sort (dloc, StypeOmega) let type_level = Sort (dloc, StypeLevel) -let type_level = Builtin (LevelType, "TypeLevel", type_level) - -let type_int = Builtin (IntType , "Int" , type0) -let type_float = Builtin (FloatType, "Float", type0) -let type_sexp = Builtin (SexpType , "Sexp" , type0) +let type_level = Builtin ((dloc, "TypeLevel"), type_level) let op_binary t = Arrow (Aexplicit, None, t, dloc, Arrow (Aexplicit, None, t, dloc, t)) -let iop_binary = op_binary type_int -let fop_binary = op_binary type_float let type_eq = let lv = (dloc, "l") in let tv = (dloc, "t") in Arrow (Aerasable, Some lv, type_level, dloc, @@ -74,22 +68,13 @@ let type_eq = let lv = (dloc, "l") in Arrow (Aexplicit, None, Var (tv, 1), dloc, type0)))) -let builtin_iadd = Builtin (IAdd, "_+_", iop_binary) -let builtin_imult = Builtin (IMult, "_*_", iop_binary) -let builtin_eq = Builtin (EqType, "_=_", type_eq) - -(* -let builtin_fadd = Builtin (FAdd, "_+_", fop_binary) -let builtin_fmult = Builtin (FMult, "_*_", fop_binary) *) - +let type_int = Builtin((dloc, "Int"), type0) +let type_float = Builtin((dloc, "Float"), type0) +let type_string = Builtin((dloc, "String"), type0) (* Builtin of builtin * string * ltype *) let _generic_binary_iop name f loc (args_val: value_type list) (ctx: runtime_env) = - (* - let l, r = get_rte_variable None 0 ctx, - get_rte_variable None 1 ctx in *) - let l, r = match args_val with | [l; r] -> l, r | _ -> builtin_error loc (name ^ " expects 2 Integers arguments") in @@ -106,16 +91,10 @@ 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 eq_impl loc args_val ctx = - let l, r = match args_val with - | [a; b] -> a, b - | _ -> builtin_error loc "_=_ expects 2 arguments") in - - conv_p l r *) (* loc is given by the compiler *) -let none_fun = (fun loc args_val ctx -> +let none_fun : (location -> value_type list -> runtime_env -> value_type) + = (fun loc args_val ctx -> builtin_error loc "Requested Built-in was not implemented") let make_symbol loc args_val ctx = @@ -163,37 +142,12 @@ let sexp_dispatch loc args ctx = | _ -> builtin_error loc "sexp_dispatch error" + let make_block loc args_val ctx = Vdummy let make_string loc args_val ctx = Vdummy let make_integer loc args_val ctx = Vdummy let make_float loc args_val ctx = Vdummy -let type_string = type0 -let type_mblock = type0 - -let type_msymbol = Arrow (Aexplicit, None, type_string, dloc, type_sexp) -let type_mstring = Arrow (Aexplicit, None, type_string, dloc, type_sexp) -let type_minteger = Arrow (Aexplicit, None, type_int , dloc, type_sexp) -let type_mfloat = Arrow (Aexplicit, None, type_float , dloc, type_sexp) -let type_mnode = Arrow (Aexplicit, None, type_sexp , dloc, type_sexp) -let type_mexpand = Arrow (Aexplicit, None, type_sexp , dloc, type0) - -let builtin_block = Builtin (SexpType, "block_", type_mblock) -let builtin_symbol = Builtin (SexpType, "symbol_", type_msymbol) -let builtin_string = Builtin (SexpType, "string_", type_mstring) -let builtin_integer = Builtin (SexpType, "integer_", type_minteger) -let builtin_float = Builtin (SexpType, "float_", type_mfloat) -let builtin_node = Builtin (SexpType, "node_", type_mnode) -(* let builtin_expand = Builtin (SexpType, "expand_", type_mexpand) *) - - -let builtin_macro = Cons (((dloc, "Macro"), (-4)), (dloc, "Macro_")) -(* let builtin_quote = Cons (((dloc, "Macro"), (-4)), (dloc, "quote")) *) -let builtin_qq = Cons (((dloc, "Macro"), (-4)), (dloc, "qquote")) -let type_macro = Builtin (MacroType, "Macro", type0) -let macro_cons = Arrow (Aexplicit, None, type_sexp, dloc, type_macro) -let quote_cons = Arrow (Aexplicit, None, type0, dloc, type_sexp) - (* * Should we have a function that @@ -204,78 +158,34 @@ let quote_cons = Arrow (Aexplicit, None, type0, dloc, type_sexp) * -> ou seulement: 'eval expr ctx' *) -(* Built-in list of types/functions *) -(* Some of the information is redundant but it suppress a lot of warnings *) -let typer_builtins = [ -(* NAME | LXP | Type | impl *) - ("Type" , type0 , type0, none_fun); - ("Int" , type_int , type0, none_fun); - ("Float" , type_float , type0, none_fun); - ("String", type_string, type0, none_fun); - ("Sexp" , type_sexp , type0, none_fun); - ("Macro" , type_macro , type0, none_fun); - -(* Built-in Functions *) - ("_=_" , builtin_eq, type_eq, none_fun); (* t -> t -> bool *) - ("_+_" , builtin_iadd, iop_binary, iadd_impl); (* int -> int -> int *) - ("_*_" , builtin_imult, iop_binary, imult_impl); (* int -> int -> int *) - ("Macro_", builtin_macro, macro_cons, none_fun); - (*("'" , builtin_quote, quote_cons, none_fun); *) - ("qquote" , builtin_qq , quote_cons, none_fun); -(* Macro primitives *) - ("block_" , builtin_block , type_mblock , make_block); - ("symbol_" , builtin_symbol , type_msymbol , make_symbol); - ("string_" , builtin_string , type_mstring , make_string); - ("integer_", builtin_integer, type_minteger, make_integer); - ("float_" , builtin_float , type_mfloat , make_float); - ("node_" , builtin_node , type_mnode , make_node); - (* ("expand_" , builtin_expand , type_mexpand , none_fun); *) - -(* Macros primitives type ? *) +(* Built-in list of types/functions *) +let typer_builtins_impl = [ + ("_+_" , iadd_impl); + ("_*_" , imult_impl); + ("block_" , make_block); + ("symbol_" , make_symbol); + ("string_" , make_string); + ("integer_", make_integer); + ("node_" , make_node); ] - (* Make built-in lookup table *) let _builtin_lookup = - List.fold_left (fun lkup (name, _, _, f) -> + List.fold_left (fun lkup (name, f) -> SMap.add name f lkup) - SMap.empty typer_builtins - + SMap.empty typer_builtins_impl -let get_builtin_impl btype str loc = +let get_builtin_impl str loc = try SMap.find str _builtin_lookup with Not_found -> builtin_error loc "Requested Built-in does not exist" -(* Make lxp context with built-in types *) -let default_lctx () = - (* Empty context *) - let lctx = make_lexp_context in - - (* populate ctx *) - List.fold_left - (fun ctx (name, lxp, ltp, _) -> - env_extend ctx (dloc, name) (Some lxp) ltp) - lctx - typer_builtins -;; +let btl_folder = ref "./btl/" -(* Make runtime context with built-in types *) -let default_rctx () = - (* Empty context *) - let rctx = make_runtime_ctx in - - (* populate ctx *) - List.fold_left - (fun ctx (name, lxp, ltp, f) -> - add_rte_variable (Some name) (Vdummy) ctx) - rctx - typer_builtins -;; let is_lbuiltin idx ctx = - let bsize = List.length typer_builtins in + let bsize = 1 in let csize = get_size ctx in if idx >= csize - bsize then ===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -49,12 +49,11 @@ let env_error loc msg = let str_idx idx = "[" ^ (string_of_int idx) ^ "]" -(* currently, we don't do much *) type value_type = | Vint of int | Vstring of string | Vcons of symbol * value_type list - | Vbuiltin of builtin * string + | Vbuiltin of string | Closure of lexp * (((string option * value_type) ref myers) * (int * int)) | Vsexp of sexp (* Values passed to macros. *) (* Unable to eval during macro expansion, only throw if the value is used *) @@ -73,7 +72,7 @@ let rec value_print (vtp: value_type) = List.iter (fun arg -> print_string " "; value_print arg) args; print_string ")"; - | Vbuiltin(_, str) -> print_string str + | Vbuiltin(str) -> print_string str | Vdummy -> print_string "value_print_dummy" let value_location (vtp: value_type) = ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -80,7 +80,7 @@ let rec _eval lxp ctx i: (value_type) = | Inductive (_, _, _, _) -> Vdummy | Cons (_, label) -> Vcons (label, []) | Lambda (_, _, _, lxp) -> Closure(lxp, ctx) - | Builtin (btype, str, _) -> Vbuiltin(btype, str) + | Builtin ((_, str), _) -> Vbuiltin(str) (* Return a value stored in env *) | Var((loc, name), idx) as e -> eval_var ctx e ((loc, name), idx) @@ -112,26 +112,8 @@ and eval_call ctx i lname args = let args = List.map (fun (k, e) -> _eval e ctx (i + 1)) args in let f = _eval lname ctx (i + 1) in - (* - let eval_call' f arg = - match f with - | Vcons(label, fields) -> - Vcons (label, arg::fields) - - | Closure (lxp, ctx) -> - _eval lxp (add_rte_variable None arg ctx) (i + 1) - - | Vbuiltin (btype, str) -> - (get_builtin_impl btype str loc) loc [] (add_rte_variable None arg ctx) - - | _ -> value_print f; - eval_error loc "Cannot eval function" in - - List.fold_left eval_call' f args *) - let rec eval_call f args ctx = match f, args with - (* | Vcons ((_, "quote"), _), [vsxp] -> vsxp *) | Vcons (n, []), _ -> Vcons(n, args) (* we add an argument to the closure *) @@ -140,12 +122,11 @@ and eval_call ctx i lname args = let ret = _eval lxp nctx (i + 1) in eval_call ret tl nctx - | Vbuiltin (btype, str), args -> + | Vbuiltin (str), args -> (* lookup the built-in implementation and call it *) - (get_builtin_impl btype str loc) loc args ctx + (get_builtin_impl str loc) loc args ctx (* return result of eval *) - | Closure (_, _), [] -> f | _, [] -> f | _ -> value_print f; @@ -277,7 +258,7 @@ let from_lctx (ctx: lexp_context): runtime_env = let rctx = ref make_runtime_ctx in (* Skip builtins: They are already in default_rctx() *) - let bsize = List.length typer_builtins in + let bsize = 1 in let csize = get_size ctx in (* add all variables *) ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -50,17 +50,6 @@ type label = symbol (*************** Elaboration to Lexp *********************) -type builtin = - | IntType - | FloatType - | SexpType - | LexpType - | IAdd - | IMult - | EqType - | LevelType - | MacroType - (* Pour la propagation des types bidirectionnelle, tout va dans `infer`, * sauf Lambda et Case qui vont dans `check`. Je crois. *) type ltype = lexp @@ -68,7 +57,7 @@ type ltype = lexp | Imm of sexp (* Used for strings, ... *) | SortLevel of sort_level | Sort of U.location * sort - | Builtin of builtin * string * ltype + | Builtin of vdef * ltype | Var of vref | Susp of lexp * lexp S.subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) @@ -340,13 +329,10 @@ let lexp_to_string e = | Inductive _ -> "inductive_" | Cons _ -> "inductive-cons" | Case _ -> "case" - | _ -> "not implemented" + | Builtin _ -> "Builtin" + | _ -> "lexp_to_string: not implemented" + -(* let builtin_reduce b args arg = - * match b,args,arg with - * | IAdd, [(_,Imm (Integer (_, i1)))], (Imm (Integer (_, i2))) - * -> Some (Imm (Integer (U.dummy_location, i1 + i2))) - * | _ -> None *) (* Apply substitution `s' and then reduce to weak head normal form. * WHNF implies: @@ -701,11 +687,11 @@ and _lexp_to_str ctx exp = | Call(fname, args) -> ( (* get function name *) let str, idx, inner_parens, outer_parens = match fname with - | Var((_, name), idx) -> name, idx, false, true - | Builtin (_, name, _) -> name, 0, false, true - | Lambda _ -> "__", 0, true, false - | Cons _ -> "__", 0, false, false - | _ -> "__", -1, true, true in + | Var((_, name), idx) -> name, idx, false, true + | Builtin ((_, name), _) -> name, 0, false, true + | Lambda _ -> "__", 0, true, false + | Cons _ -> "__", 0, false, false + | _ -> "__", -1, true, true in let binop_str op (_, lhs) (_, rhs) = (lexp_to_str lhs) ^ op ^ (lexp_to_str rhs) in @@ -770,14 +756,14 @@ and _lexp_to_str ctx exp = | Some df -> str ^ nl ^ (make_indent 1) ^ "| _ => " ^ (lexp_to_stri 1 df)) - | Builtin (_, name, _) -> name + | Builtin ((_, name), _) -> name | Sort (_, Stype lvl) -> (match lvl with | SortLevel (SLn 0) -> "Type" | SortLevel (SLn v) -> "Type" ^ (string_of_int v) | _ -> "Type") - | _ -> print_string "Printing Not Implemented"; "" + | _ -> print_string "Printing Not Implemented"; "-- --" and lexp_str_ctor ctx ctors = SMap.fold (fun key value str -> ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -34,6 +34,9 @@ open Util open Fmt open Myers +open Prelexer +open Lexer + open Sexp open Pexp open Lexp @@ -364,19 +367,32 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = try (* Check if the function was defined *) let idx = senv_lookup name ctx in let vf = (make_var name idx loc) in - let ret_type = get_return_type name 0 ltp new_args in (* Replace a built-in name by builtin so they can be recognized - * during eval *) + * during eval *) if (is_lbuiltin idx ctx) then ( match env_lookup_expr ctx ((loc, name), idx) with | None -> lexp_error loc "Unknown builtin"; - Call(vf, new_args), ret_type + let ret_type = get_return_type name 0 ltp new_args in + Call(vf, new_args), ret_type + + | Some Builtin((_, "Built-in"), ltp) ->( + match largs with + | [Imm (String (_, str)) ] -> + Builtin((loc, str), ltp), ltp + | _ -> typer_unreachable "cannot be reached") (* a builtin functions *) - | Some e -> Call(e, new_args), ret_type + | Some Builtin((_, name), ltp) -> + (* We keep loc info *) + Call(Builtin((loc, name), ltp), new_args), ltp + + | _ -> typer_unreachable "ill formed Builtin" ) - else Call(vf, new_args), ret_type + else + let ret_type = get_return_type name 0 ltp new_args in + Call(vf, new_args), ret_type + with Not_found -> lexp_error loc ("The function \"" ^ name ^ "\" was not defined"); let vf = (make_var name (-1) loc) in @@ -407,12 +423,14 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = let lxp, ltp = _lexp_p_infer pxp ctx (i + 1) in Call(lxp, new_args), ltp in + (* let handle_qq loc = (* In quasi quote we need to traverse the sexp tree and evaluate * (uq) calls *) let rec seek_n_replace sxp = match sxp with + (* Unquote *) | Node (Symbol(_, "uquote"), [arg]) ->( let parg = pexp_parse arg in let larg, _ = _lexp_p_infer parg ctx i in @@ -421,7 +439,9 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = | Vint (i) -> Integer(loc, i) | Vstring (s) -> String (loc, s) | Vsexp(sxp) -> sxp - | _ -> lexp_warning loc "Sexp was expected"; Epsilon) + | _ -> + value_print vsxp; + lexp_warning loc "Sexp was expected"; Epsilon) | Node (op, lst) -> Node(op, (List.map seek_n_replace lst)) | _ -> sxp in @@ -429,7 +449,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = let sxp = match sargs with | [sxp] -> seek_n_replace sxp | _ -> lexp_error loc "qquote expects a sexp"; Epsilon in - Imm(sxp), type_sexp in + Imm(sxp), type_sexp in *) (* determine function type *) match fun_name, ltp with @@ -437,10 +457,11 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = | ((Plambda _), _) -> Call(body, new_args), ltp (* Call to a macro *) - | (Pvar (l, n), Builtin(tp, "Macro", _)) when tp = MacroType -> + | (Pvar (l, n), Builtin((_, "Macro"), _)) -> handle_macro_call (l, n) - | (Pvar (l, "qquote"), _) -> handle_qq l + (* + | (Pvar (l, "qquote"), _) -> handle_qq l *) (* Call to quote * ) | (Pvar (l, "'"), _) -> (match (handle_named_call (l, "'")), sargs with @@ -724,9 +745,35 @@ let add_def name ctx = let ctx = senv_add_var var ctx in env_add_var_info (0, var, None, dlxp) ctx +(* Default context with builtin types + * --------------------------------------------------------- *) + +(* Make lxp context with built-in types *) +let default_lctx () = + (* Empty context *) + let lctx = make_lexp_context in + let lxp = Builtin((dloc, "Built-in"), type0) in + let lctx = env_extend lctx (dloc, "Built-in") (Some lxp) type0 in + + (* Read BTL files *) + let pres = prelex_file "./btl/types.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 + let _, lctx = lexp_p_decls pxps lctx in + lctx +;; + +(* Make runtime context with built-in types *) +let default_rctx () = + try (from_lctx (default_lctx ())) + with e -> + lexp_fatal dloc "Could not convert lexp context into rte context" + (* String Parsing - * ------------------------ *) + * --------------------------------------------------------- *) (* Lexp helper *) let _lexp_expr_str (str: string) (tenv: bool array) @@ -747,8 +794,9 @@ let lexp_decl_str str lctx = _lexp_decl_str str default_stt default_grammar (Some ";") lctx + (* Eval String - * ---------------------- *) + * --------------------------------------------------------- *) (* Because we cant include lparse in eval.ml *) let _eval_expr_str str lctx rctx silent = ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -370,7 +370,7 @@ let pexp_decls_all (nodes: sexp list): ((pvar * pexp * bool) list) = ;; (* String Parsing - * ------------------------ *) + * --------------------------------------------------------- *) (* Lexp helper *) let _pexp_expr_str (str: string) (tenv: bool array) ===================================== src/util.ml ===================================== --- a/src/util.ml +++ b/src/util.ml @@ -52,6 +52,9 @@ let _typer_verbose = ref 20 exception Internal_error of string let internal_error s = raise (Internal_error s) +exception Unreachable_error of string +let typer_unreachable s = raise (Unreachable_error s) + (* File is not printed because currently we parse only one file... *) (* Section is the name of the compilation step [for debugging] *) (* 'prerr' output is ugly *) ===================================== tests/env_test.ml ===================================== --- a/tests/env_test.ml +++ b/tests/env_test.ml @@ -30,6 +30,7 @@ open Utest_lib open Sexp open Lexp +open Lparse open Builtin open Env ===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -350,39 +350,10 @@ let _ = (add_test "EVAL" "Partial Application" (fun () -> ));; -let list_decl = " -List : 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 a 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; -";; - let _ = (add_test "EVAL" "List" (fun () -> reset_eval_trace (); - let dcode = list_decl ^ " + let dcode = " my_list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); " in ===================================== tests/lexp_test.ml ===================================== --- a/tests/lexp_test.ml +++ b/tests/lexp_test.ml @@ -45,8 +45,8 @@ let _ = (add_test "LEXP" "Built-in type Inference" (fun () -> match ret with (* (vdef * lexp * ltype) *) - | [(_, _, Builtin(_, "Int", _)); - (_, _, Builtin(_, "Float", _))] -> + | [(_, _, Builtin((_, "Int"), _)); + (_, _, Builtin((_, "Float"), _))] -> success() | _ -> failure () View it on GitLab: https://gitlab.com/monnier/typer/compare/c4c529a9c4de0faaaf0f47d2a78498e7928...