# HG changeset patch # User haftmann # Date 1743942041 -7200 # Node ID 741f6f6df1449c74974e6e96c01c6fd718f0dbd8 # Parent 2aab65a687ec1a43587a1c24b2f7bcacc6eb5589 reflect nested lists in variables names diff -r 2aab65a687ec -r 741f6f6df144 src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Sat Apr 05 23:51:52 2025 +0200 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Sun Apr 06 14:20:41 2025 +0200 @@ -645,7 +645,7 @@ (*assumption: dummy values are not relevant for serialization*) val unitT = \<^type_name>\unit\ `%% []; val unitt = - IConst { sym = Code_Symbol.Constant \<^const_name>\Unity\, typargs = [], dicts = [], dom = [], + IConst { sym = Code_Symbol.Constant \<^const_name>\Unity\, typargs = [], dictss = [], dom = [], annotation = NONE, range = unitT }; fun dest_abs ((v, ty) `|=> (t, _), _) = ((v, ty), t) | dest_abs (t, ty) = diff -r 2aab65a687ec -r 741f6f6df144 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Sat Apr 05 23:51:52 2025 +0200 +++ b/src/Tools/Code/code_haskell.ML Sun Apr 06 14:20:41 2025 +0200 @@ -252,7 +252,7 @@ val vars = reserved |> intro_vars (map_filter I (s :: vs)); val lhs = IConst { sym = Constant classparam, typargs = [], - dicts = [], dom = dom, range = range, annotation = NONE } `$$ map IVar vs; + dictss = [], dom = dom, range = range, annotation = NONE } `$$ map IVar vs; (*dictionaries are not relevant in Haskell, and these consts never need type annotations for disambiguation *) in diff -r 2aab65a687ec -r 741f6f6df144 src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Sat Apr 05 23:51:52 2025 +0200 +++ b/src/Tools/Code/code_ml.ML Sun Apr 06 14:20:41 2025 +0200 @@ -86,10 +86,10 @@ brackify fxy [Pretty.enum " o" "(" ")" (map (Pretty.str o deresolve_classrel) classrels), brackify BR ps] fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) = print_classrels fxy classrels (print_plain_dict is_pseudo_fun fxy x) - and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) = + and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dictss)) = ((Pretty.str o deresolve_inst) inst :: (if is_pseudo_fun (Class_Instance inst) then [Pretty.str "()"] - else map_filter (print_dicts is_pseudo_fun BR o snd) dss)) + else map_filter (print_dicts is_pseudo_fun BR o snd) dictss)) | print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length, ... }) = [Pretty.str (if length = 1 then Name.enforce_case true var ^ "_" else Name.enforce_case true var ^ string_of_int (index + 1) ^ "_")] @@ -123,7 +123,7 @@ then print_case is_pseudo_fun some_thm vars fxy case_expr else print_app is_pseudo_fun some_thm vars fxy app | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr) - and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts, dom, ... }, ts)) = + and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dictss, dom, ... }, ts)) = if is_constr sym then let val wanted = length dom in if wanted < 2 orelse length ts = wanted @@ -133,7 +133,7 @@ end else if is_pseudo_fun sym then (Pretty.str o deresolve) sym @@ Pretty.str "()" - else (Pretty.str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts + else (Pretty.str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dictss @ map (print_term is_pseudo_fun some_thm vars BR) ts and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun) (print_term is_pseudo_fun) const_syntax some_thm vars @@ -412,10 +412,10 @@ fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) = print_plain_dict is_pseudo_fun fxy x |> print_classrels classrels - and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) = + and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dictss)) = brackify BR ((Pretty.str o deresolve_inst) inst :: (if is_pseudo_fun (Class_Instance inst) then [Pretty.str "()"] - else map_filter (print_dicts is_pseudo_fun BR o snd) dss)) + else map_filter (print_dicts is_pseudo_fun BR o snd) dictss)) | print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length, ... }) = Pretty.str (if length = 1 then "_" ^ Name.enforce_case true var else "_" ^ Name.enforce_case true var ^ string_of_int (index + 1)) @@ -446,7 +446,7 @@ then print_case is_pseudo_fun some_thm vars fxy case_expr else print_app is_pseudo_fun some_thm vars fxy app | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr) - and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts, dom, ... }, ts)) = + and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dictss, dom, ... }, ts)) = if is_constr sym then let val wanted = length dom in if length ts = wanted @@ -456,7 +456,7 @@ end else if is_pseudo_fun sym then (Pretty.str o deresolve) sym @@ Pretty.str "()" - else (Pretty.str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts + else (Pretty.str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dictss @ map (print_term is_pseudo_fun some_thm vars BR) ts and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun) (print_term is_pseudo_fun) const_syntax some_thm vars @@ -580,11 +580,11 @@ | print_def is_pseudo_fun _ definer (ML_Instance (inst as (tyco, class), { vs, superinsts, inst_params, ... })) = let - fun print_super_instance (super_class, dss) = + fun print_super_instance (super_class, dictss) = concat [ (Pretty.str o deresolve_classrel) (class, super_class), Pretty.str "=", - print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), dss))) + print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), dictss))) ]; fun print_classparam_instance ((classparam, (const, _)), (thm, _)) = concat [ diff -r 2aab65a687ec -r 741f6f6df144 src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Sat Apr 05 23:51:52 2025 +0200 +++ b/src/Tools/Code/code_preproc.ML Sun Apr 06 14:20:41 2025 +0200 @@ -511,7 +511,7 @@ (* applying instantiations *) -fun dicts_of ctxt (proj_sort, algebra) (T, sort) = +fun dictss_of ctxt (proj_sort, algebra) (T, sort) = let val thy = Proof_Context.theory_of ctxt; fun class_relation _ (x, _) _ = x; @@ -558,7 +558,7 @@ val algebra = Sorts.subalgebra (Context.Theory thy) (is_proper_class thy) (AList.lookup (op =) arities') (Sign.classes_of thy); val (rhss, eqngr') = Symtab.fold (add_cert ctxt vardeps) eqntab ([], eqngr); - fun deps_of (c, rhs) = c :: maps (dicts_of ctxt algebra) + fun deps_of (c, rhs) = c :: maps (dictss_of ctxt algebra) (rhs ~~ sortargs eqngr' c); val eqngr'' = fold (fn (c, rhs) => fold (curry Graph.add_edge c) (deps_of rhs)) rhss eqngr'; diff -r 2aab65a687ec -r 741f6f6df144 src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Sat Apr 05 23:51:52 2025 +0200 +++ b/src/Tools/Code/code_scala.ML Sun Apr 06 14:20:41 2025 +0200 @@ -74,14 +74,14 @@ fun print_var vars NONE = Pretty.str "_" | print_var vars (SOME v) = (Pretty.str o lookup_var vars) v; fun applify_dict tyvars (Dict (_, d)) = applify_plain_dict tyvars d - and applify_plain_dict tyvars (Dict_Const (inst, dss)) = - applify_dictss tyvars ((Pretty.str o deresolve o Class_Instance) inst) (map snd dss) + and applify_plain_dict tyvars (Dict_Const (inst, dictss)) = + applify_dictss tyvars ((Pretty.str o deresolve o Class_Instance) inst) (map snd dictss) | applify_plain_dict tyvars (Dict_Var { var, class, ... }) = Pretty.block [Pretty.str "implicitly", Pretty.enclose "[" "]" [Pretty.block [(Pretty.str o deresolve_class) class, Pretty.enclose "[" "]" [(Pretty.str o lookup_tyvar tyvars) var]]]] - and applify_dictss tyvars p dss = - applify "(" ")" (applify_dict tyvars) NOBR p (flat dss) + and applify_dictss tyvars p dictss = + applify "(" ")" (applify_dict tyvars) NOBR p (flat dictss) fun print_term tyvars is_pat some_thm vars fxy (IConst const) = print_app tyvars is_pat some_thm vars fxy (const, []) | print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) = @@ -115,7 +115,7 @@ ], vars') end and print_app tyvars is_pat some_thm vars fxy - (app as (const as { sym, typargs, dom, dicts, ... }, ts)) = + (app as (const as { sym, typargs, dom, dictss, ... }, ts)) = let val typargs' = if is_pat then [] else typargs; val syntax = case sym of @@ -123,7 +123,7 @@ | _ => NONE; val applify_dicts = if is_pat orelse is_some syntax orelse is_constr sym - orelse Code_Thingol.unambiguous_dictss dicts + orelse Code_Thingol.unambiguous_dictss dictss then fn p => K p else applify_dictss tyvars; val (wanted, print') = case syntax of @@ -131,12 +131,12 @@ (gen_applify (is_constr sym) "(" ")" (print_term tyvars is_pat some_thm vars NOBR) fxy (applify "[" "]" (print_typ tyvars NOBR) - NOBR ((Pretty.str o deresolve) sym) typargs') ts) dicts) + NOBR ((Pretty.str o deresolve) sym) typargs') ts) dictss) | SOME (k, Plain_printer s) => (k, fn fxy => fn ts => applify_dicts (applify "(" ")" (print_term tyvars is_pat some_thm vars NOBR) fxy (applify "[" "]" (print_typ tyvars NOBR) - NOBR (Pretty.str s) typargs') ts) dicts) + NOBR (Pretty.str s) typargs') ts) dictss) | SOME (k, Complex_printer print) => (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy (ts ~~ take k dom)) diff -r 2aab65a687ec -r 741f6f6df144 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Sat Apr 05 23:51:52 2025 +0200 +++ b/src/Tools/Code/code_thingol.ML Sun Apr 06 14:20:41 2025 +0200 @@ -24,7 +24,7 @@ and plain_dict = Dict_Const of (string * class) * (itype * dict list) list | Dict_Var of { var: vname, index: int, length: int, class: class, unique: bool } - type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list, + type const = { sym: Code_Symbol.T, typargs: itype list, dictss: dict list list, dom: itype list, range: itype, annotation: itype option } datatype iterm = IConst of const @@ -160,7 +160,7 @@ val (tys3, tys2) = chop n tys1; in (tys3, tys2 `--> ty1) end; -type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list, +type const = { sym: Code_Symbol.T, typargs: itype list, dictss: dict list list, dom: itype list, range: itype, annotation: itype option }; datatype iterm = @@ -350,11 +350,11 @@ in distill vs_map (map IVar vs) body end; fun exists_dict_var f (Dict (_, d)) = exists_plain_dict_var_pred f d -and exists_plain_dict_var_pred f (Dict_Const (_, dss)) = exists_dictss_var f (map snd dss) +and exists_plain_dict_var_pred f (Dict_Const (_, dictss)) = exists_dictss_var f (map snd dictss) | exists_plain_dict_var_pred f (Dict_Var x) = f x and exists_dictss_var f = (exists o exists) (exists_dict_var f); -fun contains_dict_var (IConst { dicts = dss, ... }) = exists_dictss_var (K true) dss +fun contains_dict_var (IConst { dictss = dictss, ... }) = exists_dictss_var (K true) dictss | contains_dict_var (IVar _) = false | contains_dict_var (t1 `$ t2) = contains_dict_var t1 orelse contains_dict_var t2 | contains_dict_var (_ `|=> (t, _)) = contains_dict_var t @@ -560,8 +560,8 @@ let fun class_relation unique (Weakening (classrels, x), sub_class) super_class = Weakening ((sub_class, super_class) :: classrels, brand_unique unique x); - fun type_constructor (tyco, typs) dss class = - Weakening ([], Global ((tyco, class), typs ~~ (map o map) fst dss)); + fun type_constructor (tyco, typs) dictss class = + Weakening ([], Global ((tyco, class), typs ~~ (map o map) fst dictss)); fun type_variable (TFree (v, sort)) = let val sort' = proj_sort sort; @@ -662,7 +662,7 @@ fun translate_super_instance super_class = ensure_class ctxt algbr eqngr permissive super_class ##>> translate_dicts ctxt algbr eqngr permissive NONE (arity_typ, [super_class]) - #>> (fn (super_class, [Dict ([], Dict_Const (_, dss))]) => (super_class, dss)); + #>> (fn (super_class, [Dict ([], Dict_Const (_, dictss))]) => (super_class, dictss)); fun translate_classparam_instance (c, ty) = let val raw_const = Const (c, map_type_tfree (K arity_typ') ty); @@ -739,8 +739,8 @@ ||>> fold_map (translate_typ ctxt algbr eqngr permissive) typargs ||>> fold_map (translate_dicts ctxt algbr eqngr permissive some_thm) (typargs ~~ sorts) ||>> fold_map (translate_typ ctxt algbr eqngr permissive) (range :: dom) - |>> (fn (((c, typargs), dss), range :: dom) => - { sym = Constant c, typargs = typargs, dicts = dss, + |>> (fn (((c, typargs), dictss), range :: dom) => + { sym = Constant c, typargs = typargs, dictss = dictss, dom = dom, range = range, annotation = if annotate then SOME (dom `--> range) else NONE }) end @@ -806,11 +806,11 @@ fold_map (ensure_classrel ctxt algbr eqngr permissive) classrels ##>> translate_plain_dict d #>> Dict - and translate_plain_dict (Global (inst, dss)) = + and translate_plain_dict (Global (inst, dictss)) = ensure_inst ctxt algbr eqngr permissive inst - ##>> fold_map (fn (ty, ds) => + ##>> fold_map (fn (ty, dicts) => translate_typ ctxt algbr eqngr permissive ty - ##>> fold_map translate_dict ds) dss + ##>> fold_map translate_dict dicts) dictss #>> Dict_Const | translate_plain_dict (Local { var, index, sort, unique }) = ensure_class ctxt algbr eqngr permissive (nth sort index) diff -r 2aab65a687ec -r 741f6f6df144 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Sat Apr 05 23:51:52 2025 +0200 +++ b/src/Tools/nbe.ML Sun Apr 06 14:20:41 2025 +0200 @@ -344,10 +344,10 @@ fun apply_constr sym = nbe_apps_constr (constr_fun_ident sym); fun apply_constmatch sym = nbe_apps_constmatch (constr_fun_ident sym); - fun assemble_constapp sym tys dicts ts = + fun assemble_constapp sym tys dictss ts = let val s_tys = map (assemble_type) tys; - val ts' = (maps o map) assemble_dict (map2 (fn ty => map (fn dict => (ty, dict))) tys dicts) @ ts; + val ts' = (maps o map) assemble_dict (map2 (fn ty => map (fn dict => (ty, dict))) tys dictss) @ ts; in case AList.lookup (op =) eqnss sym of SOME (num_args, _) => if num_args <= length ts' then let val (ts1, ts2) = chop num_args ts' @@ -361,13 +361,13 @@ fold_rev (fn classrel => assemble_constapp (Class_Relation classrel) [] [] o single) classrels and assemble_dict (ty, Dict (classrels, x)) = assemble_classrels classrels (assemble_plain_dict ty x) - and assemble_plain_dict (_ `%% tys) (Dict_Const (inst, dicts)) = - assemble_constapp (Class_Instance inst) tys (map snd dicts) [] + and assemble_plain_dict (_ `%% tys) (Dict_Const (inst, dictss)) = + assemble_constapp (Class_Instance inst) tys (map snd dictss) [] | assemble_plain_dict _ (Dict_Var { var, index, ... }) = nbe_dict var index - fun assemble_constmatch sym _ dicts ts = - apply_constmatch sym ((maps o map) (K "_") dicts @ ts); + fun assemble_constmatch sym _ dictss ts = + apply_constmatch sym ((maps o map) (K "_") dictss @ ts); fun assemble_iterm constapp = let @@ -375,7 +375,7 @@ let val (t', ts) = Code_Thingol.unfold_app t in of_iapp match_continuation t' (fold_rev (cons o of_iterm NONE) ts []) end - and of_iapp match_continuation (IConst { sym, typargs = tys, dicts, ... }) ts = constapp sym tys dicts ts + and of_iapp match_continuation (IConst { sym, typargs = tys, dictss, ... }) ts = constapp sym tys dictss ts | of_iapp match_continuation (IVar v) ts = nbe_apps (nbe_bound_optional v) ts | of_iapp match_continuation ((v, _) `|=> (t, _)) ts = nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts @@ -446,8 +446,8 @@ (* extraction of equations from statements *) -fun dummy_const sym tys dicts = - IConst { sym = sym, typargs = tys, dicts = dicts, +fun dummy_const sym tys dictss = + IConst { sym = sym, typargs = tys, dictss = dictss, dom = [], annotation = NONE, range = ITyVar "" }; fun eqns_of_stmt (_, Code_Thingol.NoStmt) = @@ -475,8 +475,8 @@ [] | eqns_of_stmt (sym_inst, Code_Thingol.Classinst { class, tyco, vs, superinsts, inst_params, ... }) = [(sym_inst, (vs, [([], dummy_const (Type_Class class) [] [] `$$ - map (fn (class, dicts) => - dummy_const (Class_Instance (tyco, class)) (map (ITyVar o fst) vs) (map snd dicts)) superinsts + map (fn (class, dictss) => + dummy_const (Class_Instance (tyco, class)) (map (ITyVar o fst) vs) (map snd dictss)) superinsts @ map (IConst o fst o snd o fst) inst_params)]))];