# HG changeset patch # User wenzelm # Date 1283504291 -7200 # Node ID 423b72f2d242ec05836ec522d00ba14caa53b3d6 # Parent 4006f5c3f421f2eba4e05fc9e032f1da3a0f55fe prefer regular Proof.context over background theory; misc tuning and simplification; diff -r 4006f5c3f421 -r 423b72f2d242 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Thu Sep 02 17:12:16 2010 +0200 +++ b/src/HOL/Tools/refute.ML Fri Sep 03 10:58:11 2010 +0200 @@ -25,34 +25,34 @@ exception MAXVARS_EXCEEDED - val add_interpreter : string -> (theory -> model -> arguments -> term -> + val add_interpreter : string -> (Proof.context -> model -> arguments -> term -> (interpretation * model * arguments) option) -> theory -> theory - val add_printer : string -> (theory -> model -> typ -> + val add_printer : string -> (Proof.context -> model -> typ -> interpretation -> (int -> bool) -> term option) -> theory -> theory - val interpret : theory -> model -> arguments -> term -> + val interpret : Proof.context -> model -> arguments -> term -> (interpretation * model * arguments) - val print : theory -> model -> typ -> interpretation -> (int -> bool) -> term - val print_model : theory -> model -> (int -> bool) -> string + val print : Proof.context -> model -> typ -> interpretation -> (int -> bool) -> term + val print_model : Proof.context -> model -> (int -> bool) -> string (* ------------------------------------------------------------------------- *) (* Interface *) (* ------------------------------------------------------------------------- *) val set_default_param : (string * string) -> theory -> theory - val get_default_param : theory -> string -> string option - val get_default_params : theory -> (string * string) list - val actual_params : theory -> (string * string) list -> params + val get_default_param : Proof.context -> string -> string option + val get_default_params : Proof.context -> (string * string) list + val actual_params : Proof.context -> (string * string) list -> params - val find_model : theory -> params -> term list -> term -> bool -> unit + val find_model : Proof.context -> params -> term list -> term -> bool -> unit (* tries to find a model for a formula: *) val satisfy_term : - theory -> (string * string) list -> term list -> term -> unit + Proof.context -> (string * string) list -> term list -> term -> unit (* tries to find a model that refutes a formula: *) val refute_term : - theory -> (string * string) list -> term list -> term -> unit + Proof.context -> (string * string) list -> term list -> term -> unit val refute_goal : Proof.context -> (string * string) list -> thm -> int -> unit @@ -74,7 +74,6 @@ val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ end; - structure Refute : REFUTE = struct @@ -207,12 +206,12 @@ }; -structure RefuteData = Theory_Data +structure Data = Theory_Data ( type T = - {interpreters: (string * (theory -> model -> arguments -> term -> + {interpreters: (string * (Proof.context -> model -> arguments -> term -> (interpretation * model * arguments) option)) list, - printers: (string * (theory -> model -> typ -> interpretation -> + printers: (string * (Proof.context -> model -> typ -> interpretation -> (int -> bool) -> term option)) list, parameters: string Symtab.table}; val empty = {interpreters = [], printers = [], parameters = Symtab.empty}; @@ -225,6 +224,8 @@ parameters = Symtab.merge (op=) (pa1, pa2)}; ); +val get_data = Data.get o ProofContext.theory_of; + (* ------------------------------------------------------------------------- *) (* interpret: interprets the term 't' using a suitable interpreter; returns *) @@ -232,14 +233,11 @@ (* track of the interpretation of subterms *) (* ------------------------------------------------------------------------- *) -(* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) *) - -fun interpret thy model args t = - case get_first (fn (_, f) => f thy model args t) - (#interpreters (RefuteData.get thy)) of +fun interpret ctxt model args t = + case get_first (fn (_, f) => f ctxt model args t) + (#interpreters (get_data ctxt)) of NONE => raise REFUTE ("interpret", - "no interpreter for term " ^ quote (Syntax.string_of_term_global thy t)) + "no interpreter for term " ^ quote (Syntax.string_of_term ctxt t)) | SOME x => x; (* ------------------------------------------------------------------------- *) @@ -247,14 +245,11 @@ (* type 'T', into a term using a suitable printer *) (* ------------------------------------------------------------------------- *) -(* theory -> model -> Term.typ -> interpretation -> (int -> bool) -> - Term.term *) - -fun print thy model T intr assignment = - case get_first (fn (_, f) => f thy model T intr assignment) - (#printers (RefuteData.get thy)) of +fun print ctxt model T intr assignment = + case get_first (fn (_, f) => f ctxt model T intr assignment) + (#printers (get_data ctxt)) of NONE => raise REFUTE ("print", - "no printer for type " ^ quote (Syntax.string_of_typ_global thy T)) + "no printer for type " ^ quote (Syntax.string_of_typ ctxt T)) | SOME x => x; (* ------------------------------------------------------------------------- *) @@ -263,9 +258,7 @@ (* printers *) (* ------------------------------------------------------------------------- *) -(* theory -> model -> (int -> bool) -> string *) - -fun print_model thy model assignment = +fun print_model ctxt model assignment = let val (typs, terms) = model val typs_msg = @@ -273,7 +266,7 @@ "empty universe (no type variables in term)\n" else "Size of types: " ^ commas (map (fn (T, i) => - Syntax.string_of_typ_global thy T ^ ": " ^ string_of_int i) typs) ^ "\n" + Syntax.string_of_typ ctxt T ^ ": " ^ string_of_int i) typs) ^ "\n" val show_consts_msg = if not (!show_consts) andalso Library.exists (is_Const o fst) terms then "set \"show_consts\" to show the interpretation of constants\n" @@ -286,9 +279,9 @@ cat_lines (map_filter (fn (t, intr) => (* print constants only if 'show_consts' is true *) if (!show_consts) orelse not (is_Const t) then - SOME (Syntax.string_of_term_global thy t ^ ": " ^ - Syntax.string_of_term_global thy - (print thy model (Term.type_of t) intr assignment)) + SOME (Syntax.string_of_term ctxt t ^ ": " ^ + Syntax.string_of_term ctxt + (print ctxt model (Term.type_of t) intr assignment)) else NONE) terms) ^ "\n" in @@ -300,71 +293,49 @@ (* PARAMETER MANAGEMENT *) (* ------------------------------------------------------------------------- *) -(* string -> (theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option) -> theory -> theory *) - -fun add_interpreter name f thy = - let - val {interpreters, printers, parameters} = RefuteData.get thy - in - case AList.lookup (op =) interpreters name of - NONE => RefuteData.put {interpreters = (name, f) :: interpreters, - printers = printers, parameters = parameters} thy - | SOME _ => error ("Interpreter " ^ name ^ " already declared") - end; +fun add_interpreter name f = Data.map (fn {interpreters, printers, parameters} => + case AList.lookup (op =) interpreters name of + NONE => {interpreters = (name, f) :: interpreters, + printers = printers, parameters = parameters} + | SOME _ => error ("Interpreter " ^ name ^ " already declared")); -(* string -> (theory -> model -> Term.typ -> interpretation -> - (int -> bool) -> Term.term option) -> theory -> theory *) - -fun add_printer name f thy = - let - val {interpreters, printers, parameters} = RefuteData.get thy - in - case AList.lookup (op =) printers name of - NONE => RefuteData.put {interpreters = interpreters, - printers = (name, f) :: printers, parameters = parameters} thy - | SOME _ => error ("Printer " ^ name ^ " already declared") - end; +fun add_printer name f = Data.map (fn {interpreters, printers, parameters} => + case AList.lookup (op =) printers name of + NONE => {interpreters = interpreters, + printers = (name, f) :: printers, parameters = parameters} + | SOME _ => error ("Printer " ^ name ^ " already declared")); (* ------------------------------------------------------------------------- *) -(* set_default_param: stores the '(name, value)' pair in RefuteData's *) +(* set_default_param: stores the '(name, value)' pair in Data's *) (* parameter table *) (* ------------------------------------------------------------------------- *) -(* (string * string) -> theory -> theory *) - -fun set_default_param (name, value) = RefuteData.map +fun set_default_param (name, value) = Data.map (fn {interpreters, printers, parameters} => {interpreters = interpreters, printers = printers, parameters = Symtab.update (name, value) parameters}); (* ------------------------------------------------------------------------- *) (* get_default_param: retrieves the value associated with 'name' from *) -(* RefuteData's parameter table *) +(* Data's parameter table *) (* ------------------------------------------------------------------------- *) -(* theory -> string -> string option *) - -val get_default_param = Symtab.lookup o #parameters o RefuteData.get; +val get_default_param = Symtab.lookup o #parameters o get_data; (* ------------------------------------------------------------------------- *) (* get_default_params: returns a list of all '(name, value)' pairs that are *) -(* stored in RefuteData's parameter table *) +(* stored in Data's parameter table *) (* ------------------------------------------------------------------------- *) -(* theory -> (string * string) list *) - -val get_default_params = Symtab.dest o #parameters o RefuteData.get; +val get_default_params = Symtab.dest o #parameters o get_data; (* ------------------------------------------------------------------------- *) (* actual_params: takes a (possibly empty) list 'params' of parameters that *) -(* override the default parameters currently specified in 'thy', and *) +(* override the default parameters currently specified, and *) (* returns a record that can be passed to 'find_model'. *) (* ------------------------------------------------------------------------- *) -(* theory -> (string * string) list -> params *) - -fun actual_params thy override = +fun actual_params ctxt override = let (* (string * string) list * string -> bool *) fun read_bool (parms, name) = @@ -393,7 +364,7 @@ " must be assigned a value") (* 'override' first, defaults last: *) (* (string * string) list *) - val allparams = override @ (get_default_params thy) + val allparams = override @ get_default_params ctxt (* int *) val minsize = read_int (allparams, "minsize") val maxsize = read_int (allparams, "maxsize") @@ -458,8 +429,6 @@ (* denotes membership to an axiomatic type class *) (* ------------------------------------------------------------------------- *) -(* theory -> string * Term.typ -> bool *) - fun is_const_of_class thy (s, T) = let val class_const_names = map Logic.const_of_class (Sign.all_classes thy) @@ -474,8 +443,6 @@ (* of an inductive datatype in 'thy' *) (* ------------------------------------------------------------------------- *) -(* theory -> string * Term.typ -> bool *) - fun is_IDT_constructor thy (s, T) = (case body_type T of Type (s', _) => @@ -491,8 +458,6 @@ (* operator of an inductive datatype in 'thy' *) (* ------------------------------------------------------------------------- *) -(* theory -> string * Term.typ -> bool *) - fun is_IDT_recursor thy (s, T) = let val rec_names = Symtab.fold (append o #rec_names o snd) @@ -521,8 +486,6 @@ (* get_def: looks up the definition of a constant *) (* ------------------------------------------------------------------------- *) -(* theory -> string * Term.typ -> (string * Term.term) option *) - fun get_def thy (s, T) = let (* (string * Term.term) list -> (string * Term.term) option *) @@ -554,8 +517,6 @@ (* get_typedef: looks up the definition of a type, as created by "typedef" *) (* ------------------------------------------------------------------------- *) -(* theory -> Term.typ -> (string * Term.term) option *) - fun get_typedef thy T = let (* (string * Term.term) list -> (string * Term.term) option *) @@ -581,7 +542,7 @@ case type_of_type_definition ax of SOME T' => let - val T'' = (domain_type o domain_type) T' + val T'' = domain_type (domain_type T') val typeSubs = Sign.typ_match thy (T'', T) Vartab.empty in SOME (axname, monomorphic_term typeSubs ax) @@ -599,8 +560,6 @@ (* created by the "axclass" command *) (* ------------------------------------------------------------------------- *) -(* theory -> string -> (string * Term.term) option *) - fun get_classdef thy class = let val axname = class ^ "_class_def" @@ -617,8 +576,6 @@ (* that definition does not need to be unfolded *) (* ------------------------------------------------------------------------- *) -(* theory -> Term.term -> Term.term *) - (* Note: we could intertwine unfolding of constants and beta-(eta-) *) (* normalization; this would save some unfolding for terms where *) (* constants are eliminated by beta-reduction (e.g. 'K c1 c2'). On *) @@ -716,8 +673,6 @@ (* *every* axiom of the theory and collect it if it has a constant/ *) (* type/typeclass in common with the term 't'. *) -(* theory -> Term.term -> Term.term list *) - (* Which axioms are "relevant" for a particular term/type goes hand in *) (* hand with the interpretation of that term/type by its interpreter (see *) (* way below): if the interpretation respects an axiom anyway, the axiom *) @@ -726,8 +681,9 @@ (* To avoid collecting the same axiom multiple times, we use an *) (* accumulator 'axs' which contains all axioms collected so far. *) -fun collect_axioms thy t = +fun collect_axioms ctxt t = let + val thy = ProofContext.theory_of ctxt val _ = tracing "Adding axioms..." val axioms = Theory.all_axioms_of thy fun collect_this_axiom (axname, ax) axs = @@ -744,7 +700,7 @@ TFree (_, sort) => sort | TVar (_, sort) => sort | _ => raise REFUTE ("collect_axioms", - "type " ^ Syntax.string_of_typ_global thy T ^ " is not a variable")) + "type " ^ Syntax.string_of_typ ctxt T ^ " is not a variable")) (* obtain axioms for all superclasses *) val superclasses = sort @ maps (Sign.super_classes thy) sort (* merely an optimization, because 'collect_this_axiom' disallows *) @@ -762,7 +718,7 @@ | [(idx, S)] => (axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax) | _ => raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^ - Syntax.string_of_term_global thy ax ^ + Syntax.string_of_term ctxt ax ^ ") contains more than one type variable"))) class_axioms in @@ -865,13 +821,14 @@ val ax_in = SOME (specialize_type thy (s, T) of_class) (* type match may fail due to sort constraints *) handle Type.TYPE_MATCH => NONE - val ax_1 = Option.map (fn ax => (Syntax.string_of_term_global thy ax, ax)) ax_in + val ax_1 = Option.map (fn ax => (Syntax.string_of_term ctxt ax, ax)) ax_in val ax_2 = Option.map (apsnd (specialize_type thy (s, T))) (get_classdef thy class) in collect_type_axioms T (fold collect_this_axiom (map_filter I [ax_1, ax_2]) axs) end else if is_IDT_constructor thy (s, T) - orelse is_IDT_recursor thy (s, T) then + orelse is_IDT_recursor thy (s, T) + then (* only collect relevant type axioms *) collect_type_axioms T axs else @@ -899,8 +856,9 @@ (* and all mutually recursive IDTs are considered. *) (* ------------------------------------------------------------------------- *) -fun ground_types thy t = +fun ground_types ctxt t = let + val thy = ProofContext.theory_of ctxt fun collect_types T acc = (case T of Type ("fun", [T1, T2]) => collect_types T1 (collect_types T2 acc) @@ -918,7 +876,7 @@ val _ = if Library.exists (fn d => case d of Datatype_Aux.DtTFree _ => false | _ => true) typs then raise REFUTE ("ground_types", "datatype argument (for type " - ^ Syntax.string_of_typ_global thy T ^ ") is not a variable") + ^ Syntax.string_of_typ ctxt T ^ ") is not a variable") else () (* required for mutually recursive datatypes; those need to *) (* be added even if they are an instance of an otherwise non- *) @@ -1081,19 +1039,17 @@ (* find_model: repeatedly calls 'interpret' with appropriate parameters, *) (* applies a SAT solver, and (in case a model is found) displays *) (* the model to the user by calling 'print_model' *) -(* thy : the current theory *) (* {...} : parameters that control the translation/model generation *) (* assm_ts : assumptions to be considered unless "no_assms" is specified *) (* t : term to be translated into a propositional formula *) (* negate : if true, find a model that makes 't' false (rather than true) *) (* ------------------------------------------------------------------------- *) -(* theory -> params -> Term.term -> bool -> unit *) - -fun find_model thy +fun find_model ctxt {sizes, minsize, maxsize, maxvars, maxtime, satsolver, no_assms, expect} assm_ts t negate = let + val thy = ProofContext.theory_of ctxt (* string -> unit *) fun check_expect outcome_code = if expect = "" orelse outcome_code = expect then () @@ -1107,13 +1063,13 @@ else if negate then Logic.list_implies (assm_ts, t) else Logic.mk_conjunction_list (t :: assm_ts) val u = unfold_defs thy t - val _ = tracing ("Unfolded term: " ^ Syntax.string_of_term_global thy u) - val axioms = collect_axioms thy u + val _ = tracing ("Unfolded term: " ^ Syntax.string_of_term ctxt u) + val axioms = collect_axioms ctxt u (* Term.typ list *) - val types = fold (union (op =) o ground_types thy) (u :: axioms) [] + val types = fold (union (op =) o ground_types ctxt) (u :: axioms) [] val _ = tracing ("Ground types: " ^ (if null types then "none." - else commas (map (Syntax.string_of_typ_global thy) types))) + else commas (map (Syntax.string_of_typ ctxt) types))) (* we can only consider fragments of recursive IDTs, so we issue a *) (* warning if the formula contains a recursive IDT *) (* TODO: no warning needed for /positive/ occurrences of IDTs *) @@ -1152,7 +1108,7 @@ (* translate 'u' and all axioms *) val (intrs, (model, args)) = fold_map (fn t' => fn (m, a) => let - val (i, m', a') = interpret thy m a t' + val (i, m', a') = interpret ctxt m a t' in (* set 'def_eq' to 'true' *) (i, (m', {maxvars = #maxvars a', def_eq = true, @@ -1180,7 +1136,7 @@ priority "Invoking SAT solver..."; (case solver fm of SatSolver.SATISFIABLE assignment => - (priority ("*** Model found: ***\n" ^ print_model thy model + (priority ("*** Model found: ***\n" ^ print_model ctxt model (fn i => case assignment i of SOME b => b | NONE => true)); if maybe_spurious then "potential" else "genuine") | SatSolver.UNSATISFIABLE _ => @@ -1225,7 +1181,7 @@ (* enter loop with or without time limit *) priority ("Trying to find a model that " ^ (if negate then "refutes" else "satisfies") ^ ": " - ^ Syntax.string_of_term_global thy t); + ^ Syntax.string_of_term ctxt t); if maxtime > 0 then ( TimeLimit.timeLimit (Time.fromSeconds maxtime) wrapper () @@ -1248,10 +1204,8 @@ (* parameters *) (* ------------------------------------------------------------------------- *) -(* theory -> (string * string) list -> Term.term list -> Term.term -> unit *) - -fun satisfy_term thy params assm_ts t = - find_model thy (actual_params thy params) assm_ts t false; +fun satisfy_term ctxt params assm_ts t = + find_model ctxt (actual_params ctxt params) assm_ts t false; (* ------------------------------------------------------------------------- *) (* refute_term: calls 'find_model' to find a model that refutes 't' *) @@ -1259,9 +1213,7 @@ (* parameters *) (* ------------------------------------------------------------------------- *) -(* theory -> (string * string) list -> Term.term list -> Term.term -> unit *) - -fun refute_term thy params assm_ts t = +fun refute_term ctxt params assm_ts t = let (* disallow schematic type variables, since we cannot properly negate *) (* terms containing them (their logical meaning is that there EXISTS a *) @@ -1309,7 +1261,7 @@ val frees = Term.rename_wrt_term strip_t (strip_all_vars ex_closure) val subst_t = Term.subst_bounds (map Free frees, strip_t) in - find_model thy (actual_params thy params) assm_ts subst_t true + find_model ctxt (actual_params ctxt params) assm_ts subst_t true end; (* ------------------------------------------------------------------------- *) @@ -1327,8 +1279,7 @@ val assms = map term_of (Assumption.all_assms_of ctxt) val (t, frees) = Logic.goal_params t i in - refute_term (ProofContext.theory_of ctxt) params assms - (subst_bounds (frees, t)) + refute_term ctxt params assms (subst_bounds (frees, t)) end end @@ -1343,9 +1294,7 @@ (* variables) *) (* ------------------------------------------------------------------------- *) -(* theory -> model -> Term.typ -> interpretation list *) - -fun make_constants thy model T = +fun make_constants ctxt model T = let (* returns a list with all unit vectors of length n *) (* int -> interpretation list *) @@ -1376,7 +1325,7 @@ | make_constants_intr (Node xs) = map Node (pick_all (length xs) (make_constants_intr (hd xs))) (* obtain the interpretation for a variable of type 'T' *) - val (i, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, + val (i, _, _) = interpret ctxt model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T)) in make_constants_intr i @@ -1387,8 +1336,6 @@ (* (make_constants T)', but implemented more efficiently) *) (* ------------------------------------------------------------------------- *) -(* theory -> model -> Term.typ -> int *) - (* returns 0 for an empty ground type or a function type with empty *) (* codomain, but fails for a function type with empty domain -- *) (* admissibility of datatype constructor argument types (see "Inductive *) @@ -1397,14 +1344,14 @@ (* never occur as the domain of a function type that is the type of a *) (* constructor argument *) -fun size_of_type thy model T = +fun size_of_type ctxt model T = let (* returns the number of elements that have the same tree structure as a *) (* given interpretation *) fun size_of_intr (Leaf xs) = length xs | size_of_intr (Node xs) = Integer.pow (length xs) (size_of_intr (hd xs)) (* obtain the interpretation for a variable of type 'T' *) - val (i, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, + val (i, _, _) = interpret ctxt model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T)) in size_of_intr i @@ -1585,9 +1532,9 @@ (* their arguments) of the size of the argument types *) (* ------------------------------------------------------------------------- *) -fun size_of_dtyp thy typ_sizes descr typ_assoc constructors = +fun size_of_dtyp ctxt typ_sizes descr typ_assoc constructors = Integer.sum (map (fn (_, dtyps) => - Integer.prod (map (size_of_type thy (typ_sizes, []) o + Integer.prod (map (size_of_type ctxt (typ_sizes, []) o (typ_of_dtyp descr typ_assoc)) dtyps)) constructors); @@ -1596,14 +1543,12 @@ (* INTERPRETERS: Actual Interpreters *) (* ------------------------------------------------------------------------- *) -(* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) - (* simply typed lambda calculus: Isabelle's basic term syntax, with type *) (* variables, function types, and propT *) -fun stlc_interpreter thy model args t = +fun stlc_interpreter ctxt model args t = let + val thy = ProofContext.theory_of ctxt val (typs, terms) = model val {maxvars, def_eq, next_idx, bounds, wellformed} = args (* Term.typ -> (interpretation * model * arguments) option *) @@ -1651,7 +1596,7 @@ fun make_copies idx 0 = (idx, [], True) | make_copies idx n = let - val (copy, _, new_args) = interpret thy (typs, []) + val (copy, _, new_args) = interpret ctxt (typs, []) {maxvars = maxvars, def_eq = false, next_idx = idx, bounds = [], wellformed = True} (Free ("dummy", T2)) val (idx', copies, wf') = make_copies (#next_idx new_args) (n-1) @@ -1659,7 +1604,7 @@ (idx', copy :: copies, SAnd (#wellformed new_args, wf')) end val (next, copies, wf) = make_copies next_idx - (size_of_type thy model T1) + (size_of_type ctxt model T1) (* combine copies into a single interpretation *) val intr = Node copies in @@ -1687,13 +1632,13 @@ | Abs (x, T, body) => let (* create all constants of type 'T' *) - val constants = make_constants thy model T + val constants = make_constants ctxt model T (* interpret the 'body' separately for each constant *) val (bodies, (model', args')) = fold_map (fn c => fn (m, a) => let (* add 'c' to 'bounds' *) - val (i', m', a') = interpret thy m {maxvars = #maxvars a, + val (i', m', a') = interpret ctxt m {maxvars = #maxvars a, def_eq = #def_eq a, next_idx = #next_idx a, bounds = (c :: #bounds a), wellformed = #wellformed a} body in @@ -1710,21 +1655,18 @@ | t1 $ t2 => let (* interpret 't1' and 't2' separately *) - val (intr1, model1, args1) = interpret thy model args t1 - val (intr2, model2, args2) = interpret thy model1 args1 t2 + val (intr1, model1, args1) = interpret ctxt model args t1 + val (intr2, model2, args2) = interpret ctxt model1 args1 t2 in SOME (interpretation_apply (intr1, intr2), model2, args2) end) end; -(* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) - -fun Pure_interpreter thy model args t = +fun Pure_interpreter ctxt model args t = case t of Const (@{const_name all}, _) $ t1 => let - val (i, m, a) = interpret thy model args t1 + val (i, m, a) = interpret ctxt model args t1 in case i of Node xs => @@ -1740,40 +1682,37 @@ "\"all\" is followed by a non-function") end | Const (@{const_name all}, _) => - SOME (interpret thy model args (eta_expand t 1)) + SOME (interpret ctxt model args (eta_expand t 1)) | Const (@{const_name "=="}, _) $ t1 $ t2 => let - val (i1, m1, a1) = interpret thy model args t1 - val (i2, m2, a2) = interpret thy m1 a1 t2 + val (i1, m1, a1) = interpret ctxt model args t1 + val (i2, m2, a2) = interpret ctxt m1 a1 t2 in (* we use either 'make_def_equality' or 'make_equality' *) SOME ((if #def_eq args then make_def_equality else make_equality) (i1, i2), m2, a2) end | Const (@{const_name "=="}, _) $ t1 => - SOME (interpret thy model args (eta_expand t 1)) + SOME (interpret ctxt model args (eta_expand t 1)) | Const (@{const_name "=="}, _) => - SOME (interpret thy model args (eta_expand t 2)) + SOME (interpret ctxt model args (eta_expand t 2)) | Const (@{const_name "==>"}, _) $ t1 $ t2 => (* 3-valued logic *) let - val (i1, m1, a1) = interpret thy model args t1 - val (i2, m2, a2) = interpret thy m1 a1 t2 + val (i1, m1, a1) = interpret ctxt model args t1 + val (i2, m2, a2) = interpret ctxt m1 a1 t2 val fmTrue = PropLogic.SOr (toFalse i1, toTrue i2) val fmFalse = PropLogic.SAnd (toTrue i1, toFalse i2) in SOME (Leaf [fmTrue, fmFalse], m2, a2) end | Const (@{const_name "==>"}, _) $ t1 => - SOME (interpret thy model args (eta_expand t 1)) + SOME (interpret ctxt model args (eta_expand t 1)) | Const (@{const_name "==>"}, _) => - SOME (interpret thy model args (eta_expand t 2)) + SOME (interpret ctxt model args (eta_expand t 2)) | _ => NONE; -(* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) - -fun HOLogic_interpreter thy model args t = +fun HOLogic_interpreter ctxt model args t = (* Providing interpretations directly is more efficient than unfolding the *) (* logical constants. In HOL however, logical constants can themselves be *) (* arguments. They are then translated using eta-expansion. *) @@ -1790,7 +1729,7 @@ SOME (FF, model, args) | Const (@{const_name All}, _) $ t1 => (* similar to "all" (Pure) *) let - val (i, m, a) = interpret thy model args t1 + val (i, m, a) = interpret ctxt model args t1 in case i of Node xs => @@ -1806,10 +1745,10 @@ "\"All\" is followed by a non-function") end | Const (@{const_name All}, _) => - SOME (interpret thy model args (eta_expand t 1)) + SOME (interpret ctxt model args (eta_expand t 1)) | Const (@{const_name Ex}, _) $ t1 => let - val (i, m, a) = interpret thy model args t1 + val (i, m, a) = interpret ctxt model args t1 in case i of Node xs => @@ -1825,81 +1764,79 @@ "\"Ex\" is followed by a non-function") end | Const (@{const_name Ex}, _) => - SOME (interpret thy model args (eta_expand t 1)) + SOME (interpret ctxt model args (eta_expand t 1)) | Const (@{const_name HOL.eq}, _) $ t1 $ t2 => (* similar to "==" (Pure) *) let - val (i1, m1, a1) = interpret thy model args t1 - val (i2, m2, a2) = interpret thy m1 a1 t2 + val (i1, m1, a1) = interpret ctxt model args t1 + val (i2, m2, a2) = interpret ctxt m1 a1 t2 in SOME (make_equality (i1, i2), m2, a2) end | Const (@{const_name HOL.eq}, _) $ t1 => - SOME (interpret thy model args (eta_expand t 1)) + SOME (interpret ctxt model args (eta_expand t 1)) | Const (@{const_name HOL.eq}, _) => - SOME (interpret thy model args (eta_expand t 2)) + SOME (interpret ctxt model args (eta_expand t 2)) | Const (@{const_name HOL.conj}, _) $ t1 $ t2 => (* 3-valued logic *) let - val (i1, m1, a1) = interpret thy model args t1 - val (i2, m2, a2) = interpret thy m1 a1 t2 + val (i1, m1, a1) = interpret ctxt model args t1 + val (i2, m2, a2) = interpret ctxt m1 a1 t2 val fmTrue = PropLogic.SAnd (toTrue i1, toTrue i2) val fmFalse = PropLogic.SOr (toFalse i1, toFalse i2) in SOME (Leaf [fmTrue, fmFalse], m2, a2) end | Const (@{const_name HOL.conj}, _) $ t1 => - SOME (interpret thy model args (eta_expand t 1)) + SOME (interpret ctxt model args (eta_expand t 1)) | Const (@{const_name HOL.conj}, _) => - SOME (interpret thy model args (eta_expand t 2)) + SOME (interpret ctxt model args (eta_expand t 2)) (* this would make "undef" propagate, even for formulae like *) (* "False & undef": *) (* SOME (Node [Node [TT, FF], Node [FF, FF]], model, args) *) | Const (@{const_name HOL.disj}, _) $ t1 $ t2 => (* 3-valued logic *) let - val (i1, m1, a1) = interpret thy model args t1 - val (i2, m2, a2) = interpret thy m1 a1 t2 + val (i1, m1, a1) = interpret ctxt model args t1 + val (i2, m2, a2) = interpret ctxt m1 a1 t2 val fmTrue = PropLogic.SOr (toTrue i1, toTrue i2) val fmFalse = PropLogic.SAnd (toFalse i1, toFalse i2) in SOME (Leaf [fmTrue, fmFalse], m2, a2) end | Const (@{const_name HOL.disj}, _) $ t1 => - SOME (interpret thy model args (eta_expand t 1)) + SOME (interpret ctxt model args (eta_expand t 1)) | Const (@{const_name HOL.disj}, _) => - SOME (interpret thy model args (eta_expand t 2)) + SOME (interpret ctxt model args (eta_expand t 2)) (* this would make "undef" propagate, even for formulae like *) (* "True | undef": *) (* SOME (Node [Node [TT, TT], Node [TT, FF]], model, args) *) | Const (@{const_name HOL.implies}, _) $ t1 $ t2 => (* similar to "==>" (Pure) *) (* 3-valued logic *) let - val (i1, m1, a1) = interpret thy model args t1 - val (i2, m2, a2) = interpret thy m1 a1 t2 + val (i1, m1, a1) = interpret ctxt model args t1 + val (i2, m2, a2) = interpret ctxt m1 a1 t2 val fmTrue = PropLogic.SOr (toFalse i1, toTrue i2) val fmFalse = PropLogic.SAnd (toTrue i1, toFalse i2) in SOME (Leaf [fmTrue, fmFalse], m2, a2) end | Const (@{const_name HOL.implies}, _) $ t1 => - SOME (interpret thy model args (eta_expand t 1)) + SOME (interpret ctxt model args (eta_expand t 1)) | Const (@{const_name HOL.implies}, _) => - SOME (interpret thy model args (eta_expand t 2)) + SOME (interpret ctxt model args (eta_expand t 2)) (* this would make "undef" propagate, even for formulae like *) (* "False --> undef": *) (* SOME (Node [Node [TT, FF], Node [TT, TT]], model, args) *) | _ => NONE; -(* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) - (* interprets variables and constants whose type is an IDT (this is *) (* relatively easy and merely requires us to compute the size of the IDT); *) (* constructors of IDTs however are properly interpreted by *) (* 'IDT_constructor_interpreter' *) -fun IDT_interpreter thy model args t = +fun IDT_interpreter ctxt model args t = let + val thy = ProofContext.theory_of ctxt val (typs, terms) = model (* Term.typ -> (interpretation * model * arguments) option *) fun interpret_term (Type (s, Ts)) = @@ -1933,7 +1870,7 @@ then raise REFUTE ("IDT_interpreter", "datatype argument (for type " - ^ Syntax.string_of_typ_global thy (Type (s, Ts)) + ^ Syntax.string_of_typ ctxt (Type (s, Ts)) ^ ") is not a variable") else () (* if the model specifies a depth for the current type, *) @@ -1941,7 +1878,7 @@ val typs' = case depth of NONE => typs | SOME n => AList.update (op =) (Type (s, Ts), n-1) typs (* recursively compute the size of the datatype *) - val size = size_of_dtyp thy typs' descr typ_assoc constrs + val size = size_of_dtyp ctxt typs' descr typ_assoc constrs val next_idx = #next_idx args val next = next_idx+size (* check if 'maxvars' is large enough *) @@ -1982,9 +1919,6 @@ | _ => NONE) end; -(* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) - (* This function imposes an order on the elements of a datatype fragment *) (* as follows: C_i x_1 ... x_n < C_j y_1 ... y_m iff i < j or *) (* (x_1, ..., x_n) < (y_1, ..., y_m). With this order, a constructor is *) @@ -1993,8 +1927,9 @@ (* same for recursive datatypes, although the computation of indices gets *) (* a little tricky. *) -fun IDT_constructor_interpreter thy model args t = +fun IDT_constructor_interpreter ctxt model args t = let + val thy = ProofContext.theory_of ctxt (* returns a list of canonical representations for terms of the type 'T' *) (* It would be nice if we could just use 'print' for this, but 'print' *) (* for IDTs calls 'IDT_constructor_interpreter' again, and this could *) @@ -2057,7 +1992,7 @@ then raise REFUTE ("IDT_constructor_interpreter", "datatype argument (for type " - ^ Syntax.string_of_typ_global thy T + ^ Syntax.string_of_typ ctxt T ^ ") is not a variable") else () (* decrement depth for the IDT 'T' *) @@ -2088,11 +2023,11 @@ | NONE => (* not an inductive datatype; in this case the argument types in *) (* 'Ts' may not be IDTs either, so 'print' should be safe *) - map (fn intr => print thy (typs, []) T intr (K false)) - (make_constants thy (typs, []) T)) + map (fn intr => print ctxt (typs, []) T intr (K false)) + (make_constants ctxt (typs, []) T)) | _ => (* TFree ..., TVar ... *) - map (fn intr => print thy (typs, []) T intr (K false)) - (make_constants thy (typs, []) T)) + map (fn intr => print ctxt (typs, []) T intr (K false)) + (make_constants ctxt (typs, []) T)) val (typs, terms) = model in case AList.lookup (op =) terms t of @@ -2117,7 +2052,7 @@ then raise REFUTE ("IDT_constructor_interpreter", "datatype argument (for type " - ^ Syntax.string_of_typ_global thy (Type (s', Ts')) + ^ Syntax.string_of_typ ctxt (Type (s', Ts')) ^ ") is not a variable") else () (* split the constructors into those occuring before/after *) @@ -2148,12 +2083,12 @@ (* elements of the datatype come before elements generated *) (* by 'Const (s, T)' iff they are generated by a *) (* constructor in constrs1 *) - val offset = size_of_dtyp thy typs' descr typ_assoc constrs1 + val offset = size_of_dtyp ctxt typs' descr typ_assoc constrs1 (* compute the total (current) size of the datatype *) val total = offset + - size_of_dtyp thy typs' descr typ_assoc constrs2 + size_of_dtyp ctxt typs' descr typ_assoc constrs2 (* sanity check *) - val _ = if total <> size_of_type thy (typs, []) + val _ = if total <> size_of_type ctxt (typs, []) (Type (s', Ts')) then raise REFUTE ("IDT_constructor_interpreter", "total is not equal to current size") @@ -2165,7 +2100,7 @@ let (* compute the current size of the type 'd' *) val dT = typ_of_dtyp descr typ_assoc d - val size = size_of_type thy (typs, []) dT + val size = size_of_type ctxt (typs, []) dT in Node (replicate size (make_undef ds)) end @@ -2187,7 +2122,7 @@ val terms' = canonical_terms typs' dT (* sanity check *) val _ = - if length terms' <> size_of_type thy (typs', []) dT + if length terms' <> size_of_type ctxt (typs', []) dT then raise REFUTE ("IDT_constructor_interpreter", "length of terms' is not equal to old size") @@ -2198,7 +2133,7 @@ val terms = canonical_terms typs dT (* sanity check *) val _ = - if length terms <> size_of_type thy (typs, []) dT + if length terms <> size_of_type ctxt (typs, []) dT then raise REFUTE ("IDT_constructor_interpreter", "length of terms is not equal to current size") @@ -2253,350 +2188,348 @@ NONE) end; -(* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) - (* Difficult code ahead. Make sure you understand the *) (* 'IDT_constructor_interpreter' and the order in which it enumerates *) (* elements of an IDT before you try to understand this function. *) -fun IDT_recursion_interpreter thy model args t = - (* careful: here we descend arbitrarily deep into 't', possibly before *) - (* any other interpreter for atomic terms has had a chance to look at *) - (* 't' *) - case strip_comb t of - (Const (s, T), params) => - (* iterate over all datatypes in 'thy' *) - Symtab.fold (fn (_, info) => fn result => - case result of - SOME _ => - result (* just keep 'result' *) - | NONE => - if member (op =) (#rec_names info) s then - (* we do have a recursion operator of one of the (mutually *) - (* recursive) datatypes given by 'info' *) - let - (* number of all constructors, including those of different *) - (* (mutually recursive) datatypes within the same descriptor *) - val mconstrs_count = - Integer.sum (map (fn (_, (_, _, cs)) => length cs) (#descr info)) - in - if mconstrs_count < length params then - (* too many actual parameters; for now we'll use the *) - (* 'stlc_interpreter' to strip off one application *) - NONE - else if mconstrs_count > length params then - (* too few actual parameters; we use eta expansion *) - (* Note that the resulting expansion of lambda abstractions *) - (* by the 'stlc_interpreter' may be rather slow (depending *) - (* on the argument types and the size of the IDT, of *) - (* course). *) - SOME (interpret thy model args (eta_expand t - (mconstrs_count - length params))) - else (* mconstrs_count = length params *) - let - (* interpret each parameter separately *) - val (p_intrs, (model', args')) = fold_map (fn p => fn (m, a) => - let - val (i, m', a') = interpret thy m a p - in - (i, (m', a')) - end) params (model, args) - val (typs, _) = model' - (* 'index' is /not/ necessarily the index of the IDT that *) - (* the recursion operator is associated with, but merely *) - (* the index of some mutually recursive IDT *) - val index = #index info - val descr = #descr info - val (_, dtyps, _) = the (AList.lookup (op =) descr index) - (* sanity check: we assume that the order of constructors *) - (* in 'descr' is the same as the order of *) - (* corresponding parameters, otherwise the *) - (* association code below won't match the *) - (* right constructors/parameters; we also *) - (* assume that the order of recursion *) - (* operators in '#rec_names info' is the *) - (* same as the order of corresponding *) - (* datatypes in 'descr' *) - val _ = if map fst descr <> (0 upto (length descr - 1)) then - raise REFUTE ("IDT_recursion_interpreter", - "order of constructors and corresponding parameters/" ^ - "recursion operators and corresponding datatypes " ^ - "different?") - else () - (* sanity check: every element in 'dtyps' must be a *) - (* 'DtTFree' *) - val _ = - if Library.exists (fn d => - case d of Datatype_Aux.DtTFree _ => false - | _ => true) dtyps - then - raise REFUTE ("IDT_recursion_interpreter", - "datatype argument is not a variable") - else () - (* the type of a recursion operator is *) - (* [T1, ..., Tn, IDT] ---> Tresult *) - val IDT = List.nth (binder_types T, mconstrs_count) - (* by our assumption on the order of recursion operators *) - (* and datatypes, this is the index of the datatype *) - (* corresponding to the given recursion operator *) - val idt_index = find_index (fn s' => s' = s) (#rec_names info) - (* mutually recursive types must have the same type *) - (* parameters, unless the mutual recursion comes from *) - (* indirect recursion *) - fun rec_typ_assoc acc [] = acc - | rec_typ_assoc acc ((d, T)::xs) = - (case AList.lookup op= acc d of - NONE => - (case d of - Datatype_Aux.DtTFree _ => - (* add the association, proceed *) - rec_typ_assoc ((d, T)::acc) xs - | Datatype_Aux.DtType (s, ds) => - let - val (s', Ts) = dest_Type T - in - if s=s' then +fun IDT_recursion_interpreter ctxt model args t = + let + val thy = ProofContext.theory_of ctxt + in + (* careful: here we descend arbitrarily deep into 't', possibly before *) + (* any other interpreter for atomic terms has had a chance to look at *) + (* 't' *) + case strip_comb t of + (Const (s, T), params) => + (* iterate over all datatypes in 'thy' *) + Symtab.fold (fn (_, info) => fn result => + case result of + SOME _ => + result (* just keep 'result' *) + | NONE => + if member (op =) (#rec_names info) s then + (* we do have a recursion operator of one of the (mutually *) + (* recursive) datatypes given by 'info' *) + let + (* number of all constructors, including those of different *) + (* (mutually recursive) datatypes within the same descriptor *) + val mconstrs_count = + Integer.sum (map (fn (_, (_, _, cs)) => length cs) (#descr info)) + in + if mconstrs_count < length params then + (* too many actual parameters; for now we'll use the *) + (* 'stlc_interpreter' to strip off one application *) + NONE + else if mconstrs_count > length params then + (* too few actual parameters; we use eta expansion *) + (* Note that the resulting expansion of lambda abstractions *) + (* by the 'stlc_interpreter' may be rather slow (depending *) + (* on the argument types and the size of the IDT, of *) + (* course). *) + SOME (interpret ctxt model args (eta_expand t + (mconstrs_count - length params))) + else (* mconstrs_count = length params *) + let + (* interpret each parameter separately *) + val (p_intrs, (model', args')) = fold_map (fn p => fn (m, a) => + let + val (i, m', a') = interpret ctxt m a p + in + (i, (m', a')) + end) params (model, args) + val (typs, _) = model' + (* 'index' is /not/ necessarily the index of the IDT that *) + (* the recursion operator is associated with, but merely *) + (* the index of some mutually recursive IDT *) + val index = #index info + val descr = #descr info + val (_, dtyps, _) = the (AList.lookup (op =) descr index) + (* sanity check: we assume that the order of constructors *) + (* in 'descr' is the same as the order of *) + (* corresponding parameters, otherwise the *) + (* association code below won't match the *) + (* right constructors/parameters; we also *) + (* assume that the order of recursion *) + (* operators in '#rec_names info' is the *) + (* same as the order of corresponding *) + (* datatypes in 'descr' *) + val _ = if map fst descr <> (0 upto (length descr - 1)) then + raise REFUTE ("IDT_recursion_interpreter", + "order of constructors and corresponding parameters/" ^ + "recursion operators and corresponding datatypes " ^ + "different?") + else () + (* sanity check: every element in 'dtyps' must be a *) + (* 'DtTFree' *) + val _ = + if Library.exists (fn d => + case d of Datatype_Aux.DtTFree _ => false + | _ => true) dtyps + then + raise REFUTE ("IDT_recursion_interpreter", + "datatype argument is not a variable") + else () + (* the type of a recursion operator is *) + (* [T1, ..., Tn, IDT] ---> Tresult *) + val IDT = List.nth (binder_types T, mconstrs_count) + (* by our assumption on the order of recursion operators *) + (* and datatypes, this is the index of the datatype *) + (* corresponding to the given recursion operator *) + val idt_index = find_index (fn s' => s' = s) (#rec_names info) + (* mutually recursive types must have the same type *) + (* parameters, unless the mutual recursion comes from *) + (* indirect recursion *) + fun rec_typ_assoc acc [] = acc + | rec_typ_assoc acc ((d, T)::xs) = + (case AList.lookup op= acc d of + NONE => + (case d of + Datatype_Aux.DtTFree _ => + (* add the association, proceed *) + rec_typ_assoc ((d, T)::acc) xs + | Datatype_Aux.DtType (s, ds) => + let + val (s', Ts) = dest_Type T + in + if s=s' then + rec_typ_assoc ((d, T)::acc) ((ds ~~ Ts) @ xs) + else + raise REFUTE ("IDT_recursion_interpreter", + "DtType/Type mismatch") + end + | Datatype_Aux.DtRec i => + let + val (_, ds, _) = the (AList.lookup (op =) descr i) + val (_, Ts) = dest_Type T + in rec_typ_assoc ((d, T)::acc) ((ds ~~ Ts) @ xs) - else - raise REFUTE ("IDT_recursion_interpreter", - "DtType/Type mismatch") - end - | Datatype_Aux.DtRec i => - let - val (_, ds, _) = the (AList.lookup (op =) descr i) - val (_, Ts) = dest_Type T - in - rec_typ_assoc ((d, T)::acc) ((ds ~~ Ts) @ xs) - end) - | SOME T' => - if T=T' then - (* ignore the association since it's already *) - (* present, proceed *) - rec_typ_assoc acc xs - else - raise REFUTE ("IDT_recursion_interpreter", - "different type associations for the same dtyp")) - val typ_assoc = filter - (fn (Datatype_Aux.DtTFree _, _) => true | (_, _) => false) - (rec_typ_assoc [] - (#2 (the (AList.lookup (op =) descr idt_index)) ~~ (snd o dest_Type) IDT)) - (* sanity check: typ_assoc must associate types to the *) - (* elements of 'dtyps' (and only to those) *) - val _ = - if not (eq_set (op =) (dtyps, map fst typ_assoc)) - then - raise REFUTE ("IDT_recursion_interpreter", - "type association has extra/missing elements") - else () - (* interpret each constructor in the descriptor (including *) - (* those of mutually recursive datatypes) *) - (* (int * interpretation list) list *) - val mc_intrs = map (fn (idx, (_, _, cs)) => - let - val c_return_typ = typ_of_dtyp descr typ_assoc - (Datatype_Aux.DtRec idx) - in - (idx, map (fn (cname, cargs) => - (#1 o interpret thy (typs, []) {maxvars=0, - def_eq=false, next_idx=1, bounds=[], - wellformed=True}) (Const (cname, map (typ_of_dtyp - descr typ_assoc) cargs ---> c_return_typ))) cs) - end) descr - (* associate constructors with corresponding parameters *) - (* (int * (interpretation * interpretation) list) list *) - val (mc_p_intrs, p_intrs') = fold_map - (fn (idx, c_intrs) => fn p_intrs' => + end) + | SOME T' => + if T=T' then + (* ignore the association since it's already *) + (* present, proceed *) + rec_typ_assoc acc xs + else + raise REFUTE ("IDT_recursion_interpreter", + "different type associations for the same dtyp")) + val typ_assoc = filter + (fn (Datatype_Aux.DtTFree _, _) => true | (_, _) => false) + (rec_typ_assoc [] + (#2 (the (AList.lookup (op =) descr idt_index)) ~~ (snd o dest_Type) IDT)) + (* sanity check: typ_assoc must associate types to the *) + (* elements of 'dtyps' (and only to those) *) + val _ = + if not (eq_set (op =) (dtyps, map fst typ_assoc)) + then + raise REFUTE ("IDT_recursion_interpreter", + "type association has extra/missing elements") + else () + (* interpret each constructor in the descriptor (including *) + (* those of mutually recursive datatypes) *) + (* (int * interpretation list) list *) + val mc_intrs = map (fn (idx, (_, _, cs)) => let - val len = length c_intrs + val c_return_typ = typ_of_dtyp descr typ_assoc + (Datatype_Aux.DtRec idx) in - ((idx, c_intrs ~~ List.take (p_intrs', len)), - List.drop (p_intrs', len)) - end) mc_intrs p_intrs - (* sanity check: no 'p_intr' may be left afterwards *) - val _ = - if p_intrs' <> [] then - raise REFUTE ("IDT_recursion_interpreter", - "more parameter than constructor interpretations") - else () - (* The recursion operator, applied to 'mconstrs_count' *) - (* arguments, is a function that maps every element of the *) - (* inductive datatype to an element of some result type. *) - (* Recursion operators for mutually recursive IDTs are *) - (* translated simultaneously. *) - (* Since the order on datatype elements is given by an *) - (* order on constructors (and then by the order on *) - (* argument tuples), we can simply copy corresponding *) - (* subtrees from 'p_intrs', in the order in which they are *) - (* given. *) - (* interpretation * interpretation -> interpretation list *) - fun ci_pi (Leaf xs, pi) = - (* if the constructor does not match the arguments to a *) - (* defined element of the IDT, the corresponding value *) - (* of the parameter must be ignored *) - if List.exists (equal True) xs then [pi] else [] - | ci_pi (Node xs, Node ys) = maps ci_pi (xs ~~ ys) - | ci_pi (Node _, Leaf _) = - raise REFUTE ("IDT_recursion_interpreter", - "constructor takes more arguments than the " ^ - "associated parameter") - (* (int * interpretation list) list *) - val rec_operators = map (fn (idx, c_p_intrs) => - (idx, maps ci_pi c_p_intrs)) mc_p_intrs - (* sanity check: every recursion operator must provide as *) - (* many values as the corresponding datatype *) - (* has elements *) - val _ = map (fn (idx, intrs) => - let - val T = typ_of_dtyp descr typ_assoc - (Datatype_Aux.DtRec idx) - in - if length intrs <> size_of_type thy (typs, []) T then - raise REFUTE ("IDT_recursion_interpreter", - "wrong number of interpretations for rec. operator") - else () - end) rec_operators - (* For non-recursive datatypes, we are pretty much done at *) - (* this point. For recursive datatypes however, we still *) - (* need to apply the interpretations in 'rec_operators' to *) - (* (recursively obtained) interpretations for recursive *) - (* constructor arguments. To do so more efficiently, we *) - (* copy 'rec_operators' into arrays first. Each Boolean *) - (* indicates whether the recursive arguments have been *) - (* considered already. *) - (* (int * (bool * interpretation) Array.array) list *) - val REC_OPERATORS = map (fn (idx, intrs) => - (idx, Array.fromList (map (pair false) intrs))) - rec_operators - (* takes an interpretation, and if some leaf of this *) - (* interpretation is the 'elem'-th element of the type, *) - (* the indices of the arguments leading to this leaf are *) - (* returned *) - (* interpretation -> int -> int list option *) - fun get_args (Leaf xs) elem = - if find_index (fn x => x = True) xs = elem then - SOME [] - else - NONE - | get_args (Node xs) elem = + (idx, map (fn (cname, cargs) => + (#1 o interpret ctxt (typs, []) {maxvars=0, + def_eq=false, next_idx=1, bounds=[], + wellformed=True}) (Const (cname, map (typ_of_dtyp + descr typ_assoc) cargs ---> c_return_typ))) cs) + end) descr + (* associate constructors with corresponding parameters *) + (* (int * (interpretation * interpretation) list) list *) + val (mc_p_intrs, p_intrs') = fold_map + (fn (idx, c_intrs) => fn p_intrs' => let - (* interpretation list * int -> int list option *) - fun search ([], _) = - NONE - | search (x::xs, n) = - (case get_args x elem of - SOME result => SOME (n::result) - | NONE => search (xs, n+1)) + val len = length c_intrs in - search (xs, 0) - end - (* returns the index of the constructor and indices for *) - (* its arguments that generate the 'elem'-th element of *) - (* the datatype given by 'idx' *) - (* int -> int -> int * int list *) - fun get_cargs idx elem = - let - (* int * interpretation list -> int * int list *) - fun get_cargs_rec (_, []) = - raise REFUTE ("IDT_recursion_interpreter", - "no matching constructor found for datatype element") - | get_cargs_rec (n, x::xs) = - (case get_args x elem of - SOME args => (n, args) - | NONE => get_cargs_rec (n+1, xs)) - in - get_cargs_rec (0, the (AList.lookup (op =) mc_intrs idx)) - end - (* computes one entry in 'REC_OPERATORS', and recursively *) - (* all entries needed for it, where 'idx' gives the *) - (* datatype and 'elem' the element of it *) - (* int -> int -> interpretation *) - fun compute_array_entry idx elem = - let - val arr = the (AList.lookup (op =) REC_OPERATORS idx) - val (flag, intr) = Array.sub (arr, elem) - in - if flag then - (* simply return the previously computed result *) - intr - else - (* we have to apply 'intr' to interpretations for all *) - (* recursive arguments *) - let - (* int * int list *) - val (c, args) = get_cargs idx elem - (* find the indices of the constructor's /recursive/ *) - (* arguments *) - val (_, _, constrs) = the (AList.lookup (op =) descr idx) - val (_, dtyps) = List.nth (constrs, c) - val rec_dtyps_args = filter - (Datatype_Aux.is_rec_type o fst) (dtyps ~~ args) - (* map those indices to interpretations *) - val rec_dtyps_intrs = map (fn (dtyp, arg) => - let - val dT = typ_of_dtyp descr typ_assoc dtyp - val consts = make_constants thy (typs, []) dT - val arg_i = List.nth (consts, arg) - in - (dtyp, arg_i) - end) rec_dtyps_args - (* takes the dtyp and interpretation of an element, *) - (* and computes the interpretation for the *) - (* corresponding recursive argument *) - fun rec_intr (Datatype_Aux.DtRec i) (Leaf xs) = - (* recursive argument is "rec_i params elem" *) - compute_array_entry i (find_index (fn x => x = True) xs) - | rec_intr (Datatype_Aux.DtRec _) (Node _) = - raise REFUTE ("IDT_recursion_interpreter", - "interpretation for IDT is a node") - | rec_intr (Datatype_Aux.DtType ("fun", [dt1, dt2])) (Node xs) = - (* recursive argument is something like *) - (* "\x::dt1. rec_? params (elem x)" *) - Node (map (rec_intr dt2) xs) - | rec_intr (Datatype_Aux.DtType ("fun", [_, _])) (Leaf _) = - raise REFUTE ("IDT_recursion_interpreter", - "interpretation for function dtyp is a leaf") - | rec_intr _ _ = - (* admissibility ensures that every recursive type *) - (* is of the form 'Dt_1 -> ... -> Dt_k -> *) - (* (DtRec i)' *) - raise REFUTE ("IDT_recursion_interpreter", - "non-recursive codomain in recursive dtyp") - (* obtain interpretations for recursive arguments *) - (* interpretation list *) - val arg_intrs = map (uncurry rec_intr) rec_dtyps_intrs - (* apply 'intr' to all recursive arguments *) - val result = fold (fn arg_i => fn i => - interpretation_apply (i, arg_i)) arg_intrs intr - (* update 'REC_OPERATORS' *) - val _ = Array.update (arr, elem, (true, result)) - in - result - end - end - val idt_size = Array.length (the (AList.lookup (op =) REC_OPERATORS idt_index)) - (* sanity check: the size of 'IDT' should be 'idt_size' *) - val _ = - if idt_size <> size_of_type thy (typs, []) IDT then + ((idx, c_intrs ~~ List.take (p_intrs', len)), + List.drop (p_intrs', len)) + end) mc_intrs p_intrs + (* sanity check: no 'p_intr' may be left afterwards *) + val _ = + if p_intrs' <> [] then raise REFUTE ("IDT_recursion_interpreter", - "unexpected size of IDT (wrong type associated?)") + "more parameter than constructor interpretations") else () - (* interpretation *) - val rec_op = Node (map_range (compute_array_entry idt_index) idt_size) - in - SOME (rec_op, model', args') - end - end - else - NONE (* not a recursion operator of this datatype *) - ) (Datatype.get_all thy) NONE - | _ => (* head of term is not a constant *) - NONE; + (* The recursion operator, applied to 'mconstrs_count' *) + (* arguments, is a function that maps every element of the *) + (* inductive datatype to an element of some result type. *) + (* Recursion operators for mutually recursive IDTs are *) + (* translated simultaneously. *) + (* Since the order on datatype elements is given by an *) + (* order on constructors (and then by the order on *) + (* argument tuples), we can simply copy corresponding *) + (* subtrees from 'p_intrs', in the order in which they are *) + (* given. *) + (* interpretation * interpretation -> interpretation list *) + fun ci_pi (Leaf xs, pi) = + (* if the constructor does not match the arguments to a *) + (* defined element of the IDT, the corresponding value *) + (* of the parameter must be ignored *) + if List.exists (equal True) xs then [pi] else [] + | ci_pi (Node xs, Node ys) = maps ci_pi (xs ~~ ys) + | ci_pi (Node _, Leaf _) = + raise REFUTE ("IDT_recursion_interpreter", + "constructor takes more arguments than the " ^ + "associated parameter") + (* (int * interpretation list) list *) + val rec_operators = map (fn (idx, c_p_intrs) => + (idx, maps ci_pi c_p_intrs)) mc_p_intrs + (* sanity check: every recursion operator must provide as *) + (* many values as the corresponding datatype *) + (* has elements *) + val _ = map (fn (idx, intrs) => + let + val T = typ_of_dtyp descr typ_assoc + (Datatype_Aux.DtRec idx) + in + if length intrs <> size_of_type ctxt (typs, []) T then + raise REFUTE ("IDT_recursion_interpreter", + "wrong number of interpretations for rec. operator") + else () + end) rec_operators + (* For non-recursive datatypes, we are pretty much done at *) + (* this point. For recursive datatypes however, we still *) + (* need to apply the interpretations in 'rec_operators' to *) + (* (recursively obtained) interpretations for recursive *) + (* constructor arguments. To do so more efficiently, we *) + (* copy 'rec_operators' into arrays first. Each Boolean *) + (* indicates whether the recursive arguments have been *) + (* considered already. *) + (* (int * (bool * interpretation) Array.array) list *) + val REC_OPERATORS = map (fn (idx, intrs) => + (idx, Array.fromList (map (pair false) intrs))) + rec_operators + (* takes an interpretation, and if some leaf of this *) + (* interpretation is the 'elem'-th element of the type, *) + (* the indices of the arguments leading to this leaf are *) + (* returned *) + (* interpretation -> int -> int list option *) + fun get_args (Leaf xs) elem = + if find_index (fn x => x = True) xs = elem then + SOME [] + else + NONE + | get_args (Node xs) elem = + let + (* interpretation list * int -> int list option *) + fun search ([], _) = + NONE + | search (x::xs, n) = + (case get_args x elem of + SOME result => SOME (n::result) + | NONE => search (xs, n+1)) + in + search (xs, 0) + end + (* returns the index of the constructor and indices for *) + (* its arguments that generate the 'elem'-th element of *) + (* the datatype given by 'idx' *) + (* int -> int -> int * int list *) + fun get_cargs idx elem = + let + (* int * interpretation list -> int * int list *) + fun get_cargs_rec (_, []) = + raise REFUTE ("IDT_recursion_interpreter", + "no matching constructor found for datatype element") + | get_cargs_rec (n, x::xs) = + (case get_args x elem of + SOME args => (n, args) + | NONE => get_cargs_rec (n+1, xs)) + in + get_cargs_rec (0, the (AList.lookup (op =) mc_intrs idx)) + end + (* computes one entry in 'REC_OPERATORS', and recursively *) + (* all entries needed for it, where 'idx' gives the *) + (* datatype and 'elem' the element of it *) + (* int -> int -> interpretation *) + fun compute_array_entry idx elem = + let + val arr = the (AList.lookup (op =) REC_OPERATORS idx) + val (flag, intr) = Array.sub (arr, elem) + in + if flag then + (* simply return the previously computed result *) + intr + else + (* we have to apply 'intr' to interpretations for all *) + (* recursive arguments *) + let + (* int * int list *) + val (c, args) = get_cargs idx elem + (* find the indices of the constructor's /recursive/ *) + (* arguments *) + val (_, _, constrs) = the (AList.lookup (op =) descr idx) + val (_, dtyps) = List.nth (constrs, c) + val rec_dtyps_args = filter + (Datatype_Aux.is_rec_type o fst) (dtyps ~~ args) + (* map those indices to interpretations *) + val rec_dtyps_intrs = map (fn (dtyp, arg) => + let + val dT = typ_of_dtyp descr typ_assoc dtyp + val consts = make_constants ctxt (typs, []) dT + val arg_i = List.nth (consts, arg) + in + (dtyp, arg_i) + end) rec_dtyps_args + (* takes the dtyp and interpretation of an element, *) + (* and computes the interpretation for the *) + (* corresponding recursive argument *) + fun rec_intr (Datatype_Aux.DtRec i) (Leaf xs) = + (* recursive argument is "rec_i params elem" *) + compute_array_entry i (find_index (fn x => x = True) xs) + | rec_intr (Datatype_Aux.DtRec _) (Node _) = + raise REFUTE ("IDT_recursion_interpreter", + "interpretation for IDT is a node") + | rec_intr (Datatype_Aux.DtType ("fun", [dt1, dt2])) (Node xs) = + (* recursive argument is something like *) + (* "\x::dt1. rec_? params (elem x)" *) + Node (map (rec_intr dt2) xs) + | rec_intr (Datatype_Aux.DtType ("fun", [_, _])) (Leaf _) = + raise REFUTE ("IDT_recursion_interpreter", + "interpretation for function dtyp is a leaf") + | rec_intr _ _ = + (* admissibility ensures that every recursive type *) + (* is of the form 'Dt_1 -> ... -> Dt_k -> *) + (* (DtRec i)' *) + raise REFUTE ("IDT_recursion_interpreter", + "non-recursive codomain in recursive dtyp") + (* obtain interpretations for recursive arguments *) + (* interpretation list *) + val arg_intrs = map (uncurry rec_intr) rec_dtyps_intrs + (* apply 'intr' to all recursive arguments *) + val result = fold (fn arg_i => fn i => + interpretation_apply (i, arg_i)) arg_intrs intr + (* update 'REC_OPERATORS' *) + val _ = Array.update (arr, elem, (true, result)) + in + result + end + end + val idt_size = Array.length (the (AList.lookup (op =) REC_OPERATORS idt_index)) + (* sanity check: the size of 'IDT' should be 'idt_size' *) + val _ = + if idt_size <> size_of_type ctxt (typs, []) IDT then + raise REFUTE ("IDT_recursion_interpreter", + "unexpected size of IDT (wrong type associated?)") + else () + (* interpretation *) + val rec_op = Node (map_range (compute_array_entry idt_index) idt_size) + in + SOME (rec_op, model', args') + end + end + else + NONE (* not a recursion operator of this datatype *) + ) (Datatype.get_all thy) NONE + | _ => (* head of term is not a constant *) + NONE + end; -(* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) - -fun set_interpreter thy model args t = +fun set_interpreter ctxt model args t = let val (typs, terms) = model in @@ -2608,27 +2541,24 @@ (case t of (* 'Collect' == identity *) Const (@{const_name Collect}, _) $ t1 => - SOME (interpret thy model args t1) + SOME (interpret ctxt model args t1) | Const (@{const_name Collect}, _) => - SOME (interpret thy model args (eta_expand t 1)) + SOME (interpret ctxt model args (eta_expand t 1)) (* 'op :' == application *) | Const (@{const_name Set.member}, _) $ t1 $ t2 => - SOME (interpret thy model args (t2 $ t1)) + SOME (interpret ctxt model args (t2 $ t1)) | Const (@{const_name Set.member}, _) $ t1 => - SOME (interpret thy model args (eta_expand t 1)) + SOME (interpret ctxt model args (eta_expand t 1)) | Const (@{const_name Set.member}, _) => - SOME (interpret thy model args (eta_expand t 2)) + SOME (interpret ctxt model args (eta_expand t 2)) | _ => NONE) end; -(* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) - (* only an optimization: 'card' could in principle be interpreted with *) (* interpreters available already (using its definition), but the code *) (* below is more efficient *) -fun Finite_Set_card_interpreter thy model args t = +fun Finite_Set_card_interpreter ctxt model args t = case t of Const (@{const_name Finite_Set.card}, Type ("fun", [Type ("fun", [T, @{typ bool}]), @{typ nat}])) => @@ -2647,7 +2577,7 @@ | number_of_elements (Leaf _) = raise REFUTE ("Finite_Set_card_interpreter", "interpretation for set type is a leaf") - val size_of_nat = size_of_type thy model (@{typ nat}) + val size_of_nat = size_of_type ctxt model (@{typ nat}) (* takes an interpretation for a set and returns an interpretation *) (* for a 'nat' denoting the set's cardinality *) (* interpretation -> interpretation *) @@ -2662,20 +2592,17 @@ Leaf (replicate size_of_nat False) end val set_constants = - make_constants thy model (Type ("fun", [T, HOLogic.boolT])) + make_constants ctxt model (Type ("fun", [T, HOLogic.boolT])) in SOME (Node (map card set_constants), model, args) end | _ => NONE; -(* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) - (* only an optimization: 'finite' could in principle be interpreted with *) (* interpreters available already (using its definition), but the code *) (* below is more efficient *) -fun Finite_Set_finite_interpreter thy model args t = +fun Finite_Set_finite_interpreter ctxt model args t = case t of Const (@{const_name Finite_Set.finite}, Type ("fun", [Type ("fun", [T, @{typ bool}]), @@ -2688,7 +2615,7 @@ @{typ bool}])) => let val size_of_set = - size_of_type thy model (Type ("fun", [T, HOLogic.boolT])) + size_of_type ctxt model (Type ("fun", [T, HOLogic.boolT])) in (* we only consider finite models anyway, hence EVERY set is *) (* "finite" *) @@ -2696,19 +2623,16 @@ end | _ => NONE; -(* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) - (* only an optimization: 'less' could in principle be interpreted with *) (* interpreters available already (using its definition), but the code *) (* below is more efficient *) -fun Nat_less_interpreter thy model args t = +fun Nat_less_interpreter ctxt model args t = case t of Const (@{const_name Orderings.less}, Type ("fun", [@{typ nat}, Type ("fun", [@{typ nat}, @{typ bool}])])) => let - val size_of_nat = size_of_type thy model (@{typ nat}) + val size_of_nat = size_of_type ctxt model (@{typ nat}) (* the 'n'-th nat is not less than the first 'n' nats, while it *) (* is less than the remaining 'size_of_nat - n' nats *) (* int -> interpretation *) @@ -2718,19 +2642,16 @@ end | _ => NONE; -(* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) - (* only an optimization: 'plus' could in principle be interpreted with *) (* interpreters available already (using its definition), but the code *) (* below is more efficient *) -fun Nat_plus_interpreter thy model args t = +fun Nat_plus_interpreter ctxt model args t = case t of Const (@{const_name Groups.plus}, Type ("fun", [@{typ nat}, Type ("fun", [@{typ nat}, @{typ nat}])])) => let - val size_of_nat = size_of_type thy model (@{typ nat}) + val size_of_nat = size_of_type ctxt model (@{typ nat}) (* int -> int -> interpretation *) fun plus m n = let @@ -2748,19 +2669,16 @@ end | _ => NONE; -(* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) - (* only an optimization: 'minus' could in principle be interpreted *) (* with interpreters available already (using its definition), but the *) (* code below is more efficient *) -fun Nat_minus_interpreter thy model args t = +fun Nat_minus_interpreter ctxt model args t = case t of Const (@{const_name Groups.minus}, Type ("fun", [@{typ nat}, Type ("fun", [@{typ nat}, @{typ nat}])])) => let - val size_of_nat = size_of_type thy model (@{typ nat}) + val size_of_nat = size_of_type ctxt model (@{typ nat}) (* int -> int -> interpretation *) fun minus m n = let @@ -2775,19 +2693,16 @@ end | _ => NONE; -(* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) - (* only an optimization: 'times' could in principle be interpreted *) (* with interpreters available already (using its definition), but the *) (* code below is more efficient *) -fun Nat_times_interpreter thy model args t = +fun Nat_times_interpreter ctxt model args t = case t of Const (@{const_name Groups.times}, Type ("fun", [@{typ nat}, Type ("fun", [@{typ nat}, @{typ nat}])])) => let - val size_of_nat = size_of_type thy model (@{typ nat}) + val size_of_nat = size_of_type ctxt model (@{typ nat}) (* nat -> nat -> interpretation *) fun mult m n = let @@ -2805,20 +2720,17 @@ end | _ => NONE; -(* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) - (* only an optimization: 'append' could in principle be interpreted with *) (* interpreters available already (using its definition), but the code *) (* below is more efficient *) -fun List_append_interpreter thy model args t = +fun List_append_interpreter ctxt model args t = case t of Const (@{const_name List.append}, Type ("fun", [Type ("List.list", [T]), Type ("fun", [Type ("List.list", [_]), Type ("List.list", [_])])])) => let - val size_elem = size_of_type thy model T - val size_list = size_of_type thy model (Type ("List.list", [T])) + val size_elem = size_of_type ctxt model T + val size_list = size_of_type ctxt model (Type ("List.list", [T])) (* maximal length of lists; 0 if we only consider the empty list *) val list_length = let @@ -2901,28 +2813,25 @@ (* UNSOUND -(* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) - (* only an optimization: 'lfp' could in principle be interpreted with *) (* interpreters available already (using its definition), but the code *) (* below is more efficient *) -fun lfp_interpreter thy model args t = +fun lfp_interpreter ctxt model args t = case t of Const (@{const_name lfp}, Type ("fun", [Type ("fun", [Type ("fun", [T, @{typ bool}]), Type ("fun", [_, @{typ bool}])]), Type ("fun", [_, @{typ bool}])])) => let - val size_elem = size_of_type thy model T + val size_elem = size_of_type ctxt model T (* the universe (i.e. the set that contains every element) *) val i_univ = Node (replicate size_elem TT) (* all sets with elements from type 'T' *) val i_sets = - make_constants thy model (Type ("fun", [T, HOLogic.boolT])) + make_constants ctxt model (Type ("fun", [T, HOLogic.boolT])) (* all functions that map sets to sets *) - val i_funs = make_constants thy model (Type ("fun", + val i_funs = make_constants ctxt model (Type ("fun", [Type ("fun", [T, @{typ bool}]), Type ("fun", [T, @{typ bool}])])) (* "lfp(f) == Inter({u. f(u) <= u})" *) @@ -2954,28 +2863,25 @@ end | _ => NONE; -(* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) - (* only an optimization: 'gfp' could in principle be interpreted with *) (* interpreters available already (using its definition), but the code *) (* below is more efficient *) -fun gfp_interpreter thy model args t = +fun gfp_interpreter ctxt model args t = case t of Const (@{const_name gfp}, Type ("fun", [Type ("fun", [Type ("fun", [T, @{typ bool}]), Type ("fun", [_, @{typ bool}])]), Type ("fun", [_, @{typ bool}])])) => let - val size_elem = size_of_type thy model T + val size_elem = size_of_type ctxt model T (* the universe (i.e. the set that contains every element) *) val i_univ = Node (replicate size_elem TT) (* all sets with elements from type 'T' *) val i_sets = - make_constants thy model (Type ("fun", [T, HOLogic.boolT])) + make_constants ctxt model (Type ("fun", [T, HOLogic.boolT])) (* all functions that map sets to sets *) - val i_funs = make_constants thy model (Type ("fun", + val i_funs = make_constants ctxt model (Type ("fun", [Type ("fun", [T, HOLogic.boolT]), Type ("fun", [T, HOLogic.boolT])])) (* "gfp(f) == Union({u. u <= f(u)})" *) @@ -3009,37 +2915,31 @@ | _ => NONE; *) -(* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) - (* only an optimization: 'fst' could in principle be interpreted with *) (* interpreters available already (using its definition), but the code *) (* below is more efficient *) -fun Product_Type_fst_interpreter thy model args t = +fun Product_Type_fst_interpreter ctxt model args t = case t of Const (@{const_name fst}, Type ("fun", [Type (@{type_name Product_Type.prod}, [T, U]), _])) => let - val constants_T = make_constants thy model T - val size_U = size_of_type thy model U + val constants_T = make_constants ctxt model T + val size_U = size_of_type ctxt model U in SOME (Node (maps (replicate size_U) constants_T), model, args) end | _ => NONE; -(* theory -> model -> arguments -> Term.term -> - (interpretation * model * arguments) option *) - (* only an optimization: 'snd' could in principle be interpreted with *) (* interpreters available already (using its definition), but the code *) (* below is more efficient *) -fun Product_Type_snd_interpreter thy model args t = +fun Product_Type_snd_interpreter ctxt model args t = case t of Const (@{const_name snd}, Type ("fun", [Type (@{type_name Product_Type.prod}, [T, U]), _])) => let - val size_T = size_of_type thy model T - val constants_U = make_constants thy model U + val size_T = size_of_type ctxt model T + val constants_U = make_constants ctxt model U in SOME (Node (flat (replicate size_T constants_U)), model, args) end @@ -3050,10 +2950,7 @@ (* PRINTERS *) (* ------------------------------------------------------------------------- *) -(* theory -> model -> Term.typ -> interpretation -> (int -> bool) -> - Term.term option *) - -fun stlc_printer thy model T intr assignment = +fun stlc_printer ctxt model T intr assignment = let (* string -> string *) fun strip_leading_quote s = @@ -3075,7 +2972,7 @@ Type ("fun", [T1, T2]) => let (* create all constants of type 'T1' *) - val constants = make_constants thy model T1 + val constants = make_constants ctxt model T1 (* interpretation list *) val results = (case intr of @@ -3085,8 +2982,8 @@ (* Term.term list *) val pairs = map (fn (arg, result) => HOLogic.mk_prod - (print thy model T1 arg assignment, - print thy model T2 result assignment)) + (print ctxt model T1 arg assignment, + print ctxt model T2 result assignment)) (constants ~~ results) (* Term.typ *) val HOLogic_prodT = HOLogic.mk_prodT (T1, T2) @@ -3125,100 +3022,101 @@ string_of_int (index_from_interpretation intr), T)) end; -(* theory -> model -> Term.typ -> interpretation -> (int -> bool) -> - Term.term option *) - -fun IDT_printer thy model T intr assignment = - (case T of - Type (s, Ts) => - (case Datatype.get_info thy s of - SOME info => (* inductive datatype *) - let - val (typs, _) = model - val index = #index info - val descr = #descr info - val (_, dtyps, constrs) = the (AList.lookup (op =) descr index) - val typ_assoc = dtyps ~~ Ts - (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) - val _ = - if Library.exists (fn d => - case d of Datatype_Aux.DtTFree _ => false | _ => true) dtyps - then - raise REFUTE ("IDT_printer", "datatype argument (for type " ^ - Syntax.string_of_typ_global thy (Type (s, Ts)) ^ ") is not a variable") - else () - (* the index of the element in the datatype *) - val element = - (case intr of - Leaf xs => find_index (PropLogic.eval assignment) xs - | Node _ => raise REFUTE ("IDT_printer", - "interpretation is not a leaf")) - in - if element < 0 then - SOME (Const (@{const_name undefined}, Type (s, Ts))) - else - let - (* takes a datatype constructor, and if for some arguments this *) - (* constructor generates the datatype's element that is given by *) - (* 'element', returns the constructor (as a term) as well as the *) - (* indices of the arguments *) - fun get_constr_args (cname, cargs) = - let - val cTerm = Const (cname, - map (typ_of_dtyp descr typ_assoc) cargs ---> Type (s, Ts)) - val (iC, _, _) = interpret thy (typs, []) {maxvars=0, - def_eq=false, next_idx=1, bounds=[], wellformed=True} cTerm - (* interpretation -> int list option *) - fun get_args (Leaf xs) = - if find_index (fn x => x = True) xs = element then - SOME [] - else - NONE - | get_args (Node xs) = - let - (* interpretation * int -> int list option *) - fun search ([], _) = +fun IDT_printer ctxt model T intr assignment = + let + val thy = ProofContext.theory_of ctxt + in + (case T of + Type (s, Ts) => + (case Datatype.get_info thy s of + SOME info => (* inductive datatype *) + let + val (typs, _) = model + val index = #index info + val descr = #descr info + val (_, dtyps, constrs) = the (AList.lookup (op =) descr index) + val typ_assoc = dtyps ~~ Ts + (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) + val _ = + if Library.exists (fn d => + case d of Datatype_Aux.DtTFree _ => false | _ => true) dtyps + then + raise REFUTE ("IDT_printer", "datatype argument (for type " ^ + Syntax.string_of_typ ctxt (Type (s, Ts)) ^ ") is not a variable") + else () + (* the index of the element in the datatype *) + val element = + (case intr of + Leaf xs => find_index (PropLogic.eval assignment) xs + | Node _ => raise REFUTE ("IDT_printer", + "interpretation is not a leaf")) + in + if element < 0 then + SOME (Const (@{const_name undefined}, Type (s, Ts))) + else + let + (* takes a datatype constructor, and if for some arguments this *) + (* constructor generates the datatype's element that is given by *) + (* 'element', returns the constructor (as a term) as well as the *) + (* indices of the arguments *) + fun get_constr_args (cname, cargs) = + let + val cTerm = Const (cname, + map (typ_of_dtyp descr typ_assoc) cargs ---> Type (s, Ts)) + val (iC, _, _) = interpret ctxt (typs, []) {maxvars=0, + def_eq=false, next_idx=1, bounds=[], wellformed=True} cTerm + (* interpretation -> int list option *) + fun get_args (Leaf xs) = + if find_index (fn x => x = True) xs = element then + SOME [] + else NONE - | search (x::xs, n) = - (case get_args x of - SOME result => SOME (n::result) - | NONE => search (xs, n+1)) - in - search (xs, 0) - end - in - Option.map (fn args => (cTerm, cargs, args)) (get_args iC) - end - val (cTerm, cargs, args) = - (* we could speed things up by computing the correct *) - (* constructor directly (rather than testing all *) - (* constructors), based on the order in which constructors *) - (* generate elements of datatypes; the current implementation *) - (* of 'IDT_printer' however is independent of the internals *) - (* of 'IDT_constructor_interpreter' *) - (case get_first get_constr_args constrs of - SOME x => x - | NONE => raise REFUTE ("IDT_printer", - "no matching constructor found for element " ^ - string_of_int element)) - val argsTerms = map (fn (d, n) => - let - val dT = typ_of_dtyp descr typ_assoc d - (* we only need the n-th element of this list, so there *) - (* might be a more efficient implementation that does not *) - (* generate all constants *) - val consts = make_constants thy (typs, []) dT - in - print thy (typs, []) dT (List.nth (consts, n)) assignment - end) (cargs ~~ args) - in - SOME (list_comb (cTerm, argsTerms)) - end - end - | NONE => (* not an inductive datatype *) - NONE) - | _ => (* a (free or schematic) type variable *) - NONE); + | get_args (Node xs) = + let + (* interpretation * int -> int list option *) + fun search ([], _) = + NONE + | search (x::xs, n) = + (case get_args x of + SOME result => SOME (n::result) + | NONE => search (xs, n+1)) + in + search (xs, 0) + end + in + Option.map (fn args => (cTerm, cargs, args)) (get_args iC) + end + val (cTerm, cargs, args) = + (* we could speed things up by computing the correct *) + (* constructor directly (rather than testing all *) + (* constructors), based on the order in which constructors *) + (* generate elements of datatypes; the current implementation *) + (* of 'IDT_printer' however is independent of the internals *) + (* of 'IDT_constructor_interpreter' *) + (case get_first get_constr_args constrs of + SOME x => x + | NONE => raise REFUTE ("IDT_printer", + "no matching constructor found for element " ^ + string_of_int element)) + val argsTerms = map (fn (d, n) => + let + val dT = typ_of_dtyp descr typ_assoc d + (* we only need the n-th element of this list, so there *) + (* might be a more efficient implementation that does not *) + (* generate all constants *) + val consts = make_constants ctxt (typs, []) dT + in + print ctxt (typs, []) dT (List.nth (consts, n)) assignment + end) (cargs ~~ args) + in + SOME (list_comb (cTerm, argsTerms)) + end + end + | NONE => (* not an inductive datatype *) + NONE) + | _ => (* a (free or schematic) type variable *) + NONE) + end; (* ------------------------------------------------------------------------- *) @@ -3293,7 +3191,7 @@ let val thy' = fold set_default_param parms thy; val output = - (case get_default_params thy' of + (case get_default_params (ProofContext.init_global thy') of [] => "none" | new_defaults => cat_lines (map (fn (x, y) => x ^ "=" ^ y) new_defaults)); val _ = writeln ("Default parameters for 'refute':\n" ^ output);