diff --git a/src/HOL/Tools/Lifting/lifting_setup.ML b/src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML +++ b/src/HOL/Tools/Lifting/lifting_setup.ML @@ -1,1046 +1,1042 @@ (* Title: HOL/Tools/Lifting/lifting_setup.ML Author: Ondrej Kuncar Setting up the lifting infrastructure. *) signature LIFTING_SETUP = sig exception SETUP_LIFTING_INFR of string type config = { notes: bool }; val default_config: config; val setup_by_quotient: config -> thm -> thm option -> thm option -> local_theory -> binding * local_theory val setup_by_typedef_thm: config -> thm -> local_theory -> binding * local_theory val lifting_restore: Lifting_Info.quotient -> Context.generic -> Context.generic val lifting_forget: string -> local_theory -> local_theory val update_transfer_rules: string -> local_theory -> local_theory val pointer_of_bundle_binding: Proof.context -> binding -> string end structure Lifting_Setup: LIFTING_SETUP = struct open Lifting_Util infix 0 MRSL exception SETUP_LIFTING_INFR of string (* Config *) type config = { notes: bool }; val default_config = { notes = true }; fun define_crel (config: config) rep_fun lthy = let val (qty, rty) = (dest_funT o fastype_of) rep_fun val rep_fun_graph = (HOLogic.eq_const rty) $ Bound 1 $ (rep_fun $ Bound 0) val def_term = Abs ("x", rty, Abs ("y", qty, rep_fun_graph)) val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty val crel_name = Binding.prefix_name "cr_" qty_name val (fixed_def_term, lthy1) = lthy |> yield_singleton (Variable.importT_terms) def_term val ((_, (_ , def_thm)), lthy2) = if #notes config then Local_Theory.define ((crel_name, NoSyn), ((Thm.def_binding crel_name, []), fixed_def_term)) lthy1 else Local_Theory.define ((Binding.concealed crel_name, NoSyn), (Binding.empty_atts, fixed_def_term)) lthy1 in (def_thm, lthy2) end fun print_define_pcrel_warning msg = let val warning_msg = cat_lines ["Generation of a parametrized correspondence relation failed.", (Pretty.string_of (Pretty.block [Pretty.str "Reason:", Pretty.brk 2, msg]))] in warning warning_msg end fun define_pcrel (config: config) crel lthy0 = let val (fixed_crel, lthy1) = yield_singleton Variable.importT_terms crel lthy0 val [rty', qty] = (binder_types o fastype_of) fixed_crel val (param_rel, args) = Lifting_Term.generate_parametrized_relator lthy1 rty' val rty_raw = (domain_type o range_type o fastype_of) param_rel val tyenv_match = Sign.typ_match (Proof_Context.theory_of lthy1) (rty_raw, rty') Vartab.empty val param_rel_subst = Envir.subst_term (tyenv_match,Vartab.empty) param_rel val args_subst = map (Envir.subst_term (tyenv_match,Vartab.empty)) args val (instT, lthy2) = lthy1 |> Variable.declare_names fixed_crel |> Variable.importT_inst (param_rel_subst :: args_subst) val args_fixed = (map (Term_Subst.instantiate (instT, Vars.empty))) args_subst val param_rel_fixed = Term_Subst.instantiate (instT, Vars.empty) param_rel_subst val rty = (domain_type o fastype_of) param_rel_fixed val relcomp_op = Const (\<^const_name>\relcompp\, (rty --> rty' --> HOLogic.boolT) --> (rty' --> qty --> HOLogic.boolT) --> rty --> qty --> HOLogic.boolT) val qty_name = (fst o dest_Type) qty val pcrel_name = Binding.prefix_name "pcr_" ((Binding.name o Long_Name.base_name) qty_name) val relator_type = foldr1 (op -->) ((map type_of args_fixed) @ [rty, qty, HOLogic.boolT]) val lhs = Library.foldl (op $) ((Free (Binding.name_of pcrel_name, relator_type)), args_fixed) val rhs = relcomp_op $ param_rel_fixed $ fixed_crel val definition_term = Logic.mk_equals (lhs, rhs) fun note_def lthy = Specification.definition (SOME (pcrel_name, SOME relator_type, NoSyn)) [] [] (Binding.empty_atts, definition_term) lthy |>> (snd #> snd); fun raw_def lthy = let val ((_, rhs), prove) = Local_Defs.derived_def lthy (K []) {conditional = true} definition_term; val ((_, (_, raw_th)), lthy') = Local_Theory.define ((Binding.concealed pcrel_name, NoSyn), (Binding.empty_atts, rhs)) lthy; val th = prove lthy' raw_th; in (th, lthy') end val (def_thm, lthy3) = if #notes config then note_def lthy2 else raw_def lthy2 in (SOME def_thm, lthy3) end handle Lifting_Term.PARAM_QUOT_THM (_, msg) => (print_define_pcrel_warning msg; (NONE, lthy0)) local val eq_OO_meta = mk_meta_eq @{thm eq_OO} fun print_generate_pcr_cr_eq_error ctxt term = let val goal = Const (\<^const_name>\HOL.eq\, dummyT) $ term $ Const (\<^const_name>\HOL.eq\, dummyT) val error_msg = cat_lines ["Generation of a pcr_cr_eq failed.", (Pretty.string_of (Pretty.block [Pretty.str "Reason: Cannot prove this: ", Pretty.brk 2, Syntax.pretty_term ctxt goal])), "Most probably a relator_eq rule for one of the involved types is missing."] in error error_msg end in fun define_pcr_cr_eq (config: config) lthy pcr_rel_def = let val lhs = (Thm.term_of o Thm.lhs_of) pcr_rel_def val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type o List.last o binder_types o fastype_of) lhs val args = (snd o strip_comb) lhs fun make_inst var ctxt = let val typ = snd (relation_types (#2 (dest_Var var))) val sort = Type.sort_of_atyp typ val (fresh_var, ctxt') = yield_singleton Variable.invent_types sort ctxt val inst = (#1 (dest_Var var), Thm.cterm_of ctxt' (HOLogic.eq_const (TFree fresh_var))) in (inst, ctxt') end val (args_inst, args_ctxt) = fold_map make_inst args lthy val pcr_cr_eq = pcr_rel_def |> infer_instantiate args_ctxt args_inst |> Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.bottom_rewrs_conv (Transfer.get_relator_eq args_ctxt) args_ctxt))) in case (Thm.term_of o Thm.rhs_of) pcr_cr_eq of Const (\<^const_name>\relcompp\, _) $ Const (\<^const_name>\HOL.eq\, _) $ _ => let val thm = pcr_cr_eq |> Conv.fconv_rule (Conv.arg_conv (Conv.rewr_conv eq_OO_meta)) |> HOLogic.mk_obj_eq |> singleton (Variable.export args_ctxt lthy) val lthy' = lthy |> #notes config ? (Local_Theory.note ((Binding.qualify_name true qty_name "pcr_cr_eq", []), [thm]) #> #2) in (thm, lthy') end | Const (\<^const_name>\relcompp\, _) $ t $ _ => print_generate_pcr_cr_eq_error args_ctxt t | _ => error "generate_pcr_cr_eq: implementation error" end end fun define_code_constr quot_thm lthy = let val abs = quot_thm_abs quot_thm in if is_Const abs then let val (fixed_abs, lthy') = yield_singleton Variable.importT_terms abs lthy in Local_Theory.background_theory (Code.declare_datatype_global [dest_Const fixed_abs]) lthy' end else lthy end fun define_abs_type quot_thm = Lifting_Def.can_generate_code_cert quot_thm ? Code.declare_abstype (quot_thm RS @{thm Quotient_abs_rep}); local exception QUOT_ERROR of Pretty.T list in fun quot_thm_sanity_check ctxt quot_thm = let val _ = if (Thm.nprems_of quot_thm > 0) then raise QUOT_ERROR [Pretty.block [Pretty.str "The Quotient theorem has extra assumptions:", Pretty.brk 1, Thm.pretty_thm ctxt quot_thm]] else () val _ = quot_thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_Quotient handle TERM _ => raise QUOT_ERROR [Pretty.block [Pretty.str "The Quotient theorem is not of the right form:", Pretty.brk 1, Thm.pretty_thm ctxt quot_thm]] val ((_, [quot_thm_fixed]), ctxt') = Variable.importT [quot_thm] ctxt val (rty, qty) = quot_thm_rty_qty quot_thm_fixed val rty_tfreesT = Term.add_tfree_namesT rty [] val qty_tfreesT = Term.add_tfree_namesT qty [] val extra_rty_tfrees = case subtract (op =) qty_tfreesT rty_tfreesT of [] => [] | extras => [Pretty.block ([Pretty.str "Extra variables in the raw type:", Pretty.brk 1] @ ((Pretty.commas o map (Pretty.str o quote)) extras) @ [Pretty.str "."])] val not_type_constr = case qty of Type _ => [] | _ => [Pretty.block [Pretty.str "The quotient type ", Pretty.quote (Syntax.pretty_typ ctxt' qty), Pretty.brk 1, Pretty.str "is not a type constructor."]] val errs = extra_rty_tfrees @ not_type_constr in if null errs then () else raise QUOT_ERROR errs end handle QUOT_ERROR errs => error (cat_lines (["Sanity check of the quotient theorem failed:"] @ (map (Pretty.string_of o Pretty.item o single) errs))) end fun lifting_bundle qty_full_name qinfo lthy = let val thy = Proof_Context.theory_of lthy val binding = Binding.qualify_name true (qty_full_name |> Long_Name.base_name |> Binding.name) "lifting" val morphed_binding = Morphism.binding (Local_Theory.target_morphism lthy) binding val bundle_name = Name_Space.full_name (Name_Space.naming_of (Context.Theory thy)) morphed_binding fun phi_qinfo phi = Lifting_Info.transform_quotient phi qinfo val dummy_thm = Thm.transfer thy Drule.dummy_thm val restore_lifting_att = ([dummy_thm], [map Token.make_string0 ["Lifting.lifting_restore_internal", bundle_name]]) in lthy |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>} (fn phi => Lifting_Info.init_restore_data bundle_name (phi_qinfo phi)) |> Bundle.bundle ((binding, [restore_lifting_att])) [] |> pair binding end fun setup_lifting_infr config quot_thm opt_reflp_thm lthy = let val _ = quot_thm_sanity_check lthy quot_thm val (_, qty) = quot_thm_rty_qty quot_thm val (pcrel_def, lthy1) = define_pcrel config (quot_thm_crel quot_thm) lthy (**) val pcrel_def = Option.map (Morphism.thm (Local_Theory.target_morphism lthy1)) pcrel_def (**) val (pcr_cr_eq, lthy2) = case pcrel_def of SOME pcrel_def => apfst SOME (define_pcr_cr_eq config lthy1 pcrel_def) | NONE => (NONE, lthy1) val pcr_info = case pcrel_def of SOME pcrel_def => SOME { pcrel_def = pcrel_def, pcr_cr_eq = the pcr_cr_eq } | NONE => NONE val quotients = { quot_thm = quot_thm, pcr_info = pcr_info } val qty_full_name = (fst o dest_Type) qty fun quot_info phi = Lifting_Info.transform_quotient phi quotients val reflexivity_rule_attr = Attrib.internal \<^here> (K Lifting_Info.add_reflexivity_rule_attribute) val lthy3 = case opt_reflp_thm of SOME reflp_thm => lthy2 |> (#2 oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]), [reflp_thm RS @{thm reflp_ge_eq}]) |> define_code_constr quot_thm | NONE => lthy2 |> define_abs_type quot_thm in lthy3 |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>} (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi)) |> lifting_bundle qty_full_name quotients end local fun importT_inst_exclude exclude ts ctxt = let val tvars = rev (subtract op= exclude (fold Term.add_tvars ts [])) val (tfrees, ctxt') = Variable.invent_types (map #2 tvars) ctxt in (TVars.make (tvars ~~ map TFree tfrees), ctxt') end fun import_inst_exclude exclude ts ctxt = let val excludeT = fold (Term.add_tvarsT o snd) exclude [] val (instT, ctxt') = importT_inst_exclude excludeT ts ctxt val vars = map (apsnd (Term_Subst.instantiateT instT)) (rev (subtract op= exclude (fold Term.add_vars ts []))) val (xs, ctxt'') = Variable.variant_fixes (map (#1 o #1) vars) ctxt' val inst = Vars.make (vars ~~ map Free (xs ~~ map #2 vars)) in ((instT, inst), ctxt'') end fun import_terms_exclude exclude ts ctxt = let val (inst, ctxt') = import_inst_exclude exclude ts ctxt in (map (Term_Subst.instantiate inst) ts, ctxt') end in fun reduce_goal not_fix goal tac ctxt = let val (fixed_goal, ctxt') = yield_singleton (import_terms_exclude not_fix) goal ctxt val init_goal = Goal.init (Thm.cterm_of ctxt' fixed_goal) in (singleton (Variable.export ctxt' ctxt) o Goal.conclude) (the (SINGLE tac init_goal)) end end local val OO_rules = @{thms left_total_OO left_unique_OO right_total_OO right_unique_OO bi_total_OO bi_unique_OO} in fun parametrize_class_constraint ctxt0 pcr_def constraint = let fun generate_transfer_rule pcr_def constraint goal ctxt = let val (fixed_goal, ctxt') = yield_singleton (Variable.import_terms true) goal ctxt val init_goal = Goal.init (Thm.cterm_of ctxt' fixed_goal) val rules = Transfer.get_transfer_raw ctxt' val rules = constraint :: OO_rules @ rules val tac = K (Local_Defs.unfold0_tac ctxt' [pcr_def]) THEN' REPEAT_ALL_NEW (resolve_tac ctxt' rules) in (singleton (Variable.export ctxt' ctxt) o Goal.conclude) (the (SINGLE (tac 1) init_goal)) end fun make_goal pcr_def constr = let val pred_name = (fst o dest_Const o strip_args 1 o HOLogic.dest_Trueprop o Thm.prop_of) constr val arg = (fst o Logic.dest_equals o Thm.prop_of) pcr_def in HOLogic.mk_Trueprop ((Const (pred_name, (fastype_of arg) --> HOLogic.boolT)) $ arg) end val check_assms = let val right_names = ["right_total", "right_unique", "left_total", "left_unique", "bi_total", "bi_unique"] fun is_right_name name = member op= right_names (Long_Name.base_name name) fun is_trivial_assm (Const (name, _) $ Var (_, _)) = is_right_name name | is_trivial_assm (Const (name, _) $ Free (_, _)) = is_right_name name | is_trivial_assm _ = false in fn thm => let val prems = map HOLogic.dest_Trueprop (Thm.prems_of thm) val thm_name = (Long_Name.base_name o fst o dest_Const o strip_args 1 o HOLogic.dest_Trueprop o Thm.concl_of) thm val non_trivial_assms = filter_out is_trivial_assm prems in if null non_trivial_assms then () else Pretty.block ([Pretty.str "Non-trivial assumptions in ", Pretty.str thm_name, Pretty.str " transfer rule found:", Pretty.brk 1] @ Pretty.commas (map (Syntax.pretty_term ctxt0) non_trivial_assms)) |> Pretty.string_of |> warning end end val goal = make_goal pcr_def constraint val thm = generate_transfer_rule pcr_def constraint goal ctxt0 val _ = check_assms thm in thm end end local val id_unfold = (Conv.rewr_conv (mk_meta_eq @{thm id_def})) in fun generate_parametric_id lthy rty id_transfer_rule = let (* it doesn't raise an exception because it would have already raised it in define_pcrel *) val (quot_thm, _, ctxt') = Lifting_Term.prove_param_quot_thm lthy rty val parametrized_relator = singleton (Variable.export_terms ctxt' lthy) (quot_thm_crel quot_thm) val id_transfer = @{thm id_transfer} |> Thm.incr_indexes (Term.maxidx_of_term parametrized_relator + 1) |> Conv.fconv_rule(HOLogic.Trueprop_conv (Conv.arg_conv id_unfold then_conv Conv.arg1_conv id_unfold)) val var = hd (Term.add_vars (Thm.prop_of id_transfer) []) val inst = [(#1 var, Thm.cterm_of lthy parametrized_relator)] val id_par_thm = infer_instantiate lthy inst id_transfer in Lifting_Def.generate_parametric_transfer_rule lthy id_transfer_rule id_par_thm end handle Lifting_Term.MERGE_TRANSFER_REL msg => let val error_msg = cat_lines ["Generation of a parametric transfer rule for the abs. or the rep. function failed.", "A non-parametric version will be used.", (Pretty.string_of (Pretty.block [Pretty.str "Reason:", Pretty.brk 2, msg]))] in (warning error_msg; id_transfer_rule) end end local fun rewrite_first_Domainp_arg rewr_thm thm = Conv.fconv_rule (Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.arg1_conv (Conv.arg_conv (Conv.rewr_conv rewr_thm))))) thm fun fold_Domainp_pcrel pcrel_def thm = let val ct = thm |> Thm.cprop_of |> Drule.strip_imp_concl |> Thm.dest_arg |> Thm.dest_arg1 |> Thm.dest_arg val pcrel_def = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) pcrel_def val thm' = Thm.instantiate (Thm.match (ct, Thm.rhs_of pcrel_def)) thm handle Pattern.MATCH => raise CTERM ("fold_Domainp_pcrel", [ct, Thm.rhs_of pcrel_def]) in rewrite_first_Domainp_arg (Thm.symmetric pcrel_def) thm' end fun reduce_Domainp ctxt rules thm = let val goal = thm |> Thm.prems_of |> hd val var = goal |> HOLogic.dest_Trueprop |> dest_comb |> snd |> dest_Var val reduced_assm = reduce_goal [var] goal (TRY (REPEAT_ALL_NEW (resolve_tac ctxt rules) 1)) ctxt in reduced_assm RS thm end in fun parametrize_domain dom_thm (pcr_info : Lifting_Info.pcr) ctxt0 = let fun reduce_first_assm ctxt rules thm = let val goal = thm |> Thm.prems_of |> hd val reduced_assm = reduce_goal [] goal (TRY (REPEAT_ALL_NEW (resolve_tac ctxt rules) 1)) ctxt in reduced_assm RS thm end val pcr_cr_met_eq = #pcr_cr_eq pcr_info RS @{thm eq_reflection} val pcr_Domainp_eq = rewrite_first_Domainp_arg (Thm.symmetric pcr_cr_met_eq) dom_thm val pcrel_def = #pcrel_def pcr_info val pcr_Domainp_par_left_total = (dom_thm RS @{thm pcr_Domainp_par_left_total}) |> fold_Domainp_pcrel pcrel_def |> reduce_first_assm ctxt0 (Lifting_Info.get_reflexivity_rules ctxt0) val pcr_Domainp_par = (dom_thm RS @{thm pcr_Domainp_par}) |> fold_Domainp_pcrel pcrel_def |> reduce_Domainp ctxt0 (Transfer.get_relator_domain ctxt0) val pcr_Domainp = (dom_thm RS @{thm pcr_Domainp}) |> fold_Domainp_pcrel pcrel_def val thms = [("domain", [pcr_Domainp], @{attributes [transfer_domain_rule]}), ("domain_par", [pcr_Domainp_par], @{attributes [transfer_domain_rule]}), ("domain_par_left_total", [pcr_Domainp_par_left_total], @{attributes [transfer_domain_rule]}), ("domain_eq", [pcr_Domainp_eq], @{attributes [transfer_domain_rule]})] in thms end fun parametrize_total_domain left_total pcrel_def ctxt = let val thm = (left_total RS @{thm pcr_Domainp_total}) |> fold_Domainp_pcrel pcrel_def |> reduce_Domainp ctxt (Transfer.get_relator_domain ctxt) in [("domain", [thm], @{attributes [transfer_domain_rule]})] end end fun get_pcrel_info ctxt qty_full_name = #pcr_info (the (Lifting_Info.lookup_quotients ctxt qty_full_name)) fun get_Domainp_thm quot_thm = the (get_first (try(curry op RS quot_thm)) [@{thm eq_onp_to_Domainp}, @{thm Quotient_to_Domainp}]) fun notes names thms = let val notes = if names then map (fn (name, thms, attrs) => ((name, []), [(thms, attrs)])) thms else map_filter (fn (_, thms, attrs) => if null attrs then NONE else SOME (Binding.empty_atts, [(thms, attrs)])) thms in Local_Theory.notes notes #> snd end fun map_thms map_name map_thm thms = map (fn (name, thms, attr) => (map_name name, map map_thm thms, attr)) thms (* Sets up the Lifting package by a quotient theorem. quot_thm - a quotient theorem (Quotient R Abs Rep T) opt_reflp_thm - a theorem saying that a relation from quot_thm is reflexive (in the form "reflp R") opt_par_thm - a parametricity theorem for R *) fun setup_by_quotient (config: config) quot_thm opt_reflp_thm opt_par_thm lthy0 = let (**) val quot_thm = Morphism.thm (Local_Theory.target_morphism lthy0) quot_thm (**) val (rty, qty) = quot_thm_rty_qty quot_thm val induct_attr = Attrib.internal \<^here> (K (Induct.induct_type (fst (dest_Type qty)))) val qty_full_name = (fst o dest_Type) qty val qty_name = (Binding.name o Long_Name.base_name) qty_full_name val qualify = Binding.qualify_name true qty_name val notes1 = case opt_reflp_thm of SOME reflp_thm => let val thms = [("abs_induct", @{thms Quotient_total_abs_induct}, [induct_attr]), ("abs_eq_iff", @{thms Quotient_total_abs_eq_iff}, [])] in map_thms qualify (fn thm => [quot_thm, reflp_thm] MRSL thm) thms end | NONE => let val thms = [("abs_induct", @{thms Quotient_abs_induct}, [induct_attr])] in map_thms qualify (fn thm => quot_thm RS thm) thms end val dom_thm = get_Domainp_thm quot_thm fun setup_transfer_rules_nonpar notes = let val notes1 = case opt_reflp_thm of SOME reflp_thm => let val thms = [("id_abs_transfer",@{thms Quotient_id_abs_transfer}, @{attributes [transfer_rule]}), ("left_total", @{thms Quotient_left_total}, @{attributes [transfer_rule]}), ("bi_total", @{thms Quotient_bi_total}, @{attributes [transfer_rule]})] in map_thms qualify (fn thm => [quot_thm, reflp_thm] MRSL thm) thms end | NONE => map_thms qualify I [("domain", [dom_thm], @{attributes [transfer_domain_rule]})] val notes2 = map_thms qualify (fn thm => quot_thm RS thm) [("rel_eq_transfer", @{thms Quotient_rel_eq_transfer}, @{attributes [transfer_rule]}), ("right_unique", @{thms Quotient_right_unique}, @{attributes [transfer_rule]}), ("right_total", @{thms Quotient_right_total}, @{attributes [transfer_rule]})] in notes2 @ notes1 @ notes end fun generate_parametric_rel_eq ctxt transfer_rule opt_param_thm = (case opt_param_thm of NONE => transfer_rule | SOME param_thm => (Lifting_Def.generate_parametric_transfer_rule ctxt transfer_rule param_thm handle Lifting_Term.MERGE_TRANSFER_REL msg => error ("Generation of a parametric transfer rule for the quotient relation failed:\n" ^ Pretty.string_of msg))) fun setup_transfer_rules_par ctxt notes = let val pcrel_info = the (get_pcrel_info ctxt qty_full_name) val pcrel_def = #pcrel_def pcrel_info val notes1 = case opt_reflp_thm of SOME reflp_thm => let val left_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_left_total}) val bi_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}) val domain_thms = parametrize_total_domain left_total pcrel_def ctxt val id_abs_transfer = generate_parametric_id ctxt rty (Lifting_Term.parametrize_transfer_rule ctxt ([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer})) val left_total = parametrize_class_constraint ctxt pcrel_def left_total val bi_total = parametrize_class_constraint ctxt pcrel_def bi_total val thms = [("id_abs_transfer", [id_abs_transfer], @{attributes [transfer_rule]}), ("left_total", [left_total], @{attributes [transfer_rule]}), ("bi_total", [bi_total], @{attributes [transfer_rule]})] in map_thms qualify I thms @ map_thms qualify I domain_thms end | NONE => let val thms = parametrize_domain dom_thm pcrel_info ctxt in map_thms qualify I thms end val rel_eq_transfer = generate_parametric_rel_eq ctxt (Lifting_Term.parametrize_transfer_rule ctxt (quot_thm RS @{thm Quotient_rel_eq_transfer})) opt_par_thm val right_unique = parametrize_class_constraint ctxt pcrel_def (quot_thm RS @{thm Quotient_right_unique}) val right_total = parametrize_class_constraint ctxt pcrel_def (quot_thm RS @{thm Quotient_right_total}) val notes2 = map_thms qualify I [("rel_eq_transfer", [rel_eq_transfer], @{attributes [transfer_rule]}), ("right_unique", [right_unique], @{attributes [transfer_rule]}), ("right_total", [right_total], @{attributes [transfer_rule]})] in notes2 @ notes1 @ notes end fun setup_rules lthy = let val thms = if is_some (get_pcrel_info lthy qty_full_name) then setup_transfer_rules_par lthy notes1 else setup_transfer_rules_nonpar notes1 in notes (#notes config) thms lthy end in lthy0 |> setup_lifting_infr config quot_thm opt_reflp_thm ||> setup_rules end (* Sets up the Lifting package by a typedef theorem. gen_code - flag if an abstract type given by typedef_thm should be registred as an abstract type in the code generator typedef_thm - a typedef theorem (type_definition Rep Abs S) *) fun setup_by_typedef_thm config typedef_thm lthy0 = let val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o Thm.prop_of) typedef_thm val (T_def, lthy1) = define_crel config rep_fun lthy0 (**) val T_def = Morphism.thm (Local_Theory.target_morphism lthy1) T_def (**) val quot_thm = case typedef_set of Const (\<^const_name>\top\, _) => [typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient} | Const (\<^const_name>\Collect\, _) $ Abs (_, _, _) => [typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient} | _ => [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient} val (rty, qty) = quot_thm_rty_qty quot_thm val qty_full_name = (fst o dest_Type) qty val qty_name = (Binding.name o Long_Name.base_name) qty_full_name val qualify = Binding.qualify_name true qty_name val opt_reflp_thm = case typedef_set of Const (\<^const_name>\top\, _) => SOME ((typedef_thm RS @{thm UNIV_typedef_to_equivp}) RS @{thm equivp_reflp2}) | _ => NONE val dom_thm = get_Domainp_thm quot_thm fun setup_transfer_rules_nonpar notes = let val notes1 = case opt_reflp_thm of SOME reflp_thm => let val thms = [("id_abs_transfer",@{thms Quotient_id_abs_transfer}, @{attributes [transfer_rule]}), ("left_total", @{thms Quotient_left_total}, @{attributes [transfer_rule]}), ("bi_total", @{thms Quotient_bi_total}, @{attributes [transfer_rule]})] in map_thms qualify (fn thm => [quot_thm, reflp_thm] MRSL thm) thms end | NONE => map_thms qualify I [("domain", [dom_thm], @{attributes [transfer_domain_rule]})] val thms = [("rep_transfer", @{thms typedef_rep_transfer}, @{attributes [transfer_rule]}), ("left_unique", @{thms typedef_left_unique}, @{attributes [transfer_rule]}), ("right_unique", @{thms typedef_right_unique}, @{attributes [transfer_rule]}), ("right_total", @{thms typedef_right_total}, @{attributes [transfer_rule]}), ("bi_unique", @{thms typedef_bi_unique}, @{attributes [transfer_rule]})] in map_thms qualify (fn thm => [typedef_thm, T_def] MRSL thm) thms @ notes1 @ notes end fun setup_transfer_rules_par ctxt notes = let val pcrel_info = (the (get_pcrel_info ctxt qty_full_name)) val pcrel_def = #pcrel_def pcrel_info val notes1 = case opt_reflp_thm of SOME reflp_thm => let val left_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_left_total}) val bi_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}) val domain_thms = parametrize_total_domain left_total pcrel_def ctxt val left_total = parametrize_class_constraint ctxt pcrel_def left_total val bi_total = parametrize_class_constraint ctxt pcrel_def bi_total val id_abs_transfer = generate_parametric_id ctxt rty (Lifting_Term.parametrize_transfer_rule ctxt ([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer})) val thms = [("left_total", [left_total], @{attributes [transfer_rule]}), ("bi_total", [bi_total], @{attributes [transfer_rule]}), ("id_abs_transfer",[id_abs_transfer], @{attributes [transfer_rule]})] in map_thms qualify I thms @ map_thms qualify I domain_thms end | NONE => let val thms = parametrize_domain dom_thm pcrel_info ctxt in map_thms qualify I thms end val notes2 = map_thms qualify (fn thm => generate_parametric_id ctxt rty (Lifting_Term.parametrize_transfer_rule ctxt ([typedef_thm, T_def] MRSL thm))) [("rep_transfer", @{thms typedef_rep_transfer}, @{attributes [transfer_rule]})]; val notes3 = map_thms qualify (fn thm => parametrize_class_constraint ctxt pcrel_def ([typedef_thm, T_def] MRSL thm)) [("left_unique", @{thms typedef_left_unique}, @{attributes [transfer_rule]}), ("right_unique", @{thms typedef_right_unique},@{attributes [transfer_rule]}), ("bi_unique", @{thms typedef_bi_unique}, @{attributes [transfer_rule]}), ("right_total", @{thms typedef_right_total}, @{attributes [transfer_rule]})] in notes3 @ notes2 @ notes1 @ notes end val notes1 = [(Binding.prefix_name "Quotient_" qty_name, [quot_thm], [])] fun setup_rules lthy = let val thms = if is_some (get_pcrel_info lthy qty_full_name) then setup_transfer_rules_par lthy notes1 else setup_transfer_rules_nonpar notes1 in notes (#notes config) thms lthy end in lthy1 |> setup_lifting_infr config quot_thm opt_reflp_thm ||> setup_rules end fun setup_lifting_cmd xthm opt_reflp_xthm opt_par_xthm lthy = let val input_thm = singleton (Attrib.eval_thms lthy) xthm val input_term = (HOLogic.dest_Trueprop o Thm.prop_of) input_thm handle TERM _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported." fun sanity_check_reflp_thm reflp_thm = let val reflp_tm = (HOLogic.dest_Trueprop o Thm.prop_of) reflp_thm handle TERM _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"." in case reflp_tm of \<^Const_>\reflp_on _ for \<^Const>\top_class.top _\ _\ => () | _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"." end fun check_qty qty = if not (is_Type qty) then error "The abstract type must be a type constructor." else () fun setup_quotient () = let val opt_reflp_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_reflp_xthm val _ = if is_some opt_reflp_thm then sanity_check_reflp_thm (the opt_reflp_thm) else () val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm val _ = check_qty (snd (quot_thm_rty_qty input_thm)) in setup_by_quotient default_config input_thm opt_reflp_thm opt_par_thm lthy |> snd end fun setup_typedef () = let val qty = (range_type o fastype_of o hd o get_args 2) input_term val _ = check_qty qty in case opt_reflp_xthm of SOME _ => error "The reflexivity theorem cannot be specified if the type_definition theorem is used." | NONE => ( case opt_par_xthm of SOME _ => error "The parametricity theorem cannot be specified if the type_definition theorem is used." | NONE => setup_by_typedef_thm default_config input_thm lthy |> snd ) end in case input_term of (Const (\<^const_name>\Quotient\, _) $ _ $ _ $ _ $ _) => setup_quotient () | (Const (\<^const_name>\type_definition\, _) $ _ $ _ $ _) => setup_typedef () | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported." end val _ = Outer_Syntax.local_theory \<^command_keyword>\setup_lifting\ "setup lifting infrastructure" (Parse.thm -- Scan.option Parse.thm -- Scan.option (\<^keyword>\parametric\ |-- Parse.!!! Parse.thm) >> (fn ((xthm, opt_reflp_xthm), opt_par_xthm) => setup_lifting_cmd xthm opt_reflp_xthm opt_par_xthm)) (* restoring lifting infrastructure *) local exception PCR_ERROR of Pretty.T list in fun lifting_restore_sanity_check ctxt (qinfo:Lifting_Info.quotient) = let val quot_thm = (#quot_thm qinfo) val _ = quot_thm_sanity_check ctxt quot_thm val pcr_info_err = (case #pcr_info qinfo of SOME pcr => let val pcrel_def = #pcrel_def pcr val pcr_cr_eq = #pcr_cr_eq pcr val (def_lhs, _) = Logic.dest_equals (Thm.prop_of pcrel_def) handle TERM _ => raise PCR_ERROR [Pretty.block [Pretty.str "The pcr definiton theorem is not a plain meta equation:", Pretty.brk 1, Thm.pretty_thm ctxt pcrel_def]] val pcr_const_def = head_of def_lhs val (eq_lhs, eq_rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of pcr_cr_eq)) handle TERM _ => raise PCR_ERROR [Pretty.block [Pretty.str "The pcr_cr equation theorem is not a plain equation:", Pretty.brk 1, Thm.pretty_thm ctxt pcr_cr_eq]] val (pcr_const_eq, eqs) = strip_comb eq_lhs fun is_eq (Const (\<^const_name>\HOL.eq\, _)) = true | is_eq _ = false fun eq_Const (Const (name1, _)) (Const (name2, _)) = (name1 = name2) | eq_Const _ _ = false val all_eqs = if not (forall is_eq eqs) then [Pretty.block [Pretty.str "Arguments of the lhs of the pcr_cr equation theorem are not only equalities:", Pretty.brk 1, Thm.pretty_thm ctxt pcr_cr_eq]] else [] val pcr_consts_not_equal = if not (eq_Const pcr_const_def pcr_const_eq) then [Pretty.block [Pretty.str "Parametrized correspondence relation constants in pcr_def and pcr_cr_eq are not equal:", Pretty.brk 1, Syntax.pretty_term ctxt pcr_const_def, Pretty.brk 1, Pretty.str "vs.", Pretty.brk 1, Syntax.pretty_term ctxt pcr_const_eq]] else [] val crel = quot_thm_crel quot_thm val cr_consts_not_equal = if not (eq_Const crel eq_rhs) then [Pretty.block [Pretty.str "Correspondence relation constants in the Quotient theorem and pcr_cr_eq are not equal:", Pretty.brk 1, Syntax.pretty_term ctxt crel, Pretty.brk 1, Pretty.str "vs.", Pretty.brk 1, Syntax.pretty_term ctxt eq_rhs]] else [] in all_eqs @ pcr_consts_not_equal @ cr_consts_not_equal end | NONE => []) val errs = pcr_info_err in if null errs then () else raise PCR_ERROR errs end handle PCR_ERROR errs => error (cat_lines (["Sanity check failed:"] @ (map (Pretty.string_of o Pretty.item o single) errs))) end (* Registers the data in qinfo in the Lifting infrastructure. *) fun lifting_restore qinfo ctxt = let val _ = lifting_restore_sanity_check (Context.proof_of ctxt) qinfo val (_, qty) = quot_thm_rty_qty (#quot_thm qinfo) val qty_full_name = (fst o dest_Type) qty val stored_qinfo = Lifting_Info.lookup_quotients (Context.proof_of ctxt) qty_full_name in if is_some (stored_qinfo) andalso not (Lifting_Info.quotient_eq (qinfo, (the stored_qinfo))) then error (Pretty.string_of (Pretty.block [Pretty.str "Lifting is already setup for the type", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ (Context.proof_of ctxt) qty)])) else Lifting_Info.update_quotients qty_full_name qinfo ctxt end val parse_opt_pcr = Scan.optional (Attrib.thm -- Attrib.thm >> (fn (pcrel_def, pcr_cr_eq) => SOME {pcrel_def = pcrel_def, pcr_cr_eq = pcr_cr_eq})) NONE val lifting_restore_attribute_setup = Attrib.setup \<^binding>\lifting_restore\ ((Attrib.thm -- parse_opt_pcr) >> (fn (quot_thm, opt_pcr) => let val qinfo = { quot_thm = quot_thm, pcr_info = opt_pcr} in Thm.declaration_attribute (K (lifting_restore qinfo)) end)) "restoring lifting infrastructure" val _ = Theory.setup lifting_restore_attribute_setup fun lifting_restore_internal bundle_name ctxt = let val restore_info = Lifting_Info.lookup_restore_data (Context.proof_of ctxt) bundle_name in case restore_info of SOME restore_info => ctxt |> lifting_restore (#quotient restore_info) |> fold_rev Transfer.transfer_raw_add (Item_Net.content (#transfer_rules restore_info)) | NONE => ctxt end val lifting_restore_internal_attribute_setup = Attrib.setup \<^binding>\lifting_restore_internal\ (Scan.lift Parse.string >> (fn name => Thm.declaration_attribute (K (lifting_restore_internal name)))) "restoring lifting infrastructure; internal attribute; not meant to be used directly by regular users" val _ = Theory.setup lifting_restore_internal_attribute_setup (* lifting_forget *) val monotonicity_names = [\<^const_name>\right_unique\, \<^const_name>\left_unique\, \<^const_name>\right_total\, \<^const_name>\left_total\, \<^const_name>\bi_unique\, \<^const_name>\bi_total\] fun fold_transfer_rel f (Const (\<^const_name>\Transfer.Rel\, _) $ rel $ _ $ _) = f rel | fold_transfer_rel f (Const (\<^const_name>\HOL.eq\, _) $ (Const (\<^const_name>\Domainp\, _) $ rel) $ _) = f rel | fold_transfer_rel f (Const (name, _) $ rel) = if member op= monotonicity_names name then f rel else f \<^term>\undefined\ | fold_transfer_rel f _ = f \<^term>\undefined\ fun filter_transfer_rules_by_rel transfer_rel transfer_rules = let val transfer_rel_name = transfer_rel |> dest_Const |> fst; fun has_transfer_rel thm = let val concl = thm |> Thm.concl_of |> HOLogic.dest_Trueprop in member op= (fold_transfer_rel (fn tm => Term.add_const_names tm []) concl) transfer_rel_name end handle TERM _ => false in filter has_transfer_rel transfer_rules end type restore_data = {quotient : Lifting_Info.quotient, transfer_rules: thm Item_Net.T} fun get_transfer_rel (qinfo : Lifting_Info.quotient) = let fun get_pcrel pcr_def = pcr_def |> Thm.concl_of |> Logic.dest_equals |> fst |> head_of in if is_some (#pcr_info qinfo) then get_pcrel (#pcrel_def (the (#pcr_info qinfo))) else quot_thm_crel (#quot_thm qinfo) end fun pointer_of_bundle_name bundle_name ctxt = let val bundle = Bundle.read ctxt bundle_name fun err () = error "The provided bundle is not a lifting bundle" in (case bundle of - [(_, [arg_src])] => - let - val (name, _) = Token.syntax (Scan.lift Parse.string) arg_src ctxt - handle ERROR _ => err () - in name end + [(_, [arg_src])] => (Token.read ctxt Parse.string arg_src handle ERROR _ => err ()) | _ => err ()) end fun pointer_of_bundle_binding ctxt binding = Name_Space.full_name (Name_Space.naming_of (Context.Theory (Proof_Context.theory_of ctxt))) binding fun lifting_forget pointer lthy = let fun get_transfer_rules_to_delete qinfo ctxt = let val transfer_rel = get_transfer_rel qinfo in filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw ctxt) end in case Lifting_Info.lookup_restore_data lthy pointer of SOME restore_info => let val qinfo = #quotient restore_info val quot_thm = #quot_thm qinfo val transfer_rules = get_transfer_rules_to_delete qinfo lthy in Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>} (K (fold (Transfer.transfer_raw_del) transfer_rules #> Lifting_Info.delete_quotients quot_thm)) lthy end | NONE => error "The lifting bundle refers to non-existent restore data." end fun lifting_forget_cmd bundle_name lthy = lifting_forget (pointer_of_bundle_name bundle_name lthy) lthy val _ = Outer_Syntax.local_theory \<^command_keyword>\lifting_forget\ "unsetup Lifting and Transfer for the given lifting bundle" (Parse.name_position >> lifting_forget_cmd) (* lifting_update *) fun update_transfer_rules pointer lthy = let fun new_transfer_rules ({ quotient = qinfo, ... }:Lifting_Info.restore_data) lthy = let val transfer_rel = get_transfer_rel qinfo val transfer_rules = filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw lthy) in fn phi => fold_rev (Item_Net.update o Morphism.thm phi) transfer_rules Thm.item_net end in case Lifting_Info.lookup_restore_data lthy pointer of SOME refresh_data => Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>} (fn phi => Lifting_Info.add_transfer_rules_in_restore_data pointer (new_transfer_rules refresh_data lthy phi)) lthy | NONE => error "The lifting bundle refers to non-existent restore data." end fun lifting_update_cmd bundle_name lthy = update_transfer_rules (pointer_of_bundle_name bundle_name lthy) lthy val _ = Outer_Syntax.local_theory \<^command_keyword>\lifting_update\ "add newly introduced transfer rules to a bundle storing the state of Lifting and Transfer" (Parse.name_position >> lifting_update_cmd) end diff --git a/src/Pure/Isar/parse.ML b/src/Pure/Isar/parse.ML --- a/src/Pure/Isar/parse.ML +++ b/src/Pure/Isar/parse.ML @@ -1,540 +1,540 @@ (* Title: Pure/Isar/parse.ML Author: Markus Wenzel, TU Muenchen Generic parsers for Isabelle/Isar outer syntax. *) signature PARSE = sig val group: (unit -> string) -> (Token.T list -> 'a) -> Token.T list -> 'a val !!! : (Token.T list -> 'a) -> Token.T list -> 'a val !!!! : (Token.T list -> 'a) -> Token.T list -> 'a val not_eof: Token.T parser val token: 'a parser -> Token.T parser val range: 'a parser -> ('a * Position.range) parser val position: 'a parser -> ('a * Position.T) parser val input: 'a parser -> Input.source parser val inner_syntax: 'a parser -> string parser val command: string parser val keyword: string parser val short_ident: string parser val long_ident: string parser val sym_ident: string parser val dots: string parser val minus: string parser val term_var: string parser val type_ident: string parser val type_var: string parser val number: string parser val float_number: string parser val string: string parser val string_position: (string * Position.T) parser val alt_string: string parser val cartouche: string parser val control: Antiquote.control parser val eof: string parser val command_name: string -> string parser val keyword_with: (string -> bool) -> string parser val keyword_markup: bool * Markup.T -> string -> string parser val keyword_improper: string -> string parser val $$$ : string -> string parser val reserved: string -> string parser val underscore: string parser val maybe: 'a parser -> 'a option parser val maybe_position: ('a * Position.T) parser -> ('a option * Position.T) parser val opt_keyword: string -> bool parser val opt_bang: bool parser val begin: string parser val opt_begin: bool parser val nat: int parser val int: int parser val real: real parser val enum_positions: string -> 'a parser -> ('a list * Position.T list) parser val enum1_positions: string -> 'a parser -> ('a list * Position.T list) parser val enum: string -> 'a parser -> 'a list parser val enum1: string -> 'a parser -> 'a list parser val and_list: 'a parser -> 'a list parser val and_list1: 'a parser -> 'a list parser val enum': string -> 'a context_parser -> 'a list context_parser val enum1': string -> 'a context_parser -> 'a list context_parser val and_list': 'a context_parser -> 'a list context_parser val and_list1': 'a context_parser -> 'a list context_parser val list: 'a parser -> 'a list parser val list1: 'a parser -> 'a list parser val name: string parser val name_range: (string * Position.range) parser val name_position: (string * Position.T) parser val binding: binding parser val embedded: string parser val embedded_inner_syntax: string parser val embedded_input: Input.source parser val embedded_position: (string * Position.T) parser val path_input: Input.source parser val path: string parser val path_binding: (string * Position.T) parser val in_path: string -> Input.source parser val in_path_parens: string -> Input.source parser val chapter_name: (string * Position.T) parser val session_name: (string * Position.T) parser val theory_name: (string * Position.T) parser val liberal_name: string parser val parname: string parser val parbinding: binding parser val class: string parser val sort: string parser val type_const: string parser val arity: (string * string list * string) parser val multi_arity: (string list * string list * string) parser val type_args: string list parser val type_args_constrained: (string * string option) list parser val typ: string parser val mixfix: mixfix parser val mixfix': mixfix parser val opt_mixfix: mixfix parser val opt_mixfix': mixfix parser val syntax_mode: Syntax.mode parser val where_: string parser val const_decl: (string * string * mixfix) parser val const_binding: (binding * string * mixfix) parser val params: (binding * string option * mixfix) list parser val vars: (binding * string option * mixfix) list parser val for_fixes: (binding * string option * mixfix) list parser val ML_source: Input.source parser val document_source: Input.source parser val document_marker: Input.source parser val const: string parser val term: string parser val prop: string parser val literal_fact: string parser val propp: (string * string list) parser val termp: (string * string list) parser val private: Position.T parser val qualified: Position.T parser val target: (string * Position.T) parser val opt_target: (string * Position.T) option parser val args: Token.T list parser val args1: (string -> bool) -> Token.T list parser val attribs: Token.src list parser val opt_attribs: Token.src list parser val thm_sel: Facts.interval list parser val thm: (Facts.ref * Token.src list) parser val thms1: (Facts.ref * Token.src list) list parser val options: ((string * Position.T) * (string * Position.T)) list parser val embedded_ml: ML_Lex.token Antiquote.antiquote list parser val read_antiq: Keyword.keywords -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a val read_embedded: Proof.context -> Keyword.keywords -> 'a parser -> Input.source -> 'a val read_embedded_src: Proof.context -> Keyword.keywords -> 'a parser -> Token.src -> 'a end; structure Parse: PARSE = struct (** error handling **) (* group atomic parsers (no cuts!) *) fun group s scan = scan || Scan.fail_with (fn [] => (fn () => s () ^ " expected,\nbut end-of-input was found") | tok :: _ => (fn () => (case Token.text_of tok of (txt, "") => s () ^ " expected,\nbut " ^ txt ^ Position.here (Token.pos_of tok) ^ " was found" | (txt1, txt2) => s () ^ " expected,\nbut " ^ txt1 ^ Position.here (Token.pos_of tok) ^ " was found:\n" ^ txt2))); (* cut *) fun cut kind scan = let fun get_pos [] = " (end-of-input)" | get_pos (tok :: _) = Position.here (Token.pos_of tok); fun err (toks, NONE) = (fn () => kind ^ get_pos toks) | err (toks, SOME msg) = (fn () => let val s = msg () in if String.isPrefix kind s then s else kind ^ get_pos toks ^ ": " ^ s end); in Scan.!! err scan end; fun !!! scan = cut "Outer syntax error" scan; fun !!!! scan = cut "Corrupted outer syntax in presentation" scan; (** basic parsers **) (* tokens *) fun RESET_VALUE atom = (*required for all primitive parsers*) Scan.ahead (Scan.one (K true)) -- atom >> (fn (arg, x) => (Token.assign NONE arg; x)); val not_eof = RESET_VALUE (Scan.one Token.not_eof); fun token atom = Scan.ahead not_eof --| atom; fun range scan = (Scan.ahead not_eof >> (Token.range_of o single)) -- scan >> Library.swap; fun position scan = (Scan.ahead not_eof >> Token.pos_of) -- scan >> Library.swap; fun input atom = Scan.ahead atom |-- not_eof >> Token.input_of; fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.inner_syntax_of; fun kind k = group (fn () => Token.str_of_kind k) (RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of)); val command = kind Token.Command; val keyword = kind Token.Keyword; val short_ident = kind Token.Ident; val long_ident = kind Token.Long_Ident; val sym_ident = kind Token.Sym_Ident; val term_var = kind Token.Var; val type_ident = kind Token.Type_Ident; val type_var = kind Token.Type_Var; val number = kind Token.Nat; val float_number = kind Token.Float; val string = kind Token.String; val alt_string = kind Token.Alt_String; val cartouche = kind Token.Cartouche; val control = token (kind Token.control_kind) >> (the o Token.get_control); val eof = kind Token.EOF; fun command_name x = group (fn () => Token.str_of_kind Token.Command ^ " " ^ quote x) (RESET_VALUE (Scan.one (fn tok => Token.is_command tok andalso Token.content_of tok = x))) >> Token.content_of; fun keyword_with pred = RESET_VALUE (Scan.one (Token.keyword_with pred) >> Token.content_of); fun keyword_markup markup x = group (fn () => Token.str_of_kind Token.Keyword ^ " " ^ quote x) (Scan.ahead not_eof -- keyword_with (fn y => x = y)) >> (fn (tok, x) => (Token.assign (SOME (Token.Literal markup)) tok; x)); val keyword_improper = keyword_markup (true, Markup.improper); val $$$ = keyword_markup (false, Markup.quasi_keyword); fun reserved x = group (fn () => "reserved identifier " ^ quote x) (RESET_VALUE (Scan.one (Token.ident_with (fn y => x = y)) >> Token.content_of)); val dots = sym_ident :-- (fn "\" => Scan.succeed () | _ => Scan.fail) >> #1; val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1; val underscore = sym_ident :-- (fn "_" => Scan.succeed () | _ => Scan.fail) >> #1; fun maybe scan = underscore >> K NONE || scan >> SOME; fun maybe_position scan = position (underscore >> K NONE) || scan >> apfst SOME; val nat = number >> (#1 o Library.read_int o Symbol.explode); val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *; val real = float_number >> Value.parse_real || int >> Real.fromInt; fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false; val opt_bang = Scan.optional ($$$ "!" >> K true) false; val begin = $$$ "begin"; val opt_begin = Scan.optional (begin >> K true) false; (* enumerations *) fun enum1_positions sep scan = scan -- Scan.repeat (position ($$$ sep) -- !!! scan) >> (fn (x, ys) => (x :: map #2 ys, map (#2 o #1) ys)); fun enum_positions sep scan = enum1_positions sep scan || Scan.succeed ([], []); fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan); fun enum sep scan = enum1 sep scan || Scan.succeed []; fun enum1' sep scan = scan ::: Scan.repeat (Scan.lift ($$$ sep) |-- scan); fun enum' sep scan = enum1' sep scan || Scan.succeed []; fun and_list1 scan = enum1 "and" scan; fun and_list scan = enum "and" scan; fun and_list1' scan = enum1' "and" scan; fun and_list' scan = enum' "and" scan; fun list1 scan = enum1 "," scan; fun list scan = enum "," scan; (* names and embedded content *) val name = group (fn () => "name") (short_ident || long_ident || sym_ident || number || string); val name_range = input name >> Input.source_content_range; val name_position = input name >> Input.source_content; val string_position = input string >> Input.source_content; val binding = name_position >> Binding.make; val embedded = group (fn () => "embedded content") (cartouche || string || short_ident || long_ident || sym_ident || term_var || type_ident || type_var || number); val embedded_inner_syntax = inner_syntax embedded; val embedded_input = input embedded; val embedded_position = embedded_input >> Input.source_content; val path_input = group (fn () => "file name/path specification") embedded_input; val path = path_input >> Input.string_of; val path_binding = group (fn () => "path binding (strict file name)") (position embedded); fun in_path default = Scan.optional ($$$ "in" |-- !!! path_input) (Input.string default); fun in_path_parens default = Scan.optional ($$$ "(" |-- !!! ($$$ "in" |-- path_input --| $$$ ")")) (Input.string default); val chapter_name = group (fn () => "chapter name") name_position; val session_name = group (fn () => "session name") name_position; val theory_name = group (fn () => "theory name") name_position; val liberal_name = keyword_with Token.ident_or_symbolic || name; val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") ""; val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Binding.empty; (* type classes *) val class = group (fn () => "type class") (inner_syntax embedded); val sort = group (fn () => "sort") (inner_syntax embedded); val type_const = group (fn () => "type constructor") (inner_syntax embedded); val arity = type_const -- ($$$ "::" |-- !!! (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> Scan.triple2; val multi_arity = and_list1 type_const -- ($$$ "::" |-- !!! (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> Scan.triple2; (* types *) val typ = group (fn () => "type") (inner_syntax embedded); fun type_arguments arg = arg >> single || $$$ "(" |-- !!! (list1 arg --| $$$ ")") || Scan.succeed []; val type_args = type_arguments type_ident; val type_args_constrained = type_arguments (type_ident -- Scan.option ($$$ "::" |-- !!! sort)); (* mixfix annotations *) local val mfix = input (string || cartouche); val mixfix_ = mfix -- !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] -- Scan.optional nat 1000) >> (fn (sy, (ps, p)) => fn range => Mixfix (sy, ps, p, range)); val structure_ = $$$ "structure" >> K Structure; val binder_ = $$$ "binder" |-- !!! (mfix -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n)))) >> (fn (sy, (p, q)) => fn range => Binder (sy, p, q, range)); val infixl_ = $$$ "infixl" |-- !!! (mfix -- nat >> (fn (sy, p) => fn range => Infixl (sy, p, range))); val infixr_ = $$$ "infixr" |-- !!! (mfix -- nat >> (fn (sy, p) => fn range => Infixr (sy, p, range))); val infix_ = $$$ "infix" |-- !!! (mfix -- nat >> (fn (sy, p) => fn range => Infix (sy, p, range))); val mixfix_body = mixfix_ || structure_ || binder_ || infixl_ || infixr_ || infix_; fun annotation guard body = Scan.trace ($$$ "(" |-- guard (body --| $$$ ")")) >> (fn (mx, toks) => mx (Token.range_of toks)); fun opt_annotation guard body = Scan.optional (annotation guard body) NoSyn; in val mixfix = annotation !!! mixfix_body; val mixfix' = annotation I mixfix_body; val opt_mixfix = opt_annotation !!! mixfix_body; val opt_mixfix' = opt_annotation I mixfix_body; end; (* syntax mode *) val syntax_mode_spec = ($$$ "output" >> K ("", false)) || name -- Scan.optional ($$$ "output" >> K false) true; val syntax_mode = Scan.optional ($$$ "(" |-- !!! (syntax_mode_spec --| $$$ ")")) Syntax.mode_default; (* fixes *) val where_ = $$$ "where"; val const_decl = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> Scan.triple1; val const_binding = binding -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> Scan.triple1; val param_mixfix = binding -- Scan.option ($$$ "::" |-- typ) -- mixfix' >> (single o Scan.triple1); val params = (binding -- Scan.repeat binding) -- Scan.option ($$$ "::" |-- !!! (Scan.ahead typ -- embedded)) >> (fn ((x, ys), T) => (x, Option.map #1 T, NoSyn) :: map (fn y => (y, Option.map #2 T, NoSyn)) ys); val vars = and_list1 (param_mixfix || params) >> flat; val for_fixes = Scan.optional ($$$ "for" |-- !!! vars) []; (* embedded source text *) val ML_source = input (group (fn () => "ML source") embedded); val document_source = input (group (fn () => "document source") embedded); val document_marker = group (fn () => "document marker") (RESET_VALUE (Scan.one Token.is_document_marker >> Token.input_of)); (* terms *) val const = group (fn () => "constant") (inner_syntax embedded); val term = group (fn () => "term") (inner_syntax embedded); val prop = group (fn () => "proposition") (inner_syntax embedded); val literal_fact = inner_syntax (group (fn () => "literal fact") (alt_string || cartouche)); (* patterns *) val is_terms = Scan.repeat1 ($$$ "is" |-- term); val is_props = Scan.repeat1 ($$$ "is" |-- prop); val propp = prop -- Scan.optional ($$$ "(" |-- !!! (is_props --| $$$ ")")) []; val termp = term -- Scan.optional ($$$ "(" |-- !!! (is_terms --| $$$ ")")) []; (* target information *) val private = position ($$$ "private") >> #2; val qualified = position ($$$ "qualified") >> #2; val target = ($$$ "(" -- $$$ "in") |-- !!! (name_position --| $$$ ")"); val opt_target = Scan.option target; (* arguments within outer syntax *) local val argument_kinds = [Token.Ident, Token.Long_Ident, Token.Sym_Ident, Token.Var, Token.Type_Ident, Token.Type_Var, Token.Nat, Token.Float, Token.String, Token.Alt_String, Token.Cartouche]; fun arguments is_symid = let fun argument blk = group (fn () => "argument") (Scan.one (fn tok => let val kind = Token.kind_of tok in member (op =) argument_kinds kind orelse Token.keyword_with is_symid tok orelse (blk andalso Token.keyword_with (fn s => s = ",") tok) end)); fun args blk x = Scan.optional (args1 blk) [] x and args1 blk x = (Scan.repeats1 (Scan.repeat1 (argument blk) || argsp "(" ")" || argsp "[" "]")) x and argsp l r x = (token ($$$ l) ::: !!! (args true @@@ (token ($$$ r) >> single))) x; in (args, args1) end; in val args = #1 (arguments Token.ident_or_symbolic) false; fun args1 is_symid = #2 (arguments is_symid) false; end; (* attributes *) val attrib = token liberal_name ::: !!! args; val attribs = $$$ "[" |-- list attrib --| $$$ "]"; val opt_attribs = Scan.optional attribs []; (* theorem references *) val thm_sel = $$$ "(" |-- list1 (nat --| minus -- nat >> Facts.FromTo || nat --| minus >> Facts.From || nat >> Facts.Single) --| $$$ ")"; val thm = $$$ "[" |-- attribs --| $$$ "]" >> pair (Facts.named "") || (literal_fact >> Facts.Fact || name_position -- Scan.option thm_sel >> Facts.Named) -- opt_attribs; val thms1 = Scan.repeat1 thm; (* options *) val option_name = group (fn () => "option name") name_position; val option_value = group (fn () => "option value") ((token real || token name) >> Token.content_of); val option = option_name :-- (fn (_, pos) => Scan.optional ($$$ "=" |-- !!! (position option_value)) ("true", pos)); val options = $$$ "[" |-- list1 option --| $$$ "]"; (* embedded ML *) val embedded_ml = input underscore >> ML_Lex.read_source || embedded_input >> ML_Lex.read_source || control >> (ML_Lex.read_symbols o Antiquote.control_symbols); (* read embedded source, e.g. for antiquotations *) fun tokenize keywords = Token.tokenize keywords {strict = true} #> filter Token.is_proper; fun read_antiq keywords scan (syms, pos) = (case Scan.read Token.stopper scan (tokenize (Keyword.no_major_keywords keywords) syms) of SOME res => res | NONE => error ("Malformed antiquotation" ^ Position.here pos)); fun read_embedded ctxt keywords parse input = let val toks = tokenize keywords (Input.source_explode input); val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks); in (case Scan.read Token.stopper parse toks of SOME res => res | NONE => error ("Bad input" ^ Position.here (Input.pos_of input))) end; fun read_embedded_src ctxt keywords parse src = - Token.syntax (Scan.lift embedded_input) src ctxt - |> #1 |> read_embedded ctxt keywords parse; + Token.read ctxt embedded_input src + |> read_embedded ctxt keywords parse; end; diff --git a/src/Pure/Isar/token.ML b/src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML +++ b/src/Pure/Isar/token.ML @@ -1,839 +1,842 @@ (* Title: Pure/Isar/token.ML Author: Markus Wenzel, TU Muenchen Outer token syntax for Isabelle/Isar. *) signature TOKEN = sig datatype kind = (*immediate source*) Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat | Float | Space | (*delimited content*) String | Alt_String | Cartouche | Control of Antiquote.control | Comment of Comment.kind option | (*special content*) Error of string | EOF val control_kind: kind val str_of_kind: kind -> string type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T} type T type src = T list type name_value = {name: string, kind: string, print: Proof.context -> Markup.T * xstring} datatype value = Source of src | Literal of bool * Markup.T | Name of name_value * morphism | Typ of typ | Term of term | Fact of string option * thm list | Attribute of attribute Morphism.entity | Declaration of Morphism.declaration_entity | Files of file Exn.result list | Output of XML.body option val pos_of: T -> Position.T val adjust_offsets: (int -> int option) -> T -> T val eof: T val is_eof: T -> bool val not_eof: T -> bool val stopper: T Scan.stopper val kind_of: T -> kind val is_kind: kind -> T -> bool val get_control: T -> Antiquote.control option val is_command: T -> bool val keyword_with: (string -> bool) -> T -> bool val is_command_modifier: T -> bool val ident_with: (string -> bool) -> T -> bool val is_proper: T -> bool val is_comment: T -> bool val is_informal_comment: T -> bool val is_formal_comment: T -> bool val is_document_marker: T -> bool val is_ignored: T -> bool val is_begin_ignore: T -> bool val is_end_ignore: T -> bool val is_error: T -> bool val is_space: T -> bool val is_blank: T -> bool val is_newline: T -> bool val range_of: T list -> Position.range val core_range_of: T list -> Position.range val content_of: T -> string val source_of: T -> string val input_of: T -> Input.source val inner_syntax_of: T -> string val keyword_markup: bool * Markup.T -> string -> Markup.T val completion_report: T -> Position.report_text list val reports: Keyword.keywords -> T -> Position.report_text list val markups: Keyword.keywords -> T -> Markup.T list val unparse: T -> string val print: T -> string val text_of: T -> string * string val file_source: file -> Input.source val get_files: T -> file Exn.result list val put_files: file Exn.result list -> T -> T val get_output: T -> XML.body option val put_output: XML.body -> T -> T val get_value: T -> value option val reports_of_value: T -> Position.report list val name_value: name_value -> value val get_name: T -> name_value option val declare_maxidx: T -> Proof.context -> Proof.context val map_facts: (string option -> thm list -> thm list) -> T -> T val trim_context: T -> T val transfer: theory -> T -> T val transform: morphism -> T -> T val init_assignable: T -> T val assign: value option -> T -> T val evaluate: ('a -> value) -> (T -> 'a) -> T -> 'a val closure: T -> T val pretty_value: Proof.context -> T -> Pretty.T val name_of_src: src -> string * Position.T val args_of_src: src -> T list val checked_src: src -> bool val check_src: Proof.context -> (Proof.context -> 'a Name_Space.table) -> src -> src * 'a val pretty_src: Proof.context -> src -> Pretty.T val ident_or_symbolic: string -> bool val read_cartouche: Symbol_Pos.T list -> T val tokenize: Keyword.keywords -> {strict: bool} -> Symbol_Pos.T list -> T list val explode: Keyword.keywords -> Position.T -> string -> T list val explode0: Keyword.keywords -> string -> T list val print_name: Keyword.keywords -> string -> string val print_properties: Keyword.keywords -> Properties.T -> string val make: (int * int) * string -> Position.T -> T * Position.T val make_string: string * Position.T -> T val make_string0: string -> T val make_int: int -> T list val make_src: string * Position.T -> T list -> src type 'a parser = T list -> 'a * T list type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list) val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context + val read: Proof.context -> 'a parser -> src -> 'a end; structure Token: TOKEN = struct (** tokens **) (* token kind *) datatype kind = (*immediate source*) Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat | Float | Space | (*delimited content*) String | Alt_String | Cartouche | Control of Antiquote.control | Comment of Comment.kind option | (*special content*) Error of string | EOF; val control_kind = Control Antiquote.no_control; fun equiv_kind kind kind' = (case (kind, kind') of (Control _, Control _) => true | (Error _, Error _) => true | _ => kind = kind'); val str_of_kind = fn Command => "command" | Keyword => "keyword" | Ident => "identifier" | Long_Ident => "long identifier" | Sym_Ident => "symbolic identifier" | Var => "schematic variable" | Type_Ident => "type variable" | Type_Var => "schematic type variable" | Nat => "natural number" | Float => "floating-point number" | Space => "white space" | String => "quoted string" | Alt_String => "back-quoted string" | Cartouche => "text cartouche" | Control _ => "control cartouche" | Comment NONE => "informal comment" | Comment (SOME _) => "formal comment" | Error _ => "bad input" | EOF => "end-of-input"; val immediate_kinds = Vector.fromList [Command, Keyword, Ident, Long_Ident, Sym_Ident, Var, Type_Ident, Type_Var, Nat, Float, Space]; val delimited_kind = (fn String => true | Alt_String => true | Cartouche => true | Control _ => true | Comment _ => true | _ => false); (* datatype token *) (*The value slot assigns an (optional) internal value to a token, usually as a side-effect of special scanner setup (see also args.ML). Note that an assignable ref designates an intermediate state of internalization -- it is NOT meant to persist.*) type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}; type name_value = {name: string, kind: string, print: Proof.context -> Markup.T * xstring}; datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot and slot = Slot | Value of value option | Assignable of value option Unsynchronized.ref and value = Source of T list | Literal of bool * Markup.T | Name of name_value * morphism | Typ of typ | Term of term | Fact of string option * thm list | (*optional name for dynamic fact, i.e. fact "variable"*) Attribute of attribute Morphism.entity | Declaration of Morphism.declaration_entity | Files of file Exn.result list | Output of XML.body option; type src = T list; (* position *) fun pos_of (Token ((_, (pos, _)), _, _)) = pos; fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos; fun adjust_offsets adjust (Token ((x, range), y, z)) = Token ((x, apply2 (Position.adjust_offsets adjust) range), y, z); (* stopper *) fun mk_eof pos = Token (("", (pos, Position.none)), (EOF, ""), Slot); val eof = mk_eof Position.none; fun is_eof (Token (_, (EOF, _), _)) = true | is_eof _ = false; val not_eof = not o is_eof; val stopper = Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof; (* kind of token *) fun kind_of (Token (_, (k, _), _)) = k; fun is_kind k (Token (_, (k', _), _)) = equiv_kind k k'; fun get_control tok = (case kind_of tok of Control control => SOME control | _ => NONE); val is_command = is_kind Command; fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x | keyword_with _ _ = false; val is_command_modifier = keyword_with (fn x => x = "private" orelse x = "qualified"); fun ident_with pred (Token (_, (Ident, x), _)) = pred x | ident_with _ _ = false; fun is_ignored (Token (_, (Space, _), _)) = true | is_ignored (Token (_, (Comment NONE, _), _)) = true | is_ignored _ = false; fun is_proper (Token (_, (Space, _), _)) = false | is_proper (Token (_, (Comment _, _), _)) = false | is_proper _ = true; fun is_comment (Token (_, (Comment _, _), _)) = true | is_comment _ = false; fun is_informal_comment (Token (_, (Comment NONE, _), _)) = true | is_informal_comment _ = false; fun is_formal_comment (Token (_, (Comment (SOME _), _), _)) = true | is_formal_comment _ = false; fun is_document_marker (Token (_, (Comment (SOME Comment.Marker), _), _)) = true | is_document_marker _ = false; fun is_begin_ignore (Token (_, (Comment NONE, "<"), _)) = true | is_begin_ignore _ = false; fun is_end_ignore (Token (_, (Comment NONE, ">"), _)) = true | is_end_ignore _ = false; fun is_error (Token (_, (Error _, _), _)) = true | is_error _ = false; (* blanks and newlines -- space tokens obey lines *) fun is_space (Token (_, (Space, _), _)) = true | is_space _ = false; fun is_blank (Token (_, (Space, x), _)) = not (String.isSuffix "\n" x) | is_blank _ = false; fun is_newline (Token (_, (Space, x), _)) = String.isSuffix "\n" x | is_newline _ = false; (* range of tokens *) fun range_of (toks as tok :: _) = let val pos' = end_pos_of (List.last toks) in Position.range (pos_of tok, pos') end | range_of [] = Position.no_range; val core_range_of = drop_prefix is_ignored #> drop_suffix is_ignored #> range_of; (* token content *) fun content_of (Token (_, (_, x), _)) = x; fun source_of (Token ((source, _), _, _)) = source; fun input_of (Token ((source, range), (kind, _), _)) = Input.source (delimited_kind kind) source range; fun inner_syntax_of tok = let val x = content_of tok in if YXML.detect x then x else Syntax.implode_input (input_of tok) end; (* markup reports *) local val token_kind_markup = fn Var => (Markup.var, "") | Type_Ident => (Markup.tfree, "") | Type_Var => (Markup.tvar, "") | String => (Markup.string, "") | Alt_String => (Markup.alt_string, "") | Cartouche => (Markup.cartouche, "") | Control _ => (Markup.cartouche, "") | Comment _ => (Markup.comment, "") | Error msg => (Markup.bad (), msg) | _ => (Markup.empty, ""); fun keyword_reports tok = map (fn markup => ((pos_of tok, markup), "")); fun command_markups keywords x = if Keyword.is_theory_end keywords x then [Markup.keyword2 |> Markup.keyword_properties] else (if Keyword.is_proof_asm keywords x then [Markup.keyword3] else if Keyword.is_improper keywords x then [Markup.keyword1, Markup.improper] else [Markup.keyword1]) |> map Markup.command_properties; in fun keyword_markup (important, keyword) x = if important orelse Symbol.is_ascii_identifier x then keyword else Markup.delimiter; fun completion_report tok = if is_kind Keyword tok then map (fn m => ((pos_of tok, m), "")) (Completion.suppress_abbrevs (content_of tok)) else []; fun reports keywords tok = if is_command tok then keyword_reports tok (command_markups keywords (content_of tok)) else if is_kind Keyword tok then keyword_reports tok [keyword_markup (false, Markup.keyword2 |> Markup.keyword_properties) (content_of tok)] else let val pos = pos_of tok; val (m, text) = token_kind_markup (kind_of tok); val deleted = Symbol_Pos.explode_deleted (source_of tok, pos); in ((pos, m), text) :: map (fn p => ((p, Markup.delete), "")) deleted end; fun markups keywords = map (#2 o #1) o reports keywords; end; (* unparse *) fun unparse (Token (_, (kind, x), _)) = (case kind of String => Symbol_Pos.quote_string_qq x | Alt_String => Symbol_Pos.quote_string_bq x | Cartouche => cartouche x | Control control => Symbol_Pos.content (Antiquote.control_symbols control) | Comment NONE => enclose "(*" "*)" x | EOF => "" | _ => x); fun print tok = Markup.markups (markups Keyword.empty_keywords tok) (unparse tok); fun text_of tok = let val k = str_of_kind (kind_of tok); val ms = markups Keyword.empty_keywords tok; val s = unparse tok; in if s = "" then (k, "") else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ Markup.markups ms s, "") else (k, Markup.markups ms s) end; (** associated values **) (* inlined file content *) fun file_source (file: file) = let val text = cat_lines (#lines file); val end_pos = Position.symbol_explode text (#pos file); in Input.source true text (Position.range (#pos file, end_pos)) end; fun get_files (Token (_, _, Value (SOME (Files files)))) = files | get_files _ = []; fun put_files [] tok = tok | put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files))) | put_files _ tok = raise Fail ("Cannot put inlined files here" ^ Position.here (pos_of tok)); (* document output *) fun get_output (Token (_, _, Value (SOME (Output output)))) = output | get_output _ = NONE; fun put_output output (Token (x, y, Slot)) = Token (x, y, Value (SOME (Output (SOME output)))) | put_output _ tok = raise Fail ("Cannot put document output here" ^ Position.here (pos_of tok)); (* access values *) fun get_value (Token (_, _, Value v)) = v | get_value _ = NONE; fun map_value f (Token (x, y, Value (SOME v))) = Token (x, y, Value (SOME (f v))) | map_value _ tok = tok; (* reports of value *) fun get_assignable_value (Token (_, _, Assignable r)) = ! r | get_assignable_value (Token (_, _, Value v)) = v | get_assignable_value _ = NONE; fun reports_of_value tok = (case get_assignable_value tok of SOME (Literal markup) => let val pos = pos_of tok; val x = content_of tok; in if Position.is_reported pos then map (pair pos) (keyword_markup markup x :: Completion.suppress_abbrevs x) else [] end | _ => []); (* name value *) fun name_value a = Name (a, Morphism.identity); fun get_name tok = (case get_assignable_value tok of SOME (Name (a, _)) => SOME a | _ => NONE); (* maxidx *) fun declare_maxidx tok = (case get_value tok of SOME (Source src) => fold declare_maxidx src | SOME (Typ T) => Variable.declare_maxidx (Term.maxidx_of_typ T) | SOME (Term t) => Variable.declare_maxidx (Term.maxidx_of_term t) | SOME (Fact (_, ths)) => fold (Variable.declare_maxidx o Thm.maxidx_of) ths | SOME (Attribute _) => I (* FIXME !? *) | SOME (Declaration decl) => (fn ctxt => let val ctxt' = Context.proof_map (Morphism.form decl) ctxt in Variable.declare_maxidx (Variable.maxidx_of ctxt') ctxt end) | _ => I); (* fact values *) fun map_facts f = map_value (fn v => (case v of Source src => Source (map (map_facts f) src) | Fact (a, ths) => Fact (a, f a ths) | _ => v)); (* implicit context *) local fun context thm_context morphism_context attribute_context declaration_context = let fun token_context tok = map_value (fn Source src => Source (map token_context src) | Fact (a, ths) => Fact (a, map thm_context ths) | Name (a, phi) => Name (a, morphism_context phi) | Attribute a => Attribute (attribute_context a) | Declaration a => Declaration (declaration_context a) | v => v) tok; in token_context end; in val trim_context = context Thm.trim_context Morphism.reset_context Morphism.entity_reset_context Morphism.entity_reset_context; fun transfer thy = context (Thm.transfer thy) (Morphism.set_context thy) (Morphism.entity_set_context thy) (Morphism.entity_set_context thy); end; (* transform *) fun transform phi = map_value (fn v => (case v of Source src => Source (map (transform phi) src) | Literal _ => v | Name (a, psi) => Name (a, psi $> phi) | Typ T => Typ (Morphism.typ phi T) | Term t => Term (Morphism.term phi t) | Fact (a, ths) => Fact (a, Morphism.fact phi ths) | Attribute att => Attribute (Morphism.transform phi att) | Declaration decl => Declaration (Morphism.transform phi decl) | Files _ => v | Output _ => v)); (* static binding *) (*1st stage: initialize assignable slots*) fun init_assignable tok = (case tok of Token (x, y, Slot) => Token (x, y, Assignable (Unsynchronized.ref NONE)) | Token (_, _, Value _) => tok | Token (_, _, Assignable r) => (r := NONE; tok)); (*2nd stage: assign values as side-effect of scanning*) fun assign v tok = (case tok of Token (x, y, Slot) => Token (x, y, Value v) | Token (_, _, Value _) => tok | Token (_, _, Assignable r) => (r := v; tok)); fun evaluate mk eval arg = let val x = eval arg in (assign (SOME (mk x)) arg; x) end; (*3rd stage: static closure of final values*) fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v) | closure tok = tok; (* pretty *) fun pretty_keyword3 tok = let val props = Position.properties_of (pos_of tok) in Pretty.mark_str (Markup.properties props Markup.keyword3, unparse tok) end; fun pretty_value ctxt tok = (case get_value tok of SOME (Literal markup) => let val x = content_of tok in Pretty.mark_str (keyword_markup markup x, x) end | SOME (Name ({print, ...}, _)) => Pretty.quote (Pretty.mark_str (print ctxt)) | SOME (Typ T) => Syntax.pretty_typ ctxt T | SOME (Term t) => Syntax.pretty_term ctxt t | SOME (Fact (_, ths)) => Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.cartouche o Thm.pretty_thm ctxt) ths)) | SOME (Attribute _) => pretty_keyword3 tok | SOME (Declaration _) => pretty_keyword3 tok | _ => Pretty.marks_str (markups Keyword.empty_keywords tok, unparse tok)); (* src *) fun dest_src ([]: src) = raise Fail "Empty token source" | dest_src (head :: args) = (head, args); fun name_of_src src = let val head = #1 (dest_src src); val name = (case get_name head of SOME {name, ...} => name | NONE => content_of head); in (name, pos_of head) end; val args_of_src = #2 o dest_src; fun pretty_src ctxt src = let val (head, args) = dest_src src; val prt_name = (case get_name head of SOME {print, ...} => Pretty.mark_str (print ctxt) | NONE => Pretty.str (content_of head)); in Pretty.block (Pretty.breaks (Pretty.quote prt_name :: map (pretty_value ctxt) args)) end; fun checked_src (head :: _) = is_some (get_name head) | checked_src [] = true; fun check_src ctxt get_table src = let val (head, args) = dest_src src; val table = get_table ctxt; in (case get_name head of SOME {name, ...} => (src, Name_Space.get table name) | NONE => let val pos = pos_of head; val (name, x) = Name_Space.check (Context.Proof ctxt) table (content_of head, pos); val _ = Context_Position.report ctxt pos Markup.operator; val kind = Name_Space.kind_of (Name_Space.space_of_table table); fun print ctxt' = Name_Space.markup_extern ctxt' (Name_Space.space_of_table (get_table ctxt')) name; val value = name_value {name = name, kind = kind, print = print}; val head' = closure (assign (SOME value) head); in (head' :: args, x) end) end; (** scanners **) open Basic_Symbol_Pos; val err_prefix = "Outer lexical error: "; fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg); (* scan symbolic idents *) val scan_symid = Scan.many1 (Symbol.is_symbolic_char o Symbol_Pos.symbol) || Scan.one (Symbol.is_symbolic o Symbol_Pos.symbol) >> single; fun is_symid str = (case try Symbol.explode str of SOME [s] => Symbol.is_symbolic s orelse Symbol.is_symbolic_char s | SOME ss => forall Symbol.is_symbolic_char ss | _ => false); fun ident_or_symbolic "begin" = false | ident_or_symbolic ":" = true | ident_or_symbolic "::" = true | ident_or_symbolic s = Symbol_Pos.is_identifier s orelse is_symid s; (* scan cartouche *) val scan_cartouche = Symbol_Pos.scan_pos -- ((Symbol_Pos.scan_cartouche err_prefix >> Symbol_Pos.cartouche_content) -- Symbol_Pos.scan_pos); (* scan space *) fun space_symbol (s, _) = Symbol.is_blank s andalso s <> "\n"; val scan_space = Scan.many1 space_symbol @@@ Scan.optional ($$$ "\n") [] || Scan.many space_symbol @@@ $$$ "\n"; (* scan comment *) val scan_comment = Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body err_prefix -- Symbol_Pos.scan_pos); (** token sources **) local fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2; fun token k ss = Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.content ss), Slot); fun token_range k (pos1, (ss, pos2)) = Token (Symbol_Pos.implode_range (pos1, pos2) ss, (k, Symbol_Pos.content ss), Slot); fun scan_token keywords = !!! "bad input" (Symbol_Pos.scan_string_qq err_prefix >> token_range String || Symbol_Pos.scan_string_bq err_prefix >> token_range Alt_String || scan_comment >> token_range (Comment NONE) || Comment.scan_outer >> (fn (k, ss) => token (Comment (SOME k)) ss) || scan_cartouche >> token_range Cartouche || Antiquote.scan_control err_prefix >> (fn control => token (Control control) (Antiquote.control_symbols control)) || scan_space >> token Space || (Scan.max token_leq (Scan.max token_leq (Scan.literal (Keyword.major_keywords keywords) >> pair Command) (Scan.literal (Keyword.minor_keywords keywords) >> pair Keyword)) (Lexicon.scan_longid >> pair Long_Ident || Lexicon.scan_id >> pair Ident || Lexicon.scan_var >> pair Var || Lexicon.scan_tid >> pair Type_Ident || Lexicon.scan_tvar >> pair Type_Var || Symbol_Pos.scan_float >> pair Float || Symbol_Pos.scan_nat >> pair Nat || scan_symid >> pair Sym_Ident) >> uncurry token)); fun recover msg = (Symbol_Pos.recover_string_qq || Symbol_Pos.recover_string_bq || Symbol_Pos.recover_cartouche || Symbol_Pos.recover_comment || Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single) >> (single o token (Error msg)); in fun make_source keywords {strict} = let val scan_strict = Scan.bulk (scan_token keywords); val scan = if strict then scan_strict else Scan.recover scan_strict recover; in Source.source Symbol_Pos.stopper scan end; fun read_cartouche syms = (case Scan.read Symbol_Pos.stopper (scan_cartouche >> token_range Cartouche) syms of SOME tok => tok | NONE => error ("Single cartouche expected" ^ Position.here (#1 (Symbol_Pos.range syms)))); end; (* explode *) fun tokenize keywords strict syms = Source.of_list syms |> make_source keywords strict |> Source.exhaust; fun explode keywords pos text = Symbol_Pos.explode (text, pos) |> tokenize keywords {strict = false}; fun explode0 keywords = explode keywords Position.none; (* print names in parsable form *) fun print_name keywords name = ((case explode keywords Position.none name of [tok] => not (member (op =) [Ident, Long_Ident, Sym_Ident, Nat] (kind_of tok)) | _ => true) ? Symbol_Pos.quote_string_qq) name; fun print_properties keywords = map (apply2 (print_name keywords) #> (fn (a, b) => a ^ " = " ^ b)) #> commas #> enclose "[" "]"; (* make *) fun make ((k, n), s) pos = let val pos' = Position.shift_offsets {remove_id = false} n pos; val range = Position.range (pos, pos'); val tok = if 0 <= k andalso k < Vector.length immediate_kinds then Token ((s, range), (Vector.nth immediate_kinds k, s), Slot) else (case explode Keyword.empty_keywords pos s of [tok] => tok | _ => Token ((s, range), (Error (err_prefix ^ "exactly one token expected"), s), Slot)) in (tok, pos') end; fun make_string (s, pos) = let val Token ((x, _), y, z) = #1 (make ((~1, 0), Symbol_Pos.quote_string_qq s) Position.none); val pos' = Position.no_range_position pos; in Token ((x, (pos', pos')), y, z) end; fun make_string0 s = make_string (s, Position.none); val make_int = explode Keyword.empty_keywords Position.none o signed_string_of_int; fun make_src a args = make_string a :: args; (** parsers **) type 'a parser = T list -> 'a * T list; type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list); (* wrapped syntax *) fun syntax_generic scan src0 context = let val src = map (transfer (Context.theory_of context)) src0; val (name, pos) = name_of_src src; val old_reports = maps reports_of_value src; val args1 = map init_assignable (args_of_src src); fun reported_text () = if Context_Position.reports_enabled_generic context then let val new_reports = maps (reports_of_value o closure) args1 in if old_reports <> new_reports then map (fn (p, m) => Position.reported_text p m "") new_reports else [] end else []; in (case Scan.error (Scan.finite' stopper (Scan.option scan)) (context, args1) of (SOME x, (context', [])) => let val _ = Output.report (reported_text ()) in (x, context') end | (_, (context', args2)) => let val print_name = (case get_name (hd src) of NONE => quote name | SOME {kind, print, ...} => let val ctxt' = Context.proof_of context'; val (markup, xname) = print ctxt'; in plain_words kind ^ " " ^ quote (Markup.markup markup xname) end); val print_args = if null args2 then "" else ":\n " ^ space_implode " " (map print args2); in error ("Bad arguments for " ^ print_name ^ Position.here pos ^ print_args ^ Markup.markup_report (implode (reported_text ()))) end) end; fun syntax scan src = apsnd Context.the_proof o syntax_generic scan src o Context.Proof; +fun read ctxt scan src = syntax (Scan.lift scan) src ctxt |> #1; + end; type 'a parser = 'a Token.parser; type 'a context_parser = 'a Token.context_parser; diff --git a/src/Pure/ML/ml_antiquotation.ML b/src/Pure/ML/ml_antiquotation.ML --- a/src/Pure/ML/ml_antiquotation.ML +++ b/src/Pure/ML/ml_antiquotation.ML @@ -1,118 +1,118 @@ (* Title: Pure/ML/ml_antiquotation.ML Author: Makarius ML antiquotations. *) signature ML_ANTIQUOTATION = sig val value_decl: string -> string -> Proof.context -> (Proof.context -> string * string) * Proof.context val declaration: binding -> 'a context_parser -> (Token.src -> 'a -> Proof.context -> (Proof.context -> string * string) * Proof.context) -> theory -> theory val declaration_embedded: binding -> 'a context_parser -> (Token.src -> 'a -> Proof.context -> (Proof.context -> string * string) * Proof.context) -> theory -> theory val inline: binding -> string context_parser -> theory -> theory val inline_embedded: binding -> string context_parser -> theory -> theory val value: binding -> string context_parser -> theory -> theory val value_embedded: binding -> string context_parser -> theory -> theory val special_form: binding -> string -> theory -> theory val conditional: binding -> (Proof.context -> bool) -> theory -> theory end; structure ML_Antiquotation: ML_ANTIQUOTATION = struct (* define antiquotations *) fun value_decl a s ctxt = let val (b, ctxt') = ML_Context.variant a ctxt; val env = "val " ^ b ^ " = " ^ s ^ ";\n"; val body = ML_Context.struct_name ctxt ^ "." ^ b; fun decl (_: Proof.context) = (env, body); in (decl, ctxt') end; local fun gen_declaration name embedded scan body = ML_Context.add_antiquotation name embedded (fn range => fn src => fn orig_ctxt => let val (x, _) = Token.syntax scan src orig_ctxt; val (decl, ctxt') = body src x orig_ctxt; in (decl #> apply2 (ML_Lex.tokenize_range range), ctxt') end); fun gen_inline name embedded scan = gen_declaration name embedded scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt)); fun gen_value name embedded scan = gen_declaration name embedded scan (fn _ => value_decl (Binding.name_of name)); in fun declaration name = gen_declaration name false; fun declaration_embedded name = gen_declaration name true; fun inline name = gen_inline name false; fun inline_embedded name = gen_inline name true; fun value name = gen_value name false; fun value_embedded name = gen_value name true; end; (* ML macros *) fun special_form binding operator = ML_Context.add_antiquotation binding true (fn _ => fn src => fn ctxt => let - val (s, _) = Token.syntax (Scan.lift Parse.embedded_input) src ctxt; + val s = Token.read ctxt Parse.embedded_input src; val tokenize = ML_Lex.tokenize_no_range; val tokenize_range = ML_Lex.tokenize_range (Input.range_of s); val (decl, ctxt') = ML_Context.read_antiquotes s ctxt; fun decl' ctxt'' = let val (ml_env, ml_body) = decl ctxt''; val ml_body' = tokenize "let val expr = (fn () => " @ ml_body @ tokenize ");" @ tokenize " val " @ tokenize_range "result" @ tokenize (" = " ^ operator ^ " expr; in result end"); in (ml_env, ml_body') end; in (decl', ctxt') end); fun conditional binding check = ML_Context.add_antiquotation binding true (fn _ => fn src => fn ctxt => - let val (s, _) = Token.syntax (Scan.lift Parse.embedded_input) src ctxt in + let val s = Token.read ctxt Parse.embedded_input src in if check ctxt then ML_Context.read_antiquotes s ctxt else (K ([], []), ctxt) end); (* basic antiquotations *) val _ = Theory.setup (declaration (Binding.make ("here", \<^here>)) (Scan.succeed ()) (fn src => fn () => value_decl "position" (ML_Syntax.print_position (#2 (Token.name_of_src src)))) #> inline (Binding.make ("make_string", \<^here>)) (Args.context >> K ML_Pretty.make_string_fn) #> value_embedded (Binding.make ("binding", \<^here>)) (Scan.lift Parse.embedded_input >> (ML_Syntax.make_binding o Input.source_content)) #> value_embedded (Binding.make ("cartouche", \<^here>)) (Scan.lift Args.cartouche_input >> (fn source => "Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^ ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))) #> inline_embedded (Binding.make ("verbatim", \<^here>)) (Scan.lift Parse.embedded >> ML_Syntax.print_string)); end; diff --git a/src/Pure/ML/ml_antiquotations.ML b/src/Pure/ML/ml_antiquotations.ML --- a/src/Pure/ML/ml_antiquotations.ML +++ b/src/Pure/ML/ml_antiquotations.ML @@ -1,460 +1,460 @@ (* Title: Pure/ML/ml_antiquotations.ML Author: Makarius Miscellaneous ML antiquotations. *) signature ML_ANTIQUOTATIONS = sig val make_judgment: Proof.context -> term -> term val dest_judgment: Proof.context -> term -> term end; structure ML_Antiquotations: ML_ANTIQUOTATIONS = struct (* ML support *) val _ = Theory.setup (ML_Antiquotation.inline \<^binding>\undefined\ (Scan.succeed "(raise General.Match)") #> ML_Antiquotation.inline \<^binding>\assert\ (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #> ML_Antiquotation.declaration_embedded \<^binding>\print\ (Scan.lift (Scan.optional Parse.embedded "Output.writeln")) (fn src => fn output => fn ctxt => let val struct_name = ML_Context.struct_name ctxt; val (_, pos) = Token.name_of_src src; val (a, ctxt') = ML_Context.variant "output" ctxt; val env = "val " ^ a ^ ": string -> unit =\n\ \ (" ^ output ^ ") o (fn s => s ^ Position.here (" ^ ML_Syntax.print_position pos ^ "));\n"; val body = "(fn x => (" ^ struct_name ^ "." ^ a ^ " (" ^ ML_Pretty.make_string_fn ^ " x); x))"; in (K (env, body), ctxt') end) #> ML_Antiquotation.value \<^binding>\rat\ (Scan.lift (Scan.optional (Args.$$$ "~" >> K ~1) 1 -- Parse.nat -- Scan.optional (Args.$$$ "/" |-- Parse.nat) 1) >> (fn ((sign, a), b) => "Rat.make " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int (sign * a, b))) #> ML_Antiquotation.conditional \<^binding>\if_linux\ (fn _ => ML_System.platform_is_linux) #> ML_Antiquotation.conditional \<^binding>\if_macos\ (fn _ => ML_System.platform_is_macos) #> ML_Antiquotation.conditional \<^binding>\if_windows\ (fn _ => ML_System.platform_is_windows) #> ML_Antiquotation.conditional \<^binding>\if_unix\ (fn _ => ML_System.platform_is_unix)); (* formal entities *) val _ = Theory.setup (ML_Antiquotation.value_embedded \<^binding>\system_option\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) => (Completion.check_option (Options.default ()) ctxt (name, pos) |> ML_Syntax.print_string))) #> ML_Antiquotation.value_embedded \<^binding>\theory\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) => (Theory.check {long = false} ctxt (name, pos); "Context.get_theory {long = false} (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name)) || Scan.succeed "Proof_Context.theory_of ML_context") #> ML_Antiquotation.value_embedded \<^binding>\theory_context\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) => (Theory.check {long = false} ctxt (name, pos); "Proof_Context.get_global {long = false} (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))) #> ML_Antiquotation.inline \<^binding>\context\ (Args.context >> (fn ctxt => ML_Context.struct_name ctxt ^ ".ML_context")) #> ML_Antiquotation.inline_embedded \<^binding>\typ\ (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #> ML_Antiquotation.inline_embedded \<^binding>\term\ (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> ML_Antiquotation.inline_embedded \<^binding>\prop\ (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> ML_Antiquotation.value_embedded \<^binding>\ctyp\ (Args.typ >> (fn T => "Thm.ctyp_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #> ML_Antiquotation.value_embedded \<^binding>\cterm\ (Args.term >> (fn t => "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> ML_Antiquotation.value_embedded \<^binding>\cprop\ (Args.prop >> (fn t => "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> ML_Antiquotation.inline_embedded \<^binding>\oracle_name\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) => ML_Syntax.print_string (Thm.check_oracle ctxt (name, pos))))); (* type classes *) fun class syn = Args.context -- Scan.lift Parse.embedded_inner_syntax >> (fn (ctxt, s) => Proof_Context.read_class ctxt s |> syn ? Lexicon.mark_class |> ML_Syntax.print_string); val _ = Theory.setup (ML_Antiquotation.inline_embedded \<^binding>\class\ (class false) #> ML_Antiquotation.inline_embedded \<^binding>\class_syntax\ (class true) #> ML_Antiquotation.inline_embedded \<^binding>\sort\ (Args.context -- Scan.lift Parse.embedded_inner_syntax >> (fn (ctxt, s) => ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))))); (* type constructors *) fun type_name kind check = Args.context -- Scan.lift (Parse.token Parse.embedded) >> (fn (ctxt, tok) => let val s = Token.inner_syntax_of tok; val (_, pos) = Input.source_content (Token.input_of tok); val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s; val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos); val res = (case try check (c, decl) of SOME res => res | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos)); in ML_Syntax.print_string res end); val _ = Theory.setup (ML_Antiquotation.inline_embedded \<^binding>\type_name\ (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #> ML_Antiquotation.inline_embedded \<^binding>\type_abbrev\ (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #> ML_Antiquotation.inline_embedded \<^binding>\nonterminal\ (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #> ML_Antiquotation.inline_embedded \<^binding>\type_syntax\ (type_name "type" (fn (c, _) => Lexicon.mark_type c))); (* constants *) fun const_name check = Args.context -- Scan.lift (Parse.token Parse.embedded) >> (fn (ctxt, tok) => let val s = Token.inner_syntax_of tok; val (_, pos) = Input.source_content (Token.input_of tok); val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s; val res = check (Proof_Context.consts_of ctxt, c) handle TYPE (msg, _, _) => error (msg ^ Position.here pos); in ML_Syntax.print_string res end); val _ = Theory.setup (ML_Antiquotation.inline_embedded \<^binding>\const_name\ (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #> ML_Antiquotation.inline_embedded \<^binding>\const_abbrev\ (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #> ML_Antiquotation.inline_embedded \<^binding>\const_syntax\ (const_name (fn (_, c) => Lexicon.mark_const c)) #> ML_Antiquotation.inline_embedded \<^binding>\syntax_const\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, arg) => ML_Syntax.print_string (Proof_Context.check_syntax_const ctxt arg))) #> ML_Antiquotation.inline_embedded \<^binding>\const\ (Args.context -- Scan.lift (Parse.position Parse.embedded_inner_syntax) -- Scan.optional (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] >> (fn ((ctxt, (raw_c, pos)), Ts) => let val Const (c, _) = Proof_Context.read_const {proper = true, strict = true} ctxt raw_c; val consts = Proof_Context.consts_of ctxt; val n = length (Consts.typargs consts (c, Consts.type_scheme consts c)); val _ = length Ts <> n andalso error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^ quote c ^ enclose "(" ")" (commas (replicate n "_")) ^ Position.here pos); val const = Const (c, Consts.instance consts (c, Ts)); in ML_Syntax.atomic (ML_Syntax.print_term const) end))); (* object-logic judgment *) fun make_judgment ctxt = let val const = Object_Logic.judgment_const ctxt in fn t => Const const $ t end; fun dest_judgment ctxt = let val is_judgment = Object_Logic.is_judgment ctxt; val drop_judgment = Object_Logic.drop_judgment ctxt; in fn t => if is_judgment t then drop_judgment t else raise TERM ("dest_judgment", [t]) end; val _ = Theory.setup (ML_Antiquotation.value \<^binding>\make_judgment\ (Scan.succeed "ML_Antiquotations.make_judgment ML_context") #> ML_Antiquotation.value \<^binding>\dest_judgment\ (Scan.succeed "ML_Antiquotations.dest_judgment ML_context")); (* type/term constructors *) local val keywords = Keyword.add_minor_keywords ["for", "=>"] Keyword.empty_keywords; val parse_name_args = Parse.input Parse.name -- Scan.repeat Parse.embedded_ml; val parse_for_args = Scan.optional (Parse.$$$ "for" |-- Parse.!!! (Scan.repeat1 Parse.embedded_ml)) []; fun parse_body b = if b then Parse.$$$ "=>" |-- Parse.!!! (Parse.embedded_ml >> single) else Scan.succeed []; fun is_dummy [Antiquote.Text tok] = ML_Lex.content_of tok = "_" | is_dummy _ = false; val ml = ML_Lex.tokenize_no_range; val ml_range = ML_Lex.tokenize_range; val ml_dummy = ml "_"; fun ml_enclose range x = ml "(" @ x @ ml_range range ")"; fun ml_parens x = ml "(" @ x @ ml ")"; fun ml_bracks x = ml "[" @ x @ ml "]"; fun ml_commas xs = flat (separate (ml ", ") xs); val ml_list = ml_bracks o ml_commas; val ml_string = ml o ML_Syntax.print_string; fun ml_pair (x, y) = ml_parens (ml_commas [x, y]); fun type_antiquotation binding {function} = ML_Context.add_antiquotation binding true (fn range => fn src => fn ctxt => let val ((s, type_args), fn_body) = src |> Parse.read_embedded_src ctxt keywords (parse_name_args -- parse_body function); val pos = Input.pos_of s; val Type (c, Ts) = Proof_Context.read_type_name {proper = true, strict = true} ctxt (Syntax.implode_input s); val n = length Ts; val _ = length type_args = n orelse error ("Type constructor " ^ quote (Proof_Context.markup_type ctxt c) ^ " takes " ^ string_of_int n ^ " argument(s)" ^ Position.here pos); val (decls1, ctxt1) = ML_Context.expand_antiquotes_list type_args ctxt; val (decls2, ctxt2) = ML_Context.expand_antiquotes_list fn_body ctxt1; fun decl' ctxt' = let val (ml_args_env, ml_args_body) = split_list (decls1 ctxt'); val (ml_fn_env, ml_fn_body) = split_list (decls2 ctxt'); val ml1 = ml_enclose range (ml "Term.Type " @ ml_pair (ml_string c, ml_list ml_args_body)); val ml2 = if function then ml_enclose range (ml_range range "fn " @ ml1 @ ml "=> " @ flat ml_fn_body @ ml "| T => " @ ml_range range "raise" @ ml " Term.TYPE (" @ ml_string ("Type_fn " ^ quote c) @ ml ", [T], [])") else ml1; in (flat (ml_args_env @ ml_fn_env), ml2) end; in (decl', ctxt2) end); fun const_antiquotation binding {pattern, function} = ML_Context.add_antiquotation binding true (fn range => fn src => fn ctxt => let val (((s, type_args), term_args), fn_body) = src |> Parse.read_embedded_src ctxt keywords (parse_name_args -- parse_for_args -- parse_body function); val Const (c, T) = Proof_Context.read_const {proper = true, strict = true} ctxt (Syntax.implode_input s); val consts = Proof_Context.consts_of ctxt; val type_paths = Consts.type_arguments consts c; val type_params = map Term.dest_TVar (Consts.typargs consts (c, T)); val n = length type_params; val m = length (Term.binder_types T); fun err msg = error ("Constant " ^ quote (Proof_Context.markup_const ctxt c) ^ msg ^ Position.here (Input.pos_of s)); val _ = length type_args <> n andalso err (" takes " ^ string_of_int n ^ " type argument(s)"); val _ = length term_args > m andalso Term.is_Type (Term.body_type T) andalso err (" cannot have more than " ^ string_of_int m ^ " argument(s)"); val (decls1, ctxt1) = ML_Context.expand_antiquotes_list type_args ctxt; val (decls2, ctxt2) = ML_Context.expand_antiquotes_list term_args ctxt1; val (decls3, ctxt3) = ML_Context.expand_antiquotes_list fn_body ctxt2; fun decl' ctxt' = let val (ml_args_env1, ml_args_body1) = split_list (decls1 ctxt'); val (ml_args_env2, ml_args_body2) = split_list (decls2 ctxt'); val (ml_fn_env, ml_fn_body) = split_list (decls3 ctxt'); val relevant = map is_dummy type_args ~~ type_paths; fun relevant_path is = not pattern orelse let val p = rev is in relevant |> exists (fn (u, q) => not u andalso is_prefix (op =) p q) end; val ml_typarg = the o AList.lookup (op =) (type_params ~~ ml_args_body1); fun ml_typ is (Type (d, Us)) = if relevant_path is then ml "Term.Type " @ ml_pair (ml_string d, ml_list (map_index (fn (i, U) => ml_typ (i :: is) U) Us)) else ml_dummy | ml_typ is (TVar arg) = if relevant_path is then ml_typarg arg else ml_dummy | ml_typ _ (TFree _) = raise Match; fun ml_app [] = ml "Term.Const " @ ml_pair (ml_string c, ml_typ [] T) | ml_app (u :: us) = ml "Term.$ " @ ml_pair (ml_app us, u); val ml_env = flat (ml_args_env1 @ ml_args_env2 @ ml_fn_env); val ml1 = ml_enclose range (ml_app (rev ml_args_body2)); val ml2 = if function then ml_enclose range (ml_range range "fn " @ ml1 @ ml "=> " @ flat ml_fn_body @ ml "| t => " @ ml_range range "raise" @ ml " Term.TERM (" @ ml_string ("Const_fn " ^ quote c) @ ml ", [t])") else ml1; in (ml_env, ml2) end; in (decl', ctxt3) end); val _ = Theory.setup (type_antiquotation \<^binding>\Type\ {function = false} #> type_antiquotation \<^binding>\Type_fn\ {function = true} #> const_antiquotation \<^binding>\Const\ {pattern = false, function = false} #> const_antiquotation \<^binding>\Const_\ {pattern = true, function = false} #> const_antiquotation \<^binding>\Const_fn\ {pattern = true, function = true}); in end; (* special forms for option type *) val _ = Theory.setup (ML_Antiquotation.special_form \<^binding>\try\ "Isabelle_Thread.try" #> ML_Antiquotation.special_form \<^binding>\can\ "Isabelle_Thread.can" #> ML_Context.add_antiquotation \<^binding>\if_none\ true (fn _ => fn src => fn ctxt => let - val (s, _) = Token.syntax (Scan.lift Parse.embedded_input) src ctxt; + val s = Token.read ctxt Parse.embedded_input src; val tokenize = ML_Lex.tokenize_no_range; val (decl, ctxt') = ML_Context.read_antiquotes s ctxt; fun decl' ctxt'' = let val (ml_env, ml_body) = decl ctxt''; val ml_body' = tokenize "(fn SOME x => x | NONE => " @ ml_body @ tokenize ")"; in (ml_env, ml_body') end; in (decl', ctxt') end)); (* basic combinators *) local val parameter = Parse.position Parse.nat >> (fn (n, pos) => if n > 1 then n else error ("Bad parameter: " ^ string_of_int n ^ Position.here pos)); fun indices n = map string_of_int (1 upto n); fun empty n = replicate_string n " []"; fun dummy n = replicate_string n " _"; fun vars x n = implode (map (fn a => " " ^ x ^ a) (indices n)); fun cons n = implode (map (fn a => " (x" ^ a ^ " :: xs" ^ a ^ ")") (indices n)); val tuple = enclose "(" ")" o commas; fun tuple_empty n = tuple (replicate n "[]"); fun tuple_vars x n = tuple (map (fn a => x ^ a) (indices n)); fun tuple_cons n = "(" ^ tuple_vars "x" n ^ " :: xs)" fun cons_tuple n = tuple (map (fn a => "x" ^ a ^ " :: xs" ^ a) (indices n)); in val _ = Theory.setup (ML_Antiquotation.value \<^binding>\map\ (Scan.lift parameter >> (fn n => "fn f =>\n\ \ let\n\ \ fun map _" ^ empty n ^ " = []\n\ \ | map f" ^ cons n ^ " = f" ^ vars "x" n ^ " :: map f" ^ vars "xs" n ^ "\n\ \ | map _" ^ dummy n ^ " = raise ListPair.UnequalLengths\n" ^ " in map f end")) #> ML_Antiquotation.value \<^binding>\fold\ (Scan.lift parameter >> (fn n => "fn f =>\n\ \ let\n\ \ fun fold _" ^ empty n ^ " a = a\n\ \ | fold f" ^ cons n ^ " a = fold f" ^ vars "xs" n ^ " (f" ^ vars "x" n ^ " a)\n\ \ | fold _" ^ dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^ " in fold f end")) #> ML_Antiquotation.value \<^binding>\fold_map\ (Scan.lift parameter >> (fn n => "fn f =>\n\ \ let\n\ \ fun fold_map _" ^ empty n ^ " a = ([], a)\n\ \ | fold_map f" ^ cons n ^ " a =\n\ \ let\n\ \ val (x, a') = f" ^ vars "x" n ^ " a\n\ \ val (xs, a'') = fold_map f" ^ vars "xs" n ^ " a'\n\ \ in (x :: xs, a'') end\n\ \ | fold_map _" ^ dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^ " in fold_map f end")) #> ML_Antiquotation.value \<^binding>\split_list\ (Scan.lift parameter >> (fn n => "fn list =>\n\ \ let\n\ \ fun split_list [] =" ^ tuple_empty n ^ "\n\ \ | split_list" ^ tuple_cons n ^ " =\n\ \ let val" ^ tuple_vars "xs" n ^ " = split_list xs\n\ \ in " ^ cons_tuple n ^ "end\n\ \ in split_list list end")) #> ML_Antiquotation.value \<^binding>\apply\ (Scan.lift (parameter -- Scan.option (Args.parens (Parse.position Parse.nat))) >> (fn (n, opt_index) => let val cond = (case opt_index of NONE => K true | SOME (index, index_pos) => if 1 <= index andalso index <= n then equal (string_of_int index) else error ("Bad index: " ^ string_of_int index ^ Position.here index_pos)); in "fn f => fn " ^ tuple_vars "x" n ^ " => " ^ tuple (map (fn a => (if cond a then "f x" else "x") ^ a) (indices n)) end))); end; (* outer syntax *) val _ = Theory.setup (ML_Antiquotation.value_embedded \<^binding>\keyword\ (Args.context -- Scan.lift (Parse.embedded_position || Parse.position (Parse.keyword_with (K true))) >> (fn (ctxt, (name, pos)) => if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then (Context_Position.report ctxt pos (Token.keyword_markup (true, Markup.keyword2) name); "Parse.$$$ " ^ ML_Syntax.print_string name) else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #> ML_Antiquotation.value_embedded \<^binding>\command_keyword\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) => (case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of SOME markup => (Context_Position.reports ctxt [(pos, markup), (pos, Markup.keyword1)]; ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position (name, pos)) | NONE => error ("Bad outer syntax command " ^ quote name ^ Position.here pos))))); end; diff --git a/src/Pure/Thy/term_style.ML b/src/Pure/Thy/term_style.ML --- a/src/Pure/Thy/term_style.ML +++ b/src/Pure/Thy/term_style.ML @@ -1,90 +1,90 @@ (* Title: Pure/Thy/term_style.ML Author: Florian Haftmann, TU Muenchen Styles for term printing. *) signature TERM_STYLE = sig val setup: binding -> (Proof.context -> term -> term) parser -> theory -> theory val parse: (term -> term) context_parser end; structure Term_Style: TERM_STYLE = struct (* theory data *) structure Data = Theory_Data ( type T = (Proof.context -> term -> term) parser Name_Space.table; val empty : T = Name_Space.empty_table "antiquotation_style"; fun merge data : T = Name_Space.merge_tables data; ); val get_data = Data.get o Proof_Context.theory_of; fun setup binding style thy = Data.map (#2 o Name_Space.define (Context.Theory thy) true (binding, style)) thy; (* style parsing *) fun parse_single ctxt = Parse.token Parse.name ::: Parse.args >> (fn src0 => let val (src, parse) = Token.check_src ctxt get_data src0; - val (f, _) = Token.syntax (Scan.lift parse) src ctxt; + val f = Token.read ctxt parse src; in f ctxt end); val parse = Args.context :|-- (fn ctxt => Scan.lift (Args.parens (parse_single ctxt ::: Scan.repeat (Args.$$$ "," |-- parse_single ctxt)) >> fold I || Scan.succeed I)); (* predefined styles *) fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t => let val concl = Object_Logic.drop_judgment ctxt (Logic.strip_imp_concl t); in (case concl of _ $ l $ r => proj (l, r) | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)) end); val style_prem = Parse.nat >> (fn i => fn ctxt => fn t => let val prems = Logic.strip_imp_prems t; in if i <= length prems then nth prems (i - 1) else error ("Not enough premises for prem " ^ string_of_int i ^ " in propositon: " ^ Syntax.string_of_term ctxt t) end); fun sub_symbols (d :: s :: ss) = if Symbol.is_ascii_digit d andalso not (Symbol.is_control s) then d :: "\<^sub>" :: sub_symbols (s :: ss) else d :: s :: ss | sub_symbols cs = cs; val sub_name = implode o rev o sub_symbols o rev o Symbol.explode; fun sub_term (Free (n, T)) = Free (sub_name n, T) | sub_term (Var ((n, idx), T)) = if idx <> 0 then Var ((sub_name (n ^ string_of_int idx), 0), T) else Var ((sub_name n, 0), T) | sub_term (t $ u) = sub_term t $ sub_term u | sub_term (Abs (n, T, b)) = Abs (sub_name n, T, sub_term b) | sub_term t = t; val _ = Theory.setup (setup \<^binding>\lhs\ (style_lhs_rhs fst) #> setup \<^binding>\rhs\ (style_lhs_rhs snd) #> setup \<^binding>\prem\ style_prem #> setup \<^binding>\concl\ (Scan.succeed (K Logic.strip_imp_concl)) #> setup \<^binding>\sub\ (Scan.succeed (K sub_term))); end;