src/HOL/Import/hol4rews.ML
author skalberg
Sat, 17 Apr 2004 23:53:35 +0200
changeset 14620 1be590fd2422
parent 14518 c3019a66180f
child 14818 ad83019a66a4
permissions -rw-r--r--
Minor cleanup of headers and some speedup of the HOL4 import.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14620
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents: 14518
diff changeset
     1
(*  Title:      HOL/Import/hol4rews.ML
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents: 14518
diff changeset
     2
    ID:         $Id$
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents: 14518
diff changeset
     3
    Author:     Sebastian Skalberg (TU Muenchen)
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents: 14518
diff changeset
     4
*)
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents: 14518
diff changeset
     5
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     6
structure StringPair = TableFun(type key = string * string val ord = prod_ord string_ord string_ord);
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     7
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     8
type holthm = (term * term) list * thm
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     9
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    10
datatype ImportStatus =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    11
	 NoImport
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    12
       | Generating of string
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    13
       | Replaying of string
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    14
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    15
structure HOL4DefThyArgs: THEORY_DATA_ARGS =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    16
struct
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    17
val name = "HOL4/import_status"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    18
type T = ImportStatus
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    19
val empty = NoImport
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    20
val copy = I
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    21
val prep_ext = I
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    22
fun merge (NoImport,NoImport) = NoImport
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    23
  | merge _ = (warning "Import status set during merge"; NoImport)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    24
fun print sg import_status =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    25
    Pretty.writeln (Pretty.str (case import_status of NoImport => "No current import" | Generating thyname => ("Generating " ^ thyname) | Replaying thyname => ("Replaying " ^ thyname)))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    26
end;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    27
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    28
structure HOL4DefThy = TheoryDataFun(HOL4DefThyArgs);
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    29
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    30
structure ImportSegmentArgs: THEORY_DATA_ARGS =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    31
struct
14620
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents: 14518
diff changeset
    32
val name = "HOL4/import_segment"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    33
type T = string
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    34
val empty = ""
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    35
val copy = I
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    36
val prep_ext = I
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    37
fun merge ("",arg) = arg
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    38
  | merge (arg,"") = arg
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    39
  | merge (s1,s2) =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    40
    if s1 = s2
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    41
    then s1
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    42
    else error "Trying to merge two different import segments"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    43
fun print sg import_segment =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    44
    Pretty.writeln (Pretty.str ("Import segment: " ^ import_segment))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    45
end;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    46
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    47
structure ImportSegment = TheoryDataFun(ImportSegmentArgs);
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    48
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    49
val get_import_segment = ImportSegment.get
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    50
val set_import_segment = ImportSegment.put
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    51
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    52
structure HOL4UNamesArgs: THEORY_DATA_ARGS =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    53
struct
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    54
val name = "HOL4/used_names"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    55
type T = string list
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    56
val empty = []
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    57
val copy = I
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    58
val prep_ext = I
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    59
fun merge ([],[]) = []
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    60
  | merge _ = error "Used names not empty during merge"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    61
fun print sg used_names =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    62
    Pretty.writeln (Pretty.str "Printing of HOL4/used_names Not implemented")
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    63
end;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    64
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    65
structure HOL4UNames = TheoryDataFun(HOL4UNamesArgs);
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    66
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    67
structure HOL4DumpArgs: THEORY_DATA_ARGS =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    68
struct
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    69
val name = "HOL4/dump_data"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    70
type T = string * string * string list
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    71
val empty = ("","",[])
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    72
val copy = I
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    73
val prep_ext = I
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    74
fun merge (("","",[]),("","",[])) = ("","",[])
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    75
  | merge _ = error "Dump data not empty during merge"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    76
fun print sg dump_data =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    77
    Pretty.writeln (Pretty.str "Printing of HOL4/dump_data Not implemented")
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    78
end;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    79
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    80
structure HOL4Dump = TheoryDataFun(HOL4DumpArgs);
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    81
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    82
structure HOL4MovesArgs: THEORY_DATA_ARGS =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    83
struct
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    84
val name = "HOL4/moves"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    85
type T = string Symtab.table
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    86
val empty = Symtab.empty
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    87
val copy = I
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    88
val prep_ext = I
14518
c3019a66180f Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents: 14516
diff changeset
    89
val merge : T * T -> T = Symtab.merge (K true)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    90
fun print sg tab =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    91
    Pretty.writeln (Pretty.big_list "HOL4 moves:"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    92
	(Symtab.foldl (fn (xl,(bef,aft)) => (Pretty.str (bef ^ " --> " ^ aft)::xl)) ([],tab)))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    93
end;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    94
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    95
structure HOL4Moves = TheoryDataFun(HOL4MovesArgs);
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    96
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    97
structure HOL4ImportsArgs: THEORY_DATA_ARGS =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    98
struct
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    99
val name = "HOL4/imports"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   100
type T = string Symtab.table
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   101
val empty = Symtab.empty
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   102
val copy = I
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   103
val prep_ext = I
14518
c3019a66180f Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents: 14516
diff changeset
   104
val merge : T * T -> T = Symtab.merge (K true)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   105
fun print sg tab =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   106
    Pretty.writeln (Pretty.big_list "HOL4 imports:"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   107
	(Symtab.foldl (fn (xl,(thyname,segname)) => (Pretty.str (thyname ^ " imported from segment " ^ segname)::xl)) ([],tab)))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   108
end;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   109
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   110
structure HOL4Imports = TheoryDataFun(HOL4ImportsArgs);
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   111
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   112
fun get_segment2 thyname thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   113
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   114
	val imps = HOL4Imports.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   115
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   116
	Symtab.lookup(imps,thyname)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   117
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   118
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   119
fun set_segment thyname segname thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   120
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   121
	val imps = HOL4Imports.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   122
	val imps' = Symtab.update_new((thyname,segname),imps)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   123
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   124
	HOL4Imports.put imps' thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   125
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   126
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   127
structure HOL4CMovesArgs: THEORY_DATA_ARGS =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   128
struct
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   129
val name = "HOL4/constant_moves"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   130
type T = string Symtab.table
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   131
val empty = Symtab.empty
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   132
val copy = I
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   133
val prep_ext = I
14518
c3019a66180f Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents: 14516
diff changeset
   134
val merge : T * T -> T = Symtab.merge (K true)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   135
fun print sg tab =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   136
    Pretty.writeln (Pretty.big_list "HOL4 constant moves:"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   137
	(Symtab.foldl (fn (xl,(bef,aft)) => (Pretty.str (bef ^ " --> " ^ aft)::xl)) ([],tab)))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   138
end;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   139
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   140
structure HOL4CMoves = TheoryDataFun(HOL4CMovesArgs);
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   141
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   142
structure HOL4MapsArgs: THEORY_DATA_ARGS =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   143
struct
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   144
val name = "HOL4/mappings"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   145
type T = (string option) StringPair.table
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   146
val empty = StringPair.empty
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   147
val copy = I
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   148
val prep_ext = I
14518
c3019a66180f Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents: 14516
diff changeset
   149
val merge : T * T -> T = StringPair.merge (K true)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   150
fun print sg tab =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   151
    Pretty.writeln (Pretty.big_list "HOL4 mappings:"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   152
	(StringPair.foldl (fn (xl,((bthy,bthm),isathm)) => (Pretty.str (bthy ^ "." ^ bthm ^ (case isathm of Some th => " --> " ^ th | None => "IGNORED"))::xl)) ([],tab)))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   153
end;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   154
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   155
structure HOL4Maps = TheoryDataFun(HOL4MapsArgs);
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   156
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   157
structure HOL4ThmsArgs: THEORY_DATA_ARGS =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   158
struct
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   159
val name = "HOL4/theorems"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   160
type T = holthm StringPair.table
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   161
val empty = StringPair.empty
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   162
val copy = I
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   163
val prep_ext = I
14518
c3019a66180f Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents: 14516
diff changeset
   164
val merge : T * T -> T = StringPair.merge (K true)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   165
fun print sg tab =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   166
    Pretty.writeln (Pretty.big_list "HOL4 mappings:"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   167
	(StringPair.foldl (fn (xl,((bthy,bthm),(_,thm))) => (Pretty.str (bthy ^ "." ^ bthm ^ ":")::(Display.pretty_thm thm)::xl)) ([],tab)))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   168
end;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   169
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   170
structure HOL4Thms = TheoryDataFun(HOL4ThmsArgs);
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   171
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   172
structure HOL4ConstMapsArgs: THEORY_DATA_ARGS =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   173
struct
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   174
val name = "HOL4/constmappings"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   175
type T = (bool * string * typ option) StringPair.table
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   176
val empty = StringPair.empty
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   177
val copy = I
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   178
val prep_ext = I
14518
c3019a66180f Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents: 14516
diff changeset
   179
val merge : T * T -> T = StringPair.merge (K true)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   180
fun print sg tab =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   181
    Pretty.writeln (Pretty.big_list "HOL4 constant mappings:"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   182
	(StringPair.foldl (fn (xl,((bthy,bconst),(internal,isaconst,_))) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else ""))::xl)) ([],tab)))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   183
end;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   184
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   185
structure HOL4ConstMaps = TheoryDataFun(HOL4ConstMapsArgs);
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   186
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   187
structure HOL4RenameArgs: THEORY_DATA_ARGS =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   188
struct
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   189
val name = "HOL4/renamings"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   190
type T = string StringPair.table
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   191
val empty = StringPair.empty
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   192
val copy = I
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   193
val prep_ext = I
14518
c3019a66180f Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents: 14516
diff changeset
   194
val merge : T * T -> T = StringPair.merge (K true)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   195
fun print sg tab =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   196
    Pretty.writeln (Pretty.big_list "HOL4 constant renamings:"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   197
	(StringPair.foldl (fn (xl,((bthy,bconst),newname)) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ newname)::xl)) ([],tab)))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   198
end;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   199
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   200
structure HOL4Rename = TheoryDataFun(HOL4RenameArgs);
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   201
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   202
structure HOL4DefMapsArgs: THEORY_DATA_ARGS =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   203
struct
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   204
val name = "HOL4/def_maps"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   205
type T = string StringPair.table
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   206
val empty = StringPair.empty
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   207
val copy = I
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   208
val prep_ext = I
14518
c3019a66180f Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents: 14516
diff changeset
   209
val merge : T * T -> T = StringPair.merge (K true)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   210
fun print sg tab =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   211
    Pretty.writeln (Pretty.big_list "HOL4 constant definitions:"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   212
	(StringPair.foldl (fn (xl,((bthy,bconst),newname)) => (Pretty.str (bthy ^ "." ^ bconst ^ ": " ^ newname)::xl)) ([],tab)))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   213
end;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   214
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   215
structure HOL4DefMaps = TheoryDataFun(HOL4DefMapsArgs);
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   216
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   217
structure HOL4TypeMapsArgs: THEORY_DATA_ARGS =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   218
struct
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   219
val name = "HOL4/typemappings"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   220
type T = (bool * string) StringPair.table
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   221
val empty = StringPair.empty
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   222
val copy = I
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   223
val prep_ext = I
14518
c3019a66180f Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents: 14516
diff changeset
   224
val merge : T * T -> T = StringPair.merge (K true)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   225
fun print sg tab =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   226
    Pretty.writeln (Pretty.big_list "HOL4 type mappings:"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   227
	(StringPair.foldl (fn (xl,((bthy,bconst),(internal,isaconst))) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else ""))::xl)) ([],tab)))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   228
end;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   229
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   230
structure HOL4TypeMaps = TheoryDataFun(HOL4TypeMapsArgs);
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   231
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   232
structure HOL4PendingArgs: THEORY_DATA_ARGS =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   233
struct
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   234
val name = "HOL4/pending"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   235
type T = ((term * term) list * thm) StringPair.table
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   236
val empty = StringPair.empty
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   237
val copy = I
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   238
val prep_ext = I
14518
c3019a66180f Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents: 14516
diff changeset
   239
val merge : T * T -> T = StringPair.merge (K true)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   240
fun print sg tab =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   241
    Pretty.writeln (Pretty.big_list "HOL4 pending theorems:"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   242
	(StringPair.foldl (fn (xl,((bthy,bthm),(_,th))) => (Pretty.chunks [Pretty.str (bthy ^ "." ^ bthm ^ ":"),Display.pretty_thm th]::xl)) ([],tab)))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   243
end;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   244
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   245
structure HOL4Pending = TheoryDataFun(HOL4PendingArgs);
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   246
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   247
structure HOL4RewritesArgs: THEORY_DATA_ARGS =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   248
struct
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   249
val name = "HOL4/rewrites"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   250
type T = thm list
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   251
val empty = []
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   252
val copy = I
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   253
val prep_ext = I
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   254
val merge = Library.gen_union Thm.eq_thm
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   255
fun print sg thms =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   256
    Pretty.writeln (Pretty.big_list "HOL4 rewrite rules:"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   257
				    (map Display.pretty_thm thms))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   258
end;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   259
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   260
structure HOL4Rewrites = TheoryDataFun(HOL4RewritesArgs);
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   261
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   262
val hol4_debug = ref false
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   263
fun message s = if !hol4_debug then writeln s else ()
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   264
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   265
fun add_hol4_rewrite (thy,th) =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   266
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   267
	val _ = message "Adding HOL4 rewrite"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   268
	val th1 = th RS eq_reflection
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   269
	val current_rews = HOL4Rewrites.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   270
	val new_rews = gen_ins Thm.eq_thm (th1,current_rews)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   271
	val updated_thy  = HOL4Rewrites.put new_rews thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   272
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   273
	(updated_thy,th1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   274
    end;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   275
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   276
fun ignore_hol4 bthy bthm thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   277
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   278
	val _ = message ("Ignoring " ^ bthy ^ "." ^ bthm)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   279
	val curmaps = HOL4Maps.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   280
	val newmaps = StringPair.update_new(((bthy,bthm),None),curmaps)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   281
	val upd_thy = HOL4Maps.put newmaps thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   282
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   283
	upd_thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   284
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   285
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   286
val opt_get_output_thy = #2 o HOL4Dump.get
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   287
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   288
fun get_output_thy thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   289
    case #2 (HOL4Dump.get thy) of
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   290
	"" => error "No theory file being output"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   291
      | thyname => thyname
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   292
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   293
val get_output_dir = #1 o HOL4Dump.get
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   294
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   295
fun add_hol4_move bef aft thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   296
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   297
	val curmoves = HOL4Moves.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   298
	val newmoves = Symtab.update_new((bef,aft),curmoves)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   299
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   300
	HOL4Moves.put newmoves thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   301
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   302
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   303
fun get_hol4_move bef thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   304
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   305
	val moves = HOL4Moves.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   306
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   307
	Symtab.lookup(moves,bef)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   308
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   309
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   310
fun follow_name thmname thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   311
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   312
	val moves = HOL4Moves.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   313
	fun F thmname =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   314
	    case Symtab.lookup(moves,thmname) of
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   315
		Some name => F name
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   316
	      | None => thmname
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   317
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   318
	F thmname
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   319
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   320
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   321
fun add_hol4_cmove bef aft thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   322
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   323
	val curmoves = HOL4CMoves.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   324
	val newmoves = Symtab.update_new((bef,aft),curmoves)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   325
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   326
	HOL4CMoves.put newmoves thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   327
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   328
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   329
fun get_hol4_cmove bef thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   330
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   331
	val moves = HOL4CMoves.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   332
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   333
	Symtab.lookup(moves,bef)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   334
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   335
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   336
fun follow_cname thmname thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   337
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   338
	val moves = HOL4CMoves.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   339
	fun F thmname =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   340
	    case Symtab.lookup(moves,thmname) of
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   341
		Some name => F name
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   342
	      | None => thmname
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   343
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   344
	F thmname
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   345
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   346
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   347
fun add_hol4_mapping bthy bthm isathm thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   348
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   349
	val isathm = follow_name isathm thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   350
	val _ = message ("Adding theorem map: " ^ bthy ^ "." ^ bthm ^ " --> " ^ isathm)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   351
	val curmaps = HOL4Maps.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   352
	val newmaps = StringPair.update_new(((bthy,bthm),Some isathm),curmaps)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   353
	val upd_thy = HOL4Maps.put newmaps thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   354
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   355
	upd_thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   356
    end;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   357
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   358
fun get_hol4_type_mapping bthy tycon thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   359
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   360
	val maps = HOL4TypeMaps.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   361
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   362
	StringPair.lookup(maps,(bthy,tycon))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   363
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   364
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   365
fun get_hol4_mapping bthy bthm thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   366
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   367
	val curmaps = HOL4Maps.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   368
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   369
	StringPair.lookup(curmaps,(bthy,bthm))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   370
    end;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   371
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   372
fun add_hol4_const_mapping bthy bconst internal isaconst thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   373
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   374
	val thy = case opt_get_output_thy thy of
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   375
		      "" => thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   376
		    | output_thy => if internal
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   377
				    then add_hol4_cmove (Sign.full_name (sign_of thy) bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   378
				    else thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   379
	val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   380
	val curmaps = HOL4ConstMaps.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   381
	val newmaps = StringPair.update_new(((bthy,bconst),(internal,isaconst,None)),curmaps)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   382
	val upd_thy = HOL4ConstMaps.put newmaps thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   383
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   384
	upd_thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   385
    end;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   386
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   387
fun add_hol4_const_renaming bthy bconst newname thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   388
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   389
	val currens = HOL4Rename.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   390
	val _ = message ("Adding renaming " ^ bthy ^ "." ^ bconst ^ " -> " ^ newname)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   391
	val newrens = StringPair.update_new(((bthy,bconst),newname),currens)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   392
	val upd_thy = HOL4Rename.put newrens thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   393
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   394
	upd_thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   395
    end;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   396
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   397
fun get_hol4_const_renaming bthy bconst thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   398
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   399
	val currens = HOL4Rename.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   400
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   401
	StringPair.lookup(currens,(bthy,bconst))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   402
    end;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   403
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   404
fun get_hol4_const_mapping bthy bconst thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   405
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   406
	val bconst = case get_hol4_const_renaming bthy bconst thy of
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   407
			 Some name => name
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   408
		       | None => bconst
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   409
	val maps = HOL4ConstMaps.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   410
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   411
	StringPair.lookup(maps,(bthy,bconst))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   412
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   413
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   414
fun add_hol4_const_wt_mapping bthy bconst internal isaconst typ thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   415
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   416
	val thy = case opt_get_output_thy thy of
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   417
		      "" => thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   418
		    | output_thy => if internal
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   419
				    then add_hol4_cmove (Sign.full_name (sign_of thy) bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   420
				    else thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   421
	val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   422
	val curmaps = HOL4ConstMaps.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   423
	val newmaps = StringPair.update_new(((bthy,bconst),(internal,isaconst,Some typ)),curmaps)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   424
	val upd_thy = HOL4ConstMaps.put newmaps thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   425
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   426
	upd_thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   427
    end;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   428
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   429
fun add_hol4_type_mapping bthy bconst internal isaconst thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   430
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   431
	val curmaps = HOL4TypeMaps.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   432
	val _ = message ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   433
	val newmaps = StringPair.update_new(((bthy,bconst),(internal,isaconst)),curmaps)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   434
	val upd_thy = HOL4TypeMaps.put newmaps thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   435
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   436
	upd_thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   437
    end;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   438
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   439
fun add_hol4_pending bthy bthm hth thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   440
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   441
	val thmname = Sign.full_name (sign_of thy) bthm
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   442
	val _ = message ("Add pending " ^ bthy ^ "." ^ bthm)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   443
	val curpend = HOL4Pending.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   444
	val newpend = StringPair.update_new(((bthy,bthm),hth),curpend)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   445
	val upd_thy = HOL4Pending.put newpend thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   446
	val thy' = case opt_get_output_thy upd_thy of
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   447
		       "" => add_hol4_mapping bthy bthm thmname upd_thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   448
		     | output_thy =>
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   449
		       let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   450
			   val new_thmname = output_thy ^ "." ^ bthy ^ "." ^ bthm
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   451
		       in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   452
			   upd_thy |> add_hol4_move thmname new_thmname
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   453
				   |> add_hol4_mapping bthy bthm new_thmname
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   454
		       end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   455
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   456
	thy'
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   457
    end;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   458
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   459
fun get_hol4_theorem thyname thmname thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   460
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   461
	val isathms = HOL4Thms.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   462
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   463
	StringPair.lookup (isathms,(thyname,thmname))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   464
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   465
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   466
fun add_hol4_theorem thyname thmname hth thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   467
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   468
	val _ = message ("Adding HOL4 theorem " ^ thyname ^ "." ^ thmname)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   469
	val isathms = HOL4Thms.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   470
	val isathms' = StringPair.update_new (((thyname,thmname),hth),isathms)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   471
	val thy' = HOL4Thms.put isathms' thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   472
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   473
	thy'
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   474
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   475
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   476
fun export_hol4_pending thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   477
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   478
	val rews    = HOL4Rewrites.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   479
	val outthy  = get_output_thy thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   480
	fun process (thy,((bthy,bthm),hth as (_,thm))) =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   481
	    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   482
		val sg      = sign_of thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   483
		val thm1 = rewrite_rule (map (transfer_sg sg) rews) (transfer_sg sg thm)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   484
		val thm2 = standard thm1
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   485
		val (thy2,_) = PureThy.store_thm((bthm,thm2),[]) thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   486
		val thy5 = add_hol4_theorem bthy bthm hth thy2
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   487
	    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   488
		thy5
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   489
	    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   490
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   491
	val pending = HOL4Pending.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   492
	val thy1    = StringPair.foldl process (thy,pending)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   493
	val thy2    = HOL4Pending.put (StringPair.empty) thy1
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   494
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   495
	thy2
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   496
    end;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   497
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   498
fun setup_dump (dir,thyname) thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   499
    HOL4Dump.put (dir,thyname,[]) thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   500
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   501
fun add_dump str thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   502
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   503
	val (dir,thyname,curdump) = HOL4Dump.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   504
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   505
	HOL4Dump.put (dir,thyname,str::curdump) thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   506
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   507
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   508
fun flush_dump thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   509
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   510
	val (dir,thyname,dumpdata) = HOL4Dump.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   511
	val os = TextIO.openOut (OS.Path.joinDirFile {dir=dir,
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   512
						      file=thyname ^ ".thy"})
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   513
	val _  = app (fn s => TextIO.output(os,s ^ "\n\n")) (rev dumpdata)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   514
	val  _ = TextIO.closeOut os
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   515
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   516
	HOL4Dump.put ("","",[]) thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   517
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   518
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   519
fun set_generating_thy thyname thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   520
    case HOL4DefThy.get thy of
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   521
	NoImport => HOL4DefThy.put (Generating thyname) thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   522
      | _ => error "Import already in progess"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   523
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   524
fun set_replaying_thy thyname thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   525
    case HOL4DefThy.get thy of
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   526
	NoImport => HOL4DefThy.put (Replaying thyname) thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   527
      | _ => error "Import already in progess"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   528
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   529
fun clear_import_thy thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   530
    case HOL4DefThy.get thy of
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   531
	NoImport => error "No import in progress"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   532
      | _ => HOL4DefThy.put NoImport thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   533
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   534
fun get_generating_thy thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   535
    case HOL4DefThy.get thy of
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   536
	Generating thyname => thyname
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   537
      | _ => error "No theory being generated"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   538
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   539
fun get_replaying_thy thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   540
    case HOL4DefThy.get thy of
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   541
	Replaying thyname => thyname
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   542
      | _ => error "No theory being replayed"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   543
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   544
fun get_import_thy thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   545
    case HOL4DefThy.get thy of
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   546
	Replaying thyname => thyname
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   547
      | Generating thyname => thyname
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   548
      | _ => error "No theory being imported"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   549
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   550
fun should_ignore thyname thy thmname =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   551
    case get_hol4_mapping thyname thmname thy of
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   552
	Some None => true 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   553
      | _ => false
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   554
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   555
val trans_string =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   556
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   557
	fun quote s = "\"" ^ s ^ "\""
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   558
	fun F [] = []
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   559
	  | F (#"\\" :: cs) = patch #"\\" cs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   560
	  | F (#"\"" :: cs) = patch #"\"" cs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   561
	  | F (c     :: cs) = c :: F cs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   562
	and patch c rest = #"\\" :: c :: F rest
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   563
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   564
	quote o String.implode o F o String.explode
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   565
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   566
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   567
fun dump_import_thy thyname thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   568
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   569
	val output_dir = get_output_dir thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   570
	val output_thy = get_output_thy thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   571
	val import_segment = get_import_segment thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   572
	val sg = sign_of thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   573
	val os = TextIO.openOut (OS.Path.joinDirFile {dir=output_dir,
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   574
						      file=thyname ^ ".imp"})
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   575
	fun out s = TextIO.output(os,s)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   576
	val (ignored,mapped) =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   577
	    StringPair.foldl (fn ((ign,map),((bthy,bthm),v)) =>
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   578
				 if bthy = thyname
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   579
				 then (case v of
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   580
					   None => (bthm::ign,map)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   581
					 | Some w => (ign,(bthm,w)::map))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   582
				 else (ign,map))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   583
				 (([],[]),HOL4Maps.get thy)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   584
	val constmaps =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   585
	    StringPair.foldl (fn (map,((bthy,bthm),v)) =>
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   586
				 if bthy = thyname
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   587
				 then (bthm,v)::map
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   588
				 else map)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   589
				 ([],HOL4ConstMaps.get thy)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   590
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   591
	val constrenames =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   592
	    StringPair.foldl (fn (map,((bthy,bthm),v)) =>
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   593
				 if bthy = thyname
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   594
				 then (bthm,v)::map
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   595
				 else map)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   596
				 ([],HOL4Rename.get thy)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   597
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   598
	val typemaps =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   599
	    StringPair.foldl (fn (map,((bthy,bthm),v)) =>
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   600
				 if bthy = thyname
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   601
				 then (bthm,v)::map
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   602
				 else map)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   603
				 ([],HOL4TypeMaps.get thy)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   604
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   605
	val defmaps =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   606
	    StringPair.foldl (fn (map,((bthy,bthm),v)) =>
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   607
				 if bthy = thyname
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   608
				 then (bthm,v)::map
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   609
				 else map)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   610
				 ([],HOL4DefMaps.get thy)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   611
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   612
	fun new_name internal isa =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   613
	    if internal
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   614
	    then
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   615
		let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   616
		    val paths = NameSpace.unpack isa
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   617
		    val i = drop(length paths - 2,paths)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   618
		in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   619
		    case i of
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   620
			[seg,con] => output_thy ^ "." ^ seg ^ "." ^ con
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   621
		      | _ => error "hol4rews.dump internal error"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   622
		end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   623
	    else
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   624
		isa
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   625
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   626
	val _ = out "import\n\n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   627
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   628
	val _ = out ("import_segment " ^ trans_string import_segment ^ "\n\n")
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   629
	val _ = if null defmaps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   630
		then ()
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   631
		else out "def_maps"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   632
	val _ = app (fn (hol,isa) =>
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   633
			out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string isa))) defmaps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   634
	val _ = if null defmaps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   635
		then ()
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   636
		else out "\n\n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   637
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   638
	val _ = if null typemaps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   639
		then ()
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   640
		else out "type_maps"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   641
	val _ = app (fn (hol,(internal,isa)) =>
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   642
			out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string (new_name internal isa)))) typemaps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   643
	val _ = if null typemaps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   644
		then ()
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   645
		else out "\n\n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   646
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   647
	val _ = if null constmaps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   648
		then ()
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   649
		else out "const_maps"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   650
	val _ = app (fn (hol,(internal,isa,opt_ty)) =>
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   651
			(out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy)));
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   652
			 case opt_ty of
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   653
			     Some ty => out (" :: \"" ^ (string_of_ctyp (ctyp_of sg ty)) ^ "\"")
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   654
			   | None => ())) constmaps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   655
	val _ = if null constmaps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   656
		then ()
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   657
		else out "\n\n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   658
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   659
	val _ = if null constrenames
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   660
		then ()
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   661
		else out "const_renames"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   662
	val _ = app (fn (old,new) =>
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   663
			out ("\n  " ^ (trans_string old) ^ " > " ^ (trans_string new))) constrenames
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   664
	val _ = if null constrenames
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   665
		then ()
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   666
		else out "\n\n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   667
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   668
	val _ = if null mapped
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   669
		then ()
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   670
		else out "thm_maps"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   671
	val _ = app (fn (hol,isa) => out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string isa))) mapped
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   672
	val _ = if null mapped 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   673
		then ()
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   674
		else out "\n\n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   675
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   676
	val _ = if null ignored
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   677
		then ()
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   678
		else out "ignore_thms"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   679
	val _ = app (fn ign => out ("\n  " ^ (trans_string ign))) ignored
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   680
	val _ = if null ignored
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   681
		then ()
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   682
		else out "\n\n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   683
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   684
	val _ = out "end\n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   685
	val _ = TextIO.closeOut os
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   686
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   687
	thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   688
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   689
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   690
fun set_used_names names thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   691
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   692
	val unames = HOL4UNames.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   693
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   694
	case unames of
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   695
	    [] => HOL4UNames.put names thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   696
	  | _ => error "hol4rews.set_used_names called on initialized data!"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   697
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   698
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   699
val clear_used_names = HOL4UNames.put HOL4UNamesArgs.empty
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   700
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   701
fun get_defmap thyname const thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   702
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   703
	val maps = HOL4DefMaps.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   704
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   705
	StringPair.lookup(maps,(thyname,const))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   706
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   707
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   708
fun add_defmap thyname const defname thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   709
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   710
	val _ = message ("Adding defmap " ^ thyname ^ "." ^ const ^ " --> " ^ defname)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   711
	val maps = HOL4DefMaps.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   712
	val maps' = StringPair.update_new(((thyname,const),defname),maps)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   713
	val thy' = HOL4DefMaps.put maps' thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   714
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   715
	thy'
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   716
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   717
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   718
fun get_defname thyname name thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   719
    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   720
	val maps = HOL4DefMaps.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   721
	fun F dname = (dname,add_defmap thyname name dname thy)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   722
    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   723
	case StringPair.lookup(maps,(thyname,name)) of
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   724
	    Some thmname => (thmname,thy)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   725
	  | None =>
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   726
	    let
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   727
		val used = HOL4UNames.get thy
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   728
		val defname = def_name name
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   729
		val pdefname = name ^ "_primdef"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   730
	    in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   731
		if not (defname mem used)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   732
		then F defname                 (* name_def *)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   733
		else if not (pdefname mem used)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   734
		then F pdefname                (* name_primdef *)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   735
		else F (variant used pdefname) (* last resort *)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   736
	    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   737
    end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   738
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   739
local
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   740
    fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==", _],_,_]] = x
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   741
      | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "all", _],_]] = x
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   742
      | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==>", _],_,_]] = x
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   743
      | handle_meta [x] = Appl[Constant "Trueprop",x]
14518
c3019a66180f Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents: 14516
diff changeset
   744
      | handle_meta _ = error "hol4rews error: Trueprop not applied to single argument"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   745
in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   746
val smarter_trueprop_parsing = [("Trueprop",handle_meta)]
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   747
end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   748
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   749
local
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   750
    fun initial_maps thy =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   751
	thy |> add_hol4_type_mapping "min" "bool" false "bool"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   752
	    |> add_hol4_type_mapping "min" "fun" false "fun"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   753
	    |> add_hol4_type_mapping "min" "ind" false "Nat.ind"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   754
	    |> add_hol4_const_mapping "min" "=" false "op ="
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   755
	    |> add_hol4_const_mapping "min" "==>" false "op -->"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   756
	    |> add_hol4_const_mapping "min" "@" false "Hilbert_Choice.Eps"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   757
in
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   758
val hol4_setup =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   759
    [HOL4Rewrites.init,
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   760
     HOL4Maps.init,
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   761
     HOL4UNames.init,
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   762
     HOL4DefMaps.init,
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   763
     HOL4Moves.init,
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   764
     HOL4CMoves.init,
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   765
     HOL4ConstMaps.init,
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   766
     HOL4Rename.init,
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   767
     HOL4TypeMaps.init,
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   768
     HOL4Pending.init,
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   769
     HOL4Thms.init,
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   770
     HOL4Dump.init,
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   771
     HOL4DefThy.init,
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   772
     HOL4Imports.init,
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   773
     ImportSegment.init,
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   774
     initial_maps,
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   775
     Attrib.add_attributes [("hol4rew",
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   776
			     (Attrib.no_args add_hol4_rewrite,
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   777
			      Attrib.no_args Attrib.undef_local_attribute),
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   778
			     "HOL4 rewrite rule")]]
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   779
end