diff --git a/src/HOL/Tools/Lifting/lifting_info.ML b/src/HOL/Tools/Lifting/lifting_info.ML --- a/src/HOL/Tools/Lifting/lifting_info.ML +++ b/src/HOL/Tools/Lifting/lifting_info.ML @@ -1,576 +1,576 @@ (* Title: HOL/Tools/Lifting/lifting_info.ML Author: Ondrej Kuncar Context data for the lifting package. *) signature LIFTING_INFO = sig type quot_map = {rel_quot_thm: thm} val lookup_quot_maps: Proof.context -> string -> quot_map option val print_quot_maps: Proof.context -> unit type pcr = {pcrel_def: thm, pcr_cr_eq: thm} type quotient = {quot_thm: thm, pcr_info: pcr option} val pcr_eq: pcr * pcr -> bool val quotient_eq: quotient * quotient -> bool val transform_quotient: morphism -> quotient -> quotient val lookup_quotients: Proof.context -> string -> quotient option val lookup_quot_thm_quotients: Proof.context -> thm -> quotient option val update_quotients: string -> quotient -> Context.generic -> Context.generic val delete_quotients: thm -> Context.generic -> Context.generic val print_quotients: Proof.context -> unit type restore_data = {quotient : quotient, transfer_rules: thm Item_Net.T} val lookup_restore_data: Proof.context -> string -> restore_data option val init_restore_data: string -> quotient -> Context.generic -> Context.generic val add_transfer_rules_in_restore_data: string -> thm Item_Net.T -> Context.generic -> Context.generic val get_relator_eq_onp_rules: Proof.context -> thm list val get_reflexivity_rules: Proof.context -> thm list val add_reflexivity_rule_attribute: attribute type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, pos_distr_rules: thm list, neg_distr_rules: thm list} val lookup_relator_distr_data: Proof.context -> string -> relator_distr_data option val add_no_code_type: string -> Context.generic -> Context.generic val is_no_code_type: Proof.context -> string -> bool val get_quot_maps : Proof.context -> quot_map Symtab.table val get_quotients : Proof.context -> quotient Symtab.table val get_relator_distr_data : Proof.context -> relator_distr_data Symtab.table val get_restore_data : Proof.context -> restore_data Symtab.table - val get_no_code_types : Proof.context -> unit Symtab.table + val get_no_code_types : Proof.context -> Symset.T end structure Lifting_Info: LIFTING_INFO = struct open Lifting_Util (* context data *) type quot_map = {rel_quot_thm: thm} type pcr = {pcrel_def: thm, pcr_cr_eq: thm} type quotient = {quot_thm: thm, pcr_info: pcr option} type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, pos_distr_rules: thm list, neg_distr_rules: thm list} type restore_data = {quotient : quotient, transfer_rules: thm Item_Net.T} fun pcr_eq ({pcrel_def = pcrel_def1, pcr_cr_eq = pcr_cr_eq1}, {pcrel_def = pcrel_def2, pcr_cr_eq = pcr_cr_eq2}) = Thm.eq_thm (pcrel_def1, pcrel_def2) andalso Thm.eq_thm (pcr_cr_eq1, pcr_cr_eq2) fun quotient_eq ({quot_thm = quot_thm1, pcr_info = pcr_info1}, {quot_thm = quot_thm2, pcr_info = pcr_info2}) = Thm.eq_thm (quot_thm1, quot_thm2) andalso eq_option pcr_eq (pcr_info1, pcr_info2) fun join_restore_data key (rd1:restore_data, rd2) = if pointer_eq (rd1, rd2) then raise Symtab.SAME else if not (quotient_eq (#quotient rd1, #quotient rd2)) then raise Symtab.DUP key else { quotient = #quotient rd1, transfer_rules = Item_Net.merge (#transfer_rules rd1, #transfer_rules rd2)} structure Data = Generic_Data ( type T = { quot_maps : quot_map Symtab.table, quotients : quotient Symtab.table, reflexivity_rules : thm Item_Net.T, relator_distr_data : relator_distr_data Symtab.table, restore_data : restore_data Symtab.table, - no_code_types : unit Symtab.table + no_code_types : Symset.T } val empty = { quot_maps = Symtab.empty, quotients = Symtab.empty, reflexivity_rules = Thm.item_net, relator_distr_data = Symtab.empty, restore_data = Symtab.empty, - no_code_types = Symtab.empty + no_code_types = Symset.empty } fun merge ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1, restore_data = rd1, no_code_types = nct1 }, { quot_maps = qm2, quotients = q2, reflexivity_rules = rr2, relator_distr_data = rdd2, restore_data = rd2, no_code_types = nct2 } ) = { quot_maps = Symtab.merge (K true) (qm1, qm2), quotients = Symtab.merge (K true) (q1, q2), reflexivity_rules = Item_Net.merge (rr1, rr2), relator_distr_data = Symtab.merge (K true) (rdd1, rdd2), restore_data = Symtab.join join_restore_data (rd1, rd2), - no_code_types = Symtab.merge (K true) (nct1, nct2) + no_code_types = Symset.merge (nct1, nct2) } ) fun map_data f1 f2 f3 f4 f5 f6 { quot_maps, quotients, reflexivity_rules, relator_distr_data, restore_data, no_code_types } = { quot_maps = f1 quot_maps, quotients = f2 quotients, reflexivity_rules = f3 reflexivity_rules, relator_distr_data = f4 relator_distr_data, restore_data = f5 restore_data, no_code_types = f6 no_code_types } fun map_quot_maps f = map_data f I I I I I fun map_quotients f = map_data I f I I I I fun map_reflexivity_rules f = map_data I I f I I I fun map_relator_distr_data f = map_data I I I f I I fun map_restore_data f = map_data I I I I f I fun map_no_code_types f = map_data I I I I I f val get_quot_maps' = #quot_maps o Data.get val get_quotients' = #quotients o Data.get val get_reflexivity_rules' = #reflexivity_rules o Data.get val get_relator_distr_data' = #relator_distr_data o Data.get val get_restore_data' = #restore_data o Data.get val get_no_code_types' = #no_code_types o Data.get val get_quot_maps = get_quot_maps' o Context.Proof val get_quotients = get_quotients' o Context.Proof val get_relator_distr_data = get_relator_distr_data' o Context.Proof val get_restore_data = get_restore_data' o Context.Proof val get_no_code_types = get_no_code_types' o Context.Proof (* info about Quotient map theorems *) val lookup_quot_maps = Symtab.lookup o get_quot_maps fun quot_map_thm_sanity_check rel_quot_thm ctxt = let fun quot_term_absT ctxt quot_term = let val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) quot_term handle TERM (_, [t]) => error (Pretty.string_of (Pretty.block [Pretty.str "The Quotient map theorem is not in the right form.", Pretty.brk 1, Pretty.str "The following term is not the Quotient predicate:", Pretty.brk 1, Syntax.pretty_term ctxt t])) in fastype_of abs end val ((_, [rel_quot_thm_fixed]), ctxt') = Variable.importT [rel_quot_thm] ctxt val rel_quot_thm_prop = Thm.prop_of rel_quot_thm_fixed val rel_quot_thm_concl = Logic.strip_imp_concl rel_quot_thm_prop val rel_quot_thm_prems = Logic.strip_imp_prems rel_quot_thm_prop; val concl_absT = quot_term_absT ctxt' rel_quot_thm_concl val concl_tfrees = Term.add_tfree_namesT (concl_absT) [] val prems_tfrees = fold (fn typ => fn list => Term.add_tfree_namesT (quot_term_absT ctxt' typ) list) rel_quot_thm_prems [] val extra_prem_tfrees = case subtract (op =) concl_tfrees prems_tfrees of [] => [] | extras => [Pretty.block ([Pretty.str "Extra type variables in the premises:", Pretty.brk 1] @ ((Pretty.commas o map (Pretty.str o quote)) extras) @ [Pretty.str "."])] val errs = extra_prem_tfrees in if null errs then () else error (cat_lines (["Sanity check of the quotient map theorem failed:",""] @ (map Pretty.string_of errs))) end fun add_quot_map rel_quot_thm context = let val _ = Context.cases (K ()) (quot_map_thm_sanity_check rel_quot_thm) context val rel_quot_thm_concl = (Logic.strip_imp_concl o Thm.prop_of) rel_quot_thm val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) rel_quot_thm_concl val relatorT_name = (fst o dest_Type o fst o dest_funT o fastype_of) abs val minfo = {rel_quot_thm = Thm.trim_context rel_quot_thm} in Data.map (map_quot_maps (Symtab.update (relatorT_name, minfo))) context end val _ = Theory.setup (Attrib.setup \<^binding>\quot_map\ (Scan.succeed (Thm.declaration_attribute add_quot_map)) "declaration of the Quotient map theorem") fun print_quot_maps ctxt = let fun prt_map (ty_name, {rel_quot_thm}) = Pretty.block (separate (Pretty.brk 2) [Pretty.str "type:", Pretty.str ty_name, Pretty.str "quot. theorem:", Syntax.pretty_term ctxt (Thm.prop_of rel_quot_thm)]) in map prt_map (Symtab.dest (get_quot_maps ctxt)) |> Pretty.big_list "maps for type constructors:" |> Pretty.writeln end (* info about quotient types *) fun transform_pcr_info phi {pcrel_def, pcr_cr_eq} = {pcrel_def = Morphism.thm phi pcrel_def, pcr_cr_eq = Morphism.thm phi pcr_cr_eq} fun transform_quotient phi {quot_thm, pcr_info} = {quot_thm = Morphism.thm phi quot_thm, pcr_info = Option.map (transform_pcr_info phi) pcr_info} fun lookup_quotients ctxt type_name = Symtab.lookup (get_quotients ctxt) type_name |> Option.map (transform_quotient (Morphism.transfer_morphism' ctxt)) fun lookup_quot_thm_quotients ctxt quot_thm = let val (_, qtyp) = quot_thm_rty_qty quot_thm val qty_full_name = (fst o dest_Type) qtyp fun compare_data (data:quotient) = Thm.eq_thm_prop (#quot_thm data, quot_thm) in case lookup_quotients ctxt qty_full_name of SOME quotient => if compare_data quotient then SOME quotient else NONE | NONE => NONE end fun update_quotients type_name qinfo context = let val qinfo' = transform_quotient Morphism.trim_context_morphism qinfo in Data.map (map_quotients (Symtab.update (type_name, qinfo'))) context end fun delete_quotients quot_thm context = let val (_, qtyp) = quot_thm_rty_qty quot_thm val qty_full_name = (fst o dest_Type) qtyp in if is_some (lookup_quot_thm_quotients (Context.proof_of context) quot_thm) then Data.map (map_quotients (Symtab.delete qty_full_name)) context else context end fun print_quotients ctxt = let fun prt_quot (qty_name, {quot_thm, pcr_info}: quotient) = Pretty.block (separate (Pretty.brk 2) ([Pretty.str "type:", Pretty.str qty_name, Pretty.str "quot thm:", Thm.pretty_thm ctxt quot_thm] @ (case pcr_info of NONE => [] | SOME {pcrel_def, pcr_cr_eq, ...} => [Pretty.str "pcrel_def thm:", Thm.pretty_thm ctxt pcrel_def, Pretty.str "pcr_cr_eq thm:", Thm.pretty_thm ctxt pcr_cr_eq]))) in map prt_quot (Symtab.dest (get_quotients ctxt)) |> Pretty.big_list "quotients:" |> Pretty.writeln end val _ = Theory.setup (Attrib.setup \<^binding>\quot_del\ (Scan.succeed (Thm.declaration_attribute delete_quotients)) "deletes the Quotient theorem") (* data for restoring Transfer/Lifting context *) fun lookup_restore_data ctxt bundle_name = Symtab.lookup (get_restore_data ctxt) bundle_name fun update_restore_data bundle_name restore_data context = Data.map (map_restore_data (Symtab.update (bundle_name, restore_data))) context fun init_restore_data bundle_name qinfo context = update_restore_data bundle_name { quotient = qinfo, transfer_rules = Thm.item_net } context fun add_transfer_rules_in_restore_data bundle_name transfer_rules context = (case Symtab.lookup (get_restore_data' context) bundle_name of SOME restore_data => update_restore_data bundle_name { quotient = #quotient restore_data, transfer_rules = Item_Net.merge ((#transfer_rules restore_data), transfer_rules) } context | NONE => error ("The restore data " ^ quote bundle_name ^ " is not defined.")) (* theorems that a relator of an eq_onp is an eq_onp of the corresponding predicate *) fun get_relator_eq_onp_rules ctxt = map safe_mk_meta_eq (rev (Named_Theorems.get ctxt \<^named_theorems>\relator_eq_onp\)) (* info about reflexivity rules *) fun get_reflexivity_rules ctxt = Item_Net.content (get_reflexivity_rules' (Context.Proof ctxt)) |> map (Thm.transfer' ctxt) fun add_reflexivity_rule thm = Data.map (map_reflexivity_rules (Item_Net.update (Thm.trim_context thm))) val add_reflexivity_rule_attribute = Thm.declaration_attribute add_reflexivity_rule (* info about relator distributivity theorems *) fun map_relator_distr_data' f1 f2 f3 f4 {pos_mono_rule, neg_mono_rule, pos_distr_rules, neg_distr_rules} = {pos_mono_rule = f1 pos_mono_rule, neg_mono_rule = f2 neg_mono_rule, pos_distr_rules = f3 pos_distr_rules, neg_distr_rules = f4 neg_distr_rules} fun map_pos_mono_rule f = map_relator_distr_data' f I I I fun map_neg_mono_rule f = map_relator_distr_data' I f I I fun map_pos_distr_rules f = map_relator_distr_data' I I f I fun map_neg_distr_rules f = map_relator_distr_data' I I I f fun introduce_polarities rule = let val dest_less_eq = HOLogic.dest_bin \<^const_name>\less_eq\ dummyT val prems_pairs = map (dest_less_eq o HOLogic.dest_Trueprop) (Thm.prems_of rule) val equal_prems = filter op= prems_pairs val _ = if null equal_prems then () else error "The rule contains reflexive assumptions." val concl_pairs = rule |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_less_eq |> apply2 (snd o strip_comb) |> op ~~ |> filter_out op = val _ = if has_duplicates op= concl_pairs then error "The rule contains duplicated variables in the conlusion." else () fun rewrite_prem prem_pair = if member op= concl_pairs prem_pair then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm POS_def})) else if member op= concl_pairs (swap prem_pair) then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm NEG_def})) else error "The rule contains a non-relevant assumption." fun rewrite_prems [] = Conv.all_conv | rewrite_prems (x::xs) = Conv.implies_conv (rewrite_prem x) (rewrite_prems xs) val rewrite_prems_conv = rewrite_prems prems_pairs val rewrite_concl_conv = Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm POS_def}))) in (Conv.fconv_rule (rewrite_prems_conv then_conv rewrite_concl_conv)) rule end handle TERM _ => error "The rule has a wrong format." | CTERM _ => error "The rule has a wrong format." fun negate_mono_rule mono_rule = let val rewr_conv = HOLogic.Trueprop_conv (Conv.rewrs_conv [@{thm POS_NEG}, @{thm NEG_POS}]) in Conv.fconv_rule (Conv.prems_conv ~1 rewr_conv then_conv Conv.concl_conv ~1 rewr_conv) mono_rule end; fun add_reflexivity_rules mono_rule context = let val ctxt = Context.proof_of context val thy = Context.theory_of context fun find_eq_rule thm = let val concl_rhs = (hd o get_args 1 o HOLogic.dest_Trueprop o Thm.concl_of) thm val rules = Transfer.retrieve_relator_eq ctxt concl_rhs in find_first (fn th => Pattern.matches thy (concl_rhs, (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.concl_of) th)) rules end val eq_rule = find_eq_rule mono_rule; val eq_rule = if is_some eq_rule then the eq_rule else error "No corresponding rule that the relator preserves equality was found." in context |> add_reflexivity_rule (Drule.zero_var_indexes (@{thm ord_le_eq_trans} OF [mono_rule, eq_rule])) |> add_reflexivity_rule (Drule.zero_var_indexes (@{thm ord_eq_le_trans} OF [sym OF [eq_rule], mono_rule])) end fun add_mono_rule mono_rule context = let val pol_mono_rule = introduce_polarities mono_rule val mono_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o dest_Const o head_of o HOLogic.dest_Trueprop o Thm.concl_of) pol_mono_rule in if Symtab.defined (get_relator_distr_data' context) mono_ruleT_name then (if Context_Position.is_visible_generic context then warning ("Monotonicity rule for type " ^ quote mono_ruleT_name ^ " is already_defined.") else (); context) else let val neg_mono_rule = negate_mono_rule pol_mono_rule val relator_distr_data = {pos_mono_rule = pol_mono_rule, neg_mono_rule = neg_mono_rule, pos_distr_rules = [], neg_distr_rules = []} in context |> Data.map (map_relator_distr_data (Symtab.update (mono_ruleT_name, relator_distr_data))) |> add_reflexivity_rules mono_rule end end; local fun add_distr_rule update_entry distr_rule context = let val distr_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o dest_Const o head_of o HOLogic.dest_Trueprop o Thm.concl_of) distr_rule in if Symtab.defined (get_relator_distr_data' context) distr_ruleT_name then Data.map (map_relator_distr_data (Symtab.map_entry distr_ruleT_name (update_entry distr_rule))) context else error "The monotonicity rule is not defined." end fun rewrite_concl_conv thm ctm = Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric thm))) ctm handle CTERM _ => error "The rule has a wrong format." in fun add_pos_distr_rule distr_rule context = let val distr_rule = Conv.fconv_rule (rewrite_concl_conv @{thm POS_def}) distr_rule fun update_entry distr_rule data = map_pos_distr_rules (cons (@{thm POS_trans} OF [distr_rule, #pos_mono_rule data])) data in add_distr_rule update_entry distr_rule context end handle THM _ => error "Combining of the distr. rule and the monotonicity rule together has failed." fun add_neg_distr_rule distr_rule context = let val distr_rule = Conv.fconv_rule (rewrite_concl_conv @{thm NEG_def}) distr_rule fun update_entry distr_rule data = map_neg_distr_rules (cons (@{thm NEG_trans} OF [distr_rule, #neg_mono_rule data])) data in add_distr_rule update_entry distr_rule context end handle THM _ => error "Combining of the distr. rule and the monotonicity rule together has failed." end local val eq_refl2 = sym RS @{thm eq_refl} in fun add_eq_distr_rule distr_rule context = let val pos_distr_rule = @{thm eq_refl} OF [distr_rule] val neg_distr_rule = eq_refl2 OF [distr_rule] in context |> add_pos_distr_rule pos_distr_rule |> add_neg_distr_rule neg_distr_rule end end; local fun sanity_check rule = let val assms = map (perhaps (try HOLogic.dest_Trueprop)) (Thm.prems_of rule) val concl = (perhaps (try HOLogic.dest_Trueprop)) (Thm.concl_of rule); val (lhs, rhs) = (case concl of Const (\<^const_name>\less_eq\, _) $ (lhs as Const (\<^const_name>\relcompp\,_) $ _ $ _) $ rhs => (lhs, rhs) | Const (\<^const_name>\less_eq\, _) $ rhs $ (lhs as Const (\<^const_name>\relcompp\,_) $ _ $ _) => (lhs, rhs) | Const (\<^const_name>\HOL.eq\, _) $ (lhs as Const (\<^const_name>\relcompp\,_) $ _ $ _) $ rhs => (lhs, rhs) | _ => error "The rule has a wrong format.") val lhs_vars = Term.add_vars lhs [] val rhs_vars = Term.add_vars rhs [] val assms_vars = fold Term.add_vars assms []; val _ = if has_duplicates op= lhs_vars then error "Left-hand side has variable duplicates" else () val _ = if subset op= (rhs_vars, lhs_vars) then () else error "Extra variables in the right-hand side of the rule" val _ = if subset op= (assms_vars, lhs_vars) then () else error "Extra variables in the assumptions of the rule" val rhs_args = (snd o strip_comb) rhs; fun check_comp t = (case t of Const (\<^const_name>\relcompp\, _) $ Var _ $ Var _ => () | _ => error "There is an argument on the rhs that is not a composition.") val _ = map check_comp rhs_args in () end in fun add_distr_rule distr_rule context = let val _ = sanity_check distr_rule val concl = (perhaps (try HOLogic.dest_Trueprop)) (Thm.concl_of distr_rule) in (case concl of Const (\<^const_name>\less_eq\, _) $ (Const (\<^const_name>\relcompp\,_) $ _ $ _) $ _ => add_pos_distr_rule distr_rule context | Const (\<^const_name>\less_eq\, _) $ _ $ (Const (\<^const_name>\relcompp\,_) $ _ $ _) => add_neg_distr_rule distr_rule context | Const (\<^const_name>\HOL.eq\, _) $ (Const (\<^const_name>\relcompp\,_) $ _ $ _) $ _ => add_eq_distr_rule distr_rule context) end end fun get_distr_rules_raw context = Symtab.fold (fn (_, {pos_distr_rules, neg_distr_rules, ...}) => fn rules => pos_distr_rules @ neg_distr_rules @ rules) (get_relator_distr_data' context) [] |> map (Thm.transfer'' context) fun get_mono_rules_raw context = Symtab.fold (fn (_, {pos_mono_rule, neg_mono_rule, ...}) => fn rules => [pos_mono_rule, neg_mono_rule] @ rules) (get_relator_distr_data' context) [] |> map (Thm.transfer'' context) val lookup_relator_distr_data = Symtab.lookup o get_relator_distr_data val _ = Theory.setup (Attrib.setup \<^binding>\relator_mono\ (Scan.succeed (Thm.declaration_attribute add_mono_rule)) "declaration of relator's monotonicity" #> Attrib.setup \<^binding>\relator_distr\ (Scan.succeed (Thm.declaration_attribute add_distr_rule)) "declaration of relator's distributivity over OO" #> Global_Theory.add_thms_dynamic (\<^binding>\relator_distr_raw\, get_distr_rules_raw) #> Global_Theory.add_thms_dynamic (\<^binding>\relator_mono_raw\, get_mono_rules_raw)) (* no_code types *) fun add_no_code_type type_name context = - Data.map (map_no_code_types (Symtab.update (type_name, ()))) context; + Data.map (map_no_code_types (Symset.insert type_name)) context; -fun is_no_code_type context type_name = (Symtab.defined o get_no_code_types) context type_name +fun is_no_code_type context type_name = (Symset.member o get_no_code_types) context type_name (* setup fixed eq_onp rules *) val _ = Context.>> (fold (Named_Theorems.add_thm \<^named_theorems>\relator_eq_onp\ o Transfer.prep_transfer_domain_thm \<^context>) @{thms composed_equiv_rel_eq_onp composed_equiv_rel_eq_eq_onp}) (* setup fixed reflexivity rules *) val _ = Context.>> (fold add_reflexivity_rule @{thms order_refl[of "(=)"] eq_onp_le_eq Quotient_composition_le_eq Quotient_composition_ge_eq bi_unique_OO bi_total_OO right_unique_OO right_total_OO left_unique_OO left_total_OO}) (* outer syntax commands *) val _ = Outer_Syntax.command \<^command_keyword>\print_quot_maps\ "print quotient map functions" (Scan.succeed (Toplevel.keep (print_quot_maps o Toplevel.context_of))) val _ = Outer_Syntax.command \<^command_keyword>\print_quotients\ "print quotients" (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of))) end diff --git a/src/HOL/Tools/Mirabelle/mirabelle.ML b/src/HOL/Tools/Mirabelle/mirabelle.ML --- a/src/HOL/Tools/Mirabelle/mirabelle.ML +++ b/src/HOL/Tools/Mirabelle/mirabelle.ML @@ -1,356 +1,356 @@ (* Title: HOL/Tools/Mirabelle/mirabelle.ML Author: Jasmin Blanchette, TU Munich Author: Sascha Boehme, TU Munich Author: Makarius Author: Martin Desharnais, UniBw Munich *) signature MIRABELLE = sig (*core*) type action_context = {index: int, label: string, name: string, arguments: Properties.T, timeout: Time.time, output_dir: Path.T} type command = {theory_index: int, name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state} type action = {run: command -> string, finalize: unit -> string} val register_action: string -> (action_context -> string * action) -> unit (*utility functions*) val print_exn: exn -> string val can_apply : Time.time -> (Proof.context -> int -> tactic) -> Proof.state -> bool val theorems_in_proof_term : theory -> thm -> thm list val theorems_of_sucessful_proof: Toplevel.state -> thm list val get_argument : (string * string) list -> string * string -> string val get_int_argument : (string * string) list -> string * int -> int val get_bool_argument : (string * string) list -> string * bool -> bool val cpu_time : ('a -> 'b) -> 'a -> 'b * int end structure Mirabelle : MIRABELLE = struct (** Mirabelle core **) (* concrete syntax *) fun read_actions str = let val thy = \<^theory>; val ctxt = Proof_Context.init_global thy val keywords = Keyword.no_major_keywords (Thy_Header.get_keywords thy) fun read_actions () = Parse.read_embedded ctxt keywords (Parse.enum ";" (Parse.name -- Sledgehammer_Commands.parse_params)) (Input.string str) fun split_name_label (name, args) labels = (case String.tokens (fn c => c = #".") name of [name] => (("", name, args), labels) | [label, name] => - (if Symtab.defined labels label then + (if Symset.member labels label then error ("Action label '" ^ label ^ "' already defined.") else (); - ((label, name, args), Symtab.insert_set label labels)) + ((label, name, args), Symset.insert label labels)) | _ => error "Cannot parse action") in try read_actions () - |> Option.map (fn xs => fst (fold_map split_name_label xs Symtab.empty)) + |> Option.map (fn xs => fst (fold_map split_name_label xs Symset.empty)) end (* actions *) type command = {theory_index: int, name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state}; type action_context = {index: int, label: string, name: string, arguments: Properties.T, timeout: Time.time, output_dir: Path.T}; type action = {run: command -> string, finalize: unit -> string}; val dry_run_action : action = {run = K "", finalize = K ""} local val actions = Synchronized.var "Mirabelle.actions" (Symtab.empty : (action_context -> string * action) Symtab.table); in fun register_action name make_action = (if name = "" then error "Registering unnamed Mirabelle action" else (); Synchronized.change actions (Symtab.map_default (name, make_action) (fn f => (warning ("Redefining Mirabelle action: " ^ quote name); f)))); fun get_action name = Symtab.lookup (Synchronized.value actions) name; end (* apply actions *) fun print_exn exn = (case exn of Timeout.TIMEOUT _ => "timeout" | ERROR msg => "error: " ^ msg | exn => "exception: " ^ General.exnMessage exn); fun run_action_function f = f () handle exn => if Exn.is_interrupt exn then Exn.reraise exn else print_exn exn; fun make_action_path ({index, label, name, ...} : action_context) = Path.basic (if label = "" then string_of_int index ^ "." ^ name else label); fun initialize_action (make_action : action_context -> string * action) context = let val (s, action) = make_action context val action_path = make_action_path context; val export_name = Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "initialize"); val () = if s <> "" then Export.export \<^theory> export_name [XML.Text s] else () in action end fun finalize_action ({finalize, ...} : action) context = let val s = run_action_function finalize; val action_path = make_action_path context; val export_name = Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "finalize"); in if s <> "" then Export.export \<^theory> export_name [XML.Text s] else () end fun apply_action ({run, ...} : action) context (command as {pos, pre, ...} : command) = let val thy = Proof.theory_of pre; val action_path = make_action_path context; val goal_name_path = Path.basic (#name command) val line_path = Path.basic (string_of_int (the (Position.line_of pos))); val offset_path = Path.basic (string_of_int (the (Position.offset_of pos))); val ({elapsed, ...}, s) = Timing.timing run_action_function (fn () => run command); val export_name = Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "goal" + goal_name_path + line_path + offset_path + Path.basic (string_of_int (Time.toMilliseconds elapsed))); in Export.export thy export_name [XML.Text s] end; (* theory line range *) local val theory_name = Scan.many1 (Symbol_Pos.symbol #> (fn s => Symbol.not_eof s andalso s <> "[")) >> Symbol_Pos.content; val line = Symbol_Pos.scan_nat >> (Symbol_Pos.content #> Value.parse_nat); val end_line = Symbol_Pos.$$ ":" |-- line; val range = Symbol_Pos.$$ "[" |-- line -- Scan.option end_line --| Symbol_Pos.$$ "]"; in fun read_theory_range str = (case Scan.read Symbol_Pos.stopper (theory_name -- Scan.option range) (Symbol_Pos.explode0 str) of SOME res => res | NONE => error ("Malformed specification of theory line range: " ^ quote str)); end; fun check_theories strs = let fun theory_import_name s = #theory_name (Resources.import_name (Session.get_name ()) Path.current s); val theories = map read_theory_range strs |> map (apfst theory_import_name); fun get_theory name = if null theories then SOME NONE else get_first (fn (a, b) => if a = name then SOME b else NONE) theories; fun check_line NONE _ = false | check_line _ NONE = true | check_line (SOME NONE) _ = true | check_line (SOME (SOME (line, NONE))) (SOME i) = line <= i | check_line (SOME (SOME (line, SOME end_line))) (SOME i) = line <= i andalso i <= end_line; fun check_pos range = check_line range o Position.line_of; in check_pos o get_theory end; (* presentation hook *) val whitelist = ["apply", "by", "proof", "unfolding", "using"]; val _ = Build.add_hook (fn qualifier => fn loaded_theories => let val mirabelle_actions = Options.default_string \<^system_option>\mirabelle_actions\; val actions = (case read_actions mirabelle_actions of SOME actions => actions | NONE => error ("Failed to parse mirabelle_actions: " ^ quote mirabelle_actions)); in if null actions then () else let val mirabelle_dry_run = Options.default_bool \<^system_option>\mirabelle_dry_run\; val mirabelle_timeout = Options.default_seconds \<^system_option>\mirabelle_timeout\; val mirabelle_stride = Options.default_int \<^system_option>\mirabelle_stride\; val mirabelle_max_calls = Options.default_int \<^system_option>\mirabelle_max_calls\; val mirabelle_randomize = Options.default_int \<^system_option>\mirabelle_randomize\; val mirabelle_theories = Options.default_string \<^system_option>\mirabelle_theories\; val mirabelle_output_dir = Options.default_string \<^system_option>\mirabelle_output_dir\; val check_theory = check_theories (space_explode "," mirabelle_theories); fun make_commands (thy_index, (thy, segments)) = let val thy_long_name = Context.theory_long_name thy; val check_thy = check_theory thy_long_name; fun make_command {command = tr, prev_state = st, state = st', ...} = let val name = Toplevel.name_of tr; val pos = Toplevel.pos_of tr; in if Context.proper_subthy (\<^theory>, thy) andalso can (Proof.assert_backward o Toplevel.proof_of) st andalso member (op =) whitelist name andalso check_thy pos then SOME {theory_index = thy_index, name = name, pos = pos, pre = Toplevel.proof_of st, post = st'} else NONE end; in if Resources.theory_qualifier thy_long_name = qualifier then map_filter make_command segments else [] end; (* initialize actions *) val contexts = actions |> map_index (fn (n, (label, name, args)) => let val make_action = (case get_action name of SOME f => f | NONE => error "Unknown action"); val action_subdir = if label = "" then string_of_int n ^ "." ^ name else label; val output_dir = Path.append (Path.explode mirabelle_output_dir) (Path.basic action_subdir); val context = {index = n, label = label, name = name, arguments = args, timeout = mirabelle_timeout, output_dir = output_dir}; in (initialize_action make_action context, context) end); in (* run actions on all relevant goals *) loaded_theories |> map_index I |> maps make_commands |> (if mirabelle_randomize <= 0 then I else fst o MLCG.shuffle (MLCG.initialize mirabelle_randomize)) |> (fn xs => fold_map (fn x => fn i => ((i, x), i + 1)) xs 0) |> (fn (indexed_commands, commands_length) => let val stride = if mirabelle_stride <= 0 then Integer.max 1 (commands_length div mirabelle_max_calls) else mirabelle_stride in maps (fn (n, command) => let val (m, k) = Integer.div_mod (n + 1) stride in if k = 0 andalso (mirabelle_max_calls <= 0 orelse m <= mirabelle_max_calls) then map (fn context => (context, command)) contexts else [] end) indexed_commands end) (* Don't use multithreading for a dry run because of the high per-thread overhead. *) |> (if mirabelle_dry_run then map else Par_List.map) (fn ((action, context), command) => apply_action (if mirabelle_dry_run then dry_run_action else action) context command); (* finalize actions *) List.app (uncurry finalize_action) contexts end end); (* Mirabelle utility functions *) fun can_apply time tac st = let val {context = ctxt, facts, goal} = Proof.goal st; val full_tac = HEADGOAL (Method.insert_tac ctxt facts THEN' tac ctxt); in (case try (Timeout.apply time (Seq.pull o full_tac)) goal of SOME (SOME _) => true | _ => false) end; local fun fold_body_thms f = let fun app n (PBody {thms, ...}) = thms |> fold (fn (i, thm_node) => fn (x, seen) => if Inttab.defined seen i then (x, seen) else let val name = Proofterm.thm_node_name thm_node; val prop = Proofterm.thm_node_prop thm_node; val body = Future.join (Proofterm.thm_node_body thm_node); val (x', seen') = app (n + (if name = "" then 0 else 1)) body (x, Inttab.update (i, ()) seen); in (x' |> n = 0 ? f (name, prop, body), seen') end); in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end; in fun theorems_in_proof_term thy thm = let val all_thms = Global_Theory.all_thms_of thy true; fun collect (s, _, _) = if s <> "" then insert (op =) s else I; fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE; fun resolve_thms names = map_filter (member_of names) all_thms; in resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) end; end; fun theorems_of_sucessful_proof st = (case try Toplevel.proof_of st of NONE => [] | SOME prf => theorems_in_proof_term (Proof.theory_of prf) (#goal (Proof.goal prf))); fun get_argument arguments (key, default) = the_default default (AList.lookup (op =) arguments key); fun get_int_argument arguments (key, default) = (case Option.map Int.fromString (AList.lookup (op =) arguments key) of SOME (SOME i) => i | SOME NONE => error ("bad option: " ^ key) | NONE => default); fun get_bool_argument arguments (key, default) = (case Option.map Bool.fromString (AList.lookup (op =) arguments key) of SOME (SOME i) => i | SOME NONE => error ("bad option: " ^ key) | NONE => default); fun cpu_time f x = (* CPU time is problematics with multithreading as it refers to the per-process CPU time. *) let val ({elapsed, ...}, y) = Timing.timing f x in (y, Time.toMilliseconds elapsed) end; end diff --git a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML @@ -1,299 +1,299 @@ (* Title: HOL/Tools/Predicate_Compile/predicate_compile_data.ML Author: Lukas Bulwahn, TU Muenchen Book-keeping datastructure for the predicate compiler. *) signature PREDICATE_COMPILE_DATA = sig val ignore_consts : string list -> theory -> theory val keep_functions : string list -> theory -> theory val keep_function : theory -> string -> bool val processed_specs : theory -> string -> (string * thm list) list option val store_processed_specs : (string * (string * thm list) list) -> theory -> theory val get_specification : Predicate_Compile_Aux.options -> theory -> term -> thm list val obtain_specification_graph : Predicate_Compile_Aux.options -> theory -> term -> thm list Term_Graph.T val normalize_equation : theory -> thm -> thm end; structure Predicate_Compile_Data : PREDICATE_COMPILE_DATA = struct open Predicate_Compile_Aux; structure Data = Theory_Data ( type T = - {ignore_consts : unit Symtab.table, - keep_functions : unit Symtab.table, + {ignore_consts : Symset.T, + keep_functions : Symset.T, processed_specs : ((string * thm list) list) Symtab.table}; val empty = - {ignore_consts = Symtab.empty, - keep_functions = Symtab.empty, + {ignore_consts = Symset.empty, + keep_functions = Symset.empty, processed_specs = Symtab.empty}; fun merge ({ignore_consts = c1, keep_functions = k1, processed_specs = s1}, {ignore_consts = c2, keep_functions = k2, processed_specs = s2}) = - {ignore_consts = Symtab.merge (K true) (c1, c2), - keep_functions = Symtab.merge (K true) (k1, k2), + {ignore_consts = Symset.merge (c1, c2), + keep_functions = Symset.merge (k1, k2), processed_specs = Symtab.merge (K true) (s1, s2)} ); fun mk_data (c, k, s) = {ignore_consts = c, keep_functions = k, processed_specs = s} fun map_data f {ignore_consts = c, keep_functions = k, processed_specs = s} = mk_data (f (c, k, s)) fun ignore_consts cs = - Data.map (map_data (@{apply 3(1)} (fold (fn c => Symtab.insert (op =) (c, ())) cs))) + Data.map (map_data (@{apply 3(1)} (fold Symset.insert cs))) fun keep_functions cs = - Data.map (map_data (@{apply 3(2)} (fold (fn c => Symtab.insert (op =) (c, ())) cs))) + Data.map (map_data (@{apply 3(2)} (fold Symset.insert cs))) -fun keep_function thy = Symtab.defined (#keep_functions (Data.get thy)) +fun keep_function thy = Symset.member (#keep_functions (Data.get thy)) fun processed_specs thy = Symtab.lookup (#processed_specs (Data.get thy)) fun store_processed_specs (constname, specs) = Data.map (map_data (@{apply 3(3)} (Symtab.update_new (constname, specs)))) fun defining_term_of_introrule_term t = let val _ $ u = Logic.strip_imp_concl t in fst (strip_comb u) end (* in case pred of Const (c, T) => c | _ => raise TERM ("defining_const_of_introrule_term failed: Not a constant", [t]) end *) val defining_term_of_introrule = defining_term_of_introrule_term o Thm.prop_of fun defining_const_of_introrule th = (case defining_term_of_introrule th of Const (c, _) => c | _ => raise TERM ("defining_const_of_introrule failed: Not a constant", [Thm.prop_of th])) (*TODO*) fun is_introlike_term _ = true val is_introlike = is_introlike_term o Thm.prop_of fun check_equation_format_term (t as (Const (\<^const_name>\Pure.eq\, _) $ u $ _)) = (case strip_comb u of (Const (_, T), args) => if (length (binder_types T) = length args) then true else raise TERM ("check_equation_format_term failed: Number of arguments mismatch", [t]) | _ => raise TERM ("check_equation_format_term failed: Not a constant", [t])) | check_equation_format_term t = raise TERM ("check_equation_format_term failed: Not an equation", [t]) val check_equation_format = check_equation_format_term o Thm.prop_of fun defining_term_of_equation_term (Const (\<^const_name>\Pure.eq\, _) $ u $ _) = fst (strip_comb u) | defining_term_of_equation_term t = raise TERM ("defining_const_of_equation_term failed: Not an equation", [t]) val defining_term_of_equation = defining_term_of_equation_term o Thm.prop_of fun defining_const_of_equation th = (case defining_term_of_equation th of Const (c, _) => c | _ => raise TERM ("defining_const_of_equation failed: Not a constant", [Thm.prop_of th])) (* Normalizing equations *) fun mk_meta_equation th = (case Thm.prop_of th of Const (\<^const_name>\Trueprop\, _) $ (Const (\<^const_name>\HOL.eq\, _) $ _ $ _) => th RS @{thm eq_reflection} | _ => th) val meta_fun_cong = @{lemma "\f :: 'a::{} \ 'b::{}.f == g ==> f x == g x" by simp} fun full_fun_cong_expand th = let val (f, args) = strip_comb (fst (Logic.dest_equals (Thm.prop_of th))) val i = length (binder_types (fastype_of f)) - length args in funpow i (fn th => th RS meta_fun_cong) th end; fun declare_names s xs ctxt = let val res = Name.invent_names ctxt s xs in (res, fold Name.declare (map fst res) ctxt) end fun split_all_pairs thy th = let val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *) val ((_, [th']), _) = Variable.import true [th] ctxt val t = Thm.prop_of th' val frees = Term.add_frees t [] val freenames = Term.add_free_names t [] val nctxt = Name.make_context freenames fun mk_tuple_rewrites (x, T) nctxt = let val Ts = HOLogic.flatten_tupleT T val (xTs, nctxt') = declare_names x Ts nctxt val paths = HOLogic.flat_tupleT_paths T in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt val t' = Pattern.rewrite_term thy rewr [] t val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt)) val th''' = Local_Defs.unfold0 ctxt [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}] th'' in th''' end; fun inline_equations thy th = let val ctxt = Proof_Context.init_global thy val inline_defs = Named_Theorems.get ctxt \<^named_theorems>\code_pred_inline\ val th' = Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps inline_defs) th (*val _ = print_step options ("Inlining " ^ (Syntax.string_of_term_global thy (prop_of th)) ^ "with " ^ (commas (map ((Syntax.string_of_term_global thy) o prop_of) inline_defs)) ^" to " ^ (Syntax.string_of_term_global thy (prop_of th')))*) in th' end fun normalize_equation thy th = mk_meta_equation th |> full_fun_cong_expand |> split_all_pairs thy |> tap check_equation_format |> inline_equations thy fun normalize_intros thy th = split_all_pairs thy th |> inline_equations thy fun normalize thy th = if is_equationlike th then normalize_equation thy th else normalize_intros thy th fun get_specification options thy t = let (*val (c, T) = dest_Const t val t = Const (Axclass.unoverload_const thy (c, T), T)*) val _ = if show_steps options then tracing ("getting specification of " ^ Syntax.string_of_term_global thy t ^ " with type " ^ Syntax.string_of_typ_global thy (fastype_of t)) else () val ctxt = Proof_Context.init_global thy fun filtering th = if is_equationlike th andalso defining_const_of_equation (normalize_equation thy th) = fst (dest_Const t) then SOME (normalize_equation thy th) else if is_introlike th andalso defining_const_of_introrule th = fst (dest_Const t) then SOME th else NONE fun filter_defs ths = map_filter filtering (map (normalize thy o Thm.transfer thy) ths) val spec = (case filter_defs (Named_Theorems.get ctxt \<^named_theorems>\code_pred_def\) of [] => (case Spec_Rules.retrieve ctxt t of [] => error ("No specification for " ^ Syntax.string_of_term_global thy t) | ({rules = ths, ...} :: _) => filter_defs ths) | ths => ths) val _ = if show_intermediate_results options then tracing ("Specification for " ^ (Syntax.string_of_term_global thy t) ^ ":\n" ^ commas (map (Thm.string_of_thm_global thy) spec)) else () in spec end val logic_operator_names = [\<^const_name>\Pure.eq\, \<^const_name>\Pure.imp\, \<^const_name>\Trueprop\, \<^const_name>\Not\, \<^const_name>\HOL.eq\, \<^const_name>\HOL.implies\, \<^const_name>\All\, \<^const_name>\Ex\, \<^const_name>\HOL.conj\, \<^const_name>\HOL.disj\] fun special_cases (c, _) = member (op =) [\<^const_name>\Product_Type.Unity\, \<^const_name>\False\, \<^const_name>\Suc\, \<^const_name>\Nat.zero_nat_inst.zero_nat\, \<^const_name>\Nat.one_nat_inst.one_nat\, \<^const_name>\Orderings.less\, \<^const_name>\Orderings.less_eq\, \<^const_name>\Groups.zero\, \<^const_name>\Groups.one\, \<^const_name>\Groups.plus\, \<^const_name>\Nat.ord_nat_inst.less_eq_nat\, \<^const_name>\Nat.ord_nat_inst.less_nat\, (* FIXME @{const_name number_nat_inst.number_of_nat}, *) \<^const_name>\Num.Bit0\, \<^const_name>\Num.Bit1\, \<^const_name>\Num.One\, \<^const_name>\Int.zero_int_inst.zero_int\, \<^const_name>\List.filter\, \<^const_name>\HOL.If\, \<^const_name>\Groups.minus\] c fun obtain_specification_graph options thy t = let val ctxt = Proof_Context.init_global thy fun is_nondefining_const (c, _) = member (op =) logic_operator_names c fun has_code_pred_intros (c, _) = can (Core_Data.intros_of ctxt) c fun case_consts (c, _) = is_some (Ctr_Sugar.ctr_sugar_of_case ctxt c) fun is_datatype_constructor (x as (_, T)) = (case body_type T of Type (Tcon, _) => can (Ctr_Sugar.dest_ctr ctxt Tcon) (Const x) | _ => false) fun defiants_of specs = fold (Term.add_consts o Thm.prop_of) specs [] |> filter_out is_datatype_constructor |> filter_out is_nondefining_const |> filter_out has_code_pred_intros |> filter_out case_consts |> filter_out special_cases - |> filter_out (fn (c, _) => Symtab.defined (#ignore_consts (Data.get thy)) c) + |> filter_out (fn (c, _) => Symset.member (#ignore_consts (Data.get thy)) c) |> map (fn (c, _) => (c, Sign.the_const_constraint thy c)) |> map Const (* |> filter is_defining_constname*) fun extend t gr = if can (Term_Graph.get_node gr) t then gr else let val specs = get_specification options thy t (*val _ = print_specification options thy constname specs*) val us = defiants_of specs in gr |> Term_Graph.new_node (t, specs) |> fold extend us |> fold (fn u => Term_Graph.add_edge (t, u)) us end in extend t Term_Graph.empty end; end diff --git a/src/Pure/Concurrent/task_queue.ML b/src/Pure/Concurrent/task_queue.ML --- a/src/Pure/Concurrent/task_queue.ML +++ b/src/Pure/Concurrent/task_queue.ML @@ -1,436 +1,436 @@ (* Title: Pure/Concurrent/task_queue.ML Author: Makarius Ordered queue of grouped tasks. *) signature TASK_QUEUE = sig type group val new_group: group option -> group val group_id: group -> int val eq_group: group * group -> bool val cancel_group: group -> exn -> unit val is_canceled: group -> bool val group_status: group -> exn list val str_of_group: group -> string val str_of_groups: group -> string val urgent_pri: int type task val dummy_task: task val group_of_task: task -> group val name_of_task: task -> string val pri_of_task: task -> int val eq_task: task * task -> bool val str_of_task: task -> string val str_of_task_groups: task -> string val task_statistics: task -> Properties.T val running: task -> (unit -> 'a) -> 'a val joining: task -> (unit -> 'a) -> 'a val waiting: task -> task list -> (unit -> 'a) -> 'a type queue val empty: queue val group_tasks: queue -> group list -> task list val known_task: queue -> task -> bool val all_passive: queue -> bool val total_jobs: queue -> int val status: queue -> {ready: int, pending: int, running: int, passive: int, urgent: int} val cancel: queue -> group -> Thread.thread list val cancel_all: queue -> group list * Thread.thread list val finish: task -> queue -> bool * queue val enroll: Thread.thread -> string -> group -> queue -> task * queue val enqueue_passive: group -> string -> (unit -> bool) -> queue -> task * queue val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue val extend: task -> (bool -> bool) -> queue -> queue option val dequeue_passive: Thread.thread -> task -> queue -> bool option * queue val dequeue: Thread.thread -> bool -> queue -> (task * (bool -> bool) list) option * queue val dequeue_deps: Thread.thread -> task list -> queue -> (((task * (bool -> bool) list) option * task list) * queue) end; structure Task_Queue: TASK_QUEUE = struct val new_id = Counter.make (); (** nested groups of tasks **) (* groups *) abstype group = Group of {parent: group option, id: int, status: exn option Unsynchronized.ref} with fun make_group (parent, id, status) = Group {parent = parent, id = id, status = status}; fun new_group parent = make_group (parent, new_id (), Unsynchronized.ref NONE); fun group_id (Group {id, ...}) = id; fun eq_group (group1, group2) = group_id group1 = group_id group2; fun fold_groups f (g as Group {parent = NONE, ...}) a = f g a | fold_groups f (g as Group {parent = SOME group, ...}) a = fold_groups f group (f g a); (* group status *) local fun is_canceled_unsynchronized (Group {parent, status, ...}) = is_some (! status) orelse (case parent of NONE => false | SOME group => is_canceled_unsynchronized group); fun group_status_unsynchronized (Group {parent, status, ...}) = the_list (! status) @ (case parent of NONE => [] | SOME group => group_status_unsynchronized group); val lock = Mutex.mutex (); fun SYNCHRONIZED e = Multithreading.synchronized "group_status" lock e; in fun cancel_group (Group {status, ...}) exn = SYNCHRONIZED (fn () => Unsynchronized.change status (fn exns => SOME (Par_Exn.make (exn :: the_list exns)))); fun is_canceled group = SYNCHRONIZED (fn () => is_canceled_unsynchronized group); fun group_status group = SYNCHRONIZED (fn () => group_status_unsynchronized group); end; fun str_of_group group = (is_canceled group ? enclose "(" ")") (string_of_int (group_id group)); fun str_of_groups group = space_implode "/" (map str_of_group (rev (fold_groups cons group []))); end; (* tasks *) val urgent_pri = 1000; type timing = Time.time * Time.time * string list; (*run, wait, wait dependencies*) val timing_start = (Time.zeroTime, Time.zeroTime, []): timing; fun new_timing () = if ! Multithreading.trace < 2 then NONE else SOME (Synchronized.var "timing" timing_start); abstype task = Task of {group: group, name: string, id: int, pri: int option, timing: timing Synchronized.var option, pos: Position.T} with val dummy_task = Task {group = new_group NONE, name = "", id = 0, pri = NONE, timing = NONE, pos = Position.none}; fun new_task group name pri = Task {group = group, name = name, id = new_id (), pri = pri, timing = new_timing (), pos = Position.thread_data ()}; fun group_of_task (Task {group, ...}) = group; fun name_of_task (Task {name, ...}) = name; fun id_of_task (Task {id, ...}) = id; fun pri_of_task (Task {pri, ...}) = the_default 0 pri; fun eq_task (task1, task2) = id_of_task task1 = id_of_task task2; fun str_of_task (Task {name, id, ...}) = if name = "" then string_of_int id else string_of_int id ^ " (" ^ name ^ ")"; fun str_of_task_groups task = str_of_task task ^ " in " ^ str_of_groups (group_of_task task); fun update_timing update (Task {timing, ...}) e = Thread_Attributes.uninterruptible (fn restore_attributes => fn () => let val start = Time.now (); val result = Exn.capture (restore_attributes e) (); val t = Time.now () - start; val _ = (case timing of NONE => () | SOME var => Synchronized.change var (update t)); in Exn.release result end) (); fun task_ord (Task {id = id1, pri = pri1, ...}, Task {id = id2, pri = pri2, ...}) = prod_ord (rev_order o option_ord int_ord) int_ord ((pri1, id1), (pri2, id2)); fun task_statistics (Task {name, id, timing, pos, ...}) = let val (run, wait, wait_deps) = (case timing of NONE => timing_start | SOME var => Synchronized.value var); fun micros time = string_of_int (Time.toNanoseconds time div 1000); in [("now", Value.print_real (Time.toReal (Time.now ()))), ("task_name", name), ("task_id", Value.print_int id), ("run", micros run), ("wait", micros wait), ("wait_deps", commas wait_deps)] @ Position.properties_of pos end; end; -structure Tasks = Table(type key = task val ord = task_ord); +structure Tasks = Set(type key = task val ord = task_ord); structure Task_Graph = Graph(type key = task val ord = task_ord); (* timing *) fun running task = update_timing (fn t => fn (a, b, ds) => (a + t, b, ds)) task; fun joining task = update_timing (fn t => fn (a, b, ds) => (a - t, b, ds)) task; fun waiting task deps = update_timing (fn t => fn (a, b, ds) => (a - t, b + t, if ! Multithreading.trace > 0 then fold (insert (op =) o name_of_task) deps ds else ds)) task; (** queue of jobs and groups **) (* known group members *) -type groups = unit Tasks.table Inttab.table; +type groups = Tasks.T Inttab.table; fun get_tasks (groups: groups) gid = the_default Tasks.empty (Inttab.lookup groups gid); fun add_task (gid, task) groups = - Inttab.update (gid, Tasks.update (task, ()) (get_tasks groups gid)) groups; + Inttab.update (gid, Tasks.insert task (get_tasks groups gid)) groups; fun del_task (gid, task) groups = - let val tasks = Tasks.delete_safe task (get_tasks groups gid) in + let val tasks = Tasks.remove task (get_tasks groups gid) in if Tasks.is_empty tasks then Inttab.delete_safe gid groups else Inttab.update (gid, tasks) groups end; (* job dependency graph *) datatype job = Job of (bool -> bool) list | Running of Thread.thread | Passive of unit -> bool; type jobs = job Task_Graph.T; fun get_job (jobs: jobs) task = Task_Graph.get_node jobs task; fun set_job task job (jobs: jobs) = Task_Graph.map_node task (K job) jobs; fun add_job task dep (jobs: jobs) = Task_Graph.add_edge (dep, task) jobs handle Task_Graph.UNDEF _ => jobs; (* queue *) datatype queue = Queue of {groups: groups, jobs: jobs, urgent: int, total: int}; fun make_queue groups jobs urgent total = Queue {groups = groups, jobs = jobs, urgent = urgent, total = total}; val empty = make_queue Inttab.empty Task_Graph.empty 0 0; fun group_tasks (Queue {groups, ...}) gs = - fold (fn g => fn tasks => Tasks.merge (op =) (tasks, get_tasks groups (group_id g))) + fold (fn g => fn tasks => Tasks.merge (tasks, get_tasks groups (group_id g))) gs Tasks.empty - |> Tasks.keys; + |> Tasks.dest; fun known_task (Queue {jobs, ...}) task = can (Task_Graph.get_entry jobs) task; (* job status *) fun ready_job (task, (Job list, (deps, _))) = if Task_Graph.Keys.is_empty deps then SOME (task, rev list) else NONE | ready_job (task, (Passive abort, (deps, _))) = if Task_Graph.Keys.is_empty deps andalso is_canceled (group_of_task task) then SOME (task, [fn _ => abort ()]) else NONE | ready_job _ = NONE; fun ready_job_urgent false = ready_job | ready_job_urgent true = (fn entry as (task, _) => if pri_of_task task >= urgent_pri then ready_job entry else NONE); fun active_job (task, (Running _, _)) = SOME (task, []) | active_job arg = ready_job arg; fun all_passive (Queue {jobs, ...}) = is_none (Task_Graph.get_first active_job jobs); fun total_jobs (Queue {total, ...}) = total; (* queue status *) fun status (Queue {jobs, urgent, ...}) = let val (x, y, z, w) = Task_Graph.fold (fn (_, (job, (deps, _))) => fn (x, y, z, w) => (case job of Job _ => if Task_Graph.Keys.is_empty deps then (x + 1, y, z, w) else (x, y + 1, z, w) | Running _ => (x, y, z + 1, w) | Passive _ => (x, y, z, w + 1))) jobs (0, 0, 0, 0); in {ready = x, pending = y, running = z, passive = w, urgent = urgent} end; (** task queue operations **) (* cancel -- peers and sub-groups *) fun cancel (Queue {groups, jobs, ...}) group = let val _ = cancel_group group Exn.Interrupt; val running = - Tasks.fold (fn (task, _) => + Tasks.fold (fn task => (case get_job jobs task of Running thread => insert Thread.equal thread | _ => I)) (get_tasks groups (group_id group)) []; in running end; fun cancel_all (Queue {jobs, ...}) = let fun cancel_job (task, (job, _)) (groups, running) = let val group = group_of_task task; val _ = cancel_group group Exn.Interrupt; in (case job of Running t => (insert eq_group group groups, insert Thread.equal t running) | _ => (groups, running)) end; val running = Task_Graph.fold cancel_job jobs ([], []); in running end; (* finish *) fun finish task (Queue {groups, jobs, urgent, total}) = let val group = group_of_task task; val groups' = fold_groups (fn g => del_task (group_id g, task)) group groups; val jobs' = Task_Graph.del_node task jobs; val total' = total - 1; val maximal = Task_Graph.is_maximal jobs task; in (maximal, make_queue groups' jobs' urgent total') end; (* enroll *) fun enroll thread name group (Queue {groups, jobs, urgent, total}) = let val task = new_task group name NONE; val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups; val jobs' = jobs |> Task_Graph.new_node (task, Running thread); val total' = total + 1; in (task, make_queue groups' jobs' urgent total') end; (* enqueue *) fun enqueue_passive group name abort (Queue {groups, jobs, urgent, total}) = let val task = new_task group name NONE; val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups; val jobs' = jobs |> Task_Graph.new_node (task, Passive abort); val total' = total + 1; in (task, make_queue groups' jobs' urgent total') end; fun enqueue name group deps pri job (Queue {groups, jobs, urgent, total}) = let val task = new_task group name (SOME pri); val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups; val jobs' = jobs |> Task_Graph.new_node (task, Job [job]) |> fold (add_job task) deps; val urgent' = if pri >= urgent_pri then urgent + 1 else urgent; val total' = total + 1; in (task, make_queue groups' jobs' urgent' total') end; fun extend task job (Queue {groups, jobs, urgent, total}) = (case try (get_job jobs) task of SOME (Job list) => SOME (make_queue groups (set_job task (Job (job :: list)) jobs) urgent total) | _ => NONE); (* dequeue *) fun dequeue_passive thread task (queue as Queue {groups, jobs, urgent, total}) = (case try (get_job jobs) task of SOME (Passive _) => let val jobs' = set_job task (Running thread) jobs in (SOME true, make_queue groups jobs' urgent total) end | SOME _ => (SOME false, queue) | NONE => (NONE, queue)); fun dequeue thread urgent_only (queue as Queue {groups, jobs, urgent, total}) = if not urgent_only orelse urgent > 0 then (case Task_Graph.get_first (ready_job_urgent urgent_only) jobs of SOME (result as (task, _)) => let val jobs' = set_job task (Running thread) jobs; val urgent' = if pri_of_task task >= urgent_pri then urgent - 1 else urgent; in (SOME result, make_queue groups jobs' urgent' total) end | NONE => (NONE, queue)) else (NONE, queue); (* dequeue wrt. dynamic dependencies *) fun dequeue_deps thread deps (queue as Queue {groups, jobs, urgent, total}) = let fun ready [] rest = (NONE, rev rest) | ready (task :: tasks) rest = (case try (Task_Graph.get_entry jobs) task of NONE => ready tasks rest | SOME (_, entry) => (case ready_job (task, entry) of NONE => ready tasks (task :: rest) | some => (some, fold cons rest tasks))); fun ready_dep _ [] = NONE | ready_dep seen (task :: tasks) = - if Tasks.defined seen task then ready_dep seen tasks + if Tasks.member seen task then ready_dep seen tasks else let val entry as (_, (ds, _)) = #2 (Task_Graph.get_entry jobs task) in (case ready_job (task, entry) of - NONE => ready_dep (Tasks.update (task, ()) seen) (Task_Graph.Keys.dest ds @ tasks) + NONE => ready_dep (Tasks.insert task seen) (Task_Graph.Keys.dest ds @ tasks) | some => some) end; fun result (res as (task, _)) deps' = let val jobs' = set_job task (Running thread) jobs; val urgent' = if pri_of_task task >= urgent_pri then urgent - 1 else urgent; in ((SOME res, deps'), make_queue groups jobs' urgent' total) end; in (case ready deps [] of (SOME res, deps') => result res deps' | (NONE, deps') => (case ready_dep Tasks.empty deps' of SOME res => result res deps' | NONE => ((NONE, deps'), queue))) end; (* toplevel pretty printing *) val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_task); val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_group); end; diff --git a/src/Pure/General/change_table.ML b/src/Pure/General/change_table.ML --- a/src/Pure/General/change_table.ML +++ b/src/Pure/General/change_table.ML @@ -1,158 +1,159 @@ (* Title: Pure/General/change_table.ML Author: Makarius Generic tables with extra bookkeeping of changes relative to some common base version, subject to implicit block structure. Support for efficient join/merge of big global tables with small local updates. *) signature CHANGE_TABLE = sig structure Table: TABLE type key = Table.key exception DUP of key exception SAME type 'a T val table_of: 'a T -> 'a Table.table val empty: 'a T val is_empty: 'a T -> bool val change_base: bool -> 'a T -> 'a T val change_ignore: 'a T -> 'a T val join: (key -> 'a * 'a -> 'a) (*exception SAME*) -> 'a T * 'a T -> 'a T (*exception DUP*) val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception DUP*) val fold: (key * 'b -> 'a -> 'a) -> 'b T -> 'a -> 'a val dest: 'a T -> (key * 'a) list val lookup_key: 'a T -> key -> (key * 'a) option val lookup: 'a T -> key -> 'a option val defined: 'a T -> key -> bool val update: key * 'a -> 'a T -> 'a T val update_new: key * 'a -> 'a T -> 'a T (*exception DUP*) val map_entry: key -> ('a -> 'a) -> 'a T -> 'a T val map_default: key * 'a -> ('a -> 'a) -> 'a T -> 'a T val delete_safe: key -> 'a T -> 'a T end; functor Change_Table(Key: KEY): CHANGE_TABLE = struct structure Table = Table(Key); +structure Set = Set(Key); type key = Table.key; exception SAME = Table.SAME; exception DUP = Table.DUP; (* optional change *) datatype change = - No_Change | Change of {base: serial, depth: int, changes: Table.set option}; + No_Change | Change of {base: serial, depth: int, changes: Set.T option}; fun make_change base depth changes = Change {base = base, depth = depth, changes = changes}; fun ignore_change (Change {base, depth, changes = SOME _}) = make_change base depth NONE | ignore_change change = change; fun update_change key (Change {base, depth, changes = SOME ch}) = - make_change base depth (SOME (Table.insert (K true) (key, ()) ch)) + make_change base depth (SOME (Set.insert key ch)) | update_change _ change = change; fun base_change true No_Change = - make_change (serial ()) 0 (SOME Table.empty) + make_change (serial ()) 0 (SOME Set.empty) | base_change true (Change {base, depth, changes}) = make_change base (depth + 1) changes | base_change false (Change {base, depth, changes}) = if depth = 0 then No_Change else make_change base (depth - 1) changes | base_change false No_Change = raise Fail "Unbalanced change structure"; fun cannot_merge () = raise Fail "Cannot merge: incompatible change structure"; fun merge_change (No_Change, No_Change) = NONE | merge_change (Change change1, Change change2) = let val {base = base1, depth = depth1, changes = changes1} = change1; val {base = base2, depth = depth2, changes = changes2} = change2; val _ = if base1 = base2 andalso depth1 = depth2 then () else cannot_merge (); val (swapped, ch2) = (case (changes1, changes2) of (_, SOME ch2) => (false, ch2) | (SOME ch1, _) => (true, ch1) | _ => cannot_merge ()); in SOME (swapped, ch2, make_change base1 depth1 NONE) end | merge_change _ = cannot_merge (); (* table with changes *) datatype 'a T = Change_Table of {change: change, table: 'a Table.table}; fun table_of (Change_Table {table, ...}) = table; val empty = Change_Table {change = No_Change, table = Table.empty}; fun is_empty (Change_Table {change, table}) = (case change of No_Change => Table.is_empty table | _ => false); fun make_change_table (change, table) = Change_Table {change = change, table = table}; fun map_change_table f (Change_Table {change, table}) = make_change_table (f (change, table)); fun change_base begin = (map_change_table o apfst) (base_change begin); fun change_ignore arg = (map_change_table o apfst) ignore_change arg; (* join and merge *) fun join f (arg1, arg2) = let val Change_Table {change = change1, table = table1} = arg1; val Change_Table {change = change2, table = table2} = arg2; in if pointer_eq (change1, change2) andalso pointer_eq (table1, table2) then arg1 else if is_empty arg2 then arg1 else if is_empty arg1 then arg2 else (case merge_change (change1, change2) of NONE => make_change_table (No_Change, Table.join f (table1, table2)) | SOME (swapped, ch2, change') => let fun maybe_swap (x, y) = if swapped then (y, x) else (x, y); val (tab1, tab2) = maybe_swap (table1, table2); fun update key tab = (case Table.lookup tab2 key of NONE => tab | SOME y => (case Table.lookup tab key of NONE => Table.update (key, y) tab | SOME x => (case (SOME (f key (maybe_swap (x, y))) handle Table.SAME => NONE) of NONE => tab | SOME z => Table.update (key, z) tab))); - in make_change_table (change', Table.fold (update o #1) ch2 tab1) end) + in make_change_table (change', Set.fold update ch2 tab1) end) end; fun merge eq = join (fn key => fn xy => if eq xy then raise Table.SAME else raise Table.DUP key); (* derived operations *) fun fold f arg = Table.fold f (table_of arg); fun dest arg = Table.dest (table_of arg); fun lookup_key arg = Table.lookup_key (table_of arg); fun lookup arg = Table.lookup (table_of arg); fun defined arg = Table.defined (table_of arg); fun change_table key f = map_change_table (fn (change, table) => (update_change key change, f table)); fun update (key, x) = change_table key (Table.update (key, x)); fun update_new (key, x) = change_table key (Table.update_new (key, x)); fun map_entry key f = change_table key (Table.map_entry key f); fun map_default (key, x) f = change_table key (Table.map_default (key, x) f); fun delete_safe key = change_table key (Table.delete_safe key); end; structure Change_Table = Change_Table(type key = string val ord = fast_string_ord); diff --git a/src/Pure/General/graph.ML b/src/Pure/General/graph.ML --- a/src/Pure/General/graph.ML +++ b/src/Pure/General/graph.ML @@ -1,353 +1,354 @@ (* Title: Pure/General/graph.ML Author: Markus Wenzel and Stefan Berghofer, TU Muenchen Directed graphs. *) signature GRAPH = sig type key structure Keys: sig type T val is_empty: T -> bool val fold: (key -> 'a -> 'a) -> T -> 'a -> 'a val fold_rev: (key -> 'a -> 'a) -> T -> 'a -> 'a val dest: T -> key list end type 'a T exception DUP of key exception SAME exception UNDEF of key val empty: 'a T val is_empty: 'a T -> bool val keys: 'a T -> key list val get_first: (key * ('a * (Keys.T * Keys.T)) -> 'b option) -> 'a T -> 'b option val fold: (key * ('a * (Keys.T * Keys.T)) -> 'b -> 'b) -> 'a T -> 'b -> 'b val get_entry: 'a T -> key -> key * ('a * (Keys.T * Keys.T)) (*exception UNDEF*) val get_node: 'a T -> key -> 'a (*exception UNDEF*) val map_node: key -> ('a -> 'a) -> 'a T -> 'a T val map: (key -> 'a -> 'b) -> 'a T -> 'b T val imm_preds: 'a T -> key -> Keys.T val imm_succs: 'a T -> key -> Keys.T val immediate_preds: 'a T -> key -> key list val immediate_succs: 'a T -> key -> key list val all_preds: 'a T -> key list -> key list val all_succs: 'a T -> key list -> key list val strong_conn: 'a T -> key list list val map_strong_conn: ((key * 'a) list -> 'b list) -> 'a T -> 'b T val minimals: 'a T -> key list val maximals: 'a T -> key list val is_minimal: 'a T -> key -> bool val is_maximal: 'a T -> key -> bool val is_isolated: 'a T -> key -> bool val new_node: key * 'a -> 'a T -> 'a T (*exception DUP*) val default_node: key * 'a -> 'a T -> 'a T val del_node: key -> 'a T -> 'a T (*exception UNDEF*) val is_edge: 'a T -> key * key -> bool val add_edge: key * key -> 'a T -> 'a T (*exception UNDEF*) val del_edge: key * key -> 'a T -> 'a T (*exception UNDEF*) val restrict: (key -> bool) -> 'a T -> 'a T val dest: 'a T -> ((key * 'a) * key list) list val make: ((key * 'a) * key list) list -> 'a T (*exception DUP | UNDEF*) val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception DUP*) val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) -> 'a T * 'a T -> 'a T (*exception DUP*) val irreducible_paths: 'a T -> key * key -> key list list exception CYCLES of key list list val add_edge_acyclic: key * key -> 'a T -> 'a T (*exception UNDEF | CYCLES*) val add_deps_acyclic: key * key list -> 'a T -> 'a T (*exception UNDEF | CYCLES*) val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception CYCLES*) val topological_order: 'a T -> key list val add_edge_trans_acyclic: key * key -> 'a T -> 'a T (*exception UNDEF | CYCLES*) val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception CYCLES*) exception DEP of key * key val schedule: ((key * 'b) list -> key * 'a -> 'b) -> 'a T -> 'b list (*exception DEP*) val encode: key XML.Encode.T -> 'a XML.Encode.T -> 'a T XML.Encode.T val decode: key XML.Decode.T -> 'a XML.Decode.T -> 'a T XML.Decode.T end; functor Graph(Key: KEY): GRAPH = struct (* keys *) type key = Key.key; val eq_key = is_equal o Key.ord; structure Table = Table(Key); +structure Set = Set(Key); structure Keys = struct -abstype T = Keys of unit Table.table +abstype T = Keys of Set.T with -val empty = Keys Table.empty; -fun is_empty (Keys tab) = Table.is_empty tab; +val empty = Keys Set.empty; +fun is_empty (Keys set) = Set.is_empty set; -fun member (Keys tab) = Table.defined tab; -fun insert x (Keys tab) = Keys (Table.insert (K true) (x, ()) tab); -fun remove x (Keys tab) = Keys (Table.delete_safe x tab); +fun member (Keys set) = Set.member set; +fun insert x (Keys set) = Keys (Set.insert x set); +fun remove x (Keys set) = Keys (Set.remove x set); -fun fold f (Keys tab) = Table.fold (f o #1) tab; -fun fold_rev f (Keys tab) = Table.fold_rev (f o #1) tab; +fun fold f (Keys set) = Set.fold f set; +fun fold_rev f (Keys set) = Set.fold_rev f set; fun dest keys = fold_rev cons keys []; fun filter P keys = fold (fn x => P x ? insert x) keys empty; end; end; (* graphs *) datatype 'a T = Graph of ('a * (Keys.T * Keys.T)) Table.table; exception DUP = Table.DUP; exception UNDEF = Table.UNDEF; exception SAME = Table.SAME; val empty = Graph Table.empty; fun is_empty (Graph tab) = Table.is_empty tab; fun keys (Graph tab) = Table.keys tab; fun get_first f (Graph tab) = Table.get_first f tab; fun fold_graph f (Graph tab) = Table.fold f tab; fun get_entry (Graph tab) x = (case Table.lookup_key tab x of SOME entry => entry | NONE => raise UNDEF x); fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (#2 (get_entry G x))) tab); (* nodes *) fun get_node G = #1 o #2 o get_entry G; fun map_node x f = map_entry x (fn (i, ps) => (f i, ps)); fun map_nodes f (Graph tab) = Graph (Table.map (apfst o f) tab); (* reachability *) (*nodes reachable from xs -- topologically sorted for acyclic graphs*) fun reachable next xs = let fun reach x (rs, R) = if Keys.member R x then (rs, R) else Keys.fold_rev reach (next x) (rs, Keys.insert x R) |>> cons x; fun reachs x (rss, R) = reach x ([], R) |>> (fn rs => rs :: rss); in fold reachs xs ([], Keys.empty) end; (*immediate*) fun imm_preds G = #1 o #2 o #2 o get_entry G; fun imm_succs G = #2 o #2 o #2 o get_entry G; fun immediate_preds G = Keys.dest o imm_preds G; fun immediate_succs G = Keys.dest o imm_succs G; (*transitive*) fun all_preds G = flat o #1 o reachable (imm_preds G); fun all_succs G = flat o #1 o reachable (imm_succs G); (*strongly connected components; see: David King and John Launchbury, "Structuring Depth First Search Algorithms in Haskell"*) fun strong_conn G = rev (filter_out null (#1 (reachable (imm_preds G) (all_succs G (keys G))))); fun map_strong_conn f G = let val xss = strong_conn G; fun map' xs = fold2 (curry Table.update) xs (f (AList.make (get_node G) xs)); val tab' = Table.empty |> fold map' xss; in map_nodes (fn x => fn _ => the (Table.lookup tab' x)) G end; (* minimal and maximal elements *) fun minimals G = fold_graph (fn (m, (_, (preds, _))) => Keys.is_empty preds ? cons m) G []; fun maximals G = fold_graph (fn (m, (_, (_, succs))) => Keys.is_empty succs ? cons m) G []; fun is_minimal G x = Keys.is_empty (imm_preds G x); fun is_maximal G x = Keys.is_empty (imm_succs G x); fun is_isolated G x = is_minimal G x andalso is_maximal G x; (* node operations *) fun new_node (x, info) (Graph tab) = Graph (Table.update_new (x, (info, (Keys.empty, Keys.empty))) tab); fun default_node (x, info) (Graph tab) = Graph (Table.default (x, (info, (Keys.empty, Keys.empty))) tab); fun del_node x (G as Graph tab) = let fun del_adjacent which y = Table.map_entry y (fn (i, ps) => (i, (which (Keys.remove x) ps))); val (preds, succs) = #2 (#2 (get_entry G x)); in Graph (tab |> Table.delete x |> Keys.fold (del_adjacent apsnd) preds |> Keys.fold (del_adjacent apfst) succs) end; fun restrict pred G = fold_graph (fn (x, _) => not (pred x) ? del_node x) G G; (* edge operations *) fun is_edge G (x, y) = Keys.member (imm_succs G x) y handle UNDEF _ => false; fun add_edge (x, y) G = if is_edge G (x, y) then G else G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.insert x preds, succs))) |> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.insert y succs))); fun del_edge (x, y) G = if is_edge G (x, y) then G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.remove x preds, succs))) |> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.remove y succs))) else G; fun diff_edges G1 G2 = fold_graph (fn (x, (_, (_, succs))) => Keys.fold (fn y => not (is_edge G2 (x, y)) ? cons (x, y)) succs) G1 []; fun edges G = diff_edges G empty; (* dest and make *) fun dest G = fold_graph (fn (x, (i, (_, succs))) => cons ((x, i), Keys.dest succs)) G []; fun make entries = empty |> fold (new_node o fst) entries |> fold (fn ((x, _), ys) => fold (fn y => add_edge (x, y)) ys) entries; (* join and merge *) fun no_edges (i, _) = (i, (Keys.empty, Keys.empty)); fun join f (G1 as Graph tab1, G2 as Graph tab2) = let fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1) in if pointer_eq (G1, G2) then G1 else fold add_edge (edges G2) (Graph (Table.join join_node (tab1, Table.map (K no_edges) tab2))) end; fun gen_merge add eq (G1 as Graph tab1, G2 as Graph tab2) = let fun eq_node ((i1, _), (i2, _)) = eq (i1, i2) in if pointer_eq (G1, G2) then G1 else fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map (K no_edges) tab2))) end; fun merge eq GG = gen_merge add_edge eq GG; (* irreducible paths -- Hasse diagram *) fun irreducible_preds G X path z = let fun red x x' = is_edge G (x, x') andalso not (eq_key (x', z)); fun irreds [] xs' = xs' | irreds (x :: xs) xs' = if not (Keys.member X x) orelse eq_key (x, z) orelse member eq_key path x orelse exists (red x) xs orelse exists (red x) xs' then irreds xs xs' else irreds xs (x :: xs'); in irreds (immediate_preds G z) [] end; fun irreducible_paths G (x, y) = let val (_, X) = reachable (imm_succs G) [x]; fun paths path z = if eq_key (x, z) then cons (z :: path) else fold (paths (z :: path)) (irreducible_preds G X path z); in if eq_key (x, y) andalso not (is_edge G (x, x)) then [[]] else paths [] y [] end; (* maintain acyclic graphs *) exception CYCLES of key list list; fun add_edge_acyclic (x, y) G = if is_edge G (x, y) then G else (case irreducible_paths G (y, x) of [] => add_edge (x, y) G | cycles => raise CYCLES (map (cons x) cycles)); fun add_deps_acyclic (y, xs) = fold (fn x => add_edge_acyclic (x, y)) xs; fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG; fun topological_order G = minimals G |> all_succs G; (* maintain transitive acyclic graphs *) fun add_edge_trans_acyclic (x, y) G = add_edge_acyclic (x, y) G |> fold_product (curry add_edge) (all_preds G [x]) (all_succs G [y]); fun merge_trans_acyclic eq (G1, G2) = if pointer_eq (G1, G2) then G1 else merge_acyclic eq (G1, G2) |> fold add_edge_trans_acyclic (diff_edges G1 G2) |> fold add_edge_trans_acyclic (diff_edges G2 G1); (* schedule acyclic graph *) exception DEP of key * key; fun schedule f G = let val xs = topological_order G; val results = (xs, Table.empty) |-> fold (fn x => fn tab => let val a = get_node G x; val deps = immediate_preds G x |> map (fn y => (case Table.lookup tab y of SOME b => (y, b) | NONE => raise DEP (x, y))); in Table.update (x, f deps (x, a)) tab end); in map (the o Table.lookup results) xs end; (* XML data representation *) fun encode key info G = dest G |> let open XML.Encode in list (pair (pair key info) (list key)) end; fun decode key info body = body |> let open XML.Decode in list (pair (pair key info) (list key)) end |> make; (*final declarations of this structure!*) val map = map_nodes; val fold = fold_graph; end; structure Graph = Graph(type key = string val ord = fast_string_ord); structure String_Graph = Graph(type key = string val ord = string_ord); structure Int_Graph = Graph(type key = int val ord = int_ord); diff --git a/src/Pure/General/symbol.ML b/src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML +++ b/src/Pure/General/symbol.ML @@ -1,519 +1,519 @@ (* Title: Pure/General/symbol.ML Author: Makarius Isabelle text symbols. *) signature SYMBOL = sig type symbol = string val explode: string -> symbol list val spaces: int -> string val STX: symbol val DEL: symbol val open_: symbol val close: symbol val space: symbol val is_space: symbol -> bool val comment: symbol val cancel: symbol val latex: symbol val marker: symbol val is_char: symbol -> bool val is_utf8: symbol -> bool val is_symbolic: symbol -> bool val is_symbolic_char: symbol -> bool val is_printable: symbol -> bool val control_prefix: string val control_suffix: string val is_control: symbol -> bool val eof: symbol val is_eof: symbol -> bool val not_eof: symbol -> bool val stopper: symbol Scan.stopper val is_malformed: symbol -> bool val malformed_msg: symbol -> string val is_ascii: symbol -> bool val is_ascii_letter: symbol -> bool val is_ascii_digit: symbol -> bool val is_ascii_hex: symbol -> bool val is_ascii_quasi: symbol -> bool val is_ascii_blank: symbol -> bool val is_ascii_line_terminator: symbol -> bool val is_ascii_control: symbol -> bool val is_ascii_letdig: symbol -> bool val is_ascii_lower: symbol -> bool val is_ascii_upper: symbol -> bool val to_ascii_lower: symbol -> symbol val to_ascii_upper: symbol -> symbol val is_ascii_identifier: string -> bool val scan_ascii_id: string list -> string * string list datatype sym = Char of string | UTF8 of string | Sym of string | Control of string | Malformed of string | EOF val decode: symbol -> sym val encode: sym -> symbol datatype kind = Letter | Digit | Quasi | Blank | Other val kind: symbol -> kind val is_letter: symbol -> bool val is_digit: symbol -> bool val is_quasi: symbol -> bool val is_blank: symbol -> bool val is_control_block: symbol -> bool val has_control_block: symbol list -> bool val is_quasi_letter: symbol -> bool val is_letdig: symbol -> bool val beginning: int -> symbol list -> string val esc: symbol -> string val escape: string -> string val scanner: string -> (string list -> 'a * string list) -> symbol list -> 'a val split_words: symbol list -> string list val explode_words: string -> string list val trim_blanks: string -> string val bump_init: string -> string val bump_string: string -> string val sub: symbol val sup: symbol val bold: symbol val make_sub: string -> string val make_sup: string -> string val make_bold: string -> string val length: symbol list -> int val output: string -> Output.output * int end; structure Symbol: SYMBOL = struct (** type symbol **) (*Symbols, which are considered the smallest entities of any Isabelle string, may be of the following form: (1) ASCII: a (2) UTF-8: ä (2) regular symbols: \ (3) control symbols: \<^ident> Output is subject to the print_mode variable (default: verbatim), actual interpretation in display is up to front-end tools. *) type symbol = string; val STX = chr 2; val DEL = chr 127; val open_ = "\"; val close = "\"; val space = chr 32; fun is_space s = s = space; local val small_spaces = Vector.tabulate (65, fn i => replicate_string i space); in fun spaces n = if n < 64 then Vector.sub (small_spaces, n) else replicate_string (n div 64) (Vector.sub (small_spaces, 64)) ^ Vector.sub (small_spaces, n mod 64); end; val comment = "\"; val cancel = "\<^cancel>"; val latex = "\<^latex>"; val marker = "\<^marker>"; fun is_char s = size s = 1; fun is_utf8 s = size s > 0 andalso forall_string (fn c => ord c >= 128) s; fun raw_symbolic s = String.isPrefix "\092<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\092<^" s); fun is_symbolic s = s <> open_ andalso s <> close andalso raw_symbolic s; val is_symbolic_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~"); fun is_printable s = if is_char s then 32 <= ord s andalso ord s <= Char.ord #"~" else is_utf8 s orelse raw_symbolic s; val control_prefix = "\092<^"; val control_suffix = ">"; fun is_control s = String.isPrefix control_prefix s andalso String.isSuffix control_suffix s; (* input source control *) val eof = ""; fun is_eof s = s = eof; fun not_eof s = s <> eof; val stopper = Scan.stopper (K eof) is_eof; fun is_malformed s = String.isPrefix "\092<" s andalso not (String.isSuffix ">" s) orelse s = "\092<>" orelse s = "\092<^>"; fun malformed_msg s = "Malformed symbolic character: " ^ quote s; (* ASCII symbols *) fun is_ascii s = is_char s andalso ord s < 128; fun is_ascii_letter s = is_char s andalso (Char.ord #"A" <= ord s andalso ord s <= Char.ord #"Z" orelse Char.ord #"a" <= ord s andalso ord s <= Char.ord #"z"); fun is_ascii_digit s = is_char s andalso Char.ord #"0" <= ord s andalso ord s <= Char.ord #"9"; fun is_ascii_hex s = is_char s andalso (Char.ord #"0" <= ord s andalso ord s <= Char.ord #"9" orelse Char.ord #"A" <= ord s andalso ord s <= Char.ord #"F" orelse Char.ord #"a" <= ord s andalso ord s <= Char.ord #"f"); fun is_ascii_quasi "_" = true | is_ascii_quasi "'" = true | is_ascii_quasi _ = false; val is_ascii_blank = fn " " => true | "\t" => true | "\n" => true | "\^K" => true | "\f" => true | "\^M" => true | _ => false; val is_ascii_line_terminator = fn "\r" => true | "\n" => true | _ => false; fun is_ascii_control s = is_char s andalso ord s < 32 andalso not (is_ascii_blank s); fun is_ascii_letdig s = is_ascii_letter s orelse is_ascii_digit s orelse is_ascii_quasi s; fun is_ascii_lower s = is_char s andalso (Char.ord #"a" <= ord s andalso ord s <= Char.ord #"z"); fun is_ascii_upper s = is_char s andalso (Char.ord #"A" <= ord s andalso ord s <= Char.ord #"Z"); fun to_ascii_lower s = if is_ascii_upper s then chr (ord s + Char.ord #"a" - Char.ord #"A") else s; fun to_ascii_upper s = if is_ascii_lower s then chr (ord s + Char.ord #"A" - Char.ord #"a") else s; fun is_ascii_identifier s = size s > 0 andalso is_ascii_letter (String.substring (s, 0, 1)) andalso forall_string is_ascii_letdig s; val scan_ascii_id = Scan.one is_ascii_letter ^^ (Scan.many is_ascii_letdig >> implode); (* diagnostics *) fun beginning n cs = let val drop_blanks = drop_suffix is_ascii_blank; val all_cs = drop_blanks cs; val dots = if length all_cs > n then " ..." else ""; in (drop_blanks (take n all_cs) |> map (fn c => if is_ascii_blank c then space else c) |> implode) ^ dots end; (* symbol variants *) datatype sym = Char of string | UTF8 of string | Sym of string | Control of string | Malformed of string | EOF; fun decode s = if s = "" then EOF else if is_char s then Char s else if is_utf8 s then UTF8 s else if is_malformed s then Malformed s else if is_control s then Control (String.substring (s, 3, size s - 4)) else Sym (String.substring (s, 2, size s - 3)); fun encode (Char s) = s | encode (UTF8 s) = s | encode (Sym s) = "\092<" ^ s ^ ">" | encode (Control s) = "\092<^" ^ s ^ ">" | encode (Malformed s) = s | encode EOF = ""; (* standard symbol kinds *) local val letter_symbols = - Symtab.make_set [ + Symset.make [ "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\

", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\

", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\
", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", (*"\", sic!*) "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\" ]; in -val is_letter_symbol = Symtab.defined letter_symbols; +val is_letter_symbol = Symset.member letter_symbols; end; datatype kind = Letter | Digit | Quasi | Blank | Other; fun kind s = if is_ascii_letter s then Letter else if is_ascii_digit s then Digit else if is_ascii_quasi s then Quasi else if is_ascii_blank s then Blank else if is_char s then Other else if is_letter_symbol s then Letter else Other; fun is_letter s = kind s = Letter; fun is_digit s = kind s = Digit; fun is_quasi s = kind s = Quasi; fun is_blank s = kind s = Blank; val is_control_block = member (op =) ["\<^bsub>", "\<^esub>", "\<^bsup>", "\<^esup>"]; val has_control_block = exists is_control_block; fun is_quasi_letter s = let val k = kind s in k = Letter orelse k = Quasi end; fun is_letdig s = let val k = kind s in k = Letter orelse k = Digit orelse k = Quasi end; (* escape *) val esc = fn s => if is_char s then s else if is_utf8 s then translate_string (fn c => "\\" ^ string_of_int (ord c)) s else "\\" ^ s; val escape = implode o map esc o Symbol.explode; (** scanning through symbols **) (* scanner *) fun scanner msg scan syms = let fun message (ss, NONE) = (fn () => msg ^ ": " ^ quote (beginning 10 ss)) | message (ss, SOME msg') = (fn () => msg ^ ", " ^ msg' () ^ ": " ^ quote (beginning 10 ss)); val finite_scan = Scan.error (Scan.finite stopper (!! message scan)); in (case finite_scan syms of (result, []) => result | (_, rest) => error (message (rest, NONE) ())) end; (* space-separated words *) val scan_word = Scan.many1 is_ascii_blank >> K NONE || Scan.many1 (fn s => not (is_ascii_blank s) andalso not_eof s) >> (SOME o implode); val split_words = scanner "Bad text" (Scan.repeat scan_word >> map_filter I); val explode_words = split_words o Symbol.explode; (* blanks *) val trim_blanks = Symbol.explode #> trim is_blank #> implode; (* bump string -- treat as base 26 or base 1 numbers *) fun symbolic_end (_ :: "\<^sub>" :: _) = true | symbolic_end ("'" :: ss) = symbolic_end ss | symbolic_end (s :: _) = raw_symbolic s | symbolic_end [] = false; fun bump_init str = if symbolic_end (rev (Symbol.explode str)) then str ^ "'" else str ^ "a"; fun bump_string str = let fun bump [] = ["a"] | bump ("z" :: ss) = "a" :: bump ss | bump (s :: ss) = if is_char s andalso Char.ord #"a" <= ord s andalso ord s < Char.ord #"z" then chr (ord s + 1) :: ss else "a" :: s :: ss; val (ss, qs) = apfst rev (chop_suffix is_quasi (Symbol.explode str)); val ss' = if symbolic_end ss then "'" :: ss else bump ss; in implode (rev ss' @ qs) end; (* styles *) val sub = "\092<^sub>"; val sup = "\092<^sup>"; val bold = "\092<^bold>"; fun make_style sym = Symbol.explode #> maps (fn s => [sym, s]) #> implode; val make_sub = make_style sub; val make_sup = make_style sup; val make_bold = make_style bold; (** symbol output **) (* length *) fun sym_len s = if String.isPrefix "\092 fn n => sym_len s + n) ss 0; fun output s = (s, sym_length (Symbol.explode s)); (*final declarations of this structure!*) val explode = Symbol.explode; val length = sym_length; end; diff --git a/src/Pure/Isar/experiment.ML b/src/Pure/Isar/experiment.ML --- a/src/Pure/Isar/experiment.ML +++ b/src/Pure/Isar/experiment.ML @@ -1,44 +1,44 @@ (* Title: Pure/Isar/experiment.ML Author: Makarius Target for specification experiments that are mostly private. *) signature EXPERIMENT = sig val is_experiment: theory -> string -> bool val experiment: Element.context_i list -> theory -> Binding.scope * local_theory val experiment_cmd: Element.context list -> theory -> Binding.scope * local_theory end; structure Experiment: EXPERIMENT = struct structure Data = Theory_Data ( - type T = Symtab.set; - val empty = Symtab.empty; - val merge = Symtab.merge (K true); + type T = Symset.T; + val empty = Symset.empty; + val merge = Symset.merge; ); -fun is_experiment thy name = Symtab.defined (Data.get thy) name; +fun is_experiment thy name = Symset.member (Data.get thy) name; fun gen_experiment add_locale elems thy = let val experiment_name = Binding.name ("experiment" ^ serial_string ()) |> Binding.concealed; val lthy = thy |> add_locale experiment_name Binding.empty [] ([], []) elems - |-> (Local_Theory.background_theory o Data.map o Symtab.insert_set); + |-> (Local_Theory.background_theory o Data.map o Symset.insert); val (scope, naming) = Name_Space.new_scope (Proof_Context.naming_of (Local_Theory.target_of lthy)); val naming' = naming |> Name_Space.private_scope scope; val lthy' = lthy |> Local_Theory.map_contexts (K (Proof_Context.map_naming (K naming'))) |> Local_Theory.map_background_naming Name_Space.concealed; in (scope, lthy') end; val experiment = gen_experiment Expression.add_locale; val experiment_cmd = gen_experiment Expression.add_locale_cmd; end; diff --git a/src/Pure/Isar/keyword.ML b/src/Pure/Isar/keyword.ML --- a/src/Pure/Isar/keyword.ML +++ b/src/Pure/Isar/keyword.ML @@ -1,296 +1,296 @@ (* Title: Pure/Isar/keyword.ML Author: Makarius Isar keyword classification. *) signature KEYWORD = sig val diag: string val document_heading: string val document_body: string val document_raw: string val thy_begin: string val thy_end: string val thy_decl: string val thy_decl_block: string val thy_defn: string val thy_stmt: string val thy_load: string val thy_goal: string val thy_goal_defn: string val thy_goal_stmt: string val qed: string val qed_script: string val qed_block: string val qed_global: string val prf_goal: string val prf_block: string val next_block: string val prf_open: string val prf_close: string val prf_chain: string val prf_decl: string val prf_asm: string val prf_asm_goal: string val prf_script: string val prf_script_goal: string val prf_script_asm_goal: string val before_command: string val quasi_command: string type spec = {kind: string, load_command: string * Position.T, tags: string list} val command_spec: string * string list -> spec val no_spec: spec val before_command_spec: spec val quasi_command_spec: spec val document_heading_spec: spec val document_body_spec: spec type keywords val minor_keywords: keywords -> Scan.lexicon val major_keywords: keywords -> Scan.lexicon val empty_keywords: keywords val merge_keywords: keywords * keywords -> keywords val add_keywords: ((string * Position.T) * spec) list -> keywords -> keywords val add_minor_keywords: string list -> keywords -> keywords val add_major_keywords: string list -> keywords -> keywords val no_major_keywords: keywords -> keywords val is_keyword: keywords -> string -> bool val is_command: keywords -> string -> bool val is_literal: keywords -> string -> bool val dest_commands: keywords -> string list val command_markup: keywords -> string -> Markup.T option val command_kind: keywords -> string -> string option val command_tags: keywords -> string -> string list val is_vacuous: keywords -> string -> bool val is_diag: keywords -> string -> bool val is_document_heading: keywords -> string -> bool val is_document_body: keywords -> string -> bool val is_document_raw: keywords -> string -> bool val is_document: keywords -> string -> bool val is_theory_end: keywords -> string -> bool val is_theory_load: keywords -> string -> bool val is_theory: keywords -> string -> bool val is_theory_body: keywords -> string -> bool val is_proof: keywords -> string -> bool val is_proof_body: keywords -> string -> bool val is_theory_goal: keywords -> string -> bool val is_proof_goal: keywords -> string -> bool val is_qed: keywords -> string -> bool val is_qed_global: keywords -> string -> bool val is_proof_open: keywords -> string -> bool val is_proof_close: keywords -> string -> bool val is_proof_asm: keywords -> string -> bool val is_improper: keywords -> string -> bool val is_printed: keywords -> string -> bool end; structure Keyword: KEYWORD = struct (** keyword classification **) (* kinds *) val diag = "diag"; val document_heading = "document_heading"; val document_body = "document_body"; val document_raw = "document_raw"; val thy_begin = "thy_begin"; val thy_end = "thy_end"; val thy_decl = "thy_decl"; val thy_decl_block = "thy_decl_block"; val thy_defn = "thy_defn"; val thy_stmt = "thy_stmt"; val thy_load = "thy_load"; val thy_goal = "thy_goal"; val thy_goal_defn = "thy_goal_defn"; val thy_goal_stmt = "thy_goal_stmt"; val qed = "qed"; val qed_script = "qed_script"; val qed_block = "qed_block"; val qed_global = "qed_global"; val prf_goal = "prf_goal"; val prf_block = "prf_block"; val next_block = "next_block"; val prf_open = "prf_open"; val prf_close = "prf_close"; val prf_chain = "prf_chain"; val prf_decl = "prf_decl"; val prf_asm = "prf_asm"; val prf_asm_goal = "prf_asm_goal"; val prf_script = "prf_script"; val prf_script_goal = "prf_script_goal"; val prf_script_asm_goal = "prf_script_asm_goal"; val before_command = "before_command"; val quasi_command = "quasi_command"; val command_kinds = [diag, document_heading, document_body, document_raw, thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_defn, thy_stmt, thy_goal, thy_goal_defn, thy_goal_stmt, qed, qed_script, qed_block, qed_global, prf_goal, prf_block, next_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal, prf_script_asm_goal]; (* specifications *) type spec = {kind: string, load_command: string * Position.T, tags: string list}; fun command_spec (kind, tags) : spec = {kind = kind, load_command = ("", Position.none), tags = tags}; val no_spec = command_spec ("", []); val before_command_spec = command_spec (before_command, []); val quasi_command_spec = command_spec (quasi_command, []); val document_heading_spec = command_spec ("document_heading", ["document"]); val document_body_spec = command_spec ("document_body", ["document"]); type entry = {pos: Position.T, id: serial, kind: string, tags: string list}; fun check_spec pos ({kind, tags, ...}: spec) : entry = if not (member (op =) command_kinds kind) then error ("Unknown outer syntax keyword kind " ^ quote kind) else {pos = pos, id = serial (), kind = kind, tags = tags}; (** keyword tables **) (* type keywords *) datatype keywords = Keywords of {minor: Scan.lexicon, major: Scan.lexicon, commands: entry Symtab.table}; fun minor_keywords (Keywords {minor, ...}) = minor; fun major_keywords (Keywords {major, ...}) = major; fun make_keywords (minor, major, commands) = Keywords {minor = minor, major = major, commands = commands}; fun map_keywords f (Keywords {minor, major, commands}) = make_keywords (f (minor, major, commands)); (* build keywords *) val empty_keywords = make_keywords (Scan.empty_lexicon, Scan.empty_lexicon, Symtab.empty); fun merge_keywords (Keywords {minor = minor1, major = major1, commands = commands1}, Keywords {minor = minor2, major = major2, commands = commands2}) = make_keywords (Scan.merge_lexicons (minor1, minor2), Scan.merge_lexicons (major1, major2), Symtab.merge (K true) (commands1, commands2)); val add_keywords = fold (fn ((name, pos), spec as {kind, ...}: spec) => map_keywords (fn (minor, major, commands) => if kind = "" orelse kind = before_command orelse kind = quasi_command then let val minor' = Scan.extend_lexicon (Symbol.explode name) minor; in (minor', major, commands) end else let val entry = check_spec pos spec; val major' = Scan.extend_lexicon (Symbol.explode name) major; val commands' = Symtab.update (name, entry) commands; in (minor, major', commands') end)); val add_minor_keywords = add_keywords o map (fn name => ((name, Position.none), no_spec)); val add_major_keywords = add_keywords o map (fn name => ((name, Position.none), command_spec (diag, []))); val no_major_keywords = map_keywords (fn (minor, _, _) => (minor, Scan.empty_lexicon, Symtab.empty)); (* keyword status *) fun is_keyword keywords s = Scan.is_literal (minor_keywords keywords) (Symbol.explode s); fun is_command (Keywords {commands, ...}) = Symtab.defined commands; fun is_literal keywords = is_keyword keywords orf is_command keywords; fun dest_commands (Keywords {commands, ...}) = Symtab.keys commands; (* command keywords *) fun lookup_command (Keywords {commands, ...}) = Symtab.lookup commands; fun command_markup keywords name = lookup_command keywords name |> Option.map (fn {pos, id, ...} => Position.make_entity_markup {def = false} id Markup.command_keywordN (name, pos)); fun command_kind keywords = Option.map #kind o lookup_command keywords; fun command_tags keywords name = (case lookup_command keywords name of SOME {tags, ...} => tags | NONE => []); (* command categories *) fun command_category ks = let - val tab = Symtab.make_set ks; + val set = Symset.make ks; fun pred keywords name = (case lookup_command keywords name of NONE => false - | SOME {kind, ...} => Symtab.defined tab kind); + | SOME {kind, ...} => Symset.member set kind); in pred end; val is_vacuous = command_category [diag, document_heading, document_body, document_raw]; val is_diag = command_category [diag]; val is_document_heading = command_category [document_heading]; val is_document_body = command_category [document_body]; val is_document_raw = command_category [document_raw]; val is_document = command_category [document_heading, document_body, document_raw]; val is_theory_end = command_category [thy_end]; val is_theory_load = command_category [thy_load]; val is_theory = command_category [thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_defn, thy_stmt, thy_goal, thy_goal_defn, thy_goal_stmt]; val is_theory_body = command_category [thy_load, thy_decl, thy_decl_block, thy_defn, thy_stmt, thy_goal, thy_goal_defn, thy_goal_stmt]; val is_proof = command_category [qed, qed_script, qed_block, qed_global, prf_goal, prf_block, next_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal, prf_script_asm_goal]; val is_proof_body = command_category [diag, document_heading, document_body, document_raw, prf_block, next_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal, prf_script_asm_goal]; val is_theory_goal = command_category [thy_goal, thy_goal_defn, thy_goal_stmt]; val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal]; val is_qed = command_category [qed, qed_script, qed_block]; val is_qed_global = command_category [qed_global]; val is_proof_open = command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal, prf_open]; val is_proof_close = command_category [qed, qed_script, qed_block, prf_close]; val is_proof_asm = command_category [prf_asm, prf_asm_goal]; val is_improper = command_category [qed_script, prf_script, prf_script_goal, prf_script_asm_goal]; fun is_printed keywords = is_theory_goal keywords orf is_proof keywords; end; diff --git a/src/Pure/Isar/proof_context.ML b/src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML +++ b/src/Pure/Isar/proof_context.ML @@ -1,1676 +1,1676 @@ (* Title: Pure/Isar/proof_context.ML Author: Markus Wenzel, TU Muenchen The key concept of Isar proof contexts: elevates primitive local reasoning Gamma |- phi to a structured concept, with generic context elements. See also structure Variable and Assumption. *) signature PROOF_CONTEXT = sig val theory_of: Proof.context -> theory val init_global: theory -> Proof.context val get_global: theory -> string -> Proof.context type mode val mode_default: mode val mode_pattern: mode val mode_schematic: mode val mode_abbrev: mode val set_mode: mode -> Proof.context -> Proof.context val get_mode: Proof.context -> mode val restore_mode: Proof.context -> Proof.context -> Proof.context val abbrev_mode: Proof.context -> bool val syn_of: Proof.context -> Syntax.syntax val tsig_of: Proof.context -> Type.tsig val set_defsort: sort -> Proof.context -> Proof.context val default_sort: Proof.context -> indexname -> sort val arity_sorts: Proof.context -> string -> sort -> sort list val consts_of: Proof.context -> Consts.T val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context val naming_of: Proof.context -> Name_Space.naming val restore_naming: Proof.context -> Proof.context -> Proof.context val full_name: Proof.context -> binding -> string val get_scope: Proof.context -> Binding.scope option val new_scope: Proof.context -> Binding.scope * Proof.context val private_scope: Binding.scope -> Proof.context -> Proof.context val private: Position.T -> Proof.context -> Proof.context val qualified_scope: Binding.scope -> Proof.context -> Proof.context val qualified: Position.T -> Proof.context -> Proof.context val concealed: Proof.context -> Proof.context val class_space: Proof.context -> Name_Space.T val type_space: Proof.context -> Name_Space.T val const_space: Proof.context -> Name_Space.T val defs_context: Proof.context -> Defs.context val intern_class: Proof.context -> xstring -> string val intern_type: Proof.context -> xstring -> string val intern_const: Proof.context -> xstring -> string val extern_class: Proof.context -> string -> xstring val markup_class: Proof.context -> string -> string val pretty_class: Proof.context -> string -> Pretty.T val extern_type: Proof.context -> string -> xstring val markup_type: Proof.context -> string -> string val pretty_type: Proof.context -> string -> Pretty.T val extern_const: Proof.context -> string -> xstring val markup_const: Proof.context -> string -> string val pretty_const: Proof.context -> string -> Pretty.T val transfer: theory -> Proof.context -> Proof.context val transfer_facts: theory -> Proof.context -> Proof.context val background_theory: (theory -> theory) -> Proof.context -> Proof.context val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context val facts_of: Proof.context -> Facts.T val facts_of_fact: Proof.context -> string -> Facts.T val markup_extern_fact: Proof.context -> string -> Markup.T list * xstring val augment: term -> Proof.context -> Proof.context val print_name: Proof.context -> string -> string val pretty_name: Proof.context -> string -> Pretty.T val pretty_term_abbrev: Proof.context -> term -> Pretty.T val pretty_fact: Proof.context -> string * thm list -> Pretty.T val check_class: Proof.context -> xstring * Position.T -> class * Position.report list val read_class: Proof.context -> string -> class val read_typ: Proof.context -> string -> typ val read_typ_syntax: Proof.context -> string -> typ val read_typ_abbrev: Proof.context -> string -> typ val cert_typ: Proof.context -> typ -> typ val cert_typ_syntax: Proof.context -> typ -> typ val cert_typ_abbrev: Proof.context -> typ -> typ val infer_type: Proof.context -> string * typ -> typ val inferred_param: string -> Proof.context -> (string * typ) * Proof.context val inferred_fixes: Proof.context -> (string * typ) list * Proof.context val check_type_name: {proper: bool, strict: bool} -> Proof.context -> xstring * Position.T -> typ * Position.report list val read_type_name: {proper: bool, strict: bool} -> Proof.context -> string -> typ val consts_completion_message: Proof.context -> xstring * Position.T list -> string val check_const: {proper: bool, strict: bool} -> Proof.context -> xstring * Position.T list -> term * Position.report list val read_const: {proper: bool, strict: bool} -> Proof.context -> string -> term val read_arity: Proof.context -> xstring * string list * string -> arity val cert_arity: Proof.context -> arity -> arity val allow_dummies: Proof.context -> Proof.context val prepare_sortsT: Proof.context -> typ list -> string list * typ list val prepare_sorts: Proof.context -> term list -> string list * term list val check_tfree: Proof.context -> string * sort -> string * sort val read_term_pattern: Proof.context -> string -> term val read_term_schematic: Proof.context -> string -> term val read_term_abbrev: Proof.context -> string -> term val show_abbrevs: bool Config.T val expand_abbrevs: Proof.context -> term -> term val cert_term: Proof.context -> term -> term val cert_prop: Proof.context -> term -> term val def_type: Proof.context -> indexname -> typ option val standard_typ_check: Proof.context -> typ list -> typ list val standard_term_check_finish: Proof.context -> term list -> term list val standard_term_uncheck: Proof.context -> term list -> term list val goal_export: Proof.context -> Proof.context -> thm list -> thm list val export: Proof.context -> Proof.context -> thm list -> thm list val export_morphism: Proof.context -> Proof.context -> morphism val norm_export_morphism: Proof.context -> Proof.context -> morphism val auto_bind_goal: term list -> Proof.context -> Proof.context val auto_bind_facts: term list -> Proof.context -> Proof.context val simult_matches: Proof.context -> term * term list -> (indexname * term) list val maybe_bind_term: indexname * term option -> Proof.context -> Proof.context val bind_term: indexname * term -> Proof.context -> Proof.context val cert_propp: Proof.context -> (term * term list) list list -> (term list list * (indexname * term) list) val read_propp: Proof.context -> (string * string list) list list -> (term list list * (indexname * term) list) val fact_tac: Proof.context -> thm list -> int -> tactic val some_fact_tac: Proof.context -> int -> tactic val lookup_fact: Proof.context -> string -> {dynamic: bool, thms: thm list} option val dynamic_facts_dummy: bool Config.T val get_fact_generic: Context.generic -> Facts.ref -> string option * thm list val get_fact: Proof.context -> Facts.ref -> thm list val get_fact_single: Proof.context -> Facts.ref -> thm val get_thms: Proof.context -> xstring -> thm list val get_thm: Proof.context -> xstring -> thm val is_stmt: Proof.context -> bool val set_stmt: bool -> Proof.context -> Proof.context val restore_stmt: Proof.context -> Proof.context -> Proof.context val add_thms_dynamic: binding * (Context.generic -> thm list) -> Proof.context -> string * Proof.context val add_thms_lazy: string -> (binding * thm list lazy) -> Proof.context -> Proof.context val note_thms: string -> Thm.binding * (thm list * attribute list) list -> Proof.context -> (string * thm list) * Proof.context val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list -> Proof.context -> (string * thm list) list * Proof.context val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context val alias_fact: binding -> string -> Proof.context -> Proof.context val read_var: binding * string option * mixfix -> Proof.context -> (binding * typ option * mixfix) * Proof.context val cert_var: binding * typ option * mixfix -> Proof.context -> (binding * typ option * mixfix) * Proof.context val add_fixes: (binding * typ option * mixfix) list -> Proof.context -> string list * Proof.context val add_fixes_cmd: (binding * string option * mixfix) list -> Proof.context -> string list * Proof.context val add_assms: Assumption.export -> (Thm.binding * (term * term list) list) list -> Proof.context -> (string * thm list) list * Proof.context val add_assms_cmd: Assumption.export -> (Thm.binding * (string * string list) list) list -> Proof.context -> (string * thm list) list * Proof.context val dest_cases: Proof.context option -> Proof.context -> (string * Rule_Cases.T) list val update_cases: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context val check_case: Proof.context -> bool -> string * Position.T -> binding option list -> Rule_Cases.T val check_syntax_const: Proof.context -> string * Position.T -> string val syntax: bool -> Syntax.mode -> (string * typ * mixfix) list -> Proof.context -> Proof.context val generic_syntax: bool -> Syntax.mode -> (string * typ * mixfix) list -> Context.generic -> Context.generic val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context val generic_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism -> Context.generic -> Context.generic val generic_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism -> Context.generic -> Context.generic val type_alias: binding -> string -> Proof.context -> Proof.context val const_alias: binding -> string -> Proof.context -> Proof.context val add_const_constraint: string * typ option -> Proof.context -> Proof.context val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context val revert_abbrev: string -> string -> Proof.context -> Proof.context val generic_add_abbrev: string -> binding * term -> Context.generic -> (term * term) * Context.generic val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic type stmt = {vars: ((binding * typ option * mixfix) * (string * term)) list, propss: term list list, binds: (indexname * term) list, result_binds: (indexname * term) list} val cert_stmt: (binding * typ option * mixfix) list -> (term * term list) list list -> Proof.context -> stmt * Proof.context val read_stmt: (binding * string option * mixfix) list -> (string * string list) list list -> Proof.context -> stmt * Proof.context type statement = {fixes: (string * term) list, assumes: term list list, shows: term list list, result_binds: (indexname * term option) list, text: term, result_text: term} val cert_statement: (binding * typ option * mixfix) list -> (term * term list) list list -> (term * term list) list list -> Proof.context -> statement * Proof.context val read_statement: (binding * string option * mixfix) list -> (string * string list) list list -> (string * string list) list list -> Proof.context -> statement * Proof.context val print_syntax: Proof.context -> unit val print_abbrevs: bool -> Proof.context -> unit val pretty_term_bindings: Proof.context -> Pretty.T list val pretty_local_facts: bool -> Proof.context -> Pretty.T list val print_local_facts: bool -> Proof.context -> unit val pretty_cases: Proof.context -> Pretty.T list val print_cases_proof: Proof.context -> Proof.context -> string val debug: bool Config.T val verbose: bool Config.T val pretty_ctxt: Proof.context -> Pretty.T list val pretty_context: Proof.context -> Pretty.T list end; structure Proof_Context: PROOF_CONTEXT = struct val theory_of = Proof_Context.theory_of; val init_global = Proof_Context.init_global; val get_global = Proof_Context.get_global; (** inner syntax mode **) datatype mode = Mode of {pattern: bool, (*pattern binding schematic variables*) schematic: bool, (*term referencing loose schematic variables*) abbrev: bool}; (*abbrev mode -- no normalization*) fun make_mode (pattern, schematic, abbrev) = Mode {pattern = pattern, schematic = schematic, abbrev = abbrev}; val mode_default = make_mode (false, false, false); val mode_pattern = make_mode (true, false, false); val mode_schematic = make_mode (false, true, false); val mode_abbrev = make_mode (false, false, true); (** Isar proof context information **) type cases = Rule_Cases.T Name_Space.table; val empty_cases: cases = Name_Space.empty_table Markup.caseN; datatype data = Data of {mode: mode, (*inner syntax mode*) syntax: Local_Syntax.T, (*local syntax*) tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*) consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*) facts: Facts.T, (*local facts, based on initial global facts*) cases: cases}; (*named case contexts*) fun make_data (mode, syntax, tsig, consts, facts, cases) = Data {mode = mode, syntax = syntax, tsig = tsig, consts = consts, facts = facts, cases = cases}; structure Data = Proof_Data ( type T = data; fun init thy = make_data (mode_default, Local_Syntax.init thy, (Type.change_ignore (Sign.tsig_of thy), Sign.tsig_of thy), (Consts.change_ignore (Sign.consts_of thy), Sign.consts_of thy), Global_Theory.facts_of thy, empty_cases); ); fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep); fun map_data_result f ctxt = let val Data {mode, syntax, tsig, consts, facts, cases} = Data.get ctxt; val (res, data') = f (mode, syntax, tsig, consts, facts, cases) ||> make_data; in (res, Data.put data' ctxt) end; fun map_data f = snd o map_data_result (pair () o f); fun set_mode mode = map_data (fn (_, syntax, tsig, consts, facts, cases) => (mode, syntax, tsig, consts, facts, cases)); fun map_syntax f = map_data (fn (mode, syntax, tsig, consts, facts, cases) => (mode, f syntax, tsig, consts, facts, cases)); fun map_syntax_idents f ctxt = let val (opt_idents', syntax') = f (#syntax (rep_data ctxt)) in ctxt |> map_syntax (K syntax') |> (case opt_idents' of NONE => I | SOME idents' => Syntax_Trans.put_idents idents') end; fun map_tsig f = map_data (fn (mode, syntax, tsig, consts, facts, cases) => (mode, syntax, f tsig, consts, facts, cases)); fun map_consts f = map_data (fn (mode, syntax, tsig, consts, facts, cases) => (mode, syntax, tsig, f consts, facts, cases)); fun map_facts_result f = map_data_result (fn (mode, syntax, tsig, consts, facts, cases) => let val (res, facts') = f facts in (res, (mode, syntax, tsig, consts, facts', cases)) end); fun map_facts f = snd o map_facts_result (pair () o f); fun map_cases f = map_data (fn (mode, syntax, tsig, consts, facts, cases) => (mode, syntax, tsig, consts, facts, f cases)); val get_mode = #mode o rep_data; val restore_mode = set_mode o get_mode; val abbrev_mode = get_mode #> (fn Mode {abbrev, ...} => abbrev); val syntax_of = #syntax o rep_data; val syn_of = Local_Syntax.syn_of o syntax_of; val set_syntax_mode = map_syntax o Local_Syntax.set_mode; val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of; val tsig_of = #1 o #tsig o rep_data; val set_defsort = map_tsig o apfst o Type.set_defsort; fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt; fun arity_sorts ctxt = Type.arity_sorts (Context.Proof ctxt) (tsig_of ctxt); val consts_of = #1 o #consts o rep_data; val cases_of = #cases o rep_data; (* naming *) val naming_of = Name_Space.naming_of o Context.Proof; val map_naming = Context.proof_map o Name_Space.map_naming; val restore_naming = map_naming o K o naming_of; val full_name = Name_Space.full_name o naming_of; val get_scope = Name_Space.get_scope o naming_of; fun new_scope ctxt = let val (scope, naming') = Name_Space.new_scope (naming_of ctxt); val ctxt' = map_naming (K naming') ctxt; in (scope, ctxt') end; val private_scope = map_naming o Name_Space.private_scope; val private = map_naming o Name_Space.private; val qualified_scope = map_naming o Name_Space.qualified_scope; val qualified = map_naming o Name_Space.qualified; val concealed = map_naming Name_Space.concealed; (* name spaces *) val class_space = Type.class_space o tsig_of; val type_space = Type.type_space o tsig_of; val const_space = Consts.space_of o consts_of; fun defs_context ctxt = (ctxt, (const_space ctxt, type_space ctxt)); val intern_class = Name_Space.intern o class_space; val intern_type = Name_Space.intern o type_space; val intern_const = Name_Space.intern o const_space; fun extern_class ctxt = Name_Space.extern ctxt (class_space ctxt); fun extern_type ctxt = Name_Space.extern ctxt (type_space ctxt); fun extern_const ctxt = Name_Space.extern ctxt (const_space ctxt); fun markup_class ctxt c = Name_Space.markup_extern ctxt (class_space ctxt) c |-> Markup.markup; fun markup_type ctxt c = Name_Space.markup_extern ctxt (type_space ctxt) c |-> Markup.markup; fun markup_const ctxt c = Name_Space.markup_extern ctxt (const_space ctxt) c |-> Markup.markup; fun pretty_class ctxt c = Name_Space.markup_extern ctxt (class_space ctxt) c |> Pretty.mark_str; fun pretty_type ctxt c = Name_Space.markup_extern ctxt (type_space ctxt) c |> Pretty.mark_str; fun pretty_const ctxt c = Name_Space.markup_extern ctxt (const_space ctxt) c |> Pretty.mark_str; (* theory transfer *) fun transfer_syntax thy ctxt = ctxt |> map_syntax (Local_Syntax.rebuild thy) |> map_tsig (fn tsig as (local_tsig, global_tsig) => let val thy_tsig = Sign.tsig_of thy in if Type.eq_tsig (thy_tsig, global_tsig) then tsig else (Type.merge_tsig (Context.Proof ctxt) (local_tsig, thy_tsig), thy_tsig) (*historic merge order*) end) |> map_consts (fn consts as (local_consts, global_consts) => let val thy_consts = Sign.consts_of thy in if Consts.eq_consts (thy_consts, global_consts) then consts else (Consts.merge (local_consts, thy_consts), thy_consts) (*historic merge order*) end); fun transfer thy = Context.raw_transfer thy #> transfer_syntax thy; fun transfer_facts thy = map_facts (fn local_facts => Facts.merge (Global_Theory.facts_of thy, local_facts)); fun background_theory f ctxt = transfer (f (theory_of ctxt)) ctxt; fun background_theory_result f ctxt = let val (res, thy') = f (theory_of ctxt) in (res, ctxt |> transfer thy') end; (* hybrid facts *) val facts_of = #facts o rep_data; fun facts_of_fact ctxt name = let val local_facts = facts_of ctxt; val global_facts = Global_Theory.facts_of (theory_of ctxt); in if Facts.defined local_facts name then local_facts else global_facts end; fun markup_extern_fact ctxt name = let val facts = facts_of_fact ctxt name; val (markup, xname) = Facts.markup_extern ctxt facts name; val markups = if Facts.is_dynamic facts name then [markup, Markup.dynamic_fact name] else [markup]; in (markups, xname) end; (* augment context by implicit term declarations *) fun augment t ctxt = ctxt |> Variable.add_fixes_implicit t |> Variable.declare_term t |> Soft_Type_System.augment t; (** pretty printing **) val print_name = Token.print_name o Thy_Header.get_keywords'; val pretty_name = Pretty.str oo print_name; fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt); fun pretty_fact_name ctxt a = Pretty.block [Pretty.marks_str (markup_extern_fact ctxt a), Pretty.str ":"]; fun pretty_fact ctxt = let val pretty_thm = Thm.pretty_thm ctxt; val pretty_thms = map (Thm.pretty_thm_item ctxt); in fn ("", [th]) => pretty_thm th | ("", ths) => Pretty.blk (0, Pretty.fbreaks (pretty_thms ths)) | (a, [th]) => Pretty.block [pretty_fact_name ctxt a, Pretty.brk 1, pretty_thm th] | (a, ths) => Pretty.block (Pretty.fbreaks (pretty_fact_name ctxt a :: pretty_thms ths)) end; (** prepare types **) (* classes *) fun check_class ctxt (xname, pos) = let val tsig = tsig_of ctxt; val class_space = Type.class_space tsig; val name = Type.cert_class tsig (Name_Space.intern class_space xname) handle TYPE (msg, _, _) => error (msg ^ Position.here pos ^ Completion.markup_report [Name_Space.completion (Context.Proof ctxt) class_space (K true) (xname, pos)]); val reports = if Context_Position.is_reported ctxt pos then [(pos, Name_Space.markup class_space name)] else []; in (name, reports) end; fun read_class ctxt text = let val source = Syntax.read_input text; val (c, reports) = check_class ctxt (Input.source_content source); val _ = Context_Position.reports ctxt reports; in c end; (* types *) fun read_typ_mode mode ctxt s = Syntax.read_typ (Type.set_mode mode ctxt) s; val read_typ = read_typ_mode Type.mode_default; val read_typ_syntax = read_typ_mode Type.mode_syntax; val read_typ_abbrev = read_typ_mode Type.mode_abbrev; fun cert_typ_mode mode ctxt T = Type.cert_typ_mode mode (tsig_of ctxt) T handle TYPE (msg, _, _) => error msg; val cert_typ = cert_typ_mode Type.mode_default; val cert_typ_syntax = cert_typ_mode Type.mode_syntax; val cert_typ_abbrev = cert_typ_mode Type.mode_abbrev; (** prepare terms and propositions **) (* inferred types of parameters *) fun infer_type ctxt x = Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) (Free x)); fun inferred_param x ctxt = let val p = (x, infer_type ctxt (x, dummyT)) in (p, ctxt |> Variable.declare_term (Free p)) end; fun inferred_fixes ctxt = fold_map inferred_param (map #2 (Variable.dest_fixes ctxt)) ctxt; (* type names *) fun check_type_name {proper, strict} ctxt (c, pos) = if Lexicon.is_tid c then if proper then error ("Not a type constructor: " ^ quote c ^ Position.here pos) else let val reports = if Context_Position.is_reported ctxt pos then [(pos, Markup.tfree)] else []; in (TFree (c, default_sort ctxt (c, ~1)), reports) end else let val ((d, reports), decl) = Type.check_decl (Context.Proof ctxt) (tsig_of ctxt) (c, pos); fun err () = error ("Bad type name: " ^ quote d ^ Position.here pos); val args = (case decl of Type.LogicalType n => n | Type.Abbreviation (vs, _, _) => if strict then err () else length vs | Type.Nonterminal => if strict then err () else 0); in (Type (d, replicate args dummyT), reports) end; fun read_type_name flags ctxt text = let val source = Syntax.read_input text; val (T, reports) = check_type_name flags ctxt (Input.source_content source); val _ = Context_Position.reports ctxt reports; in T end; (* constant names *) fun consts_completion_message ctxt (c, ps) = ps |> map (fn pos => Name_Space.completion (Context.Proof ctxt) (Consts.space_of (consts_of ctxt)) (K true) (c, pos)) |> Completion.markup_report; fun check_const {proper, strict} ctxt (c, ps) = let val _ = Name.reject_internal (c, ps) handle ERROR msg => error (msg ^ consts_completion_message ctxt (c, ps)); fun err msg = error (msg ^ Position.here_list ps); val consts = consts_of ctxt; val fixed = if proper then NONE else Variable.lookup_fixed ctxt c; val (t, reports) = (case (fixed, Variable.lookup_const ctxt c) of (SOME x, NONE) => let val reports = ps |> filter (Context_Position.is_reported ctxt) |> map (fn pos => (pos, Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free))); in (Free (x, infer_type ctxt (x, dummyT)), reports) end | (_, SOME d) => let val T = Consts.type_scheme consts d handle TYPE (msg, _, _) => err msg; val reports = ps |> filter (Context_Position.is_reported ctxt) |> map (fn pos => (pos, Name_Space.markup (Consts.space_of consts) d)); in (Const (d, T), reports) end | _ => Consts.check_const (Context.Proof ctxt) consts (c, ps)); val _ = (case (strict, t) of (true, Const (d, _)) => (ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg) | _ => ()); in (t, reports) end; fun read_const flags ctxt text = let val source = Syntax.read_input text; val (c, pos) = Input.source_content source; val (t, reports) = check_const flags ctxt (c, [pos]); val _ = Context_Position.reports ctxt reports; in t end; (* type arities *) local fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) = let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S) in Type.add_arity (Context.Proof ctxt) arity (tsig_of ctxt); arity end; in val read_arity = prep_arity ((#1 o dest_Type) oo read_type_name {proper = true, strict = true}) Syntax.read_sort; val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of); end; (* read_term *) fun read_term_mode mode ctxt = Syntax.read_term (set_mode mode ctxt); val read_term_pattern = read_term_mode mode_pattern; val read_term_schematic = read_term_mode mode_schematic; val read_term_abbrev = read_term_mode mode_abbrev; (* local abbreviations *) local fun certify_consts ctxt = Consts.certify (Context.Proof ctxt) (tsig_of ctxt) (not (abbrev_mode ctxt)) (consts_of ctxt); fun expand_binds ctxt = let val Mode {pattern, schematic, ...} = get_mode ctxt; fun reject_schematic (t as Var _) = error ("Unbound schematic variable: " ^ Syntax.string_of_term ctxt t) | reject_schematic (Abs (_, _, t)) = reject_schematic t | reject_schematic (t $ u) = (reject_schematic t; reject_schematic u) | reject_schematic _ = (); in if pattern then I else Variable.expand_binds ctxt #> (if schematic then I else tap reject_schematic) end; in fun expand_abbrevs ctxt = certify_consts ctxt #> expand_binds ctxt; end; val show_abbrevs = Config.declare_bool ("show_abbrevs", \<^here>) (K true); fun contract_abbrevs ctxt t = let val thy = theory_of ctxt; val consts = consts_of ctxt; val Mode {abbrev, ...} = get_mode ctxt; val retrieve = Consts.retrieve_abbrevs consts (print_mode_value () @ [""]); fun match_abbrev u = Option.map #1 (get_first (Pattern.match_rew thy u) (retrieve u)); in if abbrev orelse not (Config.get ctxt show_abbrevs) orelse not (can Term.type_of t) then t else Pattern.rewrite_term_top thy [] [match_abbrev] t end; (* patterns *) fun prepare_patternT ctxt T = let val Mode {pattern, schematic, ...} = get_mode ctxt; val _ = pattern orelse schematic orelse T |> Term.exists_subtype (fn T as TVar (xi, _) => not (Type_Infer.is_param xi) andalso error ("Illegal schematic type variable: " ^ Syntax.string_of_typ ctxt T) | _ => false) in T end; local val dummies = Config.declare_bool ("Proof_Context.dummies", \<^here>) (K false); fun check_dummies ctxt t = if Config.get ctxt dummies then t else Term.no_dummy_patterns t handle TERM _ => error "Illegal dummy pattern(s) in term"; fun prepare_dummies ts = #1 (fold_map Term.replace_dummy_patterns ts 1); in val allow_dummies = Config.put dummies true; fun prepare_patterns ctxt = let val Mode {pattern, ...} = get_mode ctxt in Type_Infer.fixate ctxt pattern #> pattern ? Variable.polymorphic ctxt #> (map o Term.map_types) (prepare_patternT ctxt) #> (if pattern then prepare_dummies else map (check_dummies ctxt)) end; end; (* sort constraints *) local fun prepare_sorts_env ctxt tys = let val tsig = tsig_of ctxt; val defaultS = Type.defaultS tsig; val dummy_var = ("'_dummy_", ~1); fun constraint (xi, raw_S) env = let val (ps, S) = Term_Position.decode_positionS raw_S in if xi = dummy_var orelse S = dummyS then env else Vartab.insert (op =) (xi, Type.minimize_sort tsig S) env handle Vartab.DUP _ => error ("Inconsistent sort constraints for type variable " ^ quote (Term.string_of_vname' xi) ^ Position.here_list ps) end; val env = Vartab.build (tys |> (fold o fold_atyps) (fn TFree (x, S) => constraint ((x, ~1), S) | TVar v => constraint v | _ => I)); fun get_sort xi raw_S = if xi = dummy_var then Type.minimize_sort tsig (#2 (Term_Position.decode_positionS raw_S)) else (case (Vartab.lookup env xi, Variable.def_sort ctxt xi) of (NONE, NONE) => defaultS | (NONE, SOME S) => S | (SOME S, NONE) => S | (SOME S, SOME S') => if Type.eq_sort tsig (S, S') then S' else error ("Sort constraint " ^ Syntax.string_of_sort ctxt S ^ " inconsistent with default " ^ Syntax.string_of_sort ctxt S' ^ " for type variable " ^ quote (Term.string_of_vname' xi))); fun add_report S pos reports = if Position.is_reported pos andalso not (AList.defined (op =) reports pos) then (pos, Position.reported_text pos Markup.sorting (Syntax.string_of_sort ctxt S)) :: reports else reports; fun get_sort_reports xi raw_S = let val ps = #1 (Term_Position.decode_positionS raw_S); val S = get_sort xi raw_S handle ERROR msg => error (msg ^ Position.here_list ps); in fold (add_report S) ps end; val reports = (fold o fold_atyps) (fn T => if Term_Position.is_positionT T then I else (case T of TFree (x, raw_S) => get_sort_reports (x, ~1) raw_S | TVar (xi, raw_S) => get_sort_reports xi raw_S | _ => I)) tys []; in (map #2 reports, get_sort) end; fun replace_sortsT get_sort = map_atyps (fn T => if Term_Position.is_positionT T then T else (case T of TFree (x, raw_S) => TFree (x, get_sort (x, ~1) raw_S) | TVar (xi, raw_S) => TVar (xi, get_sort xi raw_S) | _ => T)); in fun prepare_sortsT ctxt tys = let val (sorting_report, get_sort) = prepare_sorts_env ctxt tys in (sorting_report, map (replace_sortsT get_sort) tys) end; fun prepare_sorts ctxt tms = let val tys = rev ((fold o fold_types) cons tms []); val (sorting_report, get_sort) = prepare_sorts_env ctxt tys; in (sorting_report, (map o map_types) (replace_sortsT get_sort) tms) end; fun check_tfree ctxt v = let val (sorting_report, [TFree a]) = prepare_sortsT ctxt [TFree v]; val _ = if Context_Position.reports_enabled ctxt then Output.report sorting_report else (); in a end; end; (* certify terms *) local fun gen_cert prop ctxt t = t |> expand_abbrevs ctxt |> (fn t' => #1 (Sign.certify' prop (Context.Proof ctxt) false (consts_of ctxt) (theory_of ctxt) t') handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg); in val cert_term = gen_cert false; val cert_prop = gen_cert true; end; (* check/uncheck *) fun def_type ctxt = let val Mode {pattern, ...} = get_mode ctxt in Variable.def_type ctxt pattern end; fun standard_typ_check ctxt = map (cert_typ_mode (Type.get_mode ctxt) ctxt #> prepare_patternT ctxt); val standard_term_check_finish = prepare_patterns; fun standard_term_uncheck ctxt = map (contract_abbrevs ctxt); (** export results **) fun common_export is_goal inner outer = map (Assumption.export is_goal inner outer) #> Variable.export inner outer; val goal_export = common_export true; val export = common_export false; fun export_morphism inner outer = Assumption.export_morphism inner outer $> Variable.export_morphism inner outer; fun norm_export_morphism inner outer = export_morphism inner outer $> Morphism.thm_morphism "Proof_Context.norm_export" (Goal.norm_result outer); (** term bindings **) (* auto bindings *) fun auto_bind f props ctxt = fold Variable.maybe_bind_term (f ctxt props) ctxt; val auto_bind_goal = auto_bind Auto_Bind.goal; val auto_bind_facts = auto_bind Auto_Bind.facts; (* match bindings *) fun simult_matches ctxt (t, pats) = (case Seq.pull (Unify.matchers (Context.Proof ctxt) (map (rpair t) pats)) of NONE => error "Pattern match failed!" | SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []); fun maybe_bind_term (xi, t) ctxt = ctxt |> Variable.maybe_bind_term (xi, Option.map (cert_term (set_mode mode_default ctxt)) t); val bind_term = maybe_bind_term o apsnd SOME; (* propositions with patterns *) local fun prep_propp prep_props ctxt raw_args = let val props = prep_props ctxt (maps (map fst) raw_args); val props_ctxt = fold Variable.declare_term props ctxt; val patss = maps (map (prep_props (set_mode mode_pattern props_ctxt) o snd)) raw_args; val propps = unflat raw_args (props ~~ patss); val binds = (maps o maps) (simult_matches props_ctxt) propps; in (map (map fst) propps, binds) end; in val cert_propp = prep_propp (map o cert_prop); val read_propp = prep_propp Syntax.read_props; end; (** theorems **) (* fact_tac *) local fun comp_hhf_tac ctxt th i st = PRIMSEQ (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true} (false, Drule.lift_all ctxt (Thm.cprem_of st i) th, 0) i) st; fun comp_incr_tac _ [] _ = no_tac | comp_incr_tac ctxt (th :: ths) i = (fn st => comp_hhf_tac ctxt (Drule.incr_indexes st th) i st) APPEND comp_incr_tac ctxt ths i; val vacuous_facts = [Drule.termI]; in fun potential_facts ctxt prop = let val body = Term.strip_all_body prop; val vacuous = filter (fn th => Term.could_unify (body, Thm.concl_of th)) vacuous_facts |> map (rpair Position.none); in Facts.could_unify (facts_of ctxt) body @ vacuous end; fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac ctxt facts; fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac ctxt (map #1 (potential_facts ctxt goal)) i); end; (* lookup facts *) fun lookup_fact ctxt name = let val context = Context.Proof ctxt; val thy = Proof_Context.theory_of ctxt; in (case Facts.lookup context (facts_of ctxt) name of NONE => Facts.lookup context (Global_Theory.facts_of thy) name | some => some) end; (* retrieve facts *) val dynamic_facts_dummy = Config.declare_bool ("dynamic_facts_dummy_", \<^here>) (K false); local fun retrieve_global context = Facts.retrieve context (Global_Theory.facts_of (Context.theory_of context)); fun retrieve_generic (context as Context.Proof ctxt) arg = (Facts.retrieve context (facts_of ctxt) arg handle ERROR local_msg => (retrieve_global context arg handle ERROR _ => error local_msg)) | retrieve_generic context arg = retrieve_global context arg; fun retrieve pick context (Facts.Fact s) = let val ctxt = Context.the_proof context; val pos = Syntax.read_input_pos s; val prop = Syntax.read_prop (ctxt |> set_mode mode_default |> allow_dummies) s |> singleton (Variable.polymorphic ctxt); fun err ps msg = error (msg ^ Position.here_list (pos :: ps) ^ ":\n" ^ Syntax.string_of_term ctxt prop); val (prop', _) = Term.replace_dummy_patterns prop (Variable.maxidx_of ctxt + 1); fun prove th = Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac ctxt [th]))); val results = map_filter (try (apfst prove)) (potential_facts ctxt prop'); val (thm, thm_pos) = (case distinct (eq_fst Thm.eq_thm_prop) results of [res] => res | [] => err [] "Failed to retrieve literal fact" | dups => err (distinct (op =) (map #2 dups)) "Ambiguous specification of literal fact"); val markup = Position.entity_markup Markup.literal_factN ("", thm_pos); val _ = Context_Position.report_generic context pos markup; in pick true ("", thm_pos) [thm] end | retrieve pick context (Facts.Named ((xname, pos), sel)) = let val thy = Context.theory_of context; fun immediate thms = {name = xname, dynamic = false, thms = map (Thm.transfer thy) thms}; val {name, dynamic, thms} = (case xname of "" => immediate [Drule.dummy_thm] | "_" => immediate [Drule.asm_rl] | "nothing" => immediate [] | _ => retrieve_generic context (xname, pos)); val thms' = if dynamic andalso Config.get_generic context dynamic_facts_dummy then [Drule.free_dummy_thm] else Facts.select (Facts.Named ((name, pos), sel)) thms; in pick (dynamic andalso is_none sel) (name, pos) thms' end; in val get_fact_generic = retrieve (fn dynamic => fn (name, _) => fn thms => (if dynamic then SOME name else NONE, thms)); val get_fact = retrieve (K (K I)) o Context.Proof; val get_fact_single = retrieve (K Facts.the_single) o Context.Proof; fun get_thms ctxt = get_fact ctxt o Facts.named; fun get_thm ctxt = get_fact_single ctxt o Facts.named; end; (* inner statement mode *) val inner_stmt = Config.declare_bool ("inner_stmt", \<^here>) (K false); fun is_stmt ctxt = Config.get ctxt inner_stmt; val set_stmt = Config.put inner_stmt; val restore_stmt = set_stmt o is_stmt; (* facts *) fun add_thms_dynamic arg ctxt = ctxt |> map_facts_result (Facts.add_dynamic (Context.Proof ctxt) arg); local fun add_facts {index} arg ctxt = ctxt |> map_facts_result (Facts.add_static (Context.Proof ctxt) {strict = false, index = index} arg); fun update_facts flags (b, SOME ths) ctxt = ctxt |> add_facts flags (b, Lazy.value ths) |> #2 | update_facts _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b)); fun bind_name ctxt b = (full_name ctxt b, Binding.default_pos_of b); in fun add_thms_lazy kind (b, ths) ctxt = let val name_pos = bind_name ctxt b; val ths' = Global_Theory.check_thms_lazy ths |> Lazy.map_finished (Global_Theory.name_thms Global_Theory.unofficial1 name_pos #> map (Thm.kind_rule kind)); val (_, ctxt') = add_facts {index = is_stmt ctxt} (b, ths') ctxt; in ctxt' end; fun note_thms kind ((b, more_atts), facts) ctxt = let val (name, pos) = bind_name ctxt b; val facts' = facts |> Global_Theory.burrow_fact (Global_Theory.name_thms Global_Theory.unofficial1 (name, pos)); fun app (ths, atts) = fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths; val (res, ctxt') = fold_map app facts' ctxt; val thms = Global_Theory.name_thms Global_Theory.unofficial2 (name, pos) (flat res); val (_, ctxt'') = ctxt' |> add_facts {index = is_stmt ctxt} (b, Lazy.value thms); in ((name, thms), ctxt'') end; val note_thmss = fold_map o note_thms; fun put_thms index thms ctxt = ctxt |> map_naming (K Name_Space.local_naming) |> Context_Position.set_visible false |> update_facts {index = index} (apfst Binding.name thms) |> Context_Position.restore_visible ctxt |> restore_naming ctxt; end; fun alias_fact b c ctxt = map_facts (Facts.alias (naming_of ctxt) b c) ctxt; (** basic logical entities **) (* variables *) fun declare_var (x, opt_T, mx) ctxt = let val T = (case opt_T of SOME T => T | NONE => Mixfix.default_constraint mx) in (T, ctxt |> Variable.declare_constraints (Free (x, T))) end; fun add_syntax vars ctxt = map_syntax_idents (Local_Syntax.add_syntax ctxt (map (pair Local_Syntax.Fixed) vars)) ctxt; fun check_var internal b = let val x = Variable.check_name b; val check = if internal then Name.reject_skolem else Name.reject_internal; val _ = if can check (x, []) andalso Symbol_Pos.is_identifier x then () else error ("Bad name: " ^ Binding.print b); in x end; local fun check_mixfix ctxt (b, T, mx) = let val ([x], ctxt') = Variable.add_fixes_binding [Binding.reset_pos b] ctxt; val mx' = Mixfix.reset_pos mx; val _ = add_syntax [(x, T, if Context_Position.reports_enabled ctxt then mx else mx')] ctxt'; in mx' end; fun prep_var prep_typ internal (b, raw_T, mx) ctxt = let val x = check_var internal b; fun cond_tvars T = if internal then T else Type.no_tvars T handle TYPE (msg, _, _) => error msg; val opt_T = Option.map (cond_tvars o prep_typ ctxt) raw_T; val (T, ctxt') = ctxt |> declare_var (x, opt_T, mx); val mx' = if Mixfix.is_empty mx then mx else check_mixfix ctxt' (b, T, mx); in ((b, SOME T, mx'), ctxt') end; in val read_var = prep_var Syntax.read_typ false; val cert_var = prep_var cert_typ true; end; (* syntax *) fun check_syntax_const ctxt (c, pos) = if is_some (Syntax.lookup_const (syn_of ctxt) c) then c else error ("Unknown syntax const: " ^ quote c ^ Position.here pos); fun syntax add mode args ctxt = let val args' = map (pair Local_Syntax.Const) args in ctxt |> map_syntax (#2 o Local_Syntax.update_modesyntax ctxt add mode args') end; fun generic_syntax add mode args = Context.mapping (Sign.syntax add mode args) (syntax add mode args); (* notation *) local fun type_syntax (Type (c, args), mx) = SOME (Local_Syntax.Type, (Lexicon.mark_type c, Mixfix.make_type (length args), mx)) | type_syntax _ = NONE; fun const_syntax _ (Free (x, T), mx) = SOME (Local_Syntax.Fixed, (x, T, mx)) | const_syntax ctxt (Const (c, _), mx) = (case try (Consts.type_scheme (consts_of ctxt)) c of SOME T => SOME (Local_Syntax.Const, (Lexicon.mark_const c, T, mx)) | NONE => NONE) | const_syntax _ _ = NONE; fun gen_notation make_syntax add mode args ctxt = ctxt |> map_syntax_idents (Local_Syntax.update_modesyntax ctxt add mode (map_filter (make_syntax ctxt) args)); in val type_notation = gen_notation (K type_syntax); val notation = gen_notation const_syntax; fun generic_type_notation add mode args phi = let val args' = args |> map_filter (fn (T, mx) => let val T' = Morphism.typ phi T; val similar = (case (T, T') of (Type (c, _), Type (c', _)) => c = c' | _ => false); in if similar then SOME (T', mx) else NONE end); in Context.mapping (Sign.type_notation add mode args') (type_notation add mode args') end; fun generic_notation add mode args phi = let val args' = args |> map_filter (fn (t, mx) => let val t' = Morphism.term phi t in if Term.aconv_untyped (t, t') then SOME (t', mx) else NONE end); in Context.mapping (Sign.notation add mode args') (notation add mode args') end; end; (* aliases *) fun type_alias b c ctxt = (map_tsig o apfst) (Type.type_alias (naming_of ctxt) b c) ctxt; fun const_alias b c ctxt = (map_consts o apfst) (Consts.alias (naming_of ctxt) b c) ctxt; (* local constants *) fun add_const_constraint (c, opt_T) ctxt = let fun prepT raw_T = let val T = cert_typ ctxt raw_T in cert_term ctxt (Const (c, T)); T end; in ctxt |> (map_consts o apfst) (Consts.constrain (c, Option.map prepT opt_T)) end; fun add_abbrev mode (b, raw_t) ctxt = let val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t handle ERROR msg => cat_error msg ("in constant abbreviation " ^ Binding.print b); val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0]; val ((lhs, rhs), consts') = consts_of ctxt |> Consts.abbreviate (Context.Proof ctxt) (tsig_of ctxt) mode (b, t); in ctxt |> (map_consts o apfst) (K consts') |> Variable.declare_term rhs |> pair (lhs, rhs) end; fun revert_abbrev mode c = (map_consts o apfst) (Consts.revert_abbrev mode c); fun generic_add_abbrev mode arg = Context.mapping_result (Sign.add_abbrev mode arg) (add_abbrev mode arg); fun generic_revert_abbrev mode arg = Context.mapping (Sign.revert_abbrev mode arg) (revert_abbrev mode arg); (* fixes *) local fun gen_fixes prep_var raw_vars ctxt = let val (vars, _) = fold_map prep_var raw_vars ctxt; val (xs, ctxt') = Variable.add_fixes_binding (map #1 vars) ctxt; val _ = Context_Position.reports ctxt' (flat (map2 (fn x => fn pos => [(pos, Variable.markup ctxt' x), (pos, Variable.markup_entity_def ctxt' x)]) xs (map (Binding.pos_of o #1) vars))); val vars' = map2 (fn x => fn (_, opt_T, mx) => (x, opt_T, mx)) xs vars; val (Ts, ctxt'') = fold_map declare_var vars' ctxt'; val vars'' = map2 (fn T => fn (x, _, mx) => (x, T, mx)) Ts vars'; in (xs, add_syntax vars'' ctxt'') end; in val add_fixes = gen_fixes cert_var; val add_fixes_cmd = gen_fixes read_var; end; (** assumptions **) local fun gen_assms prep_propp exp args ctxt = let val (propss, binds) = prep_propp ctxt (map snd args); val props = flat propss; in ctxt |> fold Variable.declare_term props |> tap (Variable.warn_extra_tfrees ctxt) |> fold_burrow (Assumption.add_assms exp o map (Thm.cterm_of ctxt)) propss |-> (fn premss => auto_bind_facts props #> fold Variable.bind_term binds #> note_thmss "" (map fst args ~~ map (map (fn th => ([th], []))) premss)) end; in val add_assms = gen_assms cert_propp; val add_assms_cmd = gen_assms read_propp; end; (** cases **) fun dest_cases prev_ctxt ctxt = let val serial_of = #serial oo (Name_Space.the_entry o Name_Space.space_of_table); val ignored = (case prev_ctxt of - NONE => Inttab.empty + NONE => Intset.empty | SOME ctxt0 => let val cases0 = cases_of ctxt0 in - Inttab.build (cases0 |> Name_Space.fold_table (fn (a, _) => - Inttab.insert_set (serial_of cases0 a))) + Intset.build (cases0 |> Name_Space.fold_table (fn (a, _) => + Intset.insert (serial_of cases0 a))) end); val cases = cases_of ctxt; in Name_Space.fold_table (fn (a, c) => let val i = serial_of cases a - in not (Inttab.defined ignored i) ? cons (i, (a, c)) end) cases [] + in not (Intset.member ignored i) ? cons (i, (a, c)) end) cases [] |> sort (int_ord o apply2 #1) |> map #2 end; local fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b | drop_schematic b = b; fun update_case _ ("", _) cases = cases | update_case _ (name, NONE) cases = Name_Space.del_table name cases | update_case context (name, SOME c) cases = #2 (Name_Space.define context false (Binding.name name, c) cases); fun fix (b, T) ctxt = let val ([x], ctxt') = add_fixes [(b, SOME T, NoSyn)] ctxt in (Free (x, T), ctxt') end; in fun update_cases args ctxt = let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.global_naming); in map_cases (fold (update_case context) args) ctxt end; fun case_result c ctxt = let val Rule_Cases.Case {fixes, ...} = c; val (ts, ctxt') = ctxt |> fold_map fix fixes; val Rule_Cases.Case {assumes, binds, cases, ...} = Rule_Cases.apply ts c; in ctxt' |> fold (maybe_bind_term o drop_schematic) binds |> update_cases (map (apsnd SOME) cases) |> pair (assumes, (binds, cases)) end; val apply_case = apfst fst oo case_result; fun check_case ctxt internal (name, pos) param_specs = let val (_, Rule_Cases.Case {fixes, assumes, binds, cases}) = Name_Space.check (Context.Proof ctxt) (cases_of ctxt) (name, pos); val _ = List.app (fn NONE => () | SOME b => ignore (check_var internal b)) param_specs; fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys | replace [] ys = ys | replace (_ :: _) [] = error ("Too many parameters for case " ^ quote name ^ Position.here pos); val fixes' = replace param_specs fixes; val binds' = map drop_schematic binds; in if null (fold (Term.add_tvarsT o snd) fixes []) andalso null (fold (fold Term.add_vars o snd) assumes []) then Rule_Cases.Case {fixes = fixes', assumes = assumes, binds = binds', cases = cases} else error ("Illegal schematic variable(s) in case " ^ quote name ^ Position.here pos) end; end; (* structured statements *) type stmt = {vars: ((binding * typ option * mixfix) * (string * term)) list, propss: term list list, binds: (indexname * term) list, result_binds: (indexname * term) list}; type statement = {fixes: (string * term) list, assumes: term list list, shows: term list list, result_binds: (indexname * term option) list, text: term, result_text: term}; local fun export_binds ctxt' ctxt params binds = let val rhss = map (the_list o Option.map (Logic.close_term params) o snd) binds |> burrow (Variable.export_terms ctxt' ctxt) |> map (try the_single); in map fst binds ~~ rhss end; fun prep_stmt prep_var prep_propp raw_vars raw_propps ctxt = let val (vars, vars_ctxt) = fold_map prep_var raw_vars ctxt; val xs = map (Variable.check_name o #1) vars; val (xs', fixes_ctxt) = add_fixes vars vars_ctxt; val (propss, binds) = prep_propp fixes_ctxt raw_propps; val (ps, params_ctxt) = fixes_ctxt |> (fold o fold) Variable.declare_term propss |> fold_map inferred_param xs'; val params = xs ~~ map Free ps; val vars' = map2 (fn (b, _, mx) => fn (_, T) => (b, SOME T, mx)) vars ps; val binds' = binds |> map (apsnd SOME) |> export_binds params_ctxt ctxt params |> map (apsnd the); val _ = Variable.warn_extra_tfrees fixes_ctxt params_ctxt; val result : stmt = {vars = vars' ~~ params, propss = propss, binds = binds, result_binds = binds'}; in (result, params_ctxt) end; fun prep_statement prep_var prep_propp raw_fixes raw_assumes raw_shows ctxt = let val ((fixes, (assumes, shows), binds), ctxt') = ctxt |> prep_stmt prep_var prep_propp raw_fixes (raw_assumes @ raw_shows) |-> (fn {vars, propss, binds, ...} => fold Variable.bind_term binds #> pair (map #2 vars, chop (length raw_assumes) propss, binds)); val binds' = (Auto_Bind.facts ctxt' (flat shows) @ (case try List.last (flat shows) of NONE => [] | SOME prop => map (apsnd (SOME o Auto_Bind.abs_params prop)) binds)) |> export_binds ctxt' ctxt fixes; val text = Logic.close_prop fixes (flat assumes) (Logic.mk_conjunction_list (flat shows)); val text' = singleton (Variable.export_terms ctxt' ctxt) text; val result : statement = {fixes = fixes, assumes = assumes, shows = shows, result_binds = binds', text = text, result_text = text'}; in (result, ctxt') end; in val cert_stmt = prep_stmt cert_var cert_propp; val read_stmt = prep_stmt read_var read_propp; val cert_statement = prep_statement cert_var cert_propp; val read_statement = prep_statement read_var read_propp; end; (** print context information **) (* local syntax *) val print_syntax = Syntax.print_syntax o syn_of; (* abbreviations *) fun pretty_abbrevs verbose show_globals ctxt = let val space = const_space ctxt; val (constants, global_constants) = apply2 (#constants o Consts.dest) (#consts (rep_data ctxt)); val globals = Symtab.make global_constants; fun add_abbr (_, (_, NONE)) = I | add_abbr (c, (T, SOME t)) = if not show_globals andalso Symtab.defined globals c then I else cons (c, Logic.mk_equals (Const (c, T), t)); val abbrevs = Name_Space.markup_entries verbose ctxt space (fold add_abbr constants []); in if null abbrevs then [] else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)] end; fun print_abbrevs verbose = Pretty.writeln_chunks o pretty_abbrevs verbose true; (* term bindings *) fun pretty_term_bindings ctxt = let val binds = Variable.binds_of ctxt; fun prt_bind (xi, (T, t)) = pretty_term_abbrev ctxt (Logic.mk_equals (Var (xi, T), t)); in if Vartab.is_empty binds then [] else [Pretty.big_list "term bindings:" (map prt_bind (Vartab.dest binds))] end; (* local facts *) fun pretty_local_facts verbose ctxt = let val facts = facts_of ctxt; val props = map #1 (Facts.props facts); val local_facts = (if null props then [] else [("", props)]) @ Facts.dest_static verbose [Global_Theory.facts_of (theory_of ctxt)] facts; in if null local_facts then [] else [Pretty.big_list "local facts:" (map #1 (sort_by (#1 o #2) (map (`(pretty_fact ctxt)) local_facts)))] end; fun print_local_facts verbose ctxt = Pretty.writeln_chunks (pretty_local_facts verbose ctxt); (* named local contexts *) local fun pretty_case (name, (fixes, ((asms, (lets, cs)), ctxt))) = let val prt_name = pretty_name ctxt; val prt_term = Syntax.pretty_term ctxt; fun prt_let (xi, t) = Pretty.block [Pretty.quote (prt_term (Var (xi, Term.fastype_of t))), Pretty.str " =", Pretty.brk 1, Pretty.quote (prt_term t)]; fun prt_asm (a, ts) = Pretty.block (Pretty.breaks ((if a = "" then [] else [prt_name a, Pretty.str ":"]) @ map (Pretty.quote o prt_term) ts)); fun prt_sect _ _ _ [] = [] | prt_sect head sep prt xs = [Pretty.block (Pretty.breaks (head :: flat (separate sep (map (single o prt) xs))))]; in Pretty.block (prt_name name :: Pretty.str ":" :: Pretty.fbrk :: Pretty.fbreaks (prt_sect (Pretty.keyword1 "fix") [] (prt_name o Binding.name_of o fst) fixes @ prt_sect (Pretty.keyword1 "let") [Pretty.keyword2 "and"] prt_let (map_filter (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @ (if forall (null o #2) asms then [] else prt_sect (Pretty.keyword1 "assume") [Pretty.keyword2 "and"] prt_asm asms) @ prt_sect (Pretty.str "subcases:") [] (prt_name o fst) cs)) end; in fun pretty_cases ctxt = let val cases = dest_cases NONE ctxt |> map (fn (name, c as Rule_Cases.Case {fixes, ...}) => (name, (fixes, case_result c ctxt))); in if null cases then [] else [Pretty.big_list "cases:" (map pretty_case cases)] end; end; fun print_cases_proof ctxt0 ctxt = let fun trim_name x = if Name.is_internal x then Name.clean x else "_"; val trim_names = map trim_name #> drop_suffix (equal "_"); fun print_case name xs = (case trim_names xs of [] => print_name ctxt name | xs' => enclose "(" ")" (space_implode " " (map (print_name ctxt) (name :: xs')))); fun is_case x t = x = Rule_Cases.case_conclN andalso not (Term.exists_subterm Term.is_Var t); fun indentation depth = prefix (Symbol.spaces (2 * depth)); fun print_proof depth (name, Rule_Cases.Case {fixes, binds, cases, ...}) = let val indent = indentation depth; val head = indent ("case " ^ print_case name (map (Binding.name_of o #1) fixes)); val tail = if null cases then let val concl = if exists (fn ((x, _), SOME t) => is_case x t | _ => false) binds then Rule_Cases.case_conclN else Auto_Bind.thesisN in indent ("then show ?" ^ concl ^ " sorry") end else print_proofs depth cases; in head ^ "\n" ^ tail end and print_proofs 0 [] = "" | print_proofs depth cases = let val indent = indentation depth; val body = map (print_proof (depth + 1)) cases |> separate (indent "next") in if depth = 0 then body @ [indent "qed"] else if length cases = 1 then body else indent "{" :: body @ [indent "}"] end |> cat_lines; in (case print_proofs 0 (dest_cases (SOME ctxt0) ctxt) of "" => "" | s => "Proof outline with cases:\n" ^ Active.sendback_markup_command s) end; (* core context *) val debug = Config.declare_bool ("Proof_Context.debug", \<^here>) (K false); val verbose = Config.declare_bool ("Proof_Context.verbose", \<^here>) (K false); fun pretty_ctxt ctxt = if not (Config.get ctxt debug) then [] else let val prt_term = Syntax.pretty_term ctxt; (*structures*) val {structs, ...} = Syntax_Trans.get_idents ctxt; val prt_structs = if null structs then [] else [Pretty.block (Pretty.str "structures:" :: Pretty.brk 1 :: Pretty.commas (map Pretty.str structs))]; (*fixes*) fun prt_fix (x, x') = if x = x' then Pretty.str x else Pretty.block [Pretty.str x, Pretty.str " =", Pretty.brk 1, prt_term (Syntax.free x')]; val fixes = filter_out ((Name.is_internal orf member (op =) structs) o #1) (Variable.dest_fixes ctxt); val prt_fixes = if null fixes then [] else [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 :: Pretty.commas (map prt_fix fixes))]; (*assumptions*) val prt_assms = (case Assumption.all_prems_of ctxt of [] => [] | prems => [Pretty.big_list "assumptions:" [pretty_fact ctxt ("", prems)]]); in prt_structs @ prt_fixes @ prt_assms end; (* main context *) fun pretty_context ctxt = let val verbose = Config.get ctxt verbose; fun verb f x = if verbose then f (x ()) else []; val prt_term = Syntax.pretty_term ctxt; val prt_typ = Syntax.pretty_typ ctxt; val prt_sort = Syntax.pretty_sort ctxt; (*theory*) val pretty_thy = Pretty.block [Pretty.str "theory:", Pretty.brk 1, Context.pretty_thy (theory_of ctxt)]; (*defaults*) fun prt_atom prt prtT (x, X) = Pretty.block [prt x, Pretty.str " ::", Pretty.brk 1, prtT X]; fun prt_var (x, ~1) = prt_term (Syntax.free x) | prt_var xi = prt_term (Syntax.var xi); fun prt_varT (x, ~1) = prt_typ (TFree (x, [])) | prt_varT xi = prt_typ (TVar (xi, [])); val prt_defT = prt_atom prt_var prt_typ; val prt_defS = prt_atom prt_varT prt_sort; val (types, sorts) = Variable.constraints_of ctxt; in verb single (K pretty_thy) @ pretty_ctxt ctxt @ verb (pretty_abbrevs true false) (K ctxt) @ verb pretty_term_bindings (K ctxt) @ verb (pretty_local_facts true) (K ctxt) @ verb pretty_cases (K ctxt) @ verb single (fn () => Pretty.big_list "type constraints:" (map prt_defT (Vartab.dest types))) @ verb single (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts))) end; end; val show_abbrevs = Proof_Context.show_abbrevs; diff --git a/src/Pure/PIDE/document.ML b/src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML +++ b/src/Pure/PIDE/document.ML @@ -1,922 +1,922 @@ (* Title: Pure/PIDE/document.ML Author: Makarius Document as collection of named nodes, each consisting of an editable list of commands, associated with asynchronous execution process. *) signature DOCUMENT = sig val timing: bool Unsynchronized.ref type node_header = {master: string, header: Thy_Header.header, errors: string list} type overlay = Document_ID.command * (string * string list) datatype node_edit = Edits of (Document_ID.command option * Document_ID.command option) list | Deps of node_header | Perspective of bool * Document_ID.command list * overlay list type edit = string * node_edit type state val init_state: state val define_blob: string -> string -> state -> state type blob_digest = {file_node: string, src_path: Path.T, digest: string option} Exn.result type command = {command_id: Document_ID.command, name: string, parents: string list, blobs_digests: blob_digest list, blobs_index: int, tokens: ((int * int) * string) list} val define_command: command -> state -> state val command_exec: state -> string -> Document_ID.command -> Command.exec option val remove_versions: Document_ID.version list -> state -> state val start_execution: state -> state val update: Document_ID.version -> Document_ID.version -> edit list -> string list -> state -> string list * Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state val state: unit -> state val change_state: (state -> state) -> unit end; structure Document: DOCUMENT = struct val timing = Unsynchronized.ref false; fun timeit msg e = cond_timeit (! timing) msg e; (** document structure **) fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document_ID.print id); fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document_ID.print id); type node_header = {master: string, header: Thy_Header.header, errors: string list}; type perspective = {required: bool, (*required node*) - visible: Inttab.set, (*visible commands*) + visible: Intset.T, (*visible commands*) visible_last: Document_ID.command option, (*last visible command*) overlays: (string * string list) list Inttab.table}; (*command id -> print functions with args*) structure Entries = Linear_Set(type key = Document_ID.command val ord = int_ord); abstype node = Node of {header: node_header, (*master directory, theory header, errors*) keywords: Keyword.keywords option, (*outer syntax keywords*) perspective: perspective, (*command perspective*) entries: Command.exec option Entries.T, (*command entries with executions*) result: (Document_ID.command * Command.eval) option, (*result of last execution*) consolidated: unit lazy} (*consolidated status of eval forks*) and version = Version of node String_Graph.T (*development graph wrt. static imports*) with fun make_node (header, keywords, perspective, entries, result, consolidated) = Node {header = header, keywords = keywords, perspective = perspective, entries = entries, result = result, consolidated = consolidated}; fun map_node f (Node {header, keywords, perspective, entries, result, consolidated}) = make_node (f (header, keywords, perspective, entries, result, consolidated)); fun make_perspective (required, command_ids, overlays) : perspective = {required = required, - visible = Inttab.make_set command_ids, + visible = Intset.make command_ids, visible_last = try List.last command_ids, overlays = Inttab.make_list overlays}; val no_header: node_header = {master = "", header = Thy_Header.make ("", Position.none) [] [], errors = []}; val empty_perspective = make_perspective (false, [], []); val empty_node = make_node (no_header, NONE, empty_perspective, Entries.empty, NONE, Lazy.value ()); fun is_empty_perspective ({required, visible, visible_last, overlays}: perspective) = not required andalso - Inttab.is_empty visible andalso + Intset.is_empty visible andalso is_none visible_last andalso Inttab.is_empty overlays; fun is_empty_node (Node {header, keywords, perspective, entries, result, consolidated}) = header = no_header andalso is_none keywords andalso is_empty_perspective perspective andalso Entries.is_empty entries andalso is_none result andalso Lazy.is_finished consolidated; (* basic components *) fun master_directory (Node {header = {master, ...}, ...}) = (case try Url.explode master of SOME (Url.File path) => path | _ => Path.current); fun set_header master header errors = map_node (fn (_, keywords, perspective, entries, result, consolidated) => ({master = master, header = header, errors = errors}, keywords, perspective, entries, result, consolidated)); fun get_header (Node {header, ...}) = header; fun set_keywords keywords = map_node (fn (header, _, perspective, entries, result, consolidated) => (header, keywords, perspective, entries, result, consolidated)); fun read_header node span = let val (name, imports0) = (case get_header node of {errors = [], header = {name = (name, _), imports, ...}, ...} => (name, imports) | {errors, ...} => cat_lines errors |> (case Position.id_of (Position.thread_data ()) of NONE => I | SOME id => Protocol_Message.command_positions_yxml id) |> error); val {name = (_, pos), imports = imports1, keywords} = Thy_Header.read_tokens Position.none span; val imports = (map #1 imports0 ~~ map #2 imports1) handle ListPair.UnequalLengths => imports0; in Thy_Header.make (name, pos) imports keywords end; fun get_perspective (Node {perspective, ...}) = perspective; fun set_perspective args = map_node (fn (header, keywords, _, entries, result, consolidated) => (header, keywords, make_perspective args, entries, result, consolidated)); val required_node = #required o get_perspective; val command_overlays = Inttab.lookup_list o #overlays o get_perspective; -val command_visible = Inttab.defined o #visible o get_perspective; +val command_visible = Intset.member o #visible o get_perspective; val visible_last = #visible_last o get_perspective; val visible_node = is_some o visible_last fun map_entries f = map_node (fn (header, keywords, perspective, entries, result, consolidated) => (header, keywords, perspective, f entries, result, consolidated)); fun get_entries (Node {entries, ...}) = entries; fun iterate_entries f = Entries.iterate NONE f o get_entries; fun iterate_entries_after start f (Node {entries, ...}) = (case Entries.get_after entries start of NONE => I | SOME id => Entries.iterate (SOME id) f entries); fun get_result (Node {result, ...}) = result; fun set_result result = map_node (fn (header, keywords, perspective, entries, _, consolidated) => (header, keywords, perspective, entries, result, consolidated)); fun pending_result node = (case get_result node of SOME (_, eval) => not (Command.eval_finished eval) | NONE => false); fun finished_result node = (case get_result node of SOME (_, eval) => Command.eval_finished eval | NONE => false); fun finished_result_theory node = if finished_result node then let val (result_id, eval) = the (get_result node); val st = Command.eval_result_state eval; in SOME (result_id, Toplevel.end_theory Position.none st) handle ERROR _ => NONE end else NONE; fun get_consolidated (Node {consolidated, ...}) = consolidated; val reset_consolidated = map_node (fn (header, keywords, perspective, entries, result, _) => (header, keywords, perspective, entries, result, Lazy.lazy I)); fun could_consolidate node = not (Lazy.is_finished (get_consolidated node)) andalso is_some (finished_result_theory node); fun get_node nodes name = String_Graph.get_node nodes name handle String_Graph.UNDEF _ => empty_node; fun default_node name = String_Graph.default_node (name, empty_node); fun update_node name f = default_node name #> String_Graph.map_node name f; (* outer syntax keywords *) val pure_keywords = Thy_Header.get_keywords o Theory.get_pure; fun theory_keywords name = (case Thy_Info.lookup_theory name of SOME thy => Thy_Header.get_keywords thy | NONE => Keyword.empty_keywords); fun node_keywords name node = (case node of Node {keywords = SOME keywords, ...} => keywords | _ => theory_keywords name); (* node edits and associated executions *) type overlay = Document_ID.command * (string * string list); datatype node_edit = Edits of (Document_ID.command option * Document_ID.command option) list | Deps of node_header | Perspective of bool * Document_ID.command list * overlay list; type edit = string * node_edit; val after_entry = Entries.get_after o get_entries; fun lookup_entry node id = (case Entries.lookup (get_entries node) id of NONE => NONE | SOME (exec, _) => exec); fun the_entry node id = (case Entries.lookup (get_entries node) id of NONE => err_undef "command entry" id | SOME (exec, _) => exec); fun assign_entry (command_id, exec) node = if is_none (Entries.lookup (get_entries node) command_id) then node else map_entries (Entries.update (command_id, exec)) node; fun reset_after id entries = (case Entries.get_after entries id of NONE => entries | SOME next => Entries.update (next, NONE) entries); val edit_node = map_entries o fold (fn (id, SOME id2) => Entries.insert_after id (id2, NONE) | (id, NONE) => Entries.delete_after id #> reset_after id); (* version operations *) val empty_version = Version String_Graph.empty; fun nodes_of (Version nodes) = nodes; val node_of = get_node o nodes_of; fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names); fun edit_nodes (name, node_edit) (Version nodes) = Version (case node_edit of Edits edits => update_node name (edit_node edits) nodes | Deps {master, header, errors} => let val imports = map fst (#imports header); val nodes1 = nodes |> default_node name |> fold default_node imports; val nodes2 = nodes1 |> String_Graph.Keys.fold (fn dep => String_Graph.del_edge (dep, name)) (String_Graph.imm_preds nodes1 name); val (nodes3, errors1) = (String_Graph.add_deps_acyclic (name, imports) nodes2, errors) handle String_Graph.CYCLES cs => (nodes2, errors @ map cycle_msg cs); in String_Graph.map_node name (set_header master header errors1) nodes3 end | Perspective perspective => update_node name (set_perspective perspective) nodes); fun update_keywords name nodes = nodes |> String_Graph.map_node name (fn node => if is_empty_node node then node else let val {master, header, errors} = get_header node; val imports_keywords = map (node_keywords name o get_node nodes o #1) (#imports header); val keywords = Library.foldl Keyword.merge_keywords (pure_keywords (), imports_keywords); val (keywords', errors') = (Keyword.add_keywords (#keywords header) keywords, errors) handle ERROR msg => (keywords, if member (op =) errors msg then errors else errors @ [msg]); in node |> set_header master header errors' |> set_keywords (SOME keywords') end); fun edit_keywords edits (Version nodes) = Version (fold update_keywords (String_Graph.all_succs nodes (map_filter (fn (a, Deps _) => SOME a | _ => NONE) edits)) nodes); fun suppressed_node (nodes: node String_Graph.T) (name, node) = String_Graph.is_maximal nodes name andalso is_empty_node node; fun put_node (name, node) (Version nodes) = let val nodes1 = update_node name (K node) nodes; val nodes2 = if suppressed_node nodes1 (name, node) then String_Graph.del_node name nodes1 else nodes1; in Version nodes2 end; end; (** main state -- document structure and execution process **) type blob_digest = {file_node: string, src_path: Path.T, digest: string option} Exn.result; type execution = {version_id: Document_ID.version, (*static version id*) execution_id: Document_ID.execution, (*dynamic execution id*) delay_request: unit future, (*pending event timer request*) parallel_prints: Command.exec list}; (*parallel prints for early execution*) val no_execution: execution = {version_id = Document_ID.none, execution_id = Document_ID.none, delay_request = Future.value (), parallel_prints = []}; fun new_execution version_id delay_request parallel_prints : execution = {version_id = version_id, execution_id = Execution.start (), delay_request = delay_request, parallel_prints = parallel_prints}; abstype state = State of {versions: version Inttab.table, (*version id -> document content*) blobs: (SHA1.digest * string list) Symtab.table, (*raw digest -> digest, lines*) commands: (string * blob_digest list * int * Token.T list lazy) Inttab.table, (*command id -> name, inlined files, token index of files, command span*) execution: execution} (*current execution process*) with fun make_state (versions, blobs, commands, execution) = State {versions = versions, blobs = blobs, commands = commands, execution = execution}; fun map_state f (State {versions, blobs, commands, execution}) = make_state (f (versions, blobs, commands, execution)); val init_state = make_state (Inttab.make [(Document_ID.none, empty_version)], Symtab.empty, Inttab.empty, no_execution); (* document versions *) fun parallel_prints_node node = iterate_entries (fn (_, opt_exec) => fn rev_result => (case opt_exec of SOME (eval, prints) => (case filter Command.parallel_print prints of [] => SOME rev_result | prints' => SOME ((eval, prints') :: rev_result)) | NONE => NONE)) node [] |> rev; fun define_version version_id version assigned_nodes = map_state (fn (versions, blobs, commands, {delay_request, ...}) => let val version' = fold put_node assigned_nodes version; val versions' = Inttab.update_new (version_id, version') versions handle Inttab.DUP dup => err_dup "document version" dup; val parallel_prints = maps (parallel_prints_node o #2) assigned_nodes; val execution' = new_execution version_id delay_request parallel_prints; in (versions', blobs, commands, execution') end); fun the_version (State {versions, ...}) version_id = (case Inttab.lookup versions version_id of NONE => err_undef "document version" version_id | SOME version => version); fun delete_version version_id versions = Inttab.delete version_id versions handle Inttab.UNDEF _ => err_undef "document version" version_id; (* inlined files *) fun define_blob digest text = map_state (fn (versions, blobs, commands, execution) => let val blobs' = Symtab.update (digest, (SHA1.fake digest, split_lines text)) blobs in (versions, blobs', commands, execution) end); fun the_blob (State {blobs, ...}) digest = (case Symtab.lookup blobs digest of NONE => error ("Undefined blob: " ^ digest) | SOME content => content); fun resolve_blob state (blob_digest: blob_digest) = blob_digest |> Exn.map_res (fn {file_node, src_path, digest} => {file_node = file_node, src_path = src_path, content = Option.map (the_blob state) digest}); (* commands *) type command = {command_id: Document_ID.command, name: string, parents: string list, blobs_digests: blob_digest list, blobs_index: int, tokens: ((int * int) * string) list}; fun define_command {command_id, name, parents, blobs_digests, blobs_index, tokens} = map_state (fn (versions, blobs, commands, execution) => let val id = Document_ID.print command_id; val span = Lazy.lazy_name "Document.define_command" (fn () => Position.setmp_thread_data (Position.id_only id) (fn () => let val (tokens, _) = fold_map Token.make tokens (Position.id id); val imports = if name = Thy_Header.theoryN then (#imports (Thy_Header.read_tokens Position.none tokens) handle ERROR _ => []) else []; val _ = if length parents = length imports then (parents, imports) |> ListPair.app (fn (parent, (_, pos)) => let val markup = (case Thy_Info.lookup_theory parent of SOME thy => Theory.get_markup thy | NONE => (case try Url.explode parent of SOME (Url.File path) => Markup.path (Path.implode path) | _ => Markup.path parent)) in Position.report pos markup end) else (); val _ = if blobs_index < 0 then (*inlined errors*) map_filter Exn.get_exn blobs_digests |> List.app (Output.error_message o Runtime.exn_message) else (*auxiliary files*) let val pos = Token.pos_of (nth tokens blobs_index); fun reports (Exn.Res {file_node, ...}) = [(pos, Markup.path file_node)] | reports _ = []; in Position.reports (maps reports blobs_digests) end; in tokens end) ()); val commands' = Inttab.update_new (command_id, (name, blobs_digests, blobs_index, span)) commands handle Inttab.DUP dup => err_dup "command" dup; in (versions, blobs, commands', execution) end); fun the_command (State {commands, ...}) command_id = (case Inttab.lookup commands command_id of NONE => err_undef "command" command_id | SOME command => command); (* execution *) fun get_execution (State {execution, ...}) = execution; fun get_execution_version state = the_version state (#version_id (get_execution state)); fun command_exec state node_name command_id = let val version = get_execution_version state; val node = get_node (nodes_of version) node_name; in the_entry node command_id end; end; (* remove_versions *) fun remove_versions version_ids state = state |> map_state (fn (versions, _, _, execution) => let val _ = member (op =) version_ids (#version_id execution) andalso error ("Attempt to remove execution version " ^ Document_ID.print (#version_id execution)); val versions' = fold delete_version version_ids versions; val commands' = Inttab.build (versions' |> Inttab.fold (fn (_, version) => nodes_of version |> String_Graph.fold (fn (_, (node, _)) => node |> iterate_entries (fn ((_, command_id), _) => SOME o Inttab.insert (K true) (command_id, the_command state command_id))))); val blobs' = Symtab.build (commands' |> Inttab.fold (fn (_, (_, blobs, _, _)) => blobs |> fold (fn Exn.Res {digest = SOME b, ...} => Symtab.update (b, the_blob state b) | _ => I))); in (versions', blobs', commands', execution) end); (* document execution *) fun make_required nodes = let fun all_preds P = String_Graph.fold (fn (a, (node, _)) => P node ? cons a) nodes [] |> String_Graph.all_preds nodes - |> Symtab.make_set; + |> Symset.make; val all_visible = all_preds visible_node; val all_required = all_preds required_node; in - Symtab.fold (fn (a, ()) => - exists (Symtab.defined all_visible) (String_Graph.immediate_succs nodes a) ? - Symtab.update (a, ())) all_visible all_required + Symset.fold (fn a => + exists (Symset.member all_visible) (String_Graph.immediate_succs nodes a) ? + Symset.insert a) all_visible all_required end; fun start_execution state = state |> map_state (fn (versions, blobs, commands, execution) => timeit "Document.start_execution" (fn () => let val {version_id, execution_id, delay_request, parallel_prints} = execution; val delay = seconds (Options.default_real \<^system_option>\editor_execution_delay\); val _ = Future.cancel delay_request; val delay_request' = Event_Timer.future {physical = true} (Time.now () + delay); val delay = Future.task_of delay_request'; val parallel_prints' = parallel_prints |> map_filter (Command.exec_parallel_prints execution_id [delay]); fun finished_import (name, (node, _)) = finished_result node orelse Thy_Info.defined_theory name; val nodes = nodes_of (the_version state version_id); val required = make_required nodes; val _ = nodes |> String_Graph.schedule (fn deps => fn (name, node) => - if Symtab.defined required name orelse visible_node node orelse pending_result node then + if Symset.member required name orelse visible_node node orelse pending_result node then let val future = (singleton o Future.forks) {name = "theory:" ^ name, group = SOME (Future.new_group NONE), deps = delay :: Execution.active_tasks name @ maps (the_list o #2 o #2) deps, pri = 0, interrupts = false} (fn () => (Execution.worker_task_active true name; if forall finished_import deps then iterate_entries (fn (_, opt_exec) => fn () => (case opt_exec of SOME exec => if Execution.is_running execution_id then SOME (Command.exec execution_id exec) else NONE | NONE => NONE)) node () else (); Execution.worker_task_active false name) handle exn => (Output.system_message (Runtime.exn_message exn); Execution.worker_task_active false name; Exn.reraise exn)); in (node, SOME (Future.task_of future)) end else (node, NONE)); val execution' = {version_id = version_id, execution_id = execution_id, delay_request = delay_request', parallel_prints = parallel_prints'}; in (versions, blobs, commands, execution') end)); (** document update **) (* exec state assignment *) type assign_update = Command.exec option Inttab.table; (*command id -> exec*) val assign_update_empty: assign_update = Inttab.empty; fun assign_update_defined (tab: assign_update) command_id = Inttab.defined tab command_id; fun assign_update_change entry (tab: assign_update) : assign_update = Inttab.update entry tab; fun assign_update_apply (tab: assign_update) node = Inttab.fold assign_entry tab node; fun assign_update_new upd (tab: assign_update) : assign_update = Inttab.update_new upd tab handle Inttab.DUP dup => err_dup "exec state assignment" dup; fun assign_update_result (tab: assign_update) = Inttab.fold (fn (command_id, exec) => cons (command_id, Command.exec_ids exec)) tab []; (* update *) local fun init_theory deps node span = let val master_dir = master_directory node; val header = read_header node span; val imports = #imports header; fun maybe_eval_result eval = Command.eval_result_state eval handle Fail _ => Toplevel.make_state NONE; fun maybe_end_theory pos st = SOME (Toplevel.end_theory pos st) handle ERROR msg => (Output.error_message msg; NONE); val parents_reports = imports |> map_filter (fn (import, pos) => (case Thy_Info.lookup_theory import of NONE => maybe_end_theory pos (case get_result (snd (the (AList.lookup (op =) deps import))) of NONE => Toplevel.make_state NONE | SOME (_, eval) => maybe_eval_result eval) |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy))) | SOME thy => SOME (thy, (Position.none, Markup.empty)))); val parents = if null parents_reports then [Theory.get_pure ()] else map #1 parents_reports; val _ = List.app (fn (thy, r) => Context_Position.reports_global thy [r]) parents_reports; val thy = Resources.begin_theory master_dir header parents; val _ = Output.status [Markup.markup_only Markup.initialized]; in thy end; fun get_special_parent node = let val master_dir = master_directory node; val header as {name = (name, _), ...} = #header (get_header node); val parent = if name = Sessions.root_name then SOME (Thy_Info.get_theory Sessions.theory_name) else if member (op =) Thy_Header.ml_roots name then SOME (Thy_Info.get_theory Thy_Header.ml_bootstrapN) else NONE; in parent |> Option.map (fn thy => Resources.begin_theory master_dir header [thy]) end; fun check_theory full name node = Thy_Info.defined_theory name orelse null (#errors (get_header node)) andalso (not full orelse is_some (get_result node)); fun last_common keywords the_command_name node_required node0 node = let fun update_flags prev (visible, initial) = let val visible' = visible andalso prev <> visible_last node; val initial' = initial andalso (case prev of NONE => true | SOME command_id => the_command_name command_id <> Thy_Header.theoryN); in (visible', initial') end; fun get_common ((prev, command_id), opt_exec) (_, ok, flags, assign_update) = if ok then let val flags' as (visible', _) = update_flags prev flags; val ok' = (case (lookup_entry node0 command_id, opt_exec) of (SOME (eval0, _), SOME (eval, _)) => Command.eval_eq (eval0, eval) andalso (visible' orelse node_required orelse Command.eval_running eval) | _ => false); val assign_update' = assign_update |> ok' ? (case opt_exec of SOME (eval, prints) => let val visible = command_visible node command_id; val overlays = command_overlays node command_id; val command_name = the_command_name command_id; in (case Command.print keywords visible overlays command_name eval prints of SOME prints' => assign_update_new (command_id, SOME (eval, prints')) | NONE => I) end | NONE => I); in SOME (prev, ok', flags', assign_update') end else NONE; val (common, ok, flags, assign_update') = iterate_entries get_common node (NONE, true, (true, true), assign_update_empty); val (common', flags') = if ok then let val last = Entries.get_after (get_entries node) common in (last, update_flags last flags) end else (common, flags); in (assign_update', common', flags') end; fun illegal_init _ = error "Illegal theory header"; fun new_exec keywords state node proper_init command_id' (assign_update, command_exec, init) = if not proper_init andalso is_none init then NONE else let val visible = command_visible node command_id'; val overlays = command_overlays node command_id'; val (command_name, blob_digests, blobs_index, span0) = the_command state command_id'; val blobs = map (resolve_blob state) blob_digests; val span = Lazy.force span0; val eval' = Command.eval keywords (master_directory node) (fn () => the_default illegal_init init span) (blobs, blobs_index) command_id' span (#1 (#2 command_exec)); val prints' = perhaps (Command.print keywords visible overlays command_name eval') []; val exec' = (eval', prints'); val assign_update' = assign_update_new (command_id', SOME exec') assign_update; val init' = if command_name = Thy_Header.theoryN then NONE else init; in SOME (assign_update', (command_id', exec'), init') end; fun removed_execs node0 (command_id, exec_ids) = subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id)); fun finished_eval node = let val active = (node, false) |-> iterate_entries (fn (_, opt_exec) => fn active => if active then NONE else (case opt_exec of NONE => SOME true | SOME (eval, _) => SOME (not (null (Execution.snapshot [Command.eval_exec_id eval]))))); in not active end; fun presentation_context options the_command_span node_name node : Thy_Info.presentation_context = let val (_, offsets, rev_segments) = (node, (0, Inttab.empty, [])) |-> iterate_entries (fn ((prev, id), opt_exec) => fn (offset, offsets, segments) => (case opt_exec of SOME (eval, _) => let val command_id = Command.eval_command_id eval; val span = the_command_span command_id; val st = (case try (#1 o the o the_entry node o the) prev of NONE => Toplevel.make_state NONE | SOME prev_eval => Command.eval_result_state prev_eval); val exec_id = Command.eval_exec_id eval; val tr = Command.eval_result_command eval; val st' = Command.eval_result_state eval; val offset' = offset + the_default 0 (Command_Span.symbol_length span); val offsets' = offsets |> Inttab.update (command_id, offset) |> Inttab.update (exec_id, offset); val segments' = (span, (st, tr, st')) :: segments; in SOME (offset', offsets', segments') end | NONE => raise Fail ("Unassigned exec " ^ Value.print_int id))); val adjust = Inttab.lookup offsets; val segments = rev rev_segments |> map (fn (span, (st, tr, st')) => {span = Command_Span.adjust_offsets adjust span, prev_state = st, command = tr, state = st'}); in {options = options, file_pos = Position.file node_name, adjust_pos = Position.adjust_offsets adjust, segments = segments} end; fun print_consolidation options the_command_span node_name (assign_update, node) = timeit "Document.print_consolidation" (fn () => (case finished_result_theory node of SOME (id, thy) => if finished_eval node then let val context = presentation_context options the_command_span node_name node; val consolidate = Command.print0 {pri = Task_Queue.urgent_pri + 1, print_fn = fn _ => fn _ => let val _ = Output.status [Markup.markup_only Markup.consolidating]; val res = Exn.capture (Thy_Info.apply_presentation context) thy; val _ = Lazy.force (get_consolidated node); val _ = Output.status [Markup.markup_only Markup.consolidated]; in Exn.release res end}; val result_entry = (case lookup_entry node id of NONE => err_undef "result command entry" id | SOME (eval, prints) => (id, SOME (eval, consolidate eval :: prints))); val assign_update' = assign_update |> assign_update_change result_entry; val node' = node |> assign_entry result_entry; in (assign_update', node') end else (assign_update, node) | NONE => (assign_update, node))); in fun update old_version_id new_version_id edits consolidate state = Runtime.exn_trace_system (fn () => let val options = Options.default (); val the_command_name = #1 o the_command state; val the_command_span = Outer_Syntax.make_span o Lazy.force o #4 o the_command state; val old_version = the_version state old_version_id; val new_version = timeit "Document.edit_nodes" (fn () => old_version |> fold edit_nodes edits |> edit_keywords edits); - val consolidate = Symtab.defined (Symtab.make_set consolidate); + val consolidate = Symset.member (Symset.make consolidate); val nodes = nodes_of new_version; val required = make_required nodes; val required0 = make_required (nodes_of old_version); - val edited = Symtab.build (edits |> fold (Symtab.insert_set o #1)); + val edited = Symset.build (edits |> fold (Symset.insert o #1)); val updated = timeit "Document.update" (fn () => nodes |> String_Graph.schedule (fn deps => fn (name, node) => (singleton o Future.forks) {name = "Document.update", group = NONE, deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false} (fn () => timeit ("Document.update " ^ name) (fn () => Runtime.exn_trace_system (fn () => let val special_parent = get_special_parent node; val keywords = node_keywords name node; val maybe_consolidate = consolidate name andalso could_consolidate node; val imports = map (apsnd Future.join) deps; val imports_result_changed = exists (#4 o #1 o #2) imports; - val node_required = Symtab.defined required name; + val node_required = Symset.member required name; in - if Symtab.defined edited name orelse maybe_consolidate orelse + if Symset.member edited name orelse maybe_consolidate orelse visible_node node orelse imports_result_changed orelse - Symtab.defined required0 name <> node_required + Symset.member required0 name <> node_required then let val node0 = node_of old_version name; val init = init_theory imports node; val proper_init = is_some special_parent orelse check_theory false name node andalso forall (fn (name, (_, node)) => check_theory true name node) imports; val (print_execs, common, (still_visible, initial)) = if imports_result_changed then (assign_update_empty, NONE, (true, true)) else last_common keywords the_command_name node_required node0 node; val common_command_exec = (case common of SOME id => (id, the_default Command.no_exec (the_entry node id)) | NONE => (Document_ID.none, Command.init_exec special_parent)); val (updated_execs, (command_id', exec'), _) = (print_execs, common_command_exec, if initial then SOME init else NONE) |> (still_visible orelse node_required) ? iterate_entries_after common (fn ((prev, id), _) => fn res => if not node_required andalso prev = visible_last node then NONE else new_exec keywords state node proper_init id res) node; val assign_update = (node0, updated_execs) |-> iterate_entries_after common (fn ((_, command_id0), exec0) => fn res => if is_none exec0 then NONE else if assign_update_defined updated_execs command_id0 then SOME res else SOME (assign_update_new (command_id0, NONE) res)); val last_exec = if command_id' = Document_ID.none then NONE else SOME command_id'; val result = if is_none last_exec orelse is_some (after_entry node last_exec) then NONE else SOME (command_id', #1 exec'); val result_changed = not (eq_option (Command.eval_eq o apply2 #2) (get_result node0, result)); val (assign_update', node') = node |> assign_update_apply assign_update |> set_result result |> result_changed ? reset_consolidated |> pair assign_update |> (not result_changed andalso maybe_consolidate) ? print_consolidation options the_command_span name; val assign_result = assign_update_result assign_update'; val removed = maps (removed_execs node0) assign_result; val _ = List.app Execution.cancel removed; val assigned_node = SOME (name, node'); in ((removed, assign_result, assigned_node, result_changed), node') end else (([], [], NONE, false), node) end)))) |> Future.joins |> map #1); val removed = maps #1 updated; val assign_result = maps #2 updated; val assigned_nodes = map_filter #3 updated; val state' = state |> define_version new_version_id new_version assigned_nodes; - in (Symtab.keys edited, removed, assign_result, state') end); + in (Symset.dest edited, removed, assign_result, state') end); end; (** global state **) val global_state = Synchronized.var "Document.global_state" init_state; fun state () = Synchronized.value global_state; val change_state = Synchronized.change global_state; end; diff --git a/src/Pure/PIDE/resources.ML b/src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML +++ b/src/Pure/PIDE/resources.ML @@ -1,483 +1,483 @@ (* Title: Pure/PIDE/resources.ML Author: Makarius Resources for theories and auxiliary files. *) signature RESOURCES = sig val default_qualifier: string val init_session: {session_positions: (string * Properties.T) list, session_directories: (string * string) list, command_timings: Properties.T list, load_commands: (string * Position.T) list, scala_functions: (string * ((bool * bool) * Position.T)) list, global_theories: (string * string) list, loaded_theories: string list} -> unit val init_session_yxml: Bytes.T -> unit val init_session_env: unit -> unit val finish_session_base: unit -> unit val global_theory: string -> string option val loaded_theory: string -> bool val check_session: Proof.context -> string * Position.T -> string val last_timing: Toplevel.transition -> Time.time val check_load_command: Proof.context -> string * Position.T -> string val check_scala_function: Proof.context -> string * Position.T -> string * (bool * bool) val master_directory: theory -> Path.T val imports_of: theory -> (string * Position.T) list val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory val thy_path: Path.T -> Path.T val theory_qualifier: string -> string val find_theory_file: string -> Path.T option val import_name: string -> Path.T -> string -> {node_name: Path.T, master_dir: Path.T, theory_name: string} val check_thy: Path.T -> string -> {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T, imports: (string * Position.T) list, keywords: Thy_Header.keywords} val read_file_node: string -> Path.T -> Path.T * Position.T -> Token.file val read_file: Path.T -> Path.T * Position.T -> Token.file val parsed_files: (Path.T -> Path.T list) -> Token.file Exn.result list * Input.source -> theory -> Token.file list val parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list) parser val parse_file: (theory -> Token.file) parser val provide: Path.T * SHA1.digest -> theory -> theory val provide_file: Token.file -> theory -> theory val provide_file': Token.file -> theory -> Token.file * theory val provide_parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list * theory) parser val provide_parse_file: (theory -> Token.file * theory) parser val loaded_files_current: theory -> bool val check_path: Proof.context -> Path.T option -> Input.source -> Path.T val check_file: Proof.context -> Path.T option -> Input.source -> Path.T val check_dir: Proof.context -> Path.T option -> Input.source -> Path.T val check_session_dir: Proof.context -> Path.T option -> Input.source -> Path.T end; structure Resources: RESOURCES = struct (* command timings *) type timings = ((string * Time.time) Inttab.table) Symtab.table; (*file -> offset -> name, time*) val empty_timings: timings = Symtab.empty; fun update_timings props = (case Markup.parse_command_timing_properties props of SOME ({file, offset, name}, time) => Symtab.map_default (file, Inttab.empty) (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, t + time))) | NONE => I); fun make_timings command_timings = fold update_timings command_timings empty_timings; fun approximative_id name pos = (case (Position.file_of pos, Position.offset_of pos) of (SOME file, SOME offset) => if name = "" then NONE else SOME {file = file, offset = offset, name = name} | _ => NONE); fun get_timings timings tr = (case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of SOME {file, offset, name} => (case Symtab.lookup timings file of SOME offsets => (case Inttab.lookup offsets offset of SOME (name', time) => if name = name' then SOME time else NONE | NONE => NONE) | NONE => NONE) | NONE => NONE) |> the_default Time.zeroTime; (* session base *) val default_qualifier = "Draft"; type entry = {pos: Position.T, serial: serial}; fun make_entry props : entry = {pos = Position.of_properties props, serial = serial ()}; val empty_session_base = ({session_positions = []: (string * entry) list, session_directories = Symtab.empty: Path.T list Symtab.table, timings = empty_timings, load_commands = []: (string * Position.T) list, scala_functions = Symtab.empty: ((bool * bool) * Position.T) Symtab.table}, {global_theories = Symtab.empty: string Symtab.table, - loaded_theories = Symtab.empty: unit Symtab.table}); + loaded_theories = Symset.empty: Symset.T}); val global_session_base = Synchronized.var "Sessions.base" empty_session_base; fun init_session {session_positions, session_directories, command_timings, load_commands, scala_functions, global_theories, loaded_theories} = Synchronized.change global_session_base (fn _ => ({session_positions = sort_by #1 (map (apsnd make_entry) session_positions), session_directories = Symtab.build (session_directories |> fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir))), timings = make_timings command_timings, load_commands = load_commands, scala_functions = Symtab.make scala_functions}, {global_theories = Symtab.make global_theories, - loaded_theories = Symtab.make_set loaded_theories})); + loaded_theories = Symset.make loaded_theories})); fun init_session_yxml yxml = let val (session_positions, (session_directories, (command_timings, (load_commands, (scala_functions, (global_theories, loaded_theories)))))) = YXML.parse_body_bytes yxml |> let open XML.Decode in (pair (list (pair string properties)) (pair (list (pair string string)) (pair (list properties) (pair (list (pair string properties)) (pair (list (pair string (pair (pair bool bool) properties))) (pair (list (pair string string)) (list string))))))) end; in init_session {session_positions = session_positions, session_directories = session_directories, command_timings = command_timings, load_commands = (map o apsnd) Position.of_properties load_commands, scala_functions = (map o apsnd o apsnd) Position.of_properties scala_functions, global_theories = global_theories, loaded_theories = loaded_theories} end; fun init_session_env () = (case getenv "ISABELLE_INIT_SESSION" of "" => () | name => try Bytes.read (Path.explode name) |> Option.app init_session_yxml); val _ = init_session_env (); fun finish_session_base () = Synchronized.change global_session_base (apfst (K (#1 empty_session_base))); fun get_session_base f = f (Synchronized.value global_session_base); fun get_session_base1 f = get_session_base (f o #1); fun get_session_base2 f = get_session_base (f o #2); fun global_theory a = Symtab.lookup (get_session_base2 #global_theories) a; -fun loaded_theory a = Symtab.defined (get_session_base2 #loaded_theories) a; +fun loaded_theory a = Symset.member (get_session_base2 #loaded_theories) a; fun check_session ctxt arg = Completion.check_item "session" (fn (name, {pos, serial}) => Position.make_entity_markup {def = false} serial Markup.sessionN (name, pos)) (get_session_base1 #session_positions) ctxt arg; fun last_timing tr = get_timings (get_session_base1 #timings) tr; fun check_load_command ctxt arg = Completion.check_entity Markup.load_commandN (get_session_base1 #load_commands) ctxt arg; (* Scala functions *) fun check_scala_function ctxt arg = let val table = get_session_base1 #scala_functions; val funs = Symtab.fold (fn (a, (_, pos)) => cons (a, pos)) table [] |> sort_by #1; val name = Completion.check_entity Markup.scala_functionN funs ctxt arg; val flags = #1 (the (Symtab.lookup table name)); in (name, flags) end; val _ = Theory.setup (Document_Output.antiquotation_verbatim_embedded \<^binding>\scala_function\ (Scan.lift Parse.embedded_position) (#1 oo check_scala_function) #> ML_Antiquotation.inline_embedded \<^binding>\scala_function\ (Args.context -- Scan.lift Parse.embedded_position >> (uncurry check_scala_function #> #1 #> ML_Syntax.print_string)) #> ML_Antiquotation.value_embedded \<^binding>\scala\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, arg) => let val (name, (single, bytes)) = check_scala_function ctxt arg; val func = (if single then "Scala.function1" else "Scala.function") ^ (if bytes then "_bytes" else ""); in ML_Syntax.atomic (func ^ " " ^ ML_Syntax.print_string name) end))); (* manage source files *) type files = {master_dir: Path.T, (*master directory of theory source*) imports: (string * Position.T) list, (*source specification of imports*) provided: (Path.T * SHA1.digest) list}; (*source path, digest*) fun make_files (master_dir, imports, provided): files = {master_dir = master_dir, imports = imports, provided = provided}; structure Files = Theory_Data ( type T = files; val empty = make_files (Path.current, [], []); fun merge ({master_dir, imports, provided = provided1}, {provided = provided2, ...}) = let val provided' = Library.merge (op =) (provided1, provided2) in make_files (master_dir, imports, provided') end ); fun map_files f = Files.map (fn {master_dir, imports, provided} => make_files (f (master_dir, imports, provided))); val master_directory = #master_dir o Files.get; val imports_of = #imports o Files.get; fun begin_theory master_dir {name, imports, keywords} parents = let val thy = Theory.begin_theory name parents |> map_files (fn _ => (Path.explode (File.symbolic_path master_dir), imports, [])) |> Thy_Header.add_keywords keywords; val ctxt = Proof_Context.init_global thy; val _ = List.app (ignore o check_load_command ctxt o #load_command o #2) keywords; in thy end; (* theory files *) val thy_path = Path.ext "thy"; fun theory_qualifier theory = (case global_theory theory of SOME qualifier => qualifier | NONE => Long_Name.qualifier theory); fun literal_theory theory = Long_Name.is_qualified theory orelse is_some (global_theory theory); fun theory_name qualifier theory = if literal_theory theory then theory else Long_Name.qualify qualifier theory; fun find_theory_file thy_name = let val thy_file = thy_path (Path.basic (Long_Name.base_name thy_name)); val session = theory_qualifier thy_name; val dirs = Symtab.lookup_list (get_session_base1 #session_directories) session; in dirs |> get_first (fn dir => let val path = dir + thy_file in if File.is_file path then SOME path else NONE end) end; fun make_theory_node node_name theory = {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory}; fun loaded_theory_node theory = {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory}; fun import_name qualifier dir s = let val theory = theory_name qualifier (Thy_Header.import_name s); fun theory_node path = make_theory_node path theory; val literal_import = literal_theory theory andalso qualifier <> theory_qualifier theory; val _ = if literal_import andalso not (Thy_Header.is_base_name s) then error ("Bad import of theory from other session via file-path: " ^ quote s) else (); in if loaded_theory theory then loaded_theory_node theory else (case find_theory_file theory of SOME node_name => theory_node node_name | NONE => if Thy_Header.is_base_name s andalso Long_Name.is_qualified s then loaded_theory_node theory else theory_node (File.full_path dir (thy_path (Path.expand (Path.explode s))))) end; fun check_file dir file = File.check_file (File.full_path dir file); fun check_thy dir thy_name = let val thy_base_name = Long_Name.base_name thy_name; val master_file = (case find_theory_file thy_name of SOME path => check_file Path.current path | NONE => check_file dir (thy_path (Path.basic thy_base_name))); val text = File.read master_file; val {name = (name, pos), imports, keywords} = Thy_Header.read (Position.file (File.symbolic_path master_file)) text; val _ = thy_base_name <> name andalso error ("Bad theory name " ^ quote name ^ " for file " ^ Path.print (Path.base master_file) ^ Position.here pos); in {master = (master_file, SHA1.digest text), text = text, theory_pos = pos, imports = imports, keywords = keywords} end; (* read_file *) fun read_file_node file_node master_dir (src_path, pos) = let fun read_local () = let val path = File.check_file (File.full_path master_dir src_path); val text = File.read path; val file_pos = Position.file (File.symbolic_path path); in (text, file_pos) end; fun read_remote () = let val text = Bytes.content (Isabelle_System.download file_node); val file_pos = Position.file file_node; in (text, file_pos) end; val (text, file_pos) = (case try Url.explode file_node of NONE => read_local () | SOME (Url.File _) => read_local () | _ => read_remote ()); val lines = split_lines text; val digest = SHA1.digest text; in {src_path = src_path, lines = lines, digest = digest, pos = Position.copy_id pos file_pos} end handle ERROR msg => error (msg ^ Position.here pos); val read_file = read_file_node ""; (* load files *) fun parsed_files make_paths (files, source) thy = if null files then let val master_dir = master_directory thy; val name = Input.string_of source; val pos = Input.pos_of source; val delimited = Input.is_delimited source; val src_paths = make_paths (Path.explode name); val reports = src_paths |> maps (fn src_path => [(pos, Markup.path (File.symbolic_path (master_dir + src_path))), (pos, Markup.language_path delimited)]); val _ = Position.reports reports; in map (read_file master_dir o rpair pos) src_paths end else map Exn.release files; fun parse_files make_paths = (Scan.ahead Parse.not_eof >> Token.get_files) -- Parse.path_input >> parsed_files make_paths; val parse_file = parse_files single >> (fn f => f #> the_single); fun provide (src_path, id) = map_files (fn (master_dir, imports, provided) => if AList.defined (op =) provided src_path then error ("Duplicate use of source file: " ^ Path.print src_path) else (master_dir, imports, (src_path, id) :: provided)); fun provide_file (file: Token.file) = provide (#src_path file, #digest file); fun provide_file' file thy = (file, provide_file file thy); fun provide_parse_files make_paths = parse_files make_paths >> (fn files => fn thy => fold_map provide_file' (files thy) thy); val provide_parse_file = provide_parse_files single >> (fn f => f #>> the_single); fun load_file thy src_path = let val full_path = check_file (master_directory thy) src_path; val text = File.read full_path; val id = SHA1.digest text; in ((full_path, id), text) end; fun loaded_files_current thy = #provided (Files.get thy) |> forall (fn (src_path, id) => (case try (load_file thy) src_path of NONE => false | SOME ((_, id'), _) => id = id')); (* formal check *) fun formal_check (check: Path.T -> Path.T) ctxt opt_dir source = let val name = Input.string_of source; val pos = Input.pos_of source; val delimited = Input.is_delimited source; val _ = Context_Position.report ctxt pos (Markup.language_path delimited); fun err msg = error (msg ^ Position.here pos); val dir = (case opt_dir of SOME dir => dir | NONE => master_directory (Proof_Context.theory_of ctxt)); val path = dir + Path.explode name handle ERROR msg => err msg; val _ = Path.expand path handle ERROR msg => err msg; val _ = Context_Position.report ctxt pos (Markup.path (File.symbolic_path path)); val _ = check path handle ERROR msg => err msg; in path end; val check_path = formal_check I; val check_file = formal_check File.check_file; val check_dir = formal_check File.check_dir; fun check_session_dir ctxt opt_dir s = let val dir = Path.expand (check_dir ctxt opt_dir s); val ok = File.is_file (dir + Path.explode("ROOT")) orelse File.is_file (dir + Path.explode("ROOTS")); in if ok then dir else error ("Bad session root directory (missing ROOT or ROOTS): " ^ Path.print dir ^ Position.here (Input.pos_of s)) end; (* antiquotations *) local fun document_antiq (check: Proof.context -> Path.T option -> Input.source -> Path.T) = Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) => (check ctxt NONE source; Latex.string (Latex.output_ascii_breakable "/" (Input.string_of source)) |> Latex.macro "isatt")); fun ML_antiq check = Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) => check ctxt (SOME Path.current) source |> ML_Syntax.print_path); in val _ = Theory.setup (Document_Output.antiquotation_verbatim_embedded \<^binding>\session\ (Scan.lift Parse.embedded_position) check_session #> Document_Output.antiquotation_raw_embedded \<^binding>\path\ (document_antiq check_path) (K I) #> Document_Output.antiquotation_raw_embedded \<^binding>\file\ (document_antiq check_file) (K I) #> Document_Output.antiquotation_raw_embedded \<^binding>\dir\ (document_antiq check_dir) (K I) #> ML_Antiquotation.value_embedded \<^binding>\path\ (ML_antiq check_path) #> ML_Antiquotation.value_embedded \<^binding>\file\ (ML_antiq check_file) #> ML_Antiquotation.value_embedded \<^binding>\dir\ (ML_antiq check_dir) #> ML_Antiquotation.value_embedded \<^binding>\path_binding\ (Scan.lift (Parse.position Parse.path) >> (ML_Syntax.print_path_binding o Path.explode_binding)) #> ML_Antiquotation.value \<^binding>\master_dir\ (Args.theory >> (ML_Syntax.print_path o master_directory))); end; end; diff --git a/src/Pure/Syntax/parser.ML b/src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML +++ b/src/Pure/Syntax/parser.ML @@ -1,724 +1,724 @@ (* Title: Pure/Syntax/parser.ML Author: Carsten Clasohm, Sonia Mahjoub Author: Makarius General context-free parser for the inner syntax of terms and types. *) signature PARSER = sig type gram val empty_gram: gram val extend_gram: Syntax_Ext.xprod list -> gram -> gram val make_gram: Syntax_Ext.xprod list -> gram val pretty_gram: gram -> Pretty.T list datatype parsetree = Node of string * parsetree list | Tip of Lexicon.token exception PARSETREE of parsetree val pretty_parsetree: parsetree -> Pretty.T val parse: gram -> string -> Lexicon.token list -> parsetree list val branching_level: int Config.T end; structure Parser: PARSER = struct (** datatype gram **) (* nonterminals *) (*production for the NTs are stored in a vector, indexed by the NT tag*) type nt = int; type tags = nt Symtab.table; val tags_empty: tags = Symtab.empty; fun tags_content (tags: tags) = sort_by #1 (Symtab.dest tags); fun tags_lookup (tags: tags) = Symtab.lookup tags; fun tags_insert tag (tags: tags) = Symtab.update_new tag tags; fun tags_name (tags: tags) = the o Inttab.lookup (Inttab.make (map swap (Symtab.dest tags))); -type nts = Inttab.set; -val nts_empty: nts = Inttab.empty; -val nts_merge: nts * nts -> nts = Inttab.merge (K true); -fun nts_insert nt : nts -> nts = Inttab.insert_set nt; -fun nts_member (nts: nts) = Inttab.defined nts; -fun nts_fold f (nts: nts) = Inttab.fold (f o #1) nts; -fun nts_subset (nts1: nts, nts2: nts) = Inttab.forall (nts_member nts2 o #1) nts1; -fun nts_is_empty (nts: nts) = Inttab.is_empty nts; -fun nts_is_unique (nts: nts) = nts_is_empty nts orelse Inttab.is_single nts; +type nts = Intset.T; +val nts_empty: nts = Intset.empty; +val nts_merge: nts * nts -> nts = Intset.merge; +fun nts_insert nt : nts -> nts = Intset.insert nt; +fun nts_member (nts: nts) = Intset.member nts; +fun nts_fold f (nts: nts) = Intset.fold f nts; +fun nts_subset (nts1: nts, nts2: nts) = Intset.forall (nts_member nts2) nts1; +fun nts_is_empty (nts: nts) = Intset.is_empty nts; +fun nts_is_unique (nts: nts) = nts_is_empty nts orelse Intset.is_single nts; (* tokens *) structure Tokens = Table(type key = Lexicon.token val ord = Lexicon.tokens_match_ord); type tokens = Tokens.set; val tokens_empty: tokens = Tokens.empty; val tokens_merge: tokens * tokens -> tokens = Tokens.merge (K true); fun tokens_insert tk : tokens -> tokens = Tokens.insert_set tk; fun tokens_remove tk : tokens -> tokens = Tokens.remove_set tk; fun tokens_member (tokens: tokens) = Tokens.defined tokens; fun tokens_is_empty (tokens: tokens) = Tokens.is_empty tokens; fun tokens_fold f (tokens: tokens) = Tokens.fold (f o #1) tokens; val tokens_union = tokens_fold tokens_insert; val tokens_subtract = tokens_fold tokens_remove; fun tokens_find P (tokens: tokens) = Tokens.get_first (fn (tok, ()) => if P tok then SOME tok else NONE) tokens; fun tokens_add (nt: nt, tokens) = if tokens_is_empty tokens then I else cons (nt, tokens); (* productions *) datatype symb = Terminal of Lexicon.token | Nonterminal of nt * int; (*(tag, prio)*) type prods = (symb list * string * int) list Tokens.table; (*start_token ~> [(rhs, name, prio)]*) val prods_empty: prods = Tokens.empty; fun prods_lookup (prods: prods) = Tokens.lookup_list prods; fun prods_update entry : prods -> prods = Tokens.update entry; fun prods_content (prods: prods) = distinct (op =) (maps #2 (Tokens.dest prods)); type nt_gram = (nts * tokens) * prods; (*dependent_nts, start_tokens, prods*) (*depent_nts is a set of all NTs whose lookahead depends on this NT's lookahead*) val nt_gram_empty: nt_gram = ((nts_empty, tokens_empty), prods_empty); type chains = unit Int_Graph.T; fun chains_preds (chains: chains) = Int_Graph.immediate_preds chains; fun chains_all_preds (chains: chains) = Int_Graph.all_preds chains; fun chains_all_succs (chains: chains) = Int_Graph.all_succs chains; val chains_empty: chains = Int_Graph.empty; fun chains_member (chains: chains) = Int_Graph.is_edge chains; fun chains_declare nt : chains -> chains = Int_Graph.default_node (nt, ()); fun chains_insert (from, to) = chains_declare from #> chains_declare to #> Int_Graph.add_edge (from, to); datatype gram = Gram of {nt_count: int, prod_count: int, tags: tags, chains: chains, lambdas: nts, prods: nt_gram Vector.vector}; (*"tags" is used to map NT names (i.e. strings) to tags; chain productions are not stored as normal productions but instead as an entry in "chains": from -> to; lambda productions are stored as normal productions and also as an entry in "lambdas"*) (*productions for which no starting token is known yet are associated with this token*) val unknown_start = Lexicon.eof; fun get_start tks = (case Tokens.min tks of SOME (tk, _) => tk | NONE => unknown_start); fun add_production prods (lhs, new_prod as (rhs, _, pri)) (chains, lambdas) = let (*store chain if it does not already exist*) val (chain, new_chain, chains') = (case (pri, rhs) of (~1, [Nonterminal (from, ~1)]) => if chains_member chains (from, lhs) then (SOME from, false, chains) else (SOME from, true, chains_insert (from, lhs) chains) | _ => let val chains' = chains |> chains_declare lhs |> fold (fn Nonterminal (nt, _) => chains_declare nt | _ => I) rhs; in (NONE, false, chains') end); (*propagate new chain in lookahead and lambdas; added_starts is used later to associate existing productions with new starting tokens*) val (added_starts, lambdas') = if not new_chain then ([], lambdas) else let (*lookahead of chain's source*) val ((_, from_tks), _) = Array.sub (prods, the chain); (*copy from's lookahead to chain's destinations*) fun copy_lookahead to = let val ((to_nts, to_tks), ps) = Array.sub (prods, to); val new_tks = tokens_subtract to_tks from_tks; (*added lookahead tokens*) val to_tks' = tokens_merge (to_tks, new_tks); val _ = Array.update (prods, to, ((to_nts, to_tks'), ps)); in tokens_add (to, new_tks) end; val tos = chains_all_succs chains' [lhs]; in (fold copy_lookahead tos [], lambdas |> nts_member lambdas lhs ? fold nts_insert tos) end; (*test if new production can produce lambda (rhs must either be empty or only consist of lambda NTs)*) val new_lambdas = if forall (fn Nonterminal (id, _) => nts_member lambdas' id | Terminal _ => false) rhs then SOME (filter_out (nts_member lambdas') (chains_all_succs chains' [lhs])) else NONE; val lambdas'' = fold nts_insert (these new_lambdas) lambdas'; (*list optional terminal and all nonterminals on which the lookahead of a production depends*) fun lookahead_dependency _ [] nts = (NONE, nts) | lookahead_dependency _ (Terminal tk :: _) nts = (SOME tk, nts) | lookahead_dependency lambdas (Nonterminal (nt, _) :: symbs) nts = if nts_member lambdas nt then lookahead_dependency lambdas symbs (nts_insert nt nts) else (NONE, nts_insert nt nts); (*get all known starting tokens for a nonterminal*) fun starts_for_nt nt = snd (fst (Array.sub (prods, nt))); (*update prods, lookaheads, and lambdas according to new lambda NTs*) val (added_starts', lambdas') = let (*propagate added lambda NT*) fun propagate_lambda [] added_starts lambdas = (added_starts, lambdas) | propagate_lambda (l :: ls) added_starts lambdas = let (*get lookahead for lambda NT*) val ((dependent, l_starts), _) = Array.sub (prods, l); (*check productions whose lookahead may depend on lambda NT*) fun examine_prods [] add_lambda nt_dependencies added_tks nt_prods = (add_lambda, nt_dependencies, added_tks, nt_prods) | examine_prods ((p as (rhs, _, _)) :: ps) add_lambda nt_dependencies added_tks nt_prods = let val (tk, nts) = lookahead_dependency lambdas rhs nts_empty in if nts_member nts l then (*update production's lookahead*) let val new_lambda = is_none tk andalso nts_subset (nts, lambdas); val new_tks = tokens_empty |> fold tokens_insert (the_list tk) |> nts_fold (tokens_union o starts_for_nt) nts |> tokens_subtract l_starts; val added_tks' = tokens_merge (added_tks, new_tks); val nt_dependencies' = nts_merge (nt_dependencies, nts); (*associate production with new starting tokens*) fun copy tk nt_prods = prods_update (tk, p :: prods_lookup nt_prods tk) nt_prods; val nt_prods' = nt_prods |> tokens_fold copy new_tks |> new_lambda ? copy Lexicon.dummy; in examine_prods ps (add_lambda orelse new_lambda) nt_dependencies' added_tks' nt_prods' end else (*skip production*) examine_prods ps add_lambda nt_dependencies added_tks nt_prods end; (*check each NT whose lookahead depends on new lambda NT*) fun process_nts nt (added_lambdas, added_starts) = let val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt); (*existing productions whose lookahead may depend on l*) val tk_prods = prods_lookup nt_prods (get_start l_starts); (*add_lambda is true if an existing production of the nt produces lambda due to the new lambda NT l*) val (add_lambda, nt_dependencies, added_tks, nt_prods') = examine_prods tk_prods false nts_empty tokens_empty nt_prods; val new_nts = nts_merge (old_nts, nt_dependencies); val new_tks = tokens_merge (old_tks, added_tks); val added_lambdas' = added_lambdas |> add_lambda ? cons nt; val _ = Array.update (prods, nt, ((new_nts, new_tks), nt_prods')); (*N.B. that because the tks component is used to access existing productions we have to add new tokens at the _end_ of the list*) val added_starts' = tokens_add (nt, added_tks) added_starts; in (added_lambdas', added_starts') end; val (added_lambdas, added_starts') = nts_fold process_nts dependent ([], added_starts); val added_lambdas' = filter_out (nts_member lambdas) added_lambdas; in propagate_lambda (ls @ added_lambdas') added_starts' (fold nts_insert added_lambdas' lambdas) end; in propagate_lambda (nts_fold (fn l => not (nts_member lambdas l) ? cons l) lambdas'' []) added_starts lambdas'' end; (*insert production into grammar*) val added_starts' = if is_some chain then added_starts' (*don't store chain production*) else let (*lookahead tokens of new production and on which NTs lookahead depends*) val (start_tk, start_nts) = lookahead_dependency lambdas' rhs nts_empty; val start_tks = tokens_empty |> fold tokens_insert (the_list start_tk) |> nts_fold (tokens_union o starts_for_nt) start_nts; val start_tks' = start_tks |> (if is_some new_lambdas then tokens_insert Lexicon.dummy else if tokens_is_empty start_tks then tokens_insert unknown_start else I); (*add lhs NT to list of dependent NTs in lookahead*) fun add_nts nt initial = (if initial then let val ((old_nts, old_tks), ps) = Array.sub (prods, nt) in if nts_member old_nts lhs then () else Array.update (prods, nt, ((nts_insert lhs old_nts, old_tks), ps)) end else (); false); (*add new start tokens to chained NTs' lookahead list; also store new production for lhs NT*) fun add_tks [] added = added | add_tks (nt :: nts) added = let val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt); val new_tks = tokens_subtract old_tks start_tks; (*store new production*) fun store tk (prods, _) = let val tk_prods = prods_lookup prods tk; val tk_prods' = new_prod :: tk_prods; val prods' = prods_update (tk, tk_prods') prods; in (prods', true) end; val (nt_prods', changed) = (nt_prods, false) |> nt = lhs ? tokens_fold store start_tks'; val _ = if not changed andalso tokens_is_empty new_tks then () else Array.update (prods, nt, ((old_nts, tokens_merge (old_tks, new_tks)), nt_prods')); in add_tks nts (tokens_add (nt, new_tks) added) end; val _ = nts_fold add_nts start_nts true; in add_tks (chains_all_succs chains' [lhs]) [] end; (*associate productions with new lookaheads*) val _ = let (*propagate added start tokens*) fun add_starts [] = () | add_starts ((changed_nt, new_tks) :: starts) = let (*token under which old productions which depend on changed_nt could be stored*) val key = tokens_find (not o tokens_member new_tks) (starts_for_nt changed_nt) |> the_default unknown_start; (*copy productions whose lookahead depends on changed_nt; if key = SOME unknown_start then tk_prods is used to hold the productions not copied*) fun update_prods [] result = result | update_prods ((p as (rhs, _: string, _: nt)) :: ps) (tk_prods, nt_prods) = let (*lookahead dependency for production*) val (tk, depends) = lookahead_dependency lambdas' rhs nts_empty; (*test if this production has to be copied*) val update = nts_member depends changed_nt; (*test if production could already be associated with a member of new_tks*) val lambda = not (nts_is_unique depends) orelse not (nts_is_empty depends) andalso is_some tk andalso tokens_member new_tks (the tk); (*associate production with new starting tokens*) fun copy tk nt_prods = let val tk_prods = prods_lookup nt_prods tk; val tk_prods' = if not lambda then p :: tk_prods else insert (op =) p tk_prods; (*if production depends on lambda NT we have to look for duplicates*) in prods_update (tk, tk_prods') nt_prods end; val result = if update then (tk_prods, tokens_fold copy new_tks nt_prods) else if key = unknown_start then (p :: tk_prods, nt_prods) else (tk_prods, nt_prods); in update_prods ps result end; (*copy existing productions for new starting tokens*) fun process_nts nt = let val ((nts, tks), nt_prods) = Array.sub (prods, nt); val tk_prods = prods_lookup nt_prods key; (*associate productions with new lookahead tokens*) val (tk_prods', nt_prods') = update_prods tk_prods ([], nt_prods); val nt_prods'' = if key = unknown_start then prods_update (key, tk_prods') nt_prods' else nt_prods'; val added_tks = tokens_subtract tks new_tks; val tks' = tokens_merge (tks, added_tks); val _ = Array.update (prods, nt, ((nts, tks'), nt_prods'')); in tokens_add (nt, added_tks) end; val ((dependent, _), _) = Array.sub (prods, changed_nt); in add_starts (starts @ nts_fold process_nts dependent []) end; in add_starts added_starts' end; in (chains', lambdas') end; (* pretty_gram *) fun pretty_gram (Gram {tags, prods, chains, ...}) = let val print_nt = tags_name tags; fun print_pri p = if p < 0 then "" else Symbol.make_sup ("(" ^ string_of_int p ^ ")"); fun pretty_symb (Terminal tok) = if Lexicon.is_literal tok then Pretty.quote (Pretty.keyword1 (Lexicon.str_of_token tok)) else Pretty.str (Lexicon.str_of_token tok) | pretty_symb (Nonterminal (tag, p)) = Pretty.str (print_nt tag ^ print_pri p); fun pretty_const "" = [] | pretty_const c = [Pretty.str ("\<^bold>\ " ^ quote c)]; fun prod_of_chain from = ([Nonterminal (from, ~1)], "", ~1); fun pretty_prod (name, tag) = (prods_content (#2 (Vector.sub (prods, tag))) @ map prod_of_chain (chains_preds chains tag)) |> map (fn (symbs, const, p) => Pretty.block (Pretty.breaks (Pretty.str (name ^ print_pri p ^ " =") :: map pretty_symb symbs @ pretty_const const))); in maps pretty_prod (tags_content tags) end; (** operations on grammars **) val empty_gram = Gram {nt_count = 0, prod_count = 0, tags = tags_empty, chains = chains_empty, lambdas = nts_empty, prods = Vector.fromList [nt_gram_empty]}; (*Add productions to a grammar*) fun extend_gram [] gram = gram | extend_gram xprods (Gram {nt_count, prod_count, tags, chains, lambdas, prods}) = let (*Get tag for existing nonterminal or create a new one*) fun get_tag nt_count tags nt = (case tags_lookup tags nt of SOME tag => (nt_count, tags, tag) | NONE => (nt_count + 1, tags_insert (nt, nt_count) tags, nt_count)); (*Convert symbols to the form used by the parser; delimiters and predefined terms are stored as terminals, nonterminals are converted to integer tags*) fun symb_of [] nt_count tags result = (nt_count, tags, rev result) | symb_of (Syntax_Ext.Delim s :: ss) nt_count tags result = symb_of ss nt_count tags (Terminal (Lexicon.literal s) :: result) | symb_of (Syntax_Ext.Argument (s, p) :: ss) nt_count tags result = let val (nt_count', tags', new_symb) = (case Lexicon.get_terminal s of NONE => let val (nt_count', tags', s_tag) = get_tag nt_count tags s; in (nt_count', tags', Nonterminal (s_tag, p)) end | SOME tk => (nt_count, tags, Terminal tk)); in symb_of ss nt_count' tags' (new_symb :: result) end | symb_of (_ :: ss) nt_count tags result = symb_of ss nt_count tags result; (*Convert list of productions by invoking symb_of for each of them*) fun prod_of [] nt_count prod_count tags result = (nt_count, prod_count, tags, result) | prod_of (Syntax_Ext.XProd (lhs, xsymbs, const, pri) :: ps) nt_count prod_count tags result = let val (nt_count', tags', lhs_tag) = get_tag nt_count tags lhs; val (nt_count'', tags'', prods) = symb_of xsymbs nt_count' tags' []; in prod_of ps nt_count'' (prod_count + 1) tags'' ((lhs_tag, (prods, const, pri)) :: result) end; val (nt_count', prod_count', tags', xprods') = prod_of xprods nt_count prod_count tags []; (*Copy array containing productions of old grammar; this has to be done to preserve the old grammar while being able to change the array's content*) val prods' = let fun get_prod i = if i < nt_count then Vector.sub (prods, i) else nt_gram_empty; in Array.tabulate (nt_count', get_prod) end; val (chains', lambdas') = (chains, lambdas) |> fold (add_production prods') xprods'; in Gram {nt_count = nt_count', prod_count = prod_count', tags = tags', chains = chains', lambdas = lambdas', prods = Array.vector prods'} end; fun make_gram xprods = extend_gram xprods empty_gram; (** parser **) (* parsetree *) datatype parsetree = Node of string * parsetree list | Tip of Lexicon.token; exception PARSETREE of parsetree; fun pretty_parsetree parsetree = let fun pretty (Node (c, pts)) = [Pretty.enclose "(" ")" (Pretty.breaks (Pretty.quote (Pretty.str c) :: maps pretty pts))] | pretty (Tip tok) = if Lexicon.valued_token tok then [Pretty.str (Lexicon.str_of_token tok)] else []; in (case pretty parsetree of [prt] => prt | _ => raise PARSETREE parsetree) end; (* parser state *) type state = nt * int * (*identification and production precedence*) parsetree list * (*already parsed nonterminals on rhs*) symb list * (*rest of rhs*) string * (*name of production*) int; (*index for previous state list*) (*Get all rhss with precedence >= min_prec*) fun get_RHS min_prec = filter (fn (_, _, prec: int) => prec >= min_prec); (*Get all rhss with precedence >= min_prec and < max_prec*) fun get_RHS' min_prec max_prec = filter (fn (_, _, prec: int) => prec >= min_prec andalso prec < max_prec); (*Make states using a list of rhss*) fun mk_states i lhs_ID rhss = let fun mk_state (rhs, id, prod_prec) = (lhs_ID, prod_prec, [], rhs, id, i); in map mk_state rhss end; (*Add parse tree to list and eliminate duplicates saving the maximum precedence*) fun conc (t: parsetree list, prec: int) [] = (NONE, [(t, prec)]) | conc (t, prec) ((t', prec') :: ts) = if t = t' then (SOME prec', if prec' >= prec then (t', prec') :: ts else (t, prec) :: ts) else let val (n, ts') = conc (t, prec) ts in (n, (t', prec') :: ts') end; (*Update entry in used*) fun update_trees (A, t) used = let val (i, ts) = the (Inttab.lookup used A); val (n, ts') = conc t ts; in (n, Inttab.update (A, (i, ts')) used) end; (*Replace entry in used*) fun update_prec (A, prec) = Inttab.map_entry A (fn (_, ts) => (prec, ts)); fun getS A max_prec NONE Si = filter (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= max_prec | _ => false) Si | getS A max_prec (SOME min_prec) Si = filter (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec > min_prec andalso prec <= max_prec | _ => false) Si; fun get_states Estate j A max_prec = filter (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= max_prec | _ => false) (Array.sub (Estate, j)); fun movedot_term c (A, j, ts, Terminal a :: sa, id, i) = if Lexicon.valued_token c orelse id <> "" then (A, j, Tip c :: ts, sa, id, i) else (A, j, ts, sa, id, i); fun movedot_nonterm tt (A, j, ts, Nonterminal _ :: sa, id, i) = (A, j, tt @ ts, sa, id, i); fun movedot_lambda [] _ = [] | movedot_lambda ((t, ki) :: ts) (state as (B, j, tss, Nonterminal (A, k) :: sa, id, i)) = if k <= ki then (B, j, t @ tss, sa, id, i) :: movedot_lambda ts state else movedot_lambda ts state; (*trigger value for warnings*) val branching_level = Config.declare_int ("syntax_branching_level", \<^here>) (K 600); (*get all productions of a NT and NTs chained to it which can be started by specified token*) fun prods_for (Gram {prods, chains, ...}) tk nt = let fun token_prods prods = fold cons (prods_lookup prods tk) #> fold cons (prods_lookup prods Lexicon.dummy); fun nt_prods nt = #2 (Vector.sub (prods, nt)); in fold (token_prods o nt_prods) (chains_all_preds chains [nt]) [] end; fun PROCESSS gram Estate i c states = let fun processS _ [] (Si, Sii) = (Si, Sii) | processS used (S :: States) (Si, Sii) = (case S of (_, _, _, Nonterminal (nt, min_prec) :: _, _, _) => let (*predictor operation*) val (used', new_states) = (case Inttab.lookup used nt of SOME (used_prec, l) => (*nonterminal has been processed*) if used_prec <= min_prec then (*wanted precedence has been processed*) (used, movedot_lambda l S) else (*wanted precedence hasn't been parsed yet*) let val tk_prods = prods_for gram c nt; val States' = mk_states i nt (get_RHS' min_prec used_prec tk_prods); in (update_prec (nt, min_prec) used, movedot_lambda l S @ States') end | NONE => (*nonterminal is parsed for the first time*) let val tk_prods = prods_for gram c nt; val States' = mk_states i nt (get_RHS min_prec tk_prods); in (Inttab.update (nt, (min_prec, [])) used, States') end); in processS used' (new_states @ States) (S :: Si, Sii) end | (_, _, _, Terminal a :: _, _, _) => (*scanner operation*) processS used States (S :: Si, if Lexicon.tokens_match_ord (a, c) = EQUAL then movedot_term c S :: Sii else Sii) | (A, prec, ts, [], id, j) => (*completer operation*) let val tt = if id = "" then ts else [Node (id, rev ts)] in if j = i then (*lambda production?*) let val (prec', used') = update_trees (A, (tt, prec)) used; val Slist = getS A prec prec' Si; val States' = map (movedot_nonterm tt) Slist; in processS used' (States' @ States) (S :: Si, Sii) end else let val Slist = get_states Estate j A prec in processS used (map (movedot_nonterm tt) Slist @ States) (S :: Si, Sii) end end) in processS Inttab.empty states ([], []) end; fun produce gram stateset i indata prev_token = (case Array.sub (stateset, i) of [] => let val toks = if Lexicon.is_eof prev_token then indata else prev_token :: indata; val pos = Position.here (Lexicon.pos_of_token prev_token); in if null toks then error ("Inner syntax error: unexpected end of input" ^ pos) else error ("Inner syntax error" ^ pos ^ Markup.markup Markup.no_report ("\n" ^ Pretty.string_of (Pretty.block [ Pretty.str "at", Pretty.brk 1, Pretty.block (Pretty.str "\"" :: Pretty.breaks (map (Pretty.str o Lexicon.str_of_token) (#1 (split_last toks))) @ [Pretty.str "\""])]))) end | s => (case indata of [] => s | c :: cs => let val (si, sii) = PROCESSS gram stateset i c s; val _ = Array.update (stateset, i, si); val _ = Array.update (stateset, i + 1, sii); in produce gram stateset (i + 1) cs c end)); fun get_trees states = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) states; fun earley (gram as Gram {tags, ...}) startsymbol indata = let val start_tag = (case tags_lookup tags startsymbol of SOME tag => tag | NONE => error ("Inner syntax: bad grammar root symbol " ^ quote startsymbol)); val S0 = [(~1, 0, [], [Nonterminal (start_tag, 0), Terminal Lexicon.eof], "", 0)]; val s = length indata + 1; val Estate = Array.array (s, []); val _ = Array.update (Estate, 0, S0); in get_trees (produce gram Estate 0 indata Lexicon.eof) end; fun parse gram start toks = let val end_pos = (case try List.last toks of NONE => Position.none | SOME tok => Lexicon.end_pos_of_token tok); val r = (case earley gram start (toks @ [Lexicon.mk_eof end_pos]) of [] => raise Fail "Inner syntax: no parse trees" | pts => pts); in r end; end; diff --git a/src/Pure/context.ML b/src/Pure/context.ML --- a/src/Pure/context.ML +++ b/src/Pure/context.ML @@ -1,754 +1,752 @@ (* Title: Pure/context.ML Author: Markus Wenzel, TU Muenchen Generic theory contexts with unique identity, arbitrarily typed data, monotonic development graph and history support. Generic proof contexts with arbitrarily typed data. Firm naming conventions: thy, thy', thy1, thy2: theory ctxt, ctxt', ctxt1, ctxt2: Proof.context context: Context.generic *) signature BASIC_CONTEXT = sig type theory exception THEORY of string * theory list structure Proof: sig type context end structure Proof_Context: sig val theory_of: Proof.context -> theory val init_global: theory -> Proof.context val get_global: theory -> string -> Proof.context end end; signature CONTEXT = sig include BASIC_CONTEXT (*theory context*) type theory_id val theory_id: theory -> theory_id val timing: bool Unsynchronized.ref val parents_of: theory -> theory list val ancestors_of: theory -> theory list val theory_id_ord: theory_id ord val theory_id_long_name: theory_id -> string val theory_id_name: theory_id -> string val theory_long_name: theory -> string val theory_name: theory -> string val theory_name': {long: bool} -> theory -> string val theory_identifier: theory -> serial val PureN: string val pretty_thy: theory -> Pretty.T val pretty_abbrev_thy: theory -> Pretty.T val get_theory: {long: bool} -> theory -> string -> theory val eq_thy_id: theory_id * theory_id -> bool val eq_thy: theory * theory -> bool val proper_subthy_id: theory_id * theory_id -> bool val proper_subthy: theory * theory -> bool val subthy_id: theory_id * theory_id -> bool val subthy: theory * theory -> bool val trace_theories: bool Unsynchronized.ref val theories_trace: unit -> {active_positions: Position.T list, active: int, total: int} val join_thys: theory * theory -> theory val begin_thy: string -> theory list -> theory val finish_thy: theory -> theory val theory_sizeof1_data: theory -> (Position.T * int) list (*proof context*) val raw_transfer: theory -> Proof.context -> Proof.context (*certificate*) datatype certificate = Certificate of theory | Certificate_Id of theory_id val certificate_theory: certificate -> theory val certificate_theory_id: certificate -> theory_id val eq_certificate: certificate * certificate -> bool val join_certificate: certificate * certificate -> certificate (*generic context*) datatype generic = Theory of theory | Proof of Proof.context val cases: (theory -> 'a) -> (Proof.context -> 'a) -> generic -> 'a val mapping: (theory -> theory) -> (Proof.context -> Proof.context) -> generic -> generic val mapping_result: (theory -> 'a * theory) -> (Proof.context -> 'a * Proof.context) -> generic -> 'a * generic val the_theory: generic -> theory val the_proof: generic -> Proof.context val map_theory: (theory -> theory) -> generic -> generic val map_proof: (Proof.context -> Proof.context) -> generic -> generic val map_theory_result: (theory -> 'a * theory) -> generic -> 'a * generic val map_proof_result: (Proof.context -> 'a * Proof.context) -> generic -> 'a * generic val theory_map: (generic -> generic) -> theory -> theory val proof_map: (generic -> generic) -> Proof.context -> Proof.context val theory_of: generic -> theory (*total*) val proof_of: generic -> Proof.context (*total*) (*thread data*) val get_generic_context: unit -> generic option val put_generic_context: generic option -> unit val setmp_generic_context: generic option -> ('a -> 'b) -> 'a -> 'b val the_generic_context: unit -> generic val the_global_context: unit -> theory val the_local_context: unit -> Proof.context val >> : (generic -> generic) -> unit val >>> : (generic -> 'a * generic) -> 'a end; signature PRIVATE_CONTEXT = sig include CONTEXT structure Theory_Data: sig val declare: Position.T -> Any.T -> (theory * theory -> Any.T * Any.T -> Any.T) -> serial val get: serial -> (Any.T -> 'a) -> theory -> 'a val put: serial -> ('a -> Any.T) -> 'a -> theory -> theory end structure Proof_Data: sig val declare: (theory -> Any.T) -> serial val get: serial -> (Any.T -> 'a) -> Proof.context -> 'a val put: serial -> ('a -> Any.T) -> 'a -> Proof.context -> Proof.context end end; structure Context: PRIVATE_CONTEXT = struct (*** theory context ***) (*private copy avoids potential conflict of table exceptions*) structure Datatab = Table(type key = int val ord = int_ord); (** datatype theory **) type stage = int * int Synchronized.var; fun init_stage () : stage = (0, Synchronized.var "Context.stage" 1); fun next_stage ((_, state): stage) = (Synchronized.change_result state (fn n => (n, n + 1)), state); abstype theory_id = Theory_Id of (*identity*) {id: serial, (*identifier*) - ids: Inttab.set} * (*cumulative identifiers -- symbolic body content*) + ids: Intset.T} * (*cumulative identifiers -- symbolic body content*) (*history*) {name: string, (*official theory name*) stage: stage option} (*index and counter for anonymous updates*) with fun rep_theory_id (Theory_Id args) = args; val make_theory_id = Theory_Id; end; datatype theory = Theory of (*identity*) {theory_id: theory_id, token: Position.T Unsynchronized.ref} * (*ancestry*) {parents: theory list, (*immediate predecessors*) ancestors: theory list} * (*all predecessors -- canonical reverse order*) (*data*) Any.T Datatab.table; (*body content*) exception THEORY of string * theory list; fun rep_theory (Theory args) = args; val theory_identity = #1 o rep_theory; val theory_id = #theory_id o theory_identity; val identity_of_id = #1 o rep_theory_id; val identity_of = identity_of_id o theory_id; val history_of_id = #2 o rep_theory_id; val history_of = history_of_id o theory_id; val ancestry_of = #2 o rep_theory; val data_of = #3 o rep_theory; fun make_identity id ids = {id = id, ids = ids}; fun make_history name = {name = name, stage = SOME (init_stage ())}; fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors}; val theory_id_ord = int_ord o apply2 (#id o identity_of_id); val theory_id_long_name = #name o history_of_id; val theory_id_name = Long_Name.base_name o theory_id_long_name; val theory_long_name = #name o history_of; val theory_name = Long_Name.base_name o theory_long_name; fun theory_name' {long} = if long then theory_long_name else theory_name; val theory_identifier = #id o identity_of_id o theory_id; val parents_of = #parents o ancestry_of; val ancestors_of = #ancestors o ancestry_of; (* names *) val PureN = "Pure"; fun display_name thy_id = (case history_of_id thy_id of {name, stage = NONE} => name | {name, stage = SOME (i, _)} => name ^ ":" ^ string_of_int i); fun display_names thy = let val name = display_name (theory_id thy); val ancestor_names = map theory_long_name (ancestors_of thy); in rev (name :: ancestor_names) end; val pretty_thy = Pretty.str_list "{" "}" o display_names; val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_thy); fun pretty_abbrev_thy thy = let val names = display_names thy; val n = length names; val abbrev = if n > 5 then "..." :: List.drop (names, n - 5) else names; in Pretty.str_list "{" "}" abbrev end; fun get_theory long thy name = if theory_name' long thy <> name then (case find_first (fn thy' => theory_name' long thy' = name) (ancestors_of thy) of SOME thy' => thy' | NONE => error ("Unknown ancestor theory " ^ quote name)) else if is_none (#stage (history_of thy)) then thy else error ("Unfinished theory " ^ quote name); (* build ids *) -fun insert_id id ids = Inttab.update (id, ()) ids; - val merge_ids = apply2 (theory_id #> rep_theory_id #> #1) #> (fn ({id = id1, ids = ids1, ...}, {id = id2, ids = ids2, ...}) => - Inttab.merge (K true) (ids1, ids2) - |> insert_id id1 - |> insert_id id2); + Intset.merge (ids1, ids2) + |> Intset.insert id1 + |> Intset.insert id2); (* equality and inclusion *) val eq_thy_id = op = o apply2 (#id o identity_of_id); val eq_thy = op = o apply2 (#id o identity_of); val proper_subthy_id = - apply2 (rep_theory_id #> #1) #> (fn ({id, ...}, {ids, ...}) => Inttab.defined ids id); + apply2 (rep_theory_id #> #1) #> (fn ({id, ...}, {ids, ...}) => Intset.member ids id); val proper_subthy = proper_subthy_id o apply2 theory_id; fun subthy_id p = eq_thy_id p orelse proper_subthy_id p; val subthy = subthy_id o apply2 theory_id; (* consistent ancestors *) fun eq_thy_consistent (thy1, thy2) = eq_thy (thy1, thy2) orelse (theory_name thy1 = theory_name thy2 andalso raise THEORY ("Duplicate theory name", [thy1, thy2])); fun extend_ancestors thy thys = if member eq_thy_consistent thys thy then raise THEORY ("Duplicate theory node", thy :: thys) else thy :: thys; val merge_ancestors = merge eq_thy_consistent; (** theory data **) (* data kinds and access methods *) val timing = Unsynchronized.ref false; local type kind = {pos: Position.T, empty: Any.T, merge: theory * theory -> Any.T * Any.T -> Any.T}; val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table); fun invoke name f k x = (case Datatab.lookup (Synchronized.value kinds) k of SOME kind => if ! timing andalso name <> "" then Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.here (#pos kind)) (fn () => f kind x) else f kind x | NONE => raise Fail "Invalid theory data identifier"); in fun invoke_pos k = invoke "" (K o #pos) k (); fun invoke_empty k = invoke "" (K o #empty) k (); fun invoke_merge thys = invoke "merge" (fn kind => #merge kind thys); fun declare_theory_data pos empty merge = let val k = serial (); val kind = {pos = pos, empty = empty, merge = merge}; val _ = Synchronized.change kinds (Datatab.update (k, kind)); in k end; fun merge_data thys = Datatab.join (invoke_merge thys); end; (** build theories **) (* create theory *) val trace_theories = Unsynchronized.ref false; local val theories = Synchronized.var "theory_tokens" ([]: Position.T Unsynchronized.ref option Unsynchronized.ref list); val dummy_token = Unsynchronized.ref Position.none; fun make_token () = if ! trace_theories then let val token = Unsynchronized.ref (Position.thread_data ()); val _ = Synchronized.change theories (cons (Weak.weak (SOME token))); in token end else dummy_token; in fun theories_trace () = let val trace = Synchronized.value theories; val _ = ML_Heap.full_gc (); val active_positions = fold (fn Unsynchronized.ref (SOME pos) => cons (! pos) | _ => I) trace []; in {active_positions = active_positions, active = length active_positions, total = length trace} end; fun create_thy ids history ancestry data = let val theory_id = make_theory_id (make_identity (serial ()) ids, history); val token = make_token (); in Theory ({theory_id = theory_id, token = token}, ancestry, data) end; end; (* primitives *) val pre_pure_thy = - create_thy Inttab.empty (make_history PureN) (make_ancestry [] []) Datatab.empty; + create_thy Intset.empty (make_history PureN) (make_ancestry [] []) Datatab.empty; local fun change_thy finish f thy = let val ({id, ids}, {name, stage}) = rep_theory_id (theory_id thy); val Theory (_, ancestry, data) = thy; val ancestry' = if is_none stage then make_ancestry [thy] (extend_ancestors thy (ancestors_of thy)) else ancestry; val history' = {name = name, stage = if finish then NONE else Option.map next_stage stage}; - val ids' = insert_id id ids; + val ids' = Intset.insert id ids; val data' = f data; in create_thy ids' history' ancestry' data' end; in val update_thy = change_thy false; val extend_thy = update_thy I; val finish_thy = change_thy true I; end; (* join: anonymous theory nodes *) local fun bad_join (thy1, thy2) = raise THEORY ("Cannot join theories", [thy1, thy2]); fun join_history thys = apply2 history_of thys |> (fn ({name, stage}, {name = name', stage = stage'}) => if name = name' andalso is_some stage andalso is_some stage' then {name = name, stage = Option.map next_stage stage} else bad_join thys); fun join_ancestry thys = apply2 ancestry_of thys |> (fn (ancestry as {parents, ancestors}, {parents = parents', ancestors = ancestors'}) => if eq_list eq_thy (parents, parents') andalso eq_list eq_thy (ancestors, ancestors') then ancestry else bad_join thys); in fun join_thys thys = let val ids = merge_ids thys; val history = join_history thys; val ancestry = join_ancestry thys; val data = merge_data thys (apply2 data_of thys); in create_thy ids history ancestry data end; end; (* merge: named theory nodes *) local fun merge_thys thys = let val ids = merge_ids thys; val history = make_history ""; val ancestry = make_ancestry [] []; val data = merge_data thys (apply2 data_of thys); in create_thy ids history ancestry data end; fun maximal_thys thys = thys |> filter_out (fn thy => exists (fn thy' => proper_subthy (thy, thy')) thys); in fun begin_thy name imports = if name = "" then error ("Bad theory name: " ^ quote name) else let val parents = maximal_thys (distinct eq_thy imports); val ancestors = Library.foldl merge_ancestors ([], map ancestors_of parents) |> fold extend_ancestors parents; val thy0 = (case parents of [] => error "Missing theory imports" | [thy] => extend_thy thy | thy :: thys => Library.foldl merge_thys (thy, thys)); val ({ids, ...}, _) = rep_theory_id (theory_id thy0); val history = make_history name; val ancestry = make_ancestry parents ancestors; in create_thy ids history ancestry (data_of thy0) |> tap finish_thy end; end; (* theory data *) structure Theory_Data = struct val declare = declare_theory_data; fun get k dest thy = (case Datatab.lookup (data_of thy) k of SOME x => x | NONE => invoke_empty k) |> dest; fun put k mk x = update_thy (Datatab.update (k, mk x)); fun sizeof1 k thy = Datatab.lookup (data_of thy) k |> Option.map ML_Heap.sizeof1; end; fun theory_sizeof1_data thy = build (data_of thy |> Datatab.fold_rev (fn (k, _) => (case Theory_Data.sizeof1 k thy of NONE => I | SOME n => (cons (invoke_pos k, n))))); (*** proof context ***) (* datatype Proof.context *) structure Proof = struct datatype context = Context of Any.T Datatab.table * theory; end; (* proof data kinds *) local val kinds = Synchronized.var "Proof_Data" (Datatab.empty: (theory -> Any.T) Datatab.table); fun init_data thy = Synchronized.value kinds |> Datatab.map (fn _ => fn init => init thy); fun init_new_data thy = Synchronized.value kinds |> Datatab.fold (fn (k, init) => fn data => if Datatab.defined data k then data else Datatab.update (k, init thy) data); fun init_fallback k thy = (case Datatab.lookup (Synchronized.value kinds) k of SOME init => init thy | NONE => raise Fail "Invalid proof data identifier"); in fun raw_transfer thy' (Proof.Context (data, thy)) = let val _ = subthy (thy, thy') orelse error "Cannot transfer proof context: not a super theory"; val data' = init_new_data thy' data; in Proof.Context (data', thy') end; structure Proof_Context = struct fun theory_of (Proof.Context (_, thy)) = thy; fun init_global thy = Proof.Context (init_data thy, thy); fun get_global thy name = init_global (get_theory {long = false} thy name); end; structure Proof_Data = struct fun declare init = let val k = serial (); val _ = Synchronized.change kinds (Datatab.update (k, init)); in k end; fun get k dest (Proof.Context (data, thy)) = (case Datatab.lookup data k of SOME x => x | NONE => init_fallback k thy) |> dest; fun put k mk x (Proof.Context (data, thy)) = Proof.Context (Datatab.update (k, mk x) data, thy); end; end; (*** theory certificate ***) datatype certificate = Certificate of theory | Certificate_Id of theory_id; fun certificate_theory (Certificate thy) = thy | certificate_theory (Certificate_Id thy_id) = error ("No content for theory certificate " ^ display_name thy_id); fun certificate_theory_id (Certificate thy) = theory_id thy | certificate_theory_id (Certificate_Id thy_id) = thy_id; fun eq_certificate (Certificate thy1, Certificate thy2) = eq_thy (thy1, thy2) | eq_certificate (Certificate_Id thy_id1, Certificate_Id thy_id2) = eq_thy_id (thy_id1, thy_id2) | eq_certificate _ = false; fun join_certificate (cert1, cert2) = let val (thy_id1, thy_id2) = apply2 certificate_theory_id (cert1, cert2) in if eq_thy_id (thy_id1, thy_id2) then (case cert1 of Certificate _ => cert1 | _ => cert2) else if proper_subthy_id (thy_id2, thy_id1) then cert1 else if proper_subthy_id (thy_id1, thy_id2) then cert2 else error ("Cannot join unrelated theory certificates " ^ display_name thy_id1 ^ " and " ^ display_name thy_id2) end; (*** generic context ***) datatype generic = Theory of theory | Proof of Proof.context; fun cases f _ (Theory thy) = f thy | cases _ g (Proof prf) = g prf; fun mapping f g = cases (Theory o f) (Proof o g); fun mapping_result f g = cases (apsnd Theory o f) (apsnd Proof o g); val the_theory = cases I (fn _ => error "Ill-typed context: theory expected"); val the_proof = cases (fn _ => error "Ill-typed context: proof expected") I; fun map_theory f = Theory o f o the_theory; fun map_proof f = Proof o f o the_proof; fun map_theory_result f = apsnd Theory o f o the_theory; fun map_proof_result f = apsnd Proof o f o the_proof; fun theory_map f = the_theory o f o Theory; fun proof_map f = the_proof o f o Proof; val theory_of = cases I Proof_Context.theory_of; val proof_of = cases Proof_Context.init_global I; (** thread data **) local val generic_context_var = Thread_Data.var () : generic Thread_Data.var in fun get_generic_context () = Thread_Data.get generic_context_var; val put_generic_context = Thread_Data.put generic_context_var; fun setmp_generic_context opt_context = Thread_Data.setmp generic_context_var opt_context; fun the_generic_context () = (case get_generic_context () of SOME context => context | _ => error "Unknown context"); val the_global_context = theory_of o the_generic_context; val the_local_context = proof_of o the_generic_context; end; fun >>> f = let val (res, context') = f (the_generic_context ()); val _ = put_generic_context (SOME context'); in res end; nonfix >>; fun >> f = >>> (fn context => ((), f context)); val _ = put_generic_context (SOME (Theory pre_pure_thy)); end; structure Basic_Context: BASIC_CONTEXT = Context; open Basic_Context; (*** type-safe interfaces for data declarations ***) (** theory data **) signature THEORY_DATA'_ARGS = sig type T val empty: T val merge: theory * theory -> T * T -> T end; signature THEORY_DATA_ARGS = sig type T val empty: T val merge: T * T -> T end; signature THEORY_DATA = sig type T val get: theory -> T val put: T -> theory -> theory val map: (T -> T) -> theory -> theory end; functor Theory_Data'(Data: THEORY_DATA'_ARGS): THEORY_DATA = struct type T = Data.T; exception Data of T; val kind = let val pos = Position.thread_data () in Context.Theory_Data.declare pos (Data Data.empty) (fn thys => fn (Data x1, Data x2) => Data (Data.merge thys (x1, x2))) end; val get = Context.Theory_Data.get kind (fn Data x => x); val put = Context.Theory_Data.put kind Data; fun map f thy = put (f (get thy)) thy; end; functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA = Theory_Data' ( type T = Data.T; val empty = Data.empty; fun merge _ = Data.merge; ); (** proof data **) signature PROOF_DATA_ARGS = sig type T val init: theory -> T end; signature PROOF_DATA = sig type T val get: Proof.context -> T val put: T -> Proof.context -> Proof.context val map: (T -> T) -> Proof.context -> Proof.context end; functor Proof_Data(Data: PROOF_DATA_ARGS): PROOF_DATA = struct type T = Data.T; exception Data of T; val kind = Context.Proof_Data.declare (Data o Data.init); val get = Context.Proof_Data.get kind (fn Data x => x); val put = Context.Proof_Data.put kind Data; fun map f prf = put (f (get prf)) prf; end; (** generic data **) signature GENERIC_DATA_ARGS = sig type T val empty: T val merge: T * T -> T end; signature GENERIC_DATA = sig type T val get: Context.generic -> T val put: T -> Context.generic -> Context.generic val map: (T -> T) -> Context.generic -> Context.generic end; functor Generic_Data(Data: GENERIC_DATA_ARGS): GENERIC_DATA = struct structure Thy_Data = Theory_Data(Data); structure Prf_Data = Proof_Data(type T = Data.T val init = Thy_Data.get); type T = Data.T; fun get (Context.Theory thy) = Thy_Data.get thy | get (Context.Proof prf) = Prf_Data.get prf; fun put x (Context.Theory thy) = Context.Theory (Thy_Data.put x thy) | put x (Context.Proof prf) = Context.Proof (Prf_Data.put x prf); fun map f ctxt = put (f (get ctxt)) ctxt; end; (*hide private interface*) structure Context: CONTEXT = Context; diff --git a/src/Pure/more_thm.ML b/src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML +++ b/src/Pure/more_thm.ML @@ -1,757 +1,757 @@ (* Title: Pure/more_thm.ML Author: Makarius Further operations on type ctyp/cterm/thm, outside the inference kernel. *) infix aconvc; signature BASIC_THM = sig include BASIC_THM val show_consts: bool Config.T val show_hyps: bool Config.T val show_tags: bool Config.T val aconvc: cterm * cterm -> bool type attribute = Context.generic * thm -> Context.generic option * thm option end; signature THM = sig include THM val eq_ctyp: ctyp * ctyp -> bool val aconvc: cterm * cterm -> bool val add_tvars: thm -> ctyp TVars.table -> ctyp TVars.table val add_vars: thm -> cterm Vars.table -> cterm Vars.table val dest_funT: ctyp -> ctyp * ctyp val strip_type: ctyp -> ctyp list * ctyp val instantiate_ctyp: ctyp TVars.table -> ctyp -> ctyp val all_name: Proof.context -> string * cterm -> cterm -> cterm val all: Proof.context -> cterm -> cterm -> cterm val mk_binop: cterm -> cterm -> cterm -> cterm val dest_binop: cterm -> cterm * cterm val dest_implies: cterm -> cterm * cterm val dest_equals: cterm -> cterm * cterm val dest_equals_lhs: cterm -> cterm val dest_equals_rhs: cterm -> cterm val lhs_of: thm -> cterm val rhs_of: thm -> cterm val is_reflexive: thm -> bool val eq_thm: thm * thm -> bool val eq_thm_prop: thm * thm -> bool val eq_thm_strict: thm * thm -> bool val equiv_thm: theory -> thm * thm -> bool val class_triv: theory -> class -> thm val of_sort: ctyp * sort -> thm list val is_dummy: thm -> bool val add_thm: thm -> thm list -> thm list val del_thm: thm -> thm list -> thm list val merge_thms: thm list * thm list -> thm list val item_net: thm Item_Net.T val item_net_intro: thm Item_Net.T val item_net_elim: thm Item_Net.T val declare_hyps: cterm -> Proof.context -> Proof.context val assume_hyps: cterm -> Proof.context -> thm * Proof.context val unchecked_hyps: Proof.context -> Proof.context val restore_hyps: Proof.context -> Proof.context -> Proof.context val undeclared_hyps: Context.generic -> thm -> term list val check_hyps: Context.generic -> thm -> thm val declare_term_sorts: term -> Proof.context -> Proof.context val extra_shyps': Proof.context -> thm -> sort list val check_shyps: Proof.context -> thm -> thm val weaken_sorts': Proof.context -> cterm -> cterm val elim_implies: thm -> thm -> thm val forall_intr_name: string * cterm -> thm -> thm val forall_elim_var: int -> thm -> thm val forall_elim_vars: int -> thm -> thm val instantiate_frees: ctyp TFrees.table * cterm Frees.table -> thm -> thm val instantiate': ctyp option list -> cterm option list -> thm -> thm val forall_intr_frees: thm -> thm val forall_intr_vars: thm -> thm val unvarify_global: theory -> thm -> thm val unvarify_axiom: theory -> string -> thm val rename_params_rule: string list * int -> thm -> thm val rename_boundvars: term -> term -> thm -> thm val add_axiom: Proof.context -> binding * term -> theory -> (string * thm) * theory val add_axiom_global: binding * term -> theory -> (string * thm) * theory val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory val add_def_global: bool -> bool -> binding * term -> theory -> (string * thm) * theory type attribute = Context.generic * thm -> Context.generic option * thm option type binding = binding * attribute list val tag_rule: string * string -> thm -> thm val untag_rule: string -> thm -> thm val is_free_dummy: thm -> bool val tag_free_dummy: thm -> thm val def_name: string -> string val def_name_optional: string -> string -> string val def_binding: Binding.binding -> Binding.binding val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding val make_def_binding: bool -> Binding.binding -> Binding.binding val has_name_hint: thm -> bool val get_name_hint: thm -> string val put_name_hint: string -> thm -> thm val theoremK: string val legacy_get_kind: thm -> string val kind_rule: string -> thm -> thm val rule_attribute: thm list -> (Context.generic -> thm -> thm) -> attribute val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute val apply_attribute: attribute -> thm -> Context.generic -> thm * Context.generic val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic val theory_attributes: attribute list -> thm -> theory -> thm * theory val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context val no_attributes: 'a -> 'a * 'b list val simple_fact: 'a -> ('a * 'b list) list val tag: string * string -> attribute val untag: string -> attribute val kind: string -> attribute val register_proofs: thm list lazy -> theory -> theory val consolidate_theory: theory -> unit val expose_theory: theory -> unit val show_consts: bool Config.T val show_hyps: bool Config.T val show_tags: bool Config.T val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T val pretty_thm: Proof.context -> thm -> Pretty.T val pretty_thm_item: Proof.context -> thm -> Pretty.T val pretty_thm_global: theory -> thm -> Pretty.T val string_of_thm: Proof.context -> thm -> string val string_of_thm_global: theory -> thm -> string end; structure Thm: THM = struct (** basic operations **) (* collecting ctyps and cterms *) val eq_ctyp = op = o apply2 Thm.typ_of; val op aconvc = op aconv o apply2 Thm.term_of; val add_tvars = Thm.fold_atomic_ctyps {hyps = false} Term.is_TVar (fn cT => fn tab => let val v = Term.dest_TVar (Thm.typ_of cT) in tab |> not (TVars.defined tab v) ? TVars.add (v, cT) end); val add_vars = Thm.fold_atomic_cterms {hyps = false} Term.is_Var (fn ct => fn tab => let val v = Term.dest_Var (Thm.term_of ct) in tab |> not (Vars.defined tab v) ? Vars.add (v, ct) end); (* ctyp operations *) fun dest_funT cT = (case Thm.typ_of cT of Type ("fun", _) => let val [A, B] = Thm.dest_ctyp cT in (A, B) end | T => raise TYPE ("dest_funT", [T], [])); (* ctyp version of strip_type: maps [T1,...,Tn]--->T to ([T1,T2,...,Tn], T) *) fun strip_type cT = (case Thm.typ_of cT of Type ("fun", _) => let val (cT1, cT2) = dest_funT cT; val (cTs, cT') = strip_type cT2 in (cT1 :: cTs, cT') end | _ => ([], cT)); fun instantiate_ctyp instT cT = Thm.instantiate_cterm (instT, Vars.empty) (Thm.var (("x", 0), cT)) |> Thm.ctyp_of_cterm; (* cterm operations *) fun all_name ctxt (x, t) A = let val T = Thm.typ_of_cterm t; val all_const = Thm.cterm_of ctxt (Const ("Pure.all", (T --> propT) --> propT)); in Thm.apply all_const (Thm.lambda_name (x, t) A) end; fun all ctxt t A = all_name ctxt ("", t) A; fun mk_binop c a b = Thm.apply (Thm.apply c a) b; fun dest_binop ct = (Thm.dest_arg1 ct, Thm.dest_arg ct); fun dest_implies ct = (case Thm.term_of ct of Const ("Pure.imp", _) $ _ $ _ => dest_binop ct | _ => raise TERM ("dest_implies", [Thm.term_of ct])); fun dest_equals ct = (case Thm.term_of ct of Const ("Pure.eq", _) $ _ $ _ => dest_binop ct | _ => raise TERM ("dest_equals", [Thm.term_of ct])); fun dest_equals_lhs ct = (case Thm.term_of ct of Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg1 ct | _ => raise TERM ("dest_equals_lhs", [Thm.term_of ct])); fun dest_equals_rhs ct = (case Thm.term_of ct of Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg ct | _ => raise TERM ("dest_equals_rhs", [Thm.term_of ct])); val lhs_of = dest_equals_lhs o Thm.cprop_of; val rhs_of = dest_equals_rhs o Thm.cprop_of; (* equality *) fun is_reflexive th = op aconv (Logic.dest_equals (Thm.prop_of th)) handle TERM _ => false; val eq_thm = is_equal o Thm.thm_ord; val eq_thm_prop = op aconv o apply2 Thm.full_prop_of; fun eq_thm_strict ths = eq_thm ths andalso Context.eq_thy_id (apply2 Thm.theory_id ths) andalso op = (apply2 Thm.maxidx_of ths) andalso op = (apply2 Thm.get_tags ths); (* pattern equivalence *) fun equiv_thm thy ths = Pattern.equiv thy (apply2 (Thm.full_prop_of o Thm.transfer thy) ths); (* type classes and sorts *) fun class_triv thy c = Thm.of_class (Thm.global_ctyp_of thy (TVar ((Name.aT, 0), [c])), c); fun of_sort (T, S) = map (fn c => Thm.of_class (T, c)) S; (* misc operations *) fun is_dummy thm = (case try Logic.dest_term (Thm.concl_of thm) of NONE => false | SOME t => Term.is_dummy_pattern (Term.head_of t)); (* collections of theorems in canonical order *) val add_thm = update eq_thm_prop; val del_thm = remove eq_thm_prop; val merge_thms = merge eq_thm_prop; val item_net = Item_Net.init eq_thm_prop (single o Thm.full_prop_of); val item_net_intro = Item_Net.init eq_thm_prop (single o Thm.concl_of); val item_net_elim = Item_Net.init eq_thm_prop (single o Thm.major_prem_of); (** declared hyps and sort hyps **) structure Hyps = Proof_Data ( - type T = {checked_hyps: bool, hyps: Termtab.set, shyps: sort Ord_List.T}; - fun init _ : T = {checked_hyps = true, hyps = Termtab.empty, shyps = []}; + type T = {checked_hyps: bool, hyps: Termset.T, shyps: sort Ord_List.T}; + fun init _ : T = {checked_hyps = true, hyps = Termset.empty, shyps = []}; ); fun map_hyps f = Hyps.map (fn {checked_hyps, hyps, shyps} => let val (checked_hyps', hyps', shyps') = f (checked_hyps, hyps, shyps) in {checked_hyps = checked_hyps', hyps = hyps', shyps = shyps'} end); (* hyps *) fun declare_hyps raw_ct ctxt = ctxt |> map_hyps (fn (checked_hyps, hyps, shyps) => let val ct = Thm.transfer_cterm (Proof_Context.theory_of ctxt) raw_ct; - val hyps' = Termtab.update (Thm.term_of ct, ()) hyps; + val hyps' = Termset.insert (Thm.term_of ct) hyps; in (checked_hyps, hyps', shyps) end); fun assume_hyps ct ctxt = (Thm.assume ct, declare_hyps ct ctxt); val unchecked_hyps = map_hyps (fn (_, hyps, shyps) => (false, hyps, shyps)); fun restore_hyps ctxt = map_hyps (fn (_, hyps, shyps) => (#checked_hyps (Hyps.get ctxt), hyps, shyps)); fun undeclared_hyps context th = Thm.hyps_of th |> filter_out (case context of Context.Theory _ => K false | Context.Proof ctxt => (case Hyps.get ctxt of {checked_hyps = false, ...} => K true - | {hyps, ...} => Termtab.defined hyps)); + | {hyps, ...} => Termset.member hyps)); fun check_hyps context th = (case undeclared_hyps context th of [] => th | undeclared => error (Pretty.string_of (Pretty.big_list "Undeclared hyps:" (map (Pretty.item o single o Syntax.pretty_term (Syntax.init_pretty context)) undeclared)))); (* shyps *) fun declare_term_sorts t = map_hyps (fn (checked_hyps, hyps, shyps) => (checked_hyps, hyps, Sorts.insert_term t shyps)); fun extra_shyps' ctxt th = Sorts.subtract (#shyps (Hyps.get ctxt)) (Thm.extra_shyps th); fun check_shyps ctxt raw_th = let val th = Thm.strip_shyps raw_th; val extra_shyps = extra_shyps' ctxt th; in if null extra_shyps then th else error (Pretty.string_of (Pretty.block (Pretty.str "Pending sort hypotheses:" :: Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_sort ctxt) extra_shyps)))) end; val weaken_sorts' = Thm.weaken_sorts o #shyps o Hyps.get; (** basic derived rules **) (*Elimination of implication A A \ B ------------ B *) fun elim_implies thA thAB = Thm.implies_elim thAB thA; (* forall_intr_name *) fun forall_intr_name (a, x) th = let val th' = Thm.forall_intr x th; val prop' = (case Thm.prop_of th' of all $ Abs (_, T, b) => all $ Abs (a, T, b)); in Thm.renamed_prop prop' th' end; (* forall_elim_var(s) *) local val used_frees = Name.build_context o Thm.fold_terms {hyps = true} Term.declare_term_frees; fun used_vars i = Name.build_context o (Thm.fold_terms {hyps = false} o Term.fold_aterms) (fn Var ((x, j), _) => i = j ? Name.declare x | _ => I); fun dest_all ct used = (case Thm.term_of ct of Const ("Pure.all", _) $ Abs (x, _, _) => let val (x', used') = Name.variant x used; val (v, ct') = Thm.dest_abs_fresh x' (Thm.dest_arg ct); in SOME ((x, Thm.ctyp_of_cterm v), (ct', used')) end | _ => NONE); fun dest_all_list ct used = (case dest_all ct used of NONE => ([], used) | SOME (v, (ct', used')) => let val (vs, used'') = dest_all_list ct' used' in (v :: vs, used'') end); fun forall_elim_vars_list vars i th = let val (vars', _) = (vars, used_vars i th) |-> fold_map (fn (x, T) => fn used => let val (x', used') = Name.variant x used in (Thm.var ((x', i), T), used') end); in fold Thm.forall_elim vars' th end; in fun forall_elim_vars i th = forall_elim_vars_list (#1 (dest_all_list (Thm.cprop_of th) (used_frees th))) i th; fun forall_elim_var i th = let val vars = (case dest_all (Thm.cprop_of th) (used_frees th) of SOME (v, _) => [v] | NONE => raise THM ("forall_elim_var", i, [th])); in forall_elim_vars_list vars i th end; end; (* instantiate frees *) fun instantiate_frees (instT, inst) th = if TFrees.is_empty instT andalso Frees.is_empty inst then th else let val idx = Thm.maxidx_of th + 1; fun index ((a, A), b) = (((a, idx), A), b); val insts = (TVars.build (TFrees.fold (TVars.add o index) instT), Vars.build (Frees.fold (Vars.add o index) inst)); val tfrees = Names.build (TFrees.fold (Names.add_set o #1 o #1) instT); val frees = Names.build (Frees.fold (Names.add_set o #1 o #1) inst); val hyps = Thm.chyps_of th; val inst_cterm = Thm.generalize_cterm (tfrees, frees) idx #> Thm.instantiate_cterm insts; in th |> fold_rev Thm.implies_intr hyps |> Thm.generalize (tfrees, frees) idx |> Thm.instantiate insts |> fold (elim_implies o Thm.assume o inst_cterm) hyps end; (* instantiate by left-to-right occurrence of variables *) fun instantiate' cTs cts thm = let fun err msg = raise TYPE ("instantiate': " ^ msg, map_filter (Option.map Thm.typ_of) cTs, map_filter (Option.map Thm.term_of) cts); fun zip_vars xs ys = zip_options xs ys handle ListPair.UnequalLengths => err "more instantiations than variables in thm"; val instT = zip_vars (build_rev (Thm.fold_terms {hyps = false} Term.add_tvars thm)) cTs; val thm' = Thm.instantiate (TVars.make instT, Vars.empty) thm; val inst = zip_vars (build_rev (Thm.fold_terms {hyps = false} Term.add_vars thm')) cts; in Thm.instantiate (TVars.empty, Vars.make inst) thm' end; (* implicit generalization over variables -- canonical order *) fun forall_intr_vars th = let val vars = Cterms.build (Cterms.add_vars th) in fold_rev Thm.forall_intr (Cterms.list_set vars) th end; fun forall_intr_frees th = let val fixed = Frees.build (fold Frees.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th)) #> fold Frees.add_frees (Thm.hyps_of th)); val is_fixed = Frees.defined fixed o Term.dest_Free o Thm.term_of; val frees = Cterms.build (th |> Thm.fold_atomic_cterms {hyps = false} Term.is_Free (fn ct => not (is_fixed ct) ? Cterms.add_set ct)); in fold_rev Thm.forall_intr (Cterms.list_set frees) th end; (* unvarify_global: global schematic variables *) fun unvarify_global thy th = let val prop = Thm.full_prop_of th; val _ = map Logic.unvarify_global (prop :: Thm.hyps_of th) handle TERM (msg, _) => raise THM (msg, 0, [th]); val cert = Thm.global_cterm_of thy; val certT = Thm.global_ctyp_of thy; val instT = TVars.build (prop |> (Term.fold_types o Term.fold_atyps) (fn T => fn instT => (case T of TVar (v as ((a, _), S)) => if TVars.defined instT v then instT else TVars.add (v, TFree (a, S)) instT | _ => instT))); val cinstT = TVars.map (K certT) instT; val cinst = Vars.build (prop |> Term.fold_aterms (fn t => fn inst => (case t of Var ((x, i), T) => let val T' = Term_Subst.instantiateT instT T in Vars.add (((x, i), T'), cert (Free ((x, T')))) inst end | _ => inst))); in Thm.instantiate (cinstT, cinst) th end; fun unvarify_axiom thy = unvarify_global thy o Thm.axiom thy; (* user renaming of parameters in a subgoal *) (*The names, if distinct, are used for the innermost parameters of subgoal i; preceding parameters may be renamed to make all parameters distinct.*) fun rename_params_rule (names, i) st = let val (_, Bs, Bi, C) = Thm.dest_state (st, i); val params = map #1 (Logic.strip_params Bi); val short = length params - length names; val names' = if short < 0 then error "More names than parameters in subgoal!" else Name.variant_list names (take short params) @ names; val free_names = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi []; val Bi' = Logic.list_rename_params names' Bi; in (case duplicates (op =) names of a :: _ => (warning ("Can't rename. Bound variables not distinct: " ^ a); st) | [] => (case inter (op =) names free_names of a :: _ => (warning ("Can't rename. Bound/Free variable clash: " ^ a); st) | [] => Thm.renamed_prop (Logic.list_implies (Bs @ [Bi'], C)) st)) end; (* preservation of bound variable names *) fun rename_boundvars pat obj th = (case Term.rename_abs pat obj (Thm.prop_of th) of NONE => th | SOME prop' => Thm.renamed_prop prop' th); (** specification primitives **) (* rules *) fun stripped_sorts thy t = let val tfrees = build_rev (Term.add_tfrees t); val tfrees' = map (fn a => (a, [])) (Name.variant_list [] (map #1 tfrees)); val recover = map2 (fn (a', S') => fn (a, S) => (((a', 0), S'), Thm.global_ctyp_of thy (TVar ((a, 0), S)))) tfrees' tfrees; val strip = map (apply2 TFree) (tfrees ~~ tfrees'); val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t; in (strip, recover, t') end; fun add_axiom ctxt (b, prop) thy = let val _ = Sign.no_vars ctxt prop; val (strip, recover, prop') = stripped_sorts thy prop; val constraints = map (fn (TFree (_, S), T) => (T, S)) strip; val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of ctxt T, S)) strip; val thy' = thy |> Theory.add_axiom ctxt (b, Logic.list_implies (maps Logic.mk_of_sort constraints, prop')); val axm_name = Sign.full_name thy' b; val axm' = Thm.axiom thy' axm_name; val thm = Thm.instantiate (TVars.make recover, Vars.empty) axm' |> unvarify_global thy' |> fold elim_implies of_sorts; in ((axm_name, thm), thy') end; fun add_axiom_global arg thy = add_axiom (Syntax.init_pretty_global thy) arg thy; fun add_def (context as (ctxt, _)) unchecked overloaded (b, prop) thy = let val _ = Sign.no_vars ctxt prop; val prems = map (Thm.cterm_of ctxt) (Logic.strip_imp_prems prop); val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop); val thy' = Theory.add_def context unchecked overloaded (b, concl') thy; val axm_name = Sign.full_name thy' b; val axm' = Thm.axiom thy' axm_name; val thm = Thm.instantiate (TVars.make recover, Vars.empty) axm' |> unvarify_global thy' |> fold_rev Thm.implies_intr prems; in ((axm_name, thm), thy') end; fun add_def_global unchecked overloaded arg thy = add_def (Defs.global_context thy) unchecked overloaded arg thy; (** theorem tags **) (* add / delete tags *) fun tag_rule tg = Thm.map_tags (insert (op =) tg); fun untag_rule s = Thm.map_tags (filter_out (fn (s', _) => s = s')); (* free dummy thm -- for abstract closure *) val free_dummyN = "free_dummy"; fun is_free_dummy thm = Properties.defined (Thm.get_tags thm) free_dummyN; val tag_free_dummy = tag_rule (free_dummyN, ""); (* def_name *) fun def_name c = c ^ "_def"; fun def_name_optional c "" = def_name c | def_name_optional _ name = name; val def_binding = Binding.map_name def_name #> Binding.reset_pos; fun def_binding_optional b name = if Binding.is_empty name then def_binding b else name; fun make_def_binding cond b = if cond then def_binding b else Binding.empty; (* unofficial theorem names *) fun has_name_hint thm = AList.defined (op =) (Thm.get_tags thm) Markup.nameN; fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN); fun get_name_hint thm = if has_name_hint thm then the_name_hint thm else "??.unknown"; fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name); (* theorem kinds *) val theoremK = "theorem"; fun legacy_get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN); fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN; (** attributes **) (*attributes subsume any kind of rules or context modifiers*) type attribute = Context.generic * thm -> Context.generic option * thm option; type binding = binding * attribute list; fun rule_attribute ths f (x, th) = (NONE, (case find_first is_free_dummy (th :: ths) of SOME th' => SOME th' | NONE => SOME (f x th))); fun declaration_attribute f (x, th) = (if is_free_dummy th then NONE else SOME (f th x), NONE); fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end; fun apply_attribute (att: attribute) th x = let val (x', th') = att (x, check_hyps x (Thm.transfer'' x th)) in (the_default th th', the_default x x') end; fun attribute_declaration att th x = #2 (apply_attribute att th x); fun apply_attributes mk dest = let fun app [] th x = (th, x) | app (att :: atts) th x = apply_attribute att th (mk x) ||> dest |-> app atts; in app end; val theory_attributes = apply_attributes Context.Theory Context.the_theory; val proof_attributes = apply_attributes Context.Proof Context.the_proof; fun no_attributes x = (x, []); fun simple_fact x = [(x, [])]; fun tag tg = rule_attribute [] (K (tag_rule tg)); fun untag s = rule_attribute [] (K (untag_rule s)); fun kind k = rule_attribute [] (K (k <> "" ? kind_rule k)); (** forked proofs **) structure Proofs = Theory_Data ( type T = thm list lazy Inttab.table; val empty = Inttab.empty; val merge = Inttab.merge (K true); ); fun reset_proofs thy = if Inttab.is_empty (Proofs.get thy) then NONE else SOME (Proofs.put Inttab.empty thy); val _ = Theory.setup (Theory.at_begin reset_proofs); fun register_proofs ths thy = let val entry = (serial (), Lazy.map_finished (map Thm.trim_context) ths) in (Proofs.map o Inttab.update) entry thy end; fun force_proofs thy = Proofs.get thy |> Inttab.dest |> maps (map (Thm.transfer thy) o Lazy.force o #2); val consolidate_theory = Thm.consolidate o force_proofs; fun expose_theory thy = if Proofterm.export_enabled () then Thm.expose_proofs thy (force_proofs thy) else (); (** print theorems **) (* options *) val show_consts = Config.declare_option_bool ("show_consts", \<^here>); val show_hyps = Config.declare_bool ("show_hyps", \<^here>) (K false); val show_tags = Config.declare_bool ("show_tags", \<^here>) (K false); (* pretty_thm etc. *) fun pretty_tag (name, arg) = Pretty.strs [name, quote arg]; val pretty_tags = Pretty.list "[" "]" o map pretty_tag; fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th = let val show_tags = Config.get ctxt show_tags; val show_hyps = Config.get ctxt show_hyps; val th = raw_th |> perhaps (try (Thm.transfer' ctxt)) |> perhaps (try Thm.strip_shyps); val hyps = if show_hyps then Thm.hyps_of th else undeclared_hyps (Context.Proof ctxt) th; val extra_shyps = extra_shyps' ctxt th; val tags = Thm.get_tags th; val tpairs = Thm.tpairs_of th; val q = if quote then Pretty.quote else I; val prt_term = q o Syntax.pretty_term ctxt; val hlen = length extra_shyps + length hyps + length tpairs; val hsymbs = if hlen = 0 then [] else if show_hyps orelse show_hyps' then [Pretty.brk 2, Pretty.list "[" "]" (map (q o Pretty.block o Syntax.pretty_flexpair ctxt) tpairs @ map prt_term hyps @ map (Syntax.pretty_sort ctxt) extra_shyps)] else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")]; val tsymbs = if null tags orelse not show_tags then [] else [Pretty.brk 1, pretty_tags tags]; in Pretty.block (prt_term (Thm.prop_of th) :: (hsymbs @ tsymbs)) end; fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true}; fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th]; fun pretty_thm_global thy = pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false}; val string_of_thm = Pretty.string_of oo pretty_thm; val string_of_thm_global = Pretty.string_of oo pretty_thm_global; open Thm; end; structure Basic_Thm: BASIC_THM = Thm; open Basic_Thm; diff --git a/src/Pure/term_ord.ML b/src/Pure/term_ord.ML --- a/src/Pure/term_ord.ML +++ b/src/Pure/term_ord.ML @@ -1,225 +1,228 @@ (* Title: Pure/term_ord.ML Author: Tobias Nipkow, TU Muenchen Author: Makarius Term orderings. *) signature TERM_ORD = sig val fast_indexname_ord: indexname ord val sort_ord: sort ord val typ_ord: typ ord val fast_term_ord: term ord val syntax_term_ord: term ord val indexname_ord: indexname ord val tvar_ord: (indexname * sort) ord val var_ord: (indexname * typ) ord val term_ord: term ord val hd_ord: term ord val term_lpo: (term -> int) -> term ord end; structure Term_Ord: TERM_ORD = struct (* fast syntactic ordering -- tuned for inequalities *) val fast_indexname_ord = pointer_eq_ord (int_ord o apply2 snd ||| fast_string_ord o apply2 fst); val sort_ord = pointer_eq_ord (dict_ord fast_string_ord); local fun cons_nr (TVar _) = 0 | cons_nr (TFree _) = 1 | cons_nr (Type _) = 2; in fun typ_ord TU = if pointer_eq TU then EQUAL else (case TU of (Type (a, Ts), Type (b, Us)) => (case fast_string_ord (a, b) of EQUAL => dict_ord typ_ord (Ts, Us) | ord => ord) | (TFree (a, S), TFree (b, S')) => (case fast_string_ord (a, b) of EQUAL => sort_ord (S, S') | ord => ord) | (TVar (xi, S), TVar (yj, S')) => (case fast_indexname_ord (xi, yj) of EQUAL => sort_ord (S, S') | ord => ord) | (T, U) => int_ord (cons_nr T, cons_nr U)); end; local fun cons_nr (Const _) = 0 | cons_nr (Free _) = 1 | cons_nr (Var _) = 2 | cons_nr (Bound _) = 3 | cons_nr (Abs _) = 4 | cons_nr (_ $ _) = 5; fun struct_ord (Abs (_, _, t), Abs (_, _, u)) = struct_ord (t, u) | struct_ord (t1 $ t2, u1 $ u2) = (case struct_ord (t1, u1) of EQUAL => struct_ord (t2, u2) | ord => ord) | struct_ord (t, u) = int_ord (cons_nr t, cons_nr u); fun atoms_ord (Abs (_, _, t), Abs (_, _, u)) = atoms_ord (t, u) | atoms_ord (t1 $ t2, u1 $ u2) = (case atoms_ord (t1, u1) of EQUAL => atoms_ord (t2, u2) | ord => ord) | atoms_ord (Const (a, _), Const (b, _)) = fast_string_ord (a, b) | atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y) | atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj) | atoms_ord (Bound i, Bound j) = int_ord (i, j) | atoms_ord _ = EQUAL; fun types_ord (Abs (_, T, t), Abs (_, U, u)) = (case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord) | types_ord (t1 $ t2, u1 $ u2) = (case types_ord (t1, u1) of EQUAL => types_ord (t2, u2) | ord => ord) | types_ord (Const (_, T), Const (_, U)) = typ_ord (T, U) | types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U) | types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U) | types_ord _ = EQUAL; fun comments_ord (Abs (x, _, t), Abs (y, _, u)) = (case fast_string_ord (x, y) of EQUAL => comments_ord (t, u) | ord => ord) | comments_ord (t1 $ t2, u1 $ u2) = (case comments_ord (t1, u1) of EQUAL => comments_ord (t2, u2) | ord => ord) | comments_ord _ = EQUAL; in val fast_term_ord = pointer_eq_ord (struct_ord ||| atoms_ord ||| types_ord); val syntax_term_ord = fast_term_ord ||| comments_ord; end; (* term_ord *) (*a linear well-founded AC-compatible ordering for terms: s < t <=> 1. size(s) < size(t) or 2. size(s) = size(t) and s=f(...) and t=g(...) and f (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord) | (t, u) => (case int_ord (size_of_term t, size_of_term u) of EQUAL => (case prod_ord hd_ord int_ord (hd_depth (t, 0), hd_depth (u, 0)) of EQUAL => args_ord (t, u) | ord => ord) | ord => ord)) and hd_ord (f, g) = prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g) and args_ord (f $ t, g $ u) = (case args_ord (f, g) of EQUAL => term_ord (t, u) | ord => ord) | args_ord _ = EQUAL; end; (* Lexicographic path order on terms *) (* See Baader & Nipkow, Term rewriting, CUP 1998. Without variables. Const, Var, Bound, Free and Abs are treated all as constants. f_ord maps terms to integers and serves two purposes: - Predicate on constant symbols. Those that are not recognised by f_ord must be mapped to ~1. - Order on the recognised symbols. These must be mapped to distinct integers >= 0. The argument of f_ord is never an application. *) local fun unrecognized (Const (a, T)) = ((1, ((a, 0), T)), 0) | unrecognized (Free (a, T)) = ((1, ((a, 0), T)), 0) | unrecognized (Var v) = ((1, v), 1) | unrecognized (Bound i) = ((1, (("", i), dummyT)), 2) | unrecognized (Abs (_, T, _)) = ((1, (("", 0), T)), 3); fun dest_hd f_ord t = let val ord = f_ord t in if ord = ~1 then unrecognized t else ((0, (("", ord), fastype_of t)), 0) end; fun term_lpo f_ord (s, t) = let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in if forall (fn si => term_lpo f_ord (si, t) = LESS) ss then case hd_ord f_ord (f, g) of GREATER => if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts then GREATER else LESS | EQUAL => if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts then list_ord (term_lpo f_ord) (ss, ts) else LESS | LESS => LESS else GREATER end and hd_ord f_ord (f, g) = case (f, g) of (Abs (_, T, t), Abs (_, U, u)) => (case term_lpo f_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord) | (_, _) => prod_ord (prod_ord int_ord (prod_ord indexname_ord typ_ord)) int_ord (dest_hd f_ord f, dest_hd f_ord g); in val term_lpo = term_lpo end; end; (* scalable collections *) structure Vartab = Table(type key = indexname val ord = Term_Ord.fast_indexname_ord); structure Sorttab = Table(type key = sort val ord = Term_Ord.sort_ord); structure Typtab = Table(type key = typ val ord = Term_Ord.typ_ord); structure Termtab: sig include TABLE; val term_cache: (term -> 'a) -> term -> 'a end = struct structure Table = Table(type key = term val ord = Term_Ord.fast_term_ord); open Table; fun term_cache f = Cache.create empty lookup update f; end; +structure Sortset = Set(type key = sort val ord = Term_Ord.sort_ord); +structure Termset = Set(type key = term val ord = Term_Ord.fast_term_ord); + structure Var_Graph = Graph(type key = indexname val ord = Term_Ord.fast_indexname_ord); structure Sort_Graph = Graph(type key = sort val ord = Term_Ord.sort_ord); structure Typ_Graph = Graph(type key = typ val ord = Term_Ord.typ_ord); structure Term_Graph = Graph(type key = term val ord = Term_Ord.fast_term_ord);

", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\", "\