--- a/src/FOLP/simp.ML Tue Sep 25 13:28:35 2007 +0200
+++ b/src/FOLP/simp.ML Tue Sep 25 13:28:37 2007 +0200
@@ -594,7 +594,7 @@
let
fun readfT(f,s) =
let
- val T = Logic.incr_tvar 9 (Sign.read_typ thy s);
+ val T = Logic.incr_tvar 9 (Syntax.read_typ_global thy s);
val t = case Sign.const_type thy f of
SOME(_) => Const(f,T) | NONE => Free(f,T)
in (t,T) end
--- a/src/HOL/Import/import_syntax.ML Tue Sep 25 13:28:35 2007 +0200
+++ b/src/HOL/Import/import_syntax.ML Tue Sep 25 13:28:37 2007 +0200
@@ -137,7 +137,7 @@
val thyname = get_import_thy thy
in
Library.foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol false isa thy
- | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol false isa (Sign.read_typ thy ty) thy) (thy,constmaps)
+ | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol false isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)
end)
val const_moves = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
@@ -147,7 +147,7 @@
val thyname = get_import_thy thy
in
Library.foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol true isa thy
- | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol true isa (Sign.read_typ thy ty) thy) (thy,constmaps)
+ | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol true isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)
end)
fun import_thy s =
--- a/src/HOL/Import/proof_kernel.ML Tue Sep 25 13:28:35 2007 +0200
+++ b/src/HOL/Import/proof_kernel.ML Tue Sep 25 13:28:37 2007 +0200
@@ -10,7 +10,7 @@
type term
type thm
type ('a,'b) subst
-
+
type proof_info
datatype proof = Proof of proof_info * proof_content
and proof_content
@@ -111,8 +111,8 @@
val new_type_definition : string -> string -> string -> thm -> theory -> theory * thm
val new_axiom : string -> term -> theory -> theory * thm
- val prin : term -> unit
- val protect_factname : string -> string
+ val prin : term -> unit
+ val protect_factname : string -> string
val replay_protect_varname : string -> string -> unit
val replay_add_dump : string -> theory -> theory
end
@@ -125,7 +125,7 @@
type ('a,'b) subst = ('a * 'b) list
datatype thm = HOLThm of (Term.term * Term.term) list * Thm.thm
-fun hthm2thm (HOLThm (_, th)) = th
+fun hthm2thm (HOLThm (_, th)) = th
fun to_hol_thm th = HOLThm ([], th)
@@ -134,7 +134,7 @@
datatype proof_info
= Info of {disk_info: (string * string) option ref}
-
+
datatype proof = Proof of proof_info * proof_content
and proof_content
= PRefl of term
@@ -176,7 +176,7 @@
exception PK of string * string
fun ERR f mesg = PK (f,mesg)
-fun print_exn e =
+fun print_exn e =
case e of
PK (m,s) => (writeln ("PK (" ^ m ^ "): " ^ s); raise e)
| _ => OldGoals.print_exn e
@@ -213,21 +213,23 @@
fun smart_string_of_cterm ct =
let
val {thy,t,T,...} = rep_cterm ct
+ val ctxt = ProofContext.init thy
(* Hack to avoid parse errors with Trueprop *)
val ct = (cterm_of thy (HOLogic.dest_Trueprop t)
handle TERM _ => ct)
- fun match cu = t aconv (term_of cu)
+ fun match u = t aconv u
fun G 0 = Library.setmp show_types true (Library.setmp show_sorts true)
| G 1 = Library.setmp show_brackets true (G 0)
| G 2 = Library.setmp show_all_types true (G 0)
| G 3 = Library.setmp show_brackets true (G 2)
- | G _ = raise SMART_STRING
+ | G _ = raise SMART_STRING
fun F n =
let
val str = Library.setmp show_brackets false (G n string_of_cterm) ct
- val cu = Thm.read_cterm thy (str,T)
+ val u = Syntax.parse_term ctxt str
+ |> TypeInfer.constrain T |> Syntax.check_term ctxt
in
- if match cu
+ if match u
then quote str
else F (n+1)
end
@@ -237,7 +239,7 @@
PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0
end
handle ERROR mesg => simple_smart_string_of_cterm ct
-
+
val smart_string_of_thm = smart_string_of_cterm o cprop_of
fun prth th = writeln (PrintMode.setmp [] string_of_thm th)
@@ -272,20 +274,20 @@
in
F
end
-fun i mem L =
- let fun itr [] = false
- | itr (a::rst) = i=a orelse itr rst
+fun i mem L =
+ let fun itr [] = false
+ | itr (a::rst) = i=a orelse itr rst
in itr L end;
-
+
fun insert i L = if i mem L then L else i::L
-
+
fun mk_set [] = []
| mk_set (a::rst) = insert a (mk_set rst)
-
+
fun [] union S = S
| S union [] = S
| (a::rst) union S2 = rst union (insert a S2)
-
+
fun implode_subst [] = []
| implode_subst (x::r::rest) = ((x,r)::(implode_subst rest))
| implode_subst _ = raise ERR "implode_subst" "malformed substitution list"
@@ -300,7 +302,7 @@
fun merge (Tag tag1) (Tag tag2) = Tag (Lib.union(tag1,tag2))
end
-(* Acutal code. *)
+(* Actual code. *)
fun get_segment thyname l = (Lib.assoc "s" l
handle PK _ => thyname)
@@ -430,8 +432,8 @@
fun mk_thy_const thy Thy Nam Ty = Const(intern_const_name Thy Nam thy,Ty)
-local
- fun get_const sg thyname name =
+local
+ fun get_const sg thyname name =
(case Sign.const_type sg name of
SOME ty => Const (name, ty)
| NONE => raise ERR "get_type" (name ^ ": No such constant"))
@@ -472,16 +474,16 @@
val check_name_thy = theory "Main"
fun valid_boundvarname s =
- can (fn () => Thm.read_cterm check_name_thy ("SOME "^s^". True", dummyT)) ();
+ can (fn () => Syntax.read_term_global check_name_thy ("SOME "^s^". True")) ();
fun valid_varname s =
- can (fn () => Thm.read_cterm check_name_thy (s, dummyT)) ();
+ can (fn () => Syntax.read_term_global check_name_thy s) ();
fun protect_varname s =
if innocent_varname s andalso valid_varname s then s else
case Symtab.lookup (!protected_varnames) s of
SOME t => t
- | NONE =>
+ | NONE =>
let
val _ = inc invented_isavar
val t = "u_" ^ string_of_int (!invented_isavar)
@@ -493,56 +495,56 @@
exception REPLAY_PROTECT_VARNAME of string*string*string
-fun replay_protect_varname s t =
+fun replay_protect_varname s t =
case Symtab.lookup (!protected_varnames) s of
SOME t' => raise REPLAY_PROTECT_VARNAME (s, t, t')
- | NONE =>
+ | NONE =>
let
val _ = inc invented_isavar
val t = "u_" ^ string_of_int (!invented_isavar)
val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
in
()
- end
-
+ end
+
fun protect_boundvarname s = if innocent_varname s andalso valid_boundvarname s then s else "u"
fun mk_lambda (v as Free (x, T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t))
| mk_lambda (v as Var ((x, _), T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t))
| mk_lambda v t = raise TERM ("lambda", [v, t]);
-
-fun replacestr x y s =
+
+fun replacestr x y s =
let
val xl = explode x
val yl = explode y
fun isprefix [] ys = true
| isprefix (x::xs) (y::ys) = if x = y then isprefix xs ys else false
- | isprefix _ _ = false
+ | isprefix _ _ = false
fun isp s = isprefix xl s
fun chg s = yl@(List.drop (s, List.length xl))
fun r [] = []
- | r (S as (s::ss)) = if isp S then r (chg S) else s::(r ss)
+ | r (S as (s::ss)) = if isp S then r (chg S) else s::(r ss)
in
implode(r (explode s))
-end
+end
fun protect_factname s = replacestr "." "_dot_" s
-fun unprotect_factname s = replacestr "_dot_" "." s
+fun unprotect_factname s = replacestr "_dot_" "." s
val ty_num_prefix = "N_"
fun startsWithDigit s = Char.isDigit (hd (String.explode s))
-fun protect_tyname tyn =
+fun protect_tyname tyn =
let
- val tyn' =
- if String.isPrefix ty_num_prefix tyn then raise (ERR "protect_ty_name" ("type name '"^tyn^"' is reserved")) else
+ val tyn' =
+ if String.isPrefix ty_num_prefix tyn then raise (ERR "protect_ty_name" ("type name '"^tyn^"' is reserved")) else
(if startsWithDigit tyn then ty_num_prefix^tyn else tyn)
in
tyn'
end
-fun protect_constname tcn = tcn
+fun protect_constname tcn = tcn
(* if tcn = ".." then "dotdot"
else if tcn = "==" then "eqeq"
else tcn*)
@@ -634,9 +636,9 @@
in
mk_comb(f,a)
end
- | gtfx (Elem("tml",[("x",tmx),("a",tma)],[])) =
- let
- val x = get_term_from_index thy thyname types terms tmx
+ | gtfx (Elem("tml",[("x",tmx),("a",tma)],[])) =
+ let
+ val x = get_term_from_index thy thyname types terms tmx
val a = get_term_from_index thy thyname types terms tma
in
mk_lambda x a
@@ -683,7 +685,7 @@
in
Option.map (fn p => OS.Path.joinDirFile {dir = p, file = thyname}) (find path)
end
-
+
fun proof_file_name thyname thmname thy =
let
val path = case get_proof_dir thyname thy of
@@ -693,7 +695,7 @@
in
OS.Path.joinDirFile {dir = path, file = OS.Path.joinBaseExt {base = (unprotect_factname thmname), ext = SOME "prf"}}
end
-
+
fun xml_to_proof thyname types terms prf thy =
let
val xml_to_hol_type = TypeNet.get_type_from_xml thy thyname types
@@ -936,18 +938,18 @@
x2p prf
end
-fun import_proof_concl thyname thmname thy =
+fun import_proof_concl thyname thmname thy =
let
val is = TextIO.openIn(proof_file_name thyname thmname thy)
val (proof_xml,_) = scan_tag (LazySeq.of_instream is)
val _ = TextIO.closeIn is
- in
+ in
case proof_xml of
Elem("proof",[],xtypes::xterms::prf::rest) =>
let
val types = TypeNet.input_types thyname xtypes
val terms = TermNet.input_terms thyname types xterms
- fun f xtm thy = TermNet.get_term_from_xml thy thyname types terms xtm
+ fun f xtm thy = TermNet.get_term_from_xml thy thyname types terms xtm
in
case rest of
[] => NONE
@@ -962,7 +964,7 @@
val is = TextIO.openIn(proof_file_name thyname thmname thy)
val (proof_xml,_) = scan_tag (LazySeq.of_instream is)
val _ = TextIO.closeIn is
- in
+ in
case proof_xml of
Elem("proof",[],xtypes::xterms::prf::rest) =>
let
@@ -1068,7 +1070,7 @@
res
end
-val permute_prems = Thm.permute_prems
+val permute_prems = Thm.permute_prems
fun rearrange sg tm th =
let
@@ -1152,26 +1154,26 @@
| name_of _ = ERR "name_of"
fun new_name' bump map n =
let val n' = n^bump in
- if is_old_name n' orelse Symtab.lookup map n' <> NONE then
+ if is_old_name n' orelse Symtab.lookup map n' <> NONE then
new_name' (Symbol.bump_string bump) map n
else
n'
- end
+ end
val new_name = new_name' "a"
fun replace_name n' (Free (n, t)) = Free (n', t)
| replace_name n' _ = ERR "replace_name"
- (* map: old or fresh name -> old free,
+ (* map: old or fresh name -> old free,
invmap: old free which has fresh name assigned to it -> fresh name *)
fun dis (v, mapping as (map,invmap)) =
let val n = name_of v in
case Symtab.lookup map n of
NONE => (Symtab.update (n, v) map, invmap)
- | SOME v' =>
- if v=v' then
- mapping
+ | SOME v' =>
+ if v=v' then
+ mapping
else
let val n' = new_name map n in
- (Symtab.update (n', v) map,
+ (Symtab.update (n', v) map,
Termtab.update (v, n') invmap)
end
end
@@ -1179,16 +1181,16 @@
if (length freenames = length frees) then
thm
else
- let
- val (_, invmap) =
- List.foldl dis (Symtab.empty, Termtab.empty) frees
+ let
+ val (_, invmap) =
+ List.foldl dis (Symtab.empty, Termtab.empty) frees
fun make_subst ((oldfree, newname), (intros, elims)) =
- (cterm_of thy oldfree :: intros,
+ (cterm_of thy oldfree :: intros,
cterm_of thy (replace_name newname oldfree) :: elims)
val (intros, elims) = List.foldl make_subst ([], []) (Termtab.dest invmap)
- in
+ in
forall_elim_list elims (forall_intr_list intros thm)
- end
+ end
end
val debug = ref false
@@ -1201,7 +1203,7 @@
fun get_hol4_thm thyname thmname thy =
case get_hol4_theorem thyname thmname thy of
SOME hth => SOME (HOLThm hth)
- | NONE =>
+ | NONE =>
let
val pending = HOL4Pending.get thy
in
@@ -1215,7 +1217,7 @@
c = "All" orelse
c = "op -->" orelse
c = "op &" orelse
- c = "op =")) (Term.term_consts tm)
+ c = "op =")) (Term.term_consts tm)
fun match_consts t (* th *) =
let
@@ -1291,7 +1293,7 @@
end
| SOME NONE => error ("Trying to access ignored theorem " ^ thmname)
| NONE =>
- let
+ let
val _ = (message "Looking for conclusion:";
if_debug prin isaconc)
val cs = non_trivial_term_consts isaconc
@@ -1325,7 +1327,7 @@
val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
in
case concl_of i2h_conc of
- Const("==",_) $ lhs $ _ =>
+ Const("==",_) $ lhs $ _ =>
(warning ("Failed lookup of theorem '"^thmname^"':");
writeln "Original conclusion:";
prin hol4conc';
@@ -1334,10 +1336,10 @@
| _ => ()
end
in
- case b of
+ case b of
NONE => (warn () handle _ => (); (a,b))
| _ => (a, b)
- end
+ end
fun get_thm thyname thmname thy =
case get_hol4_thm thyname thmname thy of
@@ -1373,11 +1375,11 @@
val rew = rewrite_hol4_term (concl_of th) thy
val th = equal_elim rew th
val thy' = add_hol4_pending thyname thmname args thy
- val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
+ val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
val th = disambiguate_frees th
val thy2 = if gen_output
- then add_dump ("lemma " ^ (quotename thmname) ^ ": " ^
- (smart_string_of_thm th) ^ "\n by (import " ^
+ then add_dump ("lemma " ^ (quotename thmname) ^ ": " ^
+ (smart_string_of_thm th) ^ "\n by (import " ^
thyname ^ " " ^ (quotename thmname) ^ ")") thy'
else thy'
in
@@ -1768,7 +1770,7 @@
in
(thy,res)
end
-
+
fun CCONTR tm hth thy =
let
@@ -1851,7 +1853,7 @@
end) th vlist'
end
| SOME _ => raise ERR "GEN_ABS" "Bad constant"
- | NONE =>
+ | NONE =>
foldr (fn (v,th) => mk_ABS v th thy) th vlist'
val res = HOLThm(rens_of info',th1)
val _ = message "RESULT:"
@@ -1947,7 +1949,7 @@
val p3 = string_of_mixfix csyn
val p4 = smart_string_of_cterm crhs
in
- add_dump ("constdefs\n " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n " ^p4) thy''
+ add_dump ("constdefs\n " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n " ^p4) thy''
end
else
(add_dump ("consts\n " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^
@@ -1958,7 +1960,7 @@
| NONE => raise ERR "new_definition" "Bad conclusion"
val fullname = Sign.full_name thy22 thmname
val thy22' = case opt_get_output_thy thy22 of
- "" => (ImportRecorder.add_hol_mapping thyname thmname fullname;
+ "" => (ImportRecorder.add_hol_mapping thyname thmname fullname;
add_hol4_mapping thyname thmname fullname thy22)
| output_thy =>
let
@@ -1982,7 +1984,7 @@
fun new_specification thyname thmname names hth thy =
case HOL4DefThy.get thy of
Replaying _ => (thy,hth)
- | _ =>
+ | _ =>
let
val _ = message "NEW_SPEC:"
val _ = if_debug pth hth
@@ -2005,7 +2007,7 @@
dest_eta_abs abody
| dest_exists tm =
raise ERR "new_specification" "Bad existential formula"
-
+
val (consts,_) = Library.foldl (fn ((cs,ex),cname) =>
let
val (_,cT,p) = dest_exists ex
@@ -2056,11 +2058,11 @@
intern_store_thm false thyname thmname hth thy''
end
handle e => (message "exception in new_specification"; print_exn e)
-
+
end
-
+
fun new_axiom name tm thy = raise ERR "new_axiom" ("Oh, no you don't! (" ^ name ^ ")")
-
+
fun to_isa_thm (hth as HOLThm(_,th)) =
let
val (HOLThm args) = norm_hthm (theory_of_thm th) hth
@@ -2079,7 +2081,7 @@
fun new_type_definition thyname thmname tycname hth thy =
case HOL4DefThy.get thy of
Replaying _ => (thy,hth)
- | _ =>
+ | _ =>
let
val _ = message "TYPE_DEF:"
val _ = if_debug pth hth
@@ -2093,9 +2095,9 @@
val tnames = map fst tfrees
val tsyn = mk_syn thy tycname
val typ = (tycname,tnames,tsyn)
- val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy
+ val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy
val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
-
+
val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
val fulltyname = Sign.intern_type thy' tycname
@@ -2124,11 +2126,11 @@
val proc_prop = if null tnames
then smart_string_of_cterm
else Library.setmp show_all_types true smart_string_of_cterm
- val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " "
+ val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " "
^ (string_of_mixfix tsyn) ^ "\n by (rule typedef_helper,import " ^ thyname ^ " " ^ thmname ^ ")") thy4
-
+
val thy6 = add_dump ("lemmas " ^ thmname ^ " = typedef_hol2hol4 [OF type_definition_" ^ tycname ^ "]") thy5
-
+
val _ = message "RESULT:"
val _ = if_debug pth hth'
in
@@ -2145,19 +2147,19 @@
val eq = quote (constname ^ " == "^rhs)
val d = case defname of NONE => "" | SOME defname => (quotename defname)^" : "
in
- add_dump ("constdefs\n " ^ n ^ " :: \"" ^ t ^ "\" " ^ syn ^ "\n " ^ d ^ eq) thy
+ add_dump ("constdefs\n " ^ n ^ " :: \"" ^ t ^ "\" " ^ syn ^ "\n " ^ d ^ eq) thy
end
-fun add_dump_syntax thy name =
+fun add_dump_syntax thy name =
let
val n = quotename name
val syn = string_of_mixfix (mk_syn thy name)
in
add_dump ("syntax\n "^n^" :: _ "^syn) thy
end
-
+
(*val type_intro_replay_history = ref (Symtab.empty:unit Symtab.table)
-fun choose_upon_replay_history thy s dth =
+fun choose_upon_replay_history thy s dth =
case Symtab.lookup (!type_intro_replay_history) s of
NONE => (type_intro_replay_history := Symtab.update (s, ()) (!type_intro_replay_history); dth)
| SOME _ => HOLThm([], PureThy.get_thm thy (PureThy.Name s))
@@ -2167,7 +2169,7 @@
case HOL4DefThy.get thy of
Replaying _ => (thy,
HOLThm([], PureThy.get_thm thy (PureThy.Name (thmname^"_@intern"))) handle ERROR _ => hth)
- | _ =>
+ | _ =>
let
val _ = message "TYPE_INTRO:"
val _ = if_debug pth hth
@@ -2192,9 +2194,9 @@
val aty = Type (fulltyname, map mk_vartype tnames)
val abs_ty = tT --> aty
val rep_ty = aty --> tT
- val typedef_hol2hollight' =
- Drule.instantiate'
- [SOME (ctyp_of thy' aty), SOME (ctyp_of thy' tT)]
+ val typedef_hol2hollight' =
+ Drule.instantiate'
+ [SOME (ctyp_of thy' aty), SOME (ctyp_of thy' tT)]
[NONE, NONE, NONE, SOME (cterm_of thy' (Free ("a", aty))), SOME (cterm_of thy' (Free ("r", tT)))]
typedef_hol2hollight
val th4 = (#type_definition typedef_info) RS typedef_hol2hollight'
@@ -2209,7 +2211,7 @@
val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th4))
val thy4 = add_hol4_pending thyname thmname args thy''
val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
-
+
val P' = P (* why !? #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4))) *)
val c =
let
@@ -2217,27 +2219,27 @@
in
Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P'
end
-
+
val tnames_string = if null tnames
then ""
else "(" ^ commas tnames ^ ") "
val proc_prop = if null tnames
then smart_string_of_cterm
else Library.setmp show_all_types true smart_string_of_cterm
- val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^
- " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " ^
+ val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^
+ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " ^
(string_of_mixfix tsyn) ^ " morphisms "^
- (quote rep_name)^" "^(quote abs_name)^"\n"^
+ (quote rep_name)^" "^(quote abs_name)^"\n"^
(" apply (rule light_ex_imp_nonempty[where t="^
- (proc_prop (cterm_of thy4 t))^"])\n"^
+ (proc_prop (cterm_of thy4 t))^"])\n"^
(" by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4
val str_aty = string_of_ctyp (ctyp_of thy aty)
- val thy = add_dump_syntax thy rep_name
+ val thy = add_dump_syntax thy rep_name
val thy = add_dump_syntax thy abs_name
- val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^
+ val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^
" = typedef_hol2hollight \n"^
" [where a=\"a :: "^str_aty^"\" and r=r" ^
- " ,\n OF "^(quotename ("type_definition_" ^ tycname)) ^ "]") thy
+ " ,\n OF "^(quotename ("type_definition_" ^ tycname)) ^ "]") thy
val _ = message "RESULT:"
val _ = if_debug pth hth'
in
--- a/src/HOL/Nominal/nominal_primrec.ML Tue Sep 25 13:28:35 2007 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Tue Sep 25 13:28:37 2007 +0200
@@ -380,10 +380,9 @@
fun gen_primrec note def alt_name invs fctxt eqns thy =
let
- fun readt T s = term_of (Thm.read_cterm thy (s, T));
val ((names, strings), srcss) = apfst split_list (split_list eqns);
val atts = map (map (Attrib.attribute thy)) srcss;
- val eqn_ts = map (fn s => readt propT s
+ val eqn_ts = map (fn s => Syntax.read_prop_global thy s
handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s)) strings;
val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq
(HOLogic.dest_Trueprop (Logic.strip_imp_concl eq))))
@@ -391,8 +390,8 @@
val (_, eqn_ts') = PrimrecPackage.unify_consts thy rec_ts eqn_ts
in
gen_primrec_i note def alt_name
- (Option.map (map (readt dummyT)) invs)
- (Option.map (readt dummyT) fctxt)
+ (Option.map (map (Syntax.read_term_global thy)) invs)
+ (Option.map (Syntax.read_term_global thy) fctxt)
(names ~~ eqn_ts' ~~ atts) thy
end;
--- a/src/HOL/Tools/TFL/post.ML Tue Sep 25 13:28:35 2007 +0200
+++ b/src/HOL/Tools/TFL/post.ML Tue Sep 25 13:28:37 2007 +0200
@@ -245,7 +245,8 @@
in (thy, {rules = rules', induct = induct, tcs = tcs}) end;
fun define strict thy cs ss congs wfs fid R seqs =
- define_i strict thy cs ss congs wfs fid (Sign.read_term thy R) (map (Sign.read_term thy) seqs)
+ define_i strict thy cs ss congs wfs fid
+ (Syntax.read_term_global thy R) (map (Syntax.read_term_global thy) seqs)
handle U.ERR {mesg,...} => error mesg;
@@ -272,7 +273,7 @@
end
fun defer thy congs fid seqs =
- defer_i thy congs fid (map (Sign.read_term thy) seqs)
+ defer_i thy congs fid (map (Syntax.read_term_global thy) seqs)
handle U.ERR {mesg,...} => error mesg;
end;
--- a/src/HOL/Tools/primrec_package.ML Tue Sep 25 13:28:35 2007 +0200
+++ b/src/HOL/Tools/primrec_package.ML Tue Sep 25 13:28:37 2007 +0200
@@ -310,7 +310,7 @@
let
val ((names, strings), srcss) = apfst split_list (split_list eqns);
val atts = map (map (Attrib.attribute thy)) srcss;
- val eqn_ts = map (fn s => term_of (Thm.read_cterm thy (s, propT))
+ val eqn_ts = map (fn s => Syntax.read_prop_global thy s
handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s)) strings;
val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop eq)))
handle TERM _ => primrec_eq_err thy "not a proper equation" eq) eqn_ts;
--- a/src/HOL/Tools/specification_package.ML Tue Sep 25 13:28:35 2007 +0200
+++ b/src/HOL/Tools/specification_package.ML Tue Sep 25 13:28:37 2007 +0200
@@ -121,7 +121,7 @@
| myfoldr f [] = error "SpecificationPackage.process_spec internal error"
val rew_imps = alt_props |>
- map (ObjectLogic.atomize o Thm.read_cterm thy o rpair Term.propT o snd)
+ map (ObjectLogic.atomize o Thm.cterm_of thy o Syntax.read_prop_global thy o snd)
val props' = rew_imps |>
map (HOLogic.dest_Trueprop o term_of o snd o Thm.dest_equals o cprop_of)
@@ -144,7 +144,7 @@
val thawed_prop_consts = collect_consts (prop_thawed,[])
val (altcos,overloaded) = Library.split_list cos
val (names,sconsts) = Library.split_list altcos
- val consts = map (term_of o Thm.read_cterm thy o rpair dummyT) sconsts
+ val consts = map (Syntax.read_term_global thy) sconsts
val _ = not (Library.exists (not o Term.is_Const) consts)
orelse error "Specification: Non-constant found as parameter"
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Tue Sep 25 13:28:35 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Tue Sep 25 13:28:37 2007 +0200
@@ -149,7 +149,7 @@
fun hd_of (Const(a,_)) = a |
hd_of (t $ _) = hd_of t |
hd_of _ = raise malformed;
-val trm = Sign.simple_read_term thy (Sign.read_typ thy atypstr) s;
+val trm = Sign.simple_read_term thy (Syntax.read_typ_global thy atypstr) s;
in
hd_of trm handle malformed =>
error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s)
@@ -330,10 +330,10 @@
(writeln("Constructing automaton " ^ automaton_name ^ " ...");
let
val state_type_string = type_product_of_varlist(statetupel);
-val styp = Sign.read_typ thy state_type_string;
+val styp = Syntax.read_typ_global thy state_type_string;
val state_vars_tupel = "(" ^ (comma_list_of_varlist statetupel) ^ ")";
val state_vars_primed = "(" ^ (primed_comma_list_of_varlist statetupel) ^ ")";
-val atyp = Sign.read_typ thy action_type;
+val atyp = Syntax.read_typ_global thy action_type;
val inp_set_string = action_set_string thy atyp inp;
val out_set_string = action_set_string thy atyp out;
val int_set_string = action_set_string thy atyp int;
@@ -426,7 +426,7 @@
end)
fun ren_act_type_of thy funct =
- (case Term.fastype_of (Sign.read_term thy funct) of
+ (case Term.fastype_of (Syntax.read_term_global thy funct) of
Type ("fun", [a, b]) => a
| _ => error "could not extract argument type of renaming function term");
--- a/src/HOLCF/Tools/cont_consts.ML Tue Sep 25 13:28:35 2007 +0200
+++ b/src/HOLCF/Tools/cont_consts.ML Tue Sep 25 13:28:37 2007 +0200
@@ -91,7 +91,7 @@
|> Sign.add_trrules_i (List.concat (map third transformed_decls))
end;
-val add_consts = gen_add_consts Sign.read_typ;
+val add_consts = gen_add_consts Syntax.read_typ_global;
val add_consts_i = gen_add_consts Sign.certify_typ;
--- a/src/HOLCF/Tools/domain/domain_extender.ML Tue Sep 25 13:28:35 2007 +0200
+++ b/src/HOLCF/Tools/domain/domain_extender.ML Tue Sep 25 13:28:37 2007 +0200
@@ -100,7 +100,7 @@
fun gen_add_domain prep_typ (comp_dnam, eqs''') thy''' =
let
val dtnvs = map ((fn (dname,vs) =>
- (Sign.full_name thy''' dname, map (Sign.read_typ thy''') vs))
+ (Sign.full_name thy''' dname, map (Syntax.read_typ_global thy''') vs))
o fst) eqs''';
val cons''' = map snd eqs''';
fun thy_type (dname,tvars) = (Sign.base_name dname, length tvars, NoSyn);
@@ -139,7 +139,7 @@
end;
val add_domain_i = gen_add_domain Sign.certify_typ;
-val add_domain = gen_add_domain Sign.read_typ;
+val add_domain = gen_add_domain Syntax.read_typ_global;
(** outer syntax **)
--- a/src/HOLCF/Tools/fixrec_package.ML Tue Sep 25 13:28:35 2007 +0200
+++ b/src/HOLCF/Tools/fixrec_package.ML Tue Sep 25 13:28:37 2007 +0200
@@ -253,7 +253,7 @@
else thy'
end;
-val add_fixrec = gen_add_fixrec Sign.read_prop Attrib.attribute;
+val add_fixrec = gen_add_fixrec Syntax.read_prop_global Attrib.attribute;
val add_fixrec_i = gen_add_fixrec Sign.cert_prop (K I);
@@ -281,7 +281,7 @@
(snd o PureThy.add_thmss [((name, simps), atts)]) thy
end;
-val add_fixpat = gen_add_fixpat Sign.read_term Attrib.attribute;
+val add_fixpat = gen_add_fixpat Syntax.read_term_global Attrib.attribute;
val add_fixpat_i = gen_add_fixpat Sign.cert_term (K I);
--- a/src/Provers/splitter.ML Tue Sep 25 13:28:35 2007 +0200
+++ b/src/Provers/splitter.ML Tue Sep 25 13:28:37 2007 +0200
@@ -103,8 +103,8 @@
val meta_iffD = Data.meta_eq_to_iff RS Data.iffD; (* (P == Q) ==> Q ==> P *)
val lift = Goal.prove_global Pure.thy ["P", "Q", "R"]
- [Sign.read_prop Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"]
- (Sign.read_prop Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
+ [Syntax.read_prop_global Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"]
+ (Syntax.read_prop_global Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
(fn [prem] => rewtac prem THEN rtac reflexive_thm 1)
val trlift = lift RS transitive_thm;
--- a/src/Pure/Isar/class.ML Tue Sep 25 13:28:35 2007 +0200
+++ b/src/Pure/Isar/class.ML Tue Sep 25 13:28:37 2007 +0200
@@ -232,9 +232,10 @@
local
-fun gen_read_def thy prep_att read_def ((raw_name, raw_atts), raw_t) =
+fun gen_read_def thy prep_att parse_prop ((raw_name, raw_atts), raw_t) =
let
- val (_, t) = read_def thy (raw_name, raw_t);
+ val ctxt = ProofContext.init thy;
+ val t = parse_prop ctxt raw_t |> Syntax.check_prop ctxt;
val ((c, ty), _) = Sign.cert_def (Sign.pp thy) t;
val atts = map (prep_att thy) raw_atts;
val insts = Consts.typargs (Sign.consts_of thy) (c, ty);
@@ -243,7 +244,7 @@
| _ => SOME raw_name;
in (c, (insts, ((name, t), atts))) end;
-fun read_def_cmd thy = gen_read_def thy Attrib.intern_src Theory.read_axm;
+fun read_def_cmd thy = gen_read_def thy Attrib.intern_src Syntax.parse_prop;
fun read_def thy = gen_read_def thy (K I) (K I);
fun gen_instance prep_arity read_def do_proof raw_arities raw_defs after_qed theory =
@@ -544,9 +545,9 @@
local
-fun read_param thy raw_t =
+fun read_param thy raw_t = (* FIXME ProofContext.read_const (!?) *)
let
- val t = Sign.read_term thy raw_t
+ val t = Syntax.read_term_global thy raw_t
in case try dest_Const t
of SOME (c, _) => c
| NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
--- a/src/Pure/Isar/code_unit.ML Tue Sep 25 13:28:35 2007 +0200
+++ b/src/Pure/Isar/code_unit.ML Tue Sep 25 13:28:37 2007 +0200
@@ -60,7 +60,7 @@
fun read_bare_const thy raw_t =
let
- val t = Sign.read_term thy raw_t;
+ val t = Syntax.read_term_global thy raw_t;
in case try dest_Const t
of SOME c_ty => c_ty
| NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
--- a/src/Pure/Proof/extraction.ML Tue Sep 25 13:28:35 2007 +0200
+++ b/src/Pure/Proof/extraction.ML Tue Sep 25 13:28:37 2007 +0200
@@ -213,7 +213,7 @@
fun read_condeq thy =
let val thy' = add_syntax thy
in fn s =>
- let val t = Logic.varify (Sign.read_prop thy' s)
+ let val t = Logic.varify (Syntax.read_prop_global thy' s)
in (map Logic.dest_equals (Logic.strip_imp_prems t),
Logic.dest_equals (Logic.strip_imp_concl t))
end handle TERM _ => error ("Not a (conditional) meta equality:\n" ^ s)
--- a/src/Pure/codegen.ML Tue Sep 25 13:28:35 2007 +0200
+++ b/src/Pure/codegen.ML Tue Sep 25 13:28:37 2007 +0200
@@ -197,7 +197,7 @@
fun set_default_type s thy ({size, iterations, ...} : test_params) =
{size = size, iterations = iterations,
- default_type = SOME (Sign.read_typ thy s)};
+ default_type = SOME (Syntax.read_typ_global thy s)};
(* theory data *)
@@ -1112,7 +1112,7 @@
(Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
(fn xs => Toplevel.theory (fn thy => fold (assoc_type o
(fn ((name, mfx), aux) => (name, (parse_mixfix
- (Sign.read_typ thy) mfx, aux)))) xs thy)));
+ (Syntax.read_typ_global thy) mfx, aux)))) xs thy)));
val assoc_constP =
OuterSyntax.command "consts_code"
@@ -1171,7 +1171,7 @@
fun parse_tyinst xs =
(P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>
- fn (x, ys) => (x, (v, Sign.read_typ thy s) :: ys))) xs;
+ fn (x, ys) => (x, (v, Syntax.read_typ_global thy s) :: ys))) xs;
val test_paramsP =
OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl
--- a/src/Pure/meta_simplifier.ML Tue Sep 25 13:28:35 2007 +0200
+++ b/src/Pure/meta_simplifier.ML Tue Sep 25 13:28:37 2007 +0200
@@ -646,7 +646,7 @@
(* FIXME avoid global thy and Logic.varify *)
fun simproc_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify);
-fun simproc thy name = simproc_i thy name o map (Sign.read_term thy);
+fun simproc thy name = simproc_i thy name o map (Syntax.read_term_global thy);
local
--- a/src/Pure/sign.ML Tue Sep 25 13:28:35 2007 +0200
+++ b/src/Pure/sign.ML Tue Sep 25 13:28:37 2007 +0200
@@ -492,7 +492,7 @@
let val arity = (prep_tycon thy t, map (prep_sort thy) Ss, prep_sort thy S)
in Type.add_arity (pp thy) arity (tsig_of thy); arity end;
-val read_arity = prep_arity intern_type Syntax.global_read_sort;
+val read_arity = prep_arity intern_type Syntax.read_sort_global;
val cert_arity = prep_arity (K I) certify_sort;
@@ -613,7 +613,7 @@
fun gen_add_defsort prep_sort s thy =
thy |> map_tsig (Type.set_defsort (prep_sort thy s));
-val add_defsort = gen_add_defsort Syntax.global_read_sort;
+val add_defsort = gen_add_defsort Syntax.read_sort_global;
val add_defsort_i = gen_add_defsort certify_sort;
@@ -650,12 +650,13 @@
let
val syn' = Syntax.extend_type_gram [(a, length vs, mx)] syn;
val a' = Syntax.type_name a mx;
- val abbr = (a', vs, certify_typ_mode Type.mode_syntax thy (prep_typ thy rhs))
+ val abbr = (a', vs,
+ certify_typ_mode Type.mode_syntax thy (prep_typ (ProofContext.init thy) rhs))
handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote a');
val tsig' = Type.add_abbrevs naming [abbr] tsig;
in (naming, syn', tsig', consts) end);
-val add_tyabbrs = fold (gen_add_tyabbr Syntax.global_parse_typ);
+val add_tyabbrs = fold (gen_add_tyabbr Syntax.parse_typ);
val add_tyabbrs_i = fold (gen_add_tyabbr (K I));
@@ -663,18 +664,19 @@
fun gen_syntax change_gram prep_typ mode args thy =
let
- fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (prep_typ thy T), mx)
+ fun prep (c, T, mx) = (c,
+ certify_typ_mode Type.mode_syntax thy (prep_typ (ProofContext.init thy) T), mx)
handle ERROR msg =>
cat_error msg ("in syntax declaration " ^ quote (Syntax.const_name c mx));
in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
fun gen_add_syntax x = gen_syntax Syntax.extend_const_gram x;
-val add_modesyntax = gen_add_syntax Syntax.global_parse_typ;
+val add_modesyntax = gen_add_syntax Syntax.parse_typ;
val add_modesyntax_i = gen_add_syntax (K I);
val add_syntax = add_modesyntax Syntax.default_mode;
val add_syntax_i = add_modesyntax_i Syntax.default_mode;
-val del_modesyntax = gen_syntax Syntax.remove_const_gram Syntax.global_parse_typ;
+val del_modesyntax = gen_syntax Syntax.remove_const_gram Syntax.parse_typ;
val del_modesyntax_i = gen_syntax Syntax.remove_const_gram (K I);
fun const_syntax thy (Const (c, _), mx) = try (Consts.syntax (consts_of thy)) (c, mx)
--- a/src/ZF/Tools/datatype_package.ML Tue Sep 25 13:28:35 2007 +0200
+++ b/src/ZF/Tools/datatype_package.ML Tue Sep 25 13:28:37 2007 +0200
@@ -335,7 +335,7 @@
con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc. *)
fun mk_free s =
let val thy = theory_of_thm elim in (*Don't use thy1: it will be stale*)
- Goal.prove_global thy [] [] (Sign.read_prop thy s)
+ Goal.prove_global thy [] [] (Syntax.read_prop_global thy s)
(fn _ => EVERY
[rewrite_goals_tac con_defs,
fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1])
--- a/src/ZF/Tools/primrec_package.ML Tue Sep 25 13:28:35 2007 +0200
+++ b/src/ZF/Tools/primrec_package.ML Tue Sep 25 13:28:37 2007 +0200
@@ -197,7 +197,7 @@
fun add_primrec args thy =
add_primrec_i (map (fn ((name, s), srcs) =>
- ((name, Sign.read_prop thy s), map (Attrib.attribute thy) srcs))
+ ((name, Syntax.read_prop_global thy s), map (Attrib.attribute thy) srcs))
args) thy;