src/HOL/Tools/inductive_codegen.ML
changeset 17144 6642e0f96f44
parent 16861 7446b4be013b
child 17261 193b84a70ca4
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Aug 25 09:29:05 2005 +0200
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Aug 25 16:10:16 2005 +0200
     1.3 @@ -375,30 +375,31 @@
     1.4          else [Pretty.str ")"])))
     1.5    end;
     1.6  
     1.7 -fun strip_spaces s = implode (fst (take_suffix (equal " ") (explode s)));
     1.8 -
     1.9 -fun modename thy thyname thyname' s (iss, is) = space_implode "__"
    1.10 -  (mk_const_id (sign_of thy) thyname thyname' (strip_spaces s) ::
    1.11 -    map (space_implode "_" o map string_of_int) (List.mapPartial I iss @ [is]));
    1.12 +fun modename module s (iss, is) gr =
    1.13 +  let val (gr', id) = if s = "op =" then (gr, ("", "equal"))
    1.14 +    else mk_const_id module s gr
    1.15 +  in (gr', space_implode "__"
    1.16 +    (mk_qual_id module id ::
    1.17 +      map (space_implode "_" o map string_of_int) (List.mapPartial I iss @ [is])))
    1.18 +  end;
    1.19  
    1.20 -fun compile_expr thy defs dep thyname brack thynames (gr, (NONE, t)) =
    1.21 -      apsnd single (invoke_codegen thy defs dep thyname brack (gr, t))
    1.22 -  | compile_expr _ _ _ _ _ _ (gr, (SOME _, Var ((name, _), _))) =
    1.23 +fun compile_expr thy defs dep module brack (gr, (NONE, t)) =
    1.24 +      apsnd single (invoke_codegen thy defs dep module brack (gr, t))
    1.25 +  | compile_expr _ _ _ _ _ (gr, (SOME _, Var ((name, _), _))) =
    1.26        (gr, [Pretty.str name])
    1.27 -  | compile_expr thy defs dep thyname brack thynames (gr, (SOME (Mode (mode, ms)), t)) =
    1.28 +  | compile_expr thy defs dep module brack (gr, (SOME (Mode (mode, ms)), t)) =
    1.29        let
    1.30          val (Const (name, _), args) = strip_comb t;
    1.31 -        val (gr', ps) = foldl_map
    1.32 -          (compile_expr thy defs dep thyname true thynames) (gr, ms ~~ args);
    1.33 +        val (gr', (ps, mode_id)) = foldl_map
    1.34 +            (compile_expr thy defs dep module true) (gr, ms ~~ args) |>>>
    1.35 +          modename module name mode;
    1.36        in (gr', (if brack andalso not (null ps) then
    1.37          single o parens o Pretty.block else I)
    1.38            (List.concat (separate [Pretty.brk 1]
    1.39 -            ([Pretty.str (modename thy thyname
    1.40 -                (if name = "op =" then ""
    1.41 -                 else the (assoc (thynames, name))) name mode)] :: ps))))
    1.42 +            ([Pretty.str mode_id] :: ps))))
    1.43        end;
    1.44  
    1.45 -fun compile_clause thy defs gr dep thyname all_vs arg_vs modes thynames (iss, is) (ts, ps) =
    1.46 +fun compile_clause thy defs gr dep module all_vs arg_vs modes (iss, is) (ts, ps) =
    1.47    let
    1.48      val modes' = modes @ List.mapPartial
    1.49        (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
    1.50 @@ -411,7 +412,7 @@
    1.51  
    1.52      fun compile_eq (gr, (s, t)) =
    1.53        apsnd (Pretty.block o cons (Pretty.str (s ^ " = ")) o single)
    1.54 -        (invoke_codegen thy defs dep thyname false (gr, t));
    1.55 +        (invoke_codegen thy defs dep module false (gr, t));
    1.56  
    1.57      val (in_ts, out_ts) = get_args is 1 ts;
    1.58      val ((all_vs', eqs), in_ts') =
    1.59 @@ -424,14 +425,14 @@
    1.60      fun compile_prems out_ts' vs names gr [] =
    1.61            let
    1.62              val (gr2, out_ps) = foldl_map
    1.63 -              (invoke_codegen thy defs dep thyname false) (gr, out_ts);
    1.64 +              (invoke_codegen thy defs dep module false) (gr, out_ts);
    1.65              val (gr3, eq_ps) = foldl_map compile_eq (gr2, eqs);
    1.66              val ((names', eqs'), out_ts'') =
    1.67                foldl_map check_constrt ((names, []), out_ts');
    1.68              val (nvs, out_ts''') = foldl_map distinct_v
    1.69                ((names', map (fn x => (x, [x])) vs), out_ts'');
    1.70              val (gr4, out_ps') = foldl_map
    1.71 -              (invoke_codegen thy defs dep thyname false) (gr3, out_ts''');
    1.72 +              (invoke_codegen thy defs dep module false) (gr3, out_ts''');
    1.73              val (gr5, eq_ps') = foldl_map compile_eq (gr4, eqs')
    1.74            in
    1.75              (gr5, compile_match (snd nvs) (eq_ps @ eq_ps') out_ps'
    1.76 @@ -449,7 +450,7 @@
    1.77              val (nvs, out_ts'') = foldl_map distinct_v
    1.78                ((names', map (fn x => (x, [x])) vs), out_ts');
    1.79              val (gr0, out_ps) = foldl_map
    1.80 -              (invoke_codegen thy defs dep thyname false) (gr, out_ts'');
    1.81 +              (invoke_codegen thy defs dep module false) (gr, out_ts'');
    1.82              val (gr1, eq_ps) = foldl_map compile_eq (gr0, eqs)
    1.83            in
    1.84              (case p of
    1.85 @@ -457,15 +458,15 @@
    1.86                   let
    1.87                     val (in_ts, out_ts''') = get_args js 1 us;
    1.88                     val (gr2, in_ps) = foldl_map
    1.89 -                     (invoke_codegen thy defs dep thyname false) (gr1, in_ts);
    1.90 +                     (invoke_codegen thy defs dep module false) (gr1, in_ts);
    1.91                     val (gr3, ps) = if is_ind t then
    1.92                         apsnd (fn ps => ps @ [Pretty.brk 1, mk_tuple in_ps])
    1.93 -                         (compile_expr thy defs dep thyname false thynames
    1.94 +                         (compile_expr thy defs dep module false
    1.95                             (gr2, (mode, t)))
    1.96                       else
    1.97                         apsnd (fn p => conv_ntuple us t
    1.98                           [Pretty.str "Seq.of_list", Pretty.brk 1, p])
    1.99 -                           (invoke_codegen thy defs dep thyname true (gr2, t));
   1.100 +                           (invoke_codegen thy defs dep module true (gr2, t));
   1.101                     val (gr4, rest) = compile_prems out_ts''' vs' (fst nvs) gr3 ps';
   1.102                   in
   1.103                     (gr4, compile_match (snd nvs) eq_ps out_ps
   1.104 @@ -475,7 +476,7 @@
   1.105                   end
   1.106               | Sidecond t =>
   1.107                   let
   1.108 -                   val (gr2, side_p) = invoke_codegen thy defs dep thyname true (gr1, t);
   1.109 +                   val (gr2, side_p) = invoke_codegen thy defs dep module true (gr1, t);
   1.110                     val (gr3, rest) = compile_prems [] vs' (fst nvs) gr2 ps';
   1.111                   in
   1.112                     (gr3, compile_match (snd nvs) eq_ps out_ps
   1.113 @@ -490,23 +491,25 @@
   1.114      (gr', Pretty.block [Pretty.str "Seq.single inp :->", Pretty.brk 1, prem_p])
   1.115    end;
   1.116  
   1.117 -fun compile_pred thy defs gr dep thyname prfx all_vs arg_vs modes thynames s cls mode =
   1.118 -  let val (gr', cl_ps) = foldl_map (fn (gr, cl) => compile_clause thy defs
   1.119 -    gr dep thyname all_vs arg_vs modes thynames mode cl) (gr, cls)
   1.120 +fun compile_pred thy defs gr dep module prfx all_vs arg_vs modes s cls mode =
   1.121 +  let val (gr', (cl_ps, mode_id)) =
   1.122 +    foldl_map (fn (gr, cl) => compile_clause thy defs
   1.123 +      gr dep module all_vs arg_vs modes mode cl) (gr, cls) |>>>
   1.124 +    modename module s mode
   1.125    in
   1.126      ((gr', "and "), Pretty.block
   1.127        ([Pretty.block (separate (Pretty.brk 1)
   1.128 -         (Pretty.str (prfx ^ modename thy thyname thyname s mode) ::
   1.129 +         (Pretty.str (prfx ^ mode_id) ::
   1.130             map Pretty.str arg_vs) @
   1.131           [Pretty.str " inp ="]),
   1.132          Pretty.brk 1] @
   1.133         List.concat (separate [Pretty.str " ++", Pretty.brk 1] (map single cl_ps))))
   1.134    end;
   1.135  
   1.136 -fun compile_preds thy defs gr dep thyname all_vs arg_vs modes thynames preds =
   1.137 +fun compile_preds thy defs gr dep module all_vs arg_vs modes preds =
   1.138    let val ((gr', _), prs) = foldl_map (fn ((gr, prfx), (s, cls)) =>
   1.139      foldl_map (fn ((gr', prfx'), mode) => compile_pred thy defs gr'
   1.140 -      dep thyname prfx' all_vs arg_vs modes thynames s cls mode)
   1.141 +      dep module prfx' all_vs arg_vs modes s cls mode)
   1.142          ((gr, prfx), valOf (assoc (modes, s)))) ((gr, "fun "), preds)
   1.143    in
   1.144      (gr', space_implode "\n\n" (map Pretty.string_of (List.concat prs)) ^ ";\n\n")
   1.145 @@ -516,13 +519,11 @@
   1.146  
   1.147  exception Modes of
   1.148    (string * (int list option list * int list) list) list *
   1.149 -  (string * (int list list option list * int list list)) list *
   1.150 -  string;
   1.151 +  (string * (int list list option list * int list list)) list;
   1.152  
   1.153 -fun lookup_modes gr dep = foldl (fn ((xs, ys, z), (xss, yss, zss)) =>
   1.154 -    (xss @ xs, yss @ ys, zss @ map (rpair z o fst) ys)) ([], [], [])
   1.155 -  (map ((fn (SOME (Modes x), _, _) => x | _ => ([], [], "")) o Graph.get_node gr)
   1.156 -    (Graph.all_preds gr [dep]));
   1.157 +fun lookup_modes gr dep = apfst List.concat (apsnd List.concat (ListPair.unzip
   1.158 +  (map ((fn (SOME (Modes x), _, _) => x | _ => ([], [])) o get_node gr)
   1.159 +    (Graph.all_preds (fst gr) [dep]))));
   1.160  
   1.161  fun print_factors factors = message ("Factors:\n" ^
   1.162    space_implode "\n" (map (fn (s, (fs, f)) => s ^ ": " ^
   1.163 @@ -537,17 +538,18 @@
   1.164        NONE => xs
   1.165      | SOME xs' => xs inter xs') :: constrain cs ys;
   1.166  
   1.167 -fun mk_extra_defs thy defs gr dep names ts =
   1.168 +fun mk_extra_defs thy defs gr dep names module ts =
   1.169    Library.foldl (fn (gr, name) =>
   1.170      if name mem names then gr
   1.171      else (case get_clauses thy name of
   1.172          NONE => gr
   1.173        | SOME (names, thyname, intrs) =>
   1.174 -          mk_ind_def thy defs gr dep names thyname [] [] (prep_intrs intrs)))
   1.175 +          mk_ind_def thy defs gr dep names (if_library thyname module)
   1.176 +            [] [] (prep_intrs intrs)))
   1.177              (gr, foldr add_term_consts [] ts)
   1.178  
   1.179 -and mk_ind_def thy defs gr dep names thyname modecs factorcs intrs =
   1.180 -  Graph.add_edge (hd names, dep) gr handle Graph.UNDEF _ =>
   1.181 +and mk_ind_def thy defs gr dep names module modecs factorcs intrs =
   1.182 +  add_edge (hd names, dep) gr handle Graph.UNDEF _ =>
   1.183      let
   1.184        val _ $ (_ $ _ $ u) = Logic.strip_imp_concl (hd intrs);
   1.185        val (_, args) = strip_comb u;
   1.186 @@ -584,9 +586,9 @@
   1.187          | add_prod_factors _ (fs, _) = fs;
   1.188  
   1.189        val gr' = mk_extra_defs thy defs
   1.190 -        (Graph.add_edge (hd names, dep)
   1.191 -          (Graph.new_node (hd names, (NONE, "", "")) gr)) (hd names) names intrs;
   1.192 -      val (extra_modes, extra_factors, extra_thynames) = lookup_modes gr' (hd names);
   1.193 +        (add_edge (hd names, dep)
   1.194 +          (new_node (hd names, (NONE, "", "")) gr)) (hd names) names module intrs;
   1.195 +      val (extra_modes, extra_factors) = lookup_modes gr' (hd names);
   1.196        val fs = constrain factorcs (map (apsnd dest_factors)
   1.197          (Library.foldl (add_prod_factors extra_factors) ([], List.concat (map (fn t =>
   1.198            Logic.strip_imp_concl t :: Logic.strip_imp_prems t) intrs))));
   1.199 @@ -599,40 +601,42 @@
   1.200          (infer_modes thy extra_modes factors arg_vs clauses);
   1.201        val _ = print_factors factors;
   1.202        val _ = print_modes modes;
   1.203 -      val (gr'', s) = compile_preds thy defs gr' (hd names) thyname (terms_vs intrs)
   1.204 -        arg_vs (modes @ extra_modes)
   1.205 -        (map (rpair thyname o fst) factors @ extra_thynames) clauses;
   1.206 +      val (gr'', s) = compile_preds thy defs gr' (hd names) module (terms_vs intrs)
   1.207 +        arg_vs (modes @ extra_modes) clauses;
   1.208      in
   1.209 -      (Graph.map_node (hd names)
   1.210 -        (K (SOME (Modes (modes, factors, thyname)), thyname, s)) gr'')
   1.211 +      (map_node (hd names)
   1.212 +        (K (SOME (Modes (modes, factors)), module, s)) gr'')
   1.213      end;
   1.214  
   1.215 -fun find_mode s u modes is = (case find_first (fn Mode ((_, js), _) => is=js)
   1.216 +fun find_mode gr dep s u modes is = (case find_first (fn Mode ((_, js), _) => is=js)
   1.217    (modes_of modes u handle Option => []) of
   1.218 -     NONE => error ("No such mode for " ^ s ^ ": " ^ string_of_mode ([], is))
   1.219 +     NONE => codegen_error gr dep
   1.220 +       ("No such mode for " ^ s ^ ": " ^ string_of_mode ([], is))
   1.221     | mode => mode);
   1.222  
   1.223 -fun mk_ind_call thy defs gr dep thyname t u is_query = (case head_of u of
   1.224 +fun mk_ind_call thy defs gr dep module t u is_query = (case head_of u of
   1.225    Const (s, T) => (case (get_clauses thy s, get_assoc_code thy s T) of
   1.226         (NONE, _) => NONE
   1.227 -     | (SOME (names, thyname', intrs), NONE) =>
   1.228 +     | (SOME (names, thyname, intrs), NONE) =>
   1.229           let
   1.230            fun mk_mode (((ts, mode), i), Const ("dummy_pattern", _)) =
   1.231                  ((ts, mode), i+1)
   1.232              | mk_mode (((ts, mode), i), t) = ((ts @ [t], mode @ [i]), i+1);
   1.233  
   1.234 +           val module' = if_library thyname module;
   1.235             val gr1 = mk_extra_defs thy defs
   1.236 -             (mk_ind_def thy defs gr dep names thyname' [] [] (prep_intrs intrs)) dep names [u];
   1.237 -           val (modes, factors, thynames) = lookup_modes gr1 dep;
   1.238 +             (mk_ind_def thy defs gr dep names module'
   1.239 +             [] [] (prep_intrs intrs)) dep names module' [u];
   1.240 +           val (modes, factors) = lookup_modes gr1 dep;
   1.241             val ts = split_prod [] (snd (valOf (assoc (factors, s)))) t;
   1.242             val (ts', is) = if is_query then
   1.243                 fst (Library.foldl mk_mode ((([], []), 1), ts))
   1.244               else (ts, 1 upto length ts);
   1.245 -           val mode = find_mode s u modes is;
   1.246 +           val mode = find_mode gr1 dep s u modes is;
   1.247             val (gr2, in_ps) = foldl_map
   1.248 -             (invoke_codegen thy defs dep thyname false) (gr1, ts');
   1.249 +             (invoke_codegen thy defs dep module false) (gr1, ts');
   1.250             val (gr3, ps) =
   1.251 -             compile_expr thy defs dep thyname false thynames (gr2, (mode, u))
   1.252 +             compile_expr thy defs dep module false (gr2, (mode, u))
   1.253           in
   1.254             SOME (gr3, Pretty.block
   1.255               (ps @ [Pretty.brk 1, mk_tuple in_ps]))
   1.256 @@ -640,17 +644,19 @@
   1.257       | _ => NONE)
   1.258    | _ => NONE);
   1.259  
   1.260 -fun list_of_indset thy defs gr dep thyname brack u = (case head_of u of
   1.261 +fun list_of_indset thy defs gr dep module brack u = (case head_of u of
   1.262    Const (s, T) => (case (get_clauses thy s, get_assoc_code thy s T) of
   1.263         (NONE, _) => NONE
   1.264 -     | (SOME (names, thyname', intrs), NONE) =>
   1.265 +     | (SOME (names, thyname, intrs), NONE) =>
   1.266           let
   1.267 +           val module' = if_library thyname module;
   1.268             val gr1 = mk_extra_defs thy defs
   1.269 -             (mk_ind_def thy defs gr dep names thyname' [] [] (prep_intrs intrs)) dep names [u];
   1.270 -           val (modes, factors, thynames) = lookup_modes gr1 dep;
   1.271 -           val mode = find_mode s u modes [];
   1.272 +             (mk_ind_def thy defs gr dep names module'
   1.273 +             [] [] (prep_intrs intrs)) dep names module' [u];
   1.274 +           val (modes, factors) = lookup_modes gr1 dep;
   1.275 +           val mode = find_mode gr1 dep s u modes [];
   1.276             val (gr2, ps) =
   1.277 -             compile_expr thy defs dep thyname false thynames (gr1, (mode, u))
   1.278 +             compile_expr thy defs dep module false (gr1, (mode, u))
   1.279           in
   1.280             SOME (gr2, (if brack then parens else I)
   1.281               (Pretty.block ([Pretty.str "Seq.list_of", Pretty.brk 1,
   1.282 @@ -671,54 +677,56 @@
   1.283    in
   1.284      rename_term
   1.285        (Logic.list_implies (prems_of eqn, HOLogic.mk_Trueprop (HOLogic.mk_mem
   1.286 -        (foldr1 HOLogic.mk_prod (ts @ [u]), Const (s ^ " ",
   1.287 +        (foldr1 HOLogic.mk_prod (ts @ [u]), Const (s ^ "_aux",
   1.288            HOLogic.mk_setT (foldr1 HOLogic.mk_prodT (Ts @ [U])))))))
   1.289    end;
   1.290  
   1.291 -fun mk_fun thy defs name eqns dep thyname thyname' gr =
   1.292 -  let
   1.293 -    val fun_id = mk_const_id (sign_of thy) thyname' thyname' name;
   1.294 -    val call_id = mk_const_id (sign_of thy) thyname thyname' name
   1.295 -  in (Graph.add_edge (name, dep) gr handle Graph.UNDEF _ =>
   1.296 +fun mk_fun thy defs name eqns dep module module' gr =
   1.297 +  case try (get_node gr) name of
   1.298 +    NONE =>
   1.299      let
   1.300        val clauses = map clause_of_eqn eqns;
   1.301 -      val pname = name ^ " ";
   1.302 +      val pname = name ^ "_aux";
   1.303        val arity = length (snd (strip_comb (fst (HOLogic.dest_eq
   1.304          (HOLogic.dest_Trueprop (concl_of (hd eqns)))))));
   1.305        val mode = 1 upto arity;
   1.306 +      val (gr', (fun_id, mode_id)) = gr |>
   1.307 +        mk_const_id module' name |>>>
   1.308 +        modename module' pname ([], mode);
   1.309        val vars = map (fn i => Pretty.str ("x" ^ string_of_int i)) mode;
   1.310        val s = Pretty.string_of (Pretty.block
   1.311 -        [mk_app false (Pretty.str ("fun " ^ fun_id)) vars, Pretty.str " =",
   1.312 +        [mk_app false (Pretty.str ("fun " ^ snd fun_id)) vars, Pretty.str " =",
   1.313           Pretty.brk 1, Pretty.str "Seq.hd", Pretty.brk 1,
   1.314 -         parens (Pretty.block [Pretty.str (modename thy thyname' thyname' pname ([], mode)),
   1.315 +         parens (Pretty.block [Pretty.str mode_id,
   1.316             Pretty.brk 1, mk_tuple vars])]) ^ ";\n\n";
   1.317 -      val gr' = mk_ind_def thy defs (Graph.add_edge (name, dep)
   1.318 -        (Graph.new_node (name, (NONE, thyname', s)) gr)) name [pname] thyname'
   1.319 +      val gr'' = mk_ind_def thy defs (add_edge (name, dep)
   1.320 +        (new_node (name, (NONE, module', s)) gr')) name [pname] module'
   1.321          [(pname, [([], mode)])]
   1.322          [(pname, map (fn i => replicate i 2) (0 upto arity-1))]
   1.323          clauses;
   1.324 -      val (modes, _, _) = lookup_modes gr' dep;
   1.325 -      val _ = find_mode pname (snd (HOLogic.dest_mem (HOLogic.dest_Trueprop
   1.326 +      val (modes, _) = lookup_modes gr'' dep;
   1.327 +      val _ = find_mode gr'' dep pname (snd (HOLogic.dest_mem (HOLogic.dest_Trueprop
   1.328          (Logic.strip_imp_concl (hd clauses))))) modes mode
   1.329 -    in gr' end, call_id)
   1.330 -  end;
   1.331 +    in (gr'', mk_qual_id module fun_id) end
   1.332 +  | SOME _ =>
   1.333 +      (add_edge (name, dep) gr, mk_qual_id module (get_const_id name gr));
   1.334  
   1.335 -fun inductive_codegen thy defs gr dep thyname brack (Const ("op :", _) $ t $ u) =
   1.336 -      ((case mk_ind_call thy defs gr dep thyname (Term.no_dummy_patterns t) u false of
   1.337 +fun inductive_codegen thy defs gr dep module brack (Const ("op :", _) $ t $ u) =
   1.338 +      ((case mk_ind_call thy defs gr dep module (Term.no_dummy_patterns t) u false of
   1.339           NONE => NONE
   1.340         | SOME (gr', call_p) => SOME (gr', (if brack then parens else I)
   1.341             (Pretty.block [Pretty.str "?! (", call_p, Pretty.str ")"])))
   1.342 -        handle TERM _ => mk_ind_call thy defs gr dep thyname t u true)
   1.343 -  | inductive_codegen thy defs gr dep thyname brack t = (case strip_comb t of
   1.344 +        handle TERM _ => mk_ind_call thy defs gr dep module t u true)
   1.345 +  | inductive_codegen thy defs gr dep module brack t = (case strip_comb t of
   1.346        (Const (s, _), ts) => (case Symtab.lookup (#eqns (CodegenData.get thy), s) of
   1.347 -        NONE => list_of_indset thy defs gr dep thyname brack t
   1.348 +        NONE => list_of_indset thy defs gr dep module brack t
   1.349        | SOME eqns =>
   1.350            let
   1.351 -            val (_, (_, thyname')) = split_last eqns;
   1.352 +            val (_, (_, thyname)) = split_last eqns;
   1.353              val (gr', id) = mk_fun thy defs s (preprocess thy (map fst eqns))
   1.354 -              dep thyname thyname' gr;
   1.355 +              dep module (if_library thyname module) gr;
   1.356              val (gr'', ps) = foldl_map
   1.357 -              (invoke_codegen thy defs dep thyname true) (gr', ts);
   1.358 +              (invoke_codegen thy defs dep module true) (gr', ts);
   1.359            in SOME (gr'', mk_app brack (Pretty.str id) ps)
   1.360            end)
   1.361      | _ => NONE);
   1.362 @@ -745,8 +753,8 @@
   1.363  
   1.364  fun ?! s = isSome (Seq.pull s);    
   1.365  
   1.366 -fun op_61__1 x = Seq.single x;
   1.367 +fun equal__1 x = Seq.single x;
   1.368  
   1.369 -val op_61__2 = op_61__1;
   1.370 +val equal__2 = equal__1;
   1.371  
   1.372 -fun op_61__1_2 (x, y) = ?? (x = y);
   1.373 +fun equal__1_2 (x, y) = ?? (x = y);