Added a number of explicit type casts and delayed evaluations (all seemingly
authorskalberg
Sun Apr 04 15:34:14 2004 +0200 (2004-04-04)
changeset 14518c3019a66180f
parent 14517 7ae3b247c6e9
child 14519 4ca3608fdf4f
Added a number of explicit type casts and delayed evaluations (all seemingly
needless) so that SML/NJ 110.9.1 would accept the importer...
src/HOL/Import/hol4rews.ML
src/HOL/Import/import_syntax.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
     1.1 --- a/src/HOL/Import/hol4rews.ML	Fri Apr 02 17:40:32 2004 +0200
     1.2 +++ b/src/HOL/Import/hol4rews.ML	Sun Apr 04 15:34:14 2004 +0200
     1.3 @@ -81,7 +81,7 @@
     1.4  val empty = Symtab.empty
     1.5  val copy = I
     1.6  val prep_ext = I
     1.7 -val merge = Symtab.merge (K true)
     1.8 +val merge : T * T -> T = Symtab.merge (K true)
     1.9  fun print sg tab =
    1.10      Pretty.writeln (Pretty.big_list "HOL4 moves:"
    1.11  	(Symtab.foldl (fn (xl,(bef,aft)) => (Pretty.str (bef ^ " --> " ^ aft)::xl)) ([],tab)))
    1.12 @@ -96,7 +96,7 @@
    1.13  val empty = Symtab.empty
    1.14  val copy = I
    1.15  val prep_ext = I
    1.16 -val merge = Symtab.merge (K true)
    1.17 +val merge : T * T -> T = Symtab.merge (K true)
    1.18  fun print sg tab =
    1.19      Pretty.writeln (Pretty.big_list "HOL4 imports:"
    1.20  	(Symtab.foldl (fn (xl,(thyname,segname)) => (Pretty.str (thyname ^ " imported from segment " ^ segname)::xl)) ([],tab)))
    1.21 @@ -126,7 +126,7 @@
    1.22  val empty = Symtab.empty
    1.23  val copy = I
    1.24  val prep_ext = I
    1.25 -val merge = Symtab.merge (K true)
    1.26 +val merge : T * T -> T = Symtab.merge (K true)
    1.27  fun print sg tab =
    1.28      Pretty.writeln (Pretty.big_list "HOL4 constant moves:"
    1.29  	(Symtab.foldl (fn (xl,(bef,aft)) => (Pretty.str (bef ^ " --> " ^ aft)::xl)) ([],tab)))
    1.30 @@ -141,7 +141,7 @@
    1.31  val empty = StringPair.empty
    1.32  val copy = I
    1.33  val prep_ext = I
    1.34 -val merge = StringPair.merge (K true)
    1.35 +val merge : T * T -> T = StringPair.merge (K true)
    1.36  fun print sg tab =
    1.37      Pretty.writeln (Pretty.big_list "HOL4 mappings:"
    1.38  	(StringPair.foldl (fn (xl,((bthy,bthm),isathm)) => (Pretty.str (bthy ^ "." ^ bthm ^ (case isathm of Some th => " --> " ^ th | None => "IGNORED"))::xl)) ([],tab)))
    1.39 @@ -156,7 +156,7 @@
    1.40  val empty = StringPair.empty
    1.41  val copy = I
    1.42  val prep_ext = I
    1.43 -val merge = StringPair.merge (K true)
    1.44 +val merge : T * T -> T = StringPair.merge (K true)
    1.45  fun print sg tab =
    1.46      Pretty.writeln (Pretty.big_list "HOL4 mappings:"
    1.47  	(StringPair.foldl (fn (xl,((bthy,bthm),(_,thm))) => (Pretty.str (bthy ^ "." ^ bthm ^ ":")::(Display.pretty_thm thm)::xl)) ([],tab)))
    1.48 @@ -171,7 +171,7 @@
    1.49  val empty = StringPair.empty
    1.50  val copy = I
    1.51  val prep_ext = I
    1.52 -val merge = StringPair.merge (K true)
    1.53 +val merge : T * T -> T = StringPair.merge (K true)
    1.54  fun print sg tab =
    1.55      Pretty.writeln (Pretty.big_list "HOL4 constant mappings:"
    1.56  	(StringPair.foldl (fn (xl,((bthy,bconst),(internal,isaconst,_))) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else ""))::xl)) ([],tab)))
    1.57 @@ -186,7 +186,7 @@
    1.58  val empty = StringPair.empty
    1.59  val copy = I
    1.60  val prep_ext = I
    1.61 -val merge = StringPair.merge (K true)
    1.62 +val merge : T * T -> T = StringPair.merge (K true)
    1.63  fun print sg tab =
    1.64      Pretty.writeln (Pretty.big_list "HOL4 constant renamings:"
    1.65  	(StringPair.foldl (fn (xl,((bthy,bconst),newname)) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ newname)::xl)) ([],tab)))
    1.66 @@ -201,7 +201,7 @@
    1.67  val empty = StringPair.empty
    1.68  val copy = I
    1.69  val prep_ext = I
    1.70 -val merge = StringPair.merge (K true)
    1.71 +val merge : T * T -> T = StringPair.merge (K true)
    1.72  fun print sg tab =
    1.73      Pretty.writeln (Pretty.big_list "HOL4 constant definitions:"
    1.74  	(StringPair.foldl (fn (xl,((bthy,bconst),newname)) => (Pretty.str (bthy ^ "." ^ bconst ^ ": " ^ newname)::xl)) ([],tab)))
    1.75 @@ -216,7 +216,7 @@
    1.76  val empty = StringPair.empty
    1.77  val copy = I
    1.78  val prep_ext = I
    1.79 -val merge = StringPair.merge (K true)
    1.80 +val merge : T * T -> T = StringPair.merge (K true)
    1.81  fun print sg tab =
    1.82      Pretty.writeln (Pretty.big_list "HOL4 type mappings:"
    1.83  	(StringPair.foldl (fn (xl,((bthy,bconst),(internal,isaconst))) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else ""))::xl)) ([],tab)))
    1.84 @@ -231,7 +231,7 @@
    1.85  val empty = StringPair.empty
    1.86  val copy = I
    1.87  val prep_ext = I
    1.88 -val merge = StringPair.merge (K true)
    1.89 +val merge : T * T -> T = StringPair.merge (K true)
    1.90  fun print sg tab =
    1.91      Pretty.writeln (Pretty.big_list "HOL4 pending theorems:"
    1.92  	(StringPair.foldl (fn (xl,((bthy,bthm),(_,th))) => (Pretty.chunks [Pretty.str (bthy ^ "." ^ bthm ^ ":"),Display.pretty_thm th]::xl)) ([],tab)))
    1.93 @@ -736,6 +736,7 @@
    1.94        | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "all", _],_]] = x
    1.95        | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==>", _],_,_]] = x
    1.96        | handle_meta [x] = Appl[Constant "Trueprop",x]
    1.97 +      | handle_meta _ = error "hol4rews error: Trueprop not applied to single argument"
    1.98  in
    1.99  val smarter_trueprop_parsing = [("Trueprop",handle_meta)]
   1.100  end
     2.1 --- a/src/HOL/Import/import_syntax.ML	Fri Apr 02 17:40:32 2004 +0200
     2.2 +++ b/src/HOL/Import/import_syntax.ML	Sun Apr 04 15:34:14 2004 +0200
     2.3 @@ -37,24 +37,25 @@
     2.4  				      |> Theory.add_path thyname
     2.5  				      |> add_dump (";setup_theory " ^ thyname))
     2.6  
     2.7 -val end_import = Scan.succeed
     2.8 -		     (fn thy =>
     2.9 -			 let
    2.10 -			     val thyname = get_generating_thy thy
    2.11 -			     val segname = get_import_segment thy
    2.12 -			     val (int_thms,facts) = Replay.setup_int_thms thyname thy
    2.13 -			     val thmnames = filter (not o should_ignore thyname thy) facts
    2.14 -			 in
    2.15 -			     thy |> clear_import_thy
    2.16 -				 |> set_segment thyname segname
    2.17 -				 |> set_used_names facts
    2.18 -				 |> Replay.import_thms thyname int_thms thmnames
    2.19 -				 |> clear_used_names
    2.20 -				 |> export_hol4_pending
    2.21 -				 |> Theory.parent_path
    2.22 -				 |> dump_import_thy thyname
    2.23 -				 |> add_dump ";end_setup"
    2.24 -			 end)
    2.25 +fun end_import toks =
    2.26 +    Scan.succeed
    2.27 +	(fn thy =>
    2.28 +	    let
    2.29 +		val thyname = get_generating_thy thy
    2.30 +		val segname = get_import_segment thy
    2.31 +		val (int_thms,facts) = Replay.setup_int_thms thyname thy
    2.32 +		val thmnames = filter (not o should_ignore thyname thy) facts
    2.33 +	    in
    2.34 +		thy |> clear_import_thy
    2.35 +		    |> set_segment thyname segname
    2.36 +		    |> set_used_names facts
    2.37 +		    |> Replay.import_thms thyname int_thms thmnames
    2.38 +		    |> clear_used_names
    2.39 +		    |> export_hol4_pending
    2.40 +		    |> Theory.parent_path
    2.41 +		    |> dump_import_thy thyname
    2.42 +		    |> add_dump ";end_setup"
    2.43 +	    end) toks
    2.44  
    2.45  val ignore_thms = Scan.repeat1 P.name
    2.46  			       >> (fn ignored =>
    2.47 @@ -158,18 +159,20 @@
    2.48  			     | Generating _ => error "Currently generating a theory!"
    2.49  			     | Replaying _ => thy |> clear_import_thy |> import_thy thyname)
    2.50  
    2.51 -val end_setup = Scan.succeed (fn thy =>
    2.52 -				 let
    2.53 -				     val thyname = get_import_thy thy
    2.54 -				     val segname = get_import_segment thy
    2.55 -				 in
    2.56 -				     thy |> set_segment thyname segname
    2.57 -					 |> clear_import_thy
    2.58 -					 |> Theory.parent_path
    2.59 -				 end)
    2.60 +fun end_setup toks =
    2.61 +    Scan.succeed
    2.62 +	(fn thy =>
    2.63 +	    let
    2.64 +		val thyname = get_import_thy thy
    2.65 +		val segname = get_import_segment thy
    2.66 +	    in
    2.67 +		thy |> set_segment thyname segname
    2.68 +		    |> clear_import_thy
    2.69 +		    |> Theory.parent_path
    2.70 +	    end) toks
    2.71  
    2.72  val set_dump  = P.string -- P.string   >> setup_dump
    2.73 -val fl_dump   = Scan.succeed flush_dump
    2.74 +fun fl_dump toks  = Scan.succeed flush_dump toks
    2.75  val append_dump = (P.verbatim || P.string) >> add_dump
    2.76  
    2.77  val parsers = 
     3.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Apr 02 17:40:32 2004 +0200
     3.2 +++ b/src/HOL/Import/proof_kernel.ML	Sun Apr 04 15:34:14 2004 +0200
     3.3 @@ -276,7 +276,7 @@
     3.4  
     3.5  fun get_segment thyname l = (Lib.assoc "s" l
     3.6  			     handle PK _ => thyname)
     3.7 -val get_name    = Lib.assoc "n"
     3.8 +val get_name : (string * string) list -> string = Lib.assoc "n"
     3.9  
    3.10  local
    3.11      open LazyScan
    3.12 @@ -340,7 +340,11 @@
    3.13  val scan_start_of_tag = $$ #"<" |-- scan_id --
    3.14  			   repeat ($$ #" " |-- scan_attribute)
    3.15  
    3.16 -val scan_end_of_tag = $$ #"/" |-- $$ #">" |-- succeed []
    3.17 +(* The evaluation delay introduced through the 'toks' argument is needed
    3.18 +for the sake of the SML/NJ (110.9.1) compiler.  Either that or an explicit
    3.19 +type :-( *)
    3.20 +fun scan_end_of_tag toks = ($$ #"/" |-- $$ #">" |-- succeed []) toks
    3.21 +
    3.22  val scan_end_tag = $$ #"<" |-- $$ #"/" |-- scan_id --| $$ #">"
    3.23  
    3.24  fun scan_children id = $$ #">" |-- repeat scan_tag -- scan_end_tag >>
    3.25 @@ -1633,7 +1637,7 @@
    3.26  	val cv = cterm_of sg v'
    3.27  	val th2 = norm_hyps th2
    3.28  	val cvty = ctyp_of_term cv
    3.29 -	val _$c = concl_of th2
    3.30 +	val c = HOLogic.dest_Trueprop (concl_of th2)
    3.31  	val cc = cterm_of sg c
    3.32  	val a = case concl_of th1 of
    3.33  		    _ $ (Const("Ex",_) $ a) => a
     4.1 --- a/src/HOL/Import/shuffler.ML	Fri Apr 02 17:40:32 2004 +0200
     4.2 +++ b/src/HOL/Import/shuffler.ML	Sun Apr 04 15:34:14 2004 +0200
     4.3 @@ -263,7 +263,8 @@
     4.4  		  (([],tfree_names),tvars)
     4.5  	val t' = subst_TVars type_inst t
     4.6      in
     4.7 -	(t',map (fn (w,TFree(v,S)) => (v,TVar(w,S))) type_inst)
     4.8 +	(t',map (fn (w,TFree(v,S)) => (v,TVar(w,S))
     4.9 +		  | _ => error "Internal error in Shuffler.freeze_thaw") type_inst)
    4.10      end
    4.11  
    4.12  fun inst_tfrees sg [] thm = thm