diff --git a/src/HOL/SPARK/Tools/spark_vcs.ML b/src/HOL/SPARK/Tools/spark_vcs.ML --- a/src/HOL/SPARK/Tools/spark_vcs.ML +++ b/src/HOL/SPARK/Tools/spark_vcs.ML @@ -1,1122 +1,1122 @@ (* Title: HOL/SPARK/Tools/spark_vcs.ML Author: Stefan Berghofer Copyright: secunet Security Networks AG Store for verification conditions generated by SPARK/Ada. *) signature SPARK_VCS = sig val set_vcs: Fdl_Parser.decls -> Fdl_Parser.rules -> (string * string) * Fdl_Parser.vcs -> Path.T -> string -> theory -> theory val add_proof_fun: (typ option -> 'a -> term) -> string * ((string list * string) option * 'a) -> theory -> theory val add_type: string * (typ * (string * string) list) -> theory -> theory val lookup_vc: theory -> bool -> string -> (Element.context_i list * (string * thm list option * Element.context_i * Element.statement_i)) option val get_vcs: theory -> bool -> Element.context_i list * (binding * thm) list * (string * (string * thm list option * Element.context_i * Element.statement_i)) list val mark_proved: string -> thm list -> theory -> theory val close: bool -> theory -> theory val is_closed: theory -> bool end; structure SPARK_VCs: SPARK_VCS = struct open Fdl_Parser; (** theory data **) fun err_unfinished () = error "An unfinished SPARK environment is still open." val strip_number = apply2 implode o chop_suffix Fdl_Lexer.is_digit o raw_explode; val name_ord = prod_ord string_ord (option_ord int_ord) o apply2 (strip_number ##> Int.fromString); structure VCtab = Table(type key = string val ord = name_ord); structure VCs = Theory_Data ( type T = {pfuns: ((string list * string) option * term) Symtab.table, type_map: (typ * (string * string) list) Symtab.table, env: {ctxt: Element.context_i list, defs: (binding * thm) list, types: fdl_type tab, funs: (string list * string) tab, pfuns: ((string list * string) option * term) Symtab.table, ids: (term * string) Symtab.table * Name.context, proving: bool, vcs: (string * thm list option * (string * expr) list * (string * expr) list) VCtab.table, path: Path.T, prefix: string} option} val empty : T = {pfuns = Symtab.empty, type_map = Symtab.empty, env = NONE} val extend = I fun merge ({pfuns = pfuns1, type_map = type_map1, env = NONE}, {pfuns = pfuns2, type_map = type_map2, env = NONE}) = {pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2), type_map = Symtab.merge (op =) (type_map1, type_map2), env = NONE} | merge _ = err_unfinished () ) (** utilities **) val to_lower = raw_explode #> map Symbol.to_ascii_lower #> implode; val lcase_eq = (op =) o apply2 (to_lower o Long_Name.base_name); fun lookup_prfx "" tab s = Symtab.lookup tab s | lookup_prfx prfx tab s = (case Symtab.lookup tab s of NONE => Symtab.lookup tab (prfx ^ "__" ^ s) | x => x); fun strip_prfx s = let fun strip ys [] = ("", implode ys) | strip ys ("_" :: "_" :: xs) = (implode (rev xs), implode ys) | strip ys (x :: xs) = strip (x :: ys) xs in strip [] (rev (raw_explode s)) end; fun unprefix_pfun "" s = s | unprefix_pfun prfx s = let val (prfx', s') = strip_prfx s in if prfx = prfx' then s' else s end; fun mk_unop s t = let val T = fastype_of t in Const (s, T --> T) $ t end; fun mk_times (t, u) = let val setT = fastype_of t; val T = HOLogic.dest_setT setT; val U = HOLogic.dest_setT (fastype_of u) in Const (\<^const_name>\Sigma\, setT --> (T --> HOLogic.mk_setT U) --> HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u) end; fun get_type thy prfx ty = let val {type_map, ...} = VCs.get thy in lookup_prfx prfx type_map ty end; fun mk_type' _ _ "integer" = (HOLogic.intT, []) | mk_type' _ _ "boolean" = (HOLogic.boolT, []) | mk_type' thy prfx ty = (case get_type thy prfx ty of NONE => (Syntax.check_typ (Proof_Context.init_global thy) (Type (Sign.full_name thy (Binding.name ty), [])), []) | SOME p => p); fun mk_type thy prfx ty = fst (mk_type' thy prfx ty); val booleanN = "boolean"; val integerN = "integer"; fun define_overloaded (def_name, eq) lthy = let val ((c, _), rhs) = eq |> Syntax.check_term lthy |> Logic.dest_equals |>> dest_Free; val ((_, (_, thm)), lthy') = Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs)) lthy val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy'); val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm in (thm', lthy') end; fun strip_underscores s = strip_underscores (unsuffix "_" s) handle Fail _ => s; fun strip_tilde s = unsuffix "~" s ^ "_init" handle Fail _ => s; val mangle_name = strip_underscores #> strip_tilde; fun mk_variables thy prfx xs ty (tab, ctxt) = let val T = mk_type thy prfx ty; val (ys, ctxt') = fold_map Name.variant (map mangle_name xs) ctxt; val zs = map (Free o rpair T) ys; in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end; fun get_record_info thy T = (case Record.dest_recTs T of [(tyname, [\<^typ>\unit\])] => Record.get_info thy (Long_Name.qualifier tyname) | _ => NONE); fun find_field [] fname fields = find_first (curry lcase_eq fname o fst) fields | find_field cmap fname fields = (case AList.lookup (op =) cmap fname of NONE => NONE | SOME fname' => SOME (fname', the (AList.lookup (op =) fields fname'))); fun find_field' fname = get_first (fn (flds, fldty) => if member (op =) flds fname then SOME fldty else NONE); fun assoc_ty_err thy T s msg = error ("Type " ^ Syntax.string_of_typ_global thy T ^ " associated with SPARK type " ^ s ^ "\n" ^ msg); (** generate properties of enumeration types **) fun add_enum_type tyname tyname' thy = let val {case_name, ...} = the (BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] tyname'); val cs = map Const (the (BNF_LFP_Compat.get_constrs thy tyname')); val k = length cs; val T = Type (tyname', []); val p = Const (\<^const_name>\pos\, T --> HOLogic.intT); val v = Const (\<^const_name>\val\, HOLogic.intT --> T); val card = Const (\<^const_name>\card\, HOLogic.mk_setT T --> HOLogic.natT) $ HOLogic.mk_UNIV T; fun mk_binrel_def s f = Logic.mk_equals (Const (s, T --> T --> HOLogic.boolT), Abs ("x", T, Abs ("y", T, Const (s, HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ (f $ Bound 1) $ (f $ Bound 0)))); val (((def1, def2), def3), lthy) = thy |> Class.instantiation ([tyname'], [], \<^sort>\spark_enum\) |> define_overloaded ("pos_" ^ tyname ^ "_def", Logic.mk_equals (p, list_comb (Const (case_name, replicate k HOLogic.intT @ [T] ---> HOLogic.intT), map (HOLogic.mk_number HOLogic.intT) (0 upto k - 1)))) ||>> define_overloaded ("less_eq_" ^ tyname ^ "_def", mk_binrel_def \<^const_name>\less_eq\ p) ||>> define_overloaded ("less_" ^ tyname ^ "_def", mk_binrel_def \<^const_name>\less\ p); val UNIV_eq = Goal.prove lthy [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_UNIV T, HOLogic.mk_set T cs))) (fn {context = ctxt, ...} => resolve_tac ctxt @{thms subset_antisym} 1 THEN resolve_tac ctxt @{thms subsetI} 1 THEN Old_Datatype_Aux.exh_tac ctxt (K (#exhaust (BNF_LFP_Compat.the_info (Proof_Context.theory_of ctxt) [BNF_LFP_Compat.Keep_Nesting] tyname'))) 1 THEN ALLGOALS (asm_full_simp_tac ctxt)); val finite_UNIV = Goal.prove lthy [] [] (HOLogic.mk_Trueprop (Const (\<^const_name>\finite\, HOLogic.mk_setT T --> HOLogic.boolT) $ HOLogic.mk_UNIV T)) (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [UNIV_eq]) 1); val card_UNIV = Goal.prove lthy [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (card, HOLogic.mk_number HOLogic.natT k))) (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [UNIV_eq]) 1); val range_pos = Goal.prove lthy [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (\<^const_name>\image\, (T --> HOLogic.intT) --> HOLogic.mk_setT T --> HOLogic.mk_setT HOLogic.intT) $ p $ HOLogic.mk_UNIV T, Const (\<^const_name>\atLeastLessThan\, HOLogic.intT --> HOLogic.intT --> HOLogic.mk_setT HOLogic.intT) $ HOLogic.mk_number HOLogic.intT 0 $ (\<^term>\int\ $ card)))) (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [card_UNIV]) 1 THEN simp_tac (ctxt addsimps [UNIV_eq, def1]) 1 THEN resolve_tac ctxt @{thms subset_antisym} 1 THEN simp_tac ctxt 1 THEN resolve_tac ctxt @{thms subsetI} 1 THEN asm_full_simp_tac (ctxt addsimps @{thms interval_expand} delsimps @{thms atLeastLessThan_iff}) 1); val lthy' = Class.prove_instantiation_instance (fn ctxt => Class.intro_classes_tac ctxt [] THEN resolve_tac ctxt [finite_UNIV] 1 THEN resolve_tac ctxt [range_pos] 1 THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps [def3]) 1 THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps [def2]) 1) lthy; val (pos_eqs, val_eqs) = split_list (map_index (fn (i, c) => let val n = HOLogic.mk_number HOLogic.intT i; val th = Goal.prove lthy' [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (p $ c, n))) (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [def1]) 1); val th' = Goal.prove lthy' [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (v $ n, c))) (fn {context = ctxt, ...} => resolve_tac ctxt [@{thm inj_pos} RS @{thm injD}] 1 THEN simp_tac (ctxt addsimps [@{thm pos_val}, range_pos, card_UNIV, th]) 1) in (th, th') end) cs); val first_el = Goal.prove lthy' [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (\<^const_name>\first_el\, T), hd cs))) (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [@{thm first_el_def}, hd val_eqs]) 1); val last_el = Goal.prove lthy' [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (\<^const_name>\last_el\, T), List.last cs))) (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [@{thm last_el_def}, List.last val_eqs, card_UNIV]) 1); in lthy' |> Local_Theory.note ((Binding.name (tyname ^ "_card"), @{attributes [simp]}), [card_UNIV]) ||>> Local_Theory.note ((Binding.name (tyname ^ "_pos"), @{attributes [simp]}), pos_eqs) ||>> Local_Theory.note ((Binding.name (tyname ^ "_val"), @{attributes [simp]}), val_eqs) ||>> Local_Theory.note ((Binding.name (tyname ^ "_first_el"), @{attributes [simp]}), [first_el]) ||>> Local_Theory.note ((Binding.name (tyname ^ "_last_el"), @{attributes [simp]}), [last_el]) |> snd |> Local_Theory.exit_global end; fun check_no_assoc thy prfx s = case get_type thy prfx s of NONE => () | SOME _ => error ("Cannot associate a type with " ^ s ^ "\nsince it is no record or enumeration type"); fun check_enum [] [] = NONE | check_enum els [] = SOME ("has no element(s) " ^ commas els) | check_enum [] cs = SOME ("has extra element(s) " ^ commas (map (Long_Name.base_name o fst) cs)) | check_enum (el :: els) ((cname, _) :: cs) = if lcase_eq (el, cname) then check_enum els cs else SOME ("either has no element " ^ el ^ " or it is at the wrong position"); fun invert_map [] = I | invert_map cmap = map (apfst (the o AList.lookup (op =) (map swap cmap))); fun add_type_def prfx (s, Basic_Type ty) (ids, thy) = (check_no_assoc thy prfx s; (ids, Typedecl.abbrev_global (Binding.name s, [], NoSyn) (mk_type thy prfx ty) thy |> snd)) | add_type_def prfx (s, Enum_Type els) ((tab, ctxt), thy) = let val (thy', tyname) = (case get_type thy prfx s of NONE => let val tyb = Binding.name s; val tyname = Sign.full_name thy tyb in (thy |> BNF_LFP_Compat.add_datatype [BNF_LFP_Compat.Keep_Nesting] [((tyb, [], NoSyn), map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |> add_enum_type s tyname, tyname) end | SOME (T as Type (tyname, []), cmap) => (case BNF_LFP_Compat.get_constrs thy tyname of NONE => assoc_ty_err thy T s "is not a datatype" | SOME cs => let val (prfx', _) = strip_prfx s in case check_enum (map (unprefix_pfun prfx') els) (invert_map cmap cs) of NONE => (thy, tyname) | SOME msg => assoc_ty_err thy T s msg end) | SOME (T, _) => assoc_ty_err thy T s "is not a datatype"); val cs = map Const (the (BNF_LFP_Compat.get_constrs thy' tyname)); in ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab, fold Name.declare els ctxt), thy') end | add_type_def prfx (s, Array_Type (argtys, resty)) (ids, thy) = (check_no_assoc thy prfx s; (ids, Typedecl.abbrev_global (Binding.name s, [], NoSyn) (foldr1 HOLogic.mk_prodT (map (mk_type thy prfx) argtys) --> mk_type thy prfx resty) thy |> snd)) | add_type_def prfx (s, Record_Type fldtys) (ids, thy) = (ids, let val fldTs = maps (fn (flds, ty) => map (rpair (mk_type thy prfx ty)) flds) fldtys in case get_type thy prfx s of NONE => Record.add_record {overloaded = false} ([], Binding.name s) NONE (map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy | SOME (rT, cmap) => (case get_record_info thy rT of NONE => assoc_ty_err thy rT s "is not a record type" | SOME {fields, ...} => let val fields' = invert_map cmap fields in (case subtract (lcase_eq o apply2 fst) fldTs fields' of [] => () | flds => assoc_ty_err thy rT s ("has extra field(s) " ^ commas (map (Long_Name.base_name o fst) flds)); map (fn (fld, T) => case AList.lookup lcase_eq fields' fld of NONE => assoc_ty_err thy rT s ("has no field " ^ fld) | SOME U => T = U orelse assoc_ty_err thy rT s ("has field " ^ fld ^ " whose type\n" ^ Syntax.string_of_typ_global thy U ^ "\ndoes not match declared type\n" ^ Syntax.string_of_typ_global thy T)) fldTs; thy) end) end) | add_type_def prfx (s, Pending_Type) (ids, thy) = (ids, case get_type thy prfx s of SOME _ => thy | NONE => Typedecl.typedecl_global {final = true} (Binding.name s, [], NoSyn) thy |> snd); fun term_of_expr thy prfx types pfuns = let fun tm_of vs (Funct ("->", [e, e'])) = (HOLogic.mk_imp (fst (tm_of vs e), fst (tm_of vs e')), booleanN) | tm_of vs (Funct ("<->", [e, e'])) = (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN) | tm_of vs (Funct ("or", [e, e'])) = (HOLogic.mk_disj (fst (tm_of vs e), fst (tm_of vs e')), booleanN) | tm_of vs (Funct ("and", [e, e'])) = (HOLogic.mk_conj (fst (tm_of vs e), fst (tm_of vs e')), booleanN) | tm_of vs (Funct ("not", [e])) = (HOLogic.mk_not (fst (tm_of vs e)), booleanN) | tm_of vs (Funct ("=", [e, e'])) = (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN) | tm_of vs (Funct ("<>", [e, e'])) = (HOLogic.mk_not (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e'))), booleanN) | tm_of vs (Funct ("<", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\less\ (fst (tm_of vs e), fst (tm_of vs e')), booleanN) | tm_of vs (Funct (">", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\less\ (fst (tm_of vs e'), fst (tm_of vs e)), booleanN) | tm_of vs (Funct ("<=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\less_eq\ (fst (tm_of vs e), fst (tm_of vs e')), booleanN) | tm_of vs (Funct (">=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\less_eq\ (fst (tm_of vs e'), fst (tm_of vs e)), booleanN) | tm_of vs (Funct ("+", [e, e'])) = (HOLogic.mk_binop \<^const_name>\plus\ (fst (tm_of vs e), fst (tm_of vs e')), integerN) | tm_of vs (Funct ("-", [e, e'])) = (HOLogic.mk_binop \<^const_name>\minus\ (fst (tm_of vs e), fst (tm_of vs e')), integerN) | tm_of vs (Funct ("*", [e, e'])) = (HOLogic.mk_binop \<^const_name>\times\ (fst (tm_of vs e), fst (tm_of vs e')), integerN) | tm_of vs (Funct ("/", [e, e'])) = (HOLogic.mk_binop \<^const_name>\divide\ (fst (tm_of vs e), fst (tm_of vs e')), integerN) | tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop \<^const_name>\sdiv\ (fst (tm_of vs e), fst (tm_of vs e')), integerN) | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop \<^const_name>\modulo\ (fst (tm_of vs e), fst (tm_of vs e')), integerN) | tm_of vs (Funct ("-", [e])) = (mk_unop \<^const_name>\uminus\ (fst (tm_of vs e)), integerN) | tm_of vs (Funct ("**", [e, e'])) = (Const (\<^const_name>\power\, HOLogic.intT --> HOLogic.natT --> HOLogic.intT) $ fst (tm_of vs e) $ (\<^const>\nat\ $ fst (tm_of vs e')), integerN) | tm_of (tab, _) (Ident s) = (case Symtab.lookup tab s of SOME t_ty => t_ty | NONE => (case lookup_prfx prfx pfuns s of SOME (SOME ([], resty), t) => (t, resty) | _ => error ("Undeclared identifier " ^ s))) | tm_of _ (Number i) = (HOLogic.mk_number HOLogic.intT i, integerN) | tm_of vs (Quantifier (s, xs, ty, e)) = let val (ys, vs') = mk_variables thy prfx xs ty vs; val q = (case s of "for_all" => HOLogic.mk_all | "for_some" => HOLogic.mk_exists) in (fold_rev (fn Free (x, T) => fn t => q (x, T, t)) ys (fst (tm_of vs' e)), booleanN) end | tm_of vs (Funct (s, es)) = (* record field selection *) (case try (unprefix "fld_") s of SOME fname => (case es of [e] => let val (t, rcdty) = tm_of vs e; val (rT, cmap) = mk_type' thy prfx rcdty in case (get_record_info thy rT, lookup types rcdty) of (SOME {fields, ...}, SOME (Record_Type fldtys)) => (case (find_field cmap fname fields, find_field' fname fldtys) of (SOME (fname', fT), SOME fldty) => (Const (fname', rT --> fT) $ t, fldty) | _ => error ("Record " ^ rcdty ^ " has no field named " ^ fname)) | _ => error (rcdty ^ " is not a record type") end | _ => error ("Function " ^ s ^ " expects one argument")) | NONE => (* record field update *) (case try (unprefix "upf_") s of SOME fname => (case es of [e, e'] => let val (t, rcdty) = tm_of vs e; val (rT, cmap) = mk_type' thy prfx rcdty; val (u, fldty) = tm_of vs e'; val fT = mk_type thy prfx fldty in case get_record_info thy rT of SOME {fields, ...} => (case find_field cmap fname fields of SOME (fname', fU) => if fT = fU then (Const (fname' ^ "_update", (fT --> fT) --> rT --> rT) $ Abs ("x", fT, u) $ t, rcdty) else error ("Type\n" ^ Syntax.string_of_typ_global thy fT ^ "\ndoes not match type\n" ^ Syntax.string_of_typ_global thy fU ^ "\nof field " ^ fname) | NONE => error ("Record " ^ rcdty ^ " has no field named " ^ fname)) | _ => error (rcdty ^ " is not a record type") end | _ => error ("Function " ^ s ^ " expects two arguments")) | NONE => (* enumeration type to integer *) (case try (unsuffix "__pos") s of SOME tyname => (case es of [e] => (Const (\<^const_name>\pos\, mk_type thy prfx tyname --> HOLogic.intT) $ fst (tm_of vs e), integerN) | _ => error ("Function " ^ s ^ " expects one argument")) | NONE => (* integer to enumeration type *) (case try (unsuffix "__val") s of SOME tyname => (case es of [e] => (Const (\<^const_name>\val\, HOLogic.intT --> mk_type thy prfx tyname) $ fst (tm_of vs e), tyname) | _ => error ("Function " ^ s ^ " expects one argument")) | NONE => (* successor / predecessor of enumeration type element *) if s = "succ" orelse s = "pred" then (case es of [e] => let val (t, tyname) = tm_of vs e; val T = mk_type thy prfx tyname in (Const (if s = "succ" then \<^const_name>\succ\ else \<^const_name>\pred\, T --> T) $ t, tyname) end | _ => error ("Function " ^ s ^ " expects one argument")) (* user-defined proof function *) else (case lookup_prfx prfx pfuns s of SOME (SOME (_, resty), t) => (list_comb (t, map (fst o tm_of vs) es), resty) | _ => error ("Undeclared proof function " ^ s)))))) | tm_of vs (Element (e, es)) = let val (t, ty) = tm_of vs e in case lookup types ty of SOME (Array_Type (_, elty)) => (t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es), elty) | _ => error (ty ^ " is not an array type") end | tm_of vs (Update (e, es, e')) = let val (t, ty) = tm_of vs e in case lookup types ty of SOME (Array_Type (idxtys, elty)) => let val T = foldr1 HOLogic.mk_prodT (map (mk_type thy prfx) idxtys); val U = mk_type thy prfx elty; val fT = T --> U in (Const (\<^const_name>\fun_upd\, fT --> T --> U --> fT) $ t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es) $ fst (tm_of vs e'), ty) end | _ => error (ty ^ " is not an array type") end | tm_of vs (Record (s, flds)) = let val (T, cmap) = mk_type' thy prfx s; val {extension = (ext_name, _), fields, ...} = (case get_record_info thy T of NONE => error (s ^ " is not a record type") | SOME info => info); val flds' = map (apsnd (tm_of vs)) flds; val fnames = fields |> invert_map cmap |> map (Long_Name.base_name o fst); val fnames' = map fst flds; val (fvals, ftys) = split_list (map (fn s' => case AList.lookup lcase_eq flds' s' of SOME fval_ty => fval_ty | NONE => error ("Field " ^ s' ^ " missing in record " ^ s)) fnames); val _ = (case subtract lcase_eq fnames fnames' of [] => () | xs => error ("Extra field(s) " ^ commas xs ^ " in record " ^ s)); val _ = (case duplicates (op =) fnames' of [] => () | xs => error ("Duplicate field(s) " ^ commas xs ^ " in record " ^ s)) in (list_comb (Const (ext_name, map (mk_type thy prfx) ftys @ [HOLogic.unitT] ---> T), fvals @ [HOLogic.unit]), s) end | tm_of vs (Array (s, default, assocs)) = (case lookup types s of SOME (Array_Type (idxtys, elty)) => let val Ts = map (mk_type thy prfx) idxtys; val T = foldr1 HOLogic.mk_prodT Ts; val U = mk_type thy prfx elty; fun mk_idx' T (e, NONE) = HOLogic.mk_set T [fst (tm_of vs e)] | mk_idx' T (e, SOME e') = Const (\<^const_name>\atLeastAtMost\, T --> T --> HOLogic.mk_setT T) $ fst (tm_of vs e) $ fst (tm_of vs e'); fun mk_idx idx = if length Ts <> length idx then error ("Arity mismatch in construction of array " ^ s) else foldr1 mk_times (map2 mk_idx' Ts idx); fun mk_upd (idxs, e) t = if length idxs = 1 andalso forall (is_none o snd) (hd idxs) then Const (\<^const_name>\fun_upd\, (T --> U) --> T --> U --> T --> U) $ t $ foldl1 HOLogic.mk_prod (map (fst o tm_of vs o fst) (hd idxs)) $ fst (tm_of vs e) else Const (\<^const_name>\fun_upds\, (T --> U) --> HOLogic.mk_setT T --> U --> T --> U) $ t $ foldl1 (HOLogic.mk_binop \<^const_name>\sup\) (map mk_idx idxs) $ fst (tm_of vs e) in (fold mk_upd assocs (case default of SOME e => Abs ("x", T, fst (tm_of vs e)) | NONE => Const (\<^const_name>\undefined\, T --> U)), s) end | _ => error (s ^ " is not an array type")) in tm_of end; fun term_of_rule thy prfx types pfuns ids rule = let val tm_of = fst o term_of_expr thy prfx types pfuns ids in case rule of Inference_Rule (es, e) => Logic.list_implies (map (HOLogic.mk_Trueprop o tm_of) es, HOLogic.mk_Trueprop (tm_of e)) | Substitution_Rule (es, e, e') => Logic.list_implies (map (HOLogic.mk_Trueprop o tm_of) es, HOLogic.mk_Trueprop (HOLogic.mk_eq (tm_of e, tm_of e'))) end; val builtin = Symtab.make (map (rpair ()) ["->", "<->", "or", "and", "not", "=", "<>", "<", ">", "<=", ">=", "+", "-", "*", "/", "div", "mod", "**"]); fun complex_expr (Number _) = false | complex_expr (Ident _) = false | complex_expr (Funct (s, es)) = not (Symtab.defined builtin s) orelse exists complex_expr es | complex_expr (Quantifier (_, _, _, e)) = complex_expr e | complex_expr _ = true; fun complex_rule (Inference_Rule (es, e)) = complex_expr e orelse exists complex_expr es | complex_rule (Substitution_Rule (es, e, e')) = complex_expr e orelse complex_expr e' orelse exists complex_expr es; val is_pfun = Symtab.defined builtin orf can (unprefix "fld_") orf can (unprefix "upf_") orf can (unsuffix "__pos") orf can (unsuffix "__val") orf equal "succ" orf equal "pred"; fun fold_opt f = the_default I o Option.map f; fun fold_pair f g (x, y) = f x #> g y; fun fold_expr f g (Funct (s, es)) = f s #> fold (fold_expr f g) es | fold_expr f g (Ident s) = g s | fold_expr f g (Number _) = I | fold_expr f g (Quantifier (_, _, _, e)) = fold_expr f g e | fold_expr f g (Element (e, es)) = fold_expr f g e #> fold (fold_expr f g) es | fold_expr f g (Update (e, es, e')) = fold_expr f g e #> fold (fold_expr f g) es #> fold_expr f g e' | fold_expr f g (Record (_, flds)) = fold (fold_expr f g o snd) flds | fold_expr f g (Array (_, default, assocs)) = fold_opt (fold_expr f g) default #> fold (fold_pair (fold (fold (fold_pair (fold_expr f g) (fold_opt (fold_expr f g))))) (fold_expr f g)) assocs; fun add_expr_pfuns funs = fold_expr (fn s => if is_pfun s then I else insert (op =) s) (fn s => if is_none (lookup funs s) then I else insert (op =) s); val add_expr_idents = fold_expr (K I) (insert (op =)); fun pfun_type thy prfx (argtys, resty) = map (mk_type thy prfx) argtys ---> mk_type thy prfx resty; fun check_pfun_type thy prfx s t optty1 optty2 = let val T = fastype_of t; fun check ty = let val U = pfun_type thy prfx ty in T = U orelse error ("Type\n" ^ Syntax.string_of_typ_global thy T ^ "\nof function " ^ Syntax.string_of_term_global thy t ^ " associated with proof function " ^ s ^ "\ndoes not match declared type\n" ^ Syntax.string_of_typ_global thy U) end in (Option.map check optty1; Option.map check optty2; ()) end; fun upd_option x y = if is_some x then x else y; fun check_pfuns_types thy prfx funs = Symtab.map (fn s => fn (optty, t) => let val optty' = lookup funs (unprefix_pfun prfx s) in (check_pfun_type thy prfx s t optty optty'; (NONE |> upd_option optty |> upd_option optty', t)) end); (** the VC store **) fun pp_vcs msg vcs = Pretty.big_list msg (map (Pretty.str o fst) vcs); fun pp_open_vcs [] = Pretty.str "All verification conditions have been proved." | pp_open_vcs vcs = pp_vcs "The following verification conditions remain to be proved:" vcs; fun partition_vcs vcs = VCtab.fold_rev (fn (name, (trace, SOME thms, ps, cs)) => apfst (cons (name, (trace, thms, ps, cs))) | (name, (trace, NONE, ps, cs)) => apsnd (cons (name, (trace, ps, cs)))) vcs ([], []); fun insert_break prt = Pretty.blk (0, [Pretty.fbrk, prt]); fun print_open_vcs f vcs = (Pretty.writeln (f (pp_open_vcs (snd (partition_vcs vcs)))); vcs); fun set_env ctxt defs types funs ids vcs path prefix thy = VCs.map (fn {pfuns, type_map, env = NONE} => {pfuns = pfuns, type_map = type_map, env = SOME {ctxt = ctxt, defs = defs, types = types, funs = funs, pfuns = check_pfuns_types thy prefix funs pfuns, ids = ids, proving = false, vcs = print_open_vcs I vcs, path = path, prefix = prefix}} | _ => err_unfinished ()) thy; fun mk_pat s = (case Int.fromString s of SOME i => [HOLogic.mk_Trueprop (Var (("C", i), HOLogic.boolT))] | NONE => error ("Bad conclusion identifier: C" ^ s)); fun mk_vc thy prfx types pfuns ids name_concl (tr, proved, ps, cs) = let val prop_of = HOLogic.mk_Trueprop o fst o term_of_expr thy prfx types pfuns ids in (tr, proved, Element.Assumes (map (fn (s', e) => ((Binding.name ("H" ^ s'), []), [(prop_of e, [])])) ps), Element.Shows (map (fn (s', e) => (if name_concl then (Binding.name ("C" ^ s'), []) else Binding.empty_atts, [(prop_of e, mk_pat s')])) cs)) end; fun fold_vcs f vcs = VCtab.fold (fn (_, (_, _, ps, cs)) => fold f ps #> fold f cs) vcs; fun pfuns_of_vcs prfx funs pfuns vcs = fold_vcs (add_expr_pfuns funs o snd) vcs [] |> filter (is_none o lookup_prfx prfx pfuns); fun declare_missing_pfuns thy prfx funs pfuns vcs (tab, ctxt) = let val (fs, (tys, Ts)) = pfuns_of_vcs prfx funs pfuns vcs |> map_filter (fn s => lookup funs s |> Option.map (fn ty => (s, (SOME ty, pfun_type thy prfx ty)))) |> split_list ||> split_list; val (fs', ctxt') = fold_map Name.variant fs ctxt in (fold Symtab.update_new (fs ~~ (tys ~~ map Free (fs' ~~ Ts))) pfuns, Element.Fixes (map2 (fn s => fn T => (Binding.name s, SOME T, NoSyn)) fs' Ts), (tab, ctxt')) end; fun map_pfuns f {pfuns, type_map, env} = {pfuns = f pfuns, type_map = type_map, env = env} fun map_pfuns_env f {pfuns, type_map, env = SOME {ctxt, defs, types, funs, pfuns = pfuns_env, ids, proving, vcs, path, prefix}} = if proving then err_unfinished () else {pfuns = pfuns, type_map = type_map, env = SOME {ctxt = ctxt, defs = defs, types = types, funs = funs, pfuns = f pfuns_env, ids = ids, proving = false, vcs = vcs, path = path, prefix = prefix}}; fun add_proof_fun prep (s, (optty, raw_t)) thy = VCs.map (fn data as {env, ...} => let val (optty', prfx, map_pf) = (case env of SOME {funs, prefix, ...} => (lookup funs (unprefix_pfun prefix s), prefix, map_pfuns_env) | NONE => (NONE, "", map_pfuns)); val optty'' = NONE |> upd_option optty |> upd_option optty'; val t = prep (Option.map (pfun_type thy prfx) optty'') raw_t; val _ = (case fold_aterms (fn u => if is_Var u orelse is_Free u then insert (op =) u else I) t [] of [] => () | ts => error ("Term\n" ^ Syntax.string_of_term_global thy t ^ "\nto be associated with proof function " ^ s ^ " contains free variable(s) " ^ commas (map (Syntax.string_of_term_global thy) ts))); in (check_pfun_type thy prfx s t optty optty'; if is_some optty'' orelse is_none env then map_pf (Symtab.update_new (s, (optty'', t))) data handle Symtab.DUP _ => error ("Proof function " ^ s ^ " already associated with function") else error ("Undeclared proof function " ^ s)) end) thy; fun check_mapping _ _ [] _ = () | check_mapping err s cmap cs = (case duplicates (op = o apply2 fst) cmap of [] => (case duplicates (op = o apply2 snd) cmap of [] => (case subtract (op = o apsnd snd) cs cmap of [] => (case subtract (op = o apfst snd) cmap cs of [] => () | zs => err ("has extra " ^ s ^ "(s) " ^ commas zs)) | zs => err ("does not have " ^ s ^ "(s) " ^ commas (map snd zs))) | zs => error ("Several SPARK names are mapped to " ^ commas (map snd zs))) | zs => error ("The SPARK names " ^ commas (map fst zs) ^ " are mapped to more than one name")); fun add_type (s, (T as Type (tyname, Ts), cmap)) thy = let val cmap' = map (apsnd (Sign.intern_const thy)) cmap in thy |> VCs.map (fn {env = SOME _, ...} => err_unfinished () | {pfuns, type_map, env} => {pfuns = pfuns, type_map = Symtab.update_new (s, (T, cmap')) type_map, env = env} handle Symtab.DUP _ => error ("SPARK type " ^ s ^ " already associated with type")) |> (fn thy' => case BNF_LFP_Compat.get_constrs thy' tyname of NONE => (case get_record_info thy' T of NONE => thy' | SOME {fields, ...} => (check_mapping (assoc_ty_err thy' T s) "field" cmap' (map fst fields); thy')) | SOME cs => if null Ts then (map (fn (_, Type (_, [])) => () | (cname, _) => assoc_ty_err thy' T s ("has illegal constructor " ^ Long_Name.base_name cname)) cs; check_mapping (assoc_ty_err thy' T s) "constructor" cmap' (map fst cs); add_enum_type s tyname thy') else assoc_ty_err thy' T s "is illegal") end | add_type (s, (T, _)) thy = assoc_ty_err thy T s "is illegal"; val is_closed = is_none o #env o VCs.get; fun lookup_vc thy name_concl name = (case VCs.get thy of {env = SOME {vcs, types, funs, pfuns, ids, ctxt, prefix, ...}, ...} => (case VCtab.lookup vcs name of SOME vc => let val (pfuns', ctxt', ids') = declare_missing_pfuns thy prefix funs pfuns vcs ids in SOME (ctxt @ [ctxt'], mk_vc thy prefix types pfuns' ids' name_concl vc) end | NONE => NONE) | _ => NONE); fun get_vcs thy name_concl = (case VCs.get thy of {env = SOME {vcs, types, funs, pfuns, ids, ctxt, defs, prefix, ...}, ...} => let val (pfuns', ctxt', ids') = declare_missing_pfuns thy prefix funs pfuns vcs ids in (ctxt @ [ctxt'], defs, VCtab.dest vcs |> map (apsnd (mk_vc thy prefix types pfuns' ids' name_concl))) end | _ => ([], [], [])); fun mark_proved name thms = VCs.map (fn {pfuns, type_map, env = SOME {ctxt, defs, types, funs, pfuns = pfuns_env, ids, vcs, path, prefix, ...}} => {pfuns = pfuns, type_map = type_map, env = SOME {ctxt = ctxt, defs = defs, types = types, funs = funs, pfuns = pfuns_env, ids = ids, proving = true, vcs = print_open_vcs insert_break (VCtab.map_entry name (fn (trace, _, ps, cs) => (trace, SOME thms, ps, cs)) vcs), path = path, prefix = prefix}} | x => x); fun close incomplete thy = thy |> VCs.map (fn {pfuns, type_map, env} => (case env of NONE => error "No SPARK environment is currently open" | SOME {vcs, path, ...} => let val (proved, unproved) = partition_vcs vcs; val _ = Thm.consolidate (maps (#2 o snd) proved); val (proved', proved'') = List.partition (fn (_, (_, thms, _, _)) => Thm_Deps.has_skip_proof thms) proved; val _ = if null unproved then () else (if incomplete then warning else error) (Pretty.string_of (pp_open_vcs unproved)); val _ = if null proved' then () else warning (Pretty.string_of (pp_vcs "The following VCs are not marked as proved \ \because their proofs contain oracles:" proved')); val prv_path = Path.ext "prv" path; val _ = Export.export thy (Path.binding (prv_path, Position.none)) - [implode (map (fn (s, _) => snd (strip_number s) ^ - " -- proved by " ^ Distribution.version ^ "\n") proved'')]; + (proved'' |> map (fn (s, _) => + XML.Text (snd (strip_number s) ^ " -- proved by " ^ Distribution.version ^ "\n"))); in {pfuns = pfuns, type_map = type_map, env = NONE} end)) |> Sign.parent_path; (** set up verification conditions **) fun partition_opt f = let fun part ys zs [] = (rev ys, rev zs) | part ys zs (x :: xs) = (case f x of SOME y => part (y :: ys) zs xs | NONE => part ys (x :: zs) xs) in part [] [] end; fun dest_def (id, (Substitution_Rule ([], Ident s, rhs))) = SOME (id, (s, rhs)) | dest_def _ = NONE; fun mk_rulename (s, i) = Binding.name (s ^ string_of_int i); fun add_const prfx (s, ty) ((tab, ctxt), thy) = let val T = mk_type thy prfx ty; val b = Binding.name s; val c = Const (Sign.full_name thy b, T) in (c, ((Symtab.update (s, (c, ty)) tab, Name.declare s ctxt), Sign.add_consts [(b, T, NoSyn)] thy)) end; fun add_def prfx types pfuns consts (id, (s, e)) (ids as (tab, ctxt), thy) = (case lookup consts s of SOME ty => let val (t, ty') = term_of_expr thy prfx types pfuns ids e; val T = mk_type thy prfx ty; val T' = mk_type thy prfx ty'; val _ = T = T' orelse error ("Declared type " ^ ty ^ " of " ^ s ^ "\ndoes not match type " ^ ty' ^ " in definition"); val id' = mk_rulename id; val ((t', (_, th)), lthy') = Named_Target.theory_init thy |> Specification.definition NONE [] [] ((id', []), HOLogic.mk_Trueprop (HOLogic.mk_eq (Free (s, T), t))); val phi = Proof_Context.export_morphism lthy' (Proof_Context.init_global (Proof_Context.theory_of lthy')); in ((id', Morphism.thm phi th), ((Symtab.update (s, (Morphism.term phi t', ty)) tab, Name.declare s ctxt), Local_Theory.exit_global lthy')) end | NONE => error ("Undeclared constant " ^ s)); fun add_var prfx (s, ty) (ids, thy) = let val ([Free p], ids') = mk_variables thy prfx [s] ty ids in (p, (ids', thy)) end; fun add_init_vars prfx vcs (ids_thy as ((tab, _), _)) = fold_map (add_var prfx) (map_filter (fn s => case try (unsuffix "~") s of SOME s' => (case Symtab.lookup tab s' of SOME (_, ty) => SOME (s, ty) | NONE => error ("Undeclared identifier " ^ s')) | NONE => NONE) (fold_vcs (add_expr_idents o snd) vcs [])) ids_thy; fun is_trivial_vc ([], [(_, Ident "true")]) = true | is_trivial_vc _ = false; fun rulenames rules = commas (map (fn ((s, i), _) => s ^ "(" ^ string_of_int i ^ ")") rules); (* sort definitions according to their dependency *) fun sort_defs _ _ _ _ [] sdefs = rev sdefs | sort_defs prfx funs pfuns consts defs sdefs = (case find_first (fn (_, (_, e)) => forall (is_some o lookup_prfx prfx pfuns) (add_expr_pfuns funs e []) andalso forall (fn id => member (fn (s, (_, (s', _))) => s = s') sdefs id orelse consts id) (add_expr_idents e [])) defs of SOME d => sort_defs prfx funs pfuns consts (remove (op =) d defs) (d :: sdefs) | NONE => error ("Bad definitions: " ^ rulenames defs)); fun set_vcs ({types, vars, consts, funs} : decls) (rules, _) ((_, ident), vcs) path opt_prfx thy = let val prfx' = if opt_prfx = "" then space_implode "__" (Long_Name.explode (Long_Name.qualifier ident)) else opt_prfx; val prfx = to_lower prfx'; val {pfuns, ...} = VCs.get thy; val (defs, rules') = partition_opt dest_def rules; val consts' = subtract (fn ((_, (s, _)), (s', _)) => s = s') defs (items consts); (* ignore all complex rules in rls files *) val (rules'', other_rules) = List.partition (complex_rule o snd) rules'; val _ = if null rules'' then () else warning ("Ignoring rules: " ^ rulenames rules''); val vcs' = VCtab.make (maps (fn (tr, vcs) => map (fn (s, (ps, cs)) => (s, (tr, NONE, ps, cs))) (filter_out (is_trivial_vc o snd) vcs)) vcs); val _ = (case filter_out (is_some o lookup funs) (pfuns_of_vcs prfx funs pfuns vcs') of [] => () | fs => error ("Undeclared proof function(s) " ^ commas fs)); val (((defs', vars''), ivars), (ids, thy')) = ((Symtab.empty |> Symtab.update ("false", (\<^term>\False\, booleanN)) |> Symtab.update ("true", (\<^term>\True\, booleanN)), Name.context), thy |> Sign.add_path ((if prfx' = "" then "" else prfx' ^ "__") ^ Long_Name.base_name ident)) |> fold (add_type_def prfx) (items types) |> fold (snd oo add_const prfx) consts' |> (fn ids_thy as ((tab, _), _) => ids_thy |> fold_map (add_def prfx types pfuns consts) (sort_defs prfx funs pfuns (Symtab.defined tab) defs []) ||>> fold_map (add_var prfx) (items vars) ||>> add_init_vars prfx vcs'); val ctxt = [Element.Fixes (map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) (vars'' @ ivars)), Element.Assumes (map (fn (id, rl) => ((mk_rulename id, []), [(term_of_rule thy' prfx types pfuns ids rl, [])])) other_rules), Element.Notes ("", [((Binding.name "defns", []), map (rpair [] o single o snd) defs')])] in set_env ctxt defs' types funs ids vcs' path prfx thy' end; end; diff --git a/src/Pure/General/output.ML b/src/Pure/General/output.ML --- a/src/Pure/General/output.ML +++ b/src/Pure/General/output.ML @@ -1,197 +1,200 @@ (* Title: Pure/General/output.ML Author: Makarius Isabelle output channels. *) signature BASIC_OUTPUT = sig val writeln: string -> unit val tracing: string -> unit val warning: string -> unit val legacy_feature: string -> unit val profile_time: ('a -> 'b) -> 'a -> 'b val profile_time_thread: ('a -> 'b) -> 'a -> 'b val profile_allocations: ('a -> 'b) -> 'a -> 'b end; signature OUTPUT = sig include BASIC_OUTPUT type output = string val default_output: string -> output * int val default_escape: output -> string val add_mode: string -> (string -> output * int) -> (output -> string) -> unit val output_width: string -> output * int val output: string -> output val escape: output -> string val physical_stdout: output -> unit val physical_stderr: output -> unit val physical_writeln: output -> unit + type protocol_message_fn = Output_Primitives.protocol_message_fn exception Protocol_Message of Properties.T - val protocol_message_undefined: Properties.T -> string list -> unit + val protocol_message_undefined: protocol_message_fn val writelns: string list -> unit val state: string -> unit val information: string -> unit val error_message': serial * string -> unit val error_message: string -> unit val system_message: string -> unit val status: string list -> unit val report: string list -> unit val result: Properties.T -> string list -> unit - val protocol_message: Properties.T -> string list -> unit - val try_protocol_message: Properties.T -> string list -> unit + val protocol_message: protocol_message_fn + val try_protocol_message: protocol_message_fn end; signature PRIVATE_OUTPUT = sig include OUTPUT val writeln_fn: (output list -> unit) Unsynchronized.ref val state_fn: (output list -> unit) Unsynchronized.ref val information_fn: (output list -> unit) Unsynchronized.ref val tracing_fn: (output list -> unit) Unsynchronized.ref val warning_fn: (output list -> unit) Unsynchronized.ref val legacy_fn: (output list -> unit) Unsynchronized.ref val error_message_fn: (serial * output list -> unit) Unsynchronized.ref val system_message_fn: (output list -> unit) Unsynchronized.ref val status_fn: (output list -> unit) Unsynchronized.ref val report_fn: (output list -> unit) Unsynchronized.ref val result_fn: (Properties.T -> output list -> unit) Unsynchronized.ref - val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref + val protocol_message_fn: Output_Primitives.protocol_message_fn Unsynchronized.ref val init_channels: unit -> unit end; structure Private_Output: PRIVATE_OUTPUT = struct (** print modes **) type output = string; (*raw system output*) fun default_output s = (s, size s); fun default_escape (s: output) = s; local val default = {output = default_output, escape = default_escape}; val modes = Synchronized.var "Output.modes" (Symtab.make [("", default)]); in fun add_mode name output escape = if Thread_Data.is_virtual then () else Synchronized.change modes (Symtab.update_new (name, {output = output, escape = escape})); fun get_mode () = the_default default (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ())); end; fun output_width x = #output (get_mode ()) x; val output = #1 o output_width; fun escape x = #escape (get_mode ()) x; (** output channels **) (* primitives -- provided via bootstrap environment *) val writeln_fn = Unsynchronized.ref Output_Primitives.writeln_fn; val state_fn = Unsynchronized.ref Output_Primitives.state_fn; val information_fn = Unsynchronized.ref Output_Primitives.information_fn; val tracing_fn = Unsynchronized.ref Output_Primitives.tracing_fn; val warning_fn = Unsynchronized.ref Output_Primitives.warning_fn; val legacy_fn = Unsynchronized.ref Output_Primitives.legacy_fn; val error_message_fn = Unsynchronized.ref Output_Primitives.error_message_fn; val system_message_fn = Unsynchronized.ref Output_Primitives.system_message_fn; val status_fn = Unsynchronized.ref Output_Primitives.status_fn; val report_fn = Unsynchronized.ref Output_Primitives.report_fn; val result_fn = Unsynchronized.ref Output_Primitives.result_fn; + +type protocol_message_fn = Output_Primitives.protocol_message_fn; val protocol_message_fn = Unsynchronized.ref Output_Primitives.protocol_message_fn; (* physical output -- not to be used in user-space *) fun physical_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut); fun physical_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr); fun physical_writeln "" = () | physical_writeln s = physical_stdout (suffix "\n" s); (*atomic output!*) (* Isabelle output channels *) exception Protocol_Message of Properties.T; -fun protocol_message_undefined props (_: string list) = - raise Protocol_Message props; +val protocol_message_undefined: Output_Primitives.protocol_message_fn = + fn props => fn _ => raise Protocol_Message props; fun init_channels () = (writeln_fn := (physical_writeln o implode); state_fn := (fn ss => ! writeln_fn ss); information_fn := Output_Primitives.ignore_outputs; tracing_fn := (fn ss => ! writeln_fn ss); warning_fn := (physical_writeln o prefix_lines "### " o implode); legacy_fn := (fn ss => ! warning_fn ss); error_message_fn := (fn (_, ss) => physical_writeln (prefix_lines "*** " (implode ss))); system_message_fn := (fn ss => ! writeln_fn ss); status_fn := Output_Primitives.ignore_outputs; report_fn := Output_Primitives.ignore_outputs; result_fn := (fn _ => Output_Primitives.ignore_outputs); protocol_message_fn := protocol_message_undefined); val _ = if Thread_Data.is_virtual then () else init_channels (); fun writelns ss = ! writeln_fn (map output ss); fun writeln s = writelns [s]; fun state s = ! state_fn [output s]; fun information s = ! information_fn [output s]; fun tracing s = ! tracing_fn [output s]; fun warning s = ! warning_fn [output s]; fun legacy_feature s = ! legacy_fn [output ("Legacy feature! " ^ s)]; fun error_message' (i, s) = ! error_message_fn (i, [output s]); fun error_message s = error_message' (serial (), s); fun system_message s = ! system_message_fn [output s]; fun status ss = ! status_fn (map output ss); fun report ss = ! report_fn (map output ss); fun result props ss = ! result_fn props (map output ss); -fun protocol_message props ss = ! protocol_message_fn props (map output ss); -fun try_protocol_message props ss = protocol_message props ss handle Protocol_Message _ => (); +fun protocol_message props body = ! protocol_message_fn props body; +fun try_protocol_message props body = protocol_message props body handle Protocol_Message _ => (); (* profiling *) local fun output_profile title entries = let val body = entries |> sort (int_ord o apply2 fst) |> map (fn (count, name) => let val c = string_of_int count; val prefix = replicate_string (Int.max (0, 10 - size c)) " "; in prefix ^ c ^ " " ^ name end); val total = fold (curry (op +) o fst) entries 0; in if total = 0 then () else warning (cat_lines (title :: (body @ ["total: " ^ string_of_int total]))) end; in fun profile_time f x = ML_Profiling.profile_time (output_profile "time profile:") f x; fun profile_time_thread f x = ML_Profiling.profile_time_thread (output_profile "time profile (this thread):") f x; fun profile_allocations f x = ML_Profiling.profile_allocations (output_profile "allocations profile:") f x; end; end; structure Output: OUTPUT = Private_Output; structure Basic_Output: BASIC_OUTPUT = Output; open Basic_Output; diff --git a/src/Pure/General/output_primitives.ML b/src/Pure/General/output_primitives.ML --- a/src/Pure/General/output_primitives.ML +++ b/src/Pure/General/output_primitives.ML @@ -1,52 +1,80 @@ (* Title: Pure/General/output_primitives.ML Author: Makarius Primitives for Isabelle output channels. *) signature OUTPUT_PRIMITIVES = sig + structure XML: + sig + type attributes = (string * string) list + datatype tree = + Elem of (string * attributes) * tree list + | Text of string + type body = tree list + end type output = string type serial = int type properties = (string * string) list val ignore_outputs: output list -> unit val writeln_fn: output list -> unit val state_fn: output list -> unit val information_fn: output list -> unit val tracing_fn: output list -> unit val warning_fn: output list -> unit val legacy_fn: output list -> unit val error_message_fn: serial * output list -> unit val system_message_fn: output list -> unit val status_fn: output list -> unit val report_fn: output list -> unit val result_fn: properties -> output list -> unit - val protocol_message_fn: properties -> output list -> unit + type protocol_message_fn = properties -> XML.body -> unit + val protocol_message_fn: protocol_message_fn val markup_fn: string * properties -> output * output end; structure Output_Primitives: OUTPUT_PRIMITIVES = struct +(** XML trees **) + +structure XML = +struct + +type attributes = (string * string) list; + +datatype tree = + Elem of (string * attributes) * tree list + | Text of string; + +type body = tree list; +end; + + +(* output *) + type output = string; type serial = int; type properties = (string * string) list; fun ignore_outputs (_: output list) = (); val writeln_fn = ignore_outputs; val state_fn = ignore_outputs; val information_fn = ignore_outputs; val tracing_fn = ignore_outputs; val warning_fn = ignore_outputs; val legacy_fn = ignore_outputs; fun error_message_fn (_: serial, _: output list) = (); val system_message_fn = ignore_outputs; val status_fn = ignore_outputs; val report_fn = ignore_outputs; fun result_fn (_: properties) = ignore_outputs; -fun protocol_message_fn (_: properties) = ignore_outputs; + +type protocol_message_fn = properties -> XML.body -> unit; +val protocol_message_fn: protocol_message_fn = fn _ => fn _ => (); fun markup_fn (_: string * properties) = ("", ""); end; diff --git a/src/Pure/PIDE/protocol.ML b/src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML +++ b/src/Pure/PIDE/protocol.ML @@ -1,175 +1,174 @@ (* Title: Pure/PIDE/protocol.ML Author: Makarius Protocol message formats for interactive proof documents. *) structure Protocol: sig end = struct val _ = Isabelle_Process.protocol_command "Prover.echo" (fn args => List.app writeln args); val _ = Isabelle_Process.protocol_command "Prover.options" (fn [options_yxml] => (Options.set_default (Options.decode (YXML.parse_body options_yxml)); Isabelle_Process.init_options_interactive ())); val _ = Isabelle_Process.protocol_command "Prover.init_session_base" (fn [session_positions_yxml, session_directories_yxml, doc_names_yxml, global_theories_yxml, loaded_theories_yxml] => let val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end; val decode_list = YXML.parse_body #> let open XML.Decode in list string end; val decode_sessions = YXML.parse_body #> let open XML.Decode in list (pair string properties) end; in Resources.init_session_base {session_positions = decode_sessions session_positions_yxml, session_directories = decode_table session_directories_yxml, docs = decode_list doc_names_yxml, global_theories = decode_table global_theories_yxml, loaded_theories = decode_list loaded_theories_yxml} end); val _ = Isabelle_Process.protocol_command "Document.define_blob" (fn [digest, content] => Document.change_state (Document.define_blob digest content)); fun decode_command id name blobs_xml toks_xml sources : Document.command = let open XML.Decode; val (blobs_digests, blobs_index) = blobs_xml |> let val message = YXML.string_of_body o Protocol_Message.command_positions id; in pair (list (variant [fn ([], a) => Exn.Res (pair string (option string) a), fn ([], a) => Exn.Exn (ERROR (message a))])) int end; val toks = list (pair int int) toks_xml; in {command_id = Document_ID.parse id, name = name, blobs_digests = blobs_digests, blobs_index = blobs_index, tokens = toks ~~ sources} end; -fun commands_accepted ids = Output.protocol_message Markup.commands_accepted [commas ids]; +fun commands_accepted ids = Output.protocol_message Markup.commands_accepted [XML.Text (commas ids)]; val _ = Isabelle_Process.protocol_command "Document.define_command" (fn id :: name :: blobs :: toks :: sources => let val command = decode_command id name (YXML.parse_body blobs) (YXML.parse_body toks) sources; val _ = Document.change_state (Document.define_command command); in commands_accepted [id] end); val _ = Isabelle_Process.protocol_command "Document.define_commands" (fn args => let fun decode arg = let open XML.Decode; val (id, (name, (blobs_xml, (toks_xml, sources)))) = pair string (pair string (pair I (pair I (list string)))) (YXML.parse_body arg); in decode_command id name blobs_xml toks_xml sources end; val commands = map decode args; val _ = Document.change_state (fold Document.define_command commands); in commands_accepted (map (Value.print_int o #command_id) commands) end); val _ = Isabelle_Process.protocol_command "Document.discontinue_execution" (fn [] => Execution.discontinue ()); val _ = Isabelle_Process.protocol_command "Document.cancel_exec" (fn [exec_id] => Execution.cancel (Document_ID.parse exec_id)); val _ = Isabelle_Process.protocol_command "Document.update" (Future.task_context "Document.update" (Future.new_group NONE) (fn old_id_string :: new_id_string :: consolidate_yxml :: edits_yxml => Document.change_state (fn state => let val old_id = Document_ID.parse old_id_string; val new_id = Document_ID.parse new_id_string; val consolidate = YXML.parse_body consolidate_yxml |> let open XML.Decode in list string end; val edits = edits_yxml |> map (YXML.parse_body #> let open XML.Decode in pair string (variant [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), fn ([], a) => let val (master, (name, (imports, (keywords, errors)))) = pair string (pair string (pair (list string) (pair (list (pair string (pair (pair string (list string)) (list string)))) (list YXML.string_of_body)))) a; val imports' = map (rpair Position.none) imports; val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords; val header = Thy_Header.make (name, Position.none) imports' keywords'; in Document.Deps {master = master, header = header, errors = errors} end, fn (a :: b, c) => Document.Perspective (bool_atom a, map int_atom b, list (pair int (pair string (list string))) c)]) end); val _ = Execution.discontinue (); val (edited, removed, assign_update, state') = Document.update old_id new_id edits consolidate state; val _ = (singleton o Future.forks) {name = "Document.update/remove", group = NONE, deps = Execution.snapshot removed, pri = Task_Queue.urgent_pri + 2, interrupts = false} (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed)); val _ = Output.protocol_message Markup.assign_update ((new_id, edited, assign_update) |> let open XML.Encode; fun encode_upd (a, bs) = string (space_implode "," (map Value.print_int (a :: bs))); - in triple int (list string) (list encode_upd) end - |> YXML.chunks_of_body); + in triple int (list string) (list encode_upd) end); in Document.start_execution state' end))); val _ = Isabelle_Process.protocol_command "Document.remove_versions" (fn [versions_yxml] => Document.change_state (fn state => let val versions = YXML.parse_body versions_yxml |> let open XML.Decode in list int end; val state1 = Document.remove_versions versions state; - val _ = Output.protocol_message Markup.removed_versions [versions_yxml]; + val _ = Output.protocol_message Markup.removed_versions [XML.Text (versions_yxml)]; in state1 end)); val _ = Isabelle_Process.protocol_command "Document.dialog_result" (fn [serial, result] => Active.dialog_result (Value.parse_int serial) result handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn); val _ = Isabelle_Process.protocol_command "ML_Heap.share_common_data" (fn [] => ML_Heap.share_common_data ()); end; diff --git a/src/Pure/PIDE/xml.ML b/src/Pure/PIDE/xml.ML --- a/src/Pure/PIDE/xml.ML +++ b/src/Pure/PIDE/xml.ML @@ -1,420 +1,417 @@ (* Title: Pure/PIDE/xml.ML Author: David Aspinall Author: Stefan Berghofer Author: Makarius Untyped XML trees and representation of ML values. *) signature XML_DATA_OPS = sig type 'a A type 'a T type 'a V type 'a P val int_atom: int A val bool_atom: bool A val unit_atom: unit A val properties: Properties.T T val string: string T val int: int T val bool: bool T val unit: unit T val pair: 'a T -> 'b T -> ('a * 'b) T val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T val list: 'a T -> 'a list T val option: 'a T -> 'a option T val variant: 'a V list -> 'a T end; signature XML = sig type attributes = (string * string) list datatype tree = Elem of (string * attributes) * tree list | Text of string type body = tree list + val blob: string list -> body val xml_elemN: string val xml_nameN: string val xml_bodyN: string val wrap_elem: ((string * attributes) * tree list) * tree list -> tree val unwrap_elem: tree -> (((string * attributes) * tree list) * tree list) option val add_content: tree -> Buffer.T -> Buffer.T val content_of: body -> string val trim_blanks: body -> body val header: string val text: string -> string val element: string -> attributes -> string list -> string val output_markup: Markup.T -> Markup.output val string_of: tree -> string val pretty: int -> tree -> Pretty.T val output: tree -> BinIO.outstream -> unit val parse_comments: string list -> unit * string list val parse_string : string -> string option val parse_element: string list -> tree * string list val parse_document: string list -> tree * string list val parse: string -> tree exception XML_ATOM of string exception XML_BODY of body structure Encode: sig include XML_DATA_OPS val tree: tree T end structure Decode: sig include XML_DATA_OPS val tree: tree T end end; structure XML: XML = struct (** XML trees **) -type attributes = (string * string) list; +open Output_Primitives.XML; -datatype tree = - Elem of (string * attributes) * tree list - | Text of string; - -type body = tree list; +val blob = map Text; (* wrapped elements *) val xml_elemN = "xml_elem"; val xml_nameN = "xml_name"; val xml_bodyN = "xml_body"; fun wrap_elem (((a, atts), body1), body2) = Elem ((xml_elemN, (xml_nameN, a) :: atts), Elem ((xml_bodyN, []), body1) :: body2); fun unwrap_elem (Elem ((name, (n, a) :: atts), Elem ((name', atts'), body1) :: body2)) = if name = xml_elemN andalso n = xml_nameN andalso name' = xml_bodyN andalso null atts' then SOME (((a, atts), body1), body2) else NONE | unwrap_elem _ = NONE; (* text content *) fun add_content tree = (case unwrap_elem tree of SOME (_, ts) => fold add_content ts | NONE => (case tree of Elem (_, ts) => fold add_content ts | Text s => Buffer.add s)); fun content_of body = Buffer.empty |> fold add_content body |> Buffer.content; (* trim blanks *) fun trim_blanks trees = trees |> maps (fn Elem (markup, body) => [Elem (markup, trim_blanks body)] | Text s => let val s' = s |> raw_explode |> trim Symbol.is_blank |> implode; in if s' = "" then [] else [Text s'] end); (** string representation **) val header = "\n"; (* escaped text *) fun decode "<" = "<" | decode ">" = ">" | decode "&" = "&" | decode "'" = "'" | decode """ = "\"" | decode c = c; fun encode "<" = "<" | encode ">" = ">" | encode "&" = "&" | encode "'" = "'" | encode "\"" = """ | encode c = c; val text = translate_string encode; (* elements *) fun elem name atts = space_implode " " (name :: map (fn (a, x) => a ^ "=\"" ^ text x ^ "\"") atts); fun element name atts body = let val b = implode body in if b = "" then enclose "<" "/>" (elem name atts) else enclose "<" ">" (elem name atts) ^ b ^ enclose "" name end; fun output_markup (markup as (name, atts)) = if Markup.is_empty markup then Markup.no_output else (enclose "<" ">" (elem name atts), enclose "" name); (* output *) fun buffer_of depth tree = let fun traverse _ (Elem ((name, atts), [])) = Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add "/>" | traverse d (Elem ((name, atts), ts)) = Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add ">" #> traverse_body d ts #> Buffer.add " Buffer.add name #> Buffer.add ">" | traverse _ (Text s) = Buffer.add (text s) and traverse_body 0 _ = Buffer.add "..." | traverse_body d ts = fold (traverse (d - 1)) ts; in Buffer.empty |> traverse depth tree end; val string_of = Buffer.content o buffer_of ~1; val output = Buffer.output o buffer_of ~1; fun pretty depth tree = Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree)); val _ = ML_system_pp (fn depth => fn _ => Pretty.to_polyml o pretty (FixedInt.toInt depth)); (** XML parsing **) local fun err msg (xs, _) = fn () => "XML parsing error: " ^ msg () ^ "\nfound: " ^ quote (Symbol.beginning 100 xs); fun ignored _ = []; fun name_start_char c = Symbol.is_ascii_letter c orelse c = ":" orelse c = "_"; fun name_char c = name_start_char c orelse Symbol.is_ascii_digit c orelse c = "-" orelse c = "."; val parse_name = Scan.one name_start_char ::: Scan.many name_char; val blanks = Scan.many Symbol.is_blank; val special = $$ "&" ^^ (parse_name >> implode) ^^ $$ ";" >> decode; val regular = Scan.one Symbol.not_eof; fun regular_except x = Scan.one (fn c => Symbol.not_eof c andalso c <> x); val parse_chars = Scan.repeat1 (special || regular_except "<") >> implode; val parse_cdata = Scan.this_string "") regular) >> implode) --| Scan.this_string "]]>"; val parse_att = ((parse_name >> implode) --| (blanks -- $$ "=" -- blanks)) -- (($$ "\"" || $$ "'") :|-- (fn s => (Scan.repeat (special || regular_except s) >> implode) --| $$ s)); val parse_comment = Scan.this_string "") regular) -- Scan.this_string "-->" >> ignored; val parse_processing_instruction = Scan.this_string "") regular) -- Scan.this_string "?>" >> ignored; val parse_doctype = Scan.this_string "") regular) -- $$ ">" >> ignored; val parse_misc = Scan.one Symbol.is_blank >> ignored || parse_processing_instruction || parse_comment; val parse_optional_text = Scan.optional (parse_chars >> (single o Text)) []; in val parse_comments = blanks -- Scan.repeat (parse_comment -- blanks >> K ()) >> K (); val parse_string = Scan.read Symbol.stopper parse_chars o raw_explode; fun parse_content xs = (parse_optional_text @@@ Scan.repeats ((parse_element >> single || parse_cdata >> (single o Text) || parse_processing_instruction || parse_comment) @@@ parse_optional_text)) xs and parse_element xs = ($$ "<" |-- parse_name -- Scan.repeat (blanks |-- parse_att) --| blanks :-- (fn (name, _) => !! (err (fn () => "Expected > or />")) ($$ "/" -- $$ ">" >> ignored || $$ ">" |-- parse_content --| !! (err (fn () => "Expected ")) ($$ "<" -- $$ "/" -- Scan.this name -- blanks -- $$ ">"))) >> (fn ((name, atts), body) => Elem ((implode name, atts), body))) xs; val parse_document = (Scan.repeat parse_misc -- Scan.option parse_doctype -- Scan.repeat parse_misc) |-- parse_element; fun parse s = (case Scan.finite Symbol.stopper (Scan.error (!! (err (fn () => "Malformed element")) (blanks |-- parse_document --| blanks))) (raw_explode s) of (x, []) => x | (_, ys) => error ("XML parsing error: unprocessed input\n" ^ Symbol.beginning 100 ys)); end; (** XML as data representation language **) exception XML_ATOM of string; exception XML_BODY of tree list; structure Encode = struct type 'a A = 'a -> string; type 'a T = 'a -> body; type 'a V = 'a -> string list * body; type 'a P = 'a -> string list; (* atomic values *) fun int_atom i = Value.print_int i; fun bool_atom false = "0" | bool_atom true = "1"; fun unit_atom () = ""; (* structural nodes *) fun node ts = Elem ((":", []), ts); fun vector xs = map_index (fn (i, x) => (int_atom i, x)) xs; fun tagged (tag, (xs, ts)) = Elem ((int_atom tag, vector xs), ts); (* representation of standard types *) fun tree (t: tree) = [t]; fun properties props = [Elem ((":", props), [])]; fun string "" = [] | string s = [Text s]; val int = string o int_atom; val bool = string o bool_atom; val unit = string o unit_atom; fun pair f g (x, y) = [node (f x), node (g y)]; fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)]; fun list f xs = map (node o f) xs; fun option _ NONE = [] | option f (SOME x) = [node (f x)]; fun variant fs x = [tagged (the (get_index (fn f => SOME (f x) handle General.Match => NONE) fs))]; end; structure Decode = struct type 'a A = string -> 'a; type 'a T = body -> 'a; type 'a V = string list * body -> 'a; type 'a P = string list -> 'a; (* atomic values *) fun int_atom s = Value.parse_int s handle Fail _ => raise XML_ATOM s; fun bool_atom "0" = false | bool_atom "1" = true | bool_atom s = raise XML_ATOM s; fun unit_atom "" = () | unit_atom s = raise XML_ATOM s; (* structural nodes *) fun node (Elem ((":", []), ts)) = ts | node t = raise XML_BODY [t]; fun vector atts = map_index (fn (i, (a, x)) => if int_atom a = i then x else raise XML_ATOM a) atts; fun tagged (Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts)) | tagged t = raise XML_BODY [t]; (* representation of standard types *) fun tree [t] = t | tree ts = raise XML_BODY ts; fun properties [Elem ((":", props), [])] = props | properties ts = raise XML_BODY ts; fun string [] = "" | string [Text s] = s | string ts = raise XML_BODY ts; val int = int_atom o string; val bool = bool_atom o string; val unit = unit_atom o string; fun pair f g [t1, t2] = (f (node t1), g (node t2)) | pair _ _ ts = raise XML_BODY ts; fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3)) | triple _ _ _ ts = raise XML_BODY ts; fun list f ts = map (f o node) ts; fun option _ [] = NONE | option f [t] = SOME (f (node t)) | option _ ts = raise XML_BODY ts; fun variant fs [t] = let val (tag, (xs, ts)) = tagged t; val f = nth fs tag handle General.Subscript => raise XML_BODY [t]; in f (xs, ts) end | variant _ ts = raise XML_BODY ts; end; end; diff --git a/src/Pure/PIDE/yxml.ML b/src/Pure/PIDE/yxml.ML --- a/src/Pure/PIDE/yxml.ML +++ b/src/Pure/PIDE/yxml.ML @@ -1,162 +1,167 @@ (* Title: Pure/PIDE/yxml.ML Author: Makarius Efficient text representation of XML trees using extra characters X and Y -- no escaping, may nest marked text verbatim. Suitable for direct inlining into plain text. Markup ...body... is encoded as: X Y name Y att=val ... X ... body ... X Y X *) signature YXML = sig val X: Symbol.symbol val Y: Symbol.symbol val embed_controls: string -> string val detect: string -> bool val traverse: (string -> 'a -> 'a) -> XML.tree -> 'a -> 'a val buffer: XML.tree -> Buffer.T -> Buffer.T val chunks_of_body: XML.body -> string list val string_of_body: XML.body -> string val string_of: XML.tree -> string + val write_body: Path.T -> XML.body -> unit val output_markup: Markup.T -> string * string val output_markup_elem: Markup.T -> (string * string) * string val parse_body: string -> XML.body val parse: string -> XML.tree val content_of: string -> string end; structure YXML: YXML = struct (** string representation **) (* idempotent recoding of certain low ASCII control characters *) fun pseudo_utf8 c = if Symbol.is_ascii_control c then chr 192 ^ chr (128 + ord c) else c; fun embed_controls str = if exists_string Symbol.is_ascii_control str then translate_string pseudo_utf8 str else str; (* markers *) val X_char = Char.chr 5; val Y_char = Char.chr 6; val X = String.str X_char; val Y = String.str Y_char; val XY = X ^ Y; val XYX = XY ^ X; fun detect s = Char.contains s X_char orelse Char.contains s Y_char; (* output *) fun traverse string = let fun attrib (a, x) = string Y #> string a #> string "=" #> string x; fun tree (XML.Elem ((name, atts), ts)) = string XY #> string name #> fold attrib atts #> string X #> fold tree ts #> string XYX | tree (XML.Text s) = string s; in tree end; val buffer = traverse Buffer.add; fun chunks_of_body body = Buffer.empty |> fold buffer body |> Buffer.chunks; fun string_of_body body = Buffer.empty |> fold buffer body |> Buffer.content; val string_of = string_of_body o single; +fun write_body path body = + path |> File.open_output (fn file => + fold (traverse (fn s => fn () => BinIO.output (file, Byte.stringToBytes s))) body ()); + (* markup elements *) val Z = chr 0; val Z_text = [XML.Text Z]; fun output_markup (markup as (name, atts)) = if Markup.is_empty markup then Markup.no_output else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX); fun output_markup_elem markup = let val [bg1, bg2, en] = space_explode Z (string_of (XML.wrap_elem ((markup, Z_text), Z_text))) in ((bg1, bg2), en) end; (** efficient YXML parsing **) local (* splitting *) val split_string = Substring.full #> Substring.tokens (fn c => c = X_char) #> map (Substring.fields (fn c => c = Y_char) #> map Substring.string); (* structural errors *) fun err msg = raise Fail ("Malformed YXML: " ^ msg); fun err_attribute () = err "bad attribute"; fun err_element () = err "bad element"; fun err_unbalanced "" = err "unbalanced element" | err_unbalanced name = err ("unbalanced element " ^ quote name); (* stack operations *) fun add x ((elem, body) :: pending) = (elem, x :: body) :: pending; fun push "" _ _ = err_element () | push name atts pending = ((name, atts), []) :: pending; fun pop ((("", _), _) :: _) = err_unbalanced "" | pop ((markup, body) :: pending) = add (XML.Elem (markup, rev body)) pending; (* parsing *) fun parse_attrib s = (case first_field "=" s of NONE => err_attribute () | SOME ("", _) => err_attribute () | SOME att => att); fun parse_chunk ["", ""] = pop | parse_chunk ("" :: name :: atts) = push name (map parse_attrib atts) | parse_chunk txts = fold (add o XML.Text) txts; in fun parse_body source = (case fold parse_chunk (split_string source) [(("", []), [])] of [(("", _), result)] => rev result | ((name, _), _) :: _ => err_unbalanced name); fun parse source = (case parse_body source of [result] => result | [] => XML.Text "" | _ => err "multiple results"); end; val content_of = parse_body #> XML.content_of; end; diff --git a/src/Pure/System/invoke_scala.ML b/src/Pure/System/invoke_scala.ML --- a/src/Pure/System/invoke_scala.ML +++ b/src/Pure/System/invoke_scala.ML @@ -1,69 +1,69 @@ (* Title: Pure/System/invoke_scala.ML Author: Makarius JVM method invocation service via Isabelle/Scala. *) signature INVOKE_SCALA = sig val method: string -> string -> string val promise_method: string -> string -> string future exception Null end; structure Invoke_Scala: INVOKE_SCALA = struct val _ = Session.protocol_handler "isabelle.Invoke_Scala"; (* pending promises *) val new_id = string_of_int o Counter.make (); val promises = Synchronized.var "Invoke_Scala.promises" (Symtab.empty: string future Symtab.table); (* method invocation *) fun promise_method name arg = let val id = new_id (); fun abort () = Output.protocol_message (Markup.cancel_scala id) []; val promise = Future.promise_name "invoke_scala" abort : string future; val _ = Synchronized.change promises (Symtab.update (id, promise)); - val _ = Output.protocol_message (Markup.invoke_scala name id) [arg]; + val _ = Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg]; in promise end; fun method name arg = Future.join (promise_method name arg); (* fulfill *) exception Null; fun fulfill id tag res = let val result = (case tag of "0" => Exn.Exn Null | "1" => Exn.Res res | "2" => Exn.Exn (ERROR res) | "3" => Exn.Exn (Fail res) | "4" => Exn.Exn Exn.Interrupt | _ => raise Fail "Bad tag"); val promise = Synchronized.change_result promises (fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab)); val _ = Future.fulfill_result promise result; in () end; val _ = Isabelle_Process.protocol_command "Invoke_Scala.fulfill" (fn [id, tag, res] => fulfill id tag res handle exn => if Exn.is_interrupt exn then () else Exn.reraise exn); end; diff --git a/src/Pure/System/isabelle_process.ML b/src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML +++ b/src/Pure/System/isabelle_process.ML @@ -1,229 +1,230 @@ (* Title: Pure/System/isabelle_process.ML Author: Makarius Isabelle process wrapper. *) signature ISABELLE_PROCESS = sig val is_active: unit -> bool val protocol_command: string -> (string list -> unit) -> unit val reset_tracing: Document_ID.exec -> unit val crashes: exn list Synchronized.var val init_options: unit -> unit val init_options_interactive: unit -> unit val init: unit -> unit end; structure Isabelle_Process: ISABELLE_PROCESS = struct (* print mode *) val isabelle_processN = "isabelle_process"; fun is_active () = Print_Mode.print_mode_active isabelle_processN; val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape; val _ = Markup.add_mode isabelle_processN YXML.output_markup; (* protocol commands *) local val commands = Synchronized.var "Isabelle_Process.commands" (Symtab.empty: (string list -> unit) Symtab.table); in fun protocol_command name cmd = Synchronized.change commands (fn cmds => (if not (Symtab.defined cmds name) then () else warning ("Redefining Isabelle protocol command " ^ quote name); Symtab.update (name, cmd) cmds)); fun run_command name args = (case Symtab.lookup (Synchronized.value commands) name of NONE => error ("Undefined Isabelle protocol command " ^ quote name) | SOME cmd => (Runtime.exn_trace_system (fn () => cmd args) handle _ (*sic!*) => error ("Isabelle protocol command failure: " ^ quote name))); end; (* restricted tracing messages *) val tracing_messages = Synchronized.var "tracing_messages" (Inttab.empty: int Inttab.table); fun reset_tracing exec_id = Synchronized.change tracing_messages (Inttab.delete_safe exec_id); fun update_tracing () = (case Position.parse_id (Position.thread_data ()) of NONE => () | SOME exec_id => let val ok = Synchronized.change_result tracing_messages (fn tab => let val n = the_default 0 (Inttab.lookup tab exec_id) + 1; val limit = Options.default_int "editor_tracing_messages"; val ok = limit <= 0 orelse n <= limit; in (ok, Inttab.update (exec_id, n) tab) end); in if ok then () else let val (text, promise) = Active.dialog_text (); val _ = writeln ("Tracing paused. " ^ text "Stop" ^ ", or continue with next " ^ text "100" ^ ", " ^ text "1000" ^ ", " ^ text "10000" ^ " messages?") val m = Value.parse_int (Future.join promise) handle Fail _ => error "Stopped"; in Synchronized.change tracing_messages (Inttab.map_default (exec_id, 0) (fn k => k - m)) end end); (* output channels *) val serial_props = Markup.serial_properties o serial; fun init_channels out_stream = let val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF); val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF); val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF); val msg_channel = Message_Channel.make out_stream; fun message name props body = Message_Channel.send msg_channel (Message_Channel.message name props body); fun standard_message props name body = if forall (fn s => s = "") body then () else let val props' = (case (Properties.defined props Markup.idN, Position.get_id (Position.thread_data ())) of (false, SOME id') => props @ [(Markup.idN, id')] | _ => props); in message name props' body end; in Private_Output.status_fn := standard_message [] Markup.statusN; Private_Output.report_fn := standard_message [] Markup.reportN; Private_Output.result_fn := (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s); Private_Output.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s); Private_Output.state_fn := (fn s => standard_message (serial_props ()) Markup.stateN s); Private_Output.information_fn := (fn s => standard_message (serial_props ()) Markup.informationN s); Private_Output.tracing_fn := (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s)); Private_Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s); Private_Output.legacy_fn := (fn s => standard_message (serial_props ()) Markup.legacyN s); Private_Output.error_message_fn := (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s); Private_Output.system_message_fn := message Markup.systemN []; - Private_Output.protocol_message_fn := message Markup.protocolN; + Private_Output.protocol_message_fn := + (fn props => fn body => message Markup.protocolN props (YXML.chunks_of_body body)); Session.init_protocol_handlers (); message Markup.initN [] [Session.welcome ()]; msg_channel end; (* protocol loop -- uninterruptible *) val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list); local fun recover crash = (Synchronized.change crashes (cons crash); Output.physical_stderr "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n"); in fun loop stream = let val continue = (case Byte_Message.read_message stream of NONE => false | SOME [] => (Output.system_message "Isabelle process: no input"; true) | SOME (name :: args) => (run_command name args; true)) handle exn => (Runtime.exn_system_message exn handle crash => recover crash; true); in if continue then loop stream else (Future.shutdown (); Execution.reset (); ()) end; end; (* init protocol *) val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN]; val default_modes2 = [isabelle_processN, Pretty.symbolicN]; val init_protocol = Thread_Attributes.uninterruptible (fn _ => fn (address, password) => let val _ = SHA1.test_samples () handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn); val _ = Output.physical_stderr Symbol.STX; val _ = Context.put_generic_context NONE; val _ = Unsynchronized.change print_mode (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2); val (in_stream, out_stream) = Socket_IO.open_streams address; val _ = Byte_Message.write_line out_stream password; val msg_channel = init_channels out_stream; val _ = loop in_stream; val _ = Message_Channel.shutdown msg_channel; val _ = Private_Output.init_channels (); val _ = print_mode := []; in () end); (* init options *) fun init_options () = (ML_Print_Depth.set_print_depth (Options.default_int "ML_print_depth"); Future.ML_statistics := Options.default_bool "ML_statistics"; Multithreading.trace := Options.default_int "threads_trace"; Multithreading.max_threads_update (Options.default_int "threads"); Multithreading.parallel_proofs := Options.default_int "parallel_proofs"; if Options.default_bool "export_standard_proofs" then Proofterm.proofs := 2 else (); let val proofs = Options.default_int "record_proofs" in if proofs < 0 then () else Proofterm.proofs := proofs end; Printer.show_markup_default := false); fun init_options_interactive () = (init_options (); Multithreading.parallel_proofs := (if Options.default_int "parallel_proofs" > 0 then 3 else 0); Printer.show_markup_default := true); (* generic init *) fun init () = let val address = Options.default_string \<^system_option>\system_channel_address\; val password = Options.default_string \<^system_option>\system_channel_password\; in if address <> "" andalso password <> "" then init_protocol (address, password) else init_options () end; end; diff --git a/src/Pure/Thy/export.ML b/src/Pure/Thy/export.ML --- a/src/Pure/Thy/export.ML +++ b/src/Pure/Thy/export.ML @@ -1,91 +1,94 @@ (* Title: Pure/Thy/export.ML Author: Makarius Manage theory exports: compressed blobs. *) signature EXPORT = sig val report_export: theory -> Path.binding -> unit type params = {theory: theory, binding: Path.binding, executable: bool, compress: bool, strict: bool} - val export_params: params -> string list -> unit - val export: theory -> Path.binding -> string list -> unit - val export_executable: theory -> Path.binding -> string list -> unit + val export_params: params -> XML.body -> unit + val export: theory -> Path.binding -> XML.body -> unit + val export_executable: theory -> Path.binding -> XML.body -> unit val export_file: theory -> Path.binding -> Path.T -> unit val export_executable_file: theory -> Path.binding -> Path.T -> unit val markup: theory -> Path.T -> Markup.T val message: theory -> Path.T -> string - val protocol_message: Properties.T -> string list -> unit + val protocol_message: Output.protocol_message_fn end; structure Export: EXPORT = struct (* export *) fun report_export thy binding = let val theory_name = Context.theory_long_name thy; val (path, pos) = Path.dest_binding binding; val markup = Markup.export_path (Path.implode (Path.append (Path.basic theory_name) path)); in Context_Position.report_generic (Context.Theory thy) pos markup end; type params = {theory: theory, binding: Path.binding, executable: bool, compress: bool, strict: bool}; -fun export_params ({theory = thy, binding, executable, compress, strict}: params) blob = +fun export_params ({theory = thy, binding, executable, compress, strict}: params) body = (report_export thy binding; (Output.try_protocol_message o Markup.export) {id = Position.get_id (Position.thread_data ()), serial = serial (), theory_name = Context.theory_long_name thy, name = Path.implode_binding (tap Path.proper_binding binding), executable = executable, compress = compress, - strict = strict} blob); - -fun export thy binding blob = - export_params - {theory = thy, binding = binding, executable = false, compress = true, strict = true} blob; + strict = strict} body); -fun export_executable thy binding blob = +fun export thy binding body = export_params - {theory = thy, binding = binding, executable = true, compress = true, strict = true} blob; + {theory = thy, binding = binding, executable = false, compress = true, strict = true} body; -fun export_file thy binding file = export thy binding [File.read file]; -fun export_executable_file thy binding file = export_executable thy binding [File.read file]; +fun export_executable thy binding body = + export_params + {theory = thy, binding = binding, executable = true, compress = true, strict = true} body; + +fun export_file thy binding file = + export thy binding [XML.Text (File.read file)]; + +fun export_executable_file thy binding file = + export_executable thy binding [XML.Text (File.read file)]; (* information message *) fun markup thy path = let val thy_path = Path.append (Path.basic (Context.theory_long_name thy)) path; val name = (Markup.nameN, Path.implode thy_path); in Active.make_markup Markup.theory_exportsN {implicit = false, properties = [name]} end; fun message thy path = "See " ^ Markup.markup (markup thy path) "theory exports"; (* protocol message (bootstrap) *) -fun protocol_message props output = +fun protocol_message props body = (case props of function :: args => if function = (Markup.functionN, Markup.exportN) andalso not (null args) andalso #1 (hd args) = Markup.idN then let val path = Path.expand (Path.explode ("$ISABELLE_EXPORT_TMP/export" ^ serial_string ())); - val _ = File.write_list path output; + val _ = YXML.write_body path body; in Protocol_Message.inline (#2 function) (tl args @ [(Markup.fileN, Path.implode path)]) end else raise Output.Protocol_Message props | [] => raise Output.Protocol_Message props); val _ = if Thread_Data.is_virtual then () else Private_Output.protocol_message_fn := protocol_message; end; diff --git a/src/Pure/Thy/export_theory.ML b/src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML +++ b/src/Pure/Thy/export_theory.ML @@ -1,427 +1,427 @@ (* Title: Pure/Thy/export_theory.ML Author: Makarius Export foundational theory content and locale/class structure. *) signature EXPORT_THEORY = sig val setup_presentation: (Thy_Info.presentation_context -> theory -> unit) -> unit val export_body: theory -> string -> XML.body -> unit end; structure Export_Theory: EXPORT_THEORY = struct (* approximative syntax *) val get_syntax = Syntax.get_approx o Proof_Context.syn_of; fun get_syntax_type ctxt = get_syntax ctxt o Lexicon.mark_type; fun get_syntax_const ctxt = get_syntax ctxt o Lexicon.mark_const; fun get_syntax_fixed ctxt = get_syntax ctxt o Lexicon.mark_fixed; fun get_syntax_param ctxt loc x = let val thy = Proof_Context.theory_of ctxt in if Class.is_class thy loc then (case AList.lookup (op =) (Class.these_params thy [loc]) x of NONE => NONE | SOME (_, (c, _)) => get_syntax_const ctxt c) else get_syntax_fixed ctxt x end; val encode_syntax = XML.Encode.variant [fn NONE => ([], []), fn SOME (Syntax.Prefix delim) => ([delim], []), fn SOME (Syntax.Infix {assoc, delim, pri}) => let val ass = (case assoc of Printer.No_Assoc => 0 | Printer.Left_Assoc => 1 | Printer.Right_Assoc => 2); open XML.Encode Term_XML.Encode; in ([], triple int string int (ass, delim, pri)) end]; (* free variables: not declared in the context *) val is_free = not oo Name.is_declared; fun add_frees used = fold_aterms (fn Free (x, T) => is_free used x ? insert (op =) (x, T) | _ => I); fun add_tfrees used = (fold_types o fold_atyps) (fn TFree (a, S) => is_free used a ? insert (op =) (a, S) | _ => I); (* spec rules *) fun primrec_types ctxt const = Spec_Rules.retrieve ctxt (Const const) |> get_first (fn (Spec_Rules.Equational (Spec_Rules.Primrec types), _) => SOME (types, false) | (Spec_Rules.Equational (Spec_Rules.Primcorec types), _) => SOME (types, true) | _ => NONE) |> the_default ([], false); (* locales content *) fun locale_content thy loc = let val ctxt = Locale.init loc thy; val args = Locale.params_of thy loc |> map (fn ((x, T), _) => ((x, T), get_syntax_param ctxt loc x)); val axioms = let val (asm, defs) = Locale.specification_of thy loc; val cprops = map (Thm.cterm_of ctxt) (the_list asm @ defs); val (intro1, intro2) = Locale.intros_of thy loc; val intros_tac = Method.try_intros_tac ctxt (the_list intro1 @ the_list intro2) []; val res = Goal.init (Conjunction.mk_conjunction_balanced cprops) |> (ALLGOALS Goal.conjunction_tac THEN intros_tac) |> try Seq.hd; in (case res of SOME goal => Thm.prems_of goal | NONE => raise Fail ("Cannot unfold locale " ^ quote loc)) end; val typargs = rev (fold Term.add_tfrees (map (Free o #1) args @ axioms) []); in {typargs = typargs, args = args, axioms = axioms} end; fun get_locales thy = Locale.get_locales thy |> map_filter (fn loc => if Experiment.is_experiment thy loc then NONE else SOME (loc, ())); fun get_dependencies prev_thys thy = Locale.dest_dependencies prev_thys thy |> map_filter (fn dep => if Experiment.is_experiment thy (#source dep) orelse Experiment.is_experiment thy (#target dep) then NONE else let val (type_params, params) = Locale.parameters_of thy (#source dep); val typargs = fold (Term.add_tfreesT o #2 o #1) params type_params; val substT = typargs |> map_filter (fn v => let val T = TFree v; val T' = Morphism.typ (#morphism dep) T; in if T = T' then NONE else SOME (v, T') end); val subst = params |> map_filter (fn (v, _) => let val t = Free v; val t' = Morphism.term (#morphism dep) t; in if t aconv t' then NONE else SOME (v, t') end); in SOME (dep, (substT, subst)) end); (* general setup *) fun setup_presentation f = Theory.setup (Thy_Info.add_presentation (fn context => fn thy => if Options.bool (#options context) "export_theory" then f context thy else ())); fun export_buffer thy name buffer = if Buffer.is_empty buffer then () - else Export.export thy (Path.binding0 (Path.make ["theory", name])) (Buffer.chunks buffer); + else Export.export thy (Path.binding0 (Path.make ["theory", name])) (XML.blob (Buffer.chunks buffer)); fun export_body thy name body = export_buffer thy name (fold YXML.buffer body Buffer.empty); (* presentation *) val _ = setup_presentation (fn {adjust_pos, ...} => fn thy => let val parents = Theory.parents_of thy; val rep_tsig = Type.rep_tsig (Sign.tsig_of thy); val thy_ctxt = Proof_Context.init_global thy; (* entities *) fun make_entity_markup name xname pos serial = let val props = Position.offset_properties_of (adjust_pos pos) @ Position.id_properties_of pos @ Markup.serial_properties serial; in (Markup.entityN, (Markup.nameN, name) :: (Markup.xnameN, xname) :: props) end; fun entity_markup space name = let val xname = Name_Space.extern_shortest thy_ctxt space name; val {serial, pos, ...} = Name_Space.the_entry space name; in make_entity_markup name xname pos serial end; fun export_entities export_name export get_space decls = let val parent_spaces = map get_space parents; val space = get_space thy; in (decls, []) |-> fold (fn (name, decl) => if exists (fn space => Name_Space.declared space name) parent_spaces then I else (case export name decl of NONE => I | SOME body => cons (#serial (Name_Space.the_entry space name), XML.Elem (entity_markup space name, body)))) |> sort (int_ord o apply2 #1) |> map #2 |> export_body thy export_name end; (* types *) val encode_type = let open XML.Encode Term_XML.Encode in triple encode_syntax (list string) (option typ) end; fun export_type c (Type.LogicalType n) = SOME (encode_type (get_syntax_type thy_ctxt c, Name.invent Name.context Name.aT n, NONE)) | export_type c (Type.Abbreviation (args, U, false)) = SOME (encode_type (get_syntax_type thy_ctxt c, args, SOME U)) | export_type _ _ = NONE; val _ = export_entities "types" export_type Sign.type_space (Name_Space.dest_table (#types rep_tsig)); (* consts *) val consts = Sign.consts_of thy; val encode_term = Term_XML.Encode.term consts; val encode_const = let open XML.Encode Term_XML.Encode in pair encode_syntax (pair (list string) (pair typ (pair (option encode_term) (pair bool (pair (list string) bool))))) end; fun export_const c (T, abbrev) = let val syntax = get_syntax_const thy_ctxt c; val U = Logic.unvarifyT_global T; val U0 = Type.strip_sorts U; val recursion = primrec_types thy_ctxt (c, U); val abbrev' = abbrev |> Option.map (Proofterm.standard_vars_term Name.context #> map_types Type.strip_sorts); val args = map (#1 o dest_TFree) (Consts.typargs consts (c, U0)); val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0); in encode_const (syntax, (args, (U0, (abbrev', (propositional, recursion))))) end; val _ = export_entities "consts" (SOME oo export_const) Sign.const_space (#constants (Consts.dest consts)); (* axioms *) fun standard_prop used extra_shyps raw_prop raw_proof = let val (prop, proof) = Proofterm.standard_vars used (raw_prop, raw_proof); val args = rev (add_frees used prop []); val typargs = rev (add_tfrees used prop []); val used_typargs = fold (Name.declare o #1) typargs used; val sorts = Name.invent used_typargs Name.aT (length extra_shyps) ~~ extra_shyps; in ((sorts @ typargs, args, prop), proof) end; val encode_prop = let open XML.Encode Term_XML.Encode in triple (list (pair string sort)) (list (pair string typ)) encode_term end; fun encode_axiom used prop = encode_prop (#1 (standard_prop used [] prop NONE)); val _ = export_entities "axioms" (K (SOME o encode_axiom Name.context)) Theory.axiom_space (Theory.all_axioms_of thy); (* theorems and proof terms *) val clean_thm = Thm.check_hyps (Context.Theory thy) #> Thm.strip_shyps; val lookup_thm_id = Global_Theory.lookup_thm_id thy; fun proof_boxes thm thm_id = let val selection = {included = Proofterm.this_id (SOME thm_id), excluded = is_some o lookup_thm_id}; val boxes = map (Proofterm.thm_header_id o #1) (Proofterm.proof_boxes selection [Thm.proof_of thm]) handle Proofterm.MIN_PROOF () => Thm_Deps.thm_boxes selection [thm] in boxes @ [thm_id] end; fun expand_name thm_id (header: Proofterm.thm_header) = if #serial header = #serial thm_id then "" else (case lookup_thm_id (Proofterm.thm_header_id header) of NONE => "" | SOME thm_name => Thm_Name.print thm_name); fun entity_markup_thm (serial, (name, i)) = let val space = Facts.space_of (Global_Theory.facts_of thy); val xname = Name_Space.extern_shortest thy_ctxt space name; val {pos, ...} = Name_Space.the_entry space name; in make_entity_markup (Thm_Name.print (name, i)) (Thm_Name.print (xname, i)) pos serial end; fun encode_thm thm_id raw_thm = let val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]); val thm = clean_thm (Thm.unconstrainT raw_thm); val boxes = proof_boxes thm thm_id; val proof0 = if Proofterm.export_standard_enabled () then Thm.standard_proof_of {full = true, expand_name = SOME o expand_name thm_id} thm else if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm else MinProof; val (prop, SOME proof) = standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm) (SOME proof0); val _ = if Proofterm.export_proof_boxes_required thy then Proofterm.export_proof_boxes [proof] else (); in (prop, (deps, (boxes, proof))) |> let open XML.Encode Term_XML.Encode; fun encode_box {serial, theory_name} = pair int string (serial, theory_name); val encode_proof = Proofterm.encode_standard_proof consts; in pair encode_prop (pair (list string) (pair (list encode_box) encode_proof)) end end; fun buffer_export_thm (thm_id, thm_name) = let val markup = entity_markup_thm (#serial thm_id, thm_name); val thm = Global_Theory.get_thm_name thy (thm_name, Position.none); val body = encode_thm thm_id thm; in YXML.buffer (XML.Elem (markup, body)) end; val _ = Buffer.empty |> fold buffer_export_thm (Global_Theory.dest_thm_names thy) |> export_buffer thy "thms"; (* type classes *) val encode_class = let open XML.Encode Term_XML.Encode in pair (list (pair string typ)) (list (encode_axiom Name.context)) end; fun export_class name = (case try (Axclass.get_info thy) name of NONE => ([], []) | SOME {params, axioms, ...} => (params, map (Thm.plain_prop_of o clean_thm) axioms)) |> encode_class |> SOME; val _ = export_entities "classes" (fn name => fn () => export_class name) Sign.class_space (map (rpair ()) (Graph.keys (Sorts.classes_of (#2 (#classes rep_tsig))))); (* sort algebra *) local val prop = encode_axiom Name.context o Logic.varify_global; val encode_classrel = let open XML.Encode in list (pair prop (pair string string)) end; val encode_arities = let open XML.Encode Term_XML.Encode in list (pair prop (triple string (list sort) string)) end; in val export_classrel = maps (fn (c, cs) => map (pair c) cs) #> map (`Logic.mk_classrel) #> encode_classrel; val export_arities = map (`Logic.mk_arity) #> encode_arities; val {classrel, arities} = Sorts.dest_algebra (map (#2 o #classes o Type.rep_tsig o Sign.tsig_of) parents) (#2 (#classes rep_tsig)); end; val _ = if null classrel then () else export_body thy "classrel" (export_classrel classrel); val _ = if null arities then () else export_body thy "arities" (export_arities arities); (* locales *) fun encode_locale used = let open XML.Encode Term_XML.Encode in triple (list (pair string sort)) (list (pair (pair string typ) encode_syntax)) (list (encode_axiom used)) end; fun export_locale loc = let val {typargs, args, axioms} = locale_content thy loc; val used = fold Name.declare (map #1 typargs @ map (#1 o #1) args) Name.context; in encode_locale used (typargs, args, axioms) end handle ERROR msg => cat_error msg ("The error(s) above occurred in locale " ^ quote (Locale.markup_name thy_ctxt loc)); val _ = export_entities "locales" (fn loc => fn () => SOME (export_locale loc)) Locale.locale_space (get_locales thy); (* locale dependencies *) fun encode_locale_dependency (dep: Locale.locale_dependency, subst) = (#source dep, (#target dep, (#prefix dep, subst))) |> let open XML.Encode Term_XML.Encode; val encode_subst = pair (list (pair (pair string sort) typ)) (list (pair (pair string typ) (term consts))); in pair string (pair string (pair (list (pair string bool)) encode_subst)) end; val _ = get_dependencies parents thy |> map_index (fn (i, dep) => let val xname = string_of_int (i + 1); val name = Long_Name.implode [Context.theory_name thy, xname]; val markup = make_entity_markup name xname (#pos (#1 dep)) (#serial (#1 dep)); val body = encode_locale_dependency dep; in XML.Elem (markup, body) end) |> export_body thy "locale_dependencies"; (* constdefs *) val constdefs = Defs.dest_constdefs (map Theory.defs_of (Theory.parents_of thy)) (Theory.defs_of thy) |> sort_by #1; val encode_constdefs = let open XML.Encode in list (pair string string) end; val _ = if null constdefs then () else export_body thy "constdefs" (encode_constdefs constdefs); (* parents *) val _ = Export.export thy \<^path_binding>\theory/parents\ - [YXML.string_of_body (XML.Encode.string (cat_lines (map Context.theory_long_name parents)))]; + (XML.Encode.string (cat_lines (map Context.theory_long_name parents))); in () end); end; diff --git a/src/Pure/Thy/thy_info.ML b/src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML +++ b/src/Pure/Thy/thy_info.ML @@ -1,482 +1,483 @@ (* Title: Pure/Thy/thy_info.ML Author: Markus Wenzel, TU Muenchen Global theory info database, with auto-loading according to theory and file dependencies. *) signature THY_INFO = sig type presentation_context = {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T, segments: Thy_Output.segment list} val apply_presentation: presentation_context -> theory -> unit val add_presentation: (presentation_context -> theory -> unit) -> theory -> theory val get_names: unit -> string list val lookup_theory: string -> theory option val get_theory: string -> theory val master_directory: string -> Path.T val remove_thy: string -> unit type context = {options: Options.T, symbols: HTML.symbols, bibtex_entries: string list, last_timing: Toplevel.transition -> Time.time} val use_theories: context -> string -> Path.T -> (string * Position.T) list -> unit val use_thy: string -> unit val script_thy: Position.T -> string -> theory -> theory val register_thy: theory -> unit val finish: unit -> unit end; structure Thy_Info: THY_INFO = struct (** presentation of consolidated theory **) type presentation_context = {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T, segments: Thy_Output.segment list}; structure Presentation = Theory_Data ( type T = ((presentation_context -> theory -> unit) * stamp) list; val empty = []; val extend = I; fun merge data : T = Library.merge (eq_snd op =) data; ); fun apply_presentation (context: presentation_context) thy = ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy)); fun add_presentation f = Presentation.map (cons (f, stamp ())); val _ = Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy => if exists (Toplevel.is_skipped_proof o #state) segments then () else let val body = Thy_Output.present_thy options thy segments; val option = Present.document_option options; in if #disabled option then () else let val latex = Latex.isabelle_body (Context.theory_name thy) body; val output = [Latex.output_text latex, Latex.output_positions file_pos latex]; val _ = - if Options.bool options "export_document" - then Export.export thy (Path.explode_binding0 "document.tex") output else (); + if Options.bool options "export_document" then + Export.export thy (Path.explode_binding0 "document.tex") (XML.blob output) + else (); val _ = if #enabled option then Present.theory_output thy output else (); in () end end)); (** thy database **) (* messages *) val show_path = space_implode " via " o map quote; fun cycle_msg names = "Cyclic dependency of " ^ show_path names; (* derived graph operations *) fun add_deps name parents G = String_Graph.add_deps_acyclic (name, parents) G handle String_Graph.CYCLES namess => error (cat_lines (map cycle_msg namess)); fun new_entry name parents entry = String_Graph.new_node (name, entry) #> add_deps name parents; (* global thys *) type deps = {master: (Path.T * SHA1.digest), (*master dependencies for thy file*) imports: (string * Position.T) list}; (*source specification of imports (partially qualified)*) fun make_deps master imports : deps = {master = master, imports = imports}; fun master_dir_deps (d: deps option) = the_default Path.current (Option.map (Path.dir o #1 o #master) d); local val global_thys = Synchronized.var "Thy_Info.thys" (String_Graph.empty: (deps option * theory option) String_Graph.T); in fun get_thys () = Synchronized.value global_thys; fun change_thys f = Synchronized.change global_thys f; end; fun get_names () = String_Graph.topological_order (get_thys ()); (* access thy *) fun lookup thys name = try (String_Graph.get_node thys) name; fun lookup_thy name = lookup (get_thys ()) name; fun get thys name = (case lookup thys name of SOME thy => thy | NONE => error ("Theory loader: nothing known about theory " ^ quote name)); fun get_thy name = get (get_thys ()) name; (* access deps *) val lookup_deps = Option.map #1 o lookup_thy; val master_directory = master_dir_deps o #1 o get_thy; (* access theory *) fun lookup_theory name = (case lookup_thy name of SOME (_, SOME theory) => SOME theory | _ => NONE); fun get_theory name = (case lookup_theory name of SOME theory => theory | _ => error ("Theory loader: undefined entry for theory " ^ quote name)); val get_imports = Resources.imports_of o get_theory; (** thy operations **) (* remove *) fun remove name thys = (case lookup thys name of NONE => thys | SOME (NONE, _) => error ("Cannot update finished theory " ^ quote name) | SOME _ => let val succs = String_Graph.all_succs thys [name]; val _ = writeln ("Theory loader: removing " ^ commas_quote succs); in fold String_Graph.del_node succs thys end); val remove_thy = change_thys o remove; (* update *) fun update deps theory thys = let val name = Context.theory_long_name theory; val parents = map Context.theory_long_name (Theory.parents_of theory); val thys' = remove name thys; val _ = map (get thys') parents; in new_entry name parents (SOME deps, SOME theory) thys' end; fun update_thy deps theory = change_thys (update deps theory); (* context *) type context = {options: Options.T, symbols: HTML.symbols, bibtex_entries: string list, last_timing: Toplevel.transition -> Time.time}; fun default_context (): context = {options = Options.default (), symbols = HTML.no_symbols, bibtex_entries = [], last_timing = K Time.zeroTime}; (* scheduling loader tasks *) datatype result = Result of {theory: theory, exec_id: Document_ID.exec, present: unit -> unit, commit: unit -> unit, weight: int}; fun theory_result theory = Result {theory = theory, exec_id = Document_ID.none, present = I, commit = I, weight = 0}; fun result_theory (Result {theory, ...}) = theory; fun result_present (Result {present, ...}) = present; fun result_commit (Result {commit, ...}) = commit; fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i); fun join_theory (Result {theory, exec_id, ...}) = let val _ = Execution.join [exec_id]; val res = Exn.capture Thm.consolidate_theory theory; val exns = maps Task_Queue.group_status (Execution.peek exec_id); in res :: map Exn.Exn exns end; datatype task = Task of string list * (theory list -> result) | Finished of theory; fun task_finished (Task _) = false | task_finished (Finished _) = true; fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents; val schedule_seq = String_Graph.schedule (fn deps => fn (_, task) => (case task of Task (parents, body) => let val result = body (task_parents deps parents); val _ = Par_Exn.release_all (join_theory result); val _ = result_present result (); val _ = result_commit result (); in result_theory result end | Finished thy => thy)) #> ignore; val schedule_futures = Thread_Attributes.uninterruptible (fn _ => fn tasks => let val futures = tasks |> String_Graph.schedule (fn deps => fn (name, task) => (case task of Task (parents, body) => (singleton o Future.forks) {name = "theory:" ^ name, group = NONE, deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true} (fn () => (case filter (not o can Future.join o #2) deps of [] => body (map (result_theory o Future.join) (task_parents deps parents)) | bad => error ("Failed to load theory " ^ quote name ^ " (unresolved " ^ commas_quote (map #1 bad) ^ ")"))) | Finished theory => Future.value (theory_result theory))); val results1 = futures |> maps (fn future => (case Future.join_result future of Exn.Res result => join_theory result | Exn.Exn exn => [Exn.Exn exn])); val results2 = futures |> map_filter (Exn.get_res o Future.join_result) |> sort result_ord |> Par_List.map (fn result => Exn.capture (result_present result) ()); (* FIXME more precise commit order (!?) *) val results3 = futures |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ()); (* FIXME avoid global Execution.reset (!??) *) val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ())); val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4); in () end); (* eval theory *) fun excursion keywords master_dir last_timing init elements = let fun prepare_span st span = Command_Span.content span |> Command.read keywords (Command.read_thy st) master_dir init ([], ~1) |> (fn tr => Toplevel.timing (last_timing tr) tr); fun element_result span_elem (st, _) = let val elem = Thy_Element.map_element (prepare_span st) span_elem; val (results, st') = Toplevel.element_result keywords elem st; val pos' = Toplevel.pos_of (Thy_Element.last_element elem); in (results, (st', pos')) end; val (results, (end_state, end_pos)) = fold_map element_result elements (Toplevel.init_toplevel (), Position.none); val thy = Toplevel.end_theory end_pos end_state; in (results, thy) end; fun eval_thy (context: context) update_time master_dir header text_pos text parents = let val {options, symbols, bibtex_entries, last_timing} = context; val (name, _) = #name header; val keywords = fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents (Keyword.add_keywords (#keywords header) Keyword.empty_keywords); val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text); val elements = Thy_Element.parse_elements keywords spans; fun init () = Resources.begin_theory master_dir header parents |> Present.begin_theory bibtex_entries update_time (fn () => implode (map (HTML.present_span symbols keywords) spans)); val (results, thy) = cond_timeit true ("theory " ^ quote name) (fn () => excursion keywords master_dir last_timing init elements); fun present () = let val segments = (spans ~~ maps Toplevel.join_results results) |> map (fn (span, (tr, st')) => {span = span, command = tr, state = st'}); val context: presentation_context = {options = options, file_pos = text_pos, adjust_pos = I, segments = segments}; in apply_presentation context thy end; in (thy, present, size text) end; (* require_thy -- checking database entries wrt. the file-system *) local fun required_by _ [] = "" | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")"; fun load_thy context initiators update_time deps text (name, pos) keywords parents = let val _ = remove_thy name; val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators); val _ = Output.try_protocol_message (Markup.loading_theory name) []; val {master = (thy_path, _), imports} = deps; val dir = Path.dir thy_path; val header = Thy_Header.make (name, pos) imports keywords; val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents); val exec_id = Document_ID.make (); val _ = Execution.running Document_ID.none exec_id [] orelse raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id); val timing_start = Timing.start (); val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path); val (theory, present, weight) = eval_thy context update_time dir header text_pos text (if name = Context.PureN then [Context.the_global_context ()] else parents); val timing_result = Timing.result timing_start; val timing_props = [Markup.theory_timing, (Markup.nameN, name)]; val _ = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) [] fun commit () = update_thy deps theory; in Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight} end; fun check_thy_deps dir name = (case lookup_deps name of SOME NONE => (true, NONE, Position.none, get_imports name, []) | NONE => let val {master, text, theory_pos, imports, keywords} = Resources.check_thy dir name in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end | SOME (SOME {master, ...}) => let val {master = master', text = text', theory_pos = theory_pos', imports = imports', keywords = keywords'} = Resources.check_thy dir name; val deps' = SOME (make_deps master' imports', text'); val current = #2 master = #2 master' andalso (case lookup_theory name of NONE => false | SOME theory => Resources.loaded_files_current theory); in (current, deps', theory_pos', imports', keywords') end); in fun require_thys context initiators qualifier dir strs tasks = fold_map (require_thy context initiators qualifier dir) strs tasks |>> forall I and require_thy context initiators qualifier dir (s, require_pos) tasks = let val {master_dir, theory_name, ...} = Resources.import_name qualifier dir s; in (case try (String_Graph.get_node tasks) theory_name of SOME task => (task_finished task, tasks) | NONE => let val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators); val (current, deps, theory_pos, imports, keywords) = check_thy_deps master_dir theory_name handle ERROR msg => cat_error msg ("The error(s) above occurred for theory " ^ quote theory_name ^ Position.here require_pos ^ required_by "\n" initiators); val qualifier' = Resources.theory_qualifier theory_name; val dir' = Path.append dir (master_dir_deps (Option.map #1 deps)); val parents = map (#theory_name o Resources.import_name qualifier' dir' o #1) imports; val (parents_current, tasks') = require_thys context (theory_name :: initiators) qualifier' dir' imports tasks; val all_current = current andalso parents_current; val task = if all_current then Finished (get_theory theory_name) else (case deps of NONE => raise Fail "Malformed deps" | SOME (dep, text) => let val update_time = serial (); val load = load_thy context initiators update_time dep text (theory_name, theory_pos) keywords; in Task (parents, load) end); val tasks'' = new_entry theory_name parents task tasks'; in (all_current, tasks'') end) end; end; (* use theories *) fun use_theories context qualifier master_dir imports = let val (_, tasks) = require_thys context [] qualifier master_dir imports String_Graph.empty in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end; fun use_thy name = use_theories (default_context ()) Resources.default_qualifier Path.current [(name, Position.none)]; (* toplevel scripting -- without maintaining database *) fun script_thy pos txt thy = let val trs = Outer_Syntax.parse_text thy (K thy) pos txt; val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs); val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init_toplevel ()); in Toplevel.end_theory end_pos end_state end; (* register theory *) fun register_thy theory = let val name = Context.theory_long_name theory; val {master, ...} = Resources.check_thy (Resources.master_directory theory) name; val imports = Resources.imports_of theory; in change_thys (fn thys => let val thys' = remove name thys; val _ = writeln ("Registering theory " ^ quote name); in update (make_deps master imports) theory thys' end) end; (* finish all theories *) fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry))); end; fun use_thy name = Runtime.toplevel_program (fn () => Thy_Info.use_thy name); diff --git a/src/Pure/Tools/build.ML b/src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML +++ b/src/Pure/Tools/build.ML @@ -1,249 +1,250 @@ (* Title: Pure/Tools/build.ML Author: Makarius Build Isabelle sessions. *) signature BUILD = sig val build: string -> unit end; structure Build: BUILD = 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 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 timing *) fun session_timing name verbose f x = let val start = Timing.start (); val y = f x; val timing = Timing.result start; val threads = string_of_int (Multithreading.max_threads ()); val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing) |> Real.fmt (StringCvt.FIX (SOME 2)); val timing_props = [("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)]; val _ = writeln ("\fTiming = " ^ YXML.string_of_body (XML.Encode.properties timing_props)); val _ = if verbose then Output.physical_stderr ("Timing " ^ name ^ " (" ^ threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n") else (); in y end; (* protocol messages *) fun protocol_message props output = (case props of function :: args => if function = Markup.ML_statistics orelse function = Markup.task_statistics then Protocol_Message.inline (#2 function) args else if function = Markup.command_timing then let val name = the_default "" (Properties.get args Markup.nameN); val pos = Position.of_properties args; val {elapsed, ...} = Markup.parse_timing_properties args; val is_significant = Timing.is_relevant_time elapsed andalso elapsed >= Options.default_seconds "command_timing_threshold"; in if is_significant then (case approximative_id name pos of SOME id => Protocol_Message.inline (#2 function) (Markup.command_timing_properties id elapsed) | NONE => ()) else () end else if function = Markup.theory_timing then Protocol_Message.inline (#2 function) args else (case Markup.dest_loading_theory props of SOME name => writeln ("\floading_theory = " ^ name) | NONE => Export.protocol_message props output) | [] => raise Output.Protocol_Message props); (* build theories *) fun build_theories symbols bibtex_entries last_timing qualifier master_dir (options, thys) = let val context = {options = options, symbols = symbols, bibtex_entries = bibtex_entries, last_timing = last_timing}; val condition = space_explode "," (Options.string options "condition"); val conds = filter_out (can getenv_strict) condition; in if null conds then (Options.set_default options; Isabelle_Process.init_options (); Future.fork I; (Thy_Info.use_theories context qualifier master_dir |> (case Options.string options "profiling" of "" => I | "time" => profile_time | "allocations" => profile_allocations | bad => error ("Bad profiling option: " ^ quote bad)) |> Unsynchronized.setmp print_mode (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys) else Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^ " (undefined " ^ commas conds ^ ")\n") end; (* build session *) datatype args = Args of {symbol_codes: (string * int) list, command_timings: Properties.T list, do_output: bool, verbose: bool, browser_info: Path.T, document_files: (Path.T * Path.T) list, graph_file: Path.T, parent_name: string, chapter: string, name: string, master_dir: Path.T, theories: (Options.T * (string * Position.T) list) list, session_positions: (string * Properties.T) list, session_directories: (string * string) list, doc_names: string list, global_theories: (string * string) list, loaded_theories: string list, bibtex_entries: string list}; fun decode_args yxml = let open XML.Decode; val position = Position.of_properties o properties; val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info, (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir, (theories, (session_positions, (session_directories, (doc_names, (global_theories, (loaded_theories, bibtex_entries))))))))))))))))) = pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string (pair (list (pair string string)) (pair string (pair string (pair string (pair string (pair string (pair (((list (pair Options.decode (list (pair string position)))))) (pair (list (pair string properties)) (pair (list (pair string string)) (pair (list string) (pair (list (pair string string)) (pair (list string) (list string))))))))))))))))) (YXML.parse_body yxml); in Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output, verbose = verbose, browser_info = Path.explode browser_info, document_files = map (apply2 Path.explode) document_files, graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter, name = name, master_dir = Path.explode master_dir, theories = theories, session_positions = session_positions, session_directories = session_directories, doc_names = doc_names, global_theories = global_theories, loaded_theories = loaded_theories, bibtex_entries = bibtex_entries} end; fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info, document_files, graph_file, parent_name, chapter, name, master_dir, theories, session_positions, session_directories, doc_names, global_theories, loaded_theories, bibtex_entries}) = let val symbols = HTML.make_symbols symbol_codes; val _ = Resources.init_session_base {session_positions = session_positions, session_directories = session_directories, docs = doc_names, global_theories = global_theories, loaded_theories = loaded_theories}; val _ = Session.init symbols do_output (Options.default_bool "browser_info") browser_info (Options.default_string "document") (Options.default_string "document_output") (Present.document_variants (Options.default ())) document_files graph_file parent_name (chapter, name) verbose; val last_timing = get_timings (fold update_timings command_timings empty_timings); val res1 = theories |> (List.app (build_theories symbols bibtex_entries last_timing name master_dir) |> session_timing name verbose |> Exn.capture); val res2 = Exn.capture Session.finish (); val _ = Resources.finish_session_base (); val _ = Par_Exn.release_all [res1, res2]; in () end; (*command-line tool*) fun build args_file = let val _ = SHA1.test_samples (); val _ = Options.load_default (); val _ = Isabelle_Process.init_options (); val args = decode_args (File.read (Path.explode args_file)); fun error_message msg = writeln ("\ferror_message = " ^ encode_lines (YXML.content_of msg)); val _ = Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message build_session args handle exn => (List.app error_message (Runtime.exn_message_list exn); Exn.reraise exn); val _ = Private_Output.protocol_message_fn := Output.protocol_message_undefined; val _ = Options.reset_default (); in () end; (*PIDE version*) val _ = Isabelle_Process.protocol_command "build_session" (fn [args_yxml] => - let - val args = decode_args args_yxml; - val result = (build_session args; "") handle exn => - (Runtime.exn_message exn handle _ (*sic!*) => - "Exception raised, but failed to print details!"); - in Output.protocol_message Markup.build_session_finished [result] end | _ => raise Match); + let + val args = decode_args args_yxml; + val result = (build_session args; "") handle exn => + (Runtime.exn_message exn handle _ (*sic!*) => + "Exception raised, but failed to print details!"); + in Output.protocol_message Markup.build_session_finished [XML.Text result] end + | _ => raise Match); end; diff --git a/src/Pure/Tools/debugger.ML b/src/Pure/Tools/debugger.ML --- a/src/Pure/Tools/debugger.ML +++ b/src/Pure/Tools/debugger.ML @@ -1,296 +1,295 @@ (* Title: Pure/Tools/debugger.ML Author: Makarius Interactive debugger for Isabelle/ML. *) signature DEBUGGER = sig val writeln_message: string -> unit val warning_message: string -> unit val error_message: string -> unit end; structure Debugger: DEBUGGER = struct (** global state **) (* output messages *) fun output_message kind msg = if msg = "" then () else Output.protocol_message (Markup.debugger_output (Standard_Thread.the_name ())) - [Markup.markup (kind, Markup.serial_properties (serial ())) msg]; + [XML.Text (Markup.markup (kind, Markup.serial_properties (serial ())) msg)]; val writeln_message = output_message Markup.writelnN; val warning_message = output_message Markup.warningN; val error_message = output_message Markup.errorN; fun error_wrapper e = e () handle exn => if Exn.is_interrupt exn then Exn.reraise exn else error_message (Runtime.exn_message exn); (* thread input *) val thread_input = Synchronized.var "Debugger.state" (NONE: string list Queue.T Symtab.table option); fun init_input () = Synchronized.change thread_input (K (SOME Symtab.empty)); fun exit_input () = Synchronized.change thread_input (K NONE); fun input thread_name msg = if null msg then error "Empty input" else Synchronized.change thread_input (Option.map (Symtab.map_default (thread_name, Queue.empty) (Queue.enqueue msg))); fun get_input thread_name = Synchronized.guarded_access thread_input (fn NONE => SOME ([], NONE) | SOME input => (case Symtab.lookup input thread_name of NONE => NONE | SOME queue => let val (msg, queue') = Queue.dequeue queue; val input' = if Queue.is_empty queue' then Symtab.delete_safe thread_name input else Symtab.update (thread_name, queue') input; in SOME (msg, SOME input') end)); (* global break *) local val break = Synchronized.var "Debugger.break" false; in fun is_break () = Synchronized.value break; fun set_break b = Synchronized.change break (K b); end; (** thread state **) (* stack frame during debugging *) val debugging_var = Thread_Data.var () : PolyML.DebuggerInterface.debugState list Thread_Data.var; fun get_debugging () = the_default [] (Thread_Data.get debugging_var); val is_debugging = not o null o get_debugging; fun with_debugging e = Thread_Data.setmp debugging_var (SOME (PolyML.DebuggerInterface.debugState (Thread.self ()))) e (); fun the_debug_state thread_name index = (case get_debugging () of [] => error ("Missing debugger information for thread " ^ quote thread_name) | states => if index < 0 orelse index >= length states then error ("Bad debugger stack index " ^ signed_string_of_int index ^ " for thread " ^ quote thread_name) else nth states index); (* flags for single-stepping *) datatype stepping = Stepping of bool * int; (*stepping enabled, stack depth limit*) val stepping_var = Thread_Data.var () : stepping Thread_Data.var; fun get_stepping () = the_default (Stepping (false, ~1)) (Thread_Data.get stepping_var); fun put_stepping stepping = Thread_Data.put stepping_var (SOME (Stepping stepping)); fun is_stepping () = let val stack = PolyML.DebuggerInterface.debugState (Thread.self ()); val Stepping (stepping, depth) = get_stepping (); in stepping andalso (depth < 0 orelse length stack <= depth) end; fun continue () = put_stepping (false, ~1); fun step () = put_stepping (true, ~1); fun step_over () = put_stepping (true, length (get_debugging ())); fun step_out () = put_stepping (true, length (get_debugging ()) - 1); (** eval ML **) local val context_attempts = map ML_Lex.read ["Context.put_generic_context (SOME (Context.Theory ML_context))", "Context.put_generic_context (SOME (Context.Proof ML_context))", "Context.put_generic_context (SOME ML_context)"]; fun environment SML = if SML then ML_Env.SML else ML_Env.Isabelle; fun operations SML = if SML then ML_Env.SML_operations else ML_Env.Isabelle_operations; fun evaluate {SML, verbose} = ML_Context.eval {environment = environment SML, redirect = false, verbose = verbose, debug = SOME false, writeln = writeln_message, warning = warning_message} Position.none; fun eval_setup thread_name index SML context = context |> Context_Position.set_visible_generic false |> ML_Env.add_name_space (environment SML) (PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index)); fun eval_context thread_name index SML toks = let val context = Context.the_generic_context (); val context1 = if SML orelse forall (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks then context else let val context' = context |> eval_setup thread_name index SML |> ML_Context.exec (fn () => evaluate {SML = SML, verbose = true} (ML_Lex.read "val ML_context = " @ toks)); fun try_exec toks = try (ML_Context.exec (fn () => evaluate {SML = false, verbose = false} toks)) context'; in (case get_first try_exec context_attempts of SOME context2 => context2 | NONE => error "Malformed context: expected type theory, Proof.context, Context.generic") end; in context1 |> eval_setup thread_name index SML end; in fun eval thread_name index SML txt1 txt2 = let val (toks1, toks2) = apply2 (#read_source (operations SML) o Input.string) (txt1, txt2); val context = eval_context thread_name index SML toks1; in Context.setmp_generic_context (SOME context) (evaluate {SML = SML, verbose = true}) toks2 end; fun print_vals thread_name index SML txt = let val toks = #read_source (operations SML) (Input.string txt) val context = eval_context thread_name index SML toks; val space = PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index); fun print x = Pretty.from_polyml (PolyML.NameSpace.Values.printWithType (x, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()), SOME space)); fun print_all () = #allVal (PolyML.DebuggerInterface.debugLocalNameSpace (the_debug_state thread_name index)) () |> sort_by #1 |> map (Pretty.item o single o print o #2) |> Pretty.chunks |> Pretty.string_of |> writeln_message; in Context.setmp_generic_context (SOME context) print_all () end; end; (** debugger loop **) local fun debugger_state thread_name = Output.protocol_message (Markup.debugger_state thread_name) - [get_debugging () + (get_debugging () |> map (fn st => (Position.properties_of (Exn_Properties.position_of_polyml_location (PolyML.DebuggerInterface.debugLocation st)), PolyML.DebuggerInterface.debugFunction st)) - |> let open XML.Encode in list (pair properties string) end - |> YXML.string_of_body]; + |> let open XML.Encode in list (pair properties string) end); fun debugger_command thread_name = (case get_input thread_name of [] => (continue (); false) | ["continue"] => (continue (); false) | ["step"] => (step (); false) | ["step_over"] => (step_over (); false) | ["step_out"] => (step_out (); false) | ["eval", index, SML, txt1, txt2] => (error_wrapper (fn () => eval thread_name (Value.parse_int index) (Value.parse_bool SML) txt1 txt2); true) | ["print_vals", index, SML, txt] => (error_wrapper (fn () => print_vals thread_name (Value.parse_int index) (Value.parse_bool SML) txt); true) | bad => (Output.system_message ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); true)); in fun debugger_loop thread_name = Thread_Attributes.uninterruptible (fn restore_attributes => fn () => let fun loop () = (debugger_state thread_name; if debugger_command thread_name then loop () else ()); val result = Exn.capture (restore_attributes with_debugging) loop; val _ = debugger_state thread_name; in Exn.release result end) (); end; (** protocol commands **) val _ = Isabelle_Process.protocol_command "Debugger.init" (fn [] => (init_input (); PolyML.DebuggerInterface.setOnBreakPoint (SOME (fn (_, break) => if not (is_debugging ()) andalso (! break orelse is_break () orelse is_stepping ()) then (case Standard_Thread.get_name () of SOME thread_name => debugger_loop thread_name | NONE => ()) else ())))); val _ = Isabelle_Process.protocol_command "Debugger.exit" (fn [] => (PolyML.DebuggerInterface.setOnBreakPoint NONE; exit_input ())); val _ = Isabelle_Process.protocol_command "Debugger.break" (fn [b] => set_break (Value.parse_bool b)); val _ = Isabelle_Process.protocol_command "Debugger.breakpoint" (fn [node_name, id0, breakpoint0, breakpoint_state0] => let val id = Value.parse_int id0; val breakpoint = Value.parse_int breakpoint0; val breakpoint_state = Value.parse_bool breakpoint_state0; fun err () = error ("Bad exec for command " ^ Value.print_int id); in (case Document.command_exec (Document.state ()) node_name id of SOME (eval, _) => if Command.eval_finished eval then let val st = Command.eval_result_state eval; val ctxt = Toplevel.presentation_context st; in (case ML_Env.get_breakpoint (Context.Proof ctxt) breakpoint of SOME (b, _) => b := breakpoint_state | NONE => err ()) end else err () | NONE => err ()) end); val _ = Isabelle_Process.protocol_command "Debugger.input" (fn thread_name :: msg => input thread_name msg); end; diff --git a/src/Pure/Tools/generated_files.ML b/src/Pure/Tools/generated_files.ML --- a/src/Pure/Tools/generated_files.ML +++ b/src/Pure/Tools/generated_files.ML @@ -1,377 +1,377 @@ (* Title: Pure/Tools/generated_files.ML Author: Makarius Generated source files for other languages: with antiquotations, without Isabelle symbols. *) signature GENERATED_FILES = sig val add_files: Path.binding * string -> theory -> theory type file = {path: Path.T, pos: Position.T, content: string} val file_binding: file -> Path.binding val file_markup: file -> Markup.T val print_file: file -> string val report_file: Proof.context -> Position.T -> file -> unit val get_files: theory -> file list val get_file: theory -> Path.binding -> file val get_files_in: Path.binding list * theory -> (file * Position.T) list val check_files_in: Proof.context -> (string * Position.T) list * (string * Position.T) option -> Path.binding list * theory val write_file: Path.T -> file -> unit val export_file: theory -> file -> unit type file_type = {name: string, ext: string, make_comment: string -> string, make_string: string -> string} val file_type: binding -> {ext: string, make_comment: string -> string, make_string: string -> string} -> theory -> theory val antiquotation: binding -> 'a Token.context_parser -> ({context: Proof.context, source: Token.src, file_type: file_type, argument: 'a} -> string) -> theory -> theory val set_string: string -> Proof.context -> Proof.context val generate_file: Path.binding * Input.source -> Proof.context -> local_theory val generate_file_cmd: (string * Position.T) * Input.source -> local_theory -> local_theory val export_generated_files: Proof.context -> (Path.binding list * theory) list -> unit val export_generated_files_cmd: Proof.context -> ((string * Position.T) list * (string * Position.T) option) list -> unit val with_compile_dir: (Path.T -> unit) -> unit val compile_generated_files: Proof.context -> (Path.binding list * theory) list -> (Path.T list * Path.T) list -> (Path.binding list * bool option) list -> Path.binding -> Input.source -> unit val compile_generated_files_cmd: Proof.context -> ((string * Position.T) list * (string * Position.T) option) list -> ((string * Position.T) list * (string * Position.T)) list -> ((string * Position.T) list * bool option) list -> string * Position.T -> Input.source -> unit val execute: Path.T -> Input.source -> string -> string end; structure Generated_Files: GENERATED_FILES = struct (** context data **) type file_type = {name: string, ext: string, make_comment: string -> string, make_string: string -> string}; type antiquotation = Token.src -> Proof.context -> file_type -> string; structure Data = Theory_Data ( type T = (Path.T * (Position.T * string)) list * (*files for current theory*) file_type Name_Space.table * (*file types*) antiquotation Name_Space.table; (*antiquotations*) val empty = ([], Name_Space.empty_table Markup.file_typeN, Name_Space.empty_table Markup.antiquotationN); val extend = @{apply 3(1)} (K []); fun merge ((_, types1, antiqs1), (_, types2, antiqs2)) = ([], Name_Space.merge_tables (types1, types2), Name_Space.merge_tables (antiqs1, antiqs2)); ); fun add_files (binding, content) = let val _ = Path.proper_binding binding; val (path, pos) = Path.dest_binding binding; in (Data.map o @{apply 3(1)}) (fn files => (case AList.lookup (op =) files path of SOME (pos', _) => error ("Duplicate generated file: " ^ Path.print path ^ Position.here_list [pos, pos']) | NONE => (path, (pos, content)) :: files)) end; (* get files *) type file = {path: Path.T, pos: Position.T, content: string}; fun file_binding (file: file) = Path.binding (#path file, #pos file); fun file_markup (file: file) = (Markup.entityN, Position.def_properties_of (#pos file)); fun print_file (file: file) = Markup.markup (file_markup file) (quote (Path.implode (#path file))); fun report_file ctxt pos file = Context_Position.report ctxt pos (file_markup file); fun get_files thy = Data.get thy |> #1 |> rev |> map (fn (path, (pos, content)) => {path = path, pos = pos, content = content}: file); fun get_file thy binding = let val (path, pos) = Path.dest_binding binding in (case find_first (fn file => #path file = path) (get_files thy) of SOME file => file | NONE => error ("Missing generated file " ^ Path.print path ^ " in theory " ^ quote (Context.theory_long_name thy) ^ Position.here pos)) end; fun get_files_in ([], thy) = map (rpair Position.none) (get_files thy) | get_files_in (files, thy) = map (fn binding => (get_file thy binding, Path.pos_of_binding binding)) files; (* check and output files *) fun check_files_in ctxt (files, opt_thy) = let val thy = (case opt_thy of SOME name => Theory.check {long = false} ctxt name | NONE => Proof_Context.theory_of ctxt); in (map Path.explode_binding files, thy) end; fun write_file dir (file: file) = let val path = Path.expand (Path.append dir (#path file)); val _ = Isabelle_System.mkdirs (Path.dir path); val _ = File.generate path (#content file); in () end; fun export_file thy (file: file) = - Export.export thy (file_binding file) [#content file]; + Export.export thy (file_binding file) [XML.Text (#content file)]; (* file types *) fun get_file_type thy ext = if ext = "" then error "Bad file extension" else (#2 (Data.get thy), NONE) |-> Name_Space.fold_table (fn (_, file_type) => fn res => if #ext file_type = ext then SOME file_type else res) |> (fn SOME file_type => file_type | NONE => error ("Unknown file type for extension " ^ quote ext)); fun file_type binding {ext, make_comment, make_string} thy = let val name = Binding.name_of binding; val pos = Binding.pos_of binding; val file_type = {name = name, ext = ext, make_comment = make_comment, make_string = make_string}; val table = #2 (Data.get thy); val space = Name_Space.space_of_table table; val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.global_naming); val (_, data') = table |> Name_Space.define context true (Binding.make (name, pos), file_type); val _ = (case try (#name o get_file_type thy) ext of NONE => () | SOME name' => error ("Extension " ^ quote ext ^ " already registered for file type " ^ quote (Markup.markup (Name_Space.markup space name') name') ^ Position.here pos)); in thy |> (Data.map o @{apply 3(2)}) (K data') end; (* antiquotations *) val get_antiquotations = #3 o Data.get o Proof_Context.theory_of; fun antiquotation name scan body thy = let fun ant src ctxt file_type : string = let val (x, ctxt') = Token.syntax scan src ctxt in body {context = ctxt', source = src, file_type = file_type, argument = x} end; in thy |> (Data.map o @{apply 3(3)}) (Name_Space.define (Context.Theory thy) true (name, ant) #> #2) end; val scan_antiq = Antiquote.scan_control >> Antiquote.Control || Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (Antiquote.Text o Symbol_Pos.symbol); fun read_source ctxt (file_type: file_type) source = let val _ = Context_Position.report ctxt (Input.pos_of source) (Markup.language {name = #name file_type, symbols = false, antiquotes = true, delimited = Input.is_delimited source}); val (input, _) = Input.source_explode source |> Scan.error (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_antiq)); val _ = Context_Position.reports ctxt (Antiquote.antiq_reports input); fun expand antiq = (case antiq of Antiquote.Text s => s | Antiquote.Control {name, body, ...} => let val src = Token.make_src name (if null body then [] else [Token.read_cartouche body]); val (src', ant) = Token.check_src ctxt get_antiquotations src; in ant src' ctxt file_type end | Antiquote.Antiq antiq => error ("Bad antiquotation " ^ Position.here (#1 (#range antiq)))); in implode (map expand input) end; (** Isar commands **) (* generate_file *) fun generate_file (binding, source) lthy = let val thy = Proof_Context.theory_of lthy; val (path, pos) = Path.dest_binding binding; val file_type = get_file_type thy (#2 (Path.split_ext path)) handle ERROR msg => error (msg ^ Position.here pos); val header = #make_comment file_type " generated by Isabelle "; val content = header ^ "\n" ^ read_source lthy file_type source; in lthy |> (Local_Theory.background_theory o add_files) (binding, content) end; fun generate_file_cmd (file, source) lthy = generate_file (Path.explode_binding file, source) lthy; (* export_generated_files *) fun export_generated_files ctxt args = let val thy = Proof_Context.theory_of ctxt in (case map #1 (maps get_files_in args) of [] => () | files => (List.app (export_file thy) files; writeln (Export.message thy Path.current); writeln (cat_lines (map (prefix " " o print_file) files)))) end; fun export_generated_files_cmd ctxt args = export_generated_files ctxt (map (check_files_in ctxt) args); (* compile_generated_files *) val compile_dir = Config.declare_string ("compile_dir", \<^here>) (K ""); fun with_compile_dir body : unit = body (Path.explode (Config.get (Context.the_local_context ()) compile_dir)); fun compile_generated_files ctxt args external export export_prefix source = Isabelle_System.with_tmp_dir "compile" (fn dir => let val thy = Proof_Context.theory_of ctxt; val files = maps get_files_in args; val _ = List.app (fn (file, pos) => report_file ctxt pos file) files; val _ = List.app (write_file dir o #1) files; val _ = external |> List.app (fn (files, base_dir) => files |> List.app (fn file => Isabelle_System.copy_file_base (base_dir, file) dir)); val _ = ML_Context.eval_in (SOME (Config.put compile_dir (Path.implode dir) ctxt)) ML_Compiler.flags (Input.pos_of source) (ML_Lex.read "Generated_Files.with_compile_dir (" @ ML_Lex.read_source source @ ML_Lex.read ")"); val _ = export |> List.app (fn (bindings, executable) => bindings |> List.app (fn binding0 => let val binding = binding0 |> Path.map_binding (executable = SOME true ? Path.exe); val (path, pos) = Path.dest_binding binding; val content = (case try File.read (Path.append dir path) of SOME context => context | NONE => error ("Missing result file " ^ Path.print path ^ Position.here pos)); val _ = Export.report_export thy export_prefix; val binding' = Path.map_binding (Path.append (Path.path_of_binding export_prefix)) binding; in (if is_some executable then Export.export_executable else Export.export) - thy binding' [content] + thy binding' [XML.Text content] end)); val _ = if null export then () else writeln (Export.message thy (Path.path_of_binding export_prefix)); in () end); fun compile_generated_files_cmd ctxt args external export export_prefix source = compile_generated_files ctxt (map (check_files_in ctxt) args) (external |> map (fn (raw_files, raw_base_dir) => let val base_dir = Resources.check_dir ctxt NONE raw_base_dir; fun check (s, pos) = (Resources.check_file ctxt (SOME base_dir) (s, pos); Path.explode s); val files = map check raw_files; in (files, base_dir) end)) ((map o apfst o map) Path.explode_binding export) (Path.explode_binding export_prefix) source; (* execute compiler -- auxiliary *) fun execute dir title compile = Isabelle_System.bash_output_check ("cd " ^ File.bash_path dir ^ " && " ^ compile) handle ERROR msg => let val (s, pos) = Input.source_content title in error (s ^ " failed" ^ Position.here pos ^ ":\n" ^ msg) end; (** concrete file types **) val _ = Theory.setup (file_type \<^binding>\Haskell\ {ext = "hs", make_comment = enclose "{-" "-}", make_string = GHC.print_string}); (** concrete antiquotations **) (* ML expression as string literal *) structure Local_Data = Proof_Data ( type T = string option; fun init _ = NONE; ); val set_string = Local_Data.put o SOME; fun the_string ctxt = (case Local_Data.get ctxt of SOME s => s | NONE => raise Fail "No result string"); val _ = Theory.setup (antiquotation \<^binding>\cartouche\ (Scan.lift Args.cartouche_input) (fn {context = ctxt, file_type, argument, ...} => ctxt |> Context.proof_map (ML_Context.expression (Input.pos_of argument) (ML_Lex.read "Theory.local_setup (Generated_Files.set_string (" @ ML_Lex.read_source argument @ ML_Lex.read "))")) |> the_string |> #make_string file_type)); (* file-system paths *) fun path_antiquotation binding check = antiquotation binding (Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) => (check ctxt (SOME Path.current) (name, pos) |> Path.implode))) (fn {file_type, argument, ...} => #make_string file_type argument); val _ = Theory.setup (path_antiquotation \<^binding>\path\ Resources.check_path #> path_antiquotation \<^binding>\file\ Resources.check_file #> path_antiquotation \<^binding>\dir\ Resources.check_dir); end; diff --git a/src/Pure/Tools/print_operation.ML b/src/Pure/Tools/print_operation.ML --- a/src/Pure/Tools/print_operation.ML +++ b/src/Pure/Tools/print_operation.ML @@ -1,79 +1,75 @@ (* Title: Pure/Tools/print_operation.ML Author: Makarius Print operations as asynchronous query. *) signature PRINT_OPERATION = sig val register: string -> string -> (Toplevel.state -> Pretty.T list) -> unit end; structure Print_Operation: PRINT_OPERATION = struct (* maintain print operations *) local val print_operations = Synchronized.var "print_operations" ([]: (string * (string * (Toplevel.state -> Pretty.T list))) list); fun report () = Output.try_protocol_message Markup.print_operations - let - val yxml = - Synchronized.value print_operations - |> map (fn (x, (y, _)) => (x, y)) |> rev - |> let open XML.Encode in list (pair string string) end - |> YXML.string_of_body; - in [yxml] end; + (Synchronized.value print_operations + |> map (fn (x, (y, _)) => (x, y)) |> rev + |> let open XML.Encode in list (pair string string) end); val _ = Isabelle_Process.protocol_command "print_operations" (fn [] => report ()); val _ = Session.protocol_handler "isabelle.Print_Operation$Handler"; in fun register name description pr = (Synchronized.change print_operations (fn tab => (if not (AList.defined (op =) tab name) then () else warning ("Redefining print operation: " ^ quote name); AList.update (op =) (name, (description, pr)) tab)); report ()); val _ = Query_Operation.register {name = "print_operation", pri = Task_Queue.urgent_pri} (fn {state, args, writeln_result, ...} => let val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context"; fun err s = Pretty.mark_str (Markup.bad (), s); fun print name = (case AList.lookup (op =) (Synchronized.value print_operations) name of SOME (_, pr) => (pr state handle Toplevel.UNDEF => [err "Unknown context"]) | NONE => [err ("Unknown print operation: " ^ quote name)]); in writeln_result (Pretty.string_of (Pretty.chunks (maps print args))) end); end; (* common print operations *) val _ = register "context" "context of local theory target" Toplevel.pretty_context; val _ = register "cases" "cases of proof context" (Proof_Context.pretty_cases o Toplevel.context_of); val _ = register "terms" "term bindings of proof context" (Proof_Context.pretty_term_bindings o Toplevel.context_of); val _ = register "theorems" "theorems of local theory or proof context" (Isar_Cmd.pretty_theorems false); end; diff --git a/src/Pure/proofterm.ML b/src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML +++ b/src/Pure/proofterm.ML @@ -1,2318 +1,2318 @@ (* Title: Pure/proofterm.ML Author: Stefan Berghofer, TU Muenchen LF style proof terms. *) infix 8 % %% %>; signature PROOFTERM = sig type thm_header = {serial: serial, pos: Position.T list, theory_name: string, name: string, prop: term, types: typ list option} type thm_body type thm_node datatype proof = MinProof | PBound of int | Abst of string * typ option * proof | AbsP of string * term option * proof | % of proof * term option | %% of proof * proof | Hyp of term | PAxm of string * term * typ list option | OfClass of typ * class | Oracle of string * term * typ list option | PThm of thm_header * thm_body and proof_body = PBody of {oracles: (string * term option) Ord_List.T, thms: (serial * thm_node) Ord_List.T, proof: proof} type oracle = string * term option type thm = serial * thm_node exception MIN_PROOF of unit val proof_of: proof_body -> proof val join_proof: proof_body future -> proof val map_proof_of: (proof -> proof) -> proof_body -> proof_body val thm_header: serial -> Position.T list -> string -> string -> term -> typ list option -> thm_header val thm_body: proof_body -> thm_body val thm_body_proof_raw: thm_body -> proof val thm_body_proof_open: thm_body -> proof val thm_node_theory_name: thm_node -> string val thm_node_name: thm_node -> string val thm_node_prop: thm_node -> term val thm_node_body: thm_node -> proof_body future val thm_node_thms: thm_node -> thm list val join_thms: thm list -> proof_body list val consolidate: proof_body list -> unit val make_thm: thm_header -> thm_body -> thm val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a val fold_body_thms: ({serial: serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) -> proof_body list -> 'a -> 'a val oracle_ord: oracle ord val thm_ord: thm ord val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T val unions_thms: thm Ord_List.T list -> thm Ord_List.T val no_proof_body: proof -> proof_body val no_thm_names: proof -> proof val no_thm_proofs: proof -> proof val no_body_proofs: proof -> proof val encode: Consts.T -> proof XML.Encode.T val encode_body: Consts.T -> proof_body XML.Encode.T val encode_standard_term: Consts.T -> term XML.Encode.T val encode_standard_proof: Consts.T -> proof XML.Encode.T val decode: Consts.T -> proof XML.Decode.T val decode_body: Consts.T -> proof_body XML.Decode.T val %> : proof * term -> proof (*primitive operations*) val proofs: int Unsynchronized.ref val proofs_enabled: unit -> bool val atomic_proof: proof -> bool val compact_proof: proof -> bool val proof_combt: proof * term list -> proof val proof_combt': proof * term option list -> proof val proof_combP: proof * proof list -> proof val strip_combt: proof -> proof * term option list val strip_combP: proof -> proof * proof list val strip_thm_body: proof_body -> proof_body val map_proof_same: term Same.operation -> typ Same.operation -> (typ * class -> proof) -> proof Same.operation val map_proof_terms_same: term Same.operation -> typ Same.operation -> proof Same.operation val map_proof_types_same: typ Same.operation -> proof Same.operation val map_proof_terms: (term -> term) -> (typ -> typ) -> proof -> proof val map_proof_types: (typ -> typ) -> proof -> proof val fold_proof_terms: (term -> 'a -> 'a) -> proof -> 'a -> 'a val fold_proof_terms_types: (term -> 'a -> 'a) -> (typ -> 'a -> 'a) -> proof -> 'a -> 'a val maxidx_proof: proof -> int -> int val size_of_proof: proof -> int val change_types: typ list option -> proof -> proof val prf_abstract_over: term -> proof -> proof val prf_incr_bv: int -> int -> int -> int -> proof -> proof val incr_pboundvars: int -> int -> proof -> proof val prf_loose_bvar1: proof -> int -> bool val prf_loose_Pbvar1: proof -> int -> bool val prf_add_loose_bnos: int -> int -> proof -> int list * int list -> int list * int list val norm_proof: Envir.env -> proof -> proof val norm_proof': Envir.env -> proof -> proof val prf_subst_bounds: term list -> proof -> proof val prf_subst_pbounds: proof list -> proof -> proof val freeze_thaw_prf: proof -> proof * (proof -> proof) (*proof terms for specific inference rules*) val trivial_proof: proof val implies_intr_proof: term -> proof -> proof val implies_intr_proof': term -> proof -> proof val forall_intr_proof: string * term -> typ option -> proof -> proof val forall_intr_proof': term -> proof -> proof val varify_proof: term -> (string * sort) list -> proof -> proof val legacy_freezeT: term -> proof -> proof val rotate_proof: term list -> term -> (string * typ) list -> term list -> int -> proof -> proof val permute_prems_proof: term list -> int -> int -> proof -> proof val generalize_proof: string list * string list -> int -> term -> proof -> proof val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> proof -> proof val lift_proof: term -> int -> term -> proof -> proof val incr_indexes: int -> proof -> proof val assumption_proof: term list -> term -> int -> proof -> proof val bicompose_proof: bool -> term list -> term list -> term option -> term list -> int -> int -> proof -> proof -> proof val equality_axms: (string * term) list val reflexive_axm: proof val symmetric_axm: proof val transitive_axm: proof val equal_intr_axm: proof val equal_elim_axm: proof val abstract_rule_axm: proof val combination_axm: proof val reflexive_proof: proof val symmetric_proof: proof -> proof val transitive_proof: typ -> term -> proof -> proof -> proof val equal_intr_proof: term -> term -> proof -> proof -> proof val equal_elim_proof: term -> term -> proof -> proof -> proof val abstract_rule_proof: string * term -> proof -> proof val combination_proof: term -> term -> term -> term -> proof -> proof -> proof val strip_shyps_proof: Sorts.algebra -> (typ * sort) list -> (typ * sort) list -> sort list -> proof -> proof val of_sort_proof: Sorts.algebra -> (class * class -> proof) -> (string * class list list * class -> proof) -> (typ * class -> proof) -> typ * sort -> proof list val axm_proof: string -> term -> proof val oracle_proof: string -> term -> proof val shrink_proof: proof -> proof (*rewriting on proof terms*) val add_prf_rrule: proof * proof -> theory -> theory val add_prf_rproc: (typ list -> term option list -> proof -> (proof * proof) option) -> theory -> theory val set_preproc: (theory -> proof -> proof) -> theory -> theory val forall_intr_variables_term: term -> term val forall_intr_variables: term -> proof -> proof val no_skel: proof val normal_skel: proof val rewrite_proof: theory -> (proof * proof) list * (typ list -> term option list -> proof -> (proof * proof) option) list -> proof -> proof val rewrite_proof_notypes: (proof * proof) list * (typ list -> term option list -> proof -> (proof * proof) option) list -> proof -> proof val rew_proof: theory -> proof -> proof val reconstruct_proof: theory -> term -> proof -> proof val prop_of': term list -> proof -> term val prop_of: proof -> term val expand_name_empty: thm_header -> string option val expand_proof: theory -> (thm_header -> string option) -> proof -> proof val standard_vars: Name.context -> term * proof option -> term * proof option val standard_vars_term: Name.context -> term -> term val add_standard_vars: proof -> (string * typ) list -> (string * typ) list val add_standard_vars_term: term -> (string * typ) list -> (string * typ) list val export_enabled: unit -> bool val export_standard_enabled: unit -> bool val export_proof_boxes_required: theory -> bool val export_proof_boxes: proof list -> unit val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body val thm_proof: theory -> (class * class -> proof) -> (string * class list list * class -> proof) -> string * Position.T -> sort list -> term list -> term -> (serial * proof_body future) list -> proof_body -> thm * proof val unconstrain_thm_proof: theory -> (class * class -> proof) -> (string * class list list * class -> proof) -> sort list -> term -> (serial * proof_body future) list -> proof_body -> thm * proof val get_identity: sort list -> term list -> term -> proof -> {serial: serial, theory_name: string, name: string} option val get_approximative_name: sort list -> term list -> term -> proof -> string type thm_id = {serial: serial, theory_name: string} val make_thm_id: serial * string -> thm_id val thm_header_id: thm_header -> thm_id val thm_id: thm -> thm_id val get_id: sort list -> term list -> term -> proof -> thm_id option val this_id: thm_id option -> thm_id -> bool val proof_boxes: {excluded: thm_id -> bool, included: thm_id -> bool} -> proof list -> (thm_header * proof) list (*exception MIN_PROOF*) end structure Proofterm : PROOFTERM = struct (** datatype proof **) type thm_header = {serial: serial, pos: Position.T list, theory_name: string, name: string, prop: term, types: typ list option}; datatype proof = MinProof | PBound of int | Abst of string * typ option * proof | AbsP of string * term option * proof | op % of proof * term option | op %% of proof * proof | Hyp of term | PAxm of string * term * typ list option | OfClass of typ * class | Oracle of string * term * typ list option | PThm of thm_header * thm_body and proof_body = PBody of {oracles: (string * term option) Ord_List.T, thms: (serial * thm_node) Ord_List.T, proof: proof} and thm_body = Thm_Body of {export_proof: unit lazy, open_proof: proof -> proof, body: proof_body future} and thm_node = Thm_Node of {theory_name: string, name: string, prop: term, body: proof_body future, consolidate: unit lazy}; type oracle = string * term option; val oracle_ord = prod_ord fast_string_ord (option_ord Term_Ord.fast_term_ord); type thm = serial * thm_node; val thm_ord: thm ord = fn ((i, _), (j, _)) => int_ord (j, i); exception MIN_PROOF of unit; fun proof_of (PBody {proof, ...}) = proof; val join_proof = Future.join #> proof_of; fun map_proof_of f (PBody {oracles, thms, proof}) = PBody {oracles = oracles, thms = thms, proof = f proof}; fun thm_header serial pos theory_name name prop types : thm_header = {serial = serial, pos = pos, theory_name = theory_name, name = name, prop = prop, types = types}; val no_export_proof = Lazy.value (); fun thm_body body = Thm_Body {export_proof = no_export_proof, open_proof = I, body = Future.value body}; fun thm_body_export_proof (Thm_Body {export_proof, ...}) = export_proof; fun thm_body_proof_raw (Thm_Body {body, ...}) = join_proof body; fun thm_body_proof_open (Thm_Body {open_proof, body, ...}) = open_proof (join_proof body); fun rep_thm_node (Thm_Node args) = args; val thm_node_theory_name = #theory_name o rep_thm_node; val thm_node_name = #name o rep_thm_node; val thm_node_prop = #prop o rep_thm_node; val thm_node_body = #body o rep_thm_node; val thm_node_thms = thm_node_body #> Future.join #> (fn PBody {thms, ...} => thms); val thm_node_consolidate = #consolidate o rep_thm_node; fun join_thms (thms: thm list) = Future.joins (map (thm_node_body o #2) thms); val consolidate = maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms) #> Lazy.consolidate #> map Lazy.force #> ignore; fun make_thm_node theory_name name prop body = Thm_Node {theory_name = theory_name, name = name, prop = prop, body = body, consolidate = Lazy.lazy_name "Proofterm.make_thm_node" (fn () => let val PBody {thms, ...} = Future.join body in consolidate (join_thms thms) end)}; fun make_thm ({serial, theory_name, name, prop, ...}: thm_header) (Thm_Body {body, ...}) = (serial, make_thm_node theory_name name prop body); (* proof atoms *) fun fold_proof_atoms all f = let fun app (Abst (_, _, prf)) = app prf | app (AbsP (_, _, prf)) = app prf | app (prf % _) = app prf | app (prf1 %% prf2) = app prf1 #> app prf2 | app (prf as PThm ({serial = i, ...}, Thm_Body {body, ...})) = (fn (x, seen) => if Inttab.defined seen i then (x, seen) else let val (x', seen') = (if all then app (join_proof body) else I) (x, Inttab.update (i, ()) seen) in (f prf x', seen') end) | app prf = (fn (x, seen) => (f prf x, seen)); in fn prfs => fn x => #1 (fold app prfs (x, Inttab.empty)) end; fun fold_body_thms f = let fun app (PBody {thms, ...}) = tap join_thms thms |> fold (fn (i, thm_node) => fn (x, seen) => if Inttab.defined seen i then (x, seen) else let val name = thm_node_name thm_node; val prop = thm_node_prop thm_node; val body = Future.join (thm_node_body thm_node); val (x', seen') = app body (x, Inttab.update (i, ()) seen); in (f {serial = i, name = name, prop = prop, body = body} x', seen') end); in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end; (* proof body *) val unions_oracles = Ord_List.unions oracle_ord; val unions_thms = Ord_List.unions thm_ord; fun no_proof_body proof = PBody {oracles = [], thms = [], proof = proof}; val no_thm_body = thm_body (no_proof_body MinProof); fun no_thm_names (Abst (x, T, prf)) = Abst (x, T, no_thm_names prf) | no_thm_names (AbsP (x, t, prf)) = AbsP (x, t, no_thm_names prf) | no_thm_names (prf % t) = no_thm_names prf % t | no_thm_names (prf1 %% prf2) = no_thm_names prf1 %% no_thm_names prf2 | no_thm_names (PThm ({serial, pos, theory_name, name = _, prop, types}, thm_body)) = PThm (thm_header serial pos theory_name "" prop types, thm_body) | no_thm_names a = a; fun no_thm_proofs (Abst (x, T, prf)) = Abst (x, T, no_thm_proofs prf) | no_thm_proofs (AbsP (x, t, prf)) = AbsP (x, t, no_thm_proofs prf) | no_thm_proofs (prf % t) = no_thm_proofs prf % t | no_thm_proofs (prf1 %% prf2) = no_thm_proofs prf1 %% no_thm_proofs prf2 | no_thm_proofs (PThm (header, _)) = PThm (header, no_thm_body) | no_thm_proofs a = a; fun no_body_proofs (Abst (x, T, prf)) = Abst (x, T, no_body_proofs prf) | no_body_proofs (AbsP (x, t, prf)) = AbsP (x, t, no_body_proofs prf) | no_body_proofs (prf % t) = no_body_proofs prf % t | no_body_proofs (prf1 %% prf2) = no_body_proofs prf1 %% no_body_proofs prf2 | no_body_proofs (PThm (header, Thm_Body {export_proof, open_proof, body})) = let val body' = Future.value (no_proof_body (join_proof body)); val thm_body' = Thm_Body {export_proof = export_proof, open_proof = open_proof, body = body'}; in PThm (header, thm_body') end | no_body_proofs a = a; (** XML data representation **) (* encode *) local open XML.Encode Term_XML.Encode; fun proof consts prf = prf |> variant [fn MinProof => ([], []), fn PBound a => ([], int a), fn Abst (a, b, c) => ([a], pair (option typ) (proof consts) (b, c)), fn AbsP (a, b, c) => ([a], pair (option (term consts)) (proof consts) (b, c)), fn a % b => ([], pair (proof consts) (option (term consts)) (a, b)), fn a %% b => ([], pair (proof consts) (proof consts) (a, b)), fn Hyp a => ([], term consts a), fn PAxm (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)), fn OfClass (a, b) => ([b], typ a), fn Oracle (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)), fn PThm ({serial, pos, theory_name, name, prop, types}, Thm_Body {open_proof, body, ...}) => ([int_atom serial, theory_name, name], pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts))) (map Position.properties_of pos, (prop, (types, map_proof_of open_proof (Future.join body)))))] and proof_body consts (PBody {oracles, thms, proof = prf}) = triple (list (pair string (option (term consts)))) (list (thm consts)) (proof consts) (oracles, thms, prf) and thm consts (a, thm_node) = pair int (pair string (pair string (pair (term consts) (proof_body consts)))) (a, (thm_node_theory_name thm_node, (thm_node_name thm_node, (thm_node_prop thm_node, (Future.join (thm_node_body thm_node)))))); fun standard_term consts t = t |> variant [fn Const (a, b) => ([a], list typ (Consts.typargs consts (a, b))), fn Free (a, _) => ([a], []), fn Var (a, _) => (indexname a, []), fn Bound a => ([], int a), fn Abs (a, b, c) => ([a], pair typ (standard_term consts) (b, c)), fn op $ a => ([], pair (standard_term consts) (standard_term consts) a)]; fun standard_proof consts prf = prf |> variant [fn MinProof => ([], []), fn PBound a => ([], int a), fn Abst (a, SOME b, c) => ([a], pair typ (standard_proof consts) (b, c)), fn AbsP (a, SOME b, c) => ([a], pair (standard_term consts) (standard_proof consts) (b, c)), fn a % SOME b => ([], pair (standard_proof consts) (standard_term consts) (a, b)), fn a %% b => ([], pair (standard_proof consts) (standard_proof consts) (a, b)), fn Hyp a => ([], standard_term consts a), fn PAxm (name, _, SOME Ts) => ([name], list typ Ts), fn OfClass (T, c) => ([c], typ T), fn Oracle (name, prop, SOME Ts) => ([name], pair (standard_term consts) (list typ) (prop, Ts)), fn PThm ({serial, theory_name, name, types = SOME Ts, ...}, _) => ([int_atom serial, theory_name, name], list typ Ts)]; in val encode = proof; val encode_body = proof_body; val encode_standard_term = standard_term; val encode_standard_proof = standard_proof; end; (* decode *) local open XML.Decode Term_XML.Decode; fun proof consts prf = prf |> variant [fn ([], []) => MinProof, fn ([], a) => PBound (int a), fn ([a], b) => let val (c, d) = pair (option typ) (proof consts) b in Abst (a, c, d) end, fn ([a], b) => let val (c, d) = pair (option (term consts)) (proof consts) b in AbsP (a, c, d) end, fn ([], a) => op % (pair (proof consts) (option (term consts)) a), fn ([], a) => op %% (pair (proof consts) (proof consts) a), fn ([], a) => Hyp (term consts a), fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in PAxm (a, c, d) end, fn ([b], a) => OfClass (typ a, b), fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in Oracle (a, c, d) end, fn ([a, b, c], d) => let val ((e, (f, (g, h)))) = pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts))) d; val header = thm_header (int_atom a) (map Position.of_properties e) b c f g; in PThm (header, thm_body h) end] and proof_body consts x = let val (a, b, c) = triple (list (pair string (option (term consts)))) (list (thm consts)) (proof consts) x; in PBody {oracles = a, thms = b, proof = c} end and thm consts x = let val (a, (b, (c, (d, e)))) = pair int (pair string (pair string (pair (term consts) (proof_body consts)))) x in (a, make_thm_node b c d (Future.value e)) end; in val decode = proof; val decode_body = proof_body; end; (** proof objects with different levels of detail **) val proofs = Unsynchronized.ref 2; fun proofs_enabled () = ! proofs >= 2; fun atomic_proof prf = (case prf of Abst _ => false | AbsP _ => false | op % _ => false | op %% _ => false | MinProof => false | _ => true); fun compact_proof (prf % _) = compact_proof prf | compact_proof (prf1 %% prf2) = atomic_proof prf2 andalso compact_proof prf1 | compact_proof prf = atomic_proof prf; fun (prf %> t) = prf % SOME t; val proof_combt = Library.foldl (op %>); val proof_combt' = Library.foldl (op %); val proof_combP = Library.foldl (op %%); fun strip_combt prf = let fun stripc (prf % t, ts) = stripc (prf, t::ts) | stripc x = x in stripc (prf, []) end; fun strip_combP prf = let fun stripc (prf %% prf', prfs) = stripc (prf, prf'::prfs) | stripc x = x in stripc (prf, []) end; fun strip_thm_body (body as PBody {proof, ...}) = (case fst (strip_combt (fst (strip_combP proof))) of PThm (_, Thm_Body {body = body', ...}) => Future.join body' | _ => body); val mk_Abst = fold_rev (fn (x, _: typ) => fn prf => Abst (x, NONE, prf)); val mk_AbsP = fold_rev (fn _: term => fn prf => AbsP ("H", NONE, prf)); fun map_proof_same term typ ofclass = let val typs = Same.map typ; fun proof (Abst (s, T, prf)) = (Abst (s, Same.map_option typ T, Same.commit proof prf) handle Same.SAME => Abst (s, T, proof prf)) | proof (AbsP (s, t, prf)) = (AbsP (s, Same.map_option term t, Same.commit proof prf) handle Same.SAME => AbsP (s, t, proof prf)) | proof (prf % t) = (proof prf % Same.commit (Same.map_option term) t handle Same.SAME => prf % Same.map_option term t) | proof (prf1 %% prf2) = (proof prf1 %% Same.commit proof prf2 handle Same.SAME => prf1 %% proof prf2) | proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts)) | proof (OfClass T_c) = ofclass T_c | proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts)) | proof (PThm ({serial, pos, theory_name, name, prop, types = SOME Ts}, thm_body)) = PThm (thm_header serial pos theory_name name prop (SOME (typs Ts)), thm_body) | proof _ = raise Same.SAME; in proof end; fun map_proof_terms_same term typ = map_proof_same term typ (fn (T, c) => OfClass (typ T, c)); fun map_proof_types_same typ = map_proof_terms_same (Term_Subst.map_types_same typ) typ; fun same eq f x = let val x' = f x in if eq (x, x') then raise Same.SAME else x' end; fun map_proof_terms f g = Same.commit (map_proof_terms_same (same (op =) f) (same (op =) g)); fun map_proof_types f = Same.commit (map_proof_types_same (same (op =) f)); fun fold_proof_terms f (Abst (_, _, prf)) = fold_proof_terms f prf | fold_proof_terms f (AbsP (_, SOME t, prf)) = f t #> fold_proof_terms f prf | fold_proof_terms f (AbsP (_, NONE, prf)) = fold_proof_terms f prf | fold_proof_terms f (prf % SOME t) = fold_proof_terms f prf #> f t | fold_proof_terms f (prf % NONE) = fold_proof_terms f prf | fold_proof_terms f (prf1 %% prf2) = fold_proof_terms f prf1 #> fold_proof_terms f prf2 | fold_proof_terms _ _ = I; fun fold_proof_terms_types f g (Abst (_, SOME T, prf)) = g T #> fold_proof_terms_types f g prf | fold_proof_terms_types f g (Abst (_, NONE, prf)) = fold_proof_terms_types f g prf | fold_proof_terms_types f g (AbsP (_, SOME t, prf)) = f t #> fold_proof_terms_types f g prf | fold_proof_terms_types f g (AbsP (_, NONE, prf)) = fold_proof_terms_types f g prf | fold_proof_terms_types f g (prf % SOME t) = fold_proof_terms_types f g prf #> f t | fold_proof_terms_types f g (prf % NONE) = fold_proof_terms_types f g prf | fold_proof_terms_types f g (prf1 %% prf2) = fold_proof_terms_types f g prf1 #> fold_proof_terms_types f g prf2 | fold_proof_terms_types _ g (PAxm (_, _, SOME Ts)) = fold g Ts | fold_proof_terms_types _ g (OfClass (T, _)) = g T | fold_proof_terms_types _ g (Oracle (_, _, SOME Ts)) = fold g Ts | fold_proof_terms_types _ g (PThm ({types = SOME Ts, ...}, _)) = fold g Ts | fold_proof_terms_types _ _ _ = I; fun maxidx_proof prf = fold_proof_terms_types Term.maxidx_term Term.maxidx_typ prf; fun size_of_proof (Abst (_, _, prf)) = 1 + size_of_proof prf | size_of_proof (AbsP (_, _, prf)) = 1 + size_of_proof prf | size_of_proof (prf % _) = 1 + size_of_proof prf | size_of_proof (prf1 %% prf2) = size_of_proof prf1 + size_of_proof prf2 | size_of_proof _ = 1; fun change_types types (PAxm (name, prop, _)) = PAxm (name, prop, types) | change_types (SOME [T]) (OfClass (_, c)) = OfClass (T, c) | change_types types (Oracle (name, prop, _)) = Oracle (name, prop, types) | change_types types (PThm ({serial, pos, theory_name, name, prop, types = _}, thm_body)) = PThm (thm_header serial pos theory_name name prop types, thm_body) | change_types _ prf = prf; (* utilities *) fun strip_abs (_::Ts) (Abs (_, _, t)) = strip_abs Ts t | strip_abs _ t = t; fun mk_abs Ts t = Library.foldl (fn (t', T) => Abs ("", T, t')) (t, Ts); (*Abstraction of a proof term over its occurrences of v, which must contain no loose bound variables. The resulting proof term is ready to become the body of an Abst.*) fun prf_abstract_over v = let fun abst' lev u = if v aconv u then Bound lev else (case u of Abs (a, T, t) => Abs (a, T, abst' (lev + 1) t) | f $ t => (abst' lev f $ absth' lev t handle Same.SAME => f $ abst' lev t) | _ => raise Same.SAME) and absth' lev t = (abst' lev t handle Same.SAME => t); fun abst lev (AbsP (a, t, prf)) = (AbsP (a, Same.map_option (abst' lev) t, absth lev prf) handle Same.SAME => AbsP (a, t, abst lev prf)) | abst lev (Abst (a, T, prf)) = Abst (a, T, abst (lev + 1) prf) | abst lev (prf1 %% prf2) = (abst lev prf1 %% absth lev prf2 handle Same.SAME => prf1 %% abst lev prf2) | abst lev (prf % t) = (abst lev prf % Option.map (absth' lev) t handle Same.SAME => prf % Same.map_option (abst' lev) t) | abst _ _ = raise Same.SAME and absth lev prf = (abst lev prf handle Same.SAME => prf); in absth 0 end; (*increments a proof term's non-local bound variables required when moving a proof term within abstractions inc is increment for bound variables lev is level at which a bound variable is considered 'loose'*) fun incr_bv' inct tlev t = incr_bv (inct, tlev, t); fun prf_incr_bv' incP _ Plev _ (PBound i) = if i >= Plev then PBound (i+incP) else raise Same.SAME | prf_incr_bv' incP inct Plev tlev (AbsP (a, t, body)) = (AbsP (a, Same.map_option (same (op =) (incr_bv' inct tlev)) t, prf_incr_bv incP inct (Plev+1) tlev body) handle Same.SAME => AbsP (a, t, prf_incr_bv' incP inct (Plev+1) tlev body)) | prf_incr_bv' incP inct Plev tlev (Abst (a, T, body)) = Abst (a, T, prf_incr_bv' incP inct Plev (tlev+1) body) | prf_incr_bv' incP inct Plev tlev (prf %% prf') = (prf_incr_bv' incP inct Plev tlev prf %% prf_incr_bv incP inct Plev tlev prf' handle Same.SAME => prf %% prf_incr_bv' incP inct Plev tlev prf') | prf_incr_bv' incP inct Plev tlev (prf % t) = (prf_incr_bv' incP inct Plev tlev prf % Option.map (incr_bv' inct tlev) t handle Same.SAME => prf % Same.map_option (same (op =) (incr_bv' inct tlev)) t) | prf_incr_bv' _ _ _ _ _ = raise Same.SAME and prf_incr_bv incP inct Plev tlev prf = (prf_incr_bv' incP inct Plev tlev prf handle Same.SAME => prf); fun incr_pboundvars 0 0 prf = prf | incr_pboundvars incP inct prf = prf_incr_bv incP inct 0 0 prf; fun prf_loose_bvar1 (prf1 %% prf2) k = prf_loose_bvar1 prf1 k orelse prf_loose_bvar1 prf2 k | prf_loose_bvar1 (prf % SOME t) k = prf_loose_bvar1 prf k orelse loose_bvar1 (t, k) | prf_loose_bvar1 (_ % NONE) _ = true | prf_loose_bvar1 (AbsP (_, SOME t, prf)) k = loose_bvar1 (t, k) orelse prf_loose_bvar1 prf k | prf_loose_bvar1 (AbsP (_, NONE, _)) _ = true | prf_loose_bvar1 (Abst (_, _, prf)) k = prf_loose_bvar1 prf (k+1) | prf_loose_bvar1 _ _ = false; fun prf_loose_Pbvar1 (PBound i) k = i = k | prf_loose_Pbvar1 (prf1 %% prf2) k = prf_loose_Pbvar1 prf1 k orelse prf_loose_Pbvar1 prf2 k | prf_loose_Pbvar1 (prf % _) k = prf_loose_Pbvar1 prf k | prf_loose_Pbvar1 (AbsP (_, _, prf)) k = prf_loose_Pbvar1 prf (k+1) | prf_loose_Pbvar1 (Abst (_, _, prf)) k = prf_loose_Pbvar1 prf k | prf_loose_Pbvar1 _ _ = false; fun prf_add_loose_bnos plev _ (PBound i) (is, js) = if i < plev then (is, js) else (insert (op =) (i-plev) is, js) | prf_add_loose_bnos plev tlev (prf1 %% prf2) p = prf_add_loose_bnos plev tlev prf2 (prf_add_loose_bnos plev tlev prf1 p) | prf_add_loose_bnos plev tlev (prf % opt) (is, js) = prf_add_loose_bnos plev tlev prf (case opt of NONE => (is, insert (op =) ~1 js) | SOME t => (is, add_loose_bnos (t, tlev, js))) | prf_add_loose_bnos plev tlev (AbsP (_, opt, prf)) (is, js) = prf_add_loose_bnos (plev+1) tlev prf (case opt of NONE => (is, insert (op =) ~1 js) | SOME t => (is, add_loose_bnos (t, tlev, js))) | prf_add_loose_bnos plev tlev (Abst (_, _, prf)) p = prf_add_loose_bnos plev (tlev+1) prf p | prf_add_loose_bnos _ _ _ _ = ([], []); (* substitutions *) fun del_conflicting_tvars envT T = Term_Subst.instantiateT (map_filter (fn ixnS as (_, S) => (Type.lookup envT ixnS; NONE) handle TYPE _ => SOME (ixnS, Logic.dummy_tfree S)) (Term.add_tvarsT T [])) T; fun del_conflicting_vars env t = Term_Subst.instantiate (map_filter (fn ixnS as (_, S) => (Type.lookup (Envir.type_env env) ixnS; NONE) handle TYPE _ => SOME (ixnS, Logic.dummy_tfree S)) (Term.add_tvars t []), map_filter (fn (ixnT as (_, T)) => (Envir.lookup env ixnT; NONE) handle TYPE _ => SOME (ixnT, Free ("dummy", T))) (Term.add_vars t [])) t; fun norm_proof env = let val envT = Envir.type_env env; fun msg s = warning ("type conflict in norm_proof:\n" ^ s); fun htype f t = f env t handle TYPE (s, _, _) => (msg s; f env (del_conflicting_vars env t)); fun htypeT f T = f envT T handle TYPE (s, _, _) => (msg s; f envT (del_conflicting_tvars envT T)); fun htypeTs f Ts = f envT Ts handle TYPE (s, _, _) => (msg s; f envT (map (del_conflicting_tvars envT) Ts)); fun norm (Abst (s, T, prf)) = (Abst (s, Same.map_option (htypeT Envir.norm_type_same) T, Same.commit norm prf) handle Same.SAME => Abst (s, T, norm prf)) | norm (AbsP (s, t, prf)) = (AbsP (s, Same.map_option (htype Envir.norm_term_same) t, Same.commit norm prf) handle Same.SAME => AbsP (s, t, norm prf)) | norm (prf % t) = (norm prf % Option.map (htype Envir.norm_term) t handle Same.SAME => prf % Same.map_option (htype Envir.norm_term_same) t) | norm (prf1 %% prf2) = (norm prf1 %% Same.commit norm prf2 handle Same.SAME => prf1 %% norm prf2) | norm (PAxm (s, prop, Ts)) = PAxm (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts) | norm (OfClass (T, c)) = OfClass (htypeT Envir.norm_type_same T, c) | norm (Oracle (s, prop, Ts)) = Oracle (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts) | norm (PThm ({serial = i, pos = p, theory_name, name = a, prop = t, types = Ts}, thm_body)) = PThm (thm_header i p theory_name a t (Same.map_option (htypeTs Envir.norm_types_same) Ts), thm_body) | norm _ = raise Same.SAME; in Same.commit norm end; (* remove some types in proof term (to save space) *) fun remove_types (Abs (s, _, t)) = Abs (s, dummyT, remove_types t) | remove_types (t $ u) = remove_types t $ remove_types u | remove_types (Const (s, _)) = Const (s, dummyT) | remove_types t = t; fun remove_types_env (Envir.Envir {maxidx, tenv, tyenv}) = Envir.Envir {maxidx = maxidx, tenv = Vartab.map (K (apsnd remove_types)) tenv, tyenv = tyenv}; fun norm_proof' env prf = norm_proof (remove_types_env env) prf; (* substitution of bound variables *) fun prf_subst_bounds args prf = let val n = length args; fun subst' lev (Bound i) = (if i Bound (i-n)) (*loose: change it*) | subst' lev (Abs (a, T, body)) = Abs (a, T, subst' (lev+1) body) | subst' lev (f $ t) = (subst' lev f $ substh' lev t handle Same.SAME => f $ subst' lev t) | subst' _ _ = raise Same.SAME and substh' lev t = (subst' lev t handle Same.SAME => t); fun subst lev (AbsP (a, t, body)) = (AbsP (a, Same.map_option (subst' lev) t, substh lev body) handle Same.SAME => AbsP (a, t, subst lev body)) | subst lev (Abst (a, T, body)) = Abst (a, T, subst (lev+1) body) | subst lev (prf %% prf') = (subst lev prf %% substh lev prf' handle Same.SAME => prf %% subst lev prf') | subst lev (prf % t) = (subst lev prf % Option.map (substh' lev) t handle Same.SAME => prf % Same.map_option (subst' lev) t) | subst _ _ = raise Same.SAME and substh lev prf = (subst lev prf handle Same.SAME => prf); in (case args of [] => prf | _ => substh 0 prf) end; fun prf_subst_pbounds args prf = let val n = length args; fun subst (PBound i) Plev tlev = (if i < Plev then raise Same.SAME (*var is locally bound*) else incr_pboundvars Plev tlev (nth args (i-Plev)) handle General.Subscript => PBound (i-n) (*loose: change it*)) | subst (AbsP (a, t, body)) Plev tlev = AbsP (a, t, subst body (Plev+1) tlev) | subst (Abst (a, T, body)) Plev tlev = Abst (a, T, subst body Plev (tlev+1)) | subst (prf %% prf') Plev tlev = (subst prf Plev tlev %% substh prf' Plev tlev handle Same.SAME => prf %% subst prf' Plev tlev) | subst (prf % t) Plev tlev = subst prf Plev tlev % t | subst _ _ _ = raise Same.SAME and substh prf Plev tlev = (subst prf Plev tlev handle Same.SAME => prf) in (case args of [] => prf | _ => substh prf 0 0) end; (* freezing and thawing of variables in proof terms *) local fun frzT names = map_type_tvar (fn (ixn, S) => TFree (the (AList.lookup (op =) names ixn), S)); fun thawT names = map_type_tfree (fn (a, S) => (case AList.lookup (op =) names a of NONE => TFree (a, S) | SOME ixn => TVar (ixn, S))); fun freeze names names' (t $ u) = freeze names names' t $ freeze names names' u | freeze names names' (Abs (s, T, t)) = Abs (s, frzT names' T, freeze names names' t) | freeze _ names' (Const (s, T)) = Const (s, frzT names' T) | freeze _ names' (Free (s, T)) = Free (s, frzT names' T) | freeze names names' (Var (ixn, T)) = Free (the (AList.lookup (op =) names ixn), frzT names' T) | freeze _ _ t = t; fun thaw names names' (t $ u) = thaw names names' t $ thaw names names' u | thaw names names' (Abs (s, T, t)) = Abs (s, thawT names' T, thaw names names' t) | thaw _ names' (Const (s, T)) = Const (s, thawT names' T) | thaw names names' (Free (s, T)) = let val T' = thawT names' T in (case AList.lookup (op =) names s of NONE => Free (s, T') | SOME ixn => Var (ixn, T')) end | thaw _ names' (Var (ixn, T)) = Var (ixn, thawT names' T) | thaw _ _ t = t; in fun freeze_thaw_prf prf = let val (fs, Tfs, vs, Tvs) = fold_proof_terms_types (fn t => fn (fs, Tfs, vs, Tvs) => (Term.add_free_names t fs, Term.add_tfree_names t Tfs, Term.add_var_names t vs, Term.add_tvar_names t Tvs)) (fn T => fn (fs, Tfs, vs, Tvs) => (fs, Term.add_tfree_namesT T Tfs, vs, Term.add_tvar_namesT T Tvs)) prf ([], [], [], []); val names = vs ~~ Name.variant_list fs (map fst vs); val names' = Tvs ~~ Name.variant_list Tfs (map fst Tvs); val rnames = map swap names; val rnames' = map swap names'; in (map_proof_terms (freeze names names') (frzT names') prf, map_proof_terms (thaw rnames rnames') (thawT rnames')) end; end; (** inference rules **) (* trivial implication *) val trivial_proof = AbsP ("H", NONE, PBound 0); (* implication introduction *) fun gen_implies_intr_proof f h prf = let fun abshyp i (Hyp t) = if h aconv t then PBound i else raise Same.SAME | abshyp i (Abst (s, T, prf)) = Abst (s, T, abshyp i prf) | abshyp i (AbsP (s, t, prf)) = AbsP (s, t, abshyp (i + 1) prf) | abshyp i (prf % t) = abshyp i prf % t | abshyp i (prf1 %% prf2) = (abshyp i prf1 %% abshyph i prf2 handle Same.SAME => prf1 %% abshyp i prf2) | abshyp _ _ = raise Same.SAME and abshyph i prf = (abshyp i prf handle Same.SAME => prf); in AbsP ("H", f h, abshyph 0 prf) end; val implies_intr_proof = gen_implies_intr_proof (K NONE); val implies_intr_proof' = gen_implies_intr_proof SOME; (* forall introduction *) fun forall_intr_proof (a, v) opt_T prf = Abst (a, opt_T, prf_abstract_over v prf); fun forall_intr_proof' v prf = let val (a, T) = (case v of Var ((a, _), T) => (a, T) | Free (a, T) => (a, T)) in forall_intr_proof (a, v) (SOME T) prf end; (* varify *) fun varify_proof t fixed prf = let val fs = Term.fold_types (Term.fold_atyps (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t []; val used = Name.context |> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t; val fmap = fs ~~ #1 (fold_map Name.variant (map fst fs) used); fun thaw (a, S) = (case AList.lookup (op =) fmap (a, S) of NONE => TFree (a, S) | SOME b => TVar ((b, 0), S)); in map_proof_terms (map_types (map_type_tfree thaw)) (map_type_tfree thaw) prf end; local fun new_name ix (pairs, used) = let val v = singleton (Name.variant_list used) (string_of_indexname ix) in ((ix, v) :: pairs, v :: used) end; fun freeze_one alist (ix, sort) = (case AList.lookup (op =) alist ix of NONE => TVar (ix, sort) | SOME name => TFree (name, sort)); in fun legacy_freezeT t prf = let val used = Term.add_tfree_names t []; val (alist, _) = fold_rev new_name (map #1 (Term.add_tvars t [])) ([], used); in (case alist of [] => prf (*nothing to do!*) | _ => let val frzT = map_type_tvar (freeze_one alist) in map_proof_terms (map_types frzT) frzT prf end) end; end; (* rotate assumptions *) fun rotate_proof Bs Bi' params asms m prf = let val i = length asms; val j = length Bs; in mk_AbsP (Bs @ [Bi']) (proof_combP (prf, map PBound (j downto 1) @ [mk_Abst params (mk_AbsP asms (proof_combP (proof_combt (PBound i, map Bound ((length params - 1) downto 0)), map PBound (((i-m-1) downto 0) @ ((i-1) downto (i-m))))))])) end; (* permute premises *) fun permute_prems_proof prems' j k prf = let val n = length prems' in mk_AbsP prems' (proof_combP (prf, map PBound ((n-1 downto n-j) @ (k-1 downto 0) @ (n-j-1 downto k)))) end; (* generalization *) fun generalize_proof (tfrees, frees) idx prop prf = let val gen = if null frees then [] else fold_aterms (fn Free (x, T) => member (op =) frees x ? insert (op =) (x, T) | _ => I) (Term_Subst.generalize (tfrees, []) idx prop) []; in prf |> Same.commit (map_proof_terms_same (Term_Subst.generalize_same (tfrees, []) idx) (Term_Subst.generalizeT_same tfrees idx)) |> fold (fn (x, T) => forall_intr_proof (x, Free (x, T)) NONE) gen |> fold_rev (fn (x, T) => fn prf' => prf' %> Var (Name.clean_index (x, idx), T)) gen end; (* instantiation *) fun instantiate (instT, inst) = Same.commit (map_proof_terms_same (Term_Subst.instantiate_same (instT, map (apsnd remove_types) inst)) (Term_Subst.instantiateT_same instT)); (* lifting *) fun lift_proof Bi inc prop prf = let fun lift'' Us Ts t = strip_abs Ts (Logic.incr_indexes ([], Us, inc) (mk_abs Ts t)); fun lift' Us Ts (Abst (s, T, prf)) = (Abst (s, Same.map_option (Logic.incr_tvar_same inc) T, lifth' Us (dummyT::Ts) prf) handle Same.SAME => Abst (s, T, lift' Us (dummyT::Ts) prf)) | lift' Us Ts (AbsP (s, t, prf)) = (AbsP (s, Same.map_option (same (op =) (lift'' Us Ts)) t, lifth' Us Ts prf) handle Same.SAME => AbsP (s, t, lift' Us Ts prf)) | lift' Us Ts (prf % t) = (lift' Us Ts prf % Option.map (lift'' Us Ts) t handle Same.SAME => prf % Same.map_option (same (op =) (lift'' Us Ts)) t) | lift' Us Ts (prf1 %% prf2) = (lift' Us Ts prf1 %% lifth' Us Ts prf2 handle Same.SAME => prf1 %% lift' Us Ts prf2) | lift' _ _ (PAxm (s, prop, Ts)) = PAxm (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts) | lift' _ _ (OfClass (T, c)) = OfClass (Logic.incr_tvar_same inc T, c) | lift' _ _ (Oracle (s, prop, Ts)) = Oracle (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts) | lift' _ _ (PThm ({serial = i, pos = p, theory_name, name = s, prop, types = Ts}, thm_body)) = PThm (thm_header i p theory_name s prop ((Same.map_option o Same.map) (Logic.incr_tvar inc) Ts), thm_body) | lift' _ _ _ = raise Same.SAME and lifth' Us Ts prf = (lift' Us Ts prf handle Same.SAME => prf); val ps = map (Logic.lift_all inc Bi) (Logic.strip_imp_prems prop); val k = length ps; fun mk_app b (i, j, prf) = if b then (i-1, j, prf %% PBound i) else (i, j-1, prf %> Bound j); fun lift Us bs i j (Const ("Pure.imp", _) $ A $ B) = AbsP ("H", NONE (*A*), lift Us (true::bs) (i+1) j B) | lift Us bs i j (Const ("Pure.all", _) $ Abs (a, T, t)) = Abst (a, NONE (*T*), lift (T::Us) (false::bs) i (j+1) t) | lift Us bs i j _ = proof_combP (lifth' (rev Us) [] prf, map (fn k => (#3 (fold_rev mk_app bs (i-1, j-1, PBound k)))) (i + k - 1 downto i)); in mk_AbsP ps (lift [] [] 0 0 Bi) end; fun incr_indexes i = Same.commit (map_proof_terms_same (Logic.incr_indexes_same ([], [], i)) (Logic.incr_tvar_same i)); (* proof by assumption *) fun mk_asm_prf t i m = let fun imp_prf _ i 0 = PBound i | imp_prf (Const ("Pure.imp", _) $ A $ B) i m = AbsP ("H", NONE (*A*), imp_prf B (i+1) (m-1)) | imp_prf _ i _ = PBound i; fun all_prf (Const ("Pure.all", _) $ Abs (a, T, t)) = Abst (a, NONE (*T*), all_prf t) | all_prf t = imp_prf t (~i) m in all_prf t end; fun assumption_proof Bs Bi n prf = mk_AbsP Bs (proof_combP (prf, map PBound (length Bs - 1 downto 0) @ [mk_asm_prf Bi n ~1])); (* composition of object rule with proof state *) fun flatten_params_proof i j n (Const ("Pure.imp", _) $ A $ B, k) = AbsP ("H", NONE (*A*), flatten_params_proof (i+1) j n (B, k)) | flatten_params_proof i j n (Const ("Pure.all", _) $ Abs (a, T, t), k) = Abst (a, NONE (*T*), flatten_params_proof i (j+1) n (t, k)) | flatten_params_proof i j n (_, k) = proof_combP (proof_combt (PBound (k+i), map Bound (j-1 downto 0)), map PBound (remove (op =) (i-n) (i-1 downto 0))); fun bicompose_proof flatten Bs As A oldAs n m rprf sprf = let val lb = length Bs; val la = length As; in mk_AbsP (Bs @ As) (proof_combP (sprf, map PBound (lb + la - 1 downto la)) %% proof_combP (rprf, (if n>0 then [mk_asm_prf (the A) n m] else []) @ map (if flatten then flatten_params_proof 0 0 n else PBound o snd) (oldAs ~~ (la - 1 downto 0)))) end; (** type classes **) fun strip_shyps_proof algebra present witnessed extra_sorts prf = let fun get S2 (T, S1) = if Sorts.sort_le algebra (S1, S2) then SOME T else NONE; val extra = map (`Logic.dummy_tfree) extra_sorts; val replacements = present @ extra @ witnessed; fun replace T = if exists (fn (T', _) => T' = T) present then raise Same.SAME else (case get_first (get (Type.sort_of_atyp T)) replacements of SOME T' => T' | NONE => raise Fail "strip_shyps_proof: bad type variable in proof term"); in Same.commit (map_proof_types_same (Term_Subst.map_atypsT_same replace)) prf end; fun of_sort_proof algebra classrel_proof arity_proof hyps = Sorts.of_sort_derivation algebra {class_relation = fn _ => fn _ => fn (prf, c1) => fn c2 => if c1 = c2 then prf else classrel_proof (c1, c2) %% prf, type_constructor = fn (a, _) => fn dom => fn c => let val Ss = map (map snd) dom and prfs = maps (map fst) dom in proof_combP (arity_proof (a, Ss, c), prfs) end, type_variable = fn typ => map (fn c => (hyps (typ, c), c)) (Type.sort_of_atyp typ)}; (** axioms and theorems **) val add_type_variables = (fold_types o fold_atyps) (insert (op =)); fun type_variables_of t = rev (add_type_variables t []); val add_variables = fold_aterms (fn a => (is_Var a orelse is_Free a) ? insert (op =) a); fun variables_of t = rev (add_variables t []); fun test_args _ [] = true | test_args is (Bound i :: ts) = not (member (op =) is i) andalso test_args (i :: is) ts | test_args _ _ = false; fun is_fun (Type ("fun", _)) = true | is_fun (TVar _) = true | is_fun _ = false; fun vars_of t = map Var (rev (Term.add_vars t [])); fun add_funvars Ts (vs, t) = if is_fun (fastype_of1 (Ts, t)) then union (op =) vs (map_filter (fn Var (ixn, T) => if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t)) else vs; fun add_npvars q p Ts (vs, Const ("Pure.imp", _) $ t $ u) = add_npvars q p Ts (add_npvars q (not p) Ts (vs, t), u) | add_npvars q p Ts (vs, Const ("Pure.all", Type (_, [Type (_, [T, _]), _])) $ t) = add_npvars q p Ts (vs, if p andalso q then betapply (t, Var (("",0), T)) else t) | add_npvars q p Ts (vs, Abs (_, T, t)) = add_npvars q p (T::Ts) (vs, t) | add_npvars _ _ Ts (vs, t) = add_npvars' Ts (vs, t) and add_npvars' Ts (vs, t) = (case strip_comb t of (Var (ixn, _), ts) => if test_args [] ts then vs else Library.foldl (add_npvars' Ts) (AList.update (op =) (ixn, Library.foldl (add_funvars Ts) ((these ooo AList.lookup) (op =) vs ixn, ts)) vs, ts) | (Abs (_, T, u), ts) => Library.foldl (add_npvars' (T::Ts)) (vs, u :: ts) | (_, ts) => Library.foldl (add_npvars' Ts) (vs, ts)); fun prop_vars (Const ("Pure.imp", _) $ P $ Q) = union (op =) (prop_vars P) (prop_vars Q) | prop_vars (Const ("Pure.all", _) $ Abs (_, _, t)) = prop_vars t | prop_vars t = (case strip_comb t of (Var (ixn, _), _) => [ixn] | _ => []); fun is_proj t = let fun is_p i t = (case strip_comb t of (Bound _, []) => false | (Bound j, ts) => j >= i orelse exists (is_p i) ts | (Abs (_, _, u), _) => is_p (i+1) u | (_, ts) => exists (is_p i) ts) in (case strip_abs_body t of Bound _ => true | t' => is_p 0 t') end; fun prop_args prop = let val needed_vars = union (op =) (Library.foldl (uncurry (union (op =))) ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop)))) (prop_vars prop); in variables_of prop |> map (fn var as Var (ixn, _) => if member (op =) needed_vars ixn then SOME var else NONE | free => SOME free) end; fun const_proof mk name prop = let val args = prop_args prop; val ({outer_constraints, ...}, prop1) = Logic.unconstrainT [] prop; val head = mk (name, prop1, NONE); in proof_combP (proof_combt' (head, args), map OfClass outer_constraints) end; val axm_proof = const_proof PAxm; val oracle_proof = const_proof Oracle; val shrink_proof = let fun shrink ls lev (prf as Abst (a, T, body)) = let val (b, is, ch, body') = shrink ls (lev+1) body in (b, is, ch, if ch then Abst (a, T, body') else prf) end | shrink ls lev (prf as AbsP (a, t, body)) = let val (b, is, ch, body') = shrink (lev::ls) lev body in (b orelse member (op =) is 0, map_filter (fn 0 => NONE | i => SOME (i-1)) is, ch, if ch then AbsP (a, t, body') else prf) end | shrink ls lev prf = let val (is, ch, _, prf') = shrink' ls lev [] [] prf in (false, is, ch, prf') end and shrink' ls lev ts prfs (prf as prf1 %% prf2) = let val p as (_, is', ch', prf') = shrink ls lev prf2; val (is, ch, ts', prf'') = shrink' ls lev ts (p::prfs) prf1 in (union (op =) is is', ch orelse ch', ts', if ch orelse ch' then prf'' %% prf' else prf) end | shrink' ls lev ts prfs (prf as prf1 % t) = let val (is, ch, (ch', t')::ts', prf') = shrink' ls lev (t::ts) prfs prf1 in (is, ch orelse ch', ts', if ch orelse ch' then prf' % t' else prf) end | shrink' ls lev ts prfs (prf as PBound i) = (if exists (fn SOME (Bound j) => lev-j <= nth ls i | _ => true) ts orelse has_duplicates (op =) (Library.foldl (fn (js, SOME (Bound j)) => j :: js | (js, _) => js) ([], ts)) orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf) | shrink' _ _ ts _ (Hyp t) = ([], false, map (pair false) ts, Hyp t) | shrink' _ _ ts _ (prf as MinProof) = ([], false, map (pair false) ts, prf) | shrink' _ _ ts _ (prf as OfClass _) = ([], false, map (pair false) ts, prf) | shrink' _ _ ts prfs prf = let val prop = (case prf of PAxm (_, prop, _) => prop | Oracle (_, prop, _) => prop | PThm ({prop, ...}, _) => prop | _ => raise Fail "shrink: proof not in normal form"); val vs = vars_of prop; val (ts', ts'') = chop (length vs) ts; val insts = take (length ts') (map (fst o dest_Var) vs) ~~ ts'; val nvs = Library.foldl (fn (ixns', (ixn, ixns)) => insert (op =) ixn (case AList.lookup (op =) insts ixn of SOME (SOME t) => if is_proj t then union (op =) ixns ixns' else ixns' | _ => union (op =) ixns ixns')) (needed prop ts'' prfs, add_npvars false true [] ([], prop)); val insts' = map (fn (ixn, x as SOME _) => if member (op =) nvs ixn then (false, x) else (true, NONE) | (_, x) => (false, x)) insts in ([], false, insts' @ map (pair false) ts'', prf) end and needed (Const ("Pure.imp", _) $ t $ u) ts ((b, _, _, _)::prfs) = union (op =) (if b then map (fst o dest_Var) (vars_of t) else []) (needed u ts prfs) | needed (Var (ixn, _)) (_::_) _ = [ixn] | needed _ _ _ = []; in fn prf => #4 (shrink [] 0 prf) end; (** axioms for equality **) val aT = TFree ("'a", []); val bT = TFree ("'b", []); val x = Free ("x", aT); val y = Free ("y", aT); val z = Free ("z", aT); val A = Free ("A", propT); val B = Free ("B", propT); val f = Free ("f", aT --> bT); val g = Free ("g", aT --> bT); val equality_axms = [("reflexive", Logic.mk_equals (x, x)), ("symmetric", Logic.mk_implies (Logic.mk_equals (x, y), Logic.mk_equals (y, x))), ("transitive", Logic.list_implies ([Logic.mk_equals (x, y), Logic.mk_equals (y, z)], Logic.mk_equals (x, z))), ("equal_intr", Logic.list_implies ([Logic.mk_implies (A, B), Logic.mk_implies (B, A)], Logic.mk_equals (A, B))), ("equal_elim", Logic.list_implies ([Logic.mk_equals (A, B), A], B)), ("abstract_rule", Logic.mk_implies (Logic.all x (Logic.mk_equals (f $ x, g $ x)), Logic.mk_equals (lambda x (f $ x), lambda x (g $ x)))), ("combination", Logic.list_implies ([Logic.mk_equals (f, g), Logic.mk_equals (x, y)], Logic.mk_equals (f $ x, g $ y)))]; val [reflexive_axm, symmetric_axm, transitive_axm, equal_intr_axm, equal_elim_axm, abstract_rule_axm, combination_axm] = map (fn (s, t) => PAxm ("Pure." ^ s, Logic.varify_global t, NONE)) equality_axms; val reflexive_proof = reflexive_axm % NONE; val is_reflexive_proof = fn PAxm ("Pure.reflexive", _, _) % _ => true | _ => false; fun symmetric_proof prf = if is_reflexive_proof prf then prf else symmetric_axm % NONE % NONE %% prf; fun transitive_proof U u prf1 prf2 = if is_reflexive_proof prf1 then prf2 else if is_reflexive_proof prf2 then prf1 else if U = propT then transitive_axm % NONE % SOME (remove_types u) % NONE %% prf1 %% prf2 else transitive_axm % NONE % NONE % NONE %% prf1 %% prf2; fun equal_intr_proof A B prf1 prf2 = equal_intr_axm %> remove_types A %> remove_types B %% prf1 %% prf2; fun equal_elim_proof A B prf1 prf2 = equal_elim_axm %> remove_types A %> remove_types B %% prf1 %% prf2; fun abstract_rule_proof (a, x) prf = abstract_rule_axm % NONE % NONE %% forall_intr_proof (a, x) NONE prf; fun check_comb (PAxm ("Pure.combination", _, _) % f % _ % _ % _ %% prf %% _) = is_some f orelse check_comb prf | check_comb (PAxm ("Pure.transitive", _, _) % _ % _ % _ %% prf1 %% prf2) = check_comb prf1 andalso check_comb prf2 | check_comb (PAxm ("Pure.symmetric", _, _) % _ % _ %% prf) = check_comb prf | check_comb _ = false; fun combination_proof f g t u prf1 prf2 = let val f = Envir.beta_norm f; val g = Envir.beta_norm g; val prf = if check_comb prf1 then combination_axm % NONE % NONE else (case prf1 of PAxm ("Pure.reflexive", _, _) % _ => combination_axm %> remove_types f % NONE | _ => combination_axm %> remove_types f %> remove_types g) in prf % (case head_of f of Abs _ => SOME (remove_types t) | Var _ => SOME (remove_types t) | _ => NONE) % (case head_of g of Abs _ => SOME (remove_types u) | Var _ => SOME (remove_types u) | _ => NONE) %% prf1 %% prf2 end; (** rewriting on proof terms **) (* simple first order matching functions for terms and proofs (see pattern.ML) *) exception PMatch; fun flt (i: int) = filter (fn n => n < i); fun fomatch Ts tymatch j instsp p = let fun mtch (instsp as (tyinsts, insts)) = fn (Var (ixn, T), t) => if j>0 andalso not (null (flt j (loose_bnos t))) then raise PMatch else (tymatch (tyinsts, fn () => (T, fastype_of1 (Ts, t))), (ixn, t) :: insts) | (Free (a, T), Free (b, U)) => if a=b then (tymatch (tyinsts, K (T, U)), insts) else raise PMatch | (Const (a, T), Const (b, U)) => if a=b then (tymatch (tyinsts, K (T, U)), insts) else raise PMatch | (f $ t, g $ u) => mtch (mtch instsp (f, g)) (t, u) | (Bound i, Bound j) => if i=j then instsp else raise PMatch | _ => raise PMatch in mtch instsp (apply2 Envir.beta_eta_contract p) end; fun match_proof Ts tymatch = let fun optmatch _ inst (NONE, _) = inst | optmatch _ _ (SOME _, NONE) = raise PMatch | optmatch mtch inst (SOME x, SOME y) = mtch inst (x, y) fun matcht Ts j (pinst, tinst) (t, u) = (pinst, fomatch Ts tymatch j tinst (t, Envir.beta_norm u)); fun matchT (pinst, (tyinsts, insts)) p = (pinst, (tymatch (tyinsts, K p), insts)); fun matchTs inst (Ts, Us) = Library.foldl (uncurry matchT) (inst, Ts ~~ Us); fun mtch Ts i j (pinst, tinst) (Hyp (Var (ixn, _)), prf) = if i = 0 andalso j = 0 then ((ixn, prf) :: pinst, tinst) else (case apfst (flt i) (apsnd (flt j) (prf_add_loose_bnos 0 0 prf ([], []))) of ([], []) => ((ixn, incr_pboundvars (~i) (~j) prf) :: pinst, tinst) | ([], _) => if j = 0 then ((ixn, incr_pboundvars (~i) (~j) prf) :: pinst, tinst) else raise PMatch | _ => raise PMatch) | mtch Ts i j inst (prf1 % opt1, prf2 % opt2) = optmatch (matcht Ts j) (mtch Ts i j inst (prf1, prf2)) (opt1, opt2) | mtch Ts i j inst (prf1 %% prf2, prf1' %% prf2') = mtch Ts i j (mtch Ts i j inst (prf1, prf1')) (prf2, prf2') | mtch Ts i j inst (Abst (_, opT, prf1), Abst (_, opU, prf2)) = mtch (the_default dummyT opU :: Ts) i (j+1) (optmatch matchT inst (opT, opU)) (prf1, prf2) | mtch Ts i j inst (prf1, Abst (_, opU, prf2)) = mtch (the_default dummyT opU :: Ts) i (j+1) inst (incr_pboundvars 0 1 prf1 %> Bound 0, prf2) | mtch Ts i j inst (AbsP (_, opt, prf1), AbsP (_, opu, prf2)) = mtch Ts (i+1) j (optmatch (matcht Ts j) inst (opt, opu)) (prf1, prf2) | mtch Ts i j inst (prf1, AbsP (_, _, prf2)) = mtch Ts (i+1) j inst (incr_pboundvars 1 0 prf1 %% PBound 0, prf2) | mtch Ts i j inst (PAxm (s1, _, opTs), PAxm (s2, _, opUs)) = if s1 = s2 then optmatch matchTs inst (opTs, opUs) else raise PMatch | mtch Ts i j inst (OfClass (T1, c1), OfClass (T2, c2)) = if c1 = c2 then matchT inst (T1, T2) else raise PMatch | mtch Ts i j inst (PThm ({name = name1, prop = prop1, types = types1, ...}, _), PThm ({name = name2, prop = prop2, types = types2, ...}, _)) = if name1 = name2 andalso prop1 = prop2 then optmatch matchTs inst (types1, types2) else raise PMatch | mtch _ _ _ inst (PBound i, PBound j) = if i = j then inst else raise PMatch | mtch _ _ _ _ _ = raise PMatch in mtch Ts 0 0 end; fun prf_subst (pinst, (tyinsts, insts)) = let val substT = Envir.subst_type_same tyinsts; val substTs = Same.map substT; fun subst' lev (Var (xi, _)) = (case AList.lookup (op =) insts xi of NONE => raise Same.SAME | SOME u => incr_boundvars lev u) | subst' _ (Const (s, T)) = Const (s, substT T) | subst' _ (Free (s, T)) = Free (s, substT T) | subst' lev (Abs (a, T, body)) = (Abs (a, substT T, Same.commit (subst' (lev + 1)) body) handle Same.SAME => Abs (a, T, subst' (lev + 1) body)) | subst' lev (f $ t) = (subst' lev f $ Same.commit (subst' lev) t handle Same.SAME => f $ subst' lev t) | subst' _ _ = raise Same.SAME; fun subst plev tlev (AbsP (a, t, body)) = (AbsP (a, Same.map_option (subst' tlev) t, Same.commit (subst (plev + 1) tlev) body) handle Same.SAME => AbsP (a, t, subst (plev + 1) tlev body)) | subst plev tlev (Abst (a, T, body)) = (Abst (a, Same.map_option substT T, Same.commit (subst plev (tlev + 1)) body) handle Same.SAME => Abst (a, T, subst plev (tlev + 1) body)) | subst plev tlev (prf %% prf') = (subst plev tlev prf %% Same.commit (subst plev tlev) prf' handle Same.SAME => prf %% subst plev tlev prf') | subst plev tlev (prf % t) = (subst plev tlev prf % Same.commit (Same.map_option (subst' tlev)) t handle Same.SAME => prf % Same.map_option (subst' tlev) t) | subst plev tlev (Hyp (Var (xi, _))) = (case AList.lookup (op =) pinst xi of NONE => raise Same.SAME | SOME prf' => incr_pboundvars plev tlev prf') | subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Same.map_option substTs Ts) | subst _ _ (OfClass (T, c)) = OfClass (substT T, c) | subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Same.map_option substTs Ts) | subst _ _ (PThm ({serial = i, pos = p, theory_name, name = id, prop, types}, thm_body)) = PThm (thm_header i p theory_name id prop (Same.map_option substTs types), thm_body) | subst _ _ _ = raise Same.SAME; in fn t => subst 0 0 t handle Same.SAME => t end; (*A fast unification filter: true unless the two terms cannot be unified. Terms must be NORMAL. Treats all Vars as distinct. *) fun could_unify prf1 prf2 = let fun matchrands (prf1 %% prf2) (prf1' %% prf2') = could_unify prf2 prf2' andalso matchrands prf1 prf1' | matchrands (prf % SOME t) (prf' % SOME t') = Term.could_unify (t, t') andalso matchrands prf prf' | matchrands (prf % _) (prf' % _) = matchrands prf prf' | matchrands _ _ = true fun head_of (prf %% _) = head_of prf | head_of (prf % _) = head_of prf | head_of prf = prf in case (head_of prf1, head_of prf2) of (_, Hyp (Var _)) => true | (Hyp (Var _), _) => true | (PAxm (a, _, _), PAxm (b, _, _)) => a = b andalso matchrands prf1 prf2 | (OfClass (_, c), OfClass (_, d)) => c = d andalso matchrands prf1 prf2 | (PThm ({name = a, prop = propa, ...}, _), PThm ({name = b, prop = propb, ...}, _)) => a = b andalso propa = propb andalso matchrands prf1 prf2 | (PBound i, PBound j) => i = j andalso matchrands prf1 prf2 | (AbsP _, _) => true (*because of possible eta equality*) | (Abst _, _) => true | (_, AbsP _) => true | (_, Abst _) => true | _ => false end; (* rewrite proof *) val no_skel = PBound 0; val normal_skel = Hyp (Var ((Name.uu, 0), propT)); fun rewrite_prf tymatch (rules, procs) prf = let fun rew _ _ (Abst (_, _, body) % SOME t) = SOME (prf_subst_bounds [t] body, no_skel) | rew _ _ (AbsP (_, _, body) %% prf) = SOME (prf_subst_pbounds [prf] body, no_skel) | rew Ts hs prf = (case get_first (fn r => r Ts hs prf) procs of NONE => get_first (fn (prf1, prf2) => SOME (prf_subst (match_proof Ts tymatch ([], (Vartab.empty, [])) (prf1, prf)) prf2, prf2) handle PMatch => NONE) (filter (could_unify prf o fst) rules) | some => some); fun rew0 Ts hs (prf as AbsP (_, _, prf' %% PBound 0)) = if prf_loose_Pbvar1 prf' 0 then rew Ts hs prf else let val prf'' = incr_pboundvars (~1) 0 prf' in SOME (the_default (prf'', no_skel) (rew Ts hs prf'')) end | rew0 Ts hs (prf as Abst (_, _, prf' % SOME (Bound 0))) = if prf_loose_bvar1 prf' 0 then rew Ts hs prf else let val prf'' = incr_pboundvars 0 (~1) prf' in SOME (the_default (prf'', no_skel) (rew Ts hs prf'')) end | rew0 Ts hs prf = rew Ts hs prf; fun rew1 _ _ (Hyp (Var _)) _ = NONE | rew1 Ts hs skel prf = (case rew2 Ts hs skel prf of SOME prf1 => (case rew0 Ts hs prf1 of SOME (prf2, skel') => SOME (the_default prf2 (rew1 Ts hs skel' prf2)) | NONE => SOME prf1) | NONE => (case rew0 Ts hs prf of SOME (prf1, skel') => SOME (the_default prf1 (rew1 Ts hs skel' prf1)) | NONE => NONE)) and rew2 Ts hs skel (prf % SOME t) = (case prf of Abst (_, _, body) => let val prf' = prf_subst_bounds [t] body in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end | _ => (case rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf of SOME prf' => SOME (prf' % SOME t) | NONE => NONE)) | rew2 Ts hs skel (prf % NONE) = Option.map (fn prf' => prf' % NONE) (rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf) | rew2 Ts hs skel (prf1 %% prf2) = (case prf1 of AbsP (_, _, body) => let val prf' = prf_subst_pbounds [prf2] body in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end | _ => let val (skel1, skel2) = (case skel of skel1 %% skel2 => (skel1, skel2) | _ => (no_skel, no_skel)) in (case rew1 Ts hs skel1 prf1 of SOME prf1' => (case rew1 Ts hs skel2 prf2 of SOME prf2' => SOME (prf1' %% prf2') | NONE => SOME (prf1' %% prf2)) | NONE => (case rew1 Ts hs skel2 prf2 of SOME prf2' => SOME (prf1 %% prf2') | NONE => NONE)) end) | rew2 Ts hs skel (Abst (s, T, prf)) = (case rew1 (the_default dummyT T :: Ts) hs (case skel of Abst (_, _, skel') => skel' | _ => no_skel) prf of SOME prf' => SOME (Abst (s, T, prf')) | NONE => NONE) | rew2 Ts hs skel (AbsP (s, t, prf)) = (case rew1 Ts (t :: hs) (case skel of AbsP (_, _, skel') => skel' | _ => no_skel) prf of SOME prf' => SOME (AbsP (s, t, prf')) | NONE => NONE) | rew2 _ _ _ _ = NONE; in the_default prf (rew1 [] [] no_skel prf) end; fun rewrite_proof thy = rewrite_prf (fn (tyenv, f) => Sign.typ_match thy (f ()) tyenv handle Type.TYPE_MATCH => raise PMatch); fun rewrite_proof_notypes rews = rewrite_prf fst rews; (* theory data *) structure Data = Theory_Data ( type T = ((stamp * (proof * proof)) list * (stamp * (typ list -> term option list -> proof -> (proof * proof) option)) list) * (theory -> proof -> proof) option; val empty = (([], []), NONE); val extend = I; fun merge (((rules1, procs1), preproc1), ((rules2, procs2), preproc2)) : T = ((AList.merge (op =) (K true) (rules1, rules2), AList.merge (op =) (K true) (procs1, procs2)), merge_options (preproc1, preproc2)); ); fun get_rew_data thy = let val (rules, procs) = #1 (Data.get thy) in (map #2 rules, map #2 procs) end; fun rew_proof thy = rewrite_prf fst (get_rew_data thy); fun add_prf_rrule r = (Data.map o apfst o apfst) (cons (stamp (), r)); fun add_prf_rproc p = (Data.map o apfst o apsnd) (cons (stamp (), p)); fun set_preproc f = (Data.map o apsnd) (K (SOME f)); fun apply_preproc thy = (case #2 (Data.get thy) of NONE => I | SOME f => f thy); (** reconstruction of partial proof terms **) fun forall_intr_variables_term prop = fold_rev Logic.all (variables_of prop) prop; fun forall_intr_variables prop prf = fold_rev forall_intr_proof' (variables_of prop) prf; local fun app_types shift prop Ts prf = let val inst = type_variables_of prop ~~ Ts; fun subst_same A = (case AList.lookup (op =) inst A of SOME T => T | NONE => raise Same.SAME); val subst_type_same = Term_Subst.map_atypsT_same (fn TVar ((a, i), S) => subst_same (TVar ((a, i - shift), S)) | A => subst_same A); in Same.commit (map_proof_types_same subst_type_same) prf end; fun guess_name (PThm ({name, ...}, _)) = name | guess_name (prf %% Hyp _) = guess_name prf | guess_name (prf %% OfClass _) = guess_name prf | guess_name (prf % NONE) = guess_name prf | guess_name (prf % SOME (Var _)) = guess_name prf | guess_name _ = ""; (* generate constraints for proof term *) fun mk_var env Ts T = let val (env', v) = Envir.genvar "a" (env, rev Ts ---> T) in (list_comb (v, map Bound (length Ts - 1 downto 0)), env') end; fun mk_tvar S (Envir.Envir {maxidx, tenv, tyenv}) = (TVar (("'t", maxidx + 1), S), Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}); val mk_abs = fold (fn T => fn u => Abs ("", T, u)); fun unifyT thy env T U = let val Envir.Envir {maxidx, tenv, tyenv} = env; val (tyenv', maxidx') = Sign.typ_unify thy (T, U) (tyenv, maxidx); in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end; fun chaseT env (T as TVar v) = (case Type.lookup (Envir.type_env env) v of NONE => T | SOME T' => chaseT env T') | chaseT _ T = T; fun infer_type thy (env as Envir.Envir {maxidx, tenv, tyenv}) _ vTs (t as Const (s, T)) = if T = dummyT then (case Sign.const_type thy s of NONE => error ("reconstruct_proof: No such constant: " ^ quote s) | SOME T => let val T' = Type.strip_sorts (Logic.incr_tvar (maxidx + 1) T) in (Const (s, T'), T', vTs, Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}) end) else (t, T, vTs, env) | infer_type _ env _ vTs (t as Free (s, T)) = if T = dummyT then (case Symtab.lookup vTs s of NONE => let val (T, env') = mk_tvar [] env in (Free (s, T), T, Symtab.update_new (s, T) vTs, env') end | SOME T => (Free (s, T), T, vTs, env)) else (t, T, vTs, env) | infer_type _ _ _ _ (Var _) = error "reconstruct_proof: internal error" | infer_type thy env Ts vTs (Abs (s, T, t)) = let val (T', env') = if T = dummyT then mk_tvar [] env else (T, env); val (t', U, vTs', env'') = infer_type thy env' (T' :: Ts) vTs t in (Abs (s, T', t'), T' --> U, vTs', env'') end | infer_type thy env Ts vTs (t $ u) = let val (t', T, vTs1, env1) = infer_type thy env Ts vTs t; val (u', U, vTs2, env2) = infer_type thy env1 Ts vTs1 u; in (case chaseT env2 T of Type ("fun", [U', V]) => (t' $ u', V, vTs2, unifyT thy env2 U U') | _ => let val (V, env3) = mk_tvar [] env2 in (t' $ u', V, vTs2, unifyT thy env3 T (U --> V)) end) end | infer_type _ env Ts vTs (t as Bound i) = ((t, nth Ts i, vTs, env) handle General.Subscript => error ("infer_type: bad variable index " ^ string_of_int i)); fun cantunify thy (t, u) = error ("Non-unifiable terms:\n" ^ Syntax.string_of_term_global thy t ^ "\n\n" ^ Syntax.string_of_term_global thy u); fun decompose thy Ts (p as (t, u)) env = let fun rigrig (a, T) (b, U) uT ts us = if a <> b then cantunify thy p else apfst flat (fold_map (decompose thy Ts) (ts ~~ us) (uT env T U)) in case apply2 (strip_comb o Envir.head_norm env) p of ((Const c, ts), (Const d, us)) => rigrig c d (unifyT thy) ts us | ((Free c, ts), (Free d, us)) => rigrig c d (unifyT thy) ts us | ((Bound i, ts), (Bound j, us)) => rigrig (i, dummyT) (j, dummyT) (K o K) ts us | ((Abs (_, T, t), []), (Abs (_, U, u), [])) => decompose thy (T::Ts) (t, u) (unifyT thy env T U) | ((Abs (_, T, t), []), _) => decompose thy (T::Ts) (t, incr_boundvars 1 u $ Bound 0) env | (_, (Abs (_, T, u), [])) => decompose thy (T::Ts) (incr_boundvars 1 t $ Bound 0, u) env | _ => ([(mk_abs Ts t, mk_abs Ts u)], env) end; fun make_constraints_cprf thy env cprf = let fun add_cnstrt Ts prop prf cs env vTs (t, u) = let val t' = mk_abs Ts t; val u' = mk_abs Ts u in (prop, prf, cs, Pattern.unify (Context.Theory thy) (t', u') env, vTs) handle Pattern.Pattern => let val (cs', env') = decompose thy [] (t', u') env in (prop, prf, cs @ cs', env', vTs) end | Pattern.Unif => cantunify thy (Envir.norm_term env t', Envir.norm_term env u') end; fun mk_cnstrts_atom env vTs prop opTs prf = let val prop_types = type_variables_of prop; val (Ts, env') = (case opTs of NONE => fold_map (mk_tvar o Type.sort_of_atyp) prop_types env | SOME Ts => (Ts, env)); val prop' = subst_atomic_types (prop_types ~~ Ts) (forall_intr_variables_term prop) handle ListPair.UnequalLengths => error ("Wrong number of type arguments for " ^ quote (guess_name prf)) in (prop', change_types (SOME Ts) prf, [], env', vTs) end; fun head_norm (prop, prf, cnstrts, env, vTs) = (Envir.head_norm env prop, prf, cnstrts, env, vTs); fun mk_cnstrts env _ Hs vTs (PBound i) = ((nth Hs i, PBound i, [], env, vTs) handle General.Subscript => error ("mk_cnstrts: bad variable index " ^ string_of_int i)) | mk_cnstrts env Ts Hs vTs (Abst (s, opT, cprf)) = let val (T, env') = (case opT of NONE => mk_tvar [] env | SOME T => (T, env)); val (t, prf, cnstrts, env'', vTs') = mk_cnstrts env' (T::Ts) (map (incr_boundvars 1) Hs) vTs cprf; in (Const ("Pure.all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, SOME T, prf), cnstrts, env'', vTs') end | mk_cnstrts env Ts Hs vTs (AbsP (s, SOME t, cprf)) = let val (t', _, vTs', env') = infer_type thy env Ts vTs t; val (u, prf, cnstrts, env'', vTs'') = mk_cnstrts env' Ts (t'::Hs) vTs' cprf; in (Logic.mk_implies (t', u), AbsP (s, SOME t', prf), cnstrts, env'', vTs'') end | mk_cnstrts env Ts Hs vTs (AbsP (s, NONE, cprf)) = let val (t, env') = mk_var env Ts propT; val (u, prf, cnstrts, env'', vTs') = mk_cnstrts env' Ts (t::Hs) vTs cprf; in (Logic.mk_implies (t, u), AbsP (s, SOME t, prf), cnstrts, env'', vTs') end | mk_cnstrts env Ts Hs vTs (cprf1 %% cprf2) = let val (u, prf2, cnstrts, env', vTs') = mk_cnstrts env Ts Hs vTs cprf2 in (case head_norm (mk_cnstrts env' Ts Hs vTs' cprf1) of (Const ("Pure.imp", _) $ u' $ t', prf1, cnstrts', env'', vTs'') => add_cnstrt Ts t' (prf1 %% prf2) (cnstrts' @ cnstrts) env'' vTs'' (u, u') | (t, prf1, cnstrts', env'', vTs'') => let val (v, env''') = mk_var env'' Ts propT in add_cnstrt Ts v (prf1 %% prf2) (cnstrts' @ cnstrts) env''' vTs'' (t, Logic.mk_implies (u, v)) end) end | mk_cnstrts env Ts Hs vTs (cprf % SOME t) = let val (t', U, vTs1, env1) = infer_type thy env Ts vTs t in (case head_norm (mk_cnstrts env1 Ts Hs vTs1 cprf) of (Const ("Pure.all", Type ("fun", [Type ("fun", [T, _]), _])) $ f, prf, cnstrts, env2, vTs2) => let val env3 = unifyT thy env2 T U in (betapply (f, t'), prf % SOME t', cnstrts, env3, vTs2) end | (u, prf, cnstrts, env2, vTs2) => let val (v, env3) = mk_var env2 Ts (U --> propT); in add_cnstrt Ts (v $ t') (prf % SOME t') cnstrts env3 vTs2 (u, Const ("Pure.all", (U --> propT) --> propT) $ v) end) end | mk_cnstrts env Ts Hs vTs (cprf % NONE) = (case head_norm (mk_cnstrts env Ts Hs vTs cprf) of (Const ("Pure.all", Type ("fun", [Type ("fun", [T, _]), _])) $ f, prf, cnstrts, env', vTs') => let val (t, env'') = mk_var env' Ts T in (betapply (f, t), prf % SOME t, cnstrts, env'', vTs') end | (u, prf, cnstrts, env', vTs') => let val (T, env1) = mk_tvar [] env'; val (v, env2) = mk_var env1 Ts (T --> propT); val (t, env3) = mk_var env2 Ts T in add_cnstrt Ts (v $ t) (prf % SOME t) cnstrts env3 vTs' (u, Const ("Pure.all", (T --> propT) --> propT) $ v) end) | mk_cnstrts env _ _ vTs (prf as PThm ({prop, types = opTs, ...}, _)) = mk_cnstrts_atom env vTs prop opTs prf | mk_cnstrts env _ _ vTs (prf as PAxm (_, prop, opTs)) = mk_cnstrts_atom env vTs prop opTs prf | mk_cnstrts env _ _ vTs (prf as OfClass (T, c)) = mk_cnstrts_atom env vTs (Logic.mk_of_class (T, c)) NONE prf | mk_cnstrts env _ _ vTs (prf as Oracle (_, prop, opTs)) = mk_cnstrts_atom env vTs prop opTs prf | mk_cnstrts env _ _ vTs (Hyp t) = (t, Hyp t, [], env, vTs) | mk_cnstrts _ _ _ _ MinProof = raise MIN_PROOF () in mk_cnstrts env [] [] Symtab.empty cprf end; (* update list of free variables of constraints *) fun upd_constrs env cs = let val tenv = Envir.term_env env; val tyenv = Envir.type_env env; val dom = [] |> Vartab.fold (cons o #1) tenv |> Vartab.fold (cons o #1) tyenv; val vran = [] |> Vartab.fold (Term.add_var_names o #2 o #2) tenv |> Vartab.fold (Term.add_tvar_namesT o #2 o #2) tyenv; fun check_cs [] = [] | check_cs ((u, p, vs) :: ps) = let val vs' = subtract (op =) dom vs in if vs = vs' then (u, p, vs) :: check_cs ps else (true, p, fold (insert op =) vs' vran) :: check_cs ps end; in check_cs cs end; (* solution of constraints *) fun solve _ [] bigenv = bigenv | solve thy cs bigenv = let fun search _ [] = error ("Unsolvable constraints:\n" ^ Pretty.string_of (Pretty.chunks (map (fn (_, p, _) => Syntax.pretty_flexpair (Syntax.init_pretty_global thy) (apply2 (Envir.norm_term bigenv) p)) cs))) | search env ((u, p as (t1, t2), vs)::ps) = if u then let val tn1 = Envir.norm_term bigenv t1; val tn2 = Envir.norm_term bigenv t2 in if Pattern.pattern tn1 andalso Pattern.pattern tn2 then (Pattern.unify (Context.Theory thy) (tn1, tn2) env, ps) handle Pattern.Unif => cantunify thy (tn1, tn2) else let val (cs', env') = decompose thy [] (tn1, tn2) env in if cs' = [(tn1, tn2)] then apsnd (cons (false, (tn1, tn2), vs)) (search env ps) else search env' (map (fn q => (true, q, vs)) cs' @ ps) end end else apsnd (cons (false, p, vs)) (search env ps); val Envir.Envir {maxidx, ...} = bigenv; val (env, cs') = search (Envir.empty maxidx) cs; in solve thy (upd_constrs env cs') (Envir.merge (bigenv, env)) end; in (* reconstruction of proofs *) fun reconstruct_proof thy prop cprf = let val (cprf' % SOME prop', thawf) = freeze_thaw_prf (cprf % SOME prop); val (t, prf, cs, env, _) = make_constraints_cprf thy (Envir.empty (maxidx_proof cprf ~1)) cprf'; val cs' = map (apply2 (Envir.norm_term env)) ((t, prop') :: cs) |> map (fn p => (true, p, Term.add_var_names (#1 p) (Term.add_var_names (#2 p) []))); val env' = solve thy cs' env in thawf (norm_proof env' prf) end handle MIN_PROOF () => MinProof; fun prop_of_atom prop Ts = subst_atomic_types (type_variables_of prop ~~ Ts) (forall_intr_variables_term prop); val head_norm = Envir.head_norm Envir.init; fun prop_of0 Hs (PBound i) = nth Hs i | prop_of0 Hs (Abst (s, SOME T, prf)) = Logic.all_const T $ (Abs (s, T, prop_of0 Hs prf)) | prop_of0 Hs (AbsP (_, SOME t, prf)) = Logic.mk_implies (t, prop_of0 (t :: Hs) prf) | prop_of0 Hs (prf % SOME t) = (case head_norm (prop_of0 Hs prf) of Const ("Pure.all", _) $ f => f $ t | _ => error "prop_of: all expected") | prop_of0 Hs (prf1 %% _) = (case head_norm (prop_of0 Hs prf1) of Const ("Pure.imp", _) $ _ $ Q => Q | _ => error "prop_of: ==> expected") | prop_of0 _ (Hyp t) = t | prop_of0 _ (PThm ({prop, types = SOME Ts, ...}, _)) = prop_of_atom prop Ts | prop_of0 _ (PAxm (_, prop, SOME Ts)) = prop_of_atom prop Ts | prop_of0 _ (OfClass (T, c)) = Logic.mk_of_class (T, c) | prop_of0 _ (Oracle (_, prop, SOME Ts)) = prop_of_atom prop Ts | prop_of0 _ _ = error "prop_of: partial proof object"; val prop_of' = Envir.beta_eta_contract oo prop_of0; val prop_of = prop_of' []; (* expand and reconstruct subproofs *) fun expand_name_empty (header: thm_header) = if #name header = "" then SOME "" else NONE; fun expand_proof thy expand_name prf = let fun expand seen maxidx (AbsP (s, t, prf)) = let val (seen', maxidx', prf') = expand seen maxidx prf in (seen', maxidx', AbsP (s, t, prf')) end | expand seen maxidx (Abst (s, T, prf)) = let val (seen', maxidx', prf') = expand seen maxidx prf in (seen', maxidx', Abst (s, T, prf')) end | expand seen maxidx (prf1 %% prf2) = let val (seen', maxidx', prf1') = expand seen maxidx prf1; val (seen'', maxidx'', prf2') = expand seen' maxidx' prf2; in (seen'', maxidx'', prf1' %% prf2') end | expand seen maxidx (prf % t) = let val (seen', maxidx', prf') = expand seen maxidx prf in (seen', maxidx', prf' % t) end | expand seen maxidx (prf as PThm (header, thm_body)) = let val {serial, pos, theory_name, name, prop, types} = header in (case expand_name header of SOME name' => if name' = "" andalso is_some types then let val (seen', maxidx', prf') = (case Inttab.lookup seen serial of NONE => let val prf1 = thm_body_proof_open thm_body |> reconstruct_proof thy prop |> forall_intr_variables prop; val (seen1, maxidx1, prf2) = expand_init seen prf1 val seen2 = seen1 |> Inttab.update (serial, (maxidx1, prf2)); in (seen2, maxidx1, prf2) end | SOME (maxidx1, prf1) => (seen, maxidx1, prf1)); val prf'' = prf' |> incr_indexes (maxidx + 1) |> app_types (maxidx + 1) prop (the types); in (seen', maxidx' + maxidx + 1, prf'') end else if name' <> name then (seen, maxidx, PThm (thm_header serial pos theory_name name' prop types, thm_body)) else (seen, maxidx, prf) | NONE => (seen, maxidx, prf)) end | expand seen maxidx prf = (seen, maxidx, prf) and expand_init seen prf = expand seen (maxidx_proof prf ~1) prf; in #3 (expand_init Inttab.empty prf) end; end; (** promises **) fun fulfill_norm_proof thy ps body0 = let val _ = consolidate (map #2 ps @ [body0]); val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0; val oracles = unions_oracles (fold (fn (_, PBody {oracles, ...}) => not (null oracles) ? cons oracles) ps [oracles0]); val thms = unions_thms (fold (fn (_, PBody {thms, ...}) => not (null thms) ? cons thms) ps [thms0]); val proof = rew_proof thy proof0; in PBody {oracles = oracles, thms = thms, proof = proof} end; fun fulfill_proof_future thy promises (postproc: proof_body -> proof_body) body = let fun fulfill () = postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)); in if null promises then Future.map postproc body else if Future.is_finished body andalso length promises = 1 then Future.map (fn _ => fulfill ()) (snd (hd promises)) else (singleton o Future.forks) {name = "Proofterm.fulfill_proof_future", group = NONE, deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 1, interrupts = true} fulfill end; (** theorems **) (* standardization of variables for export: only frees and named bounds *) local val declare_names_term = Term.declare_term_frees; val declare_names_term' = fn SOME t => declare_names_term t | NONE => I; val declare_names_proof = fold_proof_terms declare_names_term; fun variant names bs x = #1 (Name.variant x (fold Name.declare bs names)); fun variant_term bs (Abs (x, T, t)) = let val x' = variant (declare_names_term t Name.context) bs x; val t' = variant_term (x' :: bs) t; in Abs (x', T, t') end | variant_term bs (t $ u) = variant_term bs t $ variant_term bs u | variant_term _ t = t; fun variant_proof bs (Abst (x, T, prf)) = let val x' = variant (declare_names_proof prf Name.context) bs x; val prf' = variant_proof (x' :: bs) prf; in Abst (x', T, prf') end | variant_proof bs (AbsP (x, t, prf)) = let val x' = variant (declare_names_term' t (declare_names_proof prf Name.context)) bs x; val t' = Option.map (variant_term bs) t; val prf' = variant_proof (x' :: bs) prf; in AbsP (x', t', prf') end | variant_proof bs (prf % t) = variant_proof bs prf % Option.map (variant_term bs) t | variant_proof bs (prf1 %% prf2) = variant_proof bs prf1 %% variant_proof bs prf2 | variant_proof bs (Hyp t) = Hyp (variant_term bs t) | variant_proof _ prf = prf; val used_frees_type = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I); fun used_frees_term t = fold_types used_frees_type t #> Term.declare_term_frees t; val used_frees_proof = fold_proof_terms_types used_frees_term used_frees_type; val unvarifyT = Term.map_atyps (fn TVar ((a, _), S) => TFree (a, S) | T => T); val unvarify = Term.map_aterms (fn Var ((x, _), T) => Free (x, T) | t => t) #> map_types unvarifyT; val unvarify_proof = map_proof_terms unvarify unvarifyT; fun hidden_types prop proof = let val visible = (fold_types o fold_atyps) (insert (op =)) prop []; val add_hiddenT = fold_atyps (fn T => not (member (op =) visible T) ? insert (op =) T); in rev (fold_proof_terms_types (fold_types add_hiddenT) add_hiddenT proof []) end; fun standard_hidden_types term proof = let val hidden = hidden_types term proof; val idx = Term.maxidx_term term (maxidx_proof proof ~1) + 1; fun smash T = if member (op =) hidden T then TVar (("'", idx), Type.sort_of_atyp T) else T; val smashT = map_atyps smash; in map_proof_terms (map_types smashT) smashT proof end; fun standard_hidden_terms term proof = let fun add_not excl x = ((is_Free x orelse is_Var x) andalso not (member (op =) excl x)) ? insert (op =) x; val visible = fold_aterms (add_not []) term []; val hidden = fold_proof_terms (fold_aterms (add_not visible)) proof []; val dummy_term = Term.map_aterms (fn x => if member (op =) hidden x then Term.dummy_pattern (Term.fastype_of x) else x); in proof |> not (null hidden) ? map_proof_terms dummy_term I end; in fun standard_vars used (term, opt_proof) = let val proofs = opt_proof |> Option.map (standard_hidden_types term #> standard_hidden_terms term) |> the_list; val proof_terms = rev (fold (fold_proof_terms_types cons (cons o Logic.mk_type)) proofs []); val used_frees = used |> used_frees_term term |> fold used_frees_proof proofs; val inst = Term_Subst.zero_var_indexes_inst used_frees (term :: proof_terms); val term' = term |> Term_Subst.instantiate inst |> unvarify |> variant_term []; val proofs' = proofs |> map (instantiate inst #> unvarify_proof #> variant_proof []); in (term', try hd proofs') end; fun standard_vars_term used t = #1 (standard_vars used (t, NONE)); val add_standard_vars_term = fold_aterms (fn Free (x, T) => (fn env => (case AList.lookup (op =) env x of NONE => (x, T) :: env | SOME T' => if T = T' then env else raise TYPE ("standard_vars_env: type conflict for variable " ^ quote x, [T, T'], []))) | _ => I); val add_standard_vars = fold_proof_terms add_standard_vars_term; end; (* PThm nodes *) fun export_enabled () = Options.default_bool "export_proofs"; fun export_standard_enabled () = Options.default_bool "export_standard_proofs"; fun export_proof_boxes_required thy = Context.theory_name thy = Context.PureN orelse (export_enabled () andalso not (export_standard_enabled ())); fun export_proof_boxes proofs = let fun export_boxes (AbsP (_, _, prf)) = export_boxes prf | export_boxes (Abst (_, _, prf)) = export_boxes prf | export_boxes (prf1 %% prf2) = export_boxes prf1 #> export_boxes prf2 | export_boxes (prf % _) = export_boxes prf | export_boxes (PThm ({serial = i, ...}, thm_body)) = (fn boxes => if Inttab.defined boxes i then boxes else let val prf' = thm_body_proof_raw thm_body; val export = thm_body_export_proof thm_body; val boxes' = boxes |> not (Lazy.is_finished export) ? Inttab.update (i, export); in export_boxes prf' boxes' end) | export_boxes _ = I; val boxes = (proofs, Inttab.empty) |-> fold export_boxes |> Inttab.dest; in List.app (Lazy.force o #2) boxes end; local fun unconstrainT_proof algebra classrel_proof arity_proof (ucontext: Logic.unconstrain_context) = let fun hyp_map hyp = (case AList.lookup (op =) (#constraints ucontext) hyp of SOME t => Hyp t | NONE => raise Fail "unconstrainT_proof: missing constraint"); val typ = Term_Subst.map_atypsT_same (Type.strip_sorts o #atyp_map ucontext); fun ofclass (ty, c) = let val ty' = Term.map_atyps (#atyp_map ucontext) ty; in the_single (of_sort_proof algebra classrel_proof arity_proof hyp_map (ty', [c])) end; in Same.commit (map_proof_same (Term_Subst.map_types_same typ) typ ofclass) #> fold_rev (implies_intr_proof o snd) (#constraints ucontext) end; fun export_proof thy i prop prf0 = let val prf = prf0 |> reconstruct_proof thy prop |> apply_preproc thy; val (prop', SOME prf') = (prop, SOME prf) |> standard_vars Name.context; val args = [] |> add_standard_vars_term prop' |> add_standard_vars prf' |> rev; val typargs = [] |> Term.add_tfrees prop' |> fold_proof_terms Term.add_tfrees prf' |> rev; val consts = Sign.consts_of thy; val xml = (typargs, (args, (prop', no_thm_names prf'))) |> let open XML.Encode Term_XML.Encode; val encode_vars = list (pair string typ); val encode_term = encode_standard_term consts; val encode_proof = encode_standard_proof consts; in pair (list (pair string sort)) (pair encode_vars (pair encode_term encode_proof)) end; in - YXML.chunks_of_body xml |> Export.export_params + Export.export_params {theory = thy, binding = Path.binding0 (Path.make ["proofs", string_of_int i]), executable = false, compress = true, - strict = false} + strict = false} xml end; fun export thy i prop prf = if export_enabled () then let val _ = export_proof_boxes [prf]; val _ = export_proof thy i prop prf; in () end else (); fun prune proof = if Options.default_bool "prune_proofs" then MinProof else proof; fun prepare_thm_proof unconstrain thy classrel_proof arity_proof (name, pos) shyps hyps concl promises body = let val named = name <> ""; val prop = Logic.list_implies (hyps, concl); val args = prop_args prop; val (ucontext, prop1) = Logic.unconstrainT shyps prop; val PBody {oracles = oracles0, thms = thms0, proof = prf} = body; val body0 = Future.value (PBody {oracles = oracles0, thms = thms0, proof = if proofs_enabled () then fold_rev implies_intr_proof hyps prf else MinProof}); fun publish i = map_proof_of (rew_proof thy #> tap (export thy i prop1) #> prune); val open_proof = not named ? rew_proof thy; fun new_prf () = let val i = serial (); val unconstrainT = unconstrainT_proof (Sign.classes_of thy) classrel_proof arity_proof ucontext; val postproc = map_proof_of unconstrainT #> named ? publish i; in (i, fulfill_proof_future thy promises postproc body0) end; val (i, body') = (*non-deterministic, depends on unknown promises*) (case strip_combt (fst (strip_combP prf)) of (PThm ({serial = ser, name = a, prop = prop', types = NONE, ...}, thm_body'), args') => if (a = "" orelse a = name) andalso prop' = prop1 andalso args' = args then let val Thm_Body {body = body', ...} = thm_body'; val i = if a = "" andalso named then serial () else ser; in (i, body' |> ser <> i ? Future.map (publish i)) end else new_prf () | _ => new_prf ()); val export_proof = if named orelse not (export_enabled ()) then no_export_proof else Lazy.lazy (fn () => join_proof body' |> open_proof |> export_proof thy i prop1 handle exn => if Exn.is_interrupt exn then raise Fail ("Interrupt: potential resource problems while exporting proof " ^ string_of_int i) else Exn.reraise exn); val theory_name = Context.theory_long_name thy; val thm = (i, make_thm_node theory_name name prop1 body'); val header = thm_header i ([pos, Position.thread_data ()]) theory_name name prop1 NONE; val thm_body = Thm_Body {export_proof = export_proof, open_proof = open_proof, body = body'}; val head = PThm (header, thm_body); val proof = if unconstrain then proof_combt' (head, (map o Option.map o Term.map_types) (#map_atyps ucontext) args) else proof_combP (proof_combt' (head, args), map OfClass (#outer_constraints ucontext) @ map Hyp hyps); in (thm, proof) end; in fun thm_proof thy = prepare_thm_proof false thy; fun unconstrain_thm_proof thy classrel_proof arity_proof shyps concl promises body = prepare_thm_proof true thy classrel_proof arity_proof ("", Position.none) shyps [] concl promises body; end; (* PThm identity *) fun get_identity shyps hyps prop prf = let val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)) in (case fst (strip_combt (fst (strip_combP prf))) of PThm ({serial, theory_name, name, prop = prop', ...}, _) => if prop = prop' then SOME {serial = serial, theory_name = theory_name, name = name} else NONE | _ => NONE) end; fun get_approximative_name shyps hyps prop prf = Option.map #name (get_identity shyps hyps prop prf) |> the_default ""; (* thm_id *) type thm_id = {serial: serial, theory_name: string}; fun make_thm_id (serial, theory_name) : thm_id = {serial = serial, theory_name = theory_name}; fun thm_header_id ({serial, theory_name, ...}: thm_header) = make_thm_id (serial, theory_name); fun thm_id (serial, thm_node) : thm_id = make_thm_id (serial, thm_node_theory_name thm_node); fun get_id shyps hyps prop prf : thm_id option = (case get_identity shyps hyps prop prf of NONE => NONE | SOME {name = "", ...} => NONE | SOME {serial, theory_name, ...} => SOME (make_thm_id (serial, theory_name))); fun this_id NONE _ = false | this_id (SOME (thm_id: thm_id)) (thm_id': thm_id) = #serial thm_id = #serial thm_id'; (* proof boxes: intermediate PThm nodes *) fun proof_boxes {included, excluded} proofs = let fun boxes_of (Abst (_, _, prf)) = boxes_of prf | boxes_of (AbsP (_, _, prf)) = boxes_of prf | boxes_of (prf % _) = boxes_of prf | boxes_of (prf1 %% prf2) = boxes_of prf1 #> boxes_of prf2 | boxes_of (PThm (header as {serial = i, ...}, thm_body)) = (fn boxes => let val thm_id = thm_header_id header in if Inttab.defined boxes i orelse (excluded thm_id andalso not (included thm_id)) then boxes else let val prf' = thm_body_proof_open thm_body; val boxes' = Inttab.update (i, (header, prf')) boxes; in boxes_of prf' boxes' end end) | boxes_of MinProof = raise MIN_PROOF () | boxes_of _ = I; in Inttab.fold_rev (cons o #2) (fold boxes_of proofs Inttab.empty) [] end; end; structure Basic_Proofterm = struct datatype proof = datatype Proofterm.proof datatype proof_body = datatype Proofterm.proof_body val op %> = Proofterm.%> end; open Basic_Proofterm; diff --git a/src/Tools/Code/code_target.ML b/src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML +++ b/src/Tools/Code/code_target.ML @@ -1,783 +1,783 @@ (* Title: Tools/Code/code_target.ML Author: Florian Haftmann, TU Muenchen Generic infrastructure for target language data. *) signature CODE_TARGET = sig val cert_tyco: Proof.context -> string -> string val read_tyco: Proof.context -> string -> string datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list; val next_export: theory -> string * theory val export_code_for: ({physical: bool} * (Path.T * Position.T)) option -> string -> string -> int option -> Token.T list -> Code_Thingol.program -> bool -> Code_Symbol.T list -> local_theory -> local_theory val produce_code_for: Proof.context -> string -> string -> int option -> Token.T list -> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string list * string) list * string option list val present_code_for: Proof.context -> string -> string -> int option -> Token.T list -> Code_Thingol.program -> Code_Symbol.T list * Code_Symbol.T list -> string val check_code_for: string -> bool -> Token.T list -> Code_Thingol.program -> bool -> Code_Symbol.T list -> local_theory -> local_theory val export_code: bool -> string list -> (((string * string) * ({physical: bool} * (Path.T * Position.T)) option) * Token.T list) list -> local_theory -> local_theory val export_code_cmd: bool -> string list -> (((string * string) * ({physical: bool} * (string * Position.T)) option) * Token.T list) list -> local_theory -> local_theory val produce_code: Proof.context -> bool -> string list -> string -> string -> int option -> Token.T list -> (string list * string) list * string option list val present_code: Proof.context -> string list -> Code_Symbol.T list -> string -> string -> int option -> Token.T list -> string val check_code: bool -> string list -> ((string * bool) * Token.T list) list -> local_theory -> local_theory val codeN: string val generatedN: string val code_path: Path.T -> Path.T val code_export_message: theory -> unit val export: Path.binding -> string -> theory -> theory val compilation_text: Proof.context -> string -> Code_Thingol.program -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm -> (string list * string) list * string val compilation_text': Proof.context -> string -> string option -> Code_Thingol.program -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm -> ((string list * string) list * string) * (Code_Symbol.T -> string option) type serializer type literals = Code_Printer.literals type language type ancestry val assert_target: theory -> string -> string val add_language: string * language -> theory -> theory val add_derived_target: string * ancestry -> theory -> theory val the_literals: Proof.context -> string -> literals val parse_args: 'a parser -> Token.T list -> 'a val default_code_width: int Config.T type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl val set_identifiers: (string, string, string, string, string, string) symbol_attr_decl -> theory -> theory val set_printings: (Code_Printer.raw_const_syntax, Code_Printer.tyco_syntax, string, unit, unit, string * Code_Symbol.T list) symbol_attr_decl -> theory -> theory val add_reserved: string -> string -> theory -> theory end; structure Code_Target : CODE_TARGET = struct open Basic_Code_Symbol; open Basic_Code_Thingol; type literals = Code_Printer.literals; type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl = (string * (string * 'a option) list, string * (string * 'b option) list, class * (string * 'c option) list, (class * class) * (string * 'd option) list, (class * string) * (string * 'e option) list, string * (string * 'f option) list) Code_Symbol.attr; type tyco_syntax = Code_Printer.tyco_syntax; type raw_const_syntax = Code_Printer.raw_const_syntax; (** checking and parsing of symbols **) fun cert_const ctxt const = let val _ = if Sign.declared_const (Proof_Context.theory_of ctxt) const then () else error ("No such constant: " ^ quote const); in const end; fun read_const ctxt = Code.read_const (Proof_Context.theory_of ctxt); fun cert_tyco ctxt tyco = let val _ = if Sign.declared_tyname (Proof_Context.theory_of ctxt) tyco then () else error ("No such type constructor: " ^ quote tyco); in tyco end; fun read_tyco ctxt = #1 o dest_Type o Proof_Context.read_type_name {proper = true, strict = true} ctxt; fun cert_class ctxt class = let val _ = Axclass.get_info (Proof_Context.theory_of ctxt) class; in class end; val parse_classrel_ident = Parse.class --| \<^keyword>\<\ -- Parse.class; fun cert_inst ctxt (class, tyco) = (cert_class ctxt class, cert_tyco ctxt tyco); fun read_inst ctxt (raw_tyco, raw_class) = (read_tyco ctxt raw_tyco, Proof_Context.read_class ctxt raw_class); val parse_inst_ident = Parse.name --| \<^keyword>\::\ -- Parse.class; fun cert_syms ctxt = Code_Symbol.map_attr (cert_const ctxt) (cert_tyco ctxt) (cert_class ctxt) (apply2 (cert_class ctxt)) (cert_inst ctxt) I; fun read_syms ctxt = Code_Symbol.map_attr (read_const ctxt) (read_tyco ctxt) (Proof_Context.read_class ctxt) (apply2 (Proof_Context.read_class ctxt)) (read_inst ctxt) I; fun cert_syms' ctxt = Code_Symbol.map_attr (apfst (cert_const ctxt)) (apfst (cert_tyco ctxt)) (apfst (cert_class ctxt)) ((apfst o apply2) (cert_class ctxt)) (apfst (cert_inst ctxt)) I; fun read_syms' ctxt = Code_Symbol.map_attr (apfst (read_const ctxt)) (apfst (read_tyco ctxt)) (apfst (Proof_Context.read_class ctxt)) ((apfst o apply2) (Proof_Context.read_class ctxt)) (apfst (read_inst ctxt)) I; fun check_name is_module s = let val _ = if s = "" then error "Bad empty code name" else (); val xs = Long_Name.explode s; val xs' = if is_module then map (Name.desymbolize NONE) xs else if length xs < 2 then error ("Bad code name without module component: " ^ quote s) else let val (ys, y) = split_last xs; val ys' = map (Name.desymbolize NONE) ys; val y' = Name.desymbolize NONE y; in ys' @ [y'] end; in if xs' = xs then if is_module then (xs, "") else split_last xs else error ("Invalid code name: " ^ quote s ^ "\n" ^ "better try " ^ quote (Long_Name.implode xs')) end; (** theory data **) datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list; type serializer = Token.T list -> Proof.context -> { reserved_syms: string list, identifiers: Code_Printer.identifiers, includes: (string * Pretty.T) list, class_syntax: string -> string option, tyco_syntax: string -> Code_Printer.tyco_syntax option, const_syntax: string -> Code_Printer.const_syntax option, module_name: string } -> Code_Thingol.program -> Code_Symbol.T list -> pretty_modules * (Code_Symbol.T -> string option); type language = {serializer: serializer, literals: literals, check: {env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string}, evaluation_args: Token.T list}; type ancestry = (string * (Code_Thingol.program -> Code_Thingol.program)) list; val merge_ancestry : ancestry * ancestry -> ancestry = AList.join (op =) (K snd); type target = {serial: serial, language: language, ancestry: ancestry}; structure Targets = Theory_Data ( type T = (target * Code_Printer.data) Symtab.table * int; val empty = (Symtab.empty, 0); fun extend (targets, _) = (targets, 0); fun merge ((targets1, _), (targets2, _)) : T = let val targets' = Symtab.join (fn target_name => fn ((target1, data1), (target2, data2)) => if #serial target1 = #serial target2 then ({serial = #serial target1, language = #language target1, ancestry = merge_ancestry (#ancestry target1, #ancestry target2)}, Code_Printer.merge_data (data1, data2)) else error ("Incompatible targets: " ^ quote target_name)) (targets1, targets2) in (targets', 0) end; ); val exists_target = Symtab.defined o #1 o Targets.get; val lookup_target_data = Symtab.lookup o #1 o Targets.get; fun assert_target thy target_name = if exists_target thy target_name then target_name else error ("Unknown code target language: " ^ quote target_name); fun next_export thy = let val thy' = (Targets.map o apsnd) (fn i => i + 1) thy; val i = #2 (Targets.get thy'); in ("export" ^ string_of_int i, thy') end; fun fold1 f xs = fold f (tl xs) (hd xs); fun join_ancestry thy target_name = let val _ = assert_target thy target_name; val the_target_data = the o lookup_target_data thy; val (target, this_data) = the_target_data target_name; val ancestry = #ancestry target; val modifies = rev (map snd ancestry); val modify = fold (curry (op o)) modifies I; val datas = rev (map (snd o the_target_data o fst) ancestry) @ [this_data]; val data = fold1 (fn data' => fn data => Code_Printer.merge_data (data, data')) datas; in (modify, (target, data)) end; fun allocate_target target_name target thy = let val _ = if exists_target thy target_name then error ("Attempt to overwrite existing target " ^ quote target_name) else (); in thy |> (Targets.map o apfst o Symtab.update) (target_name, (target, Code_Printer.empty_data)) end; fun add_language (target_name, language) = allocate_target target_name {serial = serial (), language = language, ancestry = []}; fun add_derived_target (target_name, initial_ancestry) thy = let val _ = if null initial_ancestry then error "Must derive from existing target(s)" else (); fun the_target_data target_name' = case lookup_target_data thy target_name' of NONE => error ("Unknown code target language: " ^ quote target_name') | SOME target_data' => target_data'; val targets = rev (map (fst o the_target_data o fst) initial_ancestry); val supremum = fold1 (fn target' => fn target => if #serial target = #serial target' then target else error "Incompatible targets") targets; val ancestries = map #ancestry targets @ [initial_ancestry]; val ancestry = fold1 (fn ancestry' => fn ancestry => merge_ancestry (ancestry, ancestry')) ancestries; in allocate_target target_name {serial = #serial supremum, language = #language supremum, ancestry = ancestry} thy end; fun map_data target_name f thy = let val _ = assert_target thy target_name; in thy |> (Targets.map o apfst o Symtab.map_entry target_name o apsnd o Code_Printer.map_data) f end; fun map_reserved target_name = map_data target_name o @{apply 3(1)}; fun map_identifiers target_name = map_data target_name o @{apply 3(2)}; fun map_printings target_name = map_data target_name o @{apply 3(3)}; (** serializers **) val codeN = "code"; val generatedN = "Generated_Code"; val code_path = Path.append (Path.basic codeN); fun code_export_message thy = writeln (Export.message thy (Path.basic codeN)); fun export binding content thy = let val thy' = thy |> Generated_Files.add_files (binding, content); - val _ = Export.export thy' binding [content]; + val _ = Export.export thy' binding [XML.Text content]; in thy' end; local fun export_logical (file_prefix, file_pos) format pretty_modules = let fun binding path = Path.binding (path, file_pos); val prefix = code_path file_prefix; in (case pretty_modules of Singleton (ext, p) => export (binding (Path.ext ext prefix)) (format p) | Hierarchy modules => fold (fn (names, p) => export (binding (Path.append prefix (Path.make names))) (format p)) modules) #> tap code_export_message end; fun export_physical root format pretty_modules = (case pretty_modules of Singleton (_, p) => File.write root (format p) | Hierarchy code_modules => (Isabelle_System.mkdirs root; List.app (fn (names, p) => File.write (Path.appends (root :: map Path.basic names)) (format p)) code_modules)); in fun export_result some_file format (pretty_code, _) thy = (case some_file of NONE => let val (file_prefix, thy') = next_export thy; in export_logical (Path.basic file_prefix, Position.none) format pretty_code thy' end | SOME ({physical = false}, file_prefix) => export_logical file_prefix format pretty_code thy | SOME ({physical = true}, (file, _)) => let val root = File.full_path (Resources.master_directory thy) file; val _ = File.check_dir (Path.dir root); val _ = export_physical root format pretty_code; in thy end); fun produce_result syms width pretty_modules = let val format = Code_Printer.format [] width in (case pretty_modules of (Singleton (_, p), deresolve) => ([([], format p)], map deresolve syms) | (Hierarchy code_modules, deresolve) => ((map o apsnd) format code_modules, map deresolve syms)) end; fun present_result selects width (pretty_modules, _) = let val format = Code_Printer.format selects width in (case pretty_modules of Singleton (_, p) => format p | Hierarchy code_modules => space_implode "\n\n" (map (format o #2) code_modules)) end; end; (** serializer usage **) (* technical aside: pretty printing width *) val default_code_width = Attrib.setup_config_int \<^binding>\default_code_width\ (K 80); fun default_width ctxt = Config.get ctxt default_code_width; val the_width = the_default o default_width; (* montage *) fun the_language ctxt = #language o fst o the o lookup_target_data (Proof_Context.theory_of ctxt); fun the_literals ctxt = #literals o the_language ctxt; fun the_evaluation_args ctxt = #evaluation_args o the_language ctxt; local fun activate_target ctxt target_name = let val thy = Proof_Context.theory_of ctxt; val (modify, (target, data)) = join_ancestry thy target_name; val serializer = (#serializer o #language) target; in { serializer = serializer, data = data, modify = modify } end; fun project_program_for_syms ctxt syms_hidden syms1 program1 = let val syms2 = subtract (op =) syms_hidden syms1; val program2 = Code_Symbol.Graph.restrict (not o member (op =) syms_hidden) program1; val unimplemented = Code_Thingol.unimplemented program2; val _ = if null unimplemented then () else error ("No code equations for " ^ commas (map (Proof_Context.markup_const ctxt) unimplemented)); val syms3 = Code_Symbol.Graph.all_succs program2 syms2; val program3 = Code_Symbol.Graph.restrict (member (op =) syms3) program2; in program3 end; fun project_includes_for_syms syms includes = let fun select_include (name, (content, cs)) = if null cs orelse exists (member (op =) syms) cs then SOME (name, content) else NONE; in map_filter select_include includes end; fun prepare_serializer ctxt target_name module_name args proto_program syms = let val { serializer, data, modify } = activate_target ctxt target_name; val printings = Code_Printer.the_printings data; val _ = if module_name = "" then () else (check_name true module_name; ()) val hidden_syms = Code_Symbol.symbols_of printings; val prepared_program = project_program_for_syms ctxt hidden_syms syms proto_program; val prepared_syms = subtract (op =) hidden_syms syms; val all_syms = Code_Symbol.Graph.all_succs proto_program syms; val includes = project_includes_for_syms all_syms (Code_Symbol.dest_module_data printings); val prepared_serializer = serializer args ctxt { reserved_syms = Code_Printer.the_reserved data, identifiers = Code_Printer.the_identifiers data, includes = includes, const_syntax = Code_Symbol.lookup_constant_data printings, tyco_syntax = Code_Symbol.lookup_type_constructor_data printings, class_syntax = Code_Symbol.lookup_type_class_data printings, module_name = module_name }; in (prepared_serializer o modify, (prepared_program, prepared_syms)) end; fun invoke_serializer ctxt target_name module_name args program all_public syms = let val (prepared_serializer, (prepared_program, prepared_syms)) = prepare_serializer ctxt target_name module_name args program syms; val exports = if all_public then [] else prepared_syms; in Code_Preproc.timed_exec "serializing" (fn () => prepared_serializer prepared_program exports) ctxt end; fun assert_module_name "" = error "Empty module name not allowed here" | assert_module_name module_name = module_name; in fun export_code_for some_file target_name module_name some_width args program all_public cs lthy = let val format = Code_Printer.format [] (the_width lthy some_width); val res = invoke_serializer lthy target_name module_name args program all_public cs; in Local_Theory.background_theory (export_result some_file format res) lthy end; fun produce_code_for ctxt target_name module_name some_width args = let val serializer = invoke_serializer ctxt target_name (assert_module_name module_name) args; in fn program => fn all_public => fn syms => produce_result syms (the_width ctxt some_width) (serializer program all_public syms) end; fun present_code_for ctxt target_name module_name some_width args = let val serializer = invoke_serializer ctxt target_name (assert_module_name module_name) args; in fn program => fn (syms, selects) => present_result selects (the_width ctxt some_width) (serializer program false syms) end; fun check_code_for target_name strict args program all_public syms lthy = let val { env_var, make_destination, make_command } = #check (the_language lthy target_name); val format = Code_Printer.format [] 80; fun ext_check p = let val destination = make_destination p; val lthy' = lthy |> Local_Theory.background_theory (export_result (SOME ({physical = true}, (destination, Position.none))) format (invoke_serializer lthy target_name generatedN args program all_public syms)); val cmd = make_command generatedN; val context_cmd = "cd " ^ File.bash_path p ^ " && " ^ cmd ^ " 2>&1"; in if Isabelle_System.bash context_cmd <> 0 then error ("Code check failed for " ^ target_name ^ ": " ^ cmd) else lthy' end; in if not (env_var = "") andalso getenv env_var = "" then if strict then error (env_var ^ " not set; cannot check code for " ^ target_name) else (warning (env_var ^ " not set; skipped checking code for " ^ target_name); lthy) else Isabelle_System.with_tmp_dir "Code_Test" ext_check end; fun dynamic_compilation_text prepared_serializer width prepared_program syms all_public ((vs, ty), t) = let val _ = if Code_Thingol.contains_dict_var t then error "Term to be evaluated contains free dictionaries" else (); val v' = singleton (Name.variant_list (map fst vs)) "a"; val vs' = (v', []) :: vs; val ty' = ITyVar v' `-> ty; val program = prepared_program |> Code_Symbol.Graph.new_node (Code_Symbol.value, Code_Thingol.Fun (((vs', ty'), [(([IVar (SOME "dummy")], t), (NONE, true))]), NONE)) |> fold (curry (perhaps o try o Code_Symbol.Graph.add_edge) Code_Symbol.value) syms; val (pretty_code, deresolve) = prepared_serializer program (if all_public then [] else [Code_Symbol.value]); val (compilation_code, [SOME value_name]) = produce_result [Code_Symbol.value] width (pretty_code, deresolve); in ((compilation_code, value_name), deresolve) end; fun compilation_text' ctxt target_name some_module_name program syms = let val width = default_width ctxt; val evaluation_args = the_evaluation_args ctxt target_name; val (prepared_serializer, (prepared_program, _)) = prepare_serializer ctxt target_name (the_default generatedN some_module_name) evaluation_args program syms; in Code_Preproc.timed_exec "serializing" (fn () => dynamic_compilation_text prepared_serializer width prepared_program syms) ctxt end; fun compilation_text ctxt target_name program syms = fst oo compilation_text' ctxt target_name NONE program syms end; (* local *) (* code generation *) fun prep_destination (location, (s, pos)) = if location = {physical = false} then (location, Path.explode_pos (s, pos)) else let val _ = if s = "" then error ("Bad bad empty " ^ Markup.markup Markup.keyword2 "file" ^ " argument") else (); val _ = legacy_feature (Markup.markup Markup.keyword1 "export_code" ^ " with " ^ Markup.markup Markup.keyword2 "file" ^ " argument" ^ Position.here pos); val _ = Position.report pos Markup.language_path; val path = #1 (Path.explode_pos (s, pos)); val _ = Position.report pos (Markup.path (Path.smart_implode path)); in (location, (path, pos)) end; fun export_code all_public cs seris lthy = let val program = Code_Thingol.consts_program lthy cs; in (seris, lthy) |-> fold (fn (((target_name, module_name), some_file), args) => export_code_for some_file target_name module_name NONE args program all_public (map Constant cs)) end; fun export_code_cmd all_public raw_cs seris lthy = let val cs = Code_Thingol.read_const_exprs lthy raw_cs; in export_code all_public cs ((map o apfst o apsnd o Option.map) prep_destination seris) lthy end; fun produce_code ctxt all_public cs target_name some_width some_module_name args = let val program = Code_Thingol.consts_program ctxt cs; in produce_code_for ctxt target_name some_width some_module_name args program all_public (map Constant cs) end; fun present_code ctxt cs syms target_name some_width some_module_name args = let val program = Code_Thingol.consts_program ctxt cs; in present_code_for ctxt target_name some_width some_module_name args program (map Constant cs, syms) end; fun check_code all_public cs seris lthy = let val program = Code_Thingol.consts_program lthy cs; in (seris, lthy) |-> fold (fn ((target_name, strict), args) => check_code_for target_name strict args program all_public (map Constant cs)) end; fun check_code_cmd all_public raw_cs seris lthy = check_code all_public (Code_Thingol.read_const_exprs lthy raw_cs) seris lthy; (** serializer configuration **) (* reserved symbol names *) fun add_reserved target_name sym thy = let val (_, (_, data)) = join_ancestry thy target_name; val _ = if member (op =) (Code_Printer.the_reserved data) sym then error ("Reserved symbol " ^ quote sym ^ " already declared") else (); in thy |> map_reserved target_name (insert (op =) sym) end; (* checking of syntax *) fun check_const_syntax ctxt target_name c syn = if Code_Printer.requires_args syn > Code.args_number (Proof_Context.theory_of ctxt) c then error ("Too many arguments in syntax for constant " ^ quote c) else Code_Printer.prep_const_syntax (Proof_Context.theory_of ctxt) (the_literals ctxt target_name) c syn; fun check_tyco_syntax ctxt target_name tyco syn = if fst syn <> Sign.arity_number (Proof_Context.theory_of ctxt) tyco then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco) else syn; (* custom symbol names *) fun arrange_name_decls x = let fun arrange is_module (sym, target_names) = map (fn (target, some_name) => (target, (sym, Option.map (check_name is_module) some_name))) target_names; in Code_Symbol.maps_attr' (arrange false) (arrange false) (arrange false) (arrange false) (arrange false) (arrange true) x end; fun cert_name_decls ctxt = cert_syms' ctxt #> arrange_name_decls; fun read_name_decls ctxt = read_syms' ctxt #> arrange_name_decls; fun set_identifier (target_name, sym_name) = map_identifiers target_name (Code_Symbol.set_data sym_name); fun gen_set_identifiers prep_name_decl raw_name_decls thy = fold set_identifier (prep_name_decl (Proof_Context.init_global thy) raw_name_decls) thy; val set_identifiers = gen_set_identifiers cert_name_decls; val set_identifiers_cmd = gen_set_identifiers read_name_decls; (* custom printings *) fun arrange_printings prep_syms ctxt = let fun arrange check (sym, target_syns) = map (fn (target_name, some_syn) => (target_name, (sym, Option.map (check ctxt target_name sym) some_syn))) target_syns; in Code_Symbol.maps_attr' (arrange check_const_syntax) (arrange check_tyco_syntax) (arrange ((K o K o K) I)) (arrange ((K o K o K) I)) (arrange ((K o K o K) I)) (arrange (fn ctxt => fn _ => fn _ => fn (raw_content, raw_syms) => (Pretty.blk (0, Pretty.fbreaks (map Code_Printer.str (split_lines raw_content))), map (prep_syms ctxt) raw_syms))) end; fun cert_printings ctxt = cert_syms' ctxt #> arrange_printings cert_syms ctxt; fun read_printings ctxt = read_syms' ctxt #> arrange_printings read_syms ctxt; fun set_printing (target_name, sym_syn) = map_printings target_name (Code_Symbol.set_data sym_syn); fun gen_set_printings prep_print_decl raw_print_decls thy = fold set_printing (prep_print_decl (Proof_Context.init_global thy) raw_print_decls) thy; val set_printings = gen_set_printings cert_printings; val set_printings_cmd = gen_set_printings read_printings; (* concrete syntax *) fun parse_args f args = case Scan.read Token.stopper f args of SOME x => x | NONE => error "Bad serializer arguments"; (** Isar setup **) val (constantK, type_constructorK, type_classK, class_relationK, class_instanceK, code_moduleK) = (\<^keyword>\constant\, \<^keyword>\type_constructor\, \<^keyword>\type_class\, \<^keyword>\class_relation\, \<^keyword>\class_instance\, \<^keyword>\code_module\); local val parse_constants = constantK |-- Scan.repeat1 Parse.term >> map Constant; val parse_type_constructors = type_constructorK |-- Scan.repeat1 Parse.type_const >> map Type_Constructor; val parse_classes = type_classK |-- Scan.repeat1 Parse.class >> map Type_Class; val parse_class_relations = class_relationK |-- Scan.repeat1 parse_classrel_ident >> map Class_Relation; val parse_instances = class_instanceK |-- Scan.repeat1 parse_inst_ident >> map Class_Instance; val parse_simple_symbols = Scan.repeats1 (parse_constants || parse_type_constructors || parse_classes || parse_class_relations || parse_instances); fun parse_single_symbol_pragma parse_keyword parse_isa parse_target = parse_keyword |-- Parse.!!! (parse_isa --| (\<^keyword>\\\ || \<^keyword>\=>\) -- Parse.and_list1 (\<^keyword>\(\ |-- (Parse.name --| \<^keyword>\)\ -- Scan.option parse_target))); fun parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module = parse_single_symbol_pragma constantK Parse.term parse_const >> Constant || parse_single_symbol_pragma type_constructorK Parse.type_const parse_tyco >> Type_Constructor || parse_single_symbol_pragma type_classK Parse.class parse_class >> Type_Class || parse_single_symbol_pragma class_relationK parse_classrel_ident parse_classrel >> Class_Relation || parse_single_symbol_pragma class_instanceK parse_inst_ident parse_inst >> Class_Instance || parse_single_symbol_pragma code_moduleK Parse.name parse_module >> Module; fun parse_symbol_pragmas parse_const parse_tyco parse_class parse_classrel parse_inst parse_module = Parse.enum1 "|" (Parse.group (fn () => "code symbol pragma") (parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module)); val code_expr_argsP = Scan.optional (\<^keyword>\(\ |-- Parse.args --| \<^keyword>\)\) []; fun code_expr_inP (all_public, raw_cs) = Scan.repeat (\<^keyword>\in\ |-- Parse.!!! (Parse.name -- Scan.optional (\<^keyword>\module_name\ |-- Parse.name) "" -- Scan.option ((\<^keyword>\file_prefix\ >> K {physical = false} || \<^keyword>\file\ >> K {physical = true}) -- Parse.!!! (Parse.position Parse.path)) -- code_expr_argsP)) >> (fn seri_args => export_code_cmd all_public raw_cs seri_args); fun code_expr_checkingP (all_public, raw_cs) = (\<^keyword>\checking\ |-- Parse.!!! (Scan.repeat (Parse.name -- (Scan.optional (\<^keyword>\?\ >> K false) true) -- code_expr_argsP))) >> (fn seri_args => check_code_cmd all_public raw_cs seri_args); in val _ = Outer_Syntax.command \<^command_keyword>\code_reserved\ "declare words as reserved for target language" (Parse.name -- Scan.repeat1 Parse.name >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)); val _ = Outer_Syntax.command \<^command_keyword>\code_identifier\ "declare mandatory names for code symbols" (parse_symbol_pragmas Parse.name Parse.name Parse.name Parse.name Parse.name Parse.name >> (Toplevel.theory o fold set_identifiers_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\code_printing\ "declare dedicated printing for code symbols" (parse_symbol_pragmas (Code_Printer.parse_const_syntax) (Code_Printer.parse_tyco_syntax) Parse.string (Parse.minus >> K ()) (Parse.minus >> K ()) (Parse.text -- Scan.optional (\<^keyword>\for\ |-- parse_simple_symbols) []) >> (Toplevel.theory o fold set_printings_cmd)); val _ = Outer_Syntax.local_theory \<^command_keyword>\export_code\ "generate executable code for constants" (Scan.optional (\<^keyword>\open\ >> K true) false -- Scan.repeat1 Parse.term :|-- (fn args => (code_expr_checkingP args || code_expr_inP args))); end; local val parse_const_terms = Args.theory -- Scan.repeat1 Args.term >> uncurry (fn thy => map (Code.check_const thy)); fun parse_symbols keyword parse internalize mark_symbol = Scan.lift (keyword --| Args.colon) |-- Args.theory -- Scan.repeat1 parse >> uncurry (fn thy => map (mark_symbol o internalize thy)); val parse_consts = parse_symbols constantK Args.term Code.check_const Constant; val parse_types = parse_symbols type_constructorK (Scan.lift Args.name) Sign.intern_type Type_Constructor; val parse_classes = parse_symbols type_classK (Scan.lift Args.name) Sign.intern_class Type_Class; val parse_instances = parse_symbols class_instanceK (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name)) (fn thy => fn (raw_tyco, raw_class) => (Sign.intern_class thy raw_tyco, Sign.intern_type thy raw_class)) Class_Instance; in val _ = Theory.setup (Thy_Output.antiquotation_raw \<^binding>\code_stmts\ (parse_const_terms -- Scan.repeats (parse_consts || parse_types || parse_classes || parse_instances) -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int))) (fn ctxt => fn ((consts, symbols), (target_name, some_width)) => present_code ctxt consts symbols target_name "Example" some_width [] |> trim_line |> Thy_Output.verbatim (Config.put Document_Antiquotation.thy_output_display true ctxt))); end; end; (*struct*)