1.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Mon Oct 05 11:48:06 2009 +0200
1.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Mon Oct 05 16:55:56 2009 +0200
1.3 @@ -28,7 +28,7 @@
1.4
1.5 (*the kind of distinctiveness axioms depends on number of constructors*)
1.6 val (distinctness_limit, distinctness_limit_setup) =
1.7 - Attrib.config_int "datatype_distinctness_limit" 7;
1.8 + Attrib.config_int "datatype_distinctness_limit" 9999 (*approx. infinity*);
1.9
1.10 val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
1.11
2.1 --- a/src/Pure/Isar/code.ML Mon Oct 05 11:48:06 2009 +0200
2.2 +++ b/src/Pure/Isar/code.ML Mon Oct 05 16:55:56 2009 +0200
2.3 @@ -13,7 +13,6 @@
2.4 val read_const: theory -> string -> string
2.5 val string_of_const: theory -> string -> string
2.6 val args_number: theory -> string -> int
2.7 - val typscheme: theory -> string * typ -> (string * sort) list * typ
2.8
2.9 (*constructor sets*)
2.10 val constrset_of_consts: theory -> (string * typ) list
2.11 @@ -28,6 +27,7 @@
2.12 -> (thm * bool) list -> (thm * bool) list
2.13 val const_typ_eqn: theory -> thm -> string * typ
2.14 val typscheme_eqn: theory -> thm -> (string * sort) list * typ
2.15 + val typscheme_eqns: theory -> string -> thm list -> (string * sort) list * typ
2.16
2.17 (*executable code*)
2.18 val add_datatype: (string * typ) list -> theory -> theory
2.19 @@ -112,10 +112,6 @@
2.20
2.21 fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy;
2.22
2.23 -fun typscheme thy (c, ty) =
2.24 - let
2.25 - val ty' = Logic.unvarifyT ty;
2.26 - in (map dest_TFree (Sign.const_typargs thy (c, ty')), Type.strip_sorts ty') end;
2.27
2.28
2.29 (** data store **)
2.30 @@ -511,9 +507,22 @@
2.31 val (c, ty) = head_eqn thm;
2.32 val c' = AxClass.unoverload_const thy (c, ty);
2.33 in (c', ty) end;
2.34 +fun const_eqn thy = fst o const_typ_eqn thy;
2.35
2.36 -fun typscheme_eqn thy = typscheme thy o const_typ_eqn thy;
2.37 -fun const_eqn thy = fst o const_typ_eqn thy;
2.38 +fun typscheme thy (c, ty) =
2.39 + (map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty);
2.40 +fun typscheme_eqn thy = typscheme thy o apsnd Logic.unvarifyT o const_typ_eqn thy;
2.41 +fun typscheme_eqns thy c [] =
2.42 + let
2.43 + val raw_ty = Sign.the_const_type thy c;
2.44 + val tvars = Term.add_tvar_namesT raw_ty [];
2.45 + val tvars' = case AxClass.class_of_param thy c
2.46 + of SOME class => [TFree (Name.aT, [class])]
2.47 + | NONE => Name.invent_list [] Name.aT (length tvars)
2.48 + |> map (fn v => TFree (v, []));
2.49 + val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty;
2.50 + in typscheme thy (c, ty) end
2.51 + | typscheme_eqns thy c (thms as thm :: _) = typscheme_eqn thy thm;
2.52
2.53 fun assert_eqns_const thy c eqns =
2.54 let
3.1 --- a/src/Tools/Code/code_preproc.ML Mon Oct 05 11:48:06 2009 +0200
3.2 +++ b/src/Tools/Code/code_preproc.ML Mon Oct 05 16:55:56 2009 +0200
3.3 @@ -19,7 +19,7 @@
3.4 type code_algebra
3.5 type code_graph
3.6 val eqns: code_graph -> string -> (thm * bool) list
3.7 - val typ: code_graph -> string -> (string * sort) list * typ
3.8 + val sortargs: code_graph -> string -> sort list
3.9 val all: code_graph -> string list
3.10 val pretty: theory -> code_graph -> Pretty.T
3.11 val obtain: theory -> string list -> term list -> code_algebra * code_graph
3.12 @@ -62,7 +62,7 @@
3.13 val empty = make_thmproc ((Simplifier.empty_ss, Simplifier.empty_ss), []);
3.14 fun copy spec = spec;
3.15 val extend = copy;
3.16 - fun merge pp = merge_thmproc;
3.17 + fun merge _ = merge_thmproc;
3.18 );
3.19
3.20 fun the_thmproc thy = case Code_Preproc_Data.get thy
3.21 @@ -196,10 +196,10 @@
3.22 (** sort algebra and code equation graph types **)
3.23
3.24 type code_algebra = (sort -> sort) * Sorts.algebra;
3.25 -type code_graph = (((string * sort) list * typ) * (thm * bool) list) Graph.T;
3.26 +type code_graph = ((string * sort) list * (thm * bool) list) Graph.T;
3.27
3.28 fun eqns eqngr = these o Option.map snd o try (Graph.get_node eqngr);
3.29 -fun typ eqngr = fst o Graph.get_node eqngr;
3.30 +fun sortargs eqngr = map snd o fst o Graph.get_node eqngr
3.31 fun all eqngr = Graph.keys eqngr;
3.32
3.33 fun pretty thy eqngr =
3.34 @@ -227,25 +227,12 @@
3.35 map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
3.36 o maps (#params o AxClass.get_info thy);
3.37
3.38 -fun consts_of thy eqns = [] |> (fold o fold o fold_aterms)
3.39 - (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I)
3.40 - (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns);
3.41 -
3.42 -fun default_typscheme_of thy c =
3.43 +fun typscheme_rhss thy c eqns =
3.44 let
3.45 - val ty = (snd o dest_Const o Term_Subst.zero_var_indexes o curry Const c
3.46 - o Type.strip_sorts o Sign.the_const_type thy) c;
3.47 - in case AxClass.class_of_param thy c
3.48 - of SOME class => ([(Name.aT, [class])], ty)
3.49 - | NONE => Code.typscheme thy (c, ty)
3.50 - end;
3.51 -
3.52 -fun tyscm_rhss_of thy c eqns =
3.53 - let
3.54 - val tyscm = case eqns
3.55 - of [] => default_typscheme_of thy c
3.56 - | ((thm, _) :: _) => Code.typscheme_eqn thy thm;
3.57 - val rhss = consts_of thy eqns;
3.58 + val tyscm = Code.typscheme_eqns thy c (map fst eqns);
3.59 + val rhss = [] |> (fold o fold o fold_aterms)
3.60 + (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I)
3.61 + (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns);
3.62 in (tyscm, rhss) end;
3.63
3.64
3.65 @@ -283,11 +270,11 @@
3.66
3.67 fun obtain_eqns thy eqngr c =
3.68 case try (Graph.get_node eqngr) c
3.69 - of SOME ((lhs, _), eqns) => ((lhs, []), [])
3.70 + of SOME (lhs, eqns) => ((lhs, []), [])
3.71 | NONE => let
3.72 val eqns = Code.these_eqns thy c
3.73 |> preprocess thy c;
3.74 - val ((lhs, _), rhss) = tyscm_rhss_of thy c eqns;
3.75 + val ((lhs, _), rhss) = typscheme_rhss thy c eqns;
3.76 in ((lhs, rhss), eqns) end;
3.77
3.78 fun obtain_instance thy arities (inst as (class, tyco)) =
3.79 @@ -434,11 +421,11 @@
3.80 Vartab.update ((v, 0), sort)) lhs;
3.81 val eqns = proto_eqns
3.82 |> (map o apfst) (inst_thm thy inst_tab);
3.83 - val (tyscm, rhss') = tyscm_rhss_of thy c eqns;
3.84 - val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr;
3.85 + val ((vs, _), rhss') = typscheme_rhss thy c eqns;
3.86 + val eqngr' = Graph.new_node (c, (vs, eqns)) eqngr;
3.87 in (map (pair c) rhss' @ rhss, eqngr') end;
3.88
3.89 -fun extend_arities_eqngr thy cs ts (arities, eqngr) =
3.90 +fun extend_arities_eqngr thy cs ts (arities, (eqngr : code_graph)) =
3.91 let
3.92 val cs_rhss = (fold o fold_aterms) (fn Const (c_ty as (c, _)) =>
3.93 insert (op =) (c, (map (styp_of NONE) o Sign.const_typargs thy) c_ty) | _ => I) ts [];
3.94 @@ -451,7 +438,7 @@
3.95 (AList.lookup (op =) arities') (Sign.classes_of thy);
3.96 val (rhss, eqngr') = Symtab.fold (add_eqs thy vardeps) eqntab ([], eqngr);
3.97 fun deps_of (c, rhs) = c :: maps (dicts_of thy algebra)
3.98 - (rhs ~~ (map snd o fst o fst o Graph.get_node eqngr') c);
3.99 + (rhs ~~ sortargs eqngr' c);
3.100 val eqngr'' = fold (fn (c, rhs) => fold
3.101 (curry Graph.add_edge c) (deps_of rhs)) rhss eqngr';
3.102 in (algebra, (arities', eqngr'')) end;
4.1 --- a/src/Tools/Code/code_thingol.ML Mon Oct 05 11:48:06 2009 +0200
4.2 +++ b/src/Tools/Code/code_thingol.ML Mon Oct 05 16:55:56 2009 +0200
4.3 @@ -533,57 +533,62 @@
4.4
4.5 (* translation *)
4.6
4.7 -fun ensure_tyco thy algbr funcgr tyco =
4.8 +fun ensure_tyco thy algbr eqngr tyco =
4.9 let
4.10 val stmt_datatype =
4.11 let
4.12 val (vs, cos) = Code.get_datatype thy tyco;
4.13 in
4.14 - fold_map (translate_tyvar_sort thy algbr funcgr) vs
4.15 + fold_map (translate_tyvar_sort thy algbr eqngr) vs
4.16 ##>> fold_map (fn (c, tys) =>
4.17 - ensure_const thy algbr funcgr c
4.18 - ##>> fold_map (translate_typ thy algbr funcgr) tys) cos
4.19 + ensure_const thy algbr eqngr c
4.20 + ##>> fold_map (translate_typ thy algbr eqngr) tys) cos
4.21 #>> (fn info => Datatype (tyco, info))
4.22 end;
4.23 in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end
4.24 -and ensure_const thy algbr funcgr c =
4.25 +and ensure_const thy algbr eqngr c =
4.26 let
4.27 fun stmt_datatypecons tyco =
4.28 - ensure_tyco thy algbr funcgr tyco
4.29 + ensure_tyco thy algbr eqngr tyco
4.30 #>> (fn tyco => Datatypecons (c, tyco));
4.31 fun stmt_classparam class =
4.32 - ensure_class thy algbr funcgr class
4.33 + ensure_class thy algbr eqngr class
4.34 #>> (fn class => Classparam (c, class));
4.35 - fun stmt_fun ((vs, ty), eqns) =
4.36 - fold_map (translate_tyvar_sort thy algbr funcgr) vs
4.37 - ##>> translate_typ thy algbr funcgr ty
4.38 - ##>> fold_map (translate_eqn thy algbr funcgr) (burrow_fst (clean_thms thy) eqns)
4.39 - #>> (fn info => Fun (c, info));
4.40 + fun stmt_fun raw_eqns =
4.41 + let
4.42 + val eqns = burrow_fst (clean_thms thy) raw_eqns;
4.43 + val (vs, ty) = Code.typscheme_eqns thy c (map fst eqns);
4.44 + in
4.45 + fold_map (translate_tyvar_sort thy algbr eqngr) vs
4.46 + ##>> translate_typ thy algbr eqngr ty
4.47 + ##>> fold_map (translate_eqn thy algbr eqngr) eqns
4.48 + #>> (fn info => Fun (c, info))
4.49 + end;
4.50 val stmt_const = case Code.get_datatype_of_constr thy c
4.51 of SOME tyco => stmt_datatypecons tyco
4.52 | NONE => (case AxClass.class_of_param thy c
4.53 of SOME class => stmt_classparam class
4.54 - | NONE => stmt_fun (Code_Preproc.typ funcgr c, Code_Preproc.eqns funcgr c))
4.55 + | NONE => stmt_fun (Code_Preproc.eqns eqngr c))
4.56 in ensure_stmt lookup_const (declare_const thy) stmt_const c end
4.57 -and ensure_class thy (algbr as (_, algebra)) funcgr class =
4.58 +and ensure_class thy (algbr as (_, algebra)) eqngr class =
4.59 let
4.60 val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
4.61 val cs = #params (AxClass.get_info thy class);
4.62 val stmt_class =
4.63 - fold_map (fn superclass => ensure_class thy algbr funcgr superclass
4.64 - ##>> ensure_classrel thy algbr funcgr (class, superclass)) superclasses
4.65 - ##>> fold_map (fn (c, ty) => ensure_const thy algbr funcgr c
4.66 - ##>> translate_typ thy algbr funcgr ty) cs
4.67 + fold_map (fn superclass => ensure_class thy algbr eqngr superclass
4.68 + ##>> ensure_classrel thy algbr eqngr (class, superclass)) superclasses
4.69 + ##>> fold_map (fn (c, ty) => ensure_const thy algbr eqngr c
4.70 + ##>> translate_typ thy algbr eqngr ty) cs
4.71 #>> (fn info => Class (class, (unprefix "'" Name.aT, info)))
4.72 in ensure_stmt lookup_class (declare_class thy) stmt_class class end
4.73 -and ensure_classrel thy algbr funcgr (subclass, superclass) =
4.74 +and ensure_classrel thy algbr eqngr (subclass, superclass) =
4.75 let
4.76 val stmt_classrel =
4.77 - ensure_class thy algbr funcgr subclass
4.78 - ##>> ensure_class thy algbr funcgr superclass
4.79 + ensure_class thy algbr eqngr subclass
4.80 + ##>> ensure_class thy algbr eqngr superclass
4.81 #>> Classrel;
4.82 in ensure_stmt lookup_classrel (declare_classrel thy) stmt_classrel (subclass, superclass) end
4.83 -and ensure_inst thy (algbr as (_, algebra)) funcgr (class, tyco) =
4.84 +and ensure_inst thy (algbr as (_, algebra)) eqngr (class, tyco) =
4.85 let
4.86 val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
4.87 val classparams = these (try (#params o AxClass.get_info thy) class);
4.88 @@ -594,9 +599,9 @@
4.89 val arity_typ = Type (tyco, map TFree vs);
4.90 val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
4.91 fun translate_superarity superclass =
4.92 - ensure_class thy algbr funcgr superclass
4.93 - ##>> ensure_classrel thy algbr funcgr (class, superclass)
4.94 - ##>> translate_dicts thy algbr funcgr NONE (arity_typ, [superclass])
4.95 + ensure_class thy algbr eqngr superclass
4.96 + ##>> ensure_classrel thy algbr eqngr (class, superclass)
4.97 + ##>> translate_dicts thy algbr eqngr NONE (arity_typ, [superclass])
4.98 #>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
4.99 (superclass, (classrel, (inst, dss))));
4.100 fun translate_classparam_inst (c, ty) =
4.101 @@ -606,73 +611,73 @@
4.102 val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd
4.103 o Logic.dest_equals o Thm.prop_of) thm;
4.104 in
4.105 - ensure_const thy algbr funcgr c
4.106 - ##>> translate_const thy algbr funcgr (SOME thm) c_ty
4.107 + ensure_const thy algbr eqngr c
4.108 + ##>> translate_const thy algbr eqngr (SOME thm) c_ty
4.109 #>> (fn (c, IConst c_inst) => ((c, c_inst), (thm, true)))
4.110 end;
4.111 val stmt_inst =
4.112 - ensure_class thy algbr funcgr class
4.113 - ##>> ensure_tyco thy algbr funcgr tyco
4.114 - ##>> fold_map (translate_tyvar_sort thy algbr funcgr) vs
4.115 + ensure_class thy algbr eqngr class
4.116 + ##>> ensure_tyco thy algbr eqngr tyco
4.117 + ##>> fold_map (translate_tyvar_sort thy algbr eqngr) vs
4.118 ##>> fold_map translate_superarity superclasses
4.119 ##>> fold_map translate_classparam_inst classparams
4.120 #>> (fn ((((class, tyco), arity), superarities), classparams) =>
4.121 Classinst ((class, (tyco, arity)), (superarities, classparams)));
4.122 in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
4.123 -and translate_typ thy algbr funcgr (TFree (v, _)) =
4.124 +and translate_typ thy algbr eqngr (TFree (v, _)) =
4.125 pair (ITyVar (unprefix "'" v))
4.126 - | translate_typ thy algbr funcgr (Type (tyco, tys)) =
4.127 - ensure_tyco thy algbr funcgr tyco
4.128 - ##>> fold_map (translate_typ thy algbr funcgr) tys
4.129 + | translate_typ thy algbr eqngr (Type (tyco, tys)) =
4.130 + ensure_tyco thy algbr eqngr tyco
4.131 + ##>> fold_map (translate_typ thy algbr eqngr) tys
4.132 #>> (fn (tyco, tys) => tyco `%% tys)
4.133 -and translate_term thy algbr funcgr thm (Const (c, ty)) =
4.134 - translate_app thy algbr funcgr thm ((c, ty), [])
4.135 - | translate_term thy algbr funcgr thm (Free (v, _)) =
4.136 +and translate_term thy algbr eqngr thm (Const (c, ty)) =
4.137 + translate_app thy algbr eqngr thm ((c, ty), [])
4.138 + | translate_term thy algbr eqngr thm (Free (v, _)) =
4.139 pair (IVar (SOME v))
4.140 - | translate_term thy algbr funcgr thm (Abs (v, ty, t)) =
4.141 + | translate_term thy algbr eqngr thm (Abs (v, ty, t)) =
4.142 let
4.143 val (v', t') = Syntax.variant_abs (Name.desymbolize false v, ty, t);
4.144 val v'' = if member (op =) (Term.add_free_names t' []) v'
4.145 then SOME v' else NONE
4.146 in
4.147 - translate_typ thy algbr funcgr ty
4.148 - ##>> translate_term thy algbr funcgr thm t'
4.149 + translate_typ thy algbr eqngr ty
4.150 + ##>> translate_term thy algbr eqngr thm t'
4.151 #>> (fn (ty, t) => (v'', ty) `|=> t)
4.152 end
4.153 - | translate_term thy algbr funcgr thm (t as _ $ _) =
4.154 + | translate_term thy algbr eqngr thm (t as _ $ _) =
4.155 case strip_comb t
4.156 of (Const (c, ty), ts) =>
4.157 - translate_app thy algbr funcgr thm ((c, ty), ts)
4.158 + translate_app thy algbr eqngr thm ((c, ty), ts)
4.159 | (t', ts) =>
4.160 - translate_term thy algbr funcgr thm t'
4.161 - ##>> fold_map (translate_term thy algbr funcgr thm) ts
4.162 + translate_term thy algbr eqngr thm t'
4.163 + ##>> fold_map (translate_term thy algbr eqngr thm) ts
4.164 #>> (fn (t, ts) => t `$$ ts)
4.165 -and translate_eqn thy algbr funcgr (thm, proper) =
4.166 +and translate_eqn thy algbr eqngr (thm, proper) =
4.167 let
4.168 val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
4.169 o Logic.unvarify o prop_of) thm;
4.170 in
4.171 - fold_map (translate_term thy algbr funcgr (SOME thm)) args
4.172 - ##>> translate_term thy algbr funcgr (SOME thm) rhs
4.173 + fold_map (translate_term thy algbr eqngr (SOME thm)) args
4.174 + ##>> translate_term thy algbr eqngr (SOME thm) rhs
4.175 #>> rpair (thm, proper)
4.176 end
4.177 -and translate_const thy algbr funcgr thm (c, ty) =
4.178 +and translate_const thy algbr eqngr thm (c, ty) =
4.179 let
4.180 val tys = Sign.const_typargs thy (c, ty);
4.181 - val sorts = (map snd o fst o Code_Preproc.typ funcgr) c;
4.182 + val sorts = Code_Preproc.sortargs eqngr c;
4.183 val tys_args = (fst o Term.strip_type) ty;
4.184 in
4.185 - ensure_const thy algbr funcgr c
4.186 - ##>> fold_map (translate_typ thy algbr funcgr) tys
4.187 - ##>> fold_map (translate_dicts thy algbr funcgr thm) (tys ~~ sorts)
4.188 - ##>> fold_map (translate_typ thy algbr funcgr) tys_args
4.189 + ensure_const thy algbr eqngr c
4.190 + ##>> fold_map (translate_typ thy algbr eqngr) tys
4.191 + ##>> fold_map (translate_dicts thy algbr eqngr thm) (tys ~~ sorts)
4.192 + ##>> fold_map (translate_typ thy algbr eqngr) tys_args
4.193 #>> (fn (((c, tys), iss), tys_args) => IConst (c, ((tys, iss), tys_args)))
4.194 end
4.195 -and translate_app_const thy algbr funcgr thm (c_ty, ts) =
4.196 - translate_const thy algbr funcgr thm c_ty
4.197 - ##>> fold_map (translate_term thy algbr funcgr thm) ts
4.198 +and translate_app_const thy algbr eqngr thm (c_ty, ts) =
4.199 + translate_const thy algbr eqngr thm c_ty
4.200 + ##>> fold_map (translate_term thy algbr eqngr thm) ts
4.201 #>> (fn (t, ts) => t `$$ ts)
4.202 -and translate_case thy algbr funcgr thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
4.203 +and translate_case thy algbr eqngr thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
4.204 let
4.205 fun arg_types num_args ty = (fst o chop num_args o fst o strip_type) ty;
4.206 val tys = arg_types num_args (snd c_ty);
4.207 @@ -716,14 +721,14 @@
4.208 (constrs ~~ ts_clause);
4.209 in ((t, ty), clauses) end;
4.210 in
4.211 - translate_const thy algbr funcgr thm c_ty
4.212 - ##>> fold_map (fn (constr, n) => translate_const thy algbr funcgr thm constr #>> rpair n) constrs
4.213 - ##>> translate_typ thy algbr funcgr ty
4.214 - ##>> fold_map (translate_term thy algbr funcgr thm) ts
4.215 + translate_const thy algbr eqngr thm c_ty
4.216 + ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr thm constr #>> rpair n) constrs
4.217 + ##>> translate_typ thy algbr eqngr ty
4.218 + ##>> fold_map (translate_term thy algbr eqngr thm) ts
4.219 #-> (fn (((t, constrs), ty), ts) =>
4.220 `(fn (_, (naming, _)) => ICase (casify naming constrs ty ts, t `$$ ts)))
4.221 end
4.222 -and translate_app_case thy algbr funcgr thm (case_scheme as (num_args, _)) ((c, ty), ts) =
4.223 +and translate_app_case thy algbr eqngr thm (case_scheme as (num_args, _)) ((c, ty), ts) =
4.224 if length ts < num_args then
4.225 let
4.226 val k = length ts;
4.227 @@ -731,24 +736,24 @@
4.228 val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
4.229 val vs = Name.names ctxt "a" tys;
4.230 in
4.231 - fold_map (translate_typ thy algbr funcgr) tys
4.232 - ##>> translate_case thy algbr funcgr thm case_scheme ((c, ty), ts @ map Free vs)
4.233 + fold_map (translate_typ thy algbr eqngr) tys
4.234 + ##>> translate_case thy algbr eqngr thm case_scheme ((c, ty), ts @ map Free vs)
4.235 #>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t)
4.236 end
4.237 else if length ts > num_args then
4.238 - translate_case thy algbr funcgr thm case_scheme ((c, ty), Library.take (num_args, ts))
4.239 - ##>> fold_map (translate_term thy algbr funcgr thm) (Library.drop (num_args, ts))
4.240 + translate_case thy algbr eqngr thm case_scheme ((c, ty), Library.take (num_args, ts))
4.241 + ##>> fold_map (translate_term thy algbr eqngr thm) (Library.drop (num_args, ts))
4.242 #>> (fn (t, ts) => t `$$ ts)
4.243 else
4.244 - translate_case thy algbr funcgr thm case_scheme ((c, ty), ts)
4.245 -and translate_app thy algbr funcgr thm (c_ty_ts as ((c, _), _)) =
4.246 + translate_case thy algbr eqngr thm case_scheme ((c, ty), ts)
4.247 +and translate_app thy algbr eqngr thm (c_ty_ts as ((c, _), _)) =
4.248 case Code.get_case_scheme thy c
4.249 - of SOME case_scheme => translate_app_case thy algbr funcgr thm case_scheme c_ty_ts
4.250 - | NONE => translate_app_const thy algbr funcgr thm c_ty_ts
4.251 -and translate_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
4.252 - fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
4.253 + of SOME case_scheme => translate_app_case thy algbr eqngr thm case_scheme c_ty_ts
4.254 + | NONE => translate_app_const thy algbr eqngr thm c_ty_ts
4.255 +and translate_tyvar_sort thy (algbr as (proj_sort, _)) eqngr (v, sort) =
4.256 + fold_map (ensure_class thy algbr eqngr) (proj_sort sort)
4.257 #>> (fn sort => (unprefix "'" v, sort))
4.258 -and translate_dicts thy (algbr as (proj_sort, algebra)) funcgr thm (ty, sort) =
4.259 +and translate_dicts thy (algbr as (proj_sort, algebra)) eqngr thm (ty, sort) =
4.260 let
4.261 datatype typarg =
4.262 Global of (class * string) * typarg list list
4.263 @@ -768,11 +773,11 @@
4.264 type_variable = type_variable} (ty, proj_sort sort)
4.265 handle Sorts.CLASS_ERROR e => not_wellsorted thy thm ty sort e;
4.266 fun mk_dict (Global (inst, yss)) =
4.267 - ensure_inst thy algbr funcgr inst
4.268 + ensure_inst thy algbr eqngr inst
4.269 ##>> (fold_map o fold_map) mk_dict yss
4.270 #>> (fn (inst, dss) => DictConst (inst, dss))
4.271 | mk_dict (Local (classrels, (v, (n, sort)))) =
4.272 - fold_map (ensure_classrel thy algbr funcgr) classrels
4.273 + fold_map (ensure_classrel thy algbr eqngr) classrels
4.274 #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (n, length sort))))
4.275 in fold_map mk_dict typargs end;
4.276
4.277 @@ -795,9 +800,9 @@
4.278
4.279 val cached_program = Program.get;
4.280
4.281 -fun invoke_generation thy (algebra, funcgr) f name =
4.282 +fun invoke_generation thy (algebra, eqngr) f name =
4.283 Program.change_yield thy (fn naming_program => (NONE, naming_program)
4.284 - |> f thy algebra funcgr name
4.285 + |> f thy algebra eqngr name
4.286 |-> (fn name => fn (_, naming_program) => (name, naming_program)));
4.287
4.288
4.289 @@ -809,8 +814,8 @@
4.290 let
4.291 val cs_all = Graph.all_succs program cs;
4.292 in (cs, (naming, Graph.subgraph (member (op =) cs_all) program)) end;
4.293 - fun generate_consts thy algebra funcgr =
4.294 - fold_map (ensure_const thy algebra funcgr);
4.295 + fun generate_consts thy algebra eqngr =
4.296 + fold_map (ensure_const thy algebra eqngr);
4.297 in
4.298 invoke_generation thy (Code_Preproc.obtain thy cs []) generate_consts cs
4.299 |-> project_consts
4.300 @@ -819,15 +824,15 @@
4.301
4.302 (* value evaluation *)
4.303
4.304 -fun ensure_value thy algbr funcgr t =
4.305 +fun ensure_value thy algbr eqngr t =
4.306 let
4.307 val ty = fastype_of t;
4.308 val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
4.309 o dest_TFree))) t [];
4.310 val stmt_value =
4.311 - fold_map (translate_tyvar_sort thy algbr funcgr) vs
4.312 - ##>> translate_typ thy algbr funcgr ty
4.313 - ##>> translate_term thy algbr funcgr NONE t
4.314 + fold_map (translate_tyvar_sort thy algbr eqngr) vs
4.315 + ##>> translate_typ thy algbr eqngr ty
4.316 + ##>> translate_term thy algbr eqngr NONE t
4.317 #>> (fn ((vs, ty), t) => Fun
4.318 (Term.dummy_patternN, ((vs, ty), [(([], t), (Drule.dummy_thm, true))])));
4.319 fun term_value (dep, (naming, program1)) =
4.320 @@ -845,10 +850,10 @@
4.321 #> term_value
4.322 end;
4.323
4.324 -fun base_evaluator thy evaluator algebra funcgr vs t =
4.325 +fun base_evaluator thy evaluator algebra eqngr vs t =
4.326 let
4.327 val (((naming, program), (((vs', ty'), t'), deps)), _) =
4.328 - invoke_generation thy (algebra, funcgr) ensure_value t;
4.329 + invoke_generation thy (algebra, eqngr) ensure_value t;
4.330 val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs';
4.331 in evaluator naming program ((vs'', (vs', ty')), t') deps end;
4.332