Stefan pushed to branch master at Stefan / Typer

Commits: 886a3589 by Stefan Monnier at 2020-04-08T18:07:18-04:00 Remove most uses of L.clean

* src/elab.ml (elab_check_sort, elab_check_def, infer_type): Skip `L.clean` since `lexp_string` already cleans up on the fly. (track_fv): Skip `L.clean` since `fv` already cleans up on the fly. (lexp_eval): Skip `L.clean` since `fv` and `erase_type` already clean up on the fly. (sform_new_attribute, sform_add_attribute, sform_built_in): Explicitly call `clean` now that `lexp_close` doesn't do it any more.

* src/eval.ml (from_lctx): Skip `L.clean` since `fv` and `erase_type` already clean up on the fly.

* src/lexp.ml (print_context_value): Remove `Expr` constructor. (pretty_ppctx): Remove unused `parent` and now unused `metavar`. (smap_lexp, pp_parent, pp_meta, set_parent, set_parent): Remove functions. (lexp_str): Don't call `set_parent` any more. Rewrite metavar case to use `metavar_lookup` rather than `clean`.

* src/opslexp.ml (lexp_close): Don't call `clean` any more. (conv_p', mkSLlub): Skip `L.clean` since `level_canon` already cleans up on the fly. (check''.assert_type): Skip `L.clean` since `lexp_string` already cleans up on the fly. (erase_type): Clean up metavars on the fly.

* src/unification.ml (unify_metavar): Skip `L.clean` since `lexp_string` already cleans up on the fly.

- - - - -

6 changed files:

- src/elab.ml - src/eval.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml

Changes:

===================================== src/elab.ml ===================================== @@ -128,8 +128,7 @@ let elab_check_sort (ctx : elab_context) lsort var ltp = "Exception during whnf of sort:"; raise e) with | Sort (_, _) -> () (* All clear! *) - | _ -> let lexp_string e = lexp_string (L.clean e) in - let typestr = lexp_string ltp ^ " : " ^ lexp_string lsort in + | _ -> let typestr = lexp_string ltp ^ " : " ^ lexp_string lsort in match var with | (l, None) -> lexp_error l ltp ("`" ^ typestr ^ "` is not a proper type") @@ -159,7 +158,6 @@ let elab_check_def (ctx : elab_context) var lxp ltype = let lctx = ectx_to_lctx ctx in let loc = lexp_location lxp in

- let lexp_string e = lexp_string (L.clean e) in let ltype' = try OL.check lctx lxp with e -> match e with | Log.Stop_Compilation _ -> raise e @@ -655,8 +653,7 @@ and infer_type pexp ectx var = s (ectx_to_lctx ectx) with | (_::_) - -> (let lexp_string e = lexp_string (L.clean e) in - let typestr = lexp_string t ^ " : " ^ lexp_string s in + -> (let typestr = lexp_string t ^ " : " ^ lexp_string s in match var with | (l, None) -> lexp_error l t ("`" ^ typestr ^ "` is not a proper type") @@ -1042,13 +1039,12 @@ and track_fv rctx lctx e = name ^ " (" ^ track_fv (Myers.nthcdr drop rctx) (Myers.nthcdr drop lctx) - (L.clean e) + e ^ ")" | _ -> name in String.concat " " (List.map tfv nc)

and lexp_eval ectx e = - let e = L.clean e in let ee = OL.erase_type e in let rctx = EV.from_ectx ectx in

@@ -1334,7 +1330,7 @@ and sform_new_attribute ctx loc sargs ot = * is False, for example): Should be a type like `AttributeMap t` * instead. *) (mkBuiltin ((loc, "new-attribute"), - OL.lexp_close (ectx_to_lctx ctx) ltp, + L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp), Some AttributeMap.empty), Lazy) | _ -> fatal ~loc "new-attribute expects a single Type argument" @@ -1350,7 +1346,7 @@ and sform_add_attribute ctx loc (sargs : sexp list) ot = | _ -> fatal ~loc "add-attribute expects a table as first argument" in

(* FIXME: Type check (attr: type == attr_type) *) - let attr' = OL.lexp_close (ectx_to_lctx ctx) attr in + 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) @@ -1411,7 +1407,11 @@ let sform_built_in ctx loc sargs ot = | true, [String (_, name)] -> (match ot with | Some ltp - -> let ltp' = OL.lexp_close (ectx_to_lctx ctx) ltp in + (* FIXME: This `L.clean` is basically the last remaining use of the + * function. It's not indispensible, tho it might still be useful for + * 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 if not (SMap.mem name (!EV.builtin_functions)) then sexp_error loc ("Unknown built-in `" ^ name ^ "`");

===================================== src/eval.ml ===================================== @@ -1113,16 +1113,15 @@ let from_lctx (lctx: lexp_context): runtime_env = Myers.cons (loname, ref (match def with | LetDef (_, e) - -> let e = L.clean e in - if closed_p rctx (OL.fv e) then - eval (OL.erase_type e) rctx - else Vundefined + -> if closed_p rctx (OL.fv e) then + eval (OL.erase_type e) rctx + else Vundefined | _ -> Vundefined)) rctx | CVfix (defs, lctx) -> let fvs = List.fold_left (fun fvs (_, e, _) - -> OL.fv_union fvs (OL.fv (L.clean e))) + -> OL.fv_union fvs (OL.fv e)) OL.fv_empty defs in let rctx = from_lctx lctx in

===================================== src/inverse_subst.ml ===================================== @@ -1,6 +1,6 @@ (* inverse_subst.ml --- Computing the inverse of a substitution

-Copyright (C) 2016-2019 Free Software Foundation, Inc. +Copyright (C) 2016-2020 Free Software Foundation, Inc.

Author: Vincent Bonnevalle tiv.crb@gmail.com

@@ -253,7 +253,7 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = match e with | SortLevel (SLz) -> e | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (apply_inv_subst e s)) | SortLevel (SLlub (e1, e2)) - (* Should we use mkSLlub? *) + (* FIXME: use mkSLlub? *) -> mkSortLevel (mkSLlub' (apply_inv_subst e1 s, apply_inv_subst e2 s)) | Sort (l, Stype e) -> mkSort (l, Stype (apply_inv_subst e s)) | Sort (l, (StypeOmega | StypeLevel)) -> e

===================================== src/lexp.ml ===================================== @@ -640,7 +640,6 @@ and lexp_name e = type print_context_value = | Bool of bool | Int of int - | Expr of lexp option | Predtl of grammar (* precedence table *)

type print_context = print_context_value SMap.t @@ -655,8 +654,6 @@ let pretty_ppctx = ("color" , Bool (true) ); (* use console color to display hints *) ("separate_decl" , Bool (true) ); (* print newline between declarations *) ("indent_level" , Int (0) ); (* current indent level *) - ("parent" , Expr (None) ); (* parent expression *) - ("metavar" , Expr (None) ); (* metavar being printed *) ("col_max" , Int (80) ); (* col_size + col_ofsset <= col_max *) ("col_size" , Int (0) ); (* current column size *) ("col_ofsset" , Int (0) ); (* if col does not start at 0 *) @@ -678,8 +675,6 @@ let smap_bool s ctx = match SMap.find s ctx with Bool b -> b | _ -> failwith "Unreachable" and smap_int s ctx = match SMap.find s ctx with Int i -> i | _ -> failwith "Unreachable" -and smap_lexp s ctx = - match SMap.find s ctx with Expr e -> e | _ -> failwith "Unreachable" and smap_predtl s ctx = match SMap.find s ctx with Predtl tl -> tl | _ -> failwith "Unreachable"

@@ -690,8 +685,6 @@ let pp_size = smap_int "indent_size" let pp_color = smap_bool "color" let pp_decl = smap_bool "separate_decl" let pp_indent = smap_int "indent_level" -let pp_parent = smap_lexp "parent" -let pp_meta = smap_lexp "metavar" let pp_grammar = smap_predtl "grammar" let pp_colsize = smap_int "col_size" let pp_colmax = smap_int "col_max" @@ -701,8 +694,6 @@ let pp_implicit = smap_bool "print_implicit" let set_col_size p ctx = SMap.add "col_size" (Int p) ctx let add_col_size p ctx = set_col_size ((pp_colsize ctx) + p) ctx let reset_col_size ctx = set_col_size 0 ctx -let set_parent p ctx = SMap.add "parent" (Expr (Some p)) ctx -let set_meta p ctx = SMap.add "metavar" (Expr (Some p)) ctx let add_indent ctx i = SMap.add "indent_level" (Int ((pp_indent ctx) + i)) ctx

let pp_append_string buffer ctx str = @@ -752,7 +743,6 @@ and lexp_cstring ctx e = lexp_str ctx e (* Implementation *) and lexp_str ctx (exp : lexp) : string =

- let ctx = set_parent exp ctx in let inter_ctx = add_indent ctx 1 in let lexp_str' = lexp_str ctx in let lexp_stri idt e = lexp_str (add_indent ctx idt) e in @@ -814,15 +804,9 @@ and lexp_str ctx (exp : lexp) : string =

| Metavar (idx, subst, (loc, name)) (* print metavar result if any *) - -> (let print_meta exp = - let ctx = set_meta exp ctx in - lexp_str ctx (clean exp) in - - match pp_meta ctx with - | None -> print_meta exp - | Some e when e != exp -> print_meta exp - | _ -> - "?" ^ maybename name ^ (subst_string subst) ^ (index idx)) + -> (match metavar_lookup idx with + | MVal e -> lexp_str ctx e + | _ -> "?" ^ maybename name ^ (subst_string subst) ^ (index idx))

| Let (_, decls, body) -> (* Print first decls without indent *)

===================================== src/opslexp.ml ===================================== @@ -113,7 +113,7 @@ let lexp_close lctx e = * - It turns the lctx (of O(log N) access time) into a subst * (of O(N) access time) * Oh well! *) - L.clean (mkSusp e (lctx_to_subst lctx)) + mkSusp e (lctx_to_subst lctx)

(** Reduce to weak head normal form. @@ -231,6 +231,7 @@ let level_canon e = | SortLevel SLz -> if c < d then (d, m) else acc | SortLevel (SLsucc e) -> canon e (d + 1) acc | SortLevel (SLlub (e1, e2)) -> canon e1 d (canon e2 d acc) + (* FIXME: Apply substitutions from surrounding `Let` bindings. *) | Var (_, i) -> add_var_depth i d acc | Metavar (i, s, _) -> (match metavar_lookup i with @@ -263,8 +264,8 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = -> (match (sl1, sl2) with | (SLz, SLz) -> true | (SLsucc sl1, SLsucc sl2) -> conv_p sl1 sl2 - | _ -> let ce1 = level_canon (L.clean e1') in - let ce2 = level_canon (L.clean e2') in + | _ -> let ce1 = level_canon e1' in + let ce2 = level_canon e2' in level_leq ce1 ce2 && level_leq ce2 ce1) | (Sort (_, s1), Sort (_, s2)) -> s1 == s2 @@ -334,8 +335,8 @@ let rec mkSLlub ctx e1 e2 = | (SortLevel (SLsucc e1), SortLevel (SLsucc e2)) -> mkSortLevel (SLsucc (mkSLlub ctx e1 e2)) | (e1', e2') - -> let ce1 = level_canon (L.clean e1') in - let ce2 = level_canon (L.clean e2') in + -> let ce1 = level_canon e1' in + let ce2 = level_canon e2' in if level_leq ce1 ce2 then e2 else if level_leq ce2 ce1 then e1 else mkSortLevel (mkSLlub' (e1, e2)) (* FIXME: Could be more canonical *) @@ -420,9 +421,9 @@ let rec check'' erased ctx e = if conv_p ctx t t' then () else (error_tc ~loc:(lexp_location e) ("Type mismatch for " - ^ lexp_string (L.clean e) ^ " : " - ^ lexp_string (L.clean t) ^ " != " - ^ lexp_string (L.clean t')); + ^ lexp_string e ^ " : " + ^ lexp_string t ^ " != " + ^ lexp_string t'); (* Log.internal_error "Type mismatch" *)) in let check_type erased ctx t = let s = check erased ctx t in @@ -939,7 +940,11 @@ let rec erase_type (lxp: L.lexp): E.elexp = | L.Sort _ -> E.Type lxp (* Still useful to some extent. *) | L.Inductive(l, label, _, _) -> E.Type lxp - | L.Metavar _ -> Log.internal_error "Metavar in erase_type" + | Metavar (idx, s, _) + -> (match metavar_lookup idx with + | MVal e -> erase_type (push_susp e s) + | MVar (_, t, _) + -> Log.internal_error "Metavar in erase_type")

and filter_arg_list lst = let rec filter_arg_list lst acc =

===================================== src/unification.ml ===================================== @@ -296,8 +296,8 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) | _ -> log_info ?loc:None ("Unification of metavar type failed:\n " - ^ lexp_string (Lexp.clean t) ^ " != " - ^ lexp_string (Lexp.clean (OL.get_type ctx lxp)) + ^ lexp_string t ^ " != " + ^ lexp_string (OL.get_type ctx lxp) ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); [(CKresidual, ctx, lxp1, lxp2)] in match lxp2 with

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/886a3589162b84e04cf636842392550547...