src/Pure/IsaPlanner/upterm_lib.ML
author haftmann
Tue Sep 06 08:30:43 2005 +0200 (2005-09-06)
changeset 17271 2756a73f63a5
parent 16179 fa7e70be26b0
permissions -rw-r--r--
introduced some new-style AList operations
     1 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     2 (*  Title:      Pure/IsaPlanner/upterm_lib.ML
     3     ID:		$Id$
     4     Author:     Lucas Dixon, University of Edinburgh
     5                 lucas.dixon@ed.ac.uk
     6     Created:    26 Jan 2004
     7 *)
     8 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     9 (*  DESCRIPTION:
    10 
    11     generic upterms for lambda calculus  
    12 
    13 *)   
    14 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    15 
    16 
    17 signature UPTERM_LIB = 
    18 sig
    19        
    20 
    21   (* type for upterms defined in terms of a 't : a downterm type, and 
    22      'y : types for bound variable in the downterm type *)
    23   datatype ('t,'y) T =
    24            abs of string * 'y * (('t,'y) T)
    25          | appl of 't * (('t,'y) T)
    26          | appr of 't * (('t,'y) T)
    27          | root
    28 
    29   (* analysis *)
    30   val tyenv_of_upterm : ('t,'y) T -> (string * 'y) list
    31   val tyenv_of_upterm' : ('t,'y) T -> 'y list
    32   val addr_of_upterm : ('t,'y) T -> int list
    33   val upsize_of_upterm : ('t,'y) T -> int
    34   
    35   (* editing *)
    36   val map_to_upterm_parts : ('t -> 't2) * ('y -> 'y2)  -> 
    37 														('t,'y) T -> ('t2,'y2) T
    38 
    39   val expand_map_to_upterm_parts : ('t -> 't2 list) * ('y -> 'y2)  -> 
    40 																	 ('t,'y) T -> ('t2,'y2) T list
    41 
    42   val fold_upterm : ('a * 't -> 'a) -> (* left *)
    43                     ('a * 't -> 'a) ->  (* right *)
    44                     ('a * (string * 'y) -> 'a) -> (* abs *)
    45                     ('a * ('t,'y) T) -> 'a (* everything *)
    46 
    47   (* apply one term to another *)
    48   val apply : ('t,'y) T -> ('t,'y) T -> ('t,'y) T
    49 
    50 end;
    51 
    52 
    53 
    54 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    55 structure UpTermLib : UPTERM_LIB =
    56 struct 
    57 
    58   (* type for upterms defined in terms of a 't : a downterm type, and 
    59      'y : types for bound variable in the downterm type *)
    60   datatype ('t,'y) T =
    61            abs of string * 'y * ('t,'y) T
    62          | appl of 't * ('t,'y) T
    63          | appr of 't * ('t,'y) T
    64          | root;
    65 
    66   (* get the bound variable names and types for the current foucs *)
    67   fun tyenv_of_upterm (appl(l,m)) = tyenv_of_upterm m
    68     | tyenv_of_upterm (appr(r,m)) = tyenv_of_upterm m
    69     | tyenv_of_upterm (abs(s,ty,m)) = (s, ty) :: (tyenv_of_upterm m)
    70     | tyenv_of_upterm root = [];
    71 
    72   (* get the bound variable types for the current foucs *)
    73   fun tyenv_of_upterm' (appl(l,m)) = tyenv_of_upterm' m
    74     | tyenv_of_upterm' (appr(r,m)) = tyenv_of_upterm' m
    75     | tyenv_of_upterm' (abs(s,ty,m)) = ty :: (tyenv_of_upterm' m)
    76     | tyenv_of_upterm' root = [];
    77 
    78   (* an address construction for the upterm, ie if we were at the
    79      root, address describes how to get to this point. *)
    80   fun addr_of_upterm1 A root = A
    81     | addr_of_upterm1 A (appl (l,m)) = addr_of_upterm1 (1::A) m
    82     | addr_of_upterm1 A (appr (r,m)) = addr_of_upterm1 (2::A) m
    83     | addr_of_upterm1 A (abs (s,ty,m)) = addr_of_upterm1 (0::A) m;
    84 
    85   fun addr_of_upterm m = addr_of_upterm1 [] m;
    86 
    87   (* the size of the upterm, ie how far to get to root *)
    88   fun upsize_of_upterm root = 0
    89     | upsize_of_upterm (appl (l,m)) = (upsize_of_upterm m) + 1
    90     | upsize_of_upterm (appr (r,m)) = (upsize_of_upterm m) + 1
    91     | upsize_of_upterm (abs (s,ty,m)) = (upsize_of_upterm m) + 1;
    92 
    93   (* apply an upterm to to another upterm *)
    94   fun apply x root = x
    95     | apply x (appl (l,m)) = appl(l, apply x m)
    96     | apply x (appr (r,m)) = appr(r, apply x m)
    97     | apply x (abs (s,ty,m)) = abs(s, ty, apply x m);
    98 
    99   (* applies the term function to each term in each part of the upterm *)
   100   fun map_to_upterm_parts (tf,yf) root = root
   101 
   102     | map_to_upterm_parts (tf,yf) (abs(s,ty,m)) = 
   103       abs(s,yf ty,map_to_upterm_parts (tf,yf) m)
   104 
   105     | map_to_upterm_parts (tf,yf) (appr(t,m)) = 
   106       appr (tf t, map_to_upterm_parts (tf,yf) m)
   107 
   108     | map_to_upterm_parts (tf,yf) (appl(t,m)) = 
   109       appl (tf t, map_to_upterm_parts (tf,yf) m);
   110 
   111 
   112   (* applies the term function to each term in each part of the upterm *)
   113   fun expand_map_to_upterm_parts (tf,yf) root = [root]
   114     | expand_map_to_upterm_parts (tf,yf) (abs(s,ty,m)) = 
   115 			map (fn x => abs(s,yf ty, x)) 
   116 					(expand_map_to_upterm_parts (tf,yf) m)
   117     | expand_map_to_upterm_parts (tf,yf) (appr(t,m)) = 
   118       map appr (IsaPLib.all_pairs 
   119 									(tf t) (expand_map_to_upterm_parts (tf,yf) m))
   120     | expand_map_to_upterm_parts (tf,yf) (appl(t,m)) = 
   121       map appl (IsaPLib.all_pairs 
   122 									(tf t) (expand_map_to_upterm_parts (tf,yf) m));
   123 
   124   (* fold along each 't (down term) in the upterm *)
   125 	fun fold_upterm fl fr fa (d, u) = 
   126       let 
   127 	      fun fold_upterm' (d, root) = d
   128 		      | fold_upterm' (d, abs(s,ty,m)) = fold_upterm' (fa(d,(s,ty)), m)
   129 		      | fold_upterm' (d, appr(t,m)) = fold_upterm' (fr(d,t), m)
   130 		      | fold_upterm' (d, appl(t,m)) = fold_upterm' (fl(d,t), m)
   131       in fold_upterm' (d,u) end;
   132 
   133 end;