src/HOL/Tools/Metis/metis_reconstruct.ML
changeset 43268 c0eaa8b9bff5
parent 43262 547a02d889f5
child 43278 1fbdcebb364b
child 43294 0271fda2a83a
equal deleted inserted replaced
43267:dd38b8ef52b9 43268:c0eaa8b9bff5
    55 fun atp_name_from_metis s =
    55 fun atp_name_from_metis s =
    56   case find_first (fn (_, (s', _)) => s' = s) metis_name_table of
    56   case find_first (fn (_, (s', _)) => s' = s) metis_name_table of
    57     SOME ((s, _), (_, swap)) => (s, swap)
    57     SOME ((s, _), (_, swap)) => (s, swap)
    58   | _ => (s, false)
    58   | _ => (s, false)
    59 fun atp_term_from_metis (Metis_Term.Fn (s, tms)) =
    59 fun atp_term_from_metis (Metis_Term.Fn (s, tms)) =
    60     let val (s, swap) = atp_name_from_metis s in
    60     let val (s, swap) = atp_name_from_metis (Metis_Name.toString s) in
    61       ATerm (s, tms |> map atp_term_from_metis |> swap ? rev)
    61       ATerm (s, tms |> map atp_term_from_metis |> swap ? rev)
    62     end
    62     end
    63   | atp_term_from_metis (Metis_Term.Var s) = ATerm (s, [])
    63   | atp_term_from_metis (Metis_Term.Var s) = ATerm (Metis_Name.toString s, [])
    64 
    64 
    65 fun hol_term_from_metis ctxt sym_tab =
    65 fun hol_term_from_metis ctxt sym_tab =
    66   atp_term_from_metis #> term_from_atp ctxt false sym_tab NONE
    66   atp_term_from_metis #> term_from_atp ctxt false sym_tab NONE
    67 
    67 
    68 fun atp_literal_from_metis (pos, atom) =
    68 fun atp_literal_from_metis (pos, atom) =
   158              | TYPE _ =>
   158              | TYPE _ =>
   159                (trace_msg ctxt (fn () => "\"hol_term_from_metis\" failed for " ^ x ^
   159                (trace_msg ctxt (fn () => "\"hol_term_from_metis\" failed for " ^ x ^
   160                                          " in " ^ Display.string_of_thm ctxt i_th);
   160                                          " in " ^ Display.string_of_thm ctxt i_th);
   161                 NONE)
   161                 NONE)
   162       fun remove_typeinst (a, t) =
   162       fun remove_typeinst (a, t) =
   163             case strip_prefix_and_unascii schematic_var_prefix a of
   163         let val a = Metis_Name.toString a in
   164                 SOME b => SOME (b, t)
   164           case strip_prefix_and_unascii schematic_var_prefix a of
   165               | NONE => case strip_prefix_and_unascii tvar_prefix a of
   165             SOME b => SOME (b, t)
   166                 SOME _ => NONE          (*type instantiations are forbidden!*)
   166           | NONE =>
   167               | NONE => SOME (a,t)    (*internal Metis var?*)
   167             case strip_prefix_and_unascii tvar_prefix a of
       
   168               SOME _ => NONE (* type instantiations are forbidden *)
       
   169             | NONE => SOME (a, t) (* internal Metis var? *)
       
   170         end
   168       val _ = trace_msg ctxt (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
   171       val _ = trace_msg ctxt (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
   169       val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
   172       val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
   170       val (vars, tms) =
   173       val (vars, tms) =
   171         ListPair.unzip (map_filter subst_translation substs)
   174         ListPair.unzip (map_filter subst_translation substs)
   172         ||> reveal_old_skolems_and_infer_types ctxt old_skolems
   175         ||> reveal_old_skolems_and_infer_types ctxt old_skolems
   347                         SOME t => " fol-term: " ^ Metis_Term.toString t
   350                         SOME t => " fol-term: " ^ Metis_Term.toString t
   348                       | NONE => ""))
   351                       | NONE => ""))
   349       fun path_finder tm [] _ = (tm, Bound 0)
   352       fun path_finder tm [] _ = (tm, Bound 0)
   350         | path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
   353         | path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
   351           let
   354           let
   352             val s = s |> perhaps (try (strip_prefix_and_unascii const_prefix
   355             val s = s |> Metis_Name.toString
       
   356                       |> perhaps (try (strip_prefix_and_unascii const_prefix
   353                                        #> the #> unmangled_const_name))
   357                                        #> the #> unmangled_const_name))
   354           in
   358           in
   355             if s = metis_predicator orelse s = predicator_name orelse
   359             if s = metis_predicator orelse s = predicator_name orelse
   356                s = metis_type_tag orelse s = type_tag_name then
   360                s = metis_type_tag orelse s = type_tag_name then
   357               path_finder tm ps (nth ts p)
   361               path_finder tm ps (nth ts p)
   420             val t_pairs = map Meson.term_pair_of (Vartab.dest tenv)
   424             val t_pairs = map Meson.term_pair_of (Vartab.dest tenv)
   421             val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
   425             val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
   422         in  th'  end
   426         in  th'  end
   423         handle THM _ => th;
   427         handle THM _ => th;
   424 
   428 
   425 fun is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix s)
   429 fun is_metis_literal_genuine (_, (s, _)) =
       
   430   not (String.isPrefix class_prefix (Metis_Name.toString s))
   426 fun is_isabelle_literal_genuine t =
   431 fun is_isabelle_literal_genuine t =
   427   case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false | _ => true
   432   case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false | _ => true
   428 
   433 
   429 fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
   434 fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
   430 
   435