src/Pure/Thy/thm_deps.ML
changeset 11530 b6e21f6cfacd
parent 9502 50ec59aff389
child 11543 d61b913431c5
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Fri Aug 31 16:24:39 2001 +0200
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Fri Aug 31 16:25:53 2001 +0200
     1.3 @@ -20,47 +20,49 @@
     1.4  structure ThmDeps : THM_DEPS =
     1.5  struct
     1.6  
     1.7 -fun enable () = Thm.keep_derivs := ThmDeriv;
     1.8 -fun disable () = Thm.keep_derivs := MinDeriv;
     1.9 -
    1.10 -fun is_internal (name, tags) = name = "" orelse Drule.has_internal tags;
    1.11 +open Proofterm;
    1.12  
    1.13 -fun is_thm_axm (Theorem x) = not (is_internal x)
    1.14 -  | is_thm_axm (Axiom x) = not (is_internal x)
    1.15 -  | is_thm_axm _ = false;
    1.16 +fun enable () = keep_derivs := ThmDeriv;
    1.17 +fun disable () = keep_derivs := MinDeriv;
    1.18  
    1.19 -fun get_name (Theorem (s, _)) = s
    1.20 -  | get_name (Axiom (s, _)) = s
    1.21 -  | get_name _ = "";
    1.22 +fun dest_thm_axm (PThm (nt, prf, _, _)) = (nt, prf)
    1.23 +  | dest_thm_axm (PAxm (n, _, _)) = ((n ^ " (Ax)", []), MinProof [])
    1.24 +  | dest_thm_axm _ = (("", []), MinProof []);
    1.25  
    1.26 -fun make_deps_graph ((gra, parents), Join (ta, ders)) =
    1.27 -  let
    1.28 -    val name = get_name ta;
    1.29 -  in
    1.30 -    if is_thm_axm ta then
    1.31 -      if is_none (Symtab.lookup (gra, name)) then
    1.32 -        let
    1.33 -          val (gra', parents') = foldl make_deps_graph ((gra, []), ders);
    1.34 -          val prefx = #1 (Library.split_last (NameSpace.unpack name));
    1.35 -          val session =
    1.36 -            (case prefx of
    1.37 -              (x :: _) =>
    1.38 -                (case ThyInfo.lookup_theory x of
    1.39 -                  Some thy =>
    1.40 -                    let val name = #name (Present.get_info thy)
    1.41 -                    in if name = "" then [] else [name] end 
    1.42 -                | None => [])
    1.43 -             | _ => ["global"]);
    1.44 -        in
    1.45 -          (Symtab.update ((name,
    1.46 -            {name = Sign.base_name name, ID = name,
    1.47 -             dir = space_implode "/" (session @ prefx),
    1.48 -             unfold = false, path = "", parents = parents'}), gra'), name ins parents)
    1.49 -        end
    1.50 -      else (gra, name ins parents)
    1.51 -    else
    1.52 -      foldl make_deps_graph ((gra, parents), ders)
    1.53 -  end;
    1.54 +fun make_deps_graph (p, AbsP (_, _, prf)) = make_deps_graph (p, prf)
    1.55 +  | make_deps_graph (p, Abst (_, _, prf)) = make_deps_graph (p, prf)
    1.56 +  | make_deps_graph (p, prf1 % prf2) =
    1.57 +      make_deps_graph (make_deps_graph (p, prf1), prf2)
    1.58 +  | make_deps_graph (p, prf %% _) = make_deps_graph (p, prf)
    1.59 +  | make_deps_graph (p, MinProof prfs) = foldl make_deps_graph (p, prfs)
    1.60 +  | make_deps_graph (p as (gra, parents), prf) =
    1.61 +      let val ((name, tags), prf') = dest_thm_axm prf
    1.62 +      in
    1.63 +        if name <> "" andalso not (Drule.has_internal tags) then
    1.64 +          if is_none (Symtab.lookup (gra, name)) then
    1.65 +            let
    1.66 +              val (gra', parents') = make_deps_graph ((gra, []), prf');
    1.67 +              val prefx = #1 (Library.split_last (NameSpace.unpack name));
    1.68 +              val session =
    1.69 +                (case prefx of
    1.70 +                  (x :: _) =>
    1.71 +                    (case ThyInfo.lookup_theory x of
    1.72 +                      Some thy =>
    1.73 +                        let val name = #name (Present.get_info thy)
    1.74 +                        in if name = "" then [] else [name] end 
    1.75 +                    | None => [])
    1.76 +                 | _ => ["global"]);
    1.77 +            in
    1.78 +              (Symtab.update ((name,
    1.79 +                {name = Sign.base_name name, ID = name,
    1.80 +                 dir = space_implode "/" (session @ prefx),
    1.81 +                 unfold = false, path = "", parents = parents'}), gra'),
    1.82 +               name ins parents)
    1.83 +            end
    1.84 +          else (gra, name ins parents)
    1.85 +        else
    1.86 +          make_deps_graph ((gra, parents), prf')
    1.87 +      end;
    1.88  
    1.89  fun thm_deps thms =
    1.90    let