hol88-library-source 2.02.19940316-19 / usr / share / hol88-2.02.19940316 / Library / trs / extract.ml

This file is indexed.

/usr/share/hol88-2.02.19940316/Library/trs/extract.ml is in hol88-library-source 2.02.19940316-19.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below. 

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
% extract.ml                                            (c) R.J.Boulton 1990 %
%----------------------------------------------------------------------------%


% Function to take a term and return a triple:     %
% (<constants>,<free variables>,<bound variables>) %

% Set union and set difference are used to avoid generating repetitions in   %
% the lists derived. For function applications, the lists from the rator and %
% the rand can simply be joined by set union. For abstractions, the bound    %
% variable is removed from the free-variable list of the body, and is added  %
% to the bound-variable list of the body.                                    %

letrec get_ids t =

   % : (term -> (term list # term list # term list)) %

   if (is_const t) then ([t],[],[])
   if (is_var t)   then ([],[t],[])
   if (is_abs t)   then
     (let (bv,body) = dest_abs t
      in  let (cl,fvl,bvl) = get_ids body
          in  (cl,(subtract fvl [bv]),(union bvl [bv]))
     )
   if (is_comb t)  then
     (let (a,b) = dest_comb t
      in  let (cla,fvla,bvla) = get_ids a
          and (clb,fvlb,bvlb) = get_ids b
          in  (union cla clb,union fvla fvlb,union bvla bvlb)
     )
   else fail;;


% Functions to extract components from the get_ids triple %

let get_consts t = (fst o get_ids) t;;

   % : (term -> term list) %


let get_freevars t = (fst o snd o get_ids) t;;

   % : (term -> term list) %


let get_boundvars t = (snd o snd o get_ids) t;;

   % : (term -> term list) %


% Function to obtain a list of the types which occur in a term %

% The lists of constants, free-variables and bound-variables are        %
% concatenated. The resulting identifiers are converted to their types, %
% and then any repetitions are removed.                                 %

let get_types t =

   % : (term -> type list) %

   let (cl,fvl,bvl) = get_ids t
   and get_typ t = snd (dest_const t ? dest_var t)
   in  remove_rep (map get_typ (cl @ fvl @ bvl));;


%--------------------------------------------------------------------------%


% Function which applied to a HOL type returns true if the type is of the %
% form ":*..." or ":op", otherwise false is returned.                     %

let is_primtype typ = (null (snd (dest_type typ))) ? true;;

   % : (type -> bool) %


% Function which applied to a HOL type returns a list containing simply %
% the type itself if it is `primitive' or the types from which it is    %
% constructed otherwise.                                                %

let subtypes typ =

   % : (type -> type list) %

   if (is_primtype typ)
   then [typ]
   else (snd (dest_type typ));;


% Function to break-up a type into its `primitive' types %

% The function uses the predicate is_primtype, defined above. If the     %
% type is not `primitive', a list of the component types is obtained, to %
% which the function is applied recursively. The resulting list of lists %
% is then `flattened' to give a list of `primitive' types, from which    %
% any repetitions are removed.                                           %

letrec prim_subtypes typ =

   % : (type -> type list) %

   if (is_primtype typ)
   then [typ]
   else (remove_rep o flat o (map prim_subtypes) o subtypes) typ;;


% Function to obtain a list of the `primitive' types occurring in a term %

% A list of the types occurring in the term is obtained. Each of these %
% types is converted to a list of its `primitive' types. The resulting %
% list of lists is then `flattened', and any repetitions are removed.  %

let get_primtypes t =

   % : (term -> type list) %

   (remove_rep o flat o (map prim_subtypes) o get_types) t;;


% Function to obtain a list of the `primitive' polymorphic types in a term %

let get_primvartypes t = filter is_vartype (get_primtypes t);;

   % : (term -> type list) %


%----------------------------------------------------------------------------%

APT Browse - Built by Thomas Orozco.