1.1 --- a/src/HOL/Tools/refute.ML Thu Sep 02 17:12:16 2010 +0200
1.2 +++ b/src/HOL/Tools/refute.ML Fri Sep 03 10:58:11 2010 +0200
1.3 @@ -25,34 +25,34 @@
1.4
1.5 exception MAXVARS_EXCEEDED
1.6
1.7 - val add_interpreter : string -> (theory -> model -> arguments -> term ->
1.8 + val add_interpreter : string -> (Proof.context -> model -> arguments -> term ->
1.9 (interpretation * model * arguments) option) -> theory -> theory
1.10 - val add_printer : string -> (theory -> model -> typ ->
1.11 + val add_printer : string -> (Proof.context -> model -> typ ->
1.12 interpretation -> (int -> bool) -> term option) -> theory -> theory
1.13
1.14 - val interpret : theory -> model -> arguments -> term ->
1.15 + val interpret : Proof.context -> model -> arguments -> term ->
1.16 (interpretation * model * arguments)
1.17
1.18 - val print : theory -> model -> typ -> interpretation -> (int -> bool) -> term
1.19 - val print_model : theory -> model -> (int -> bool) -> string
1.20 + val print : Proof.context -> model -> typ -> interpretation -> (int -> bool) -> term
1.21 + val print_model : Proof.context -> model -> (int -> bool) -> string
1.22
1.23 (* ------------------------------------------------------------------------- *)
1.24 (* Interface *)
1.25 (* ------------------------------------------------------------------------- *)
1.26
1.27 val set_default_param : (string * string) -> theory -> theory
1.28 - val get_default_param : theory -> string -> string option
1.29 - val get_default_params : theory -> (string * string) list
1.30 - val actual_params : theory -> (string * string) list -> params
1.31 + val get_default_param : Proof.context -> string -> string option
1.32 + val get_default_params : Proof.context -> (string * string) list
1.33 + val actual_params : Proof.context -> (string * string) list -> params
1.34
1.35 - val find_model : theory -> params -> term list -> term -> bool -> unit
1.36 + val find_model : Proof.context -> params -> term list -> term -> bool -> unit
1.37
1.38 (* tries to find a model for a formula: *)
1.39 val satisfy_term :
1.40 - theory -> (string * string) list -> term list -> term -> unit
1.41 + Proof.context -> (string * string) list -> term list -> term -> unit
1.42 (* tries to find a model that refutes a formula: *)
1.43 val refute_term :
1.44 - theory -> (string * string) list -> term list -> term -> unit
1.45 + Proof.context -> (string * string) list -> term list -> term -> unit
1.46 val refute_goal :
1.47 Proof.context -> (string * string) list -> thm -> int -> unit
1.48
1.49 @@ -74,7 +74,6 @@
1.50 val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ
1.51 end;
1.52
1.53 -
1.54 structure Refute : REFUTE =
1.55 struct
1.56
1.57 @@ -207,12 +206,12 @@
1.58 };
1.59
1.60
1.61 -structure RefuteData = Theory_Data
1.62 +structure Data = Theory_Data
1.63 (
1.64 type T =
1.65 - {interpreters: (string * (theory -> model -> arguments -> term ->
1.66 + {interpreters: (string * (Proof.context -> model -> arguments -> term ->
1.67 (interpretation * model * arguments) option)) list,
1.68 - printers: (string * (theory -> model -> typ -> interpretation ->
1.69 + printers: (string * (Proof.context -> model -> typ -> interpretation ->
1.70 (int -> bool) -> term option)) list,
1.71 parameters: string Symtab.table};
1.72 val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
1.73 @@ -225,6 +224,8 @@
1.74 parameters = Symtab.merge (op=) (pa1, pa2)};
1.75 );
1.76
1.77 +val get_data = Data.get o ProofContext.theory_of;
1.78 +
1.79
1.80 (* ------------------------------------------------------------------------- *)
1.81 (* interpret: interprets the term 't' using a suitable interpreter; returns *)
1.82 @@ -232,14 +233,11 @@
1.83 (* track of the interpretation of subterms *)
1.84 (* ------------------------------------------------------------------------- *)
1.85
1.86 -(* theory -> model -> arguments -> Term.term ->
1.87 - (interpretation * model * arguments) *)
1.88 -
1.89 -fun interpret thy model args t =
1.90 - case get_first (fn (_, f) => f thy model args t)
1.91 - (#interpreters (RefuteData.get thy)) of
1.92 +fun interpret ctxt model args t =
1.93 + case get_first (fn (_, f) => f ctxt model args t)
1.94 + (#interpreters (get_data ctxt)) of
1.95 NONE => raise REFUTE ("interpret",
1.96 - "no interpreter for term " ^ quote (Syntax.string_of_term_global thy t))
1.97 + "no interpreter for term " ^ quote (Syntax.string_of_term ctxt t))
1.98 | SOME x => x;
1.99
1.100 (* ------------------------------------------------------------------------- *)
1.101 @@ -247,14 +245,11 @@
1.102 (* type 'T', into a term using a suitable printer *)
1.103 (* ------------------------------------------------------------------------- *)
1.104
1.105 -(* theory -> model -> Term.typ -> interpretation -> (int -> bool) ->
1.106 - Term.term *)
1.107 -
1.108 -fun print thy model T intr assignment =
1.109 - case get_first (fn (_, f) => f thy model T intr assignment)
1.110 - (#printers (RefuteData.get thy)) of
1.111 +fun print ctxt model T intr assignment =
1.112 + case get_first (fn (_, f) => f ctxt model T intr assignment)
1.113 + (#printers (get_data ctxt)) of
1.114 NONE => raise REFUTE ("print",
1.115 - "no printer for type " ^ quote (Syntax.string_of_typ_global thy T))
1.116 + "no printer for type " ^ quote (Syntax.string_of_typ ctxt T))
1.117 | SOME x => x;
1.118
1.119 (* ------------------------------------------------------------------------- *)
1.120 @@ -263,9 +258,7 @@
1.121 (* printers *)
1.122 (* ------------------------------------------------------------------------- *)
1.123
1.124 -(* theory -> model -> (int -> bool) -> string *)
1.125 -
1.126 -fun print_model thy model assignment =
1.127 +fun print_model ctxt model assignment =
1.128 let
1.129 val (typs, terms) = model
1.130 val typs_msg =
1.131 @@ -273,7 +266,7 @@
1.132 "empty universe (no type variables in term)\n"
1.133 else
1.134 "Size of types: " ^ commas (map (fn (T, i) =>
1.135 - Syntax.string_of_typ_global thy T ^ ": " ^ string_of_int i) typs) ^ "\n"
1.136 + Syntax.string_of_typ ctxt T ^ ": " ^ string_of_int i) typs) ^ "\n"
1.137 val show_consts_msg =
1.138 if not (!show_consts) andalso Library.exists (is_Const o fst) terms then
1.139 "set \"show_consts\" to show the interpretation of constants\n"
1.140 @@ -286,9 +279,9 @@
1.141 cat_lines (map_filter (fn (t, intr) =>
1.142 (* print constants only if 'show_consts' is true *)
1.143 if (!show_consts) orelse not (is_Const t) then
1.144 - SOME (Syntax.string_of_term_global thy t ^ ": " ^
1.145 - Syntax.string_of_term_global thy
1.146 - (print thy model (Term.type_of t) intr assignment))
1.147 + SOME (Syntax.string_of_term ctxt t ^ ": " ^
1.148 + Syntax.string_of_term ctxt
1.149 + (print ctxt model (Term.type_of t) intr assignment))
1.150 else
1.151 NONE) terms) ^ "\n"
1.152 in
1.153 @@ -300,71 +293,49 @@
1.154 (* PARAMETER MANAGEMENT *)
1.155 (* ------------------------------------------------------------------------- *)
1.156
1.157 -(* string -> (theory -> model -> arguments -> Term.term ->
1.158 - (interpretation * model * arguments) option) -> theory -> theory *)
1.159 +fun add_interpreter name f = Data.map (fn {interpreters, printers, parameters} =>
1.160 + case AList.lookup (op =) interpreters name of
1.161 + NONE => {interpreters = (name, f) :: interpreters,
1.162 + printers = printers, parameters = parameters}
1.163 + | SOME _ => error ("Interpreter " ^ name ^ " already declared"));
1.164
1.165 -fun add_interpreter name f thy =
1.166 - let
1.167 - val {interpreters, printers, parameters} = RefuteData.get thy
1.168 - in
1.169 - case AList.lookup (op =) interpreters name of
1.170 - NONE => RefuteData.put {interpreters = (name, f) :: interpreters,
1.171 - printers = printers, parameters = parameters} thy
1.172 - | SOME _ => error ("Interpreter " ^ name ^ " already declared")
1.173 - end;
1.174 -
1.175 -(* string -> (theory -> model -> Term.typ -> interpretation ->
1.176 - (int -> bool) -> Term.term option) -> theory -> theory *)
1.177 -
1.178 -fun add_printer name f thy =
1.179 - let
1.180 - val {interpreters, printers, parameters} = RefuteData.get thy
1.181 - in
1.182 - case AList.lookup (op =) printers name of
1.183 - NONE => RefuteData.put {interpreters = interpreters,
1.184 - printers = (name, f) :: printers, parameters = parameters} thy
1.185 - | SOME _ => error ("Printer " ^ name ^ " already declared")
1.186 - end;
1.187 +fun add_printer name f = Data.map (fn {interpreters, printers, parameters} =>
1.188 + case AList.lookup (op =) printers name of
1.189 + NONE => {interpreters = interpreters,
1.190 + printers = (name, f) :: printers, parameters = parameters}
1.191 + | SOME _ => error ("Printer " ^ name ^ " already declared"));
1.192
1.193 (* ------------------------------------------------------------------------- *)
1.194 -(* set_default_param: stores the '(name, value)' pair in RefuteData's *)
1.195 +(* set_default_param: stores the '(name, value)' pair in Data's *)
1.196 (* parameter table *)
1.197 (* ------------------------------------------------------------------------- *)
1.198
1.199 -(* (string * string) -> theory -> theory *)
1.200 -
1.201 -fun set_default_param (name, value) = RefuteData.map
1.202 +fun set_default_param (name, value) = Data.map
1.203 (fn {interpreters, printers, parameters} =>
1.204 {interpreters = interpreters, printers = printers,
1.205 parameters = Symtab.update (name, value) parameters});
1.206
1.207 (* ------------------------------------------------------------------------- *)
1.208 (* get_default_param: retrieves the value associated with 'name' from *)
1.209 -(* RefuteData's parameter table *)
1.210 +(* Data's parameter table *)
1.211 (* ------------------------------------------------------------------------- *)
1.212
1.213 -(* theory -> string -> string option *)
1.214 -
1.215 -val get_default_param = Symtab.lookup o #parameters o RefuteData.get;
1.216 +val get_default_param = Symtab.lookup o #parameters o get_data;
1.217
1.218 (* ------------------------------------------------------------------------- *)
1.219 (* get_default_params: returns a list of all '(name, value)' pairs that are *)
1.220 -(* stored in RefuteData's parameter table *)
1.221 +(* stored in Data's parameter table *)
1.222 (* ------------------------------------------------------------------------- *)
1.223
1.224 -(* theory -> (string * string) list *)
1.225 -
1.226 -val get_default_params = Symtab.dest o #parameters o RefuteData.get;
1.227 +val get_default_params = Symtab.dest o #parameters o get_data;
1.228
1.229 (* ------------------------------------------------------------------------- *)
1.230 (* actual_params: takes a (possibly empty) list 'params' of parameters that *)
1.231 -(* override the default parameters currently specified in 'thy', and *)
1.232 +(* override the default parameters currently specified, and *)
1.233 (* returns a record that can be passed to 'find_model'. *)
1.234 (* ------------------------------------------------------------------------- *)
1.235
1.236 -(* theory -> (string * string) list -> params *)
1.237 -
1.238 -fun actual_params thy override =
1.239 +fun actual_params ctxt override =
1.240 let
1.241 (* (string * string) list * string -> bool *)
1.242 fun read_bool (parms, name) =
1.243 @@ -393,7 +364,7 @@
1.244 " must be assigned a value")
1.245 (* 'override' first, defaults last: *)
1.246 (* (string * string) list *)
1.247 - val allparams = override @ (get_default_params thy)
1.248 + val allparams = override @ get_default_params ctxt
1.249 (* int *)
1.250 val minsize = read_int (allparams, "minsize")
1.251 val maxsize = read_int (allparams, "maxsize")
1.252 @@ -458,8 +429,6 @@
1.253 (* denotes membership to an axiomatic type class *)
1.254 (* ------------------------------------------------------------------------- *)
1.255
1.256 -(* theory -> string * Term.typ -> bool *)
1.257 -
1.258 fun is_const_of_class thy (s, T) =
1.259 let
1.260 val class_const_names = map Logic.const_of_class (Sign.all_classes thy)
1.261 @@ -474,8 +443,6 @@
1.262 (* of an inductive datatype in 'thy' *)
1.263 (* ------------------------------------------------------------------------- *)
1.264
1.265 -(* theory -> string * Term.typ -> bool *)
1.266 -
1.267 fun is_IDT_constructor thy (s, T) =
1.268 (case body_type T of
1.269 Type (s', _) =>
1.270 @@ -491,8 +458,6 @@
1.271 (* operator of an inductive datatype in 'thy' *)
1.272 (* ------------------------------------------------------------------------- *)
1.273
1.274 -(* theory -> string * Term.typ -> bool *)
1.275 -
1.276 fun is_IDT_recursor thy (s, T) =
1.277 let
1.278 val rec_names = Symtab.fold (append o #rec_names o snd)
1.279 @@ -521,8 +486,6 @@
1.280 (* get_def: looks up the definition of a constant *)
1.281 (* ------------------------------------------------------------------------- *)
1.282
1.283 -(* theory -> string * Term.typ -> (string * Term.term) option *)
1.284 -
1.285 fun get_def thy (s, T) =
1.286 let
1.287 (* (string * Term.term) list -> (string * Term.term) option *)
1.288 @@ -554,8 +517,6 @@
1.289 (* get_typedef: looks up the definition of a type, as created by "typedef" *)
1.290 (* ------------------------------------------------------------------------- *)
1.291
1.292 -(* theory -> Term.typ -> (string * Term.term) option *)
1.293 -
1.294 fun get_typedef thy T =
1.295 let
1.296 (* (string * Term.term) list -> (string * Term.term) option *)
1.297 @@ -581,7 +542,7 @@
1.298 case type_of_type_definition ax of
1.299 SOME T' =>
1.300 let
1.301 - val T'' = (domain_type o domain_type) T'
1.302 + val T'' = domain_type (domain_type T')
1.303 val typeSubs = Sign.typ_match thy (T'', T) Vartab.empty
1.304 in
1.305 SOME (axname, monomorphic_term typeSubs ax)
1.306 @@ -599,8 +560,6 @@
1.307 (* created by the "axclass" command *)
1.308 (* ------------------------------------------------------------------------- *)
1.309
1.310 -(* theory -> string -> (string * Term.term) option *)
1.311 -
1.312 fun get_classdef thy class =
1.313 let
1.314 val axname = class ^ "_class_def"
1.315 @@ -617,8 +576,6 @@
1.316 (* that definition does not need to be unfolded *)
1.317 (* ------------------------------------------------------------------------- *)
1.318
1.319 -(* theory -> Term.term -> Term.term *)
1.320 -
1.321 (* Note: we could intertwine unfolding of constants and beta-(eta-) *)
1.322 (* normalization; this would save some unfolding for terms where *)
1.323 (* constants are eliminated by beta-reduction (e.g. 'K c1 c2'). On *)
1.324 @@ -716,8 +673,6 @@
1.325 (* *every* axiom of the theory and collect it if it has a constant/ *)
1.326 (* type/typeclass in common with the term 't'. *)
1.327
1.328 -(* theory -> Term.term -> Term.term list *)
1.329 -
1.330 (* Which axioms are "relevant" for a particular term/type goes hand in *)
1.331 (* hand with the interpretation of that term/type by its interpreter (see *)
1.332 (* way below): if the interpretation respects an axiom anyway, the axiom *)
1.333 @@ -726,8 +681,9 @@
1.334 (* To avoid collecting the same axiom multiple times, we use an *)
1.335 (* accumulator 'axs' which contains all axioms collected so far. *)
1.336
1.337 -fun collect_axioms thy t =
1.338 +fun collect_axioms ctxt t =
1.339 let
1.340 + val thy = ProofContext.theory_of ctxt
1.341 val _ = tracing "Adding axioms..."
1.342 val axioms = Theory.all_axioms_of thy
1.343 fun collect_this_axiom (axname, ax) axs =
1.344 @@ -744,7 +700,7 @@
1.345 TFree (_, sort) => sort
1.346 | TVar (_, sort) => sort
1.347 | _ => raise REFUTE ("collect_axioms",
1.348 - "type " ^ Syntax.string_of_typ_global thy T ^ " is not a variable"))
1.349 + "type " ^ Syntax.string_of_typ ctxt T ^ " is not a variable"))
1.350 (* obtain axioms for all superclasses *)
1.351 val superclasses = sort @ maps (Sign.super_classes thy) sort
1.352 (* merely an optimization, because 'collect_this_axiom' disallows *)
1.353 @@ -762,7 +718,7 @@
1.354 | [(idx, S)] => (axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax)
1.355 | _ =>
1.356 raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^
1.357 - Syntax.string_of_term_global thy ax ^
1.358 + Syntax.string_of_term ctxt ax ^
1.359 ") contains more than one type variable")))
1.360 class_axioms
1.361 in
1.362 @@ -865,13 +821,14 @@
1.363 val ax_in = SOME (specialize_type thy (s, T) of_class)
1.364 (* type match may fail due to sort constraints *)
1.365 handle Type.TYPE_MATCH => NONE
1.366 - val ax_1 = Option.map (fn ax => (Syntax.string_of_term_global thy ax, ax)) ax_in
1.367 + val ax_1 = Option.map (fn ax => (Syntax.string_of_term ctxt ax, ax)) ax_in
1.368 val ax_2 = Option.map (apsnd (specialize_type thy (s, T))) (get_classdef thy class)
1.369 in
1.370 collect_type_axioms T (fold collect_this_axiom (map_filter I [ax_1, ax_2]) axs)
1.371 end
1.372 else if is_IDT_constructor thy (s, T)
1.373 - orelse is_IDT_recursor thy (s, T) then
1.374 + orelse is_IDT_recursor thy (s, T)
1.375 + then
1.376 (* only collect relevant type axioms *)
1.377 collect_type_axioms T axs
1.378 else
1.379 @@ -899,8 +856,9 @@
1.380 (* and all mutually recursive IDTs are considered. *)
1.381 (* ------------------------------------------------------------------------- *)
1.382
1.383 -fun ground_types thy t =
1.384 +fun ground_types ctxt t =
1.385 let
1.386 + val thy = ProofContext.theory_of ctxt
1.387 fun collect_types T acc =
1.388 (case T of
1.389 Type ("fun", [T1, T2]) => collect_types T1 (collect_types T2 acc)
1.390 @@ -918,7 +876,7 @@
1.391 val _ = if Library.exists (fn d =>
1.392 case d of Datatype_Aux.DtTFree _ => false | _ => true) typs then
1.393 raise REFUTE ("ground_types", "datatype argument (for type "
1.394 - ^ Syntax.string_of_typ_global thy T ^ ") is not a variable")
1.395 + ^ Syntax.string_of_typ ctxt T ^ ") is not a variable")
1.396 else ()
1.397 (* required for mutually recursive datatypes; those need to *)
1.398 (* be added even if they are an instance of an otherwise non- *)
1.399 @@ -1081,19 +1039,17 @@
1.400 (* find_model: repeatedly calls 'interpret' with appropriate parameters, *)
1.401 (* applies a SAT solver, and (in case a model is found) displays *)
1.402 (* the model to the user by calling 'print_model' *)
1.403 -(* thy : the current theory *)
1.404 (* {...} : parameters that control the translation/model generation *)
1.405 (* assm_ts : assumptions to be considered unless "no_assms" is specified *)
1.406 (* t : term to be translated into a propositional formula *)
1.407 (* negate : if true, find a model that makes 't' false (rather than true) *)
1.408 (* ------------------------------------------------------------------------- *)
1.409
1.410 -(* theory -> params -> Term.term -> bool -> unit *)
1.411 -
1.412 -fun find_model thy
1.413 +fun find_model ctxt
1.414 {sizes, minsize, maxsize, maxvars, maxtime, satsolver, no_assms, expect}
1.415 assm_ts t negate =
1.416 let
1.417 + val thy = ProofContext.theory_of ctxt
1.418 (* string -> unit *)
1.419 fun check_expect outcome_code =
1.420 if expect = "" orelse outcome_code = expect then ()
1.421 @@ -1107,13 +1063,13 @@
1.422 else if negate then Logic.list_implies (assm_ts, t)
1.423 else Logic.mk_conjunction_list (t :: assm_ts)
1.424 val u = unfold_defs thy t
1.425 - val _ = tracing ("Unfolded term: " ^ Syntax.string_of_term_global thy u)
1.426 - val axioms = collect_axioms thy u
1.427 + val _ = tracing ("Unfolded term: " ^ Syntax.string_of_term ctxt u)
1.428 + val axioms = collect_axioms ctxt u
1.429 (* Term.typ list *)
1.430 - val types = fold (union (op =) o ground_types thy) (u :: axioms) []
1.431 + val types = fold (union (op =) o ground_types ctxt) (u :: axioms) []
1.432 val _ = tracing ("Ground types: "
1.433 ^ (if null types then "none."
1.434 - else commas (map (Syntax.string_of_typ_global thy) types)))
1.435 + else commas (map (Syntax.string_of_typ ctxt) types)))
1.436 (* we can only consider fragments of recursive IDTs, so we issue a *)
1.437 (* warning if the formula contains a recursive IDT *)
1.438 (* TODO: no warning needed for /positive/ occurrences of IDTs *)
1.439 @@ -1152,7 +1108,7 @@
1.440 (* translate 'u' and all axioms *)
1.441 val (intrs, (model, args)) = fold_map (fn t' => fn (m, a) =>
1.442 let
1.443 - val (i, m', a') = interpret thy m a t'
1.444 + val (i, m', a') = interpret ctxt m a t'
1.445 in
1.446 (* set 'def_eq' to 'true' *)
1.447 (i, (m', {maxvars = #maxvars a', def_eq = true,
1.448 @@ -1180,7 +1136,7 @@
1.449 priority "Invoking SAT solver...";
1.450 (case solver fm of
1.451 SatSolver.SATISFIABLE assignment =>
1.452 - (priority ("*** Model found: ***\n" ^ print_model thy model
1.453 + (priority ("*** Model found: ***\n" ^ print_model ctxt model
1.454 (fn i => case assignment i of SOME b => b | NONE => true));
1.455 if maybe_spurious then "potential" else "genuine")
1.456 | SatSolver.UNSATISFIABLE _ =>
1.457 @@ -1225,7 +1181,7 @@
1.458 (* enter loop with or without time limit *)
1.459 priority ("Trying to find a model that "
1.460 ^ (if negate then "refutes" else "satisfies") ^ ": "
1.461 - ^ Syntax.string_of_term_global thy t);
1.462 + ^ Syntax.string_of_term ctxt t);
1.463 if maxtime > 0 then (
1.464 TimeLimit.timeLimit (Time.fromSeconds maxtime)
1.465 wrapper ()
1.466 @@ -1248,10 +1204,8 @@
1.467 (* parameters *)
1.468 (* ------------------------------------------------------------------------- *)
1.469
1.470 -(* theory -> (string * string) list -> Term.term list -> Term.term -> unit *)
1.471 -
1.472 -fun satisfy_term thy params assm_ts t =
1.473 - find_model thy (actual_params thy params) assm_ts t false;
1.474 +fun satisfy_term ctxt params assm_ts t =
1.475 + find_model ctxt (actual_params ctxt params) assm_ts t false;
1.476
1.477 (* ------------------------------------------------------------------------- *)
1.478 (* refute_term: calls 'find_model' to find a model that refutes 't' *)
1.479 @@ -1259,9 +1213,7 @@
1.480 (* parameters *)
1.481 (* ------------------------------------------------------------------------- *)
1.482
1.483 -(* theory -> (string * string) list -> Term.term list -> Term.term -> unit *)
1.484 -
1.485 -fun refute_term thy params assm_ts t =
1.486 +fun refute_term ctxt params assm_ts t =
1.487 let
1.488 (* disallow schematic type variables, since we cannot properly negate *)
1.489 (* terms containing them (their logical meaning is that there EXISTS a *)
1.490 @@ -1309,7 +1261,7 @@
1.491 val frees = Term.rename_wrt_term strip_t (strip_all_vars ex_closure)
1.492 val subst_t = Term.subst_bounds (map Free frees, strip_t)
1.493 in
1.494 - find_model thy (actual_params thy params) assm_ts subst_t true
1.495 + find_model ctxt (actual_params ctxt params) assm_ts subst_t true
1.496 end;
1.497
1.498 (* ------------------------------------------------------------------------- *)
1.499 @@ -1327,8 +1279,7 @@
1.500 val assms = map term_of (Assumption.all_assms_of ctxt)
1.501 val (t, frees) = Logic.goal_params t i
1.502 in
1.503 - refute_term (ProofContext.theory_of ctxt) params assms
1.504 - (subst_bounds (frees, t))
1.505 + refute_term ctxt params assms (subst_bounds (frees, t))
1.506 end
1.507 end
1.508
1.509 @@ -1343,9 +1294,7 @@
1.510 (* variables) *)
1.511 (* ------------------------------------------------------------------------- *)
1.512
1.513 -(* theory -> model -> Term.typ -> interpretation list *)
1.514 -
1.515 -fun make_constants thy model T =
1.516 +fun make_constants ctxt model T =
1.517 let
1.518 (* returns a list with all unit vectors of length n *)
1.519 (* int -> interpretation list *)
1.520 @@ -1376,7 +1325,7 @@
1.521 | make_constants_intr (Node xs) = map Node (pick_all (length xs)
1.522 (make_constants_intr (hd xs)))
1.523 (* obtain the interpretation for a variable of type 'T' *)
1.524 - val (i, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1,
1.525 + val (i, _, _) = interpret ctxt model {maxvars=0, def_eq=false, next_idx=1,
1.526 bounds=[], wellformed=True} (Free ("dummy", T))
1.527 in
1.528 make_constants_intr i
1.529 @@ -1387,8 +1336,6 @@
1.530 (* (make_constants T)', but implemented more efficiently) *)
1.531 (* ------------------------------------------------------------------------- *)
1.532
1.533 -(* theory -> model -> Term.typ -> int *)
1.534 -
1.535 (* returns 0 for an empty ground type or a function type with empty *)
1.536 (* codomain, but fails for a function type with empty domain -- *)
1.537 (* admissibility of datatype constructor argument types (see "Inductive *)
1.538 @@ -1397,14 +1344,14 @@
1.539 (* never occur as the domain of a function type that is the type of a *)
1.540 (* constructor argument *)
1.541
1.542 -fun size_of_type thy model T =
1.543 +fun size_of_type ctxt model T =
1.544 let
1.545 (* returns the number of elements that have the same tree structure as a *)
1.546 (* given interpretation *)
1.547 fun size_of_intr (Leaf xs) = length xs
1.548 | size_of_intr (Node xs) = Integer.pow (length xs) (size_of_intr (hd xs))
1.549 (* obtain the interpretation for a variable of type 'T' *)
1.550 - val (i, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1,
1.551 + val (i, _, _) = interpret ctxt model {maxvars=0, def_eq=false, next_idx=1,
1.552 bounds=[], wellformed=True} (Free ("dummy", T))
1.553 in
1.554 size_of_intr i
1.555 @@ -1585,9 +1532,9 @@
1.556 (* their arguments) of the size of the argument types *)
1.557 (* ------------------------------------------------------------------------- *)
1.558
1.559 -fun size_of_dtyp thy typ_sizes descr typ_assoc constructors =
1.560 +fun size_of_dtyp ctxt typ_sizes descr typ_assoc constructors =
1.561 Integer.sum (map (fn (_, dtyps) =>
1.562 - Integer.prod (map (size_of_type thy (typ_sizes, []) o
1.563 + Integer.prod (map (size_of_type ctxt (typ_sizes, []) o
1.564 (typ_of_dtyp descr typ_assoc)) dtyps))
1.565 constructors);
1.566
1.567 @@ -1596,14 +1543,12 @@
1.568 (* INTERPRETERS: Actual Interpreters *)
1.569 (* ------------------------------------------------------------------------- *)
1.570
1.571 -(* theory -> model -> arguments -> Term.term ->
1.572 - (interpretation * model * arguments) option *)
1.573 -
1.574 (* simply typed lambda calculus: Isabelle's basic term syntax, with type *)
1.575 (* variables, function types, and propT *)
1.576
1.577 -fun stlc_interpreter thy model args t =
1.578 +fun stlc_interpreter ctxt model args t =
1.579 let
1.580 + val thy = ProofContext.theory_of ctxt
1.581 val (typs, terms) = model
1.582 val {maxvars, def_eq, next_idx, bounds, wellformed} = args
1.583 (* Term.typ -> (interpretation * model * arguments) option *)
1.584 @@ -1651,7 +1596,7 @@
1.585 fun make_copies idx 0 = (idx, [], True)
1.586 | make_copies idx n =
1.587 let
1.588 - val (copy, _, new_args) = interpret thy (typs, [])
1.589 + val (copy, _, new_args) = interpret ctxt (typs, [])
1.590 {maxvars = maxvars, def_eq = false, next_idx = idx,
1.591 bounds = [], wellformed = True} (Free ("dummy", T2))
1.592 val (idx', copies, wf') = make_copies (#next_idx new_args) (n-1)
1.593 @@ -1659,7 +1604,7 @@
1.594 (idx', copy :: copies, SAnd (#wellformed new_args, wf'))
1.595 end
1.596 val (next, copies, wf) = make_copies next_idx
1.597 - (size_of_type thy model T1)
1.598 + (size_of_type ctxt model T1)
1.599 (* combine copies into a single interpretation *)
1.600 val intr = Node copies
1.601 in
1.602 @@ -1687,13 +1632,13 @@
1.603 | Abs (x, T, body) =>
1.604 let
1.605 (* create all constants of type 'T' *)
1.606 - val constants = make_constants thy model T
1.607 + val constants = make_constants ctxt model T
1.608 (* interpret the 'body' separately for each constant *)
1.609 val (bodies, (model', args')) = fold_map
1.610 (fn c => fn (m, a) =>
1.611 let
1.612 (* add 'c' to 'bounds' *)
1.613 - val (i', m', a') = interpret thy m {maxvars = #maxvars a,
1.614 + val (i', m', a') = interpret ctxt m {maxvars = #maxvars a,
1.615 def_eq = #def_eq a, next_idx = #next_idx a,
1.616 bounds = (c :: #bounds a), wellformed = #wellformed a} body
1.617 in
1.618 @@ -1710,21 +1655,18 @@
1.619 | t1 $ t2 =>
1.620 let
1.621 (* interpret 't1' and 't2' separately *)
1.622 - val (intr1, model1, args1) = interpret thy model args t1
1.623 - val (intr2, model2, args2) = interpret thy model1 args1 t2
1.624 + val (intr1, model1, args1) = interpret ctxt model args t1
1.625 + val (intr2, model2, args2) = interpret ctxt model1 args1 t2
1.626 in
1.627 SOME (interpretation_apply (intr1, intr2), model2, args2)
1.628 end)
1.629 end;
1.630
1.631 -(* theory -> model -> arguments -> Term.term ->
1.632 - (interpretation * model * arguments) option *)
1.633 -
1.634 -fun Pure_interpreter thy model args t =
1.635 +fun Pure_interpreter ctxt model args t =
1.636 case t of
1.637 Const (@{const_name all}, _) $ t1 =>
1.638 let
1.639 - val (i, m, a) = interpret thy model args t1
1.640 + val (i, m, a) = interpret ctxt model args t1
1.641 in
1.642 case i of
1.643 Node xs =>
1.644 @@ -1740,40 +1682,37 @@
1.645 "\"all\" is followed by a non-function")
1.646 end
1.647 | Const (@{const_name all}, _) =>
1.648 - SOME (interpret thy model args (eta_expand t 1))
1.649 + SOME (interpret ctxt model args (eta_expand t 1))
1.650 | Const (@{const_name "=="}, _) $ t1 $ t2 =>
1.651 let
1.652 - val (i1, m1, a1) = interpret thy model args t1
1.653 - val (i2, m2, a2) = interpret thy m1 a1 t2
1.654 + val (i1, m1, a1) = interpret ctxt model args t1
1.655 + val (i2, m2, a2) = interpret ctxt m1 a1 t2
1.656 in
1.657 (* we use either 'make_def_equality' or 'make_equality' *)
1.658 SOME ((if #def_eq args then make_def_equality else make_equality)
1.659 (i1, i2), m2, a2)
1.660 end
1.661 | Const (@{const_name "=="}, _) $ t1 =>
1.662 - SOME (interpret thy model args (eta_expand t 1))
1.663 + SOME (interpret ctxt model args (eta_expand t 1))
1.664 | Const (@{const_name "=="}, _) =>
1.665 - SOME (interpret thy model args (eta_expand t 2))
1.666 + SOME (interpret ctxt model args (eta_expand t 2))
1.667 | Const (@{const_name "==>"}, _) $ t1 $ t2 =>
1.668 (* 3-valued logic *)
1.669 let
1.670 - val (i1, m1, a1) = interpret thy model args t1
1.671 - val (i2, m2, a2) = interpret thy m1 a1 t2
1.672 + val (i1, m1, a1) = interpret ctxt model args t1
1.673 + val (i2, m2, a2) = interpret ctxt m1 a1 t2
1.674 val fmTrue = PropLogic.SOr (toFalse i1, toTrue i2)
1.675 val fmFalse = PropLogic.SAnd (toTrue i1, toFalse i2)
1.676 in
1.677 SOME (Leaf [fmTrue, fmFalse], m2, a2)
1.678 end
1.679 | Const (@{const_name "==>"}, _) $ t1 =>
1.680 - SOME (interpret thy model args (eta_expand t 1))
1.681 + SOME (interpret ctxt model args (eta_expand t 1))
1.682 | Const (@{const_name "==>"}, _) =>
1.683 - SOME (interpret thy model args (eta_expand t 2))
1.684 + SOME (interpret ctxt model args (eta_expand t 2))
1.685 | _ => NONE;
1.686
1.687 -(* theory -> model -> arguments -> Term.term ->
1.688 - (interpretation * model * arguments) option *)
1.689 -
1.690 -fun HOLogic_interpreter thy model args t =
1.691 +fun HOLogic_interpreter ctxt model args t =
1.692 (* Providing interpretations directly is more efficient than unfolding the *)
1.693 (* logical constants. In HOL however, logical constants can themselves be *)
1.694 (* arguments. They are then translated using eta-expansion. *)
1.695 @@ -1790,7 +1729,7 @@
1.696 SOME (FF, model, args)
1.697 | Const (@{const_name All}, _) $ t1 => (* similar to "all" (Pure) *)
1.698 let
1.699 - val (i, m, a) = interpret thy model args t1
1.700 + val (i, m, a) = interpret ctxt model args t1
1.701 in
1.702 case i of
1.703 Node xs =>
1.704 @@ -1806,10 +1745,10 @@
1.705 "\"All\" is followed by a non-function")
1.706 end
1.707 | Const (@{const_name All}, _) =>
1.708 - SOME (interpret thy model args (eta_expand t 1))
1.709 + SOME (interpret ctxt model args (eta_expand t 1))
1.710 | Const (@{const_name Ex}, _) $ t1 =>
1.711 let
1.712 - val (i, m, a) = interpret thy model args t1
1.713 + val (i, m, a) = interpret ctxt model args t1
1.714 in
1.715 case i of
1.716 Node xs =>
1.717 @@ -1825,81 +1764,79 @@
1.718 "\"Ex\" is followed by a non-function")
1.719 end
1.720 | Const (@{const_name Ex}, _) =>
1.721 - SOME (interpret thy model args (eta_expand t 1))
1.722 + SOME (interpret ctxt model args (eta_expand t 1))
1.723 | Const (@{const_name HOL.eq}, _) $ t1 $ t2 => (* similar to "==" (Pure) *)
1.724 let
1.725 - val (i1, m1, a1) = interpret thy model args t1
1.726 - val (i2, m2, a2) = interpret thy m1 a1 t2
1.727 + val (i1, m1, a1) = interpret ctxt model args t1
1.728 + val (i2, m2, a2) = interpret ctxt m1 a1 t2
1.729 in
1.730 SOME (make_equality (i1, i2), m2, a2)
1.731 end
1.732 | Const (@{const_name HOL.eq}, _) $ t1 =>
1.733 - SOME (interpret thy model args (eta_expand t 1))
1.734 + SOME (interpret ctxt model args (eta_expand t 1))
1.735 | Const (@{const_name HOL.eq}, _) =>
1.736 - SOME (interpret thy model args (eta_expand t 2))
1.737 + SOME (interpret ctxt model args (eta_expand t 2))
1.738 | Const (@{const_name HOL.conj}, _) $ t1 $ t2 =>
1.739 (* 3-valued logic *)
1.740 let
1.741 - val (i1, m1, a1) = interpret thy model args t1
1.742 - val (i2, m2, a2) = interpret thy m1 a1 t2
1.743 + val (i1, m1, a1) = interpret ctxt model args t1
1.744 + val (i2, m2, a2) = interpret ctxt m1 a1 t2
1.745 val fmTrue = PropLogic.SAnd (toTrue i1, toTrue i2)
1.746 val fmFalse = PropLogic.SOr (toFalse i1, toFalse i2)
1.747 in
1.748 SOME (Leaf [fmTrue, fmFalse], m2, a2)
1.749 end
1.750 | Const (@{const_name HOL.conj}, _) $ t1 =>
1.751 - SOME (interpret thy model args (eta_expand t 1))
1.752 + SOME (interpret ctxt model args (eta_expand t 1))
1.753 | Const (@{const_name HOL.conj}, _) =>
1.754 - SOME (interpret thy model args (eta_expand t 2))
1.755 + SOME (interpret ctxt model args (eta_expand t 2))
1.756 (* this would make "undef" propagate, even for formulae like *)
1.757 (* "False & undef": *)
1.758 (* SOME (Node [Node [TT, FF], Node [FF, FF]], model, args) *)
1.759 | Const (@{const_name HOL.disj}, _) $ t1 $ t2 =>
1.760 (* 3-valued logic *)
1.761 let
1.762 - val (i1, m1, a1) = interpret thy model args t1
1.763 - val (i2, m2, a2) = interpret thy m1 a1 t2
1.764 + val (i1, m1, a1) = interpret ctxt model args t1
1.765 + val (i2, m2, a2) = interpret ctxt m1 a1 t2
1.766 val fmTrue = PropLogic.SOr (toTrue i1, toTrue i2)
1.767 val fmFalse = PropLogic.SAnd (toFalse i1, toFalse i2)
1.768 in
1.769 SOME (Leaf [fmTrue, fmFalse], m2, a2)
1.770 end
1.771 | Const (@{const_name HOL.disj}, _) $ t1 =>
1.772 - SOME (interpret thy model args (eta_expand t 1))
1.773 + SOME (interpret ctxt model args (eta_expand t 1))
1.774 | Const (@{const_name HOL.disj}, _) =>
1.775 - SOME (interpret thy model args (eta_expand t 2))
1.776 + SOME (interpret ctxt model args (eta_expand t 2))
1.777 (* this would make "undef" propagate, even for formulae like *)
1.778 (* "True | undef": *)
1.779 (* SOME (Node [Node [TT, TT], Node [TT, FF]], model, args) *)
1.780 | Const (@{const_name HOL.implies}, _) $ t1 $ t2 => (* similar to "==>" (Pure) *)
1.781 (* 3-valued logic *)
1.782 let
1.783 - val (i1, m1, a1) = interpret thy model args t1
1.784 - val (i2, m2, a2) = interpret thy m1 a1 t2
1.785 + val (i1, m1, a1) = interpret ctxt model args t1
1.786 + val (i2, m2, a2) = interpret ctxt m1 a1 t2
1.787 val fmTrue = PropLogic.SOr (toFalse i1, toTrue i2)
1.788 val fmFalse = PropLogic.SAnd (toTrue i1, toFalse i2)
1.789 in
1.790 SOME (Leaf [fmTrue, fmFalse], m2, a2)
1.791 end
1.792 | Const (@{const_name HOL.implies}, _) $ t1 =>
1.793 - SOME (interpret thy model args (eta_expand t 1))
1.794 + SOME (interpret ctxt model args (eta_expand t 1))
1.795 | Const (@{const_name HOL.implies}, _) =>
1.796 - SOME (interpret thy model args (eta_expand t 2))
1.797 + SOME (interpret ctxt model args (eta_expand t 2))
1.798 (* this would make "undef" propagate, even for formulae like *)
1.799 (* "False --> undef": *)
1.800 (* SOME (Node [Node [TT, FF], Node [TT, TT]], model, args) *)
1.801 | _ => NONE;
1.802
1.803 -(* theory -> model -> arguments -> Term.term ->
1.804 - (interpretation * model * arguments) option *)
1.805 -
1.806 (* interprets variables and constants whose type is an IDT (this is *)
1.807 (* relatively easy and merely requires us to compute the size of the IDT); *)
1.808 (* constructors of IDTs however are properly interpreted by *)
1.809 (* 'IDT_constructor_interpreter' *)
1.810
1.811 -fun IDT_interpreter thy model args t =
1.812 +fun IDT_interpreter ctxt model args t =
1.813 let
1.814 + val thy = ProofContext.theory_of ctxt
1.815 val (typs, terms) = model
1.816 (* Term.typ -> (interpretation * model * arguments) option *)
1.817 fun interpret_term (Type (s, Ts)) =
1.818 @@ -1933,7 +1870,7 @@
1.819 then
1.820 raise REFUTE ("IDT_interpreter",
1.821 "datatype argument (for type "
1.822 - ^ Syntax.string_of_typ_global thy (Type (s, Ts))
1.823 + ^ Syntax.string_of_typ ctxt (Type (s, Ts))
1.824 ^ ") is not a variable")
1.825 else ()
1.826 (* if the model specifies a depth for the current type, *)
1.827 @@ -1941,7 +1878,7 @@
1.828 val typs' = case depth of NONE => typs | SOME n =>
1.829 AList.update (op =) (Type (s, Ts), n-1) typs
1.830 (* recursively compute the size of the datatype *)
1.831 - val size = size_of_dtyp thy typs' descr typ_assoc constrs
1.832 + val size = size_of_dtyp ctxt typs' descr typ_assoc constrs
1.833 val next_idx = #next_idx args
1.834 val next = next_idx+size
1.835 (* check if 'maxvars' is large enough *)
1.836 @@ -1982,9 +1919,6 @@
1.837 | _ => NONE)
1.838 end;
1.839
1.840 -(* theory -> model -> arguments -> Term.term ->
1.841 - (interpretation * model * arguments) option *)
1.842 -
1.843 (* This function imposes an order on the elements of a datatype fragment *)
1.844 (* as follows: C_i x_1 ... x_n < C_j y_1 ... y_m iff i < j or *)
1.845 (* (x_1, ..., x_n) < (y_1, ..., y_m). With this order, a constructor is *)
1.846 @@ -1993,8 +1927,9 @@
1.847 (* same for recursive datatypes, although the computation of indices gets *)
1.848 (* a little tricky. *)
1.849
1.850 -fun IDT_constructor_interpreter thy model args t =
1.851 +fun IDT_constructor_interpreter ctxt model args t =
1.852 let
1.853 + val thy = ProofContext.theory_of ctxt
1.854 (* returns a list of canonical representations for terms of the type 'T' *)
1.855 (* It would be nice if we could just use 'print' for this, but 'print' *)
1.856 (* for IDTs calls 'IDT_constructor_interpreter' again, and this could *)
1.857 @@ -2057,7 +1992,7 @@
1.858 then
1.859 raise REFUTE ("IDT_constructor_interpreter",
1.860 "datatype argument (for type "
1.861 - ^ Syntax.string_of_typ_global thy T
1.862 + ^ Syntax.string_of_typ ctxt T
1.863 ^ ") is not a variable")
1.864 else ()
1.865 (* decrement depth for the IDT 'T' *)
1.866 @@ -2088,11 +2023,11 @@
1.867 | NONE =>
1.868 (* not an inductive datatype; in this case the argument types in *)
1.869 (* 'Ts' may not be IDTs either, so 'print' should be safe *)
1.870 - map (fn intr => print thy (typs, []) T intr (K false))
1.871 - (make_constants thy (typs, []) T))
1.872 + map (fn intr => print ctxt (typs, []) T intr (K false))
1.873 + (make_constants ctxt (typs, []) T))
1.874 | _ => (* TFree ..., TVar ... *)
1.875 - map (fn intr => print thy (typs, []) T intr (K false))
1.876 - (make_constants thy (typs, []) T))
1.877 + map (fn intr => print ctxt (typs, []) T intr (K false))
1.878 + (make_constants ctxt (typs, []) T))
1.879 val (typs, terms) = model
1.880 in
1.881 case AList.lookup (op =) terms t of
1.882 @@ -2117,7 +2052,7 @@
1.883 then
1.884 raise REFUTE ("IDT_constructor_interpreter",
1.885 "datatype argument (for type "
1.886 - ^ Syntax.string_of_typ_global thy (Type (s', Ts'))
1.887 + ^ Syntax.string_of_typ ctxt (Type (s', Ts'))
1.888 ^ ") is not a variable")
1.889 else ()
1.890 (* split the constructors into those occuring before/after *)
1.891 @@ -2148,12 +2083,12 @@
1.892 (* elements of the datatype come before elements generated *)
1.893 (* by 'Const (s, T)' iff they are generated by a *)
1.894 (* constructor in constrs1 *)
1.895 - val offset = size_of_dtyp thy typs' descr typ_assoc constrs1
1.896 + val offset = size_of_dtyp ctxt typs' descr typ_assoc constrs1
1.897 (* compute the total (current) size of the datatype *)
1.898 val total = offset +
1.899 - size_of_dtyp thy typs' descr typ_assoc constrs2
1.900 + size_of_dtyp ctxt typs' descr typ_assoc constrs2
1.901 (* sanity check *)
1.902 - val _ = if total <> size_of_type thy (typs, [])
1.903 + val _ = if total <> size_of_type ctxt (typs, [])
1.904 (Type (s', Ts')) then
1.905 raise REFUTE ("IDT_constructor_interpreter",
1.906 "total is not equal to current size")
1.907 @@ -2165,7 +2100,7 @@
1.908 let
1.909 (* compute the current size of the type 'd' *)
1.910 val dT = typ_of_dtyp descr typ_assoc d
1.911 - val size = size_of_type thy (typs, []) dT
1.912 + val size = size_of_type ctxt (typs, []) dT
1.913 in
1.914 Node (replicate size (make_undef ds))
1.915 end
1.916 @@ -2187,7 +2122,7 @@
1.917 val terms' = canonical_terms typs' dT
1.918 (* sanity check *)
1.919 val _ =
1.920 - if length terms' <> size_of_type thy (typs', []) dT
1.921 + if length terms' <> size_of_type ctxt (typs', []) dT
1.922 then
1.923 raise REFUTE ("IDT_constructor_interpreter",
1.924 "length of terms' is not equal to old size")
1.925 @@ -2198,7 +2133,7 @@
1.926 val terms = canonical_terms typs dT
1.927 (* sanity check *)
1.928 val _ =
1.929 - if length terms <> size_of_type thy (typs, []) dT
1.930 + if length terms <> size_of_type ctxt (typs, []) dT
1.931 then
1.932 raise REFUTE ("IDT_constructor_interpreter",
1.933 "length of terms is not equal to current size")
1.934 @@ -2253,350 +2188,348 @@
1.935 NONE)
1.936 end;
1.937
1.938 -(* theory -> model -> arguments -> Term.term ->
1.939 - (interpretation * model * arguments) option *)
1.940 -
1.941 (* Difficult code ahead. Make sure you understand the *)
1.942 (* 'IDT_constructor_interpreter' and the order in which it enumerates *)
1.943 (* elements of an IDT before you try to understand this function. *)
1.944
1.945 -fun IDT_recursion_interpreter thy model args t =
1.946 - (* careful: here we descend arbitrarily deep into 't', possibly before *)
1.947 - (* any other interpreter for atomic terms has had a chance to look at *)
1.948 - (* 't' *)
1.949 - case strip_comb t of
1.950 - (Const (s, T), params) =>
1.951 - (* iterate over all datatypes in 'thy' *)
1.952 - Symtab.fold (fn (_, info) => fn result =>
1.953 - case result of
1.954 - SOME _ =>
1.955 - result (* just keep 'result' *)
1.956 - | NONE =>
1.957 - if member (op =) (#rec_names info) s then
1.958 - (* we do have a recursion operator of one of the (mutually *)
1.959 - (* recursive) datatypes given by 'info' *)
1.960 - let
1.961 - (* number of all constructors, including those of different *)
1.962 - (* (mutually recursive) datatypes within the same descriptor *)
1.963 - val mconstrs_count =
1.964 - Integer.sum (map (fn (_, (_, _, cs)) => length cs) (#descr info))
1.965 - in
1.966 - if mconstrs_count < length params then
1.967 - (* too many actual parameters; for now we'll use the *)
1.968 - (* 'stlc_interpreter' to strip off one application *)
1.969 - NONE
1.970 - else if mconstrs_count > length params then
1.971 - (* too few actual parameters; we use eta expansion *)
1.972 - (* Note that the resulting expansion of lambda abstractions *)
1.973 - (* by the 'stlc_interpreter' may be rather slow (depending *)
1.974 - (* on the argument types and the size of the IDT, of *)
1.975 - (* course). *)
1.976 - SOME (interpret thy model args (eta_expand t
1.977 - (mconstrs_count - length params)))
1.978 - else (* mconstrs_count = length params *)
1.979 - let
1.980 - (* interpret each parameter separately *)
1.981 - val (p_intrs, (model', args')) = fold_map (fn p => fn (m, a) =>
1.982 - let
1.983 - val (i, m', a') = interpret thy m a p
1.984 - in
1.985 - (i, (m', a'))
1.986 - end) params (model, args)
1.987 - val (typs, _) = model'
1.988 - (* 'index' is /not/ necessarily the index of the IDT that *)
1.989 - (* the recursion operator is associated with, but merely *)
1.990 - (* the index of some mutually recursive IDT *)
1.991 - val index = #index info
1.992 - val descr = #descr info
1.993 - val (_, dtyps, _) = the (AList.lookup (op =) descr index)
1.994 - (* sanity check: we assume that the order of constructors *)
1.995 - (* in 'descr' is the same as the order of *)
1.996 - (* corresponding parameters, otherwise the *)
1.997 - (* association code below won't match the *)
1.998 - (* right constructors/parameters; we also *)
1.999 - (* assume that the order of recursion *)
1.1000 - (* operators in '#rec_names info' is the *)
1.1001 - (* same as the order of corresponding *)
1.1002 - (* datatypes in 'descr' *)
1.1003 - val _ = if map fst descr <> (0 upto (length descr - 1)) then
1.1004 - raise REFUTE ("IDT_recursion_interpreter",
1.1005 - "order of constructors and corresponding parameters/" ^
1.1006 - "recursion operators and corresponding datatypes " ^
1.1007 - "different?")
1.1008 - else ()
1.1009 - (* sanity check: every element in 'dtyps' must be a *)
1.1010 - (* 'DtTFree' *)
1.1011 - val _ =
1.1012 - if Library.exists (fn d =>
1.1013 - case d of Datatype_Aux.DtTFree _ => false
1.1014 - | _ => true) dtyps
1.1015 - then
1.1016 - raise REFUTE ("IDT_recursion_interpreter",
1.1017 - "datatype argument is not a variable")
1.1018 - else ()
1.1019 - (* the type of a recursion operator is *)
1.1020 - (* [T1, ..., Tn, IDT] ---> Tresult *)
1.1021 - val IDT = List.nth (binder_types T, mconstrs_count)
1.1022 - (* by our assumption on the order of recursion operators *)
1.1023 - (* and datatypes, this is the index of the datatype *)
1.1024 - (* corresponding to the given recursion operator *)
1.1025 - val idt_index = find_index (fn s' => s' = s) (#rec_names info)
1.1026 - (* mutually recursive types must have the same type *)
1.1027 - (* parameters, unless the mutual recursion comes from *)
1.1028 - (* indirect recursion *)
1.1029 - fun rec_typ_assoc acc [] = acc
1.1030 - | rec_typ_assoc acc ((d, T)::xs) =
1.1031 - (case AList.lookup op= acc d of
1.1032 - NONE =>
1.1033 - (case d of
1.1034 - Datatype_Aux.DtTFree _ =>
1.1035 - (* add the association, proceed *)
1.1036 - rec_typ_assoc ((d, T)::acc) xs
1.1037 - | Datatype_Aux.DtType (s, ds) =>
1.1038 - let
1.1039 - val (s', Ts) = dest_Type T
1.1040 - in
1.1041 - if s=s' then
1.1042 +fun IDT_recursion_interpreter ctxt model args t =
1.1043 + let
1.1044 + val thy = ProofContext.theory_of ctxt
1.1045 + in
1.1046 + (* careful: here we descend arbitrarily deep into 't', possibly before *)
1.1047 + (* any other interpreter for atomic terms has had a chance to look at *)
1.1048 + (* 't' *)
1.1049 + case strip_comb t of
1.1050 + (Const (s, T), params) =>
1.1051 + (* iterate over all datatypes in 'thy' *)
1.1052 + Symtab.fold (fn (_, info) => fn result =>
1.1053 + case result of
1.1054 + SOME _ =>
1.1055 + result (* just keep 'result' *)
1.1056 + | NONE =>
1.1057 + if member (op =) (#rec_names info) s then
1.1058 + (* we do have a recursion operator of one of the (mutually *)
1.1059 + (* recursive) datatypes given by 'info' *)
1.1060 + let
1.1061 + (* number of all constructors, including those of different *)
1.1062 + (* (mutually recursive) datatypes within the same descriptor *)
1.1063 + val mconstrs_count =
1.1064 + Integer.sum (map (fn (_, (_, _, cs)) => length cs) (#descr info))
1.1065 + in
1.1066 + if mconstrs_count < length params then
1.1067 + (* too many actual parameters; for now we'll use the *)
1.1068 + (* 'stlc_interpreter' to strip off one application *)
1.1069 + NONE
1.1070 + else if mconstrs_count > length params then
1.1071 + (* too few actual parameters; we use eta expansion *)
1.1072 + (* Note that the resulting expansion of lambda abstractions *)
1.1073 + (* by the 'stlc_interpreter' may be rather slow (depending *)
1.1074 + (* on the argument types and the size of the IDT, of *)
1.1075 + (* course). *)
1.1076 + SOME (interpret ctxt model args (eta_expand t
1.1077 + (mconstrs_count - length params)))
1.1078 + else (* mconstrs_count = length params *)
1.1079 + let
1.1080 + (* interpret each parameter separately *)
1.1081 + val (p_intrs, (model', args')) = fold_map (fn p => fn (m, a) =>
1.1082 + let
1.1083 + val (i, m', a') = interpret ctxt m a p
1.1084 + in
1.1085 + (i, (m', a'))
1.1086 + end) params (model, args)
1.1087 + val (typs, _) = model'
1.1088 + (* 'index' is /not/ necessarily the index of the IDT that *)
1.1089 + (* the recursion operator is associated with, but merely *)
1.1090 + (* the index of some mutually recursive IDT *)
1.1091 + val index = #index info
1.1092 + val descr = #descr info
1.1093 + val (_, dtyps, _) = the (AList.lookup (op =) descr index)
1.1094 + (* sanity check: we assume that the order of constructors *)
1.1095 + (* in 'descr' is the same as the order of *)
1.1096 + (* corresponding parameters, otherwise the *)
1.1097 + (* association code below won't match the *)
1.1098 + (* right constructors/parameters; we also *)
1.1099 + (* assume that the order of recursion *)
1.1100 + (* operators in '#rec_names info' is the *)
1.1101 + (* same as the order of corresponding *)
1.1102 + (* datatypes in 'descr' *)
1.1103 + val _ = if map fst descr <> (0 upto (length descr - 1)) then
1.1104 + raise REFUTE ("IDT_recursion_interpreter",
1.1105 + "order of constructors and corresponding parameters/" ^
1.1106 + "recursion operators and corresponding datatypes " ^
1.1107 + "different?")
1.1108 + else ()
1.1109 + (* sanity check: every element in 'dtyps' must be a *)
1.1110 + (* 'DtTFree' *)
1.1111 + val _ =
1.1112 + if Library.exists (fn d =>
1.1113 + case d of Datatype_Aux.DtTFree _ => false
1.1114 + | _ => true) dtyps
1.1115 + then
1.1116 + raise REFUTE ("IDT_recursion_interpreter",
1.1117 + "datatype argument is not a variable")
1.1118 + else ()
1.1119 + (* the type of a recursion operator is *)
1.1120 + (* [T1, ..., Tn, IDT] ---> Tresult *)
1.1121 + val IDT = List.nth (binder_types T, mconstrs_count)
1.1122 + (* by our assumption on the order of recursion operators *)
1.1123 + (* and datatypes, this is the index of the datatype *)
1.1124 + (* corresponding to the given recursion operator *)
1.1125 + val idt_index = find_index (fn s' => s' = s) (#rec_names info)
1.1126 + (* mutually recursive types must have the same type *)
1.1127 + (* parameters, unless the mutual recursion comes from *)
1.1128 + (* indirect recursion *)
1.1129 + fun rec_typ_assoc acc [] = acc
1.1130 + | rec_typ_assoc acc ((d, T)::xs) =
1.1131 + (case AList.lookup op= acc d of
1.1132 + NONE =>
1.1133 + (case d of
1.1134 + Datatype_Aux.DtTFree _ =>
1.1135 + (* add the association, proceed *)
1.1136 + rec_typ_assoc ((d, T)::acc) xs
1.1137 + | Datatype_Aux.DtType (s, ds) =>
1.1138 + let
1.1139 + val (s', Ts) = dest_Type T
1.1140 + in
1.1141 + if s=s' then
1.1142 + rec_typ_assoc ((d, T)::acc) ((ds ~~ Ts) @ xs)
1.1143 + else
1.1144 + raise REFUTE ("IDT_recursion_interpreter",
1.1145 + "DtType/Type mismatch")
1.1146 + end
1.1147 + | Datatype_Aux.DtRec i =>
1.1148 + let
1.1149 + val (_, ds, _) = the (AList.lookup (op =) descr i)
1.1150 + val (_, Ts) = dest_Type T
1.1151 + in
1.1152 rec_typ_assoc ((d, T)::acc) ((ds ~~ Ts) @ xs)
1.1153 - else
1.1154 - raise REFUTE ("IDT_recursion_interpreter",
1.1155 - "DtType/Type mismatch")
1.1156 - end
1.1157 - | Datatype_Aux.DtRec i =>
1.1158 - let
1.1159 - val (_, ds, _) = the (AList.lookup (op =) descr i)
1.1160 - val (_, Ts) = dest_Type T
1.1161 - in
1.1162 - rec_typ_assoc ((d, T)::acc) ((ds ~~ Ts) @ xs)
1.1163 - end)
1.1164 - | SOME T' =>
1.1165 - if T=T' then
1.1166 - (* ignore the association since it's already *)
1.1167 - (* present, proceed *)
1.1168 - rec_typ_assoc acc xs
1.1169 - else
1.1170 + end)
1.1171 + | SOME T' =>
1.1172 + if T=T' then
1.1173 + (* ignore the association since it's already *)
1.1174 + (* present, proceed *)
1.1175 + rec_typ_assoc acc xs
1.1176 + else
1.1177 + raise REFUTE ("IDT_recursion_interpreter",
1.1178 + "different type associations for the same dtyp"))
1.1179 + val typ_assoc = filter
1.1180 + (fn (Datatype_Aux.DtTFree _, _) => true | (_, _) => false)
1.1181 + (rec_typ_assoc []
1.1182 + (#2 (the (AList.lookup (op =) descr idt_index)) ~~ (snd o dest_Type) IDT))
1.1183 + (* sanity check: typ_assoc must associate types to the *)
1.1184 + (* elements of 'dtyps' (and only to those) *)
1.1185 + val _ =
1.1186 + if not (eq_set (op =) (dtyps, map fst typ_assoc))
1.1187 + then
1.1188 + raise REFUTE ("IDT_recursion_interpreter",
1.1189 + "type association has extra/missing elements")
1.1190 + else ()
1.1191 + (* interpret each constructor in the descriptor (including *)
1.1192 + (* those of mutually recursive datatypes) *)
1.1193 + (* (int * interpretation list) list *)
1.1194 + val mc_intrs = map (fn (idx, (_, _, cs)) =>
1.1195 + let
1.1196 + val c_return_typ = typ_of_dtyp descr typ_assoc
1.1197 + (Datatype_Aux.DtRec idx)
1.1198 + in
1.1199 + (idx, map (fn (cname, cargs) =>
1.1200 + (#1 o interpret ctxt (typs, []) {maxvars=0,
1.1201 + def_eq=false, next_idx=1, bounds=[],
1.1202 + wellformed=True}) (Const (cname, map (typ_of_dtyp
1.1203 + descr typ_assoc) cargs ---> c_return_typ))) cs)
1.1204 + end) descr
1.1205 + (* associate constructors with corresponding parameters *)
1.1206 + (* (int * (interpretation * interpretation) list) list *)
1.1207 + val (mc_p_intrs, p_intrs') = fold_map
1.1208 + (fn (idx, c_intrs) => fn p_intrs' =>
1.1209 + let
1.1210 + val len = length c_intrs
1.1211 + in
1.1212 + ((idx, c_intrs ~~ List.take (p_intrs', len)),
1.1213 + List.drop (p_intrs', len))
1.1214 + end) mc_intrs p_intrs
1.1215 + (* sanity check: no 'p_intr' may be left afterwards *)
1.1216 + val _ =
1.1217 + if p_intrs' <> [] then
1.1218 + raise REFUTE ("IDT_recursion_interpreter",
1.1219 + "more parameter than constructor interpretations")
1.1220 + else ()
1.1221 + (* The recursion operator, applied to 'mconstrs_count' *)
1.1222 + (* arguments, is a function that maps every element of the *)
1.1223 + (* inductive datatype to an element of some result type. *)
1.1224 + (* Recursion operators for mutually recursive IDTs are *)
1.1225 + (* translated simultaneously. *)
1.1226 + (* Since the order on datatype elements is given by an *)
1.1227 + (* order on constructors (and then by the order on *)
1.1228 + (* argument tuples), we can simply copy corresponding *)
1.1229 + (* subtrees from 'p_intrs', in the order in which they are *)
1.1230 + (* given. *)
1.1231 + (* interpretation * interpretation -> interpretation list *)
1.1232 + fun ci_pi (Leaf xs, pi) =
1.1233 + (* if the constructor does not match the arguments to a *)
1.1234 + (* defined element of the IDT, the corresponding value *)
1.1235 + (* of the parameter must be ignored *)
1.1236 + if List.exists (equal True) xs then [pi] else []
1.1237 + | ci_pi (Node xs, Node ys) = maps ci_pi (xs ~~ ys)
1.1238 + | ci_pi (Node _, Leaf _) =
1.1239 + raise REFUTE ("IDT_recursion_interpreter",
1.1240 + "constructor takes more arguments than the " ^
1.1241 + "associated parameter")
1.1242 + (* (int * interpretation list) list *)
1.1243 + val rec_operators = map (fn (idx, c_p_intrs) =>
1.1244 + (idx, maps ci_pi c_p_intrs)) mc_p_intrs
1.1245 + (* sanity check: every recursion operator must provide as *)
1.1246 + (* many values as the corresponding datatype *)
1.1247 + (* has elements *)
1.1248 + val _ = map (fn (idx, intrs) =>
1.1249 + let
1.1250 + val T = typ_of_dtyp descr typ_assoc
1.1251 + (Datatype_Aux.DtRec idx)
1.1252 + in
1.1253 + if length intrs <> size_of_type ctxt (typs, []) T then
1.1254 + raise REFUTE ("IDT_recursion_interpreter",
1.1255 + "wrong number of interpretations for rec. operator")
1.1256 + else ()
1.1257 + end) rec_operators
1.1258 + (* For non-recursive datatypes, we are pretty much done at *)
1.1259 + (* this point. For recursive datatypes however, we still *)
1.1260 + (* need to apply the interpretations in 'rec_operators' to *)
1.1261 + (* (recursively obtained) interpretations for recursive *)
1.1262 + (* constructor arguments. To do so more efficiently, we *)
1.1263 + (* copy 'rec_operators' into arrays first. Each Boolean *)
1.1264 + (* indicates whether the recursive arguments have been *)
1.1265 + (* considered already. *)
1.1266 + (* (int * (bool * interpretation) Array.array) list *)
1.1267 + val REC_OPERATORS = map (fn (idx, intrs) =>
1.1268 + (idx, Array.fromList (map (pair false) intrs)))
1.1269 + rec_operators
1.1270 + (* takes an interpretation, and if some leaf of this *)
1.1271 + (* interpretation is the 'elem'-th element of the type, *)
1.1272 + (* the indices of the arguments leading to this leaf are *)
1.1273 + (* returned *)
1.1274 + (* interpretation -> int -> int list option *)
1.1275 + fun get_args (Leaf xs) elem =
1.1276 + if find_index (fn x => x = True) xs = elem then
1.1277 + SOME []
1.1278 + else
1.1279 + NONE
1.1280 + | get_args (Node xs) elem =
1.1281 + let
1.1282 + (* interpretation list * int -> int list option *)
1.1283 + fun search ([], _) =
1.1284 + NONE
1.1285 + | search (x::xs, n) =
1.1286 + (case get_args x elem of
1.1287 + SOME result => SOME (n::result)
1.1288 + | NONE => search (xs, n+1))
1.1289 + in
1.1290 + search (xs, 0)
1.1291 + end
1.1292 + (* returns the index of the constructor and indices for *)
1.1293 + (* its arguments that generate the 'elem'-th element of *)
1.1294 + (* the datatype given by 'idx' *)
1.1295 + (* int -> int -> int * int list *)
1.1296 + fun get_cargs idx elem =
1.1297 + let
1.1298 + (* int * interpretation list -> int * int list *)
1.1299 + fun get_cargs_rec (_, []) =
1.1300 raise REFUTE ("IDT_recursion_interpreter",
1.1301 - "different type associations for the same dtyp"))
1.1302 - val typ_assoc = filter
1.1303 - (fn (Datatype_Aux.DtTFree _, _) => true | (_, _) => false)
1.1304 - (rec_typ_assoc []
1.1305 - (#2 (the (AList.lookup (op =) descr idt_index)) ~~ (snd o dest_Type) IDT))
1.1306 - (* sanity check: typ_assoc must associate types to the *)
1.1307 - (* elements of 'dtyps' (and only to those) *)
1.1308 - val _ =
1.1309 - if not (eq_set (op =) (dtyps, map fst typ_assoc))
1.1310 - then
1.1311 - raise REFUTE ("IDT_recursion_interpreter",
1.1312 - "type association has extra/missing elements")
1.1313 - else ()
1.1314 - (* interpret each constructor in the descriptor (including *)
1.1315 - (* those of mutually recursive datatypes) *)
1.1316 - (* (int * interpretation list) list *)
1.1317 - val mc_intrs = map (fn (idx, (_, _, cs)) =>
1.1318 - let
1.1319 - val c_return_typ = typ_of_dtyp descr typ_assoc
1.1320 - (Datatype_Aux.DtRec idx)
1.1321 - in
1.1322 - (idx, map (fn (cname, cargs) =>
1.1323 - (#1 o interpret thy (typs, []) {maxvars=0,
1.1324 - def_eq=false, next_idx=1, bounds=[],
1.1325 - wellformed=True}) (Const (cname, map (typ_of_dtyp
1.1326 - descr typ_assoc) cargs ---> c_return_typ))) cs)
1.1327 - end) descr
1.1328 - (* associate constructors with corresponding parameters *)
1.1329 - (* (int * (interpretation * interpretation) list) list *)
1.1330 - val (mc_p_intrs, p_intrs') = fold_map
1.1331 - (fn (idx, c_intrs) => fn p_intrs' =>
1.1332 + "no matching constructor found for datatype element")
1.1333 + | get_cargs_rec (n, x::xs) =
1.1334 + (case get_args x elem of
1.1335 + SOME args => (n, args)
1.1336 + | NONE => get_cargs_rec (n+1, xs))
1.1337 + in
1.1338 + get_cargs_rec (0, the (AList.lookup (op =) mc_intrs idx))
1.1339 + end
1.1340 + (* computes one entry in 'REC_OPERATORS', and recursively *)
1.1341 + (* all entries needed for it, where 'idx' gives the *)
1.1342 + (* datatype and 'elem' the element of it *)
1.1343 + (* int -> int -> interpretation *)
1.1344 + fun compute_array_entry idx elem =
1.1345 let
1.1346 - val len = length c_intrs
1.1347 + val arr = the (AList.lookup (op =) REC_OPERATORS idx)
1.1348 + val (flag, intr) = Array.sub (arr, elem)
1.1349 in
1.1350 - ((idx, c_intrs ~~ List.take (p_intrs', len)),
1.1351 - List.drop (p_intrs', len))
1.1352 - end) mc_intrs p_intrs
1.1353 - (* sanity check: no 'p_intr' may be left afterwards *)
1.1354 - val _ =
1.1355 - if p_intrs' <> [] then
1.1356 - raise REFUTE ("IDT_recursion_interpreter",
1.1357 - "more parameter than constructor interpretations")
1.1358 - else ()
1.1359 - (* The recursion operator, applied to 'mconstrs_count' *)
1.1360 - (* arguments, is a function that maps every element of the *)
1.1361 - (* inductive datatype to an element of some result type. *)
1.1362 - (* Recursion operators for mutually recursive IDTs are *)
1.1363 - (* translated simultaneously. *)
1.1364 - (* Since the order on datatype elements is given by an *)
1.1365 - (* order on constructors (and then by the order on *)
1.1366 - (* argument tuples), we can simply copy corresponding *)
1.1367 - (* subtrees from 'p_intrs', in the order in which they are *)
1.1368 - (* given. *)
1.1369 - (* interpretation * interpretation -> interpretation list *)
1.1370 - fun ci_pi (Leaf xs, pi) =
1.1371 - (* if the constructor does not match the arguments to a *)
1.1372 - (* defined element of the IDT, the corresponding value *)
1.1373 - (* of the parameter must be ignored *)
1.1374 - if List.exists (equal True) xs then [pi] else []
1.1375 - | ci_pi (Node xs, Node ys) = maps ci_pi (xs ~~ ys)
1.1376 - | ci_pi (Node _, Leaf _) =
1.1377 - raise REFUTE ("IDT_recursion_interpreter",
1.1378 - "constructor takes more arguments than the " ^
1.1379 - "associated parameter")
1.1380 - (* (int * interpretation list) list *)
1.1381 - val rec_operators = map (fn (idx, c_p_intrs) =>
1.1382 - (idx, maps ci_pi c_p_intrs)) mc_p_intrs
1.1383 - (* sanity check: every recursion operator must provide as *)
1.1384 - (* many values as the corresponding datatype *)
1.1385 - (* has elements *)
1.1386 - val _ = map (fn (idx, intrs) =>
1.1387 - let
1.1388 - val T = typ_of_dtyp descr typ_assoc
1.1389 - (Datatype_Aux.DtRec idx)
1.1390 - in
1.1391 - if length intrs <> size_of_type thy (typs, []) T then
1.1392 - raise REFUTE ("IDT_recursion_interpreter",
1.1393 - "wrong number of interpretations for rec. operator")
1.1394 - else ()
1.1395 - end) rec_operators
1.1396 - (* For non-recursive datatypes, we are pretty much done at *)
1.1397 - (* this point. For recursive datatypes however, we still *)
1.1398 - (* need to apply the interpretations in 'rec_operators' to *)
1.1399 - (* (recursively obtained) interpretations for recursive *)
1.1400 - (* constructor arguments. To do so more efficiently, we *)
1.1401 - (* copy 'rec_operators' into arrays first. Each Boolean *)
1.1402 - (* indicates whether the recursive arguments have been *)
1.1403 - (* considered already. *)
1.1404 - (* (int * (bool * interpretation) Array.array) list *)
1.1405 - val REC_OPERATORS = map (fn (idx, intrs) =>
1.1406 - (idx, Array.fromList (map (pair false) intrs)))
1.1407 - rec_operators
1.1408 - (* takes an interpretation, and if some leaf of this *)
1.1409 - (* interpretation is the 'elem'-th element of the type, *)
1.1410 - (* the indices of the arguments leading to this leaf are *)
1.1411 - (* returned *)
1.1412 - (* interpretation -> int -> int list option *)
1.1413 - fun get_args (Leaf xs) elem =
1.1414 - if find_index (fn x => x = True) xs = elem then
1.1415 - SOME []
1.1416 + if flag then
1.1417 + (* simply return the previously computed result *)
1.1418 + intr
1.1419 else
1.1420 - NONE
1.1421 - | get_args (Node xs) elem =
1.1422 - let
1.1423 - (* interpretation list * int -> int list option *)
1.1424 - fun search ([], _) =
1.1425 - NONE
1.1426 - | search (x::xs, n) =
1.1427 - (case get_args x elem of
1.1428 - SOME result => SOME (n::result)
1.1429 - | NONE => search (xs, n+1))
1.1430 - in
1.1431 - search (xs, 0)
1.1432 - end
1.1433 - (* returns the index of the constructor and indices for *)
1.1434 - (* its arguments that generate the 'elem'-th element of *)
1.1435 - (* the datatype given by 'idx' *)
1.1436 - (* int -> int -> int * int list *)
1.1437 - fun get_cargs idx elem =
1.1438 - let
1.1439 - (* int * interpretation list -> int * int list *)
1.1440 - fun get_cargs_rec (_, []) =
1.1441 - raise REFUTE ("IDT_recursion_interpreter",
1.1442 - "no matching constructor found for datatype element")
1.1443 - | get_cargs_rec (n, x::xs) =
1.1444 - (case get_args x elem of
1.1445 - SOME args => (n, args)
1.1446 - | NONE => get_cargs_rec (n+1, xs))
1.1447 - in
1.1448 - get_cargs_rec (0, the (AList.lookup (op =) mc_intrs idx))
1.1449 - end
1.1450 - (* computes one entry in 'REC_OPERATORS', and recursively *)
1.1451 - (* all entries needed for it, where 'idx' gives the *)
1.1452 - (* datatype and 'elem' the element of it *)
1.1453 - (* int -> int -> interpretation *)
1.1454 - fun compute_array_entry idx elem =
1.1455 - let
1.1456 - val arr = the (AList.lookup (op =) REC_OPERATORS idx)
1.1457 - val (flag, intr) = Array.sub (arr, elem)
1.1458 - in
1.1459 - if flag then
1.1460 - (* simply return the previously computed result *)
1.1461 - intr
1.1462 - else
1.1463 - (* we have to apply 'intr' to interpretations for all *)
1.1464 - (* recursive arguments *)
1.1465 - let
1.1466 - (* int * int list *)
1.1467 - val (c, args) = get_cargs idx elem
1.1468 - (* find the indices of the constructor's /recursive/ *)
1.1469 - (* arguments *)
1.1470 - val (_, _, constrs) = the (AList.lookup (op =) descr idx)
1.1471 - val (_, dtyps) = List.nth (constrs, c)
1.1472 - val rec_dtyps_args = filter
1.1473 - (Datatype_Aux.is_rec_type o fst) (dtyps ~~ args)
1.1474 - (* map those indices to interpretations *)
1.1475 - val rec_dtyps_intrs = map (fn (dtyp, arg) =>
1.1476 - let
1.1477 - val dT = typ_of_dtyp descr typ_assoc dtyp
1.1478 - val consts = make_constants thy (typs, []) dT
1.1479 - val arg_i = List.nth (consts, arg)
1.1480 - in
1.1481 - (dtyp, arg_i)
1.1482 - end) rec_dtyps_args
1.1483 - (* takes the dtyp and interpretation of an element, *)
1.1484 - (* and computes the interpretation for the *)
1.1485 - (* corresponding recursive argument *)
1.1486 - fun rec_intr (Datatype_Aux.DtRec i) (Leaf xs) =
1.1487 - (* recursive argument is "rec_i params elem" *)
1.1488 - compute_array_entry i (find_index (fn x => x = True) xs)
1.1489 - | rec_intr (Datatype_Aux.DtRec _) (Node _) =
1.1490 - raise REFUTE ("IDT_recursion_interpreter",
1.1491 - "interpretation for IDT is a node")
1.1492 - | rec_intr (Datatype_Aux.DtType ("fun", [dt1, dt2])) (Node xs) =
1.1493 - (* recursive argument is something like *)
1.1494 - (* "\<lambda>x::dt1. rec_? params (elem x)" *)
1.1495 - Node (map (rec_intr dt2) xs)
1.1496 - | rec_intr (Datatype_Aux.DtType ("fun", [_, _])) (Leaf _) =
1.1497 - raise REFUTE ("IDT_recursion_interpreter",
1.1498 - "interpretation for function dtyp is a leaf")
1.1499 - | rec_intr _ _ =
1.1500 - (* admissibility ensures that every recursive type *)
1.1501 - (* is of the form 'Dt_1 -> ... -> Dt_k -> *)
1.1502 - (* (DtRec i)' *)
1.1503 - raise REFUTE ("IDT_recursion_interpreter",
1.1504 - "non-recursive codomain in recursive dtyp")
1.1505 - (* obtain interpretations for recursive arguments *)
1.1506 - (* interpretation list *)
1.1507 - val arg_intrs = map (uncurry rec_intr) rec_dtyps_intrs
1.1508 - (* apply 'intr' to all recursive arguments *)
1.1509 - val result = fold (fn arg_i => fn i =>
1.1510 - interpretation_apply (i, arg_i)) arg_intrs intr
1.1511 - (* update 'REC_OPERATORS' *)
1.1512 - val _ = Array.update (arr, elem, (true, result))
1.1513 - in
1.1514 - result
1.1515 - end
1.1516 - end
1.1517 - val idt_size = Array.length (the (AList.lookup (op =) REC_OPERATORS idt_index))
1.1518 - (* sanity check: the size of 'IDT' should be 'idt_size' *)
1.1519 - val _ =
1.1520 - if idt_size <> size_of_type thy (typs, []) IDT then
1.1521 - raise REFUTE ("IDT_recursion_interpreter",
1.1522 - "unexpected size of IDT (wrong type associated?)")
1.1523 - else ()
1.1524 - (* interpretation *)
1.1525 - val rec_op = Node (map_range (compute_array_entry idt_index) idt_size)
1.1526 - in
1.1527 - SOME (rec_op, model', args')
1.1528 - end
1.1529 - end
1.1530 - else
1.1531 - NONE (* not a recursion operator of this datatype *)
1.1532 - ) (Datatype.get_all thy) NONE
1.1533 - | _ => (* head of term is not a constant *)
1.1534 - NONE;
1.1535 + (* we have to apply 'intr' to interpretations for all *)
1.1536 + (* recursive arguments *)
1.1537 + let
1.1538 + (* int * int list *)
1.1539 + val (c, args) = get_cargs idx elem
1.1540 + (* find the indices of the constructor's /recursive/ *)
1.1541 + (* arguments *)
1.1542 + val (_, _, constrs) = the (AList.lookup (op =) descr idx)
1.1543 + val (_, dtyps) = List.nth (constrs, c)
1.1544 + val rec_dtyps_args = filter
1.1545 + (Datatype_Aux.is_rec_type o fst) (dtyps ~~ args)
1.1546 + (* map those indices to interpretations *)
1.1547 + val rec_dtyps_intrs = map (fn (dtyp, arg) =>
1.1548 + let
1.1549 + val dT = typ_of_dtyp descr typ_assoc dtyp
1.1550 + val consts = make_constants ctxt (typs, []) dT
1.1551 + val arg_i = List.nth (consts, arg)
1.1552 + in
1.1553 + (dtyp, arg_i)
1.1554 + end) rec_dtyps_args
1.1555 + (* takes the dtyp and interpretation of an element, *)
1.1556 + (* and computes the interpretation for the *)
1.1557 + (* corresponding recursive argument *)
1.1558 + fun rec_intr (Datatype_Aux.DtRec i) (Leaf xs) =
1.1559 + (* recursive argument is "rec_i params elem" *)
1.1560 + compute_array_entry i (find_index (fn x => x = True) xs)
1.1561 + | rec_intr (Datatype_Aux.DtRec _) (Node _) =
1.1562 + raise REFUTE ("IDT_recursion_interpreter",
1.1563 + "interpretation for IDT is a node")
1.1564 + | rec_intr (Datatype_Aux.DtType ("fun", [dt1, dt2])) (Node xs) =
1.1565 + (* recursive argument is something like *)
1.1566 + (* "\<lambda>x::dt1. rec_? params (elem x)" *)
1.1567 + Node (map (rec_intr dt2) xs)
1.1568 + | rec_intr (Datatype_Aux.DtType ("fun", [_, _])) (Leaf _) =
1.1569 + raise REFUTE ("IDT_recursion_interpreter",
1.1570 + "interpretation for function dtyp is a leaf")
1.1571 + | rec_intr _ _ =
1.1572 + (* admissibility ensures that every recursive type *)
1.1573 + (* is of the form 'Dt_1 -> ... -> Dt_k -> *)
1.1574 + (* (DtRec i)' *)
1.1575 + raise REFUTE ("IDT_recursion_interpreter",
1.1576 + "non-recursive codomain in recursive dtyp")
1.1577 + (* obtain interpretations for recursive arguments *)
1.1578 + (* interpretation list *)
1.1579 + val arg_intrs = map (uncurry rec_intr) rec_dtyps_intrs
1.1580 + (* apply 'intr' to all recursive arguments *)
1.1581 + val result = fold (fn arg_i => fn i =>
1.1582 + interpretation_apply (i, arg_i)) arg_intrs intr
1.1583 + (* update 'REC_OPERATORS' *)
1.1584 + val _ = Array.update (arr, elem, (true, result))
1.1585 + in
1.1586 + result
1.1587 + end
1.1588 + end
1.1589 + val idt_size = Array.length (the (AList.lookup (op =) REC_OPERATORS idt_index))
1.1590 + (* sanity check: the size of 'IDT' should be 'idt_size' *)
1.1591 + val _ =
1.1592 + if idt_size <> size_of_type ctxt (typs, []) IDT then
1.1593 + raise REFUTE ("IDT_recursion_interpreter",
1.1594 + "unexpected size of IDT (wrong type associated?)")
1.1595 + else ()
1.1596 + (* interpretation *)
1.1597 + val rec_op = Node (map_range (compute_array_entry idt_index) idt_size)
1.1598 + in
1.1599 + SOME (rec_op, model', args')
1.1600 + end
1.1601 + end
1.1602 + else
1.1603 + NONE (* not a recursion operator of this datatype *)
1.1604 + ) (Datatype.get_all thy) NONE
1.1605 + | _ => (* head of term is not a constant *)
1.1606 + NONE
1.1607 + end;
1.1608
1.1609 -(* theory -> model -> arguments -> Term.term ->
1.1610 - (interpretation * model * arguments) option *)
1.1611 -
1.1612 -fun set_interpreter thy model args t =
1.1613 +fun set_interpreter ctxt model args t =
1.1614 let
1.1615 val (typs, terms) = model
1.1616 in
1.1617 @@ -2608,27 +2541,24 @@
1.1618 (case t of
1.1619 (* 'Collect' == identity *)
1.1620 Const (@{const_name Collect}, _) $ t1 =>
1.1621 - SOME (interpret thy model args t1)
1.1622 + SOME (interpret ctxt model args t1)
1.1623 | Const (@{const_name Collect}, _) =>
1.1624 - SOME (interpret thy model args (eta_expand t 1))
1.1625 + SOME (interpret ctxt model args (eta_expand t 1))
1.1626 (* 'op :' == application *)
1.1627 | Const (@{const_name Set.member}, _) $ t1 $ t2 =>
1.1628 - SOME (interpret thy model args (t2 $ t1))
1.1629 + SOME (interpret ctxt model args (t2 $ t1))
1.1630 | Const (@{const_name Set.member}, _) $ t1 =>
1.1631 - SOME (interpret thy model args (eta_expand t 1))
1.1632 + SOME (interpret ctxt model args (eta_expand t 1))
1.1633 | Const (@{const_name Set.member}, _) =>
1.1634 - SOME (interpret thy model args (eta_expand t 2))
1.1635 + SOME (interpret ctxt model args (eta_expand t 2))
1.1636 | _ => NONE)
1.1637 end;
1.1638
1.1639 -(* theory -> model -> arguments -> Term.term ->
1.1640 - (interpretation * model * arguments) option *)
1.1641 -
1.1642 (* only an optimization: 'card' could in principle be interpreted with *)
1.1643 (* interpreters available already (using its definition), but the code *)
1.1644 (* below is more efficient *)
1.1645
1.1646 -fun Finite_Set_card_interpreter thy model args t =
1.1647 +fun Finite_Set_card_interpreter ctxt model args t =
1.1648 case t of
1.1649 Const (@{const_name Finite_Set.card},
1.1650 Type ("fun", [Type ("fun", [T, @{typ bool}]), @{typ nat}])) =>
1.1651 @@ -2647,7 +2577,7 @@
1.1652 | number_of_elements (Leaf _) =
1.1653 raise REFUTE ("Finite_Set_card_interpreter",
1.1654 "interpretation for set type is a leaf")
1.1655 - val size_of_nat = size_of_type thy model (@{typ nat})
1.1656 + val size_of_nat = size_of_type ctxt model (@{typ nat})
1.1657 (* takes an interpretation for a set and returns an interpretation *)
1.1658 (* for a 'nat' denoting the set's cardinality *)
1.1659 (* interpretation -> interpretation *)
1.1660 @@ -2662,20 +2592,17 @@
1.1661 Leaf (replicate size_of_nat False)
1.1662 end
1.1663 val set_constants =
1.1664 - make_constants thy model (Type ("fun", [T, HOLogic.boolT]))
1.1665 + make_constants ctxt model (Type ("fun", [T, HOLogic.boolT]))
1.1666 in
1.1667 SOME (Node (map card set_constants), model, args)
1.1668 end
1.1669 | _ => NONE;
1.1670
1.1671 -(* theory -> model -> arguments -> Term.term ->
1.1672 - (interpretation * model * arguments) option *)
1.1673 -
1.1674 (* only an optimization: 'finite' could in principle be interpreted with *)
1.1675 (* interpreters available already (using its definition), but the code *)
1.1676 (* below is more efficient *)
1.1677
1.1678 -fun Finite_Set_finite_interpreter thy model args t =
1.1679 +fun Finite_Set_finite_interpreter ctxt model args t =
1.1680 case t of
1.1681 Const (@{const_name Finite_Set.finite},
1.1682 Type ("fun", [Type ("fun", [T, @{typ bool}]),
1.1683 @@ -2688,7 +2615,7 @@
1.1684 @{typ bool}])) =>
1.1685 let
1.1686 val size_of_set =
1.1687 - size_of_type thy model (Type ("fun", [T, HOLogic.boolT]))
1.1688 + size_of_type ctxt model (Type ("fun", [T, HOLogic.boolT]))
1.1689 in
1.1690 (* we only consider finite models anyway, hence EVERY set is *)
1.1691 (* "finite" *)
1.1692 @@ -2696,19 +2623,16 @@
1.1693 end
1.1694 | _ => NONE;
1.1695
1.1696 -(* theory -> model -> arguments -> Term.term ->
1.1697 - (interpretation * model * arguments) option *)
1.1698 -
1.1699 (* only an optimization: 'less' could in principle be interpreted with *)
1.1700 (* interpreters available already (using its definition), but the code *)
1.1701 (* below is more efficient *)
1.1702
1.1703 -fun Nat_less_interpreter thy model args t =
1.1704 +fun Nat_less_interpreter ctxt model args t =
1.1705 case t of
1.1706 Const (@{const_name Orderings.less}, Type ("fun", [@{typ nat},
1.1707 Type ("fun", [@{typ nat}, @{typ bool}])])) =>
1.1708 let
1.1709 - val size_of_nat = size_of_type thy model (@{typ nat})
1.1710 + val size_of_nat = size_of_type ctxt model (@{typ nat})
1.1711 (* the 'n'-th nat is not less than the first 'n' nats, while it *)
1.1712 (* is less than the remaining 'size_of_nat - n' nats *)
1.1713 (* int -> interpretation *)
1.1714 @@ -2718,19 +2642,16 @@
1.1715 end
1.1716 | _ => NONE;
1.1717
1.1718 -(* theory -> model -> arguments -> Term.term ->
1.1719 - (interpretation * model * arguments) option *)
1.1720 -
1.1721 (* only an optimization: 'plus' could in principle be interpreted with *)
1.1722 (* interpreters available already (using its definition), but the code *)
1.1723 (* below is more efficient *)
1.1724
1.1725 -fun Nat_plus_interpreter thy model args t =
1.1726 +fun Nat_plus_interpreter ctxt model args t =
1.1727 case t of
1.1728 Const (@{const_name Groups.plus}, Type ("fun", [@{typ nat},
1.1729 Type ("fun", [@{typ nat}, @{typ nat}])])) =>
1.1730 let
1.1731 - val size_of_nat = size_of_type thy model (@{typ nat})
1.1732 + val size_of_nat = size_of_type ctxt model (@{typ nat})
1.1733 (* int -> int -> interpretation *)
1.1734 fun plus m n =
1.1735 let
1.1736 @@ -2748,19 +2669,16 @@
1.1737 end
1.1738 | _ => NONE;
1.1739
1.1740 -(* theory -> model -> arguments -> Term.term ->
1.1741 - (interpretation * model * arguments) option *)
1.1742 -
1.1743 (* only an optimization: 'minus' could in principle be interpreted *)
1.1744 (* with interpreters available already (using its definition), but the *)
1.1745 (* code below is more efficient *)
1.1746
1.1747 -fun Nat_minus_interpreter thy model args t =
1.1748 +fun Nat_minus_interpreter ctxt model args t =
1.1749 case t of
1.1750 Const (@{const_name Groups.minus}, Type ("fun", [@{typ nat},
1.1751 Type ("fun", [@{typ nat}, @{typ nat}])])) =>
1.1752 let
1.1753 - val size_of_nat = size_of_type thy model (@{typ nat})
1.1754 + val size_of_nat = size_of_type ctxt model (@{typ nat})
1.1755 (* int -> int -> interpretation *)
1.1756 fun minus m n =
1.1757 let
1.1758 @@ -2775,19 +2693,16 @@
1.1759 end
1.1760 | _ => NONE;
1.1761
1.1762 -(* theory -> model -> arguments -> Term.term ->
1.1763 - (interpretation * model * arguments) option *)
1.1764 -
1.1765 (* only an optimization: 'times' could in principle be interpreted *)
1.1766 (* with interpreters available already (using its definition), but the *)
1.1767 (* code below is more efficient *)
1.1768
1.1769 -fun Nat_times_interpreter thy model args t =
1.1770 +fun Nat_times_interpreter ctxt model args t =
1.1771 case t of
1.1772 Const (@{const_name Groups.times}, Type ("fun", [@{typ nat},
1.1773 Type ("fun", [@{typ nat}, @{typ nat}])])) =>
1.1774 let
1.1775 - val size_of_nat = size_of_type thy model (@{typ nat})
1.1776 + val size_of_nat = size_of_type ctxt model (@{typ nat})
1.1777 (* nat -> nat -> interpretation *)
1.1778 fun mult m n =
1.1779 let
1.1780 @@ -2805,20 +2720,17 @@
1.1781 end
1.1782 | _ => NONE;
1.1783
1.1784 -(* theory -> model -> arguments -> Term.term ->
1.1785 - (interpretation * model * arguments) option *)
1.1786 -
1.1787 (* only an optimization: 'append' could in principle be interpreted with *)
1.1788 (* interpreters available already (using its definition), but the code *)
1.1789 (* below is more efficient *)
1.1790
1.1791 -fun List_append_interpreter thy model args t =
1.1792 +fun List_append_interpreter ctxt model args t =
1.1793 case t of
1.1794 Const (@{const_name List.append}, Type ("fun", [Type ("List.list", [T]), Type ("fun",
1.1795 [Type ("List.list", [_]), Type ("List.list", [_])])])) =>
1.1796 let
1.1797 - val size_elem = size_of_type thy model T
1.1798 - val size_list = size_of_type thy model (Type ("List.list", [T]))
1.1799 + val size_elem = size_of_type ctxt model T
1.1800 + val size_list = size_of_type ctxt model (Type ("List.list", [T]))
1.1801 (* maximal length of lists; 0 if we only consider the empty list *)
1.1802 val list_length =
1.1803 let
1.1804 @@ -2901,28 +2813,25 @@
1.1805
1.1806 (* UNSOUND
1.1807
1.1808 -(* theory -> model -> arguments -> Term.term ->
1.1809 - (interpretation * model * arguments) option *)
1.1810 -
1.1811 (* only an optimization: 'lfp' could in principle be interpreted with *)
1.1812 (* interpreters available already (using its definition), but the code *)
1.1813 (* below is more efficient *)
1.1814
1.1815 -fun lfp_interpreter thy model args t =
1.1816 +fun lfp_interpreter ctxt model args t =
1.1817 case t of
1.1818 Const (@{const_name lfp}, Type ("fun", [Type ("fun",
1.1819 [Type ("fun", [T, @{typ bool}]),
1.1820 Type ("fun", [_, @{typ bool}])]),
1.1821 Type ("fun", [_, @{typ bool}])])) =>
1.1822 let
1.1823 - val size_elem = size_of_type thy model T
1.1824 + val size_elem = size_of_type ctxt model T
1.1825 (* the universe (i.e. the set that contains every element) *)
1.1826 val i_univ = Node (replicate size_elem TT)
1.1827 (* all sets with elements from type 'T' *)
1.1828 val i_sets =
1.1829 - make_constants thy model (Type ("fun", [T, HOLogic.boolT]))
1.1830 + make_constants ctxt model (Type ("fun", [T, HOLogic.boolT]))
1.1831 (* all functions that map sets to sets *)
1.1832 - val i_funs = make_constants thy model (Type ("fun",
1.1833 + val i_funs = make_constants ctxt model (Type ("fun",
1.1834 [Type ("fun", [T, @{typ bool}]),
1.1835 Type ("fun", [T, @{typ bool}])]))
1.1836 (* "lfp(f) == Inter({u. f(u) <= u})" *)
1.1837 @@ -2954,28 +2863,25 @@
1.1838 end
1.1839 | _ => NONE;
1.1840
1.1841 -(* theory -> model -> arguments -> Term.term ->
1.1842 - (interpretation * model * arguments) option *)
1.1843 -
1.1844 (* only an optimization: 'gfp' could in principle be interpreted with *)
1.1845 (* interpreters available already (using its definition), but the code *)
1.1846 (* below is more efficient *)
1.1847
1.1848 -fun gfp_interpreter thy model args t =
1.1849 +fun gfp_interpreter ctxt model args t =
1.1850 case t of
1.1851 Const (@{const_name gfp}, Type ("fun", [Type ("fun",
1.1852 [Type ("fun", [T, @{typ bool}]),
1.1853 Type ("fun", [_, @{typ bool}])]),
1.1854 Type ("fun", [_, @{typ bool}])])) =>
1.1855 let
1.1856 - val size_elem = size_of_type thy model T
1.1857 + val size_elem = size_of_type ctxt model T
1.1858 (* the universe (i.e. the set that contains every element) *)
1.1859 val i_univ = Node (replicate size_elem TT)
1.1860 (* all sets with elements from type 'T' *)
1.1861 val i_sets =
1.1862 - make_constants thy model (Type ("fun", [T, HOLogic.boolT]))
1.1863 + make_constants ctxt model (Type ("fun", [T, HOLogic.boolT]))
1.1864 (* all functions that map sets to sets *)
1.1865 - val i_funs = make_constants thy model (Type ("fun",
1.1866 + val i_funs = make_constants ctxt model (Type ("fun",
1.1867 [Type ("fun", [T, HOLogic.boolT]),
1.1868 Type ("fun", [T, HOLogic.boolT])]))
1.1869 (* "gfp(f) == Union({u. u <= f(u)})" *)
1.1870 @@ -3009,37 +2915,31 @@
1.1871 | _ => NONE;
1.1872 *)
1.1873
1.1874 -(* theory -> model -> arguments -> Term.term ->
1.1875 - (interpretation * model * arguments) option *)
1.1876 -
1.1877 (* only an optimization: 'fst' could in principle be interpreted with *)
1.1878 (* interpreters available already (using its definition), but the code *)
1.1879 (* below is more efficient *)
1.1880
1.1881 -fun Product_Type_fst_interpreter thy model args t =
1.1882 +fun Product_Type_fst_interpreter ctxt model args t =
1.1883 case t of
1.1884 Const (@{const_name fst}, Type ("fun", [Type (@{type_name Product_Type.prod}, [T, U]), _])) =>
1.1885 let
1.1886 - val constants_T = make_constants thy model T
1.1887 - val size_U = size_of_type thy model U
1.1888 + val constants_T = make_constants ctxt model T
1.1889 + val size_U = size_of_type ctxt model U
1.1890 in
1.1891 SOME (Node (maps (replicate size_U) constants_T), model, args)
1.1892 end
1.1893 | _ => NONE;
1.1894
1.1895 -(* theory -> model -> arguments -> Term.term ->
1.1896 - (interpretation * model * arguments) option *)
1.1897 -
1.1898 (* only an optimization: 'snd' could in principle be interpreted with *)
1.1899 (* interpreters available already (using its definition), but the code *)
1.1900 (* below is more efficient *)
1.1901
1.1902 -fun Product_Type_snd_interpreter thy model args t =
1.1903 +fun Product_Type_snd_interpreter ctxt model args t =
1.1904 case t of
1.1905 Const (@{const_name snd}, Type ("fun", [Type (@{type_name Product_Type.prod}, [T, U]), _])) =>
1.1906 let
1.1907 - val size_T = size_of_type thy model T
1.1908 - val constants_U = make_constants thy model U
1.1909 + val size_T = size_of_type ctxt model T
1.1910 + val constants_U = make_constants ctxt model U
1.1911 in
1.1912 SOME (Node (flat (replicate size_T constants_U)), model, args)
1.1913 end
1.1914 @@ -3050,10 +2950,7 @@
1.1915 (* PRINTERS *)
1.1916 (* ------------------------------------------------------------------------- *)
1.1917
1.1918 -(* theory -> model -> Term.typ -> interpretation -> (int -> bool) ->
1.1919 - Term.term option *)
1.1920 -
1.1921 -fun stlc_printer thy model T intr assignment =
1.1922 +fun stlc_printer ctxt model T intr assignment =
1.1923 let
1.1924 (* string -> string *)
1.1925 fun strip_leading_quote s =
1.1926 @@ -3075,7 +2972,7 @@
1.1927 Type ("fun", [T1, T2]) =>
1.1928 let
1.1929 (* create all constants of type 'T1' *)
1.1930 - val constants = make_constants thy model T1
1.1931 + val constants = make_constants ctxt model T1
1.1932 (* interpretation list *)
1.1933 val results =
1.1934 (case intr of
1.1935 @@ -3085,8 +2982,8 @@
1.1936 (* Term.term list *)
1.1937 val pairs = map (fn (arg, result) =>
1.1938 HOLogic.mk_prod
1.1939 - (print thy model T1 arg assignment,
1.1940 - print thy model T2 result assignment))
1.1941 + (print ctxt model T1 arg assignment,
1.1942 + print ctxt model T2 result assignment))
1.1943 (constants ~~ results)
1.1944 (* Term.typ *)
1.1945 val HOLogic_prodT = HOLogic.mk_prodT (T1, T2)
1.1946 @@ -3125,100 +3022,101 @@
1.1947 string_of_int (index_from_interpretation intr), T))
1.1948 end;
1.1949
1.1950 -(* theory -> model -> Term.typ -> interpretation -> (int -> bool) ->
1.1951 - Term.term option *)
1.1952 -
1.1953 -fun IDT_printer thy model T intr assignment =
1.1954 - (case T of
1.1955 - Type (s, Ts) =>
1.1956 - (case Datatype.get_info thy s of
1.1957 - SOME info => (* inductive datatype *)
1.1958 - let
1.1959 - val (typs, _) = model
1.1960 - val index = #index info
1.1961 - val descr = #descr info
1.1962 - val (_, dtyps, constrs) = the (AList.lookup (op =) descr index)
1.1963 - val typ_assoc = dtyps ~~ Ts
1.1964 - (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
1.1965 - val _ =
1.1966 - if Library.exists (fn d =>
1.1967 - case d of Datatype_Aux.DtTFree _ => false | _ => true) dtyps
1.1968 - then
1.1969 - raise REFUTE ("IDT_printer", "datatype argument (for type " ^
1.1970 - Syntax.string_of_typ_global thy (Type (s, Ts)) ^ ") is not a variable")
1.1971 - else ()
1.1972 - (* the index of the element in the datatype *)
1.1973 - val element =
1.1974 - (case intr of
1.1975 - Leaf xs => find_index (PropLogic.eval assignment) xs
1.1976 - | Node _ => raise REFUTE ("IDT_printer",
1.1977 - "interpretation is not a leaf"))
1.1978 - in
1.1979 - if element < 0 then
1.1980 - SOME (Const (@{const_name undefined}, Type (s, Ts)))
1.1981 - else
1.1982 - let
1.1983 - (* takes a datatype constructor, and if for some arguments this *)
1.1984 - (* constructor generates the datatype's element that is given by *)
1.1985 - (* 'element', returns the constructor (as a term) as well as the *)
1.1986 - (* indices of the arguments *)
1.1987 - fun get_constr_args (cname, cargs) =
1.1988 - let
1.1989 - val cTerm = Const (cname,
1.1990 - map (typ_of_dtyp descr typ_assoc) cargs ---> Type (s, Ts))
1.1991 - val (iC, _, _) = interpret thy (typs, []) {maxvars=0,
1.1992 - def_eq=false, next_idx=1, bounds=[], wellformed=True} cTerm
1.1993 - (* interpretation -> int list option *)
1.1994 - fun get_args (Leaf xs) =
1.1995 - if find_index (fn x => x = True) xs = element then
1.1996 - SOME []
1.1997 - else
1.1998 - NONE
1.1999 - | get_args (Node xs) =
1.2000 - let
1.2001 - (* interpretation * int -> int list option *)
1.2002 - fun search ([], _) =
1.2003 +fun IDT_printer ctxt model T intr assignment =
1.2004 + let
1.2005 + val thy = ProofContext.theory_of ctxt
1.2006 + in
1.2007 + (case T of
1.2008 + Type (s, Ts) =>
1.2009 + (case Datatype.get_info thy s of
1.2010 + SOME info => (* inductive datatype *)
1.2011 + let
1.2012 + val (typs, _) = model
1.2013 + val index = #index info
1.2014 + val descr = #descr info
1.2015 + val (_, dtyps, constrs) = the (AList.lookup (op =) descr index)
1.2016 + val typ_assoc = dtyps ~~ Ts
1.2017 + (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
1.2018 + val _ =
1.2019 + if Library.exists (fn d =>
1.2020 + case d of Datatype_Aux.DtTFree _ => false | _ => true) dtyps
1.2021 + then
1.2022 + raise REFUTE ("IDT_printer", "datatype argument (for type " ^
1.2023 + Syntax.string_of_typ ctxt (Type (s, Ts)) ^ ") is not a variable")
1.2024 + else ()
1.2025 + (* the index of the element in the datatype *)
1.2026 + val element =
1.2027 + (case intr of
1.2028 + Leaf xs => find_index (PropLogic.eval assignment) xs
1.2029 + | Node _ => raise REFUTE ("IDT_printer",
1.2030 + "interpretation is not a leaf"))
1.2031 + in
1.2032 + if element < 0 then
1.2033 + SOME (Const (@{const_name undefined}, Type (s, Ts)))
1.2034 + else
1.2035 + let
1.2036 + (* takes a datatype constructor, and if for some arguments this *)
1.2037 + (* constructor generates the datatype's element that is given by *)
1.2038 + (* 'element', returns the constructor (as a term) as well as the *)
1.2039 + (* indices of the arguments *)
1.2040 + fun get_constr_args (cname, cargs) =
1.2041 + let
1.2042 + val cTerm = Const (cname,
1.2043 + map (typ_of_dtyp descr typ_assoc) cargs ---> Type (s, Ts))
1.2044 + val (iC, _, _) = interpret ctxt (typs, []) {maxvars=0,
1.2045 + def_eq=false, next_idx=1, bounds=[], wellformed=True} cTerm
1.2046 + (* interpretation -> int list option *)
1.2047 + fun get_args (Leaf xs) =
1.2048 + if find_index (fn x => x = True) xs = element then
1.2049 + SOME []
1.2050 + else
1.2051 NONE
1.2052 - | search (x::xs, n) =
1.2053 - (case get_args x of
1.2054 - SOME result => SOME (n::result)
1.2055 - | NONE => search (xs, n+1))
1.2056 - in
1.2057 - search (xs, 0)
1.2058 - end
1.2059 - in
1.2060 - Option.map (fn args => (cTerm, cargs, args)) (get_args iC)
1.2061 - end
1.2062 - val (cTerm, cargs, args) =
1.2063 - (* we could speed things up by computing the correct *)
1.2064 - (* constructor directly (rather than testing all *)
1.2065 - (* constructors), based on the order in which constructors *)
1.2066 - (* generate elements of datatypes; the current implementation *)
1.2067 - (* of 'IDT_printer' however is independent of the internals *)
1.2068 - (* of 'IDT_constructor_interpreter' *)
1.2069 - (case get_first get_constr_args constrs of
1.2070 - SOME x => x
1.2071 - | NONE => raise REFUTE ("IDT_printer",
1.2072 - "no matching constructor found for element " ^
1.2073 - string_of_int element))
1.2074 - val argsTerms = map (fn (d, n) =>
1.2075 - let
1.2076 - val dT = typ_of_dtyp descr typ_assoc d
1.2077 - (* we only need the n-th element of this list, so there *)
1.2078 - (* might be a more efficient implementation that does not *)
1.2079 - (* generate all constants *)
1.2080 - val consts = make_constants thy (typs, []) dT
1.2081 - in
1.2082 - print thy (typs, []) dT (List.nth (consts, n)) assignment
1.2083 - end) (cargs ~~ args)
1.2084 - in
1.2085 - SOME (list_comb (cTerm, argsTerms))
1.2086 - end
1.2087 - end
1.2088 - | NONE => (* not an inductive datatype *)
1.2089 - NONE)
1.2090 - | _ => (* a (free or schematic) type variable *)
1.2091 - NONE);
1.2092 + | get_args (Node xs) =
1.2093 + let
1.2094 + (* interpretation * int -> int list option *)
1.2095 + fun search ([], _) =
1.2096 + NONE
1.2097 + | search (x::xs, n) =
1.2098 + (case get_args x of
1.2099 + SOME result => SOME (n::result)
1.2100 + | NONE => search (xs, n+1))
1.2101 + in
1.2102 + search (xs, 0)
1.2103 + end
1.2104 + in
1.2105 + Option.map (fn args => (cTerm, cargs, args)) (get_args iC)
1.2106 + end
1.2107 + val (cTerm, cargs, args) =
1.2108 + (* we could speed things up by computing the correct *)
1.2109 + (* constructor directly (rather than testing all *)
1.2110 + (* constructors), based on the order in which constructors *)
1.2111 + (* generate elements of datatypes; the current implementation *)
1.2112 + (* of 'IDT_printer' however is independent of the internals *)
1.2113 + (* of 'IDT_constructor_interpreter' *)
1.2114 + (case get_first get_constr_args constrs of
1.2115 + SOME x => x
1.2116 + | NONE => raise REFUTE ("IDT_printer",
1.2117 + "no matching constructor found for element " ^
1.2118 + string_of_int element))
1.2119 + val argsTerms = map (fn (d, n) =>
1.2120 + let
1.2121 + val dT = typ_of_dtyp descr typ_assoc d
1.2122 + (* we only need the n-th element of this list, so there *)
1.2123 + (* might be a more efficient implementation that does not *)
1.2124 + (* generate all constants *)
1.2125 + val consts = make_constants ctxt (typs, []) dT
1.2126 + in
1.2127 + print ctxt (typs, []) dT (List.nth (consts, n)) assignment
1.2128 + end) (cargs ~~ args)
1.2129 + in
1.2130 + SOME (list_comb (cTerm, argsTerms))
1.2131 + end
1.2132 + end
1.2133 + | NONE => (* not an inductive datatype *)
1.2134 + NONE)
1.2135 + | _ => (* a (free or schematic) type variable *)
1.2136 + NONE)
1.2137 + end;
1.2138
1.2139
1.2140 (* ------------------------------------------------------------------------- *)
1.2141 @@ -3293,7 +3191,7 @@
1.2142 let
1.2143 val thy' = fold set_default_param parms thy;
1.2144 val output =
1.2145 - (case get_default_params thy' of
1.2146 + (case get_default_params (ProofContext.init_global thy') of
1.2147 [] => "none"
1.2148 | new_defaults => cat_lines (map (fn (x, y) => x ^ "=" ^ y) new_defaults));
1.2149 val _ = writeln ("Default parameters for 'refute':\n" ^ output);