Strict dfs traversal of imported and registered identifiers.
authorballarin
Wed Jul 19 19:24:02 2006 +0200 (2006-07-19)
changeset 20167fe5fd4fd4114
parent 20166 ae2bc00408d6
child 20168 ed7bced29e1b
Strict dfs traversal of imported and registered identifiers.
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Wed Jul 19 14:16:36 2006 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Wed Jul 19 19:24:02 2006 +0200
     1.3 @@ -737,33 +737,40 @@
     1.4                 map_mode (map (Element.rename_witness ren)) mode)
     1.5           else (parms, mode));
     1.6  
     1.7 -    (* add registrations of (name, ps), recursively; adjust hyps of witnesses *)
     1.8 +    (* add (name, ps) and its registrations, recursively; adjust hyps of witnesses *)
     1.9  
    1.10 -    fun add_regs (name, ps) (ths, ids) =
    1.11 -        let
    1.12 -          val {params, regs, ...} = the_locale thy name;
    1.13 -          val ps' = map #1 params;
    1.14 -          val ren = map #1 ps' ~~ map (fn (x, _) => (x, NONE)) ps;
    1.15 -            (* dummy syntax, since required by rename *)
    1.16 -          val ps'' = map (fn ((p, _), (_, T)) => (p, T)) (ps ~~ ps');
    1.17 -          val [env] = unify_parms ctxt ps [map (apsnd SOME) ps''];
    1.18 -            (* propagate parameter types, to keep them consistent *)
    1.19 -          val regs' = map (fn ((name, ps), wits) =>
    1.20 -              ((name, map (Element.rename ren) ps),
    1.21 -               map (Element.transfer_witness thy) wits)) regs;
    1.22 -          val new_regs = gen_rems (eq_fst (op =)) (regs', ids);
    1.23 -          val new_ids = map fst new_regs;
    1.24 -          val new_idTs = map (apsnd (map (fn p => (p, (the o AList.lookup (op =) ps) p)))) new_ids;
    1.25 +    fun add_with_regs ((name, pTs), mode) (wits, ids, visited) =
    1.26 +        if member (fn (a, (b, _)) => a = b) visited (name, map #1 pTs)
    1.27 +        then (wits, ids, visited)
    1.28 +        else
    1.29 +	  let
    1.30 +	    val {params, regs, ...} = the_locale thy name;
    1.31 +	    val pTs' = map #1 params;
    1.32 +	    val ren = map #1 pTs' ~~ map (fn (x, _) => (x, NONE)) pTs;
    1.33 +	      (* dummy syntax, since required by rename *)
    1.34 +	    val pTs'' = map (fn ((p, _), (_, T)) => (p, T)) (pTs ~~ pTs');
    1.35 +	    val [env] = unify_parms ctxt pTs [map (apsnd SOME) pTs''];
    1.36 +	      (* propagate parameter types, to keep them consistent *)
    1.37 +	    val regs' = map (fn ((name, ps), wits) =>
    1.38 +		((name, map (Element.rename ren) ps),
    1.39 +		 map (Element.transfer_witness thy) wits)) regs;
    1.40 +	    val new_regs = regs';
    1.41 +	    val new_ids = map fst new_regs;
    1.42 +	    val new_idTs = map (apsnd (map (fn p => (p, (the o AList.lookup (op =) pTs) p)))) new_ids;
    1.43  
    1.44 -          val new_ths = new_regs |> map (#2 #> map
    1.45 -            (Element.instT_witness thy env #>
    1.46 -              Element.rename_witness ren #>
    1.47 -              Element.satisfy_witness ths));
    1.48 -          val new_ids' = map (fn (id, ths) =>
    1.49 -              (id, ([], Derived ths))) (new_ids ~~ new_ths);
    1.50 -        in
    1.51 -          fold add_regs new_idTs (ths @ flat new_ths, ids @ new_ids')
    1.52 -        end;
    1.53 +	    val new_wits = new_regs |> map (#2 #> map
    1.54 +	      (Element.instT_witness thy env #> Element.rename_witness ren #>
    1.55 +		Element.satisfy_witness wits));
    1.56 +	    val new_ids' = map (fn (id, wits) =>
    1.57 +		(id, ([], Derived wits))) (new_ids ~~ new_wits);
    1.58 +	    val new_idTs' = map (fn ((n, pTs), (_, ([], mode))) =>
    1.59 +		((n, pTs), mode)) (new_idTs ~~ new_ids');
    1.60 +	    val new_id = ((name, map #1 pTs), ([], mode));
    1.61 +	    val (wits', ids', visited') = fold add_with_regs new_idTs'
    1.62 +              (wits @ flat new_wits, ids, visited @ [new_id]);
    1.63 +	  in
    1.64 +	    (wits', ids' @ [new_id], visited')
    1.65 +	  end;
    1.66  
    1.67      (* distribute top-level axioms over assumed ids *)
    1.68  
    1.69 @@ -793,11 +800,8 @@
    1.70              val (ids', parms') = identify false import;
    1.71                  (* acyclic import dependencies *)
    1.72  
    1.73 -            val ids'' = ids' @ [((name, ps), ([], Assumed []))];
    1.74 -            val (_, ids''') = add_regs (name, map #1 params) ([], ids'');
    1.75 -            val (_, ids4) = chop (length ids' + 1) ids''';
    1.76 -            val ids5 = ids' @ ids4 @ [((name, ps), ([], Assumed []))];
    1.77 -            val ids_ax = if top then fst (fold_map (axiomify ps) ids5 axiom) else ids5;
    1.78 +            val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], ids', ids');
    1.79 +            val ids_ax = if top then fst (fold_map (axiomify ps) ids'' axiom) else ids'';
    1.80              in (ids_ax, merge_lists parms' ps) end
    1.81        | identify top (Rename (e, xs)) =
    1.82            let