# HG changeset patch # User wenzelm # Date 1737107003 -3600 # Node ID 35abb6dd8bd27b86edd91a5eb10a63ad72179bd8 # Parent 9e25f6e2748c541611d1ed10e4d5a5524265fe30 clarified signature: more standard Isabelle/ML; diff -r 9e25f6e2748c -r 35abb6dd8bd2 src/HOL/Import/import_data.ML --- a/src/HOL/Import/import_data.ML Thu Jan 16 23:20:44 2025 +0100 +++ b/src/HOL/Import/import_data.ML Fri Jan 17 10:43:23 2025 +0100 @@ -7,10 +7,10 @@ signature IMPORT_DATA = sig - val get_const_map : string -> theory -> string option - val get_typ_map : string -> theory -> string option - val get_const_def : string -> theory -> thm option - val get_typ_def : string -> theory -> thm option + val get_const_map : theory -> string -> string option + val get_typ_map : theory -> string -> string option + val get_const_def : theory -> string -> thm option + val get_typ_def : theory -> string -> thm option val add_const_map : string -> string -> theory -> theory val add_const_map_cmd : string -> string -> theory -> theory @@ -37,13 +37,13 @@ } ) -fun get_const_map s thy = Symtab.lookup (#const_map (Data.get thy)) s +val get_const_map = Symtab.lookup o #const_map o Data.get -fun get_typ_map s thy = Symtab.lookup (#ty_map (Data.get thy)) s +val get_typ_map = Symtab.lookup o #ty_map o Data.get -fun get_const_def s thy = Symtab.lookup (#const_def (Data.get thy)) s +val get_const_def = Symtab.lookup o #const_def o Data.get -fun get_typ_def s thy = Symtab.lookup (#ty_def (Data.get thy)) s +val get_typ_def = Symtab.lookup o #ty_def o Data.get fun add_const_map s1 s2 thy = Data.map (fn {const_map, ty_map, const_def, ty_def} => diff -r 9e25f6e2748c -r 35abb6dd8bd2 src/HOL/Import/import_rule.ML --- a/src/HOL/Import/import_rule.ML Thu Jan 16 23:20:44 2025 +0100 +++ b/src/HOL/Import/import_rule.ML Fri Jan 17 10:43:23 2025 +0100 @@ -18,12 +18,12 @@ val conj2 : thm -> thm val refl : cterm -> thm val abs : cterm -> thm -> thm - val mdef : string -> theory -> thm + val mdef : theory -> string -> thm val def : string -> cterm -> theory -> thm * theory - val mtydef : string -> theory -> thm + val mtydef : theory -> string -> thm val tydef : string -> string -> string -> cterm -> cterm -> thm -> theory -> thm * theory - val inst_type : (ctyp * ctyp) list -> thm -> theory -> thm + val inst_type : theory -> (ctyp * ctyp) list -> thm -> thm val inst : (cterm * cterm) list -> thm -> thm type state @@ -178,18 +178,18 @@ (meta_eq_to_obj_eq def_thm, thy2) end -fun mdef name thy = - case Import_Data.get_const_def name thy of +fun mdef thy name = + case Import_Data.get_const_def thy name of SOME th => th | NONE => error ("constant mapped but no definition: " ^ name) fun def constname rhs thy = - case Import_Data.get_const_def constname thy of + case Import_Data.get_const_def thy constname of SOME _ => let val () = warning ("Const mapped but def provided: " ^ constname) in - (mdef constname thy, thy) + (mdef thy constname, thy) end | NONE => def' constname rhs thy @@ -199,7 +199,7 @@ by (metis type_definition.Rep_inverse type_definition.Abs_inverse type_definition.Rep mem_Collect_eq)} -fun typedef_hollight th thy = +fun typedef_hollight thy th = let val (th_s, cn) = Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th)) val (th_s, abst) = Thm.dest_comb th_s @@ -248,22 +248,22 @@ (th4, thy') end -fun mtydef name thy = - case Import_Data.get_typ_def name thy of - SOME thn => meta_mp (typedef_hollight thn thy) thn +fun mtydef thy name = + case Import_Data.get_typ_def thy name of + SOME thn => meta_mp (typedef_hollight thy thn) thn | NONE => error ("type mapped but no tydef thm registered: " ^ name) fun tydef tycname abs_name rep_name P t td_th thy = - case Import_Data.get_typ_def tycname thy of + case Import_Data.get_typ_def thy tycname of SOME _ => let val () = warning ("Type mapped but proofs provided: " ^ tycname) in - (mtydef tycname thy, thy) + (mtydef thy tycname, thy) end | NONE => tydef' tycname abs_name rep_name P t td_th thy -fun inst_type lambda th thy = +fun inst_type thy lambda th = let fun assoc _ [] = error "assoc" | assoc x ((x',y)::rest) = if x = x' then y else assoc x rest @@ -300,13 +300,13 @@ fun make_const thy (c, ty) = let val d = - (case Import_Data.get_const_map c thy of + (case Import_Data.get_const_map thy c 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 +fun gettyname thy s = + case Import_Data.get_typ_map thy s of SOME s => s | NONE => Sign.full_name thy (Binding.name s) @@ -393,7 +393,7 @@ val (th, tstate) = getth th (thy, state) val (tys, tstate) = fold_map getty tys tstate in - setth (inst_type (pairList tys) th thy) tstate + setth (inst_type thy (pairList tys) th) tstate end | process tstate (#"S", l) = let @@ -410,7 +410,7 @@ in setth th (thy, state) end - | process (thy, state) (#"F", [name]) = setth (mdef name thy) (thy, state) + | process (thy, state) (#"F", [name]) = setth (mdef thy name) (thy, state) | process tstate (#"Y", [name, absname, repname, t1, t2, th]) = let val (th, tstate) = getth th tstate @@ -420,12 +420,12 @@ in setth th (thy, state) end - | process (thy, state) (#"Y", [name, _, _]) = setth (mtydef name thy) (thy, state) + | process (thy, state) (#"Y", [name, _, _]) = setth (mtydef thy name) (thy, state) | process (thy, state) (#"t", [n]) = 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 + (fn tys => Thm.global_ctyp_of thy (Type (gettyname thy n, map Thm.typ_of tys))) |-> setty | process (thy, state) (#"v", [n, ty]) = 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]) =