fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
authorobua
Fri Sep 16 21:02:15 2005 +0200 (2005-09-16)
changeset 17440df77edc4f5d0
parent 17439 a358da1a0218
child 17441 5b5feca0344a
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
src/HOL/Import/proof_kernel.ML
src/HOL/Import/replay.ML
src/HOL/Import/shuffler.ML
     1.1 --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Fri Sep 16 20:30:44 2005 +0200
     1.2 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Fri Sep 16 21:02:15 2005 +0200
     1.3 @@ -28,9 +28,9 @@
     1.4    DEF_IND_SUC
     1.5    DEF_IND_0
     1.6    DEF_NUM_REP
     1.7 -  TYDEF_sum
     1.8 + (* TYDEF_sum
     1.9    DEF_INL
    1.10 -  DEF_INR;
    1.11 +  DEF_INR*);
    1.12  
    1.13  type_maps
    1.14    ind > Nat.ind
    1.15 @@ -38,8 +38,8 @@
    1.16    fun > fun
    1.17    N_1 >  Product_Type.unit
    1.18    prod > "*"
    1.19 -  num > nat
    1.20 -  sum > "+";
    1.21 +  num > nat;
    1.22 + (* sum > "+";*)
    1.23  
    1.24  const_maps
    1.25    T > True
    1.26 @@ -73,9 +73,17 @@
    1.27    "*" > "op *" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    1.28    "-" > "op -" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    1.29    BIT0 > HOLLightCompat.NUMERAL_BIT0
    1.30 -  BIT1 > HOL4Compat.NUMERAL_BIT1
    1.31 -  INL > Sum_Type.Inl
    1.32 -  INR > Sum_Type.Inr;
    1.33 +  BIT1 > HOL4Compat.NUMERAL_BIT1;
    1.34 + (* INL > Sum_Type.Inl
    1.35 +  INR > Sum_Type.Inr
    1.36 +  HAS_SIZE > HOLLightCompat.HAS_SIZE*)
    1.37 +
    1.38 +(*import_until "TYDEF_sum"
    1.39 +
    1.40 +consts
    1.41 +print_theorems
    1.42 +
    1.43 +import_until *)
    1.44  
    1.45  end_import;
    1.46  
     2.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Sep 16 20:30:44 2005 +0200
     2.2 +++ b/src/HOL/Import/proof_kernel.ML	Fri Sep 16 21:02:15 2005 +0200
     2.3 @@ -110,7 +110,7 @@
     2.4      val new_axiom : string -> term -> theory -> theory * thm
     2.5  
     2.6      val prin : term -> unit 
     2.7 -
     2.8 +    val protect_factname : string -> string
     2.9  end
    2.10  
    2.11  structure ProofKernel :> ProofKernel =
    2.12 @@ -427,7 +427,6 @@
    2.13  end
    2.14  
    2.15  fun mk_comb(f,a) = f $ a
    2.16 -fun mk_abs(x,a) = Term.lambda x a
    2.17  
    2.18  (* Needed for HOL Light *)
    2.19  fun protect_tyvarname s =
    2.20 @@ -443,6 +442,7 @@
    2.21      in
    2.22  	s |> no_quest |> beg_prime
    2.23      end
    2.24 +
    2.25  fun protect_varname s =
    2.26      let
    2.27  	fun no_beg_underscore s =
    2.28 @@ -453,6 +453,36 @@
    2.29  	s |> no_beg_underscore
    2.30      end
    2.31  
    2.32 +local
    2.33 +  val sg = theory "Main"
    2.34 +in
    2.35 +  fun is_valid_bound_varname s = (read_cterm sg ("SOME "^s^" . True", TypeInfer.logicT); true) handle _ => false
    2.36 +end
    2.37 +
    2.38 +fun protect_boundvarname s = if is_valid_bound_varname s then s else "u"
    2.39 +
    2.40 +fun mk_lambda (v as Free (x, T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t))
    2.41 +  | mk_lambda (v as Var ((x, _), T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t))
    2.42 +  | mk_lambda v t = raise TERM ("lambda", [v, t]);
    2.43 + 
    2.44 +fun replacestr x y s = 
    2.45 +let
    2.46 +  val xl = explode x
    2.47 +  val yl = explode y
    2.48 +  fun isprefix [] ys = true
    2.49 +    | isprefix (x::xs) (y::ys) = if x = y then isprefix xs ys else false
    2.50 +    | isprefix _ _ = false  
    2.51 +  fun isp s = isprefix xl s
    2.52 +  fun chg s = yl@(List.drop (s, List.length xl))
    2.53 +  fun r [] = []
    2.54 +    | r (S as (s::ss)) = if isp S then r (chg S) else s::(r ss) 
    2.55 +in
    2.56 +  implode(r (explode s))
    2.57 +end    
    2.58 +
    2.59 +fun protect_factname s = replacestr "." "_dot_" s
    2.60 +fun unprotect_factname s = replacestr "_dot_" "." s 
    2.61 +
    2.62  val ty_num_prefix = "N_"
    2.63  
    2.64  fun startsWithDigit s = Char.isDigit (hd (String.explode s))
    2.65 @@ -460,13 +490,13 @@
    2.66  fun protect_tyname tyn = 
    2.67    let
    2.68      val tyn' = 
    2.69 -      if String.isPrefix ty_num_prefix tyn then raise (ERR "conv_ty_name" ("type name '"^tyn^"' is reserved")) else 
    2.70 +      if String.isPrefix ty_num_prefix tyn then raise (ERR "protect_ty_name" ("type name '"^tyn^"' is reserved")) else 
    2.71        (if startsWithDigit tyn then ty_num_prefix^tyn else tyn)
    2.72    in
    2.73      tyn'
    2.74    end
    2.75  
    2.76 -
    2.77 +fun protect_constname tcn = implode (map (fn c => if c = "." then "_dot_" else c) (explode tcn))
    2.78  
    2.79  structure TypeNet =
    2.80  struct
    2.81 @@ -543,7 +573,7 @@
    2.82  	  | gtfx (Elem("tmc",atts,[])) =
    2.83  	    let
    2.84  		val segment = get_segment thyname atts
    2.85 -		val name = get_name atts
    2.86 +		val name = protect_constname(get_name atts)
    2.87  	    in
    2.88  		mk_thy_const thy segment name (TypeNet.get_type_from_index thy thyname types (Lib.assoc "t" atts))
    2.89  		handle PK _ => prim_mk_const thy segment name
    2.90 @@ -555,12 +585,12 @@
    2.91  	    in
    2.92  		mk_comb(f,a)
    2.93  	    end
    2.94 -	  | gtfx (Elem("tml",[("x",tmx),("a",tma)],[])) =
    2.95 +	  | gtfx (Elem("tml",[("x",tmx),("a",tma)],[])) = 
    2.96  	    let
    2.97  		val x = get_term_from_index thy thyname types terms tmx
    2.98  		val a = get_term_from_index thy thyname types terms tma
    2.99  	    in
   2.100 -		mk_abs(x,a)
   2.101 +		mk_lambda x a
   2.102  	    end
   2.103  	  | gtfx (Elem("tmi",[("i",iS)],[])) =
   2.104  	    get_term_from_index thy thyname types terms iS
   2.105 @@ -612,7 +642,7 @@
   2.106  		     | NONE => error "Cannot find proof files"
   2.107  	val _ = OS.FileSys.mkDir path handle OS.SysErr _ => ()
   2.108      in
   2.109 -	OS.Path.joinDirFile {dir = path, file = OS.Path.joinBaseExt {base = thmname, ext = SOME "prf"}}
   2.110 +	OS.Path.joinDirFile {dir = path, file = OS.Path.joinBaseExt {base = (unprotect_factname thmname), ext = SOME "prf"}}
   2.111      end
   2.112  	
   2.113  fun xml_to_proof thyname types terms prf thy =
   2.114 @@ -666,14 +696,14 @@
   2.115  	  | x2p (Elem("pfact",atts,[])) =
   2.116  	    let
   2.117  		val thyname = get_segment thyname atts
   2.118 -		val thmname = get_name atts
   2.119 +		val thmname = protect_factname (get_name atts)
   2.120  		val p = mk_proof PDisk
   2.121  		val _  = set_disk_info_of p thyname thmname
   2.122  	    in
   2.123  		p
   2.124  	    end
   2.125  	  | x2p (Elem("pdef",[("s",seg),("n",name),("i",is)],[])) =
   2.126 -	    mk_proof (PDef(seg,name,index_to_term is))
   2.127 +	    mk_proof (PDef(seg,protect_constname name,index_to_term is))
   2.128  	  | x2p (Elem("ptmspec",[("s",seg)],p::names)) =
   2.129  	    let
   2.130  		val names = map (fn Elem("name",[("n",name)],[]) => name
   2.131 @@ -686,7 +716,7 @@
   2.132  		val P = xml_to_term xP
   2.133  		val t = xml_to_term xt
   2.134  	    in
   2.135 -		mk_proof (PTyIntro(seg,protect_tyname name,abs_name,rep_name,P,t,x2p p))
   2.136 +		mk_proof (PTyIntro(seg,protect_tyname name,protect_constname abs_name,protect_constname rep_name,P,t,x2p p))
   2.137  	    end
   2.138  	  | x2p (Elem("ptydef",[("s",seg),("n",name)],[p])) =
   2.139  	    mk_proof (PTyDef(seg,protect_tyname name,x2p p))
     3.1 --- a/src/HOL/Import/replay.ML	Fri Sep 16 20:30:44 2005 +0200
     3.2 +++ b/src/HOL/Import/replay.ML	Fri Sep 16 21:02:15 2005 +0200
     3.3 @@ -284,7 +284,7 @@
     3.4  		fun get_facts facts =
     3.5  		    case TextIO.inputLine is of
     3.6  			"" => (case facts of
     3.7 -				   i::facts => (valOf (Int.fromString i),rev facts)
     3.8 +				   i::facts => (valOf (Int.fromString i),map P.protect_factname (rev facts))
     3.9  				 | _ => raise ERR "replay_thm" "Bad facts.lst file")
    3.10  		      | fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
    3.11  	    in
    3.12 @@ -340,4 +340,4 @@
    3.13  	replay_fact (thmname,thy)
    3.14      end
    3.15  
    3.16 -end
    3.17 +end
    3.18 \ No newline at end of file
     4.1 --- a/src/HOL/Import/shuffler.ML	Fri Sep 16 20:30:44 2005 +0200
     4.2 +++ b/src/HOL/Import/shuffler.ML	Fri Sep 16 21:02:15 2005 +0200
     4.3 @@ -343,9 +343,9 @@
     4.4  		       SOME res
     4.5  		  end
     4.6  	      else NONE)
     4.7 -	     handle e => (writeln "eta_contract:";print_exn e))
     4.8 -	  | _ => (error ("Bad eta_contract argument" ^ (string_of_cterm (cterm_of sg t))); NONE)
     4.9 -    end
    4.10 +	     handle e => print_exn e)
    4.11 +	  | _ => NONE
    4.12 +       end
    4.13  
    4.14  fun beta_fun sg assume t =
    4.15      SOME (beta_conversion true (cterm_of sg t))
    4.16 @@ -486,6 +486,7 @@
    4.17  be handy in its own right, for example for indexing terms. *)
    4.18  
    4.19  fun norm_term thy t =
    4.20 +    PolyML.exception_trace (fn () =>
    4.21      let
    4.22  	val sg = sign_of thy
    4.23  
    4.24 @@ -494,8 +495,8 @@
    4.25  			  addsimps (map (Thm.transfer sg) norms)
    4.26  	fun chain f th =
    4.27  	    let
    4.28 -		val rhs = snd (dest_equals (cprop_of th))
    4.29 -	    in
    4.30 +                val rhs = snd (dest_equals (cprop_of th))
    4.31 +      	    in
    4.32  		transitive th (f rhs)
    4.33  	    end
    4.34  
    4.35 @@ -508,7 +509,7 @@
    4.36  	val _ = message ("norm_term: " ^ (string_of_thm th))
    4.37      in
    4.38  	th
    4.39 -    end
    4.40 +    end)
    4.41      handle e => (writeln "norm_term internal error"; print_sign_exn (sign_of thy) e)
    4.42  
    4.43