# HG changeset patch # User wenzelm # Date 1737029664 -3600 # Node ID 4bb6c49ef791cb69f69c47fd528ceb13cb20950f # Parent 6c60f773033f5f5b82f31a017c01dcc204fb34aa clarified signature: more explicit operations; diff -r 6c60f773033f -r 4bb6c49ef791 src/HOL/Import/import_rule.ML --- a/src/HOL/Import/import_rule.ML Thu Jan 16 12:45:48 2025 +0100 +++ b/src/HOL/Import/import_rule.ML Thu Jan 16 13:14:24 2025 +0100 @@ -289,14 +289,22 @@ |> forall_elim_list rng end -val transl_dot = String.translate (fn #"." => "dot" | c => Char.toString c) +val make_name = String.translate (fn #"." => "dot" | c => Char.toString c) + +fun make_free (x, ty) = Free (make_name x, ty) -val transl_qm = String.translate (fn #"?" => "t" | c => Char.toString c) +fun make_tfree a = + let val b = "'" ^ String.translate (fn #"?" => "t" | c => Char.toString c) a + in TFree (b, \<^sort>\type\) end -fun getconstname s thy = - case Import_Data.get_const_map s thy of - SOME s => s - | NONE => Sign.full_name thy (Binding.name (transl_dot s)) +fun make_const thy (c, ty) = + let + val d = + (case Import_Data.get_const_map c thy of + SOME d => d + | NONE => Sign.full_name thy (Binding.name (make_name c))) + in Const (d, ty) end + fun gettyname s thy = case Import_Data.get_typ_map s thy of SOME s => s @@ -398,7 +406,7 @@ | process tstate (#"F", [name, t]) = let val (tm, (thy, state)) = gettm t tstate - val (th, thy) = def (transl_dot name) tm thy + val (th, thy) = def (make_name name) tm thy in setth th (thy, state) end @@ -414,20 +422,20 @@ end | process (thy, state) (#"Y", [name, _, _]) = setth (mtydef name thy) (thy, state) | process (thy, state) (#"t", [n]) = - setty (Thm.global_ctyp_of thy (TFree ("'" ^ transl_qm n, \<^sort>\type\))) (thy, state) + setty (Thm.global_ctyp_of thy (make_tfree n)) (thy, state) | process (thy, state) (#"a", n :: l) = fold_map getty l (thy, state) |>> (fn tys => Thm.global_ctyp_of thy (Type (gettyname n thy, map Thm.typ_of tys))) |-> setty | process (thy, state) (#"v", [n, ty]) = - getty ty (thy, state) |>> (fn ty => Thm.global_cterm_of thy (Free (transl_dot n, Thm.typ_of ty))) |-> settm + getty ty (thy, state) |>> (fn ty => Thm.global_cterm_of thy (make_free (n, Thm.typ_of ty))) |-> settm | process (thy, state) (#"c", [n, ty]) = - getty ty (thy, state) |>> (fn ty => Thm.global_cterm_of thy (Const (getconstname n thy, Thm.typ_of ty))) |-> settm + getty ty (thy, state) |>> (fn ty => Thm.global_cterm_of thy (make_const thy (n, Thm.typ_of ty))) |-> settm | process tstate (#"f", [t1, t2]) = gettm t1 tstate ||>> gettm t2 |>> (fn (t1, t2) => Thm.apply t1 t2) |-> settm | process tstate (#"l", [t1, t2]) = gettm t1 tstate ||>> gettm t2 |>> (fn (t1, t2) => Thm.lambda t1 t2) |-> settm | process (thy, state) (#"+", [s]) = - (store_thm (Binding.name (transl_dot s)) (last_thm state) thy, state) + (store_thm (Binding.name (make_name s)) (last_thm state) thy, state) | process _ (c, _) = error ("process: unknown command: " ^ String.implode [c]) fun parse_line s =