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