This file is indexed.

/usr/share/hol88-2.02.19940316/contrib/hol-exec/cons.ml is in hol88-contrib-source 2.02.19940316-14.

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
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
%------ FILE cons.ml ------%
% Bug fixed in an earlier version %
% sree@cs.ubc.ca %

letrec get_final_ret_type1 cons_type =
        if ((can dest_type) cons_type) then
           let t1 = dest_type cons_type in
           if (null (snd t1)) then cons_type
           else
             if ((fst t1) = `fun`) then
              get_final_ret_type1 (hd (rev (snd t1)))
             else cons_type
        else
           failwith `not a type`;;

let get_final_ret_type cons_term =
       get_final_ret_type1 (type_of cons_term);;

let get_type_axiom_from thy const_term =
       if (is_const const_term) then
          let typ = fst (dest_type (get_final_ret_type const_term)) in
          (let thm_name = concat typ `_Axiom` in
            (get_second thm_name (theorems thy)))
       else
           failwith `get_type_axiom_from: not a constant`;;

let mk_cons_tuple_str_list1 functor arg_list =
     if (null arg_list) then
        concat `CONS__`
         (concat (const_var_to_string functor) `;; \L`)
     else
      concat `CONS__`
       (concat (const_var_to_string functor)
         (concat ` (`
           (concat (inv_words `,` (map const_var_to_string arg_list))
                   `);; \L`)));;
                    
let mk_cons_tuple_str_list thy const_term =
      let t1 = concl (get_type_axiom_from thy const_term) in
       (let list_list = get_args (skolemize t1) in
         (let functor_list = functors_of_args list_list and
              args_list = args_of_args list_list in
            (map2 (uncurry mk_cons_tuple_str_list1) (functor_list,args_list))));;

let is_constructor_from thy const_term = 
      if ((can (get_type_axiom_from thy) ) const_term) then
       let t1 = concl (get_type_axiom_from thy const_term) in
        (let list_list = get_args (skolemize t1) in
         (let functor_list = functors_of_args list_list in
           (let const_name = fst (dest_const const_term) and
                functor_name_list = map fst (map dest_const functor_list) in
           mem const_name functor_name_list)))
      else
        false;;

letrec mk_quick_cons_def_from thy const_term =
      let t1 = concl (get_type_axiom_from thy const_term) in
          (let list_list = get_args (skolemize t1) in
           (let functor_list = functors_of_args list_list in
            (let const_name = fst (dest_const const_term) and
                 functor_name_list = map fst (map dest_const functor_list) in
            (let el_index = index const_name functor_name_list in
              (let args = el el_index (args_of_args list_list) in 
               (let cons_args_term_list = const_term.args in
                (let str_list = map const_var_to_ml_string cons_args_term_list in
                (let let_str =
                  concat `let `
                  (concat (inv_words ` ` str_list)
                   (concat ` = `
                           (mk_cons_tuple_str_list1 const_term args)
                           )) in
                 let_str))))))));;

let type_map = [(`num`,`int`)];;

% Does not capture type constructors like `fun` : retain for safety
letrec mk_type_list hol_type =
      let type_pair = ((dest_type hol_type) ? ((dest_vartype hol_type),[])) in
       (let type1_str = lookup_map type_map (fst type_pair) and
            type2 = snd type_pair in
       if (null type2) then [type1_str]
       else
         append (mk_type_list (hd type2)) [type1_str]);;
%

% Fix the above %
letrec mk_type_list hol_type_list =
      if (null hol_type_list) then []
      else
      let head = hd hol_type_list in
      let type_pair = ((dest_type head) ? ((dest_vartype head),[])) in
      let first = fst type_pair and
          secnd = snd type_pair in
      if (first = `prod`) then
         [inv_words `#` (mk_type_list secnd)]
      else
      if (first = `fun`) then 
         [inv_words `->` (mk_type_list secnd)]
      else
      let type1_str = lookup_map type_map first in
        if (null secnd) then
         type1_str.(mk_type_list (tl hol_type_list))
        else
         (`(`^(inv_words `,` (mk_type_list secnd))^`)`^type1_str).
         (mk_type_list (tl hol_type_list));;
                      
let hol_to_ml_type hol_type = 
      inv_words ` ` (mk_type_list [hol_type]);;

let mk_constructor_defs_strs functor arg_type_list =
      if (null arg_type_list) then 
       concat `CONS__`
               (const_var_to_string functor)
      else
       concat `CONS__`
        (concat (const_var_to_string functor)
	  (concat ` of `
	          (inv_words ` # ` (map hol_to_ml_type arg_type_list))));;

let mk_cons_type_defs1 thy const_term =
      let t1 = concl (get_type_axiom_from thy const_term) in
          (let list_list = get_args (skolemize t1) in
           (let functor_list = functors_of_args list_list in
            (let const_name = fst (dest_const const_term) and
                 functor_name_list = map fst (map dest_const functor_list) in
            (let el_index = index const_name functor_name_list in
              (let args = el el_index (args_of_args list_list) in 
               (let arg_type_list = map type_of args in
           mk_constructor_defs_strs const_term arg_type_list))))));;

let mk_cons_type_defs_str thy cons_list_pair =
% create a unique name for the rectype%
       let rectype_name = hol_to_ml_type (fst cons_list_pair) and
           cons_list = snd cons_list_pair in
       (concat `rectype `
	 (concat rectype_name
	   (concat ` = `
% We could also sort the cons_list according to type minimality,
  though its not required by ML - but we will just use reverse %
	     (concat (inv_words `| ` (map (mk_cons_type_defs1 thy) (rev cons_list)))
                     `;;\L\L`))));;

let map_map f l = map (map f) l;;
letrec mapl l1 l2 =
    if (null l1) then []
    else
       ((hd l1) (hd l2)). (mapl (tl l1) (tl l2));;

let mk_pair_list l1 l2 =
     mapl (map pair l1) l2;;

letrec mk_groups_of_same_type cons_list_pair =
      if (null cons_list_pair) then []
      else
         let type_eq term1 term2 =
                 (snd term1) = 
                 (snd term2) in
         (let type1_list_pair = (sublist (type_eq (hd cons_list_pair)) 
                                                   cons_list_pair) in
           (let cons_list_pair1 = subtract cons_list_pair type1_list_pair in
            (let type1_list = map fst type1_list_pair and
                 type1 = (snd (hd type1_list_pair)) in
             ((type1,type1_list).(mk_groups_of_same_type cons_list_pair1)))));;

let mk_cons_type_defs thy cons_list =
       (let type_list = map get_final_ret_type cons_list in
% We should actually sort the type groups according to containment,
  but we will for the moment assume a reverse order creation: %
        (let cons_list_list = rev 
                               (mk_groups_of_same_type 
                                  (mk_pair_list cons_list type_list)) in
             map (mk_cons_type_defs_str thy) cons_list_list));;


% The following is too complicated and unnecessary
letrec mk_groups_of_same_type cons_list =
      if (null cons_list) then []
      else
         let type_eq term1 term2 =
                 type_of term1 = type_of term2 in
         (let type1_list = sublist (type_eq (hd cons_list)) cons_list in
           (let cons_list1 = subtract cons_list type1_list in
             (type1_list.(mk_groups_of_same_type cons_list1))));;

let map_map f l = map (map f) l;;
letrec mapl l1 l2 =
    if (null l1) then []
    else
       ((hd l1) (hd l2)). (mapl (tl l1) (tl l2));;

let mk_cons_type_defs1 cons_list =
          (let list_list = map get_args (map skolemize cons_list) in
           (let functor_list_list = map functors_of_args list_list in
            (let const_name_list = map fst (map dest_const cons_list) and
                 functor_name_list_list = map_map fst 
                                     (map_map dest_const functor_list_list) in
            (let el_index_list = mapl (map index const_name_list) 
                                        functor_name_list_list in
              (let args_list_list = map_map type_of
                                        (mapl (map el el_index_list)
                                          (map args_of_args list_list)) in 
               mk_cons_defs cons_list args_list_list)))));;
    
let mk_cons_type_defs thy cons_list =
       let t1_list = map concl (map (get_type_axiom_from thy) cons_list) in
        (let cons_list_list = mk_groups_of_same_type cons_list in
         (let def_str_list = map mk_cons_type_defs1 cons_list_list in
           def_str_list));;



%