src/Tools/Code/code_preproc.ML
changeset 38291 62abd53f37fa
parent 37744 3daaf23b9ab4
child 38669 9ff76d0f0610
equal deleted inserted replaced
38250:b32a44361186 38291:62abd53f37fa
   385 fun add_cert thy vardeps (c, (proto_lhs, proto_cert)) (rhss, eqngr) =
   385 fun add_cert thy vardeps (c, (proto_lhs, proto_cert)) (rhss, eqngr) =
   386   if can (Graph.get_node eqngr) c then (rhss, eqngr)
   386   if can (Graph.get_node eqngr) c then (rhss, eqngr)
   387   else let
   387   else let
   388     val lhs = map_index (fn (k, (v, _)) =>
   388     val lhs = map_index (fn (k, (v, _)) =>
   389       (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs;
   389       (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs;
   390     val cert = Code.constrain_cert thy (map snd lhs) proto_cert;
   390     val cert = Code.constrain_cert thy (map (Sign.minimize_sort thy o snd) lhs) proto_cert;
   391     val (vs, rhss') = Code.typargs_deps_of_cert thy cert;
   391     val (vs, rhss') = Code.typargs_deps_of_cert thy cert;
   392     val eqngr' = Graph.new_node (c, (vs, cert)) eqngr;
   392     val eqngr' = Graph.new_node (c, (vs, cert)) eqngr;
   393   in (map (pair c) rhss' @ rhss, eqngr') end;
   393   in (map (pair c) rhss' @ rhss, eqngr') end;
   394 
   394 
   395 fun extend_arities_eqngr thy cs ts (arities, (eqngr : code_graph)) =
   395 fun extend_arities_eqngr thy cs ts (arities, (eqngr : code_graph)) =