# HG changeset patch
# User obua
# Date 1126897335 -7200
# Node ID df77edc4f5d0c83dc319559fb9f2a3cce7f7ac56
# Parent  a358da1a021851b530d0e7e8474e6147cfef4770
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions

diff -r a358da1a0218 -r df77edc4f5d0 src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Fri Sep 16 20:30:44 2005 +0200
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Fri Sep 16 21:02:15 2005 +0200
@@ -28,9 +28,9 @@
   DEF_IND_SUC
   DEF_IND_0
   DEF_NUM_REP
-  TYDEF_sum
+ (* TYDEF_sum
   DEF_INL
-  DEF_INR;
+  DEF_INR*);
 
 type_maps
   ind > Nat.ind
@@ -38,8 +38,8 @@
   fun > fun
   N_1 >  Product_Type.unit
   prod > "*"
-  num > nat
-  sum > "+";
+  num > nat;
+ (* sum > "+";*)
 
 const_maps
   T > True
@@ -73,9 +73,17 @@
   "*" > "op *" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   "-" > "op -" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   BIT0 > HOLLightCompat.NUMERAL_BIT0
-  BIT1 > HOL4Compat.NUMERAL_BIT1
-  INL > Sum_Type.Inl
-  INR > Sum_Type.Inr;
+  BIT1 > HOL4Compat.NUMERAL_BIT1;
+ (* INL > Sum_Type.Inl
+  INR > Sum_Type.Inr
+  HAS_SIZE > HOLLightCompat.HAS_SIZE*)
+
+(*import_until "TYDEF_sum"
+
+consts
+print_theorems
+
+import_until *)
 
 end_import;
 
diff -r a358da1a0218 -r df77edc4f5d0 src/HOL/Import/proof_kernel.ML
--- 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))
diff -r a358da1a0218 -r df77edc4f5d0 src/HOL/Import/replay.ML
--- a/src/HOL/Import/replay.ML	Fri Sep 16 20:30:44 2005 +0200
+++ b/src/HOL/Import/replay.ML	Fri Sep 16 21:02:15 2005 +0200
@@ -284,7 +284,7 @@
 		fun get_facts facts =
 		    case TextIO.inputLine is of
 			"" => (case facts of
-				   i::facts => (valOf (Int.fromString i),rev facts)
+				   i::facts => (valOf (Int.fromString i),map P.protect_factname (rev facts))
 				 | _ => raise ERR "replay_thm" "Bad facts.lst file")
 		      | fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
 	    in
@@ -340,4 +340,4 @@
 	replay_fact (thmname,thy)
     end
 
-end
+end
\ No newline at end of file
diff -r a358da1a0218 -r df77edc4f5d0 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Fri Sep 16 20:30:44 2005 +0200
+++ b/src/HOL/Import/shuffler.ML	Fri Sep 16 21:02:15 2005 +0200
@@ -343,9 +343,9 @@
 		       SOME res
 		  end
 	      else NONE)
-	     handle e => (writeln "eta_contract:";print_exn e))
-	  | _ => (error ("Bad eta_contract argument" ^ (string_of_cterm (cterm_of sg t))); NONE)
-    end
+	     handle e => print_exn e)
+	  | _ => NONE
+       end
 
 fun beta_fun sg assume t =
     SOME (beta_conversion true (cterm_of sg t))
@@ -486,6 +486,7 @@
 be handy in its own right, for example for indexing terms. *)
 
 fun norm_term thy t =
+    PolyML.exception_trace (fn () =>
     let
 	val sg = sign_of thy
 
@@ -494,8 +495,8 @@
 			  addsimps (map (Thm.transfer sg) norms)
 	fun chain f th =
 	    let
-		val rhs = snd (dest_equals (cprop_of th))
-	    in
+                val rhs = snd (dest_equals (cprop_of th))
+      	    in
 		transitive th (f rhs)
 	    end
 
@@ -508,7 +509,7 @@
 	val _ = message ("norm_term: " ^ (string_of_thm th))
     in
 	th
-    end
+    end)
     handle e => (writeln "norm_term internal error"; print_sign_exn (sign_of thy) e)