Setepenre pushed to branch master at Stefan / Typer

Commits: 6be3fe06 by Pierre Delaunay at 2016-11-21T02:10:56-05:00 Minor changes

- - - - - 801d9547 by Pierre Delaunay at 2016-11-21T02:11:19-05:00 Merge branch 'master' of gitlab.com:monnier/typer

- - - - - 08bee479 by Pierre Delaunay at 2016-11-21T02:54:20-05:00 * src/util.ml: Fatal error messages are not printed twice anymore * src/lexp.ml: lexp.AttributeTable was merged with lexp.Builtin

- - - - - 44f27a47 by Pierre Delaunay at 2016-11-21T14:40:37-05:00 Merge branch 'master' of gitlab.com:monnier/typer

- - - - - 9fea6e8c by Pierre Delaunay at 2016-11-22T13:08:30-05:00 * tests/eval_test.ml: delete infinite recursion failure test * src/lparse.ml: removed duplicate newlines

- - - - -

8 changed files:

- btl/types.typer - samples/bugs.typer - src/builtin.ml - src/lexp.ml - src/lparse.ml - src/opslexp.ml - src/util.ml - tests/eval_test.ml

Changes:

===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -47,7 +47,6 @@ Context = Built-in "Context"; % Lexp Context _+_ = Built-in "_+_" (Int -> Int -> Int); _*_ = Built-in "_*_" (Int -> Int -> Int);

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

===================================== samples/bugs.typer ===================================== --- a/samples/bugs.typer +++ b/samples/bugs.typer @@ -1,8 +0,0 @@ -x = 2.0; -y = 2; -% This produce the same error -% While I think the first one should say "x" has the wrong type -% and the second should say "Integer::mult expects Integers as arguments" -% i.e `hastype` should force type checking -main = (x : Int) * y; -main = x * y; \ No newline at end of file

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -54,6 +54,7 @@ let predef_name = [ "Macro"; "expand_macro_"; "expand_dmacro_"; + "Attribute"; ]

let default_predef_map : predef_table = @@ -113,9 +114,9 @@ let type_eq = let lv = (dloc, "l") in Arrow (Aexplicit, None, Var (tv, 1), dloc, type0))))

-let type_int = Builtin((dloc, "Int"), type0) -let type_float = Builtin((dloc, "Float"), type0) -let type_string = Builtin((dloc, "String"), type0) +let type_int = Builtin((dloc, "Int"), type0, None) +let type_float = Builtin((dloc, "Float"), type0, None) +let type_string = Builtin((dloc, "String"), type0, None)

(* lexp Imm list *) @@ -155,15 +156,6 @@ let is_lbuiltin idx ctx = else false

- -let has_attribute_impl loc largs ctx ftype = (*) - let table, attr_name = get_table "has-attribute" largs ctx in - let b = SMap.exists attr_name table in - let rvar = if b then get_predef "True" ctx else get_predef "False" ctx in *) - (get_predef "False" ctx), (get_predef "Bool" ctx) - - - let declexpr_impl loc largs ctx ftype =

let (vi, vn) = match largs with

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -63,7 +63,7 @@ type ltype = lexp | Imm of sexp (* Used for strings, ... *) | SortLevel of sort_level | Sort of U.location * sort - | Builtin of vdef * ltype + | Builtin of vdef * ltype * lexp AttributeMap.t option | Var of vref | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) @@ -79,8 +79,6 @@ type ltype = lexp * ltype (* The type of the return value of all branches *) * (U.location * (arg_kind * vdef option) list * lexp) SMap.t * (vdef option * lexp) option (* Default. *) - (* Special property table *) - | AttributeTable of lexp AttributeMap.t * ltype (* The `subst` only applies to the lexp associated * with the metavar's index (i.e. its "value"), not to the ltype. *) | Metavar of int * subst * vdef * ltype @@ -141,7 +139,7 @@ let hc (e : lexp) : lexp = let mkImm s = hc (Imm s) let mkSortLevel l = hc (SortLevel l) let mkSort (l, s) = hc (Sort (l, s)) -let mkBuiltin (v, t) = hc (Builtin (v, t)) +let mkBuiltin (v, t, m) = hc (Builtin (v, t, m)) let mkVar v = hc (Var v) let mkLet (l, ds, e) = hc (Let (l, ds, e)) let mkArrow (k, v, t1, l, t2) = hc (Arrow (k, v, t1, l, t2)) @@ -185,7 +183,7 @@ let rec lexp_location e = | SortLevel SLz -> U.dummy_location | Imm s -> sexp_location s | Var ((l,_),_) -> l - | Builtin ((l, _), _) -> l + | Builtin ((l, _), _, _) -> l | Let (l,_,_) -> l | Arrow (_,_,_,l,_) -> l | Lambda (_,(l,_),_,_) -> l @@ -259,7 +257,6 @@ let rec push_susp e s = (* Push a suspension one level down. *) * in many other cases than just when we bump into a Susp. *) | Susp (e,s') -> push_susp e (scompose s' s) | (Var _ | Metavar _) -> nosusp (mkSusp e s) - | AttributeTable _ -> e

and nosusp e = (* Return `e` with no outermost `Susp`. *) match e with @@ -336,9 +333,9 @@ let lexp_name e = | Cons _ -> "inductive-cons" | Case _ -> "case" | Inductive _ -> "inductive_" - | Builtin _ -> "Builtin" | Susp _ -> "Susp" - | AttributeTable _ -> "AttributeTable" + | Builtin (_, _, None) -> "Builtin" + | Builtin _ -> "AttributeTable" | _ -> "lexp_to_string: not implemented"

(* ugly printing (sexp_print (pexp_unparse (lexp_unparse e))) *) @@ -346,7 +343,10 @@ let rec lexp_unparse lxp = match lxp with | Susp _ as e -> lexp_unparse (nosusp e) | Imm (sexp) -> Pimm (sexp) - | Builtin ((loc, name), _) -> Pvar((loc, name)) + | Builtin ((loc, name), _, None) -> Pvar((loc, name)) + | Builtin ((loc, name), ltp, _ ) + -> Pcall(Pvar((loc, name)), [pexp_unparse (lexp_unparse ltp)]) + | Var ((loc, name), _) -> Pvar((loc, name)) | Cons (t, ctor) -> Pcons (lexp_unparse t, ctor) | Lambda (kind, vdef, ltp, body) -> @@ -524,7 +524,6 @@ and _lexp_to_str ctx exp = | Aexplicit -> ":" | Aimplicit -> "::" | Aerasable -> ":::" in

match exp with - | AttributeTable _ -> "AttributeTable" | Imm(value) -> (match value with | String (_, s) -> tval (""" ^ s ^ """) | Integer(_, s) -> tval (string_of_int s) @@ -576,8 +575,8 @@ and _lexp_to_str ctx exp = | Call(fname, args) -> ( (* get function name *) let str, idx, inner_parens, outer_parens = match fname with + | Builtin ((_, name), _, _) -> name, 0, false, true | 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 @@ -650,7 +649,7 @@ 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_?"

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -443,7 +443,7 @@ and check (p : pexp) (t : ltype) (ctx : elab_context): lexp = -> if not (OL.conv_p meta_ctx (ectx_to_lctx ctx) def_arg_type ltp) then lexp_error (lexp_location def_arg_type) def_arg_type ("Type mismatch! Context expected `" - ^ lexp_string ltp ^ "`\n")); + ^ lexp_string ltp ^ "`")); ltp, lbtp | lxp -> unify_with_arrow lxp kind var def_arg_type subst in

@@ -482,12 +482,12 @@ and infer_and_check pexp ctx t = -> lexp_error (pexp_location pexp) e ("Type mismatch! Context expected `" ^ lexp_string t ^ "` but expression has type `" - ^ lexp_string inferred_t ^ "`\n") + ^ lexp_string inferred_t ^ "`") | Some (_, (t1,t2)::_) -> lexp_error (pexp_location pexp) e ("Type mismatch! Context expected `" ^ lexp_string t2 ^ "` but expression has type `" - ^ lexp_string t1 ^ "`\n") + ^ lexp_string t1 ^ "`") | Some subst -> global_substitution := subst); e

@@ -745,17 +745,17 @@ 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"), _, _) -> ( (* ------ SPECIAL ------ *) match !_parsing_internals, sargs with | true, [String (_, str)] -> - Builtin((loc, str), ltp), ltp + 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), ltp + Builtin((loc, str), ltp, None), ltp

| true, _ -> error loc "Wrong Usage of `Built-in`"; dlxp, dltype @@ -1023,8 +1023,8 @@ and new_attribute_impl loc largs ctx ftype = | [ltp] -> ltp | _ -> fatal loc "new-attribute expects a single Type argument" in

- let attr_table_type = type0 in - AttributeTable (AttributeMap.empty, ltp), attr_table_type + let attr_table_type = get_predef "Attribute" ctx in + Builtin ((loc, "new-attribute"), ltp, Some AttributeMap.empty), attr_table_type

and add_attribute_impl loc largs ctx ftype = let meta_ctx, _ = !global_substitution in @@ -1034,12 +1034,13 @@ and add_attribute_impl loc largs ctx ftype = | _ -> fatal loc "add-attribute expects 3 arguments (table; var; attr)" in

let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) meta_ctx with - | AttributeTable (map, attr_type) -> map, attr_type + | 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 attr_table_type = type0 in - AttributeTable (AttributeMap.add var attr map, attr_type), attr_table_type + let attr_table_type = get_predef "Attribute" ctx in + let table = AttributeMap.add var attr map in + Builtin ((loc, "add-attribute"), attr_type, Some table), attr_table_type

and get_attribute_impl loc largs ctx ftype = let meta_ctx, _ = !global_substitution in @@ -1049,7 +1050,7 @@ and get_attribute_impl loc largs ctx ftype = | _ -> fatal loc "get-attribute expects 2 arguments (table; var)" in

let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) meta_ctx with - | AttributeTable (map, attr_type) -> map, attr_type + | Builtin (_, attr_type, Some map) -> map, attr_type | _ -> fatal loc "get-attribute expects a table as first argument" in

let lxp = AttributeMap.find var map in @@ -1067,7 +1068,7 @@ and has_attribute_impl loc largs ctx ftype = | _ -> fatal loc "get-attribute expects 2 arguments (table; var)" in

let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) meta_ctx with - | AttributeTable (map, attr_type) -> map, attr_type + | Builtin (_, attr_type, Some map) -> map, attr_type | lxp -> lexp_fatal loc lxp "get-attribute expects a table as first argument" in

try let _ = AttributeMap.find var map in @@ -1104,7 +1105,7 @@ let default_lctx, default_rctx = let lctx = ctx_define lctx (dloc, "Type1") type1 type2 in let lctx = ctx_define lctx (dloc, "Type") type0 type1 in (* FIXME: Add builtins directly here. *) - let lxp = Builtin((dloc, "Built-in"), type0) in + let lxp = Builtin((dloc, "Built-in"), type0, None) in let lctx = ctx_define lctx (dloc, "Built-in") lxp type0 in

(* Read BTL files *)

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -187,7 +187,7 @@ let rec conv_p' meta_ctx (ctx : DB.lexp_context) (vs : set_lexp) e1 e2 : bool = || (match (s1, s2) with | (Stype e1, Stype e2) -> conv_p e1 e2 | _ -> false) - | (Builtin ((_, s1), _), Builtin ((_, s2), _)) -> s1 = s2 + | (Builtin ((_, s1), _, _), Builtin ((_, s2), _, _)) -> s1 = s2 | (Var (_, v1), Var (_, v2)) -> v1 = v2 | (Arrow (ak1, vd1, t11, _, t12), Arrow (ak2, vd2, t21, _, t22)) -> ak1 == ak2 @@ -289,7 +289,7 @@ let rec check meta_ctx ctx e = | Sort (_, StypeOmega) -> (U.msg_error "TC" (lexp_location e) "Reached Unreachable sorts!"; B.type_omega) - | Builtin (_, t) -> t + | Builtin (_, t, _) -> t (* FIXME: Check recursive references. *) | Var v -> lookup_type ctx v | Susp (e, s) -> check ctx (push_susp e s) @@ -477,10 +477,9 @@ let rec erase_type (lxp: L.lexp): E.elexp =

match lxp with | L.Imm(s) -> E.Imm(s) - | L.Builtin(v, _) -> E.Builtin(v) + | L.Builtin(v, _, _) -> E.Builtin(v) | L.Var(v) -> E.Var(v) | L.Cons(_, s) -> E.Cons(s) - | L.AttributeTable _ -> E.Type | L.Lambda (P.Aerasable, _, _, body) -> (* The var shouldn't appear in body, basically, but we need * to adjust the debruijn indices of other vars, hence the subst. *)

===================================== src/util.ml ===================================== --- a/src/util.ml +++ b/src/util.ml @@ -74,13 +74,10 @@ let msg_message lvl kind section (loc: location) msg = " " ^ kind ^ " " ^ (Fmt.lalign_string section 8) ^ " " ^ msg ^ "\n" in print_string info) else ()

-(* let info = " " ^ kind ^ " [" ^ loc_string loc ^ "] " ^ (Fmt.lalign_string section 8) in - print_string (info ^ " " ^ msg ^ "\n")) else () *) - let msg_fatal s l m = msg_message 0 "[X] Fatal " s l m; flush stdout; - internal_error m + internal_error "Compiler Fatal Error"

let msg_error = msg_message 1 "[!] Error " let msg_warning = msg_message 2 "/!\ Warning "

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -265,35 +265,15 @@ let attr_decl = " greater-than = new-attribute (Int -> Int); greater-than = add-attribute greater-than w (lambda (x : Int) -> x);"

-let _ = test_eval_eqv attr_decl +let _ = test_eval_eqv_named + "has-attribute" + + attr_decl + "has-attribute greater-than w; (get-attribute greater-than w) 3;" - "True; 3"

-(* This makes sure contexts are reinitialized between calls - * i.e the context should not grow *) -let _ = (add_test "EVAL" "Infinite Recursion failure" (fun () -> - _typer_verbose := (-1); - - let code = " - infinity : Int -> Int; - infinity = lambda beyond -> infinity beyond;" in - - let rctx, lctx = eval_decl_str code lctx rctx in - - (* Expect throwing *) - try (* use the silent version as an error will be thrown *) - let _ = _eval_expr_str "(infinity 0);" lctx rctx true in - _typer_verbose := 20; - failure () - with - Internal_error m -> ( - _typer_verbose := 20; - if m = "Recursion Depth exceeded" then - success () - else - failure ()) -)) + "True; 3"

let _ = (add_test "EVAL" "Monads" (fun () ->

View it on GitLab: https://gitlab.com/monnier/typer/compare/d75bf00409392ef25d2091d5d8163d4578a...