# HG changeset patch # User wenzelm # Date 1118005649 -7200 # Node ID ea4e64b2f25a71b7be89d8467e4b4cf1458f095d # Parent e661e37a4d508e234670b558633c3a5c0cbdba55 renamed const_deps to defs; improved error messages; major cleanup -- removed quite a bit of dead code; diff -r e661e37a4d50 -r ea4e64b2f25a src/Pure/theory.ML --- a/src/Pure/theory.ML Sun Jun 05 23:07:28 2005 +0200 +++ b/src/Pure/theory.ML Sun Jun 05 23:07:29 2005 +0200 @@ -4,13 +4,14 @@ The abstract type "theory" of theories. *) + signature BASIC_THEORY = sig type theory exception THEORY of string * theory list val rep_theory: theory -> {sign: Sign.sg, - const_deps: Defs.graph, + defs: Defs.graph, axioms: term Symtab.table, oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table, parents: theory list, @@ -118,7 +119,6 @@ val put_data: Object.kind -> ('a -> Object.T) -> 'a -> theory -> theory end; - structure Theory: PRIVATE_THEORY = struct @@ -128,14 +128,14 @@ datatype theory = Theory of { sign: Sign.sg, - const_deps: Defs.graph, + defs: Defs.graph, axioms: term Symtab.table, oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table, parents: theory list, ancestors: theory list}; -fun make_theory sign const_deps axioms oracles parents ancestors = - Theory {sign = sign, const_deps = const_deps, axioms = axioms, +fun make_theory sign defs axioms oracles parents ancestors = + Theory {sign = sign, defs = defs, axioms = axioms, oracles = oracles, parents = parents, ancestors = ancestors}; fun rep_theory (Theory args) = args; @@ -185,19 +185,15 @@ fun ext_theory thy ext_sg new_axms new_oras = let - val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy - val draft = Sign.is_draft sign - val axioms' = - Symtab.extend (if draft then axioms else Symtab.empty, new_axms) - handle Symtab.DUPS names => err_dup_axms names - val oracles' = - Symtab.extend (oracles, new_oras) - handle Symtab.DUPS names => err_dup_oras names + val Theory {sign, defs, axioms, oracles, parents, ancestors} = thy; + val draft = Sign.is_draft sign; + val axioms' = Symtab.extend (if draft then axioms else Symtab.empty, new_axms) + handle Symtab.DUPS names => err_dup_axms names; + val oracles' = Symtab.extend (oracles, new_oras) + handle Symtab.DUPS names => err_dup_oras names; val (parents', ancestors') = - if draft then (parents, ancestors) else ([thy], thy :: ancestors) - in - make_theory (ext_sg sign) const_deps axioms' oracles' parents' ancestors' - end; + if draft then (parents, ancestors) else ([thy], thy :: ancestors); + in make_theory (ext_sg sign) defs axioms' oracles' parents' ancestors' end; (* extend signature of a theory *) @@ -260,22 +256,23 @@ fun err_in_axm name = error ("The error(s) above occurred in axiom " ^ quote name); -fun no_vars sg tm = (case (term_vars tm, term_tvars tm) of +fun no_vars pp tm = + (case (Term.term_vars tm, Term.term_tvars tm) of ([], []) => tm | (ts, ixns) => error (Pretty.string_of (Pretty.block (Pretty.breaks (Pretty.str "Illegal schematic variable(s) in term:" :: - map (Sign.pretty_term sg) ts @ - map (Sign.pretty_typ sg o TVar) ixns))))); + map (Pretty.term pp) ts @ map (Pretty.typ pp o TVar) ixns))))); fun cert_axm sg (name, raw_tm) = let - val (t, T, _) = Sign.certify_term (Sign.pp sg) sg raw_tm + val pp = Sign.pp sg; + val (t, T, _) = Sign.certify_term pp sg raw_tm handle TYPE (msg, _, _) => error msg - | TERM (msg, _) => error msg; + | TERM (msg, _) => error msg; in Term.no_dummy_patterns t handle TERM (msg, _) => error msg; assert (T = propT) "Term not of type prop"; - (name, no_vars sg t) + (name, no_vars pp t) end; (*some duplication of code with read_def_cterm*) @@ -289,24 +286,32 @@ fun read_axm sg name_str = read_def_axm (sg, K NONE, K NONE) [] name_str; fun inferT_axm sg (name, pre_tm) = - let val (t, _) = Sign.infer_types (Sign.pp sg) sg - (K NONE) (K NONE) [] true ([pre_tm], propT); - in (name, no_vars sg t) end + let + val pp = Sign.pp sg; + val (t, _) = Sign.infer_types pp sg (K NONE) (K NONE) [] true ([pre_tm], propT); + in (name, no_vars pp t) end handle ERROR => err_in_axm name; (* extend axioms of a theory *) -fun ext_axms prep_axm raw_axms (thy as Theory {sign, ...}) = +local + +fun gen_add_axioms prep_axm raw_axms thy = let - val raw_axms' = map (apfst (Sign.full_name sign)) raw_axms; + val sg = sign_of thy; + val raw_axms' = map (apfst (Sign.full_name sg)) raw_axms; val axioms = - map (apsnd (Term.compress_term o Logic.varify) o prep_axm sign) raw_axms'; + map (apsnd (Term.compress_term o Logic.varify) o prep_axm sg) raw_axms'; val ext_sg = Sign.add_space (axiomK, map fst axioms); in ext_theory thy ext_sg axioms [] end; -val add_axioms = ext_axms read_axm; -val add_axioms_i = ext_axms cert_axm; +in + +val add_axioms = gen_add_axioms read_axm; +val add_axioms_i = gen_add_axioms cert_axm; + +end; (* add oracle **) @@ -323,195 +328,188 @@ (* overloading *) -datatype overloading = NoOverloading | Useless | Plain; +datatype overloading = Clean | Implicit | Useless; -fun overloading sg declT defT = - let val T = Term.incr_tvar (maxidx_of_typ declT + 1) (Type.varifyT defT) in - if Sign.typ_instance sg (declT, T) then NoOverloading - else if Sign.typ_instance sg (Type.strip_sorts declT, Type.strip_sorts T) then Useless - else Plain +fun overloading sg overloaded declT defT = + let + val defT' = Term.incr_tvar (maxidx_of_typ declT + 1) (Type.varifyT defT); + in + if Sign.typ_instance sg (declT, defT') then Clean + else if Sign.typ_instance sg (Type.strip_sorts declT, Type.strip_sorts defT') then Useless + else if overloaded then Clean + else Implicit end; -(* dest_defn *) -fun dest_defn tm = +(* dest_def *) + +fun dest_def pp tm = let fun err msg = raise TERM (msg, [tm]); val (lhs, rhs) = Logic.dest_equals (Logic.strip_imp_concl tm) handle TERM _ => err "Not a meta-equality (==)"; - val (head, args) = strip_comb lhs; - val c_ty as (c, ty) = dest_Const head + val (head, args) = Term.strip_comb lhs; + val (c, T) = Term.dest_Const head handle TERM _ => err "Head of lhs not a constant"; fun dest_free (Free (x, _)) = x | dest_free (Const ("TYPE", Type ("itself", [TFree (x, _)]))) = x | dest_free _ = raise Match; + val show_terms = commas_quote o map (Pretty.string_of_term pp); val show_frees = commas_quote o map dest_free; val show_tfrees = commas_quote o map fst; + val lhs_nofrees = filter (not o can dest_free) args; val lhs_dups = duplicates args; - val rhs_extras = gen_rems (op =) (term_frees rhs, args); - val rhs_extrasT = gen_rems (op =) (term_tfrees rhs, typ_tfrees ty); + val rhs_extras = term_frees rhs |> fold (remove op =) args; + val rhs_extrasT = term_tfrees rhs |> fold (remove op =) (typ_tfrees T); in - if not (forall (can dest_free) args) then - err "Arguments (on lhs) must be variables" + if not (null lhs_nofrees) then + err ("Non-variables as arguments on lhs: " ^ show_terms lhs_nofrees) else if not (null lhs_dups) then err ("Duplicate variables on lhs: " ^ show_frees lhs_dups) else if not (null rhs_extras) then err ("Extra variables on rhs: " ^ show_frees rhs_extras) else if not (null rhs_extrasT) then err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT) - else if exists_Const (fn c_ty' => c_ty' = c_ty) rhs then + else if exists_Const (equal (c, T)) rhs then err ("Constant to be defined occurs on rhs") - else (c_ty, rhs) + else ((c, T), rhs) end; -(* check_defn *) +(* check_def *) + +fun pretty_const pp (c, T) = + [Pretty.str c, Pretty.str " ::", Pretty.brk 1, + Pretty.quote (Pretty.typ pp (Type.freeze_type T))]; (* FIXME zero indexes!? *) -fun err_in_defn sg name msg = - error (cat_lines [msg, "The error(s) above occurred in definition " ^ quote name]); +(* FIXME move error messages to defs.ML !? *) -fun pretty_const sg (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)))]; +fun pretty_path pp path = fold_rev (fn (T, c, def) => + fn [] => [Pretty.block (pretty_const pp (c, T))] + | prts => Pretty.block (pretty_const pp (c, T) @ + [Pretty.brk 1, Pretty.str ("depends via " ^ quote def ^ " on")]) :: prts) path []; -fun cycle_msg sg (infinite, namess) = - let val header = if not (infinite) then "cyclic dependency found: " else "infinite chain found: " - in - Pretty.string_of (Pretty.block (((Pretty.str header) :: Pretty.fbrk :: ( - let - fun f last (ty, constname, defname) = - (pretty_const sg (constname, ty)) @ (if last then [] else [Pretty.str (" depends via "^ quote defname^ " on ")]) - - in - foldr (fn (x,r) => (f (r=[]) x)@[Pretty.fbrk]@r) [] namess - end)))) - end +fun defs_circular pp path = + Pretty.str "Cyclic dependency in definitions: " :: pretty_path pp path + |> Pretty.chunks |> Pretty.string_of; + +fun defs_infinite_chain pp path = + Pretty.str "Infinite chain in definitions: " :: pretty_path pp path + |> Pretty.chunks |> Pretty.string_of; + +fun defs_clash def1 def2 = "Type clash in definitions " ^ quote def1 ^ " and " ^ quote def2; -fun check_defn sg overloaded ((deps, axms), def as (bname, tm)) = - let - val name = Sign.full_name sg bname; - - fun pretty_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, - Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)))]; +fun defs_final pp const = + (Pretty.str "Attempt to define final constant" :: Pretty.brk 1 :: pretty_const pp const) + |> Pretty.block |> Pretty.string_of; - fun def_txt (c_ty, txt) = Pretty.block - (Pretty.str "Definition of " :: pretty_const c_ty @ - (if txt = "" then [] else [Pretty.str txt])); +(* FIXME move to defs.ML; avoid exceptions *) +fun declare sg c defs = + let val T = Sign.the_const_type sg c + in if_none (try (Defs.declare defs) (c, T)) defs end; - fun show_defn c (dfn, ty') = Pretty.block - (Pretty.str " " :: pretty_const (c, ty') @ [Pretty.str " in ", Pretty.str dfn]); - - val (c_ty as (c, ty), rhs) = dest_defn tm - handle TERM (msg, _) => err_in_defn sg name msg; - fun decl deps c = - (case Sign.const_type sg c of - SOME T => (Defs.declare deps (c, T) handle _ => deps, T) - | NONE => err_in_defn sg name ("Undeclared constant " ^ quote c)); +fun check_def sg overloaded (bname, tm) defs = + let + val pp = Sign.pp sg; + val name = Sign.full_name sg bname; + + fun err msg = error (Pretty.string_of (Pretty.chunks + [Pretty.str msg, + Pretty.block [Pretty.str ("The error(s) above occurred in definition " ^ quote name ^ ":"), + Pretty.fbrk, Pretty.quote (Pretty.term pp tm)]])); + + fun show_def const txt = + [Pretty.block (Pretty.str "Definition of " :: pretty_const pp const), Pretty.str txt] + |> Pretty.chunks |> Pretty.string_of; - val (deps, c_decl) = decl deps c + val ((c, defT), rhs) = dest_def pp tm handle TERM (msg, _) => err msg; + val rhs_consts = Term.term_constsT rhs; + val declT = Sign.the_const_type sg c; - val body = Term.term_constsT rhs - val deps = foldl (fn ((c, _), deps) => fst (decl deps c)) deps body + val _ = + (case overloading sg overloaded declT defT of + Clean => () + | Implicit => warning (show_def (c, defT) + ("is strictly less general than the declared type (see " ^ quote name ^ ")")) + | Useless => err (Library.setmp show_sorts true (show_def (c, defT)) + "imposes additional sort constraints on the declared type of the constant")); + val decl_defs = defs |> declare sg c |> fold (declare sg) (map #1 rhs_consts); in - (case overloading sg c_decl ty of - Useless => - err_in_defn sg name (Pretty.string_of (Pretty.chunks - [Library.setmp show_sorts true def_txt (c_ty, ""), Pretty.str - "imposes additional sort constraints on the declared type of the constant"])) - | ov => - let - val deps' = Defs.define deps c_ty name body - handle Defs.DEFS s => err_in_defn sg name ("DEFS: "^s) - | Defs.CIRCULAR s => err_in_defn sg name (cycle_msg sg (false, s)) - | Defs.INFINITE_CHAIN s => err_in_defn sg name (cycle_msg sg (true, s)) - | Defs.CLASH (_, def1, def2) => err_in_defn sg name ( - "clashing definitions "^ quote def1 ^" and "^ quote def2) - | Defs.FINAL cfinal => - err_in_defn sg name (Pretty.string_of (Pretty.block - ([Pretty.str "The constant",Pretty.brk 1] @ - pretty_const cfinal @ - [Pretty.brk 1,Pretty.str "has been declared final"]))) - in - ((if ov = Plain andalso not overloaded then - warning (Pretty.string_of (Pretty.chunks - [def_txt (c_ty, ""), Pretty.str ("is strictly less general than the declared type (see " ^ quote name ^ ")")])) - else - ()); (deps', def::axms)) - end) + Defs.define decl_defs (c, defT) name rhs_consts + handle Defs.DEFS msg => err ("DEFS: " ^ msg) (* FIXME sys_error!? *) + | Defs.CIRCULAR path => err (defs_circular pp path) + | Defs.INFINITE_CHAIN path => err (defs_infinite_chain pp path) + | Defs.CLASH (_, def1, def2) => err (defs_clash def1 def2) + | Defs.FINAL const => err (defs_final pp const) end; (* add_defs *) -fun ext_defns prep_axm overloaded raw_axms thy = - let - val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy; - val all_axioms = List.concat (map (Symtab.dest o #axioms o rep_theory) (thy :: ancestors)); +local +fun gen_add_defs prep_axm overloaded raw_axms thy = + let + val Theory {sign, defs, axioms, oracles, parents, ancestors} = thy; val axms = map (prep_axm sign) raw_axms; - val (const_deps', _) = Library.foldl (check_defn sign overloaded) ((const_deps, all_axioms), axms); + val defs' = fold (check_def sign overloaded) axms defs; in - make_theory sign const_deps' axioms oracles parents ancestors + make_theory sign defs' axioms oracles parents ancestors |> add_axioms_i axms end; -val add_defs_i = ext_defns cert_axm; -val add_defs = ext_defns read_axm; +in + +val add_defs_i = gen_add_defs cert_axm; +val add_defs = gen_add_defs read_axm; + +end; (* add_finals *) -fun ext_finals prep_term overloaded raw_terms thy = +local + +fun gen_add_finals prep_term overloaded raw_terms thy = let - val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy; - fun mk_final (tm, finals) = - let - fun err msg = raise TERM(msg,[tm]) - val (c,ty) = dest_Const tm - handle TERM _ => err "Can only make constants final" - val c_decl = - (case Sign.const_type sign c of - SOME T => T - | NONE => err ("Undeclared constant " ^ quote c)) - val _ = - case overloading sign c_decl ty of - NoOverloading => () - | Useless => err "Sort constraints too strong" - | Plain => (if overloaded then () else warning "Type is more general than declared") - val finals = Defs.declare finals (c, c_decl) handle _ => finals - in - Defs.finalize finals (c,ty) - end - val consts = map (prep_term sign) raw_terms; - val const_deps' = foldl mk_final const_deps consts; - in - make_theory sign const_deps' axioms oracles parents ancestors - end; + val Theory {sign, defs, axioms, oracles, parents, ancestors} = thy; + fun finalize tm finals = + let + fun err msg = raise TERM (msg, [tm]); (* FIXME error!? *) + val (c, defT) = + (case tm of Const x => x + | Free _ => err "Attempt to finalize variable (or undeclared constant)" + | _ => err "Attempt to finalize non-constant term"); + val declT = Sign.the_const_type sign c + handle TYPE (msg, _, _) => err msg; + val _ = + (case overloading sign overloaded declT defT of + Clean => () + | Implcit => warning ("Finalizing " ^ quote c ^ + " at a strictly less general type than declared") + | Useless => err "Sort constraints stronger than declared"); + in + Defs.finalize (if_none (try (Defs.declare finals) (c, declT)) finals) (c, defT) + end; + val defs' = fold finalize (map (prep_term sign) raw_terms) defs; + in make_theory sign defs' axioms oracles parents ancestors end; -local - fun read_term sg = Sign.simple_read_term sg TypeInfer.logicT; - fun cert_term sg = #1 o Sign.certify_term (Sign.pp sg) sg; +fun read_term sg = Sign.simple_read_term sg TypeInfer.logicT; +fun cert_term sg = #1 o Sign.certify_term (Sign.pp sg) sg; + in -val add_finals = ext_finals read_term; -val add_finals_i = ext_finals cert_term; + +val add_finals = gen_add_finals read_term; +val add_finals_i = gen_add_finals cert_term; + end; -fun merge_final sg = - let - fun merge_single (tys,ty) = - if exists (curry (Sign.typ_instance sg) ty) tys - then tys - else (ty::gen_rem (Sign.typ_instance sg) (tys,ty)); - fun merge ([],_) = [] - | merge (_,[]) = [] - | merge input = Library.foldl merge_single input; - in - SOME o merge - end; (** additional theory data **) @@ -528,12 +526,12 @@ (*merge list of theories from left to right, preparing extend*) fun prep_ext_merge thys = let - val sign' = Sign.prep_ext_merge (map sign_of thys) + val sign' = Sign.prep_ext_merge (map sign_of thys); - val depss = map (#const_deps o rep_theory) thys; - val deps' = foldl (uncurry Defs.merge) (hd depss) (tl depss) - handle Defs.CIRCULAR namess => error (cycle_msg sign' (false, namess)) - | Defs.INFINITE_CHAIN namess => error (cycle_msg sign' (true, namess)) + val defss = map (#defs o rep_theory) thys; + val defs' = foldl (uncurry Defs.merge) (hd defss) (tl defss) + handle Defs.CIRCULAR namess => error (defs_circular (Sign.pp sign') namess) + | Defs.INFINITE_CHAIN namess => error (defs_infinite_chain (Sign.pp sign') namess); val axioms' = Symtab.empty; @@ -546,9 +544,7 @@ val parents' = gen_distinct eq_thy thys; val ancestors' = gen_distinct eq_thy (parents' @ List.concat (map ancestors_of thys)); - in - make_theory sign' deps' axioms' oracles' parents' ancestors' - end; + in make_theory sign' defs' axioms' oracles' parents' ancestors' end; end;