--- a/src/HOL/Import/proof_kernel.ML Fri Sep 16 20:30:44 2005 +0200
+++ b/src/HOL/Import/proof_kernel.ML Fri Sep 16 21:02:15 2005 +0200
@@ -110,7 +110,7 @@
val new_axiom : string -> term -> theory -> theory * thm
val prin : term -> unit
-
+ val protect_factname : string -> string
end
structure ProofKernel :> ProofKernel =
@@ -427,7 +427,6 @@
end
fun mk_comb(f,a) = f $ a
-fun mk_abs(x,a) = Term.lambda x a
(* Needed for HOL Light *)
fun protect_tyvarname s =
@@ -443,6 +442,7 @@
in
s |> no_quest |> beg_prime
end
+
fun protect_varname s =
let
fun no_beg_underscore s =
@@ -453,6 +453,36 @@
s |> no_beg_underscore
end
+local
+ val sg = theory "Main"
+in
+ fun is_valid_bound_varname s = (read_cterm sg ("SOME "^s^" . True", TypeInfer.logicT); true) handle _ => false
+end
+
+fun protect_boundvarname s = if is_valid_bound_varname s then s else "u"
+
+fun mk_lambda (v as Free (x, T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t))
+ | mk_lambda (v as Var ((x, _), T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t))
+ | mk_lambda v t = raise TERM ("lambda", [v, t]);
+
+fun replacestr x y s =
+let
+ val xl = explode x
+ val yl = explode y
+ fun isprefix [] ys = true
+ | isprefix (x::xs) (y::ys) = if x = y then isprefix xs ys else false
+ | isprefix _ _ = false
+ fun isp s = isprefix xl s
+ fun chg s = yl@(List.drop (s, List.length xl))
+ fun r [] = []
+ | r (S as (s::ss)) = if isp S then r (chg S) else s::(r ss)
+in
+ implode(r (explode s))
+end
+
+fun protect_factname s = replacestr "." "_dot_" s
+fun unprotect_factname s = replacestr "_dot_" "." s
+
val ty_num_prefix = "N_"
fun startsWithDigit s = Char.isDigit (hd (String.explode s))
@@ -460,13 +490,13 @@
fun protect_tyname tyn =
let
val tyn' =
- if String.isPrefix ty_num_prefix tyn then raise (ERR "conv_ty_name" ("type name '"^tyn^"' is reserved")) else
+ if String.isPrefix ty_num_prefix tyn then raise (ERR "protect_ty_name" ("type name '"^tyn^"' is reserved")) else
(if startsWithDigit tyn then ty_num_prefix^tyn else tyn)
in
tyn'
end
-
+fun protect_constname tcn = implode (map (fn c => if c = "." then "_dot_" else c) (explode tcn))
structure TypeNet =
struct
@@ -543,7 +573,7 @@
| gtfx (Elem("tmc",atts,[])) =
let
val segment = get_segment thyname atts
- val name = get_name atts
+ val name = protect_constname(get_name atts)
in
mk_thy_const thy segment name (TypeNet.get_type_from_index thy thyname types (Lib.assoc "t" atts))
handle PK _ => prim_mk_const thy segment name
@@ -555,12 +585,12 @@
in
mk_comb(f,a)
end
- | gtfx (Elem("tml",[("x",tmx),("a",tma)],[])) =
+ | gtfx (Elem("tml",[("x",tmx),("a",tma)],[])) =
let
val x = get_term_from_index thy thyname types terms tmx
val a = get_term_from_index thy thyname types terms tma
in
- mk_abs(x,a)
+ mk_lambda x a
end
| gtfx (Elem("tmi",[("i",iS)],[])) =
get_term_from_index thy thyname types terms iS
@@ -612,7 +642,7 @@
| NONE => error "Cannot find proof files"
val _ = OS.FileSys.mkDir path handle OS.SysErr _ => ()
in
- OS.Path.joinDirFile {dir = path, file = OS.Path.joinBaseExt {base = thmname, ext = SOME "prf"}}
+ OS.Path.joinDirFile {dir = path, file = OS.Path.joinBaseExt {base = (unprotect_factname thmname), ext = SOME "prf"}}
end
fun xml_to_proof thyname types terms prf thy =
@@ -666,14 +696,14 @@
| x2p (Elem("pfact",atts,[])) =
let
val thyname = get_segment thyname atts
- val thmname = get_name atts
+ val thmname = protect_factname (get_name atts)
val p = mk_proof PDisk
val _ = set_disk_info_of p thyname thmname
in
p
end
| x2p (Elem("pdef",[("s",seg),("n",name),("i",is)],[])) =
- mk_proof (PDef(seg,name,index_to_term is))
+ mk_proof (PDef(seg,protect_constname name,index_to_term is))
| x2p (Elem("ptmspec",[("s",seg)],p::names)) =
let
val names = map (fn Elem("name",[("n",name)],[]) => name
@@ -686,7 +716,7 @@
val P = xml_to_term xP
val t = xml_to_term xt
in
- mk_proof (PTyIntro(seg,protect_tyname name,abs_name,rep_name,P,t,x2p p))
+ mk_proof (PTyIntro(seg,protect_tyname name,protect_constname abs_name,protect_constname rep_name,P,t,x2p p))
end
| x2p (Elem("ptydef",[("s",seg),("n",name)],[p])) =
mk_proof (PTyDef(seg,protect_tyname name,x2p p))