src/Pure/defs.ML
author obua
Tue Jun 07 06:39:39 2005 +0200 (2005-06-07)
changeset 16308 636a1a84977a
parent 16198 cfd070a2cc4d
child 16361 cb31cb768a6c
permissions -rw-r--r--
1) Fixed bug in Defs.merge_edges_1.
2) Major optimization of Defs.define: do not store dependencies between constants that
cannot introduce cycles anyway. In that way, the cycle test adds almost no overhead to
theories that define their constants in HOL-light / HOL4 style.
3) Cleaned up Defs.graph, no superfluous name tags are stored anymore.
     1 (*  Title:      Pure/General/defs.ML
     2     ID:         $Id$
     3     Author:     Steven Obua, TU Muenchen
     4 
     5     Checks if definitions preserve consistency of logic by enforcing 
     6     that there are no cyclic definitions. The algorithm is described in 
     7     "An Algorithm for Determining Definitional Cycles in Higher-Order Logic with Overloading", 
     8     Steven Obua, technical report, to be written :-)
     9 *)
    10 
    11 signature DEFS = sig
    12     
    13   type graph
    14        
    15   exception DEFS of string
    16   exception CIRCULAR of (typ * string * string) list
    17   exception INFINITE_CHAIN of (typ * string * string) list 
    18   exception FINAL of string * typ
    19   exception CLASH of string * string * string
    20                      
    21   val empty : graph
    22   val declare : graph -> string * typ -> graph  (* exception DEFS *)
    23   val define : graph -> string * typ -> string -> (string * typ) list -> graph 
    24     (* exception DEFS, CIRCULAR, INFINITE_CHAIN, CLASH, FINAL *)   
    25                                                                      
    26   val finalize : graph -> string * typ -> graph (* exception DEFS *)
    27 
    28   val finals : graph -> (typ list) Symtab.table
    29 
    30   val merge : graph -> graph -> graph (* exception CIRCULAR, INFINITE_CHAIN, CLASH *)
    31 
    32   (* If set to true then the exceptions CIRCULAR and INFINITE_CHAIN return the full
    33      chain of definitions that lead to the exception. In the beginning, chain_history 
    34      is initialized with the Isabelle environment variable DEFS_CHAIN_HISTORY. *)
    35   val set_chain_history : bool -> unit
    36   val chain_history : unit -> bool
    37 
    38 end
    39 
    40 structure Defs :> DEFS = struct
    41 
    42 type tyenv = Type.tyenv
    43 type edgelabel = (int * typ * typ * (typ * string * string) list)
    44 
    45 datatype node = Node of
    46          typ  (* most general type of constant *)
    47          * defnode Symtab.table  
    48              (* a table of defnodes, each corresponding to 1 definition of the 
    49                 constant for a particular type, indexed by axiom name *)
    50          * (unit Symtab.table) Symtab.table 
    51              (* a table of all back referencing defnodes to this node, 
    52                 indexed by node name of the defnodes *)
    53          * typ list (* a list of all finalized types *)
    54      
    55      and defnode = Defnode of
    56          typ  (* type of the constant in this particular definition *)
    57          * (edgelabel list) Symtab.table (* The edges, grouped by nodes. *)
    58 
    59 fun getnode graph noderef = the (Symtab.lookup (graph, noderef))
    60 fun get_nodedefs (Node (_, defs, _, _)) = defs
    61 fun get_defnode (Node (_, defs, _, _)) defname = Symtab.lookup (defs, defname)
    62 fun get_defnode' graph noderef defname = 
    63     Symtab.lookup (get_nodedefs (the (Symtab.lookup (graph, noderef))), defname)
    64 
    65 datatype graphaction = Declare of string * typ
    66 		     | Define of string * typ * string * (string * typ) list
    67 		     | Finalize of string * typ
    68 
    69 type graph = int * (graphaction list) * (node Symtab.table)
    70              
    71 val CHAIN_HISTORY = 
    72     let
    73       fun f c = if Char.isSpace c then "" else String.str (Char.toUpper c) 
    74       val env = String.translate f (getenv "DEFS_CHAIN_HISTORY")
    75     in
    76       ref (env = "ON" orelse env = "TRUE")
    77     end
    78 
    79 fun set_chain_history b = CHAIN_HISTORY := b
    80 fun chain_history () = !CHAIN_HISTORY
    81 
    82 val empty = (0, [], Symtab.empty)
    83 
    84 exception DEFS of string;
    85 exception CIRCULAR of (typ * string * string) list;
    86 exception INFINITE_CHAIN of (typ * string * string) list;
    87 exception CLASH of string * string * string;
    88 exception FINAL of string * typ;
    89 
    90 fun def_err s = raise (DEFS s)
    91 
    92 fun checkT (Type (a, Ts)) = Type (a, map checkT Ts)
    93   | checkT (TVar ((a, 0), _)) = TVar ((a, 0), [])
    94   | checkT (TVar ((a, i), _)) = def_err "type is not clean"
    95   | checkT (TFree (a, _)) = TVar ((a, 0), [])
    96 
    97 fun declare' (cost, actions, g) (cty as (name, ty)) =
    98     (cost, (Declare cty)::actions, 
    99      Symtab.update_new ((name, Node (ty, Symtab.empty, Symtab.empty, [])), g))
   100     handle Symtab.DUP _ => def_err "constant is already declared"
   101 
   102 fun declare g (name, ty) = declare' g (name, checkT ty)
   103 
   104 fun rename ty1 ty2 = incr_tvar ((maxidx_of_typ ty1)+1) ty2;  
   105 
   106 fun subst_incr_tvar inc t =
   107     if (inc > 0) then 
   108       let
   109 	val tv = typ_tvars t
   110 	val t' = incr_tvar inc t
   111 	fun update_subst (((n,i), _), s) =
   112 	    Vartab.update (((n, i), ([], TVar ((n, i+inc), []))), s)
   113       in
   114 	(t',List.foldl update_subst Vartab.empty tv)
   115       end	
   116     else
   117       (t, Vartab.empty)
   118     
   119 fun subst s ty = Envir.norm_type s ty
   120                  
   121 fun subst_history s history = map (fn (ty, cn, dn) => (subst s ty, cn, dn)) history
   122                               
   123 fun is_instance instance_ty general_ty =
   124     Type.typ_instance Type.empty_tsig (instance_ty, general_ty)
   125     
   126 fun is_instance_r instance_ty general_ty =
   127     is_instance instance_ty (rename instance_ty general_ty)
   128     
   129 fun unify ty1 ty2 = 
   130     SOME (fst (Type.unify Type.empty_tsig (Vartab.empty, 0) (ty1, ty2)))
   131     handle Type.TUNIFY => NONE
   132                             
   133 (* 
   134    Unifies ty1 and ty2, renaming ty1 and ty2 so that they have greater indices than max and 
   135    so that they are different. All indices in ty1 and ty2 are supposed to be less than or 
   136    equal to max.
   137    Returns SOME (max', s1, s2), so that s1(ty1) = s2(ty2) and max' is greater or equal than 
   138    all indices in s1, s2, ty1, ty2.
   139 *)
   140 fun unify_r max ty1 ty2 = 
   141     let
   142       val max = Int.max(max, 0)
   143       val max1 = max (* >= maxidx_of_typ ty1 *)
   144       val max2 = max (* >= maxidx_of_typ ty2 *)
   145       val max = Int.max(max, Int.max (max1, max2))
   146       val (ty1, s1) = subst_incr_tvar (max + 1) ty1
   147       val (ty2, s2) = subst_incr_tvar (max + max1 + 2) ty2
   148       val max = max + max1 + max2 + 2	
   149       fun merge a b = Vartab.merge (fn _ => false) (a, b)
   150     in
   151       case unify ty1 ty2 of
   152 	NONE => NONE
   153       | SOME s => SOME (max, merge s1 s, merge s2 s)
   154     end
   155     
   156 fun can_be_unified_r ty1 ty2 =
   157     let
   158       val ty2 = rename ty1 ty2
   159     in
   160       case unify ty1 ty2 of
   161 	NONE => false
   162       | _ => true
   163     end
   164     
   165 fun can_be_unified ty1 ty2 =
   166     case unify ty1 ty2 of
   167       NONE => false
   168     | _ => true
   169            
   170 structure Inttab = TableFun(type key = int val ord = int_ord);
   171 
   172 fun normalize_edge_idx (edge as (maxidx, u1, v1, history)) =
   173     if maxidx <= 1000000 then edge else
   174     let
   175       
   176       fun idxlist idx extract_ty inject_ty (tab, max) ts = 
   177           foldr 
   178             (fn (e, ((tab, max), ts)) => 
   179                 let
   180                   val ((tab, max), ty) = idx (tab, max) (extract_ty e)
   181                   val e = inject_ty (ty, e)
   182                 in
   183                   ((tab, max), e::ts)
   184                 end)
   185             ((tab,max), []) ts
   186           
   187       fun idx (tab,max) (TVar ((a,i),_)) = 
   188           (case Inttab.lookup (tab, i) of 
   189              SOME j => ((tab, max), TVar ((a,j),[]))
   190            | NONE => ((Inttab.update ((i, max), tab), max+1), TVar ((a,max),[])))
   191         | idx (tab,max) (Type (t, ts)) = 
   192           let 
   193             val ((tab, max), ts) = idxlist idx I fst (tab, max) ts
   194           in
   195             ((tab,max), Type (t, ts))
   196           end
   197         | idx (tab, max) ty = ((tab, max), ty)
   198       
   199       val ((tab,max), u1) = idx (Inttab.empty, 0) u1
   200       val ((tab,max), v1) = idx (tab, max) v1
   201       val ((tab,max), history) = 
   202           idxlist idx
   203             (fn (ty,_,_) => ty) 
   204             (fn (ty, (_, s1, s2)) => (ty, s1, s2)) 
   205             (tab, max) history
   206     in
   207       (max, u1, v1, history)
   208     end
   209                         
   210 fun compare_edges (e1 as (maxidx1, u1, v1, history1)) (e2 as (maxidx2, u2, v2, history2)) =
   211     let
   212       val t1 = u1 --> v1
   213       val t2 = incr_tvar (maxidx1+1) (u2 --> v2)
   214     in
   215       if (is_instance t1 t2) then
   216 	(if is_instance t2 t1 then
   217 	   SOME (int_ord (length history2, length history1))
   218 	 else
   219 	   SOME LESS)
   220       else if (is_instance t2 t1) then
   221 	SOME GREATER
   222       else
   223 	NONE
   224     end
   225 
   226 fun merge_edges_1 (x, []) = [x]
   227   | merge_edges_1 (x, (y::ys)) = 
   228     (case compare_edges x y of
   229        SOME LESS => (y::ys)
   230      | SOME EQUAL => (y::ys)
   231      | SOME GREATER => merge_edges_1 (x, ys)
   232      | NONE => y::(merge_edges_1 (x, ys)))
   233     
   234 fun merge_edges xs ys = foldl merge_edges_1 xs ys
   235 
   236 fun define' (cost, actions, graph) (mainref, ty) axname body =
   237     let
   238       val mainnode  = (case Symtab.lookup (graph, mainref) of 
   239 			 NONE => def_err ("constant "^mainref^" is not declared")
   240 		       | SOME n => n)
   241       val (Node (gty, defs, backs, finals)) = mainnode
   242       val _ = (if is_instance_r ty gty then () 
   243                else def_err "type of constant does not match declared type")
   244       fun check_def (s, Defnode (ty', _)) = 
   245           (if can_be_unified_r ty ty' then 
   246 	     raise (CLASH (mainref, axname, s))
   247 	   else if s = axname then
   248 	     def_err "name of axiom is already used for another definition of this constant"
   249 	   else false)	
   250       val _ = Symtab.exists check_def defs
   251       fun check_final finalty = 
   252 	  (if can_be_unified_r finalty ty then
   253 	     raise (FINAL (mainref, finalty))
   254 	   else
   255 	     true)
   256       val _ = forall check_final finals
   257 	             
   258       (* now we know that the only thing that can prevent acceptance of the definition 
   259          is a cyclic dependency *)
   260 
   261       fun insert_edges edges (nodename, links) =
   262           (if links = [] then 
   263              edges
   264            else
   265              let
   266                val links = map normalize_edge_idx links
   267              in
   268                Symtab.update ((nodename, 
   269 	                       case Symtab.lookup (edges, nodename) of
   270 	                         NONE => links
   271 	                       | SOME links' => merge_edges links' links),
   272                               edges)
   273              end)
   274 	 
   275       fun make_edges ((bodyn, bodyty), edges) =
   276 	  let
   277 	    val bnode = 
   278 		(case Symtab.lookup (graph, bodyn) of 
   279 		   NONE => def_err "body of constant definition references undeclared constant"
   280 		 | SOME x => x)
   281 	    val (Node (general_btyp, bdefs, bbacks, bfinals)) = bnode
   282 	  in
   283 	    case unify_r 0 bodyty general_btyp of
   284 	      NONE => edges
   285 	    | SOME (maxidx, sigma1, sigma2) => 
   286               if exists (is_instance_r bodyty) bfinals then 
   287                 edges
   288               else
   289 	        let
   290 		  fun insert_trans_edges ((step1, edges), (nodename, links)) =
   291                       let
   292                         val (maxidx1, alpha1, beta1, defname) = step1
   293                         fun connect (maxidx2, alpha2, beta2, history) = 
   294 		            case unify_r (Int.max (maxidx1, maxidx2)) beta1 alpha2 of
   295 		              NONE => NONE
   296 		            | SOME (max, sleft, sright) =>				  
   297 			      SOME (max, subst sleft alpha1, subst sright beta2, 
   298                                     if !CHAIN_HISTORY then   
   299 			              ((subst sleft beta1, bodyn, defname)::
   300 				       (subst_history sright history))
   301                                     else [])            
   302                         val links' = List.mapPartial connect links
   303                       in
   304                         (step1, insert_edges edges (nodename, links'))
   305                       end
   306                                                                 
   307                   fun make_edges' ((swallowed, edges),
   308                                    (def_name, Defnode (def_ty, def_edges))) =
   309 		      if swallowed then
   310 		        (swallowed, edges)
   311 		      else 
   312 		        (case unify_r 0 bodyty def_ty of
   313 			   NONE => (swallowed, edges)
   314 		         | SOME (maxidx, sigma1, sigma2) => 
   315 			   (is_instance_r bodyty def_ty,
   316                             snd (Symtab.foldl insert_trans_edges 
   317                               (((maxidx, subst sigma1 ty, subst sigma2 def_ty, def_name),
   318                                 edges), def_edges))))
   319           	  val (swallowed, edges) = Symtab.foldl make_edges' ((false, edges), bdefs)
   320 	        in
   321 		  if swallowed then 
   322 		    edges
   323 		  else 
   324                     insert_edges edges 
   325                     (bodyn, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])
   326 	        end
   327 	  end 
   328                     
   329       val edges = foldl make_edges Symtab.empty body
   330                   				               
   331       (* We also have to add the backreferences that this new defnode induces. *)  
   332       fun install_backrefs (graph, (noderef, links)) =
   333           if links <> [] then
   334             let
   335               val (Node (ty, defs, backs, finals)) = getnode graph noderef
   336               val defnames =
   337                   (case Symtab.lookup (backs, mainref) of
   338                      NONE => Symtab.empty
   339                    | SOME s => s)
   340               val defnames' = Symtab.update_new ((axname, ()), defnames)
   341               val backs' = Symtab.update ((mainref,defnames'), backs)
   342             in
   343               Symtab.update ((noderef, Node (ty, defs, backs', finals)), graph)
   344             end
   345           else
   346             graph
   347             
   348       val graph = Symtab.foldl install_backrefs (graph, edges)
   349                   
   350       val (Node (_, _, backs, _)) = getnode graph mainref
   351       val thisDefnode = Defnode (ty, edges)
   352       val graph = Symtab.update ((mainref, Node (gty, Symtab.update_new 
   353         ((axname, thisDefnode), defs), backs, finals)), graph)
   354 		                
   355       (* Now we have to check all backreferences to this node and inform them about 
   356          the new defnode. In this section we also check for circularity. *)
   357       fun update_backrefs ((backs, graph), (noderef, defnames)) =
   358 	  let
   359 	    fun update_defs ((defnames, graph),(defname, _)) =
   360 		let
   361                   val (Node (nodety, nodedefs, nodebacks, nodefinals)) = getnode graph noderef
   362 		  val (Defnode (def_ty, defnode_edges)) = 
   363                       the (Symtab.lookup (nodedefs, defname))
   364 		  val edges = the (Symtab.lookup (defnode_edges, mainref))
   365  					
   366 	          (* the type of thisDefnode is ty *)
   367 		  fun update (e as (max, alpha, beta, history), (changed, edges)) = 
   368 		      case unify_r max beta ty of
   369 			NONE => (changed, e::edges)
   370 		      | SOME (max', s_beta, s_ty) =>
   371 			let
   372 			  val alpha' = subst s_beta alpha
   373 			  val ty' = subst s_ty ty				      
   374 			  val _ = 
   375 			      if noderef = mainref andalso defname = axname then
   376 				(case unify alpha' ty' of
   377 				   NONE => 
   378 				   if (is_instance_r ty' alpha') then
   379 				     raise (INFINITE_CHAIN (
   380 					    (alpha', mainref, axname)::
   381 					    (subst_history s_beta history)@
   382 					    [(ty', mainref, axname)]))
   383 				   else ()
   384 				 | SOME s => 
   385                                    raise (CIRCULAR (
   386 					  (subst s alpha', mainref, axname)::
   387 					  (subst_history s (subst_history s_beta history))@
   388 					  [(subst s ty', mainref, axname)])))
   389 			      else ()                             
   390 			in
   391 			  if is_instance_r beta ty then
   392 			    (true, edges)
   393 			  else
   394 			    (changed, e::edges)
   395 			end		    			   			       
   396                   
   397                   val (changed, edges') = foldl update (false, []) edges
   398                   val defnames' = if edges' = [] then 
   399                                     defnames 
   400                                   else 
   401                                     Symtab.update ((defname, ()), defnames)
   402                 in
   403                   if changed then
   404                     let
   405                       val defnode_edges' = 
   406                           if edges' = [] then
   407                             Symtab.delete mainref defnode_edges
   408                           else
   409                             Symtab.update ((mainref, edges'), defnode_edges)
   410                       val defnode' = Defnode (def_ty, defnode_edges')
   411                       val nodedefs' = Symtab.update ((defname, defnode'), nodedefs)
   412                       val graph' = 
   413                           Symtab.update 
   414                             ((noderef, Node (nodety, nodedefs', nodebacks, nodefinals)),graph) 
   415                     in
   416                       (defnames', graph')
   417                     end
   418                   else
   419                     (defnames', graph)
   420                 end
   421 		    
   422 	    val (defnames', graph') = Symtab.foldl update_defs 
   423                                                    ((Symtab.empty, graph), defnames)
   424 	  in
   425 	    if Symtab.is_empty defnames' then 
   426 	      (backs, graph')
   427 	    else
   428 	      let
   429 		val backs' = Symtab.update_new ((noderef, defnames'), backs)
   430 	      in
   431 		(backs', graph')
   432 	      end
   433 	  end
   434         
   435       val (backs, graph) = Symtab.foldl update_backrefs ((Symtab.empty, graph), backs)
   436                                         						 
   437       (* If a Circular exception is thrown then we never reach this point. *)
   438       val (Node (gty, defs, _, finals)) = getnode graph mainref
   439       val graph = Symtab.update ((mainref, Node (gty, defs, backs, finals)), graph) 
   440     in	    
   441       (cost+3,(Define (mainref, ty, axname, body))::actions, graph)
   442     end 
   443     
   444 fun define g (mainref, ty) axname body =
   445     let
   446       val ty = checkT ty
   447       val body = distinct (map (fn (n,t) => (n, checkT t)) body)
   448     in
   449       define' g (mainref, ty) axname body
   450     end
   451 
   452 fun finalize' (cost, history, graph) (noderef, ty) = 
   453     case Symtab.lookup (graph, noderef) of 
   454       NONE => def_err ("cannot finalize constant "^noderef^"; it is not declared")
   455     | SOME (Node (nodety, defs, backs, finals)) =>
   456       let 
   457 	val _ = 
   458             if (not (is_instance_r ty nodety)) then
   459 	      def_err ("only type instances of the declared constant "^
   460                        noderef^" can be finalized")
   461 	    else ()
   462 	val _ = Symtab.exists 
   463                   (fn (def_name, Defnode (def_ty, _)) =>  
   464 		      if can_be_unified_r ty def_ty then 
   465 			def_err ("cannot finalize constant "^noderef^
   466                                  "; clash with definition "^def_name)
   467 		      else 
   468 			false)
   469 		  defs 
   470         
   471         fun update_finals [] = SOME [ty]
   472           | update_finals (final_ty::finals) = 
   473             (if is_instance_r ty final_ty then NONE
   474              else
   475                case update_finals finals of
   476                  NONE => NONE
   477                | (r as SOME finals) =>
   478                  if (is_instance_r final_ty ty) then
   479                    r
   480                  else
   481                    SOME (final_ty :: finals))                              
   482       in    
   483         case update_finals finals of
   484           NONE => (cost, history, graph)
   485         | SOME finals => 
   486 	  let
   487 	    val graph = Symtab.update ((noderef, Node(nodety, defs, backs, finals)), 
   488                                        graph)
   489 	                
   490 	    fun update_backref ((graph, backs), (backrefname, backdefnames)) =
   491 		let
   492 		  fun update_backdef ((graph, defnames), (backdefname, _)) = 
   493 	              let 
   494 			val (backnode as Node (backty, backdefs, backbacks, backfinals)) = 
   495                             getnode graph backrefname
   496 			val (Defnode (def_ty, all_edges)) = 
   497                             the (get_defnode backnode backdefname)
   498 
   499 			val (defnames', all_edges') = 
   500 			    case Symtab.lookup (all_edges, noderef) of
   501 			      NONE => sys_error "finalize: corrupt backref"
   502 			    | SOME edges =>
   503 			      let
   504 				val edges' = List.filter (fn (_, _, beta, _) => 
   505                                                              not (is_instance_r beta ty)) edges
   506 			      in
   507 				if edges' = [] then 
   508 				  (defnames, Symtab.delete noderef all_edges)
   509 				else
   510 				  (Symtab.update ((backdefname, ()), defnames), 
   511 				   Symtab.update ((noderef, edges'), all_edges))
   512 			      end
   513 			val defnode' = Defnode (def_ty, all_edges')
   514 			val backnode' = 
   515                             Node (backty, 
   516                                   Symtab.update ((backdefname, defnode'), backdefs), 
   517 				  backbacks, backfinals)
   518 		      in
   519 			(Symtab.update ((backrefname, backnode'), graph), defnames') 
   520 		      end
   521 	              
   522 		  val (graph', defnames') = 
   523                       Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames)
   524 		in
   525 		  (graph', if Symtab.is_empty defnames' then backs 
   526 			   else Symtab.update ((backrefname, defnames'), backs))
   527 		end
   528 	    val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs)
   529 	    val Node ( _, defs, _, _) = getnode graph' noderef
   530 	    val graph' = Symtab.update ((noderef, Node (nodety, defs, backs', finals)), graph')
   531 	  in
   532 	    (cost+1,(Finalize (noderef, ty)) :: history, graph')
   533 	  end
   534       end
   535  
   536 fun finalize g (noderef, ty) = finalize' g (noderef, checkT ty)
   537 
   538 fun merge' (Declare cty, g) = (declare' g cty handle _ => g)
   539   | merge' (Define (name, ty, axname, body), g as (_,_, graph)) = 
   540     (case Symtab.lookup (graph, name) of
   541        NONE => define' g (name, ty) axname body
   542      | SOME (Node (_, defs, _, _)) => 
   543        (case Symtab.lookup (defs, axname) of
   544 	  NONE => define' g (name, ty) axname body
   545 	| SOME _ => g))
   546   | merge' (Finalize finals, g) = finalize' g finals 
   547                        
   548 fun merge (g1 as (cost1, actions1, _)) (g2 as (cost2, actions2, _)) =
   549     if cost1 < cost2 then
   550       foldr merge' g2 actions1
   551     else
   552       foldr merge' g1 actions2
   553                            
   554 fun finals (cost, history, graph) = 
   555     Symtab.foldl 
   556       (fn (finals, (name, Node(_, _, _, ftys))) => Symtab.update_new ((name, ftys), finals))  
   557       (Symtab.empty, graph)
   558 
   559 end;
   560 		
   561 (*
   562 
   563 fun tvar name = TVar ((name, 0), [])
   564 
   565 val bool = Type ("bool", [])
   566 val int = Type ("int", [])
   567 val lam = Type("lam", [])
   568 val alpha = tvar "'a"
   569 val beta = tvar "'b"
   570 val gamma = tvar "'c"
   571 fun pair a b = Type ("pair", [a,b])
   572 fun prm a = Type ("prm", [a])
   573 val name = Type ("name", [])
   574 
   575 val _ = print "make empty"
   576 val g = Defs.empty 
   577 
   578 val _ = print "declare perm"
   579 val g = Defs.declare g ("perm", prm alpha --> beta --> beta)
   580 
   581 val _ = print "declare permF"
   582 val g = Defs.declare g ("permF", prm alpha --> lam --> lam)
   583 
   584 val _ = print "define perm (1)"
   585 val g = Defs.define g ("perm", prm alpha --> (beta --> gamma) --> (beta --> gamma)) "perm_fun" 
   586         [("perm", prm alpha --> gamma --> gamma), ("perm", prm alpha --> beta --> beta)]
   587 
   588 val _ = print "define permF (1)"
   589 val g = Defs.define g ("permF", prm alpha --> lam --> lam) "permF_app"
   590         ([("perm", prm alpha --> lam --> lam),
   591          ("perm", prm alpha --> lam --> lam),
   592          ("perm", prm alpha --> lam --> lam),
   593          ("perm", prm alpha --> name --> name)])
   594 
   595 val _ = print "define perm (2)"
   596 val g = Defs.define g ("perm", prm alpha --> lam --> lam) "perm_lam"
   597         [("permF", (prm alpha --> lam --> lam))]
   598 
   599 *)