haftmann@24219: (* Title: Pure/Isar/code.ML haftmann@24219: Author: Florian Haftmann, TU Muenchen haftmann@24219: haftmann@34173: Abstract executable ingredients of theory. Management of data haftmann@34173: dependent on executable ingredients as synchronized cache; purged haftmann@34173: on any change of underlying executable ingredients. haftmann@24219: *) haftmann@24219: haftmann@24219: signature CODE = haftmann@24219: sig haftmann@31957: (*constants*) haftmann@31957: val check_const: theory -> term -> string haftmann@31957: val read_bare_const: theory -> string -> string * typ haftmann@31957: val read_const: theory -> string -> string haftmann@31962: val string_of_const: theory -> string -> string haftmann@33940: val const_typ: theory -> string -> typ haftmann@31962: val args_number: theory -> string -> int haftmann@31957: haftmann@31156: (*constructor sets*) haftmann@31156: val constrset_of_consts: theory -> (string * typ) list haftmann@40726: -> string * ((string * sort) list * (string * ((string * sort) list * typ list)) list) haftmann@31156: haftmann@34874: (*code equations and certificates*) haftmann@31962: val mk_eqn: theory -> thm * bool -> thm * bool haftmann@31962: val mk_eqn_warning: theory -> thm -> (thm * bool) option haftmann@31962: val mk_eqn_liberal: theory -> thm -> (thm * bool) option haftmann@31156: val assert_eqn: theory -> thm * bool -> thm * bool haftmann@31957: val const_typ_eqn: theory -> thm -> string * typ haftmann@34895: val expand_eta: theory -> int -> thm -> thm haftmann@34895: type cert haftmann@34891: val empty_cert: theory -> string -> cert haftmann@34891: val cert_of_eqns: theory -> string -> (thm * bool) list -> cert haftmann@34874: val constrain_cert: theory -> sort list -> cert -> cert haftmann@49971: val conclude_cert: cert -> cert haftmann@35226: val typargs_deps_of_cert: theory -> cert -> (string * sort) list * (string * typ list) list haftmann@36209: val equations_of_cert: theory -> cert -> ((string * sort) list * typ) haftmann@36209: * (((term * string option) list * (term * string option)) * (thm option * bool)) list haftmann@35226: val bare_thms_of_cert: theory -> cert -> thm list haftmann@34895: val pretty_cert: theory -> cert -> Pretty.T list haftmann@31156: haftmann@31962: (*executable code*) haftmann@31156: val add_datatype: (string * typ) list -> theory -> theory haftmann@31156: val add_datatype_cmd: string list -> theory -> theory haftmann@35299: val datatype_interpretation: haftmann@40726: (string * ((string * sort) list * (string * ((string * sort) list * typ list)) list) haftmann@35299: -> theory -> theory) -> theory -> theory haftmann@36112: val add_abstype: thm -> theory -> theory haftmann@35299: val abstype_interpretation: haftmann@40726: (string * ((string * sort) list * ((string * ((string * sort) list * typ)) * (string * thm))) haftmann@31156: -> theory -> theory) -> theory -> theory haftmann@28368: val add_eqn: thm -> theory -> theory haftmann@31088: val add_nbe_eqn: thm -> theory -> theory haftmann@46513: val add_abs_eqn: thm -> theory -> theory haftmann@28368: val add_default_eqn: thm -> theory -> theory haftmann@28703: val add_default_eqn_attribute: attribute haftmann@28703: val add_default_eqn_attrib: Attrib.src haftmann@37425: val add_nbe_default_eqn: thm -> theory -> theory haftmann@37425: val add_nbe_default_eqn_attribute: attribute haftmann@37425: val add_nbe_default_eqn_attrib: Attrib.src haftmann@28368: val del_eqn: thm -> theory -> theory haftmann@28368: val del_eqns: string -> theory -> theory haftmann@24844: val add_case: thm -> theory -> theory haftmann@24844: val add_undefined: string -> theory -> theory haftmann@40726: val get_type: theory -> string haftmann@40726: -> ((string * sort) list * (string * ((string * sort) list * typ list)) list) * bool haftmann@35299: val get_type_of_constr_or_abstr: theory -> string -> (string * bool) option haftmann@35226: val is_constr: theory -> string -> bool haftmann@35226: val is_abstr: theory -> string -> bool haftmann@48075: val get_cert: theory -> { functrans: ((thm * bool) list -> (thm * bool) list option) list, haftmann@48075: ss: simpset } -> string -> cert Andreas@47437: val get_case_scheme: theory -> string -> (int * (int * string option list)) option haftmann@37438: val get_case_cong: theory -> string -> thm option haftmann@31890: val undefineds: theory -> string list haftmann@24219: val print_codesetup: theory -> unit haftmann@24219: end; haftmann@24219: haftmann@24219: signature CODE_DATA_ARGS = haftmann@24219: sig haftmann@24219: type T haftmann@24219: val empty: T haftmann@24219: end; haftmann@24219: haftmann@24219: signature CODE_DATA = haftmann@24219: sig haftmann@24219: type T haftmann@39397: val change: theory option -> (T -> T) -> T haftmann@39397: val change_yield: theory option -> (T -> 'a * T) -> 'a * T haftmann@24219: end; haftmann@24219: haftmann@24219: signature PRIVATE_CODE = haftmann@24219: sig haftmann@24219: include CODE wenzelm@51368: val declare_data: Any.T -> serial wenzelm@51368: val change_yield_data: serial * ('a -> Any.T) * (Any.T -> 'a) haftmann@34251: -> theory -> ('a -> 'b * 'a) -> 'b * 'a haftmann@24219: end; haftmann@24219: haftmann@24219: structure Code : PRIVATE_CODE = haftmann@24219: struct haftmann@24219: haftmann@31962: (** auxiliary **) haftmann@31962: haftmann@31962: (* printing *) haftmann@31156: wenzelm@39134: fun string_of_typ thy = wenzelm@39134: Syntax.string_of_typ (Config.put show_sorts true (Syntax.init_pretty_global thy)); haftmann@31962: wenzelm@42359: fun string_of_const thy c = wenzelm@42360: let val ctxt = Proof_Context.init_global thy in wenzelm@42359: case AxClass.inst_of_param thy c of wenzelm@42359: SOME (c, tyco) => wenzelm@42360: Proof_Context.extern_const ctxt c ^ " " ^ enclose "[" "]" wenzelm@42360: (Proof_Context.extern_type ctxt tyco) wenzelm@42360: | NONE => Proof_Context.extern_const ctxt c wenzelm@42359: end; haftmann@31156: haftmann@31962: haftmann@31962: (* constants *) haftmann@31156: haftmann@49534: fun const_typ thy = Type.strip_sorts o Sign.the_const_type thy; haftmann@49534: haftmann@49534: fun args_number thy = length o binder_types o const_typ thy; haftmann@49534: haftmann@49534: fun devarify ty = haftmann@49534: let haftmann@49534: val tys = fold_atyps (fn TVar vi_sort => AList.update (op =) vi_sort) ty []; haftmann@49534: val vs = Name.invent Name.context Name.aT (length tys); haftmann@49534: val mapping = map2 (fn v => fn (vi, sort) => (vi, TFree (v, sort))) vs tys; haftmann@49534: in Term.typ_subst_TVars mapping ty end; haftmann@49534: haftmann@49534: fun typscheme thy (c, ty) = haftmann@49534: (map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty); haftmann@49534: haftmann@49534: fun typscheme_equiv (ty1, ty2) = haftmann@49534: Type.raw_instance (devarify ty1, ty2) andalso Type.raw_instance (devarify ty2, ty1); haftmann@49534: haftmann@31962: fun check_bare_const thy t = case try dest_Const t haftmann@31962: of SOME c_ty => c_ty haftmann@31962: | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t); haftmann@31156: haftmann@40362: fun check_unoverload thy (c, ty) = haftmann@40362: let haftmann@40362: val c' = AxClass.unoverload_const thy (c, ty); haftmann@40362: val ty_decl = Sign.the_const_type thy c'; wenzelm@45344: in haftmann@49534: if typscheme_equiv (ty_decl, Logic.varifyT_global ty) wenzelm@45344: then c' wenzelm@45344: else wenzelm@45344: error ("Type\n" ^ string_of_typ thy ty ^ wenzelm@45344: "\nof constant " ^ quote c ^ wenzelm@45344: "\nis too specific compared to declared type\n" ^ wenzelm@45344: string_of_typ thy ty_decl) haftmann@40362: end; haftmann@40362: haftmann@40362: fun check_const thy = check_unoverload thy o check_bare_const thy; haftmann@31962: haftmann@31962: fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy; haftmann@31962: haftmann@40362: fun read_const thy = check_unoverload thy o read_bare_const thy; haftmann@31156: haftmann@32872: haftmann@31962: (** data store **) haftmann@31962: haftmann@35226: (* datatypes *) haftmann@35226: haftmann@43634: datatype typ_spec = Constructors of (string * ((string * sort) list * typ list)) list * haftmann@43634: string list (*references to associated case constructors*) haftmann@40726: | Abstractor of (string * ((string * sort) list * typ)) * (string * thm); haftmann@31962: haftmann@43634: fun constructors_of (Constructors (cos, _)) = (cos, false) haftmann@40726: | constructors_of (Abstractor ((co, (vs, ty)), _)) = ([(co, (vs, [ty]))], true); haftmann@35226: haftmann@43638: fun case_consts_of (Constructors (_, case_consts)) = case_consts haftmann@43638: | case_consts_of (Abstractor _) = []; haftmann@35226: haftmann@35226: (* functions *) haftmann@31962: haftmann@37460: datatype fun_spec = Default of (thm * bool) list * (thm * bool) list lazy haftmann@43634: (* (cache for default equations, lazy computation of default equations) haftmann@43634: -- helps to restore natural order of default equations *) haftmann@35226: | Eqns of (thm * bool) list haftmann@35226: | Proj of term * string haftmann@35226: | Abstr of thm * string; haftmann@31962: haftmann@37460: val empty_fun_spec = Default ([], Lazy.value []); haftmann@31962: haftmann@35226: fun is_default (Default _) = true haftmann@35226: | is_default _ = false; haftmann@35226: haftmann@35226: fun associated_abstype (Abstr (_, tyco)) = SOME tyco haftmann@35226: | associated_abstype _ = NONE; haftmann@31962: haftmann@31962: haftmann@31962: (* executable code data *) haftmann@31962: haftmann@31962: datatype spec = Spec of { haftmann@31962: history_concluded: bool, haftmann@35226: functions: ((bool * fun_spec) * (serial * fun_spec) list) Symtab.table haftmann@31962: (*with explicit history*), haftmann@35299: types: ((serial * ((string * sort) list * typ_spec)) list) Symtab.table haftmann@31962: (*with explicit history*), Andreas@47437: cases: ((int * (int * string option list)) * thm) Symtab.table * unit Symtab.table haftmann@31962: }; haftmann@31962: haftmann@45987: fun make_spec (history_concluded, (functions, (types, cases))) = haftmann@45987: Spec { history_concluded = history_concluded, functions = functions, types = types, cases = cases }; haftmann@45987: fun map_spec f (Spec { history_concluded = history_concluded, haftmann@35299: functions = functions, types = types, cases = cases }) = haftmann@45987: make_spec (f (history_concluded, (functions, (types, cases)))); haftmann@45987: fun merge_spec (Spec { history_concluded = _, functions = functions1, haftmann@35299: types = types1, cases = (cases1, undefs1) }, haftmann@45987: Spec { history_concluded = _, functions = functions2, haftmann@35299: types = types2, cases = (cases2, undefs2) }) = haftmann@31156: let bulwahn@42707: val types = Symtab.join (K (AList.merge (op =) (K true))) (types1, types2); haftmann@43639: val case_consts_of' = (maps case_consts_of o map (snd o snd o hd o snd) o Symtab.dest); haftmann@35226: fun merge_functions ((_, history1), (_, history2)) = haftmann@31962: let haftmann@31962: val raw_history = AList.merge (op = : serial * serial -> bool) haftmann@35226: (K true) (history1, history2); haftmann@35226: val filtered_history = filter_out (is_default o snd) raw_history; haftmann@31962: val history = if null filtered_history haftmann@31962: then raw_history else filtered_history; haftmann@31962: in ((false, (snd o hd) history), history) end; haftmann@43638: val all_datatype_specs = map (snd o snd o hd o snd) (Symtab.dest types); haftmann@43638: val all_constructors = maps (map fst o fst o constructors_of) all_datatype_specs; haftmann@43639: val invalidated_case_consts = union (op =) (case_consts_of' types1) (case_consts_of' types2) haftmann@43639: |> subtract (op =) (maps case_consts_of all_datatype_specs) bulwahn@42707: val functions = Symtab.join (K merge_functions) (functions1, functions2) bulwahn@42707: |> fold (fn c => Symtab.map_entry c (apfst (K (true, empty_fun_spec)))) all_constructors; haftmann@43638: val cases = (Symtab.merge (K true) (cases1, cases2) haftmann@43639: |> fold Symtab.delete invalidated_case_consts, Symtab.merge (K true) (undefs1, undefs2)); haftmann@45987: in make_spec (false, (functions, (types, cases))) end; haftmann@31962: haftmann@31962: fun history_concluded (Spec { history_concluded, ... }) = history_concluded; haftmann@35226: fun the_functions (Spec { functions, ... }) = functions; haftmann@35299: fun the_types (Spec { types, ... }) = types; haftmann@31962: fun the_cases (Spec { cases, ... }) = cases; haftmann@32544: val map_history_concluded = map_spec o apfst; haftmann@45987: val map_functions = map_spec o apsnd o apfst; haftmann@35226: val map_typs = map_spec o apsnd o apsnd o apfst; haftmann@31962: val map_cases = map_spec o apsnd o apsnd o apsnd; haftmann@31962: haftmann@31962: haftmann@31962: (* data slots dependent on executable code *) haftmann@31962: haftmann@31962: (*private copy avoids potential conflict of table exceptions*) wenzelm@31971: structure Datatab = Table(type key = int val ord = int_ord); haftmann@31962: haftmann@31962: local haftmann@31962: wenzelm@51368: type kind = { empty: Any.T }; haftmann@31962: wenzelm@43684: val kinds = Synchronized.var "Code_Data" (Datatab.empty: kind Datatab.table); haftmann@31962: wenzelm@43684: fun invoke f k = wenzelm@43684: (case Datatab.lookup (Synchronized.value kinds) k of wenzelm@43684: SOME kind => f kind wenzelm@43684: | NONE => raise Fail "Invalid code data identifier"); haftmann@31962: haftmann@31962: in haftmann@31962: haftmann@34173: fun declare_data empty = haftmann@31962: let haftmann@31962: val k = serial (); haftmann@34173: val kind = { empty = empty }; wenzelm@43684: val _ = Synchronized.change kinds (Datatab.update (k, kind)); haftmann@31962: in k end; haftmann@31962: haftmann@31962: fun invoke_init k = invoke (fn kind => #empty kind) k; haftmann@31962: haftmann@31962: end; (*local*) haftmann@31962: haftmann@31962: haftmann@31962: (* theory store *) haftmann@31962: haftmann@31962: local haftmann@31962: wenzelm@51368: type data = Any.T Datatab.table; haftmann@34244: fun empty_dataref () = Synchronized.var "code data" (NONE : (data * theory_ref) option); haftmann@31962: haftmann@34244: structure Code_Data = Theory_Data haftmann@31962: ( haftmann@34244: type T = spec * (data * theory_ref) option Synchronized.var; haftmann@45987: val empty = (make_spec (false, (Symtab.empty, haftmann@34244: (Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_dataref ()); haftmann@49556: val extend : T -> T = apsnd (K (empty_dataref ())); haftmann@34244: fun merge ((spec1, _), (spec2, _)) = haftmann@34244: (merge_spec (spec1, spec2), empty_dataref ()); haftmann@31962: ); haftmann@31962: haftmann@31962: in haftmann@31962: haftmann@35226: haftmann@31962: (* access to executable code *) haftmann@31962: haftmann@49535: val the_exec : theory -> spec = fst o Code_Data.get; haftmann@31962: haftmann@34244: fun map_exec_purge f = Code_Data.map (fn (exec, _) => (f exec, empty_dataref ())); haftmann@31962: haftmann@35226: fun change_fun_spec delete c f = (map_exec_purge o map_functions haftmann@35226: o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, empty_fun_spec), []))) haftmann@35226: o apfst) (fn (_, spec) => (true, f spec)); haftmann@31962: haftmann@31962: haftmann@31962: (* tackling equation history *) haftmann@31962: haftmann@31962: fun continue_history thy = if (history_concluded o the_exec) thy haftmann@31962: then thy haftmann@31962: |> (Code_Data.map o apfst o map_history_concluded) (K false) haftmann@31962: |> SOME haftmann@31962: else NONE; haftmann@31962: haftmann@31962: fun conclude_history thy = if (history_concluded o the_exec) thy haftmann@31962: then NONE haftmann@31962: else thy haftmann@31962: |> (Code_Data.map o apfst) haftmann@39020: ((map_functions o Symtab.map) (fn _ => fn ((changed, current), history) => haftmann@31962: ((false, current), haftmann@31962: if changed then (serial (), current) :: history else history)) haftmann@31962: #> map_history_concluded (K true)) haftmann@31962: |> SOME; haftmann@31962: haftmann@34244: val _ = Context.>> (Context.map_theory (Theory.at_begin continue_history #> Theory.at_end conclude_history)); haftmann@31962: haftmann@31962: haftmann@31962: (* access to data dependent on abstract executable code *) haftmann@31962: haftmann@34244: fun change_yield_data (kind, mk, dest) theory f = haftmann@31962: let haftmann@34244: val dataref = (snd o Code_Data.get) theory; haftmann@34251: val (datatab, thy_ref) = case Synchronized.value dataref haftmann@34251: of SOME (datatab, thy_ref) => if Theory.eq_thy (theory, Theory.deref thy_ref) haftmann@34251: then (datatab, thy_ref) haftmann@34251: else (Datatab.empty, Theory.check_thy theory) haftmann@34251: | NONE => (Datatab.empty, Theory.check_thy theory) haftmann@34244: val data = case Datatab.lookup datatab kind haftmann@34244: of SOME data => data haftmann@34244: | NONE => invoke_init kind; haftmann@40758: val result as (_, data') = f (dest data); haftmann@34244: val _ = Synchronized.change dataref haftmann@34244: ((K o SOME) (Datatab.update (kind, mk data') datatab, thy_ref)); haftmann@34244: in result end; haftmann@31962: haftmann@31962: end; (*local*) haftmann@31962: haftmann@31962: haftmann@31962: (** foundation **) haftmann@31962: haftmann@31962: (* datatypes *) haftmann@31156: haftmann@35226: fun no_constr thy s (c, ty) = error ("Not a datatype constructor:\n" ^ string_of_const thy c haftmann@35226: ^ " :: " ^ string_of_typ thy ty ^ "\n" ^ enclose "(" ")" s); haftmann@35226: haftmann@45987: fun analyze_constructor thy (c, ty) = haftmann@31156: let haftmann@45987: val _ = Thm.cterm_of thy (Const (c, ty)); wenzelm@45344: val ty_decl = Logic.unvarifyT_global (const_typ thy c); haftmann@31156: fun last_typ c_ty ty = haftmann@31156: let haftmann@33531: val tfrees = Term.add_tfreesT ty []; wenzelm@40844: val (tyco, vs) = (apsnd o map) dest_TFree (dest_Type (body_type ty)) haftmann@35226: handle TYPE _ => no_constr thy "bad type" c_ty haftmann@36112: val _ = if tyco = "fun" then no_constr thy "bad type" c_ty else (); wenzelm@45344: val _ = wenzelm@45344: if has_duplicates (eq_fst (op =)) vs haftmann@35226: then no_constr thy "duplicate type variables in datatype" c_ty else (); wenzelm@45344: val _ = wenzelm@45344: if length tfrees <> length vs haftmann@35226: then no_constr thy "type variables missing in datatype" c_ty else (); haftmann@31156: in (tyco, vs) end; haftmann@35226: val (tyco, _) = last_typ (c, ty) ty_decl; haftmann@35226: val (_, vs) = last_typ (c, ty) ty; haftmann@35226: in ((tyco, map snd vs), (c, (map fst vs, ty))) end; haftmann@35226: haftmann@49904: fun constrset_of_consts thy consts = haftmann@35226: let haftmann@35226: val _ = map (fn (c, _) => if (is_some o AxClass.class_of_param thy) c haftmann@49904: then error ("Is a class parameter: " ^ string_of_const thy c) else ()) consts; haftmann@49904: val raw_constructors = map (analyze_constructor thy) consts; haftmann@49904: val tyco = case distinct (op =) (map (fst o fst) raw_constructors) haftmann@49904: of [tyco] => tyco haftmann@49904: | [] => error "Empty constructor set" haftmann@49904: | tycos => error ("Different type constructors in constructor set: " ^ commas_quote tycos) haftmann@49904: val vs = Name.invent Name.context Name.aT (Sign.arity_number thy tyco); haftmann@31156: fun inst vs' (c, (vs, ty)) = haftmann@31156: let haftmann@31156: val the_v = the o AList.lookup (op =) (vs ~~ vs'); haftmann@49904: val ty' = map_type_tfree (fn (v, _) => TFree (the_v v, [])) ty; haftmann@49904: val (vs'', ty'') = typscheme thy (c, ty'); haftmann@49904: in (c, (vs'', binder_types ty'')) end; haftmann@49904: val constructors = map (inst vs o snd) raw_constructors; haftmann@49904: in (tyco, (map (rpair []) vs, constructors)) end; haftmann@31156: haftmann@35299: fun get_type_entry thy tyco = case these (Symtab.lookup ((the_types o the_exec) thy) tyco) haftmann@35226: of (_, entry) :: _ => SOME entry haftmann@35226: | _ => NONE; haftmann@31962: haftmann@40726: fun get_type thy tyco = case get_type_entry thy tyco haftmann@35226: of SOME (vs, spec) => apfst (pair vs) (constructors_of spec) haftmann@45987: | NONE => Sign.arity_number thy tyco wenzelm@43329: |> Name.invent Name.context Name.aT haftmann@35226: |> map (rpair []) haftmann@35226: |> rpair [] haftmann@35226: |> rpair false; haftmann@35226: haftmann@35299: fun get_abstype_spec thy tyco = case get_type_entry thy tyco haftmann@35226: of SOME (vs, Abstractor spec) => (vs, spec) haftmann@36122: | _ => error ("Not an abstract type: " ^ tyco); haftmann@35226: haftmann@35299: fun get_type_of_constr_or_abstr thy c = wenzelm@40844: case (body_type o const_typ thy) c haftmann@40758: of Type (tyco, _) => let val ((_, cos), abstract) = get_type thy tyco haftmann@35226: in if member (op =) (map fst cos) c then SOME (tyco, abstract) else NONE end haftmann@31962: | _ => NONE; haftmann@31962: haftmann@35299: fun is_constr thy c = case get_type_of_constr_or_abstr thy c haftmann@35226: of SOME (_, false) => true haftmann@35226: | _ => false; haftmann@35226: haftmann@35299: fun is_abstr thy c = case get_type_of_constr_or_abstr thy c haftmann@35226: of SOME (_, true) => true haftmann@35226: | _ => false; haftmann@31962: haftmann@31156: haftmann@34874: (* bare code equations *) haftmann@31156: haftmann@35226: (* convention for variables: haftmann@35226: ?x ?'a for free-floating theorems (e.g. in the data store) haftmann@35226: ?x 'a for certificates haftmann@35226: x 'a for final representation of equations haftmann@35226: *) haftmann@35226: haftmann@31156: exception BAD_THM of string; haftmann@31156: fun bad_thm msg = raise BAD_THM msg; haftmann@49760: fun error_thm f thy (thm, proper) = f (thm, proper) haftmann@49760: handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Display.string_of_thm_global thy thm); haftmann@49760: fun error_abs_thm f thy thm = f thm haftmann@49760: handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Display.string_of_thm_global thy thm); haftmann@49760: fun warning_thm f thy (thm, proper) = SOME (f (thm, proper)) haftmann@49760: handle BAD_THM msg => (warning (msg ^ ", in theorem:\n" ^ Display.string_of_thm_global thy thm); NONE) haftmann@49760: fun try_thm f thm_proper = SOME (f thm_proper) haftmann@49760: handle BAD_THM _ => NONE; haftmann@31156: haftmann@31156: fun is_linear thm = haftmann@31156: let val (_, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm haftmann@31156: in not (has_duplicates (op =) ((fold o fold_aterms) haftmann@31156: (fn Var (v, _) => cons v | _ => I) args [])) end; haftmann@31156: haftmann@36209: fun check_decl_ty thy (c, ty) = haftmann@36209: let haftmann@36209: val ty_decl = Sign.the_const_type thy c; haftmann@49534: in if typscheme_equiv (ty_decl, ty) then () haftmann@36209: else bad_thm ("Type\n" ^ string_of_typ thy ty haftmann@36209: ^ "\nof constant " ^ quote c haftmann@40362: ^ "\nis too specific compared to declared type\n" haftmann@36209: ^ string_of_typ thy ty_decl) haftmann@36209: end; haftmann@36209: haftmann@35226: fun check_eqn thy { allow_nonlinear, allow_consts, allow_pats } thm (lhs, rhs) = haftmann@31156: let haftmann@31156: fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v haftmann@49760: | Free _ => bad_thm "Illegal free variable" haftmann@31156: | _ => I) t []; haftmann@31156: fun tvars_of t = fold_term_types (fn _ => haftmann@31156: fold_atyps (fn TVar (v, _) => insert (op =) v haftmann@49760: | TFree _ => bad_thm "Illegal free type variable")) t []; haftmann@31156: val lhs_vs = vars_of lhs; haftmann@31156: val rhs_vs = vars_of rhs; haftmann@31156: val lhs_tvs = tvars_of lhs; haftmann@31156: val rhs_tvs = tvars_of rhs; haftmann@31156: val _ = if null (subtract (op =) lhs_vs rhs_vs) haftmann@31156: then () haftmann@49760: else bad_thm "Free variables on right hand side of equation"; haftmann@31156: val _ = if null (subtract (op =) lhs_tvs rhs_tvs) haftmann@31156: then () haftmann@49760: else bad_thm "Free type variables on right hand side of equation"; haftmann@34894: val (head, args) = strip_comb lhs; haftmann@31156: val (c, ty) = case head haftmann@31156: of Const (c_ty as (_, ty)) => (AxClass.unoverload_const thy c_ty, ty) haftmann@49760: | _ => bad_thm "Equation not headed by constant"; haftmann@49760: fun check _ (Abs _) = bad_thm "Abstraction on left hand side of equation" haftmann@31156: | check 0 (Var _) = () haftmann@49760: | check _ (Var _) = bad_thm "Variable with application on left hand side of equation" haftmann@31156: | check n (t1 $ t2) = (check (n+1) t1; check 0 t2) haftmann@34894: | check n (Const (c_ty as (c, ty))) = haftmann@35226: if allow_pats then let haftmann@33940: val c' = AxClass.unoverload_const thy c_ty haftmann@45987: in if n = (length o binder_types) ty haftmann@35226: then if allow_consts orelse is_constr thy c' haftmann@33940: then () haftmann@49760: else bad_thm (quote c ^ " is not a constructor, on left hand side of equation") haftmann@49760: else bad_thm ("Partially applied constant " ^ quote c ^ " on left hand side of equation") haftmann@49760: end else bad_thm ("Pattern not allowed here, but constant " ^ quote c ^ " encountered on left hand side of equation") haftmann@31156: val _ = map (check 0) args; haftmann@35226: val _ = if allow_nonlinear orelse is_linear thm then () haftmann@49760: else bad_thm "Duplicate variables on left hand side of equation"; haftmann@34894: val _ = if (is_none o AxClass.class_of_param thy) c then () haftmann@49760: else bad_thm "Overloaded constant as head in equation"; haftmann@34894: val _ = if not (is_constr thy c) then () haftmann@49760: else bad_thm "Constructor as head in equation"; haftmann@35226: val _ = if not (is_abstr thy c) then () haftmann@49760: else bad_thm "Abstractor as head in equation"; haftmann@36209: val _ = check_decl_ty thy (c, ty); haftmann@35226: in () end; haftmann@35226: haftmann@35226: fun gen_assert_eqn thy check_patterns (thm, proper) = haftmann@35226: let haftmann@35226: val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm haftmann@49760: handle TERM _ => bad_thm "Not an equation" haftmann@49760: | THM _ => bad_thm "Not a proper equation"; haftmann@35226: val _ = check_eqn thy { allow_nonlinear = not proper, haftmann@35226: allow_consts = not (proper andalso check_patterns), allow_pats = true } thm (lhs, rhs); haftmann@31156: in (thm, proper) end; haftmann@31156: haftmann@35226: fun assert_abs_eqn thy some_tyco thm = haftmann@35226: let haftmann@35226: val (full_lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm haftmann@49760: handle TERM _ => bad_thm "Not an equation" haftmann@49760: | THM _ => bad_thm "Not a proper equation"; haftmann@35226: val (rep, lhs) = dest_comb full_lhs haftmann@49760: handle TERM _ => bad_thm "Not an abstract equation"; haftmann@46513: val (rep_const, ty) = dest_Const rep haftmann@49760: handle TERM _ => bad_thm "Not an abstract equation"; haftmann@40187: val (tyco, Ts) = (dest_Type o domain_type) ty haftmann@49760: handle TERM _ => bad_thm "Not an abstract equation" haftmann@49760: | TYPE _ => bad_thm "Not an abstract equation"; haftmann@35226: val _ = case some_tyco of SOME tyco' => if tyco = tyco' then () haftmann@49760: else bad_thm ("Abstract type mismatch:" ^ quote tyco ^ " vs. " ^ quote tyco') haftmann@35226: | NONE => (); haftmann@36202: val (vs', (_, (rep', _))) = get_abstype_spec thy tyco; haftmann@35226: val _ = if rep_const = rep' then () haftmann@49760: else bad_thm ("Projection mismatch: " ^ quote rep_const ^ " vs. " ^ quote rep'); haftmann@35226: val _ = check_eqn thy { allow_nonlinear = false, haftmann@35226: allow_consts = false, allow_pats = false } thm (lhs, rhs); haftmann@40564: val _ = if forall2 (fn T => fn (_, sort) => Sign.of_sort thy (T, sort)) Ts vs' then () haftmann@40187: else error ("Type arguments do not satisfy sort constraints of abstype certificate."); haftmann@35226: in (thm, tyco) end; haftmann@35226: haftmann@49760: fun assert_eqn thy = error_thm (gen_assert_eqn thy true) thy; haftmann@31962: wenzelm@42360: fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (Proof_Context.init_global thy); haftmann@31156: haftmann@49760: fun mk_eqn thy = error_thm (gen_assert_eqn thy false) thy o haftmann@31962: apfst (meta_rewrite thy); haftmann@31962: haftmann@31962: fun mk_eqn_warning thy = Option.map (fn (thm, _) => (thm, is_linear thm)) haftmann@49760: o warning_thm (gen_assert_eqn thy false) thy o rpair false o meta_rewrite thy; haftmann@31962: haftmann@31962: fun mk_eqn_liberal thy = Option.map (fn (thm, _) => (thm, is_linear thm)) haftmann@34894: o try_thm (gen_assert_eqn thy false) o rpair false o meta_rewrite thy; haftmann@31156: haftmann@49760: fun mk_abs_eqn thy = error_abs_thm (assert_abs_eqn thy NONE) thy o meta_rewrite thy; haftmann@35226: haftmann@33940: val head_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of; haftmann@31156: haftmann@31957: fun const_typ_eqn thy thm = haftmann@31156: let haftmann@32640: val (c, ty) = head_eqn thm; haftmann@31156: val c' = AxClass.unoverload_const thy (c, ty); haftmann@33940: (*permissive wrt. to overloaded constants!*) haftmann@31156: in (c', ty) end; haftmann@33940: haftmann@31957: fun const_eqn thy = fst o const_typ_eqn thy; haftmann@31156: haftmann@35226: fun const_abs_eqn thy = AxClass.unoverload_const thy o dest_Const o fst o strip_comb o snd haftmann@35226: o dest_comb o fst o Logic.dest_equals o Thm.plain_prop_of; haftmann@35226: haftmann@35226: fun mk_proj tyco vs ty abs rep = haftmann@35226: let haftmann@35226: val ty_abs = Type (tyco, map TFree vs); haftmann@35226: val xarg = Var (("x", 0), ty); haftmann@35226: in Logic.mk_equals (Const (rep, ty_abs --> ty) $ (Const (abs, ty --> ty_abs) $ xarg), xarg) end; haftmann@35226: haftmann@34895: haftmann@34895: (* technical transformations of code equations *) haftmann@34895: haftmann@34895: fun expand_eta thy k thm = haftmann@34895: let haftmann@34895: val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm; haftmann@34895: val (_, args) = strip_comb lhs; haftmann@34895: val l = if k = ~1 haftmann@34895: then (length o fst o strip_abs) rhs haftmann@34895: else Int.max (0, k - length args); haftmann@34895: val (raw_vars, _) = Term.strip_abs_eta l rhs; haftmann@34895: val vars = burrow_fst (Name.variant_list (map (fst o fst) (Term.add_vars lhs []))) haftmann@34895: raw_vars; haftmann@34895: fun expand (v, ty) thm = Drule.fun_cong_rule thm haftmann@34895: (Thm.cterm_of thy (Var ((v, 0), ty))); haftmann@34895: in haftmann@34895: thm haftmann@34895: |> fold expand vars haftmann@34895: |> Conv.fconv_rule Drule.beta_eta_conversion haftmann@34895: end; haftmann@34895: haftmann@34895: fun same_arity thy thms = haftmann@31962: let haftmann@34895: val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals; haftmann@34895: val k = fold (Integer.max o num_args_of o Thm.prop_of) thms 0; haftmann@34895: in map (expand_eta thy k) thms end; haftmann@34895: haftmann@34895: fun mk_desymbolization pre post mk vs = haftmann@34895: let haftmann@34895: val names = map (pre o fst o fst) vs haftmann@34895: |> map (Name.desymbolize false) haftmann@34895: |> Name.variant_list [] haftmann@34895: |> map post; haftmann@34895: in map_filter (fn (((v, i), x), v') => haftmann@34895: if v = v' andalso i = 0 then NONE haftmann@34895: else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names) haftmann@34895: end; haftmann@34895: haftmann@40758: fun desymbolize_tvars thms = haftmann@34895: let haftmann@34895: val tvs = fold (Term.add_tvars o Thm.prop_of) thms []; haftmann@34895: val tvar_subst = mk_desymbolization (unprefix "'") (prefix "'") TVar tvs; haftmann@34895: in map (Thm.certify_instantiate (tvar_subst, [])) thms end; haftmann@34895: haftmann@40758: fun desymbolize_vars thm = haftmann@34895: let haftmann@34895: val vs = Term.add_vars (Thm.prop_of thm) []; haftmann@34895: val var_subst = mk_desymbolization I I Var vs; haftmann@34895: in Thm.certify_instantiate ([], var_subst) thm end; haftmann@34895: haftmann@40758: fun canonize_thms thy = desymbolize_tvars #> same_arity thy #> map desymbolize_vars; haftmann@31156: haftmann@34874: haftmann@36112: (* abstype certificates *) haftmann@36112: haftmann@36112: fun check_abstype_cert thy proto_thm = haftmann@36112: let haftmann@36209: val thm = (AxClass.unoverload thy o meta_rewrite thy) proto_thm; haftmann@36112: val (lhs, rhs) = Logic.dest_equals (Thm.plain_prop_of thm) haftmann@49760: handle TERM _ => bad_thm "Not an equation" haftmann@49760: | THM _ => bad_thm "Not a proper equation"; haftmann@36209: val ((abs, raw_ty), ((rep, rep_ty), param)) = (apsnd (apfst dest_Const o dest_comb) haftmann@36112: o apfst dest_Const o dest_comb) lhs haftmann@49760: handle TERM _ => bad_thm "Not an abstype certificate"; haftmann@36209: val _ = pairself (fn c => if (is_some o AxClass.class_of_param thy) c haftmann@36209: then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep); haftmann@36209: val _ = check_decl_ty thy (abs, raw_ty); haftmann@36209: val _ = check_decl_ty thy (rep, rep_ty); haftmann@48068: val _ = if length (binder_types raw_ty) = 1 haftmann@48068: then () haftmann@49760: else bad_thm "Bad type for abstract constructor"; haftmann@40758: val _ = (fst o dest_Var) param haftmann@49760: handle TERM _ => bad_thm "Not an abstype certificate"; haftmann@49760: val _ = if param = rhs then () else bad_thm "Not an abstype certificate"; wenzelm@45344: val ((tyco, sorts), (abs, (vs, ty'))) = wenzelm@45344: analyze_constructor thy (abs, Logic.unvarifyT_global raw_ty); haftmann@36112: val ty = domain_type ty'; haftmann@49534: val (vs', _) = typscheme thy (abs, ty'); haftmann@40726: in (tyco, (vs ~~ sorts, ((abs, (vs', ty)), (rep, thm)))) end; haftmann@36112: haftmann@36112: haftmann@34874: (* code equation certificates *) haftmann@34874: haftmann@34895: fun build_head thy (c, ty) = haftmann@34895: Thm.cterm_of thy (Logic.mk_equals (Free ("HEAD", ty), Const (c, ty))); haftmann@34874: haftmann@34895: fun get_head thy cert_thm = haftmann@34895: let haftmann@34895: val [head] = (#hyps o Thm.crep_thm) cert_thm; haftmann@34895: val (_, Const (c, ty)) = (Logic.dest_equals o Thm.term_of) head; haftmann@34895: in (typscheme thy (c, ty), head) end; haftmann@34895: haftmann@35226: fun typscheme_projection thy = haftmann@35226: typscheme thy o dest_Const o fst o dest_comb o fst o Logic.dest_equals; haftmann@35226: haftmann@35226: fun typscheme_abs thy = haftmann@35226: typscheme thy o dest_Const o fst o strip_comb o snd o dest_comb o fst o Logic.dest_equals o Thm.prop_of; haftmann@35226: haftmann@35226: fun constrain_thm thy vs sorts thm = haftmann@35226: let haftmann@35226: val mapping = map2 (fn (v, sort) => fn sort' => haftmann@35226: (v, Sorts.inter_sort (Sign.classes_of thy) (sort, sort'))) vs sorts; haftmann@35226: val inst = map2 (fn (v, sort) => fn (_, sort') => haftmann@35226: (((v, 0), sort), TFree (v, sort'))) vs mapping; haftmann@40803: val subst = (map_types o map_type_tfree) haftmann@40803: (fn (v, _) => TFree (v, the (AList.lookup (op =) mapping v))); haftmann@35226: in haftmann@35226: thm wenzelm@35845: |> Thm.varifyT_global haftmann@35226: |> Thm.certify_instantiate (inst, []) haftmann@35226: |> pair subst haftmann@35226: end; haftmann@35226: haftmann@35226: fun concretify_abs thy tyco abs_thm = haftmann@35226: let haftmann@40758: val (_, ((c, _), (_, cert))) = get_abstype_spec thy tyco; haftmann@35226: val lhs = (fst o Logic.dest_equals o Thm.prop_of) abs_thm haftmann@35226: val ty = fastype_of lhs; haftmann@35226: val ty_abs = (fastype_of o snd o dest_comb) lhs; haftmann@35226: val abs = Thm.cterm_of thy (Const (c, ty --> ty_abs)); haftmann@35226: val raw_concrete_thm = Drule.transitive_thm OF [Thm.symmetric cert, Thm.combination (Thm.reflexive abs) abs_thm]; wenzelm@35845: in (c, (Thm.varifyT_global o zero_var_indexes) raw_concrete_thm) end; haftmann@35226: haftmann@35226: fun add_rhss_of_eqn thy t = haftmann@35226: let haftmann@45987: val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals) t; haftmann@35226: fun add_const (Const (c, ty)) = insert (op =) (c, Sign.const_typargs thy (c, ty)) haftmann@35226: | add_const _ = I haftmann@39568: val add_consts = fold_aterms add_const haftmann@39568: in add_consts rhs o fold add_consts args end; haftmann@35226: haftmann@46513: val dest_eqn = apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify_global; haftmann@35226: haftmann@35226: abstype cert = Equations of thm * bool list haftmann@35226: | Projection of term * string haftmann@35226: | Abstract of thm * string haftmann@35226: with haftmann@34891: haftmann@34891: fun empty_cert thy c = haftmann@34891: let haftmann@40761: val raw_ty = Logic.unvarifyT_global (const_typ thy c); haftmann@49534: val (vs, _) = typscheme thy (c, raw_ty); haftmann@40761: val sortargs = case AxClass.class_of_param thy c haftmann@40761: of SOME class => [[class]] haftmann@40761: | NONE => (case get_type_of_constr_or_abstr thy c haftmann@40761: of SOME (tyco, _) => (map snd o fst o the) haftmann@40761: (AList.lookup (op =) ((snd o fst o get_type thy) tyco) c) haftmann@40761: | NONE => replicate (length vs) []); haftmann@40761: val the_sort = the o AList.lookup (op =) (map fst vs ~~ sortargs); haftmann@40761: val ty = map_type_tfree (fn (v, _) => TFree (v, the_sort v)) raw_ty haftmann@34895: val chead = build_head thy (c, ty); haftmann@35226: in Equations (Thm.weaken chead Drule.dummy_thm, []) end; haftmann@34891: haftmann@34891: fun cert_of_eqns thy c [] = empty_cert thy c haftmann@34895: | cert_of_eqns thy c raw_eqns = haftmann@34874: let haftmann@34895: val eqns = burrow_fst (canonize_thms thy) raw_eqns; haftmann@34895: val _ = map (assert_eqn thy) eqns; haftmann@34891: val (thms, propers) = split_list eqns; haftmann@34895: val _ = map (fn thm => if c = const_eqn thy thm then () haftmann@34895: else error ("Wrong head of code equation,\nexpected constant " haftmann@34895: ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy thm)) thms; haftmann@34891: fun tvars_of T = rev (Term.add_tvarsT T []); haftmann@34891: val vss = map (tvars_of o snd o head_eqn) thms; haftmann@34891: fun inter_sorts vs = haftmann@34891: fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs []; haftmann@34891: val sorts = map_transpose inter_sorts vss; wenzelm@43329: val vts = Name.invent_names Name.context Name.aT sorts; haftmann@40758: val thms' = haftmann@34891: map2 (fn vs => Thm.certify_instantiate (vs ~~ map TFree vts, [])) vss thms; haftmann@40758: val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms')))); haftmann@34874: fun head_conv ct = if can Thm.dest_comb ct haftmann@34874: then Conv.fun_conv head_conv ct haftmann@34874: else Conv.rewr_conv head_thm ct; haftmann@34874: val rewrite_head = Conv.fconv_rule (Conv.arg1_conv head_conv); haftmann@40758: val cert_thm = Conjunction.intr_balanced (map rewrite_head thms'); haftmann@35226: in Equations (cert_thm, propers) end; haftmann@34891: haftmann@35226: fun cert_of_proj thy c tyco = haftmann@35226: let haftmann@40758: val (vs, ((abs, (_, ty)), (rep, _))) = get_abstype_spec thy tyco; haftmann@35226: val _ = if c = rep then () else haftmann@35226: error ("Wrong head of projection,\nexpected constant " ^ string_of_const thy rep); haftmann@35226: in Projection (mk_proj tyco vs ty abs rep, tyco) end; haftmann@35226: haftmann@35226: fun cert_of_abs thy tyco c raw_abs_thm = haftmann@34874: let haftmann@35226: val abs_thm = singleton (canonize_thms thy) raw_abs_thm; haftmann@35226: val _ = assert_abs_eqn thy (SOME tyco) abs_thm; haftmann@35226: val _ = if c = const_abs_eqn thy abs_thm then () haftmann@35226: else error ("Wrong head of abstract code equation,\nexpected constant " haftmann@35226: ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy abs_thm); wenzelm@36615: in Abstract (Thm.legacy_freezeT abs_thm, tyco) end; haftmann@34874: haftmann@35226: fun constrain_cert thy sorts (Equations (cert_thm, propers)) = haftmann@35226: let haftmann@35226: val ((vs, _), head) = get_head thy cert_thm; haftmann@35226: val (subst, cert_thm') = cert_thm haftmann@35226: |> Thm.implies_intr head haftmann@35226: |> constrain_thm thy vs sorts; haftmann@35226: val head' = Thm.term_of head haftmann@35226: |> subst haftmann@35226: |> Thm.cterm_of thy; haftmann@35226: val cert_thm'' = cert_thm' haftmann@35226: |> Thm.elim_implies (Thm.assume head'); haftmann@35226: in Equations (cert_thm'', propers) end haftmann@35226: | constrain_cert thy _ (cert as Projection _) = haftmann@35226: cert haftmann@35226: | constrain_cert thy sorts (Abstract (abs_thm, tyco)) = haftmann@35226: Abstract (snd (constrain_thm thy (fst (typscheme_abs thy abs_thm)) sorts abs_thm), tyco); haftmann@35226: haftmann@49971: fun conclude_cert (Equations (cert_thm, propers)) = haftmann@49971: (Equations (Thm.close_derivation cert_thm, propers)) haftmann@49971: | conclude_cert (cert as Projection _) = haftmann@49971: cert haftmann@49971: | conclude_cert (Abstract (abs_thm, tyco)) = haftmann@49971: (Abstract (Thm.close_derivation abs_thm, tyco)); haftmann@49971: haftmann@35226: fun typscheme_of_cert thy (Equations (cert_thm, _)) = haftmann@35226: fst (get_head thy cert_thm) haftmann@35226: | typscheme_of_cert thy (Projection (proj, _)) = haftmann@35226: typscheme_projection thy proj haftmann@35226: | typscheme_of_cert thy (Abstract (abs_thm, _)) = haftmann@35226: typscheme_abs thy abs_thm; haftmann@34874: haftmann@35226: fun typargs_deps_of_cert thy (Equations (cert_thm, propers)) = haftmann@35226: let haftmann@35226: val vs = (fst o fst) (get_head thy cert_thm); haftmann@35226: val equations = if null propers then [] else haftmann@35226: Thm.prop_of cert_thm haftmann@35226: |> Logic.dest_conjunction_balanced (length propers); haftmann@35226: in (vs, fold (add_rhss_of_eqn thy) equations []) end haftmann@40758: | typargs_deps_of_cert thy (Projection (t, _)) = haftmann@35226: (fst (typscheme_projection thy t), add_rhss_of_eqn thy t []) haftmann@35226: | typargs_deps_of_cert thy (Abstract (abs_thm, tyco)) = haftmann@35226: let haftmann@35226: val vs = fst (typscheme_abs thy abs_thm); haftmann@35226: val (_, concrete_thm) = concretify_abs thy tyco abs_thm; wenzelm@45344: in (vs, add_rhss_of_eqn thy (Logic.unvarify_types_global (Thm.prop_of concrete_thm)) []) end; haftmann@34895: haftmann@35226: fun equations_of_cert thy (cert as Equations (cert_thm, propers)) = haftmann@35226: let haftmann@35226: val tyscm = typscheme_of_cert thy cert; haftmann@35226: val thms = if null propers then [] else haftmann@35226: cert_thm wenzelm@35624: |> Local_Defs.expand [snd (get_head thy cert_thm)] wenzelm@35845: |> Thm.varifyT_global haftmann@35226: |> Conjunction.elim_balanced (length propers); haftmann@36209: fun abstractions (args, rhs) = (map (rpair NONE) args, (rhs, NONE)); haftmann@46513: in (tyscm, map (abstractions o dest_eqn o Thm.prop_of) thms ~~ (map SOME thms ~~ propers)) end haftmann@35226: | equations_of_cert thy (Projection (t, tyco)) = haftmann@35226: let haftmann@35226: val (_, ((abs, _), _)) = get_abstype_spec thy tyco; haftmann@35226: val tyscm = typscheme_projection thy t; wenzelm@45344: val t' = Logic.varify_types_global t; haftmann@36209: fun abstractions (args, rhs) = (map (rpair (SOME abs)) args, (rhs, NONE)); haftmann@46513: in (tyscm, [((abstractions o dest_eqn) t', (NONE, true))]) end haftmann@35226: | equations_of_cert thy (Abstract (abs_thm, tyco)) = haftmann@35226: let haftmann@35226: val tyscm = typscheme_abs thy abs_thm; haftmann@35226: val (abs, concrete_thm) = concretify_abs thy tyco abs_thm; haftmann@36209: fun abstractions (args, rhs) = (map (rpair NONE) args, (rhs, (SOME abs))); wenzelm@35845: in haftmann@46513: (tyscm, [((abstractions o dest_eqn o Thm.prop_of) concrete_thm, haftmann@36209: (SOME (Thm.varifyT_global abs_thm), true))]) wenzelm@35845: end; haftmann@34895: haftmann@35226: fun pretty_cert thy (cert as Equations _) = haftmann@35226: (map_filter (Option.map (Display.pretty_thm_global thy o AxClass.overload thy) o fst o snd) haftmann@35226: o snd o equations_of_cert thy) cert haftmann@35226: | pretty_cert thy (Projection (t, _)) = wenzelm@45344: [Syntax.pretty_term_global thy (Logic.varify_types_global t)] haftmann@40758: | pretty_cert thy (Abstract (abs_thm, _)) = wenzelm@35845: [(Display.pretty_thm_global thy o AxClass.overload thy o Thm.varifyT_global) abs_thm]; haftmann@35226: haftmann@35226: fun bare_thms_of_cert thy (cert as Equations _) = haftmann@35226: (map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE) haftmann@35226: o snd o equations_of_cert thy) cert haftmann@35376: | bare_thms_of_cert thy (Projection _) = [] haftmann@35376: | bare_thms_of_cert thy (Abstract (abs_thm, tyco)) = wenzelm@35845: [Thm.varifyT_global (snd (concretify_abs thy tyco abs_thm))]; haftmann@34895: haftmann@34895: end; haftmann@34891: haftmann@34874: haftmann@35226: (* code certificate access *) haftmann@35226: haftmann@35226: fun retrieve_raw thy c = haftmann@35226: Symtab.lookup ((the_functions o the_exec) thy) c haftmann@35226: |> Option.map (snd o fst) haftmann@37460: |> the_default empty_fun_spec haftmann@34874: haftmann@48075: fun eqn_conv conv ct = haftmann@48075: let haftmann@48075: fun lhs_conv ct = if can Thm.dest_comb ct haftmann@48075: then Conv.combination_conv lhs_conv conv ct haftmann@48075: else Conv.all_conv ct; haftmann@48075: in Conv.combination_conv (Conv.arg_conv lhs_conv) conv ct end; haftmann@48075: haftmann@48075: fun rewrite_eqn thy conv ss = haftmann@48075: let haftmann@48075: val ctxt = Proof_Context.init_global thy; haftmann@48075: val rewrite = Conv.fconv_rule (conv (Simplifier.rewrite ss)); haftmann@48075: in singleton (Variable.trade (K (map rewrite)) ctxt) end; haftmann@48075: haftmann@48075: fun cert_of_eqns_preprocess thy functrans ss c = haftmann@48075: (map o apfst) (Thm.transfer thy) haftmann@48075: #> perhaps (perhaps_loop (perhaps_apply functrans)) haftmann@48075: #> (map o apfst) (rewrite_eqn thy eqn_conv ss) haftmann@48075: #> (map o apfst) (AxClass.unoverload thy) haftmann@48075: #> cert_of_eqns thy c; haftmann@48075: haftmann@48075: fun get_cert thy { functrans, ss } c = haftmann@48075: case retrieve_raw thy c haftmann@48075: of Default (_, eqns_lazy) => Lazy.force eqns_lazy haftmann@48075: |> cert_of_eqns_preprocess thy functrans ss c haftmann@48075: | Eqns eqns => eqns haftmann@48075: |> cert_of_eqns_preprocess thy functrans ss c haftmann@48075: | Proj (_, tyco) => haftmann@48075: cert_of_proj thy c tyco haftmann@48075: | Abstr (abs_thm, tyco) => abs_thm haftmann@48075: |> Thm.transfer thy haftmann@48075: |> rewrite_eqn thy Conv.arg_conv ss haftmann@48075: |> AxClass.unoverload thy haftmann@48075: |> cert_of_abs thy tyco c; haftmann@31962: haftmann@31962: haftmann@31962: (* cases *) haftmann@31156: haftmann@31156: fun case_certificate thm = haftmann@31156: let haftmann@31156: val ((head, raw_case_expr), cases) = (apfst Logic.dest_equals haftmann@32640: o apsnd Logic.dest_conjunctions o Logic.dest_implies o Thm.plain_prop_of) thm; haftmann@31156: val _ = case head of Free _ => true haftmann@31156: | Var _ => true haftmann@31156: | _ => raise TERM ("case_cert", []); haftmann@31156: val ([(case_var, _)], case_expr) = Term.strip_abs_eta 1 raw_case_expr; haftmann@31156: val (Const (case_const, _), raw_params) = strip_comb case_expr; haftmann@31156: val n = find_index (fn Free (v, _) => v = case_var | _ => false) raw_params; haftmann@31156: val _ = if n = ~1 then raise TERM ("case_cert", []) else (); haftmann@31156: val params = map (fst o dest_Var) (nth_drop n raw_params); haftmann@31156: fun dest_case t = haftmann@31156: let haftmann@31156: val (head' $ t_co, rhs) = Logic.dest_equals t; haftmann@31156: val _ = if head' = head then () else raise TERM ("case_cert", []); haftmann@31156: val (Const (co, _), args) = strip_comb t_co; haftmann@31156: val (Var (param, _), args') = strip_comb rhs; haftmann@31156: val _ = if args' = args then () else raise TERM ("case_cert", []); haftmann@31156: in (param, co) end; haftmann@31156: fun analyze_cases cases = haftmann@31156: let haftmann@31156: val co_list = fold (AList.update (op =) o dest_case) cases []; Andreas@47437: in map (AList.lookup (op =) co_list) params end; haftmann@31156: fun analyze_let t = haftmann@31156: let haftmann@31156: val (head' $ arg, Var (param', _) $ arg') = Logic.dest_equals t; haftmann@31156: val _ = if head' = head then () else raise TERM ("case_cert", []); haftmann@31156: val _ = if arg' = arg then () else raise TERM ("case_cert", []); haftmann@31156: val _ = if [param'] = params then () else raise TERM ("case_cert", []); haftmann@31156: in [] end; haftmann@31156: fun analyze (cases as [let_case]) = haftmann@31156: (analyze_cases cases handle Bind => analyze_let let_case) haftmann@31156: | analyze cases = analyze_cases cases; haftmann@31156: in (case_const, (n, analyze cases)) end; haftmann@31156: haftmann@31156: fun case_cert thm = case_certificate thm haftmann@31156: handle Bind => error "bad case certificate" haftmann@31156: | TERM _ => error "bad case certificate"; haftmann@31156: haftmann@37438: fun get_case_scheme thy = Option.map fst o Symtab.lookup ((fst o the_cases o the_exec) thy); haftmann@37438: fun get_case_cong thy = Option.map snd o Symtab.lookup ((fst o the_cases o the_exec) thy); haftmann@24219: haftmann@31962: val undefineds = Symtab.keys o snd o the_cases o the_exec; haftmann@24219: haftmann@24219: haftmann@31962: (* diagnostic *) haftmann@24219: haftmann@24219: fun print_codesetup thy = haftmann@24219: let wenzelm@42360: val ctxt = Proof_Context.init_global thy; haftmann@24844: val exec = the_exec thy; haftmann@35226: fun pretty_equations const thms = haftmann@24219: (Pretty.block o Pretty.fbreaks) ( wenzelm@51580: Pretty.str (string_of_const thy const) :: wenzelm@51580: map (Pretty.item o single o Display.pretty_thm ctxt) thms haftmann@24219: ); wenzelm@51580: fun pretty_function (const, Default (_, eqns_lazy)) = wenzelm@51580: pretty_equations const (map fst (Lazy.force eqns_lazy)) haftmann@35226: | pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns) haftmann@35226: | pretty_function (const, Proj (proj, _)) = Pretty.block haftmann@35226: [Pretty.str (string_of_const thy const), Pretty.fbrk, Syntax.pretty_term ctxt proj] haftmann@35226: | pretty_function (const, Abstr (thm, _)) = pretty_equations const [thm]; haftmann@35226: fun pretty_typ (tyco, vs) = Pretty.str haftmann@35226: (string_of_typ thy (Type (tyco, map TFree vs))); haftmann@35226: fun pretty_typspec (typ, (cos, abstract)) = if null cos haftmann@35226: then pretty_typ typ haftmann@35226: else (Pretty.block o Pretty.breaks) ( haftmann@35226: pretty_typ typ haftmann@35226: :: Pretty.str "=" haftmann@35226: :: (if abstract then [Pretty.str "(abstract)"] else []) haftmann@40726: @ separate (Pretty.str "|") (map (fn (c, (_, [])) => Pretty.str (string_of_const thy c) haftmann@40726: | (c, (_, tys)) => haftmann@35226: (Pretty.block o Pretty.breaks) haftmann@35226: (Pretty.str (string_of_const thy c) haftmann@35226: :: Pretty.str "of" haftmann@35226: :: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos) haftmann@35226: ); haftmann@47555: fun pretty_caseparam NONE = "" haftmann@47555: | pretty_caseparam (SOME c) = string_of_const thy c haftmann@37438: fun pretty_case (const, ((_, (_, [])), _)) = Pretty.str (string_of_const thy const) haftmann@37438: | pretty_case (const, ((_, (_, cos)), _)) = (Pretty.block o Pretty.breaks) [ haftmann@34901: Pretty.str (string_of_const thy const), Pretty.str "with", haftmann@47555: (Pretty.block o Pretty.commas o map (Pretty.str o pretty_caseparam)) cos]; haftmann@35226: val functions = the_functions exec haftmann@24423: |> Symtab.dest haftmann@28695: |> (map o apsnd) (snd o fst) haftmann@24219: |> sort (string_ord o pairself fst); haftmann@35299: val datatypes = the_types exec haftmann@24219: |> Symtab.dest haftmann@35226: |> map (fn (tyco, (_, (vs, spec)) :: _) => haftmann@35226: ((tyco, vs), constructors_of spec)) haftmann@35226: |> sort (string_ord o pairself (fst o fst)); haftmann@34901: val cases = Symtab.dest ((fst o the_cases o the_exec) thy); haftmann@34901: val undefineds = Symtab.keys ((snd o the_cases o the_exec) thy); haftmann@24219: in haftmann@24219: (Pretty.writeln o Pretty.chunks) [ haftmann@24219: Pretty.block ( haftmann@34901: Pretty.str "code equations:" :: Pretty.fbrk haftmann@35226: :: (Pretty.fbreaks o map pretty_function) functions haftmann@24219: ), haftmann@25968: Pretty.block ( haftmann@34901: Pretty.str "datatypes:" :: Pretty.fbrk haftmann@35226: :: (Pretty.fbreaks o map pretty_typspec) datatypes haftmann@34901: ), haftmann@34901: Pretty.block ( haftmann@34901: Pretty.str "cases:" :: Pretty.fbrk haftmann@34901: :: (Pretty.fbreaks o map pretty_case) cases haftmann@34901: ), haftmann@34901: Pretty.block ( haftmann@34901: Pretty.str "undefined:" :: Pretty.fbrk haftmann@34901: :: (Pretty.commas o map (Pretty.str o string_of_const thy)) undefineds haftmann@24219: ) haftmann@24219: ] haftmann@24219: end; haftmann@24219: haftmann@24219: haftmann@31962: (** declaring executable ingredients **) haftmann@31962: haftmann@31962: (* code equations *) haftmann@31962: haftmann@35226: fun gen_add_eqn default (raw_thm, proper) thy = haftmann@33075: let haftmann@35226: val thm = Thm.close_derivation raw_thm; haftmann@35226: val c = const_eqn thy thm; haftmann@37460: fun update_subsume thy (thm, proper) eqns = haftmann@37460: let wenzelm@48902: val args_of = snd o take_prefix is_Var o rev o snd o strip_comb haftmann@39791: o map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of; haftmann@37460: val args = args_of thm; haftmann@37460: val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1); haftmann@39794: fun matches_args args' = haftmann@39794: let haftmann@39794: val k = length args' - length args haftmann@39794: in if k >= 0 haftmann@39794: then Pattern.matchess thy (args, (map incr_idx o drop k) args') haftmann@39794: else false haftmann@39794: end; haftmann@37460: fun drop (thm', proper') = if (proper orelse not proper') haftmann@37460: andalso matches_args (args_of thm') then haftmann@37460: (warning ("Code generator: dropping subsumed code equation\n" ^ haftmann@37460: Display.string_of_thm_global thy thm'); true) haftmann@37460: else false; haftmann@37460: in (thm, proper) :: filter_out drop eqns end; haftmann@37460: fun natural_order thy_ref eqns = haftmann@37460: (eqns, Lazy.lazy (fn () => fold (update_subsume (Theory.deref thy_ref)) eqns [])) haftmann@37460: fun add_eqn' true (Default (eqns, _)) = haftmann@37460: Default (natural_order (Theory.check_thy thy) ((thm, proper) :: eqns)) haftmann@37460: (*this restores the natural order and drops syntactic redundancies*) haftmann@39794: | add_eqn' true fun_spec = fun_spec haftmann@39794: | add_eqn' false (Eqns eqns) = Eqns (update_subsume thy (thm, proper) eqns) haftmann@35226: | add_eqn' false _ = Eqns [(thm, proper)]; haftmann@35226: in change_fun_spec false c (add_eqn' default) thy end; haftmann@31962: haftmann@31962: fun add_eqn thm thy = haftmann@31962: gen_add_eqn false (mk_eqn thy (thm, true)) thy; haftmann@31962: haftmann@31962: fun add_warning_eqn thm thy = haftmann@31962: case mk_eqn_warning thy thm haftmann@31962: of SOME eqn => gen_add_eqn false eqn thy haftmann@31962: | NONE => thy; haftmann@31962: haftmann@37425: fun add_nbe_eqn thm thy = haftmann@37425: gen_add_eqn false (mk_eqn thy (thm, false)) thy; haftmann@37425: haftmann@31962: fun add_default_eqn thm thy = haftmann@31962: case mk_eqn_liberal thy thm haftmann@31962: of SOME eqn => gen_add_eqn true eqn thy haftmann@31962: | NONE => thy; haftmann@31962: haftmann@31962: val add_default_eqn_attribute = Thm.declaration_attribute haftmann@31962: (fn thm => Context.mapping (add_default_eqn thm) I); haftmann@31962: val add_default_eqn_attrib = Attrib.internal (K add_default_eqn_attribute); haftmann@31962: haftmann@37425: fun add_nbe_default_eqn thm thy = haftmann@37425: gen_add_eqn true (mk_eqn thy (thm, false)) thy; haftmann@37425: haftmann@37425: val add_nbe_default_eqn_attribute = Thm.declaration_attribute haftmann@37425: (fn thm => Context.mapping (add_nbe_default_eqn thm) I); haftmann@37425: val add_nbe_default_eqn_attrib = Attrib.internal (K add_nbe_default_eqn_attribute); haftmann@37425: haftmann@35226: fun add_abs_eqn raw_thm thy = haftmann@35226: let haftmann@35226: val (abs_thm, tyco) = (apfst Thm.close_derivation o mk_abs_eqn thy) raw_thm; haftmann@35226: val c = const_abs_eqn thy abs_thm; haftmann@35226: in change_fun_spec false c (K (Abstr (abs_thm, tyco))) thy end; haftmann@35226: haftmann@31962: fun del_eqn thm thy = case mk_eqn_liberal thy thm haftmann@35226: of SOME (thm, _) => let haftmann@40758: fun del_eqn' (Default _) = empty_fun_spec haftmann@35226: | del_eqn' (Eqns eqns) = haftmann@35226: Eqns (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns) haftmann@35226: | del_eqn' spec = spec haftmann@35226: in change_fun_spec true (const_eqn thy thm) del_eqn' thy end haftmann@31962: | NONE => thy; haftmann@31962: haftmann@35226: fun del_eqns c = change_fun_spec true c (K empty_fun_spec); haftmann@34244: haftmann@34244: haftmann@34244: (* cases *) haftmann@34244: haftmann@40758: fun case_cong thy case_const (num_args, (pos, _)) = haftmann@37438: let wenzelm@43326: val ([x, y], ctxt) = fold_map Name.variant ["A", "A'"] Name.context; wenzelm@43326: val (zs, _) = fold_map Name.variant (replicate (num_args - 1) "") ctxt; haftmann@37438: val (ws, vs) = chop pos zs; haftmann@37448: val T = Logic.unvarifyT_global (Sign.the_const_type thy case_const); wenzelm@40844: val Ts = binder_types T; haftmann@37438: val T_cong = nth Ts pos; haftmann@37438: fun mk_prem z = Free (z, T_cong); haftmann@37438: fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts); haftmann@37438: val (prem, concl) = pairself Logic.mk_equals (pairself mk_prem (x, y), pairself mk_concl (x, y)); haftmann@37521: fun tac { context, prems } = Simplifier.rewrite_goals_tac prems wenzelm@42360: THEN ALLGOALS (Proof_Context.fact_tac [Drule.reflexive_thm]); wenzelm@51551: in Goal.prove_sorry_global thy (x :: y :: zs) [prem] concl tac end; haftmann@37438: haftmann@34244: fun add_case thm thy = haftmann@34244: let haftmann@43634: val (case_const, (k, cos)) = case_cert thm; haftmann@47555: val _ = case (filter_out (is_constr thy) o map_filter I) cos haftmann@34244: of [] => () wenzelm@45430: | cs => error ("Non-constructor(s) in case certificate: " ^ commas_quote cs); haftmann@43634: val entry = (1 + Int.max (1, length cos), (k, cos)); haftmann@43634: fun register_case cong = (map_cases o apfst) haftmann@43634: (Symtab.update (case_const, (entry, cong))); haftmann@43634: fun register_for_constructors (Constructors (cos', cases)) = haftmann@43634: Constructors (cos', Andreas@47437: if exists (fn (co, _) => member (op =) cos (SOME co)) cos' haftmann@43634: then insert (op =) case_const cases haftmann@43634: else cases) haftmann@43634: | register_for_constructors (x as Abstractor _) = x; haftmann@43634: val register_type = (map_typs o Symtab.map) haftmann@43634: (K ((map o apsnd o apsnd) register_for_constructors)); haftmann@37438: in haftmann@37438: thy haftmann@37438: |> Theory.checkpoint haftmann@37438: |> `(fn thy => case_cong thy case_const entry) haftmann@43634: |-> (fn cong => map_exec_purge (register_case cong #> register_type)) haftmann@37438: end; haftmann@34244: haftmann@34244: fun add_undefined c thy = haftmann@34244: (map_exec_purge o map_cases o apsnd) (Symtab.update (c, ())) thy; haftmann@34244: haftmann@34244: haftmann@35299: (* types *) haftmann@34244: haftmann@35299: fun register_type (tyco, vs_spec) thy = haftmann@34244: let haftmann@35226: val (old_constrs, some_old_proj) = haftmann@35299: case these (Symtab.lookup ((the_types o the_exec) thy) tyco) haftmann@43634: of (_, (_, Constructors (cos, _))) :: _ => (map fst cos, NONE) haftmann@36209: | (_, (_, Abstractor ((co, _), (proj, _)))) :: _ => ([co], SOME proj) haftmann@43636: | [] => ([], NONE); haftmann@43636: val outdated_funs1 = (map fst o fst o constructors_of o snd) vs_spec; haftmann@43636: val outdated_funs2 = case some_old_proj haftmann@43636: of NONE => [] haftmann@35226: | SOME old_proj => Symtab.fold haftmann@36209: (fn (c, ((_, spec), _)) => haftmann@36209: if member (op =) (the_list (associated_abstype spec)) tyco haftmann@35226: then insert (op =) c else I) haftmann@43637: ((the_functions o the_exec) thy) [old_proj]; haftmann@34244: fun drop_outdated_cases cases = fold Symtab.delete_safe haftmann@37438: (Symtab.fold (fn (c, ((_, (_, cos)), _)) => Andreas@47437: if exists (member (op =) old_constrs) (map_filter I cos) haftmann@34244: then insert (op =) c else I) cases []) cases; haftmann@34244: in haftmann@34244: thy haftmann@43636: |> fold del_eqns (outdated_funs1 @ outdated_funs2) haftmann@34244: |> map_exec_purge haftmann@35226: ((map_typs o Symtab.map_default (tyco, [])) (cons (serial (), vs_spec)) haftmann@34244: #> (map_cases o apfst) drop_outdated_cases) haftmann@34244: end; haftmann@34244: haftmann@35299: fun unoverload_const_typ thy (c, ty) = (AxClass.unoverload_const thy (c, ty), ty); haftmann@34244: haftmann@35299: structure Datatype_Interpretation = haftmann@35299: Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool); haftmann@35299: haftmann@35299: fun datatype_interpretation f = Datatype_Interpretation.interpretation haftmann@40726: (fn (tyco, _) => fn thy => f (tyco, fst (get_type thy tyco)) thy); haftmann@35226: haftmann@35226: fun add_datatype proto_constrs thy = haftmann@35226: let haftmann@35226: val constrs = map (unoverload_const_typ thy) proto_constrs; haftmann@35226: val (tyco, (vs, cos)) = constrset_of_consts thy constrs; haftmann@35226: in haftmann@35226: thy haftmann@43634: |> register_type (tyco, (vs, Constructors (cos, []))) haftmann@35299: |> Datatype_Interpretation.data (tyco, serial ()) haftmann@35226: end; haftmann@35226: haftmann@35226: fun add_datatype_cmd raw_constrs thy = haftmann@35226: add_datatype (map (read_bare_const thy) raw_constrs) thy; haftmann@35226: haftmann@35299: structure Abstype_Interpretation = haftmann@35299: Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool); haftmann@35299: haftmann@35299: fun abstype_interpretation f = Abstype_Interpretation.interpretation haftmann@35299: (fn (tyco, _) => fn thy => f (tyco, get_abstype_spec thy tyco) thy); haftmann@35299: haftmann@36112: fun add_abstype proto_thm thy = haftmann@34244: let haftmann@40726: val (tyco, (vs, (abs_ty as (abs, (_, ty)), (rep, cert)))) = haftmann@49760: error_abs_thm (check_abstype_cert thy) thy proto_thm; haftmann@35226: in haftmann@35226: thy haftmann@36112: |> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert)))) wenzelm@45344: |> change_fun_spec false rep wenzelm@45344: (K (Proj (Logic.varify_types_global (mk_proj tyco vs ty abs rep), tyco))) haftmann@36112: |> Abstype_Interpretation.data (tyco, serial ()) haftmann@35226: end; haftmann@34244: haftmann@35226: haftmann@32070: (* setup *) haftmann@31998: haftmann@31962: val _ = Context.>> (Context.map_theory haftmann@31962: (let haftmann@31962: fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I); haftmann@31998: val code_attribute_parser = haftmann@31998: Args.del |-- Scan.succeed (mk_attribute del_eqn) haftmann@31998: || Args.$$$ "nbe" |-- Scan.succeed (mk_attribute add_nbe_eqn) haftmann@36112: || Args.$$$ "abstype" |-- Scan.succeed (mk_attribute add_abstype) haftmann@35226: || Args.$$$ "abstract" |-- Scan.succeed (mk_attribute add_abs_eqn) haftmann@31998: || Scan.succeed (mk_attribute add_warning_eqn); haftmann@31962: in haftmann@35299: Datatype_Interpretation.init haftmann@31998: #> Attrib.setup (Binding.name "code") (Scan.lift code_attribute_parser) haftmann@31998: "declare theorems for code generation" haftmann@31962: end)); haftmann@31962: haftmann@24219: end; (*struct*) haftmann@24219: haftmann@24219: haftmann@35226: (* type-safe interfaces for data dependent on executable code *) haftmann@24219: haftmann@34173: functor Code_Data(Data: CODE_DATA_ARGS): CODE_DATA = haftmann@24219: struct haftmann@24219: haftmann@24219: type T = Data.T; haftmann@24219: exception Data of T; haftmann@24219: fun dest (Data x) = x haftmann@24219: haftmann@34173: val kind = Code.declare_data (Data Data.empty); haftmann@24219: haftmann@24219: val data_op = (kind, Data, dest); haftmann@24219: haftmann@39397: fun change_yield (SOME thy) f = Code.change_yield_data data_op thy f haftmann@39397: | change_yield NONE f = f Data.empty haftmann@39397: haftmann@39397: fun change some_thy f = snd (change_yield some_thy (pair () o f)); haftmann@24219: haftmann@24219: end; haftmann@24219: haftmann@28143: structure Code : CODE = struct open Code; end;