internalize axiom names in Defs.define; compress types via Term.compress_type
authorobua
Mon Jun 13 21:28:57 2005 +0200 (2005-06-13)
changeset 1638490c51c932154
parent 16383 7dd0eb6e89f9
child 16385 a9dec1969348
internalize axiom names in Defs.define; compress types via Term.compress_type
src/Pure/defs.ML
     1.1 --- a/src/Pure/defs.ML	Mon Jun 13 15:10:52 2005 +0200
     1.2 +++ b/src/Pure/defs.ML	Mon Jun 13 21:28:57 2005 +0200
     1.3 @@ -71,7 +71,7 @@
     1.4  		     | Define of string * typ * string * (string * typ) list
     1.5  		     | Finalize of string * typ
     1.6  
     1.7 -type graph = int * (graphaction list) * (node Symtab.table)
     1.8 +type graph = int * (string Symtab.table) * (graphaction list) * (node Symtab.table)
     1.9               
    1.10  val CHAIN_HISTORY = 
    1.11      let
    1.12 @@ -84,7 +84,7 @@
    1.13  fun set_chain_history b = CHAIN_HISTORY := b
    1.14  fun chain_history () = !CHAIN_HISTORY
    1.15  
    1.16 -val empty = (0, [], Symtab.empty)
    1.17 +val empty = (0, Symtab.empty, [], Symtab.empty)
    1.18  
    1.19  exception DEFS of string;
    1.20  exception CIRCULAR of (typ * string * string) list;
    1.21 @@ -100,10 +100,30 @@
    1.22          if not closed then false else Symtab.is_empty edges)
    1.23      (true, defs)
    1.24  
    1.25 -fun checkT (Type (a, Ts)) = Type (a, map checkT Ts)
    1.26 -  | checkT (TVar ((a, 0), _)) = TVar ((a, 0), [])
    1.27 -  | checkT (TVar ((a, i), _)) = def_err "type is not clean"
    1.28 -  | checkT (TFree (a, _)) = TVar ((a, 0), [])
    1.29 +exception No_Change;
    1.30 +
    1.31 +fun map_nc f list = 
    1.32 +    let 
    1.33 +      val changed = ref false
    1.34 +      fun f' x = 
    1.35 +          let 
    1.36 +            val x' = f x  
    1.37 +            val _ = changed := true
    1.38 +          in
    1.39 +            x'
    1.40 +          end handle No_Change => x
    1.41 +      val list' = map f' list
    1.42 +    in
    1.43 +      if !changed then list' else raise No_Change
    1.44 +    end
    1.45 +
    1.46 +fun checkT' (t as (Type (a, Ts))) = (Type (a, map_nc checkT' Ts) handle No_Change => t)
    1.47 +  | checkT' (t as (TVar ((a, 0), []))) = raise No_Change
    1.48 +  | checkT' (t as (TVar ((a, 0), _))) = TVar ((a, 0), [])
    1.49 +  | checkT' (t as (TFree (a, _))) = TVar ((a, 0), [])
    1.50 +  | checkT' _ = def_err "type is not clean"
    1.51 +
    1.52 +fun checkT t = Term.compress_type (checkT' t handle No_Change => t)
    1.53  
    1.54  fun rename ty1 ty2 = incr_tvar ((maxidx_of_typ ty1)+1) ty2;  
    1.55  
    1.56 @@ -237,8 +257,8 @@
    1.57      
    1.58  fun merge_edges xs ys = foldl merge_edges_1 xs ys
    1.59  
    1.60 -fun declare' (g as (cost, actions, graph)) (cty as (name, ty)) =
    1.61 -    (cost, (Declare cty)::actions, 
    1.62 +fun declare' (g as (cost, axmap, actions, graph)) (cty as (name, ty)) =
    1.63 +    (cost, axmap, (Declare cty)::actions, 
    1.64       Symtab.update_new ((name, Node (ty, Symtab.empty, Symtab.empty, [], Open)), graph))
    1.65      handle Symtab.DUP _ => 
    1.66             let
    1.67 @@ -252,7 +272,28 @@
    1.68  
    1.69  fun declare g (name, ty) = declare' g (name, checkT ty)
    1.70  
    1.71 -fun define' (cost, actions, graph) (mainref, ty) axname body =
    1.72 +val axcounter = ref (IntInf.fromInt 0)
    1.73 +fun newaxname axmap axname =
    1.74 +    let
    1.75 +      val c = !axcounter
    1.76 +      val _ = axcounter := c+1
    1.77 +      val axname' = axname^"_"^(IntInf.toString c)
    1.78 +    in
    1.79 +      (Symtab.update ((axname', axname), axmap), axname')
    1.80 +    end
    1.81 +
    1.82 +fun translate_ex axmap x = 
    1.83 +    let
    1.84 +      fun translate (ty, nodename, axname) = 
    1.85 +          (ty, nodename, the (Symtab.lookup (axmap, axname)))
    1.86 +    in
    1.87 +      case x of
    1.88 +        INFINITE_CHAIN chain => raise (INFINITE_CHAIN (map translate chain))
    1.89 +      | CIRCULAR cycle => raise (CIRCULAR (map translate cycle))
    1.90 +      | _ => raise x
    1.91 +    end
    1.92 +
    1.93 +fun define' (cost, axmap, actions, graph) (mainref, ty) axname body =
    1.94      let
    1.95        val mainnode  = (case Symtab.lookup (graph, mainref) of 
    1.96  			 NONE => def_err ("constant "^mainref^" is not declared")
    1.97 @@ -474,10 +515,10 @@
    1.98        val graph = Symtab.update ((mainref, Node (gty, defs, backs, finals, closed)), graph) 
    1.99        val actions' = (Define (mainref, ty, axname, body))::actions
   1.100      in	    
   1.101 -      (cost+3,actions', graph)
   1.102 -    end 
   1.103 +      (cost+3, axmap, actions', graph)
   1.104 +    end handle ex => translate_ex axmap ex
   1.105      
   1.106 -fun define (g as (_, _, graph)) (mainref, ty) axname body =
   1.107 +fun define (g as (cost, axmap, actions, graph)) (mainref, ty) axname body =
   1.108      let
   1.109        val ty = checkT ty
   1.110        fun checkbody (n, t) = 
   1.111 @@ -489,11 +530,12 @@
   1.112              | _ => SOME (n, checkT t)
   1.113            end
   1.114        val body = distinct (List.mapPartial checkbody body)
   1.115 +      val (axmap, axname) = newaxname axmap axname
   1.116      in
   1.117 -      define' g (mainref, ty) axname body
   1.118 +      define' (cost, axmap, actions, graph) (mainref, ty) axname body
   1.119      end
   1.120  
   1.121 -fun finalize' (cost, history, graph) (noderef, ty) = 
   1.122 +fun finalize' (cost, axmap, history, graph) (noderef, ty) = 
   1.123      case Symtab.lookup (graph, noderef) of 
   1.124        NONE => def_err ("cannot finalize constant "^noderef^"; it is not declared")
   1.125      | SOME (Node (nodety, defs, backs, finals, closed)) =>
   1.126 @@ -525,7 +567,7 @@
   1.127                     SOME (final_ty :: finals))                              
   1.128        in    
   1.129          case update_finals finals of
   1.130 -          NONE => (cost, history, graph)
   1.131 +          NONE => (cost, axmap, history, graph)
   1.132          | SOME finals => 
   1.133  	  let
   1.134              val closed = if closed = Open andalso is_instance_r nodety ty then 
   1.135 @@ -583,14 +625,14 @@
   1.136                                                          finals, closed)), graph')
   1.137              val history' = (Finalize (noderef, ty)) :: history
   1.138  	  in
   1.139 -	    (cost+1, history', graph')
   1.140 +	    (cost+1, axmap, history', graph')
   1.141  	  end
   1.142        end
   1.143   
   1.144  fun finalize g (noderef, ty) = finalize' g (noderef, checkT ty) 
   1.145  
   1.146  fun merge' (Declare cty, g) = declare' g cty
   1.147 -  | merge' (Define (name, ty, axname, body), g as (_,_, graph)) = 
   1.148 +  | merge' (Define (name, ty, axname, body), g as (_,_, _, graph)) = 
   1.149      (case Symtab.lookup (graph, name) of
   1.150         NONE => define' g (name, ty) axname body
   1.151       | SOME (Node (_, defs, _, _, _)) => 
   1.152 @@ -599,13 +641,13 @@
   1.153  	| SOME _ => g))
   1.154    | merge' (Finalize finals, g) = finalize' g finals 
   1.155                         
   1.156 -fun merge (g1 as (cost1, actions1, _)) (g2 as (cost2, actions2, _)) =
   1.157 +fun merge (g1 as (cost1, _, actions1, _)) (g2 as (cost2, _, actions2, _)) =
   1.158      if cost1 < cost2 then
   1.159        foldr merge' g2 actions1
   1.160      else
   1.161        foldr merge' g1 actions2
   1.162                             
   1.163 -fun finals (cost, history, graph) = 
   1.164 +fun finals (_, _, history, graph) = 
   1.165      Symtab.foldl 
   1.166        (fn (finals, (name, Node(_, _, _, ftys, _))) => 
   1.167            Symtab.update_new ((name, ftys), finals))