# HG changeset patch # User ballarin # Date 1227817516 -3600 # Node ID 3d166f1bd73345c24991cfc918d60a0985987220 # Parent f30016592375f8d2f0d7080eae399a7450f30907 Roundup bound. diff -r f30016592375 -r 3d166f1bd733 src/Pure/Isar/new_locale.ML --- a/src/Pure/Isar/new_locale.ML Thu Nov 27 10:30:42 2008 +0100 +++ b/src/Pure/Isar/new_locale.ML Thu Nov 27 21:25:16 2008 +0100 @@ -160,7 +160,7 @@ (*** Activate context elements of locale ***) -(* Resolve locale dependencies in a depth-first fashion *) +(** Resolve locale dependencies in a depth-first fashion **) local @@ -173,27 +173,49 @@ val empty = (Idtab.empty : identifiers); -fun add thy (name, morph) (deps, marked) = +val roundup_bound = 120; + +local + +fun add thy depth (name, morph) (deps, marked) = + if depth > roundup_bound + then error "Roundup bound exceeded (sublocale relation probably not terminating)." + else + let + val Loc {parameters = (_, params), dependencies, ...} = the_locale thy name; + val instance = params |> + map ((fn (b, T, _) => Free (Name.name_of b, the T)) #> Morphism.term morph); + in + if Idtab.defined marked (name, instance) + then (deps, marked) + else + let + val dependencies' = + map (fn ((name, morph'), _) => (name, morph' $> morph)) dependencies; + val marked' = Idtab.insert (op =) ((name, instance), ()) marked; + val (deps', marked'') = fold_rev (add thy (depth + 1)) dependencies' ([], marked'); + in + ((name, morph) :: deps' @ deps, marked'') + end + end; + +in + +fun roundup thy activate_dep (name, morph) (marked, ctxt) = let - val Loc {parameters = (_, params), dependencies, ...} = the_locale thy name; - val instance = params |> - map ((fn (b, T, _) => Free (Name.name_of b, the T)) #> Morphism.term morph); + val name' = intern thy name; + val Loc {dependencies, ...} = the_locale thy name'; + val (dependencies', marked') = add thy 0 (name', morph) ([], marked); in - if Idtab.defined marked (name, instance) - then (deps, marked) - else - let - val dependencies' = - map (fn ((name, morph'), _) => (name, morph' $> morph)) dependencies; - val marked' = Idtab.insert (op =) ((name, instance), ()) marked; - val (deps', marked'') = fold_rev (add thy) dependencies' ([], marked'); - in - ((name, morph) :: deps' @ deps, marked'') - end + (marked', ctxt |> fold_rev (activate_dep thy) dependencies') end; end; +end; + + +(* Declarations and facts *) fun activate_decls thy (name, morph) ctxt = let @@ -203,15 +225,6 @@ fold_rev (fn (decl, _) => Context.proof_map (decl morph)) term_decls end; -fun activate_declarations thy (name, morph) (marked, ctxt) = - let - val name' = intern thy name; - val Loc {dependencies, ...} = the_locale thy name'; - val (dependencies', marked') = add thy (name', morph) ([], marked); - in - (marked', ctxt |> fold_rev (activate_decls thy) dependencies') - end; - fun activate_notes activ_elem thy (name, morph) input = let val Loc {notes, ...} = the_locale thy name; @@ -223,14 +236,8 @@ fold_rev activate notes input end; -fun activate_facts_intern thy activ_elem (name, morph) (marked, ctxt) = - let - val name' = intern thy name; - val Loc {dependencies, ...} = the_locale thy name'; - val (dependencies', marked') = add thy (name', morph) ([], marked); - in - (marked', ctxt |> fold_rev (activate_notes activ_elem thy) dependencies') - end; + +(* Entire locale content *) fun activate name thy activ_elem input = let @@ -245,9 +252,12 @@ (if not (null defs) then activ_elem (Defines (map (fn def => (Attrib.no_binding, (def, []))) defs)) else I) |> - pair empty |> activate_facts_intern thy activ_elem (name', Morphism.identity) |> snd + pair empty |> roundup thy (activate_notes activ_elem) (name', Morphism.identity) |> snd end; + +(** Public activation functions **) + local fun init_elem (Fixes fixes) ctxt = ctxt |> @@ -277,7 +287,9 @@ in -fun activate_facts thy dep = activate_facts_intern thy init_elem dep; +fun activate_declarations thy = roundup thy activate_decls; + +fun activate_facts thy = roundup thy (activate_notes init_elem); fun init name thy = activate name thy init_elem (ProofContext.init thy);