Simon Génier pushed to branch master at Stefan / Typer

Commits: d74651cf by Simon Génier at 2020-11-25T10:59:52-05:00 Get rid of attributes on builtin.

- - - - - f73bc318 by Simon Génier at 2020-12-01T23:35:45-05:00 Merge branch 'remove-attributes' into HEAD

- - - - -

5 changed files:

- src/builtin.ml - src/debruijn.ml - src/elab.ml - src/lexp.ml - src/opslexp.ml

Changes:

===================================== src/builtin.ml ===================================== @@ -134,7 +134,7 @@ let add_builtin_cst (name : string) (e : lexp) lmap := SMap.add name (e, t) map

let new_builtin_type name kind = - let t = mkBuiltin ((dloc, name), kind, None) in + let t = mkBuiltin ((dloc, name), kind) in add_builtin_cst name t; t

===================================== src/debruijn.ml ===================================== @@ -84,18 +84,18 @@ let fatal = Log.log_fatal ~section:"DEBRUIJN" let dloc = dummy_location let type_level_sort = mkSort (dloc, StypeLevel) let sort_omega = mkSort (dloc, StypeOmega) -let type_level = mkBuiltin ((dloc, "TypeLevel"), type_level_sort, None) +let type_level = mkBuiltin ((dloc, "TypeLevel"), type_level_sort) let level0 = mkSortLevel SLz let level1 = mkSortLevel (mkSLsucc level0) let level2 = mkSortLevel (mkSLsucc level1) let type0 = mkSort (dloc, Stype level0) let type1 = mkSort (dloc, Stype level1) let type2 = mkSort (dloc, Stype level2) -let type_int = mkBuiltin ((dloc, "Int"), type0, None) -let type_integer = mkBuiltin ((dloc, "Integer"), type0, None) -let type_float = mkBuiltin ((dloc, "Float"), type0, None) -let type_string = mkBuiltin ((dloc, "String"), type0, None) -let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0, None) +let type_int = mkBuiltin ((dloc, "Int"), type0) +let type_integer = mkBuiltin ((dloc, "Integer"), type0) +let type_float = mkBuiltin ((dloc, "Float"), type0) +let type_string = mkBuiltin ((dloc, "String"), type0) +let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0) let type_eq_type = let lv = (dloc, Some "l") in let tv = (dloc, Some "t") in @@ -108,7 +108,7 @@ let type_eq_type = mkArrow (Anormal, (dloc, None), mkVar (tv, 1), dloc, mkSort (dloc, Stype (mkVar (lv, 3))))))) -let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type, None) +let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type) let eq_refl = let lv = (dloc, Some "l") in let tv = (dloc, Some "t") in @@ -124,8 +124,7 @@ let eq_refl = [Aerasable, mkVar (lv, 2); Aerasable, mkVar (tv, 1); Anormal, mkVar (xv, 0); - Anormal, mkVar (xv, 0)])))), - None) + Anormal, mkVar (xv, 0)])))))

(* easier to debug with type annotations *)

===================================== src/elab.ml ===================================== @@ -106,7 +106,7 @@ 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) = - BI.add_builtin_cst name (mkBuiltin ((dloc, name), type_special_form, None)); + BI.add_builtin_cst name (mkBuiltin ((dloc, name), type_special_form)); special_forms := SMap.add name func (!special_forms)

let get_special_form name = @@ -584,7 +584,7 @@ and infer (p : sexp) (ctx : elab_context): lexp * ltype = and elab_special_form ctx f args ot = let loc = lexp_location f in match (OL.lexp'_whnf f (ectx_to_lctx ctx)) with - | Builtin ((_, name), _, _) -> + | Builtin ((_, name), _) -> (* Special form. *) (get_special_form name) ctx loc args ot

@@ -593,40 +593,11 @@ and elab_special_form ctx f args ot =

(* Make up an argument of type `t` when none is provided. *) and get_implicit_arg ctx loc oname t = - (* lookup default attribute of t. *) - (* FIXME: Don't lookup defaults/tactics here. Instead, just always - * generate a metavar at this point. The use of defaults/tactics should be - * postponed, probably to just before we do HM-style generalization. *) - match - try (* FIXME: We shouldn't hard code as popular a name as `default`. *) - let pidx, pname = (senv_lookup "default" ctx), "default" in - let default = mkVar ((dloc, Some pname), pidx) in - get_attribute ctx loc [default; t] - with e -> None with - | Some attr - -> (* 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 - * a macro call from a function call, but here, we have no need - * to distinguish two cases. - * Better yet: let's not do any table lookup here. Instead, - * call a `default-arg-filler` function, implemented in Typer, - * just like `Macro_expand` function. That one can then look - * things up in a table and/or do anything else it wants. *) - let v = lexp_expand_macro loc attr [] ctx (Some t) in - - (* get the sexp returned by the macro *) - let lsarg = match v with - | Vcommand cmd - -> (match cmd () with - | Vsexp (sexp) -> sexp - | _ -> value_fatal loc v "default attribute should return a IO Sexp" ) - | _ -> value_fatal loc v "default attribute should return an IO" in - - (* Elaborate the argument *) - check lsarg t ctx - | None -> newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx) - (loc, oname) t + newMetavar + (ectx_to_lctx ctx) + (ectx_to_scope_level ctx) + (loc, oname) + t

(* Build the list of implicit arguments to instantiate. *) and instantiate_implicit e t ctx = @@ -1388,92 +1359,23 @@ and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp = * Special forms implementation * -------------------------------------------------------------------------- *)

-and sform_new_attribute ctx loc sargs ot = - match sargs with - | [t] -> let ltp = infer_type t ctx (loc, None) 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"), - L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp), - Some AttributeMap.empty), - Lazy) - | _ -> fatal ~loc "new-attribute expects a single Type argument" - -and sform_add_attribute ctx loc (sargs : sexp list) ot = - let n = get_size ctx in - let table, var, attr = match List.map (lexp_parse_sexp ctx) sargs with - | [table; e; attr] when is_var e - -> table, (n - (get_var_db_index (get_var e)), U.get_vname_name (get_var_vname (get_var e))), attr - | _ -> fatal ~loc "add-attribute expects 3 arguments (table; var; attr)" in - - let map, attr_type = - match OL.lexp'_whnf table (ectx_to_lctx 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 attr' = L.clean (OL.lexp_close (ectx_to_lctx ctx) attr) in - let table = AttributeMap.add var attr' map in - (mkBuiltin ((loc, "add-attribute"), attr_type, Some table), - Lazy) - - - and get_attribute ctx loc largs = - let ctx_n = get_size ctx in - let table, var = match largs with - | [table; e] when is_var e - -> table, (ctx_n - get_var_db_index (get_var e), U.get_vname_name (get_var_vname (get_var e))) - | _ -> fatal ~loc "get-attribute expects 2 arguments (table; var)" in - - - let map = - match OL.lexp'_whnf table (ectx_to_lctx ctx) with - | Builtin (_, attr_type, Some map) -> map - | _ -> fatal ~loc "get-attribute expects a table as first argument" in - - try Some (AttributeMap.find var map) - with Not_found -> None - -and sform_get_attribute ctx loc (sargs : sexp list) ot = - match get_attribute ctx loc (List.map (lexp_parse_sexp ctx) sargs) with - | Some e -> (e, Lazy) - | None -> sexp_error loc "No attribute found"; sform_dummy_ret ctx loc - -and sform_has_attribute ctx loc (sargs : sexp list) ot = - let n = get_size ctx in - let table, var = match List.map (lexp_parse_sexp ctx) sargs with - | [table; e] when is_var e - -> table, (n - get_var_db_index (get_var e), U.get_vname_name (get_var_vname (get_var e))) - | _ -> fatal ~loc "get-attribute expects 2 arguments (table; var)" in - - - let map, attr_type = - let lp = OL.lexp_whnf table (ectx_to_lctx ctx) in - match lexp_lexp' lp with - | Builtin (_, attr_type, Some map) -> map, attr_type - | lxp -> lexp_fatal loc table - "get-attribute expects a table as first argument" in - - (BI.o2l_bool ctx (AttributeMap.mem var map), Lazy) - - and sform_declexpr ctx loc sargs ot = - match List.map (lexp_parse_sexp ctx) sargs with - | [e] when is_var e - -> (match DB.env_lookup_expr ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)) with - | Some lxp -> (lxp, Lazy) - | None -> error ~loc "no expr available"; +and sform_declexpr ctx loc sargs ot = + match List.map (lexp_parse_sexp ctx) sargs with + | [e] when is_var e + -> (match DB.env_lookup_expr ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)) with + | Some lxp -> (lxp, Lazy) + | None -> error ~loc "no expr available"; sform_dummy_ret ctx loc) - | _ -> error ~loc "declexpr expects one argument"; - sform_dummy_ret ctx loc + | _ -> error ~loc "declexpr expects one argument"; + sform_dummy_ret ctx loc

- let sform_decltype ctx loc sargs ot = - match List.map (lexp_parse_sexp ctx) sargs with - | [e] when is_var e - -> (DB.env_lookup_type ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)), Lazy) - | _ -> error ~loc "decltype expects one argument"; - sform_dummy_ret ctx loc +let sform_decltype ctx loc sargs ot = + match List.map (lexp_parse_sexp ctx) sargs with + | [e] when is_var e + -> (DB.env_lookup_type ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)), Lazy) + | _ -> error ~loc "decltype expects one argument"; + sform_dummy_ret ctx loc

@@ -1489,7 +1391,7 @@ let sform_built_in ctx loc sargs ot = * performance of type-inference (at least until we have proper * memoization of push_susp and/or whnf). *) -> let ltp' = L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp) in - let bi = mkBuiltin ((loc, name), ltp', None) in + let bi = mkBuiltin ((loc, name), ltp') in if not (SMap.mem name (!EV.builtin_functions)) then sexp_error loc ("Unknown built-in `" ^ name ^ "`"); BI.add_builtin_cst name bi; @@ -1926,10 +1828,6 @@ let register_special_forms () = ("Type_", sform_type); ("load", sform_load); (* FIXME: We should add here `let_in_`, `case_`, etc... *) - ("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", sform_decltype); ("declexpr", sform_declexpr);

===================================== src/lexp.ml ===================================== @@ -40,9 +40,6 @@ type meta_id = int (* Identifier of a meta variable. *)

type label = symbol

-type attribute_key = (int * string) (* rev_dbi * Var name *) -module AttributeMap = Map.Make (struct type t = attribute_key let compare = compare end) - (*************** Elaboration to Lexp *********************)

(* The scoping of `Let` is tricky: @@ -66,7 +63,7 @@ type ltype = lexp | Imm of sexp (* Used for strings, ... *) | SortLevel of sort_level | Sort of U.location * sort - | Builtin of symbol * ltype * lexp AttributeMap.t option + | Builtin of symbol * ltype | Var of vref | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) @@ -196,12 +193,8 @@ let lexp'_hash (lp : lexp') = | Stype lp -> lexp_hash lp | StypeOmega -> Hashtbl.hash s | StypeLevel -> Hashtbl.hash s)) - | Builtin (v, t, m) - -> U.combine_hash 4 (U.combine_hash - (U.combine_hash (Hashtbl.hash v) (lexp_hash t)) - (match m with - | Some m -> Hashtbl.hash m - | None -> 404)) + | Builtin (v, t) + -> U.combine_hash 4 (U.combine_hash (Hashtbl.hash v) (lexp_hash t)) | Var v -> U.combine_hash 5 (Hashtbl.hash v) | Let (l, ds, e) -> U.combine_hash 6 (U.combine_hash (Hashtbl.hash l) @@ -264,7 +257,7 @@ let hc_eq e1 e2 = | (Sort (_, StypeOmega), Sort (_, StypeOmega)) -> true | (Sort (_, StypeLevel), Sort (_, StypeLevel)) -> true | (Sort (_, Stype e1), Sort (_, Stype e2)) -> e1 == e2 - | (Builtin ((_, name1), _, _), Builtin ((_, name2), _, _)) -> name1 = name2 + | (Builtin ((_, name1), _), Builtin ((_, name2), _)) -> name1 = name2 | (Var (_, i1), Var (_, i2)) -> i1 = i2 | (Susp (e1, s1), Susp (e2, s2)) -> e1 == e2 && compare s1 s2 = 0 | (Let (_, defs1, e1), Let (_, defs2, e2)) @@ -310,7 +303,7 @@ let hc (l : 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, m) = hc (Builtin (v, t, m)) +let mkBuiltin (v, t) = hc (Builtin (v, t)) 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)) @@ -329,18 +322,18 @@ let impossible = mkImm Sexp.dummy_epsilon

let lexp_head e = match lexp_lexp' e with - | Imm s -> if e = impossible then "impossible" else "Imm" ^ sexp_string s - | Var _ -> "Var" - | Let _ -> "let" - | Arrow _ -> "Arrow" - | Lambda _ -> "lambda" - | Call _ -> "Call" - | Cons _ -> "datacons" - | Case _ -> "case" + | Imm s -> + if e = impossible then "impossible" else "Imm" ^ sexp_string s + | Var _ -> "Var" + | Let _ -> "let" + | Arrow _ -> "Arrow" + | Lambda _ -> "lambda" + | Call _ -> "Call" + | Cons _ -> "datacons" + | Case _ -> "case" | Inductive _ -> "typecons" | Susp _ -> "Susp" - | Builtin (_, _, None) -> "Builtin" - | Builtin _ -> "AttributeTable" + | Builtin _ -> "Builtin" | Metavar _ -> "Metavar" | Sort _ -> "Sort" | SortLevel _ -> "SortLevel" @@ -512,7 +505,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 @@ -667,7 +660,7 @@ let rec lexp_unparse lxp = match lexp_lexp' lxp with | Susp _ -> lexp_unparse (nosusp lxp) | Imm (sexp) -> sexp - | Builtin ((l,name), _, _) -> Symbol (l, "##" ^ name) + | Builtin ((l,name), _) -> Symbol (l, "##" ^ name) (* FIXME: Add a Sexp syntax for debindex references. *) | Var ((loc, name), _) -> Symbol (loc, maybename name) | Cons (t, (l, name)) @@ -893,7 +886,7 @@ let rec get_precedence expr ctx = | Arrow (Aimplicit, _, _, _, _) -> lkp "=>" | Arrow (Aerasable, _, _, _, _) -> lkp "≡>" | Call (exp, _) -> get_precedence exp ctx - | Builtin ((_, name), _, _) when is_binary_op name -> + | Builtin ((_, name), _) when is_binary_op name -> lkp (get_binary_op_name name) | Var ((_, Some name), _) when is_binary_op name -> lkp (get_binary_op_name name) @@ -955,11 +948,11 @@ and lexp_str ctx (exp : lexp) : string =

let get_name fname = match lexp_lexp' fname with - | Builtin ((_, name), _, _) -> name, 0 - | Var((_, Some name), idx) -> name, idx - | Lambda _ -> "__", 0 - | Cons _ -> "__", 0 - | _ -> "__", -1 in + | Builtin ((_, name), _) -> name, 0 + | Var((_, Some name), idx) -> name, idx + | Lambda _ -> "__", 0 + | Cons _ -> "__", 0 + | _ -> "__", -1 in

match lexp_lexp' exp with | Imm(value) -> (match value with @@ -1070,7 +1063,7 @@ and lexp_str ctx (exp : lexp) : string = | (_, Some name) -> name) ^ " => " ^ (lexp_stri 1 df))

- | Builtin ((_, name), _, _) -> "##" ^ name + | Builtin ((_, name), _) -> "##" ^ name

| Sort (_, StypeLevel) -> "##TypeLevel.Sort" | Sort (_, StypeOmega) -> "##Type_ω" @@ -1131,7 +1124,7 @@ let rec 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 + | (Builtin ((_, name1), _), Builtin ((_, name2), _)) -> name1 = name2 | (Var (_, i1), Var (_, i2)) -> i1 = i2 | (Susp (e1, s1), _) -> eq (push_susp e1 s1) e2 | (_, Susp (e2, s2)) -> eq e1 (push_susp e2 s2)

===================================== src/opslexp.ml ===================================== @@ -182,7 +182,7 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = args)) ctx | Call (f', xs1) -> mkCall (f', List.append xs1 xs) - | Builtin ((_, name), _, _) + | Builtin ((_, name), _) -> (match SMap.find_opt name (!reducible_builtins) with | Some f -> U.option_default e (f ctx args) | None -> e) @@ -342,7 +342,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) 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 @@ -620,9 +620,8 @@ and check'' erased ctx e = -> ((* error_tc ~loc:(lexp_location e) "Reached unreachable sort!"; * Log.internal_error "Reached unreachable sort!"; *) DB.sort_omega) - | Builtin (_, t, _) + | Builtin (_, t) -> let _ = check_type DB.set_empty Myers.nil t in - (* FIXME: Check the attributemap as well! *) t (* FIXME: Check recursive references. *) | Var (((l, name), idx) as v) @@ -990,7 +989,7 @@ and get_type ctx e = | Imm (Integer (_, _)) -> DB.type_int | Imm (String (_, _)) -> DB.type_string | Imm (Block (_, _, _) | Symbol _ | Node (_, _)) -> DB.type_int - | Builtin (_, t, _) -> t + | Builtin (_, t) -> t | SortLevel _ -> DB.type_level | Sort (l, Stype e) -> mkSort (l, Stype (mkSortLevel (mkSLsucc e))) | Sort (_, StypeLevel) -> DB.sort_omega @@ -1101,10 +1100,10 @@ let erasure_dummy = DB.type0

let rec erase_type (lxp: lexp): E.elexp = match lexp_lexp' lxp with - | L.Imm(s) -> E.Imm(s) - | L.Builtin(v, _, _) -> E.Builtin(v) - | L.Var(v) -> E.Var(v) - | L.Cons(_, s) -> E.Cons(s) + | L.Imm(s) -> E.Imm(s) + | L.Builtin(v, _) -> E.Builtin(v) + | L.Var(v) -> E.Var(v) + | L.Cons(_, s) -> E.Cons(s) | L.Lambda (P.Aerasable, _, _, body) -> erase_type (L.push_susp body (S.substitute erasure_dummy)) | L.Lambda (_, vdef, _, body) ->

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/0b414a4694f0f468b0534f003d03de675...