added add_deps, which actually records dependencies of consts (unlike add_finals);
authorwenzelm
Wed May 24 01:05:02 2006 +0200 (2006-05-24)
changeset 19708a508bde37a81
parent 19707 0e7e236fab50
child 19709 78cd5f6af8e8
added add_deps, which actually records dependencies of consts (unlike add_finals);
tuned;
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Wed May 24 01:05:01 2006 +0200
     1.2 +++ b/src/Pure/theory.ML	Wed May 24 01:05:02 2006 +0200
     1.3 @@ -49,6 +49,7 @@
     1.4    val assert_super: theory -> theory -> theory
     1.5    val add_axioms: (bstring * string) list -> theory -> theory
     1.6    val add_axioms_i: (bstring * term) list -> theory -> theory
     1.7 +  val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
     1.8    val add_defs: bool -> bool -> (bstring * string) list -> theory -> theory
     1.9    val add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory
    1.10    val add_finals: bool -> string list -> theory -> theory
    1.11 @@ -59,6 +60,7 @@
    1.12  structure Theory: THEORY =
    1.13  struct
    1.14  
    1.15 +
    1.16  (** type theory **)
    1.17  
    1.18  (* context operations *)
    1.19 @@ -230,7 +232,34 @@
    1.20  
    1.21  (** add constant definitions **)
    1.22  
    1.23 -fun prep_const thy (c, T) = (c, Compress.typ thy (Type.varifyT T));
    1.24 +(* dependencies *)
    1.25 +
    1.26 +fun dependencies thy unchecked is_def name lhs rhs =
    1.27 +  let
    1.28 +    val pp = Sign.pp thy;
    1.29 +    val consts = Sign.consts_of thy;
    1.30 +
    1.31 +    val lhs_vars = Term.add_tfreesT (#2 lhs) [];
    1.32 +    val rhs_extras = fold (#2 #> Term.fold_atyps (fn TFree v =>
    1.33 +      if member (op =) lhs_vars v then I else insert (op =) v | _ => I)) rhs [];
    1.34 +    val _ =
    1.35 +      if null rhs_extras then ()
    1.36 +      else error ("Specification depends on extra type variables: " ^
    1.37 +        commas_quote (map (Pretty.string_of_typ pp o TFree) rhs_extras) ^
    1.38 +        "\nThe error(s) above occurred in " ^ quote name);
    1.39 +
    1.40 +    fun prep const =
    1.41 +      let val Const (c, T) = Sign.no_vars pp (Const const)
    1.42 +      in (c, Compress.typ thy (Type.varifyT T)) end;
    1.43 +  in
    1.44 +    Defs.define pp consts unchecked is_def (Context.theory_name thy) name (prep lhs) (map prep rhs)
    1.45 +  end;
    1.46 +
    1.47 +fun add_deps a raw_lhs raw_rhs thy =
    1.48 +  let
    1.49 +    val lhs :: rhs = map (dest_Const o Sign.cert_term thy o Const) (raw_lhs :: raw_rhs);
    1.50 +    val name = if a = "" then (#1 lhs ^ " axiom") else a;
    1.51 +  in thy |> map_defs (dependencies thy false false name lhs rhs) end;
    1.52  
    1.53  
    1.54  (* check_overloading *)
    1.55 @@ -266,10 +295,7 @@
    1.56      val (lhs_const, rhs) = Sign.cert_def (Sign.pp thy) tm;
    1.57      val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
    1.58      val _ = check_overloading thy overloaded lhs_const;
    1.59 -  in
    1.60 -    defs |> Defs.define (Sign.pp thy) (Sign.consts_of thy) unchecked true (Context.theory_name thy)
    1.61 -      name (prep_const thy lhs_const) (map (prep_const thy) rhs_consts)
    1.62 -  end
    1.63 +  in defs |> dependencies thy unchecked true name lhs_const rhs_consts end
    1.64    handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
    1.65     [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"),
    1.66      Pretty.fbrk, Pretty.quote (Sign.pretty_term thy tm)]));
    1.67 @@ -303,10 +329,8 @@
    1.68      fun const_of (Const const) = const
    1.69        | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
    1.70        | const_of _ = error "Attempt to finalize non-constant term";
    1.71 -    fun specify (c, T) = Defs.define (Sign.pp thy) (Sign.consts_of thy) false false
    1.72 -      (Context.theory_name thy) (c ^ " axiom") (prep_const thy (c, T)) [];
    1.73 -    val finalize = specify o check_overloading thy overloaded o
    1.74 -      const_of o Sign.no_vars (Sign.pp thy) o prep_term thy;
    1.75 +    fun specify (c, T) = dependencies thy false false (c ^ " axiom") (c, T) [];
    1.76 +    val finalize = specify o check_overloading thy overloaded o const_of o prep_term thy;
    1.77    in thy |> map_defs (fold finalize args) end;
    1.78  
    1.79  in