# HG changeset patch # User paulson # Date 824490047 -3600 # Node ID ce37c64244c0cd915a60c9a9d182e298f6ef8625 # Parent 09354d37a5abf80c4f756831d55ce3425c9f2db5 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted. diff -r 09354d37a5ab -r ce37c64244c0 doc-src/Logics/logics.bbl --- a/doc-src/Logics/logics.bbl Fri Feb 16 17:24:51 1996 +0100 +++ b/doc-src/Logics/logics.bbl Fri Feb 16 18:00:47 1996 +0100 @@ -173,8 +173,9 @@ \bibitem{paulson-CADE} Lawrence~C. Paulson. \newblock A fixedpoint approach to implementing (co)inductive definitions. -\newblock In Alan Bundy, editor, {\em 12th International Conference on - Automated Deduction}, LNAI 814, pages 148--161. Springer, 1994. +\newblock In Alan Bundy, editor, {\em Automated Deduction --- {CADE}-12}, LNAI + 814, pages 148--161. Springer, 1994. +\newblock 12th international conference. \bibitem{paulson-set-II} Lawrence~C. Paulson. diff -r 09354d37a5ab -r ce37c64244c0 src/FOLP/simp.ML --- a/src/FOLP/simp.ML Fri Feb 16 17:24:51 1996 +0100 +++ b/src/FOLP/simp.ML Fri Feb 16 18:00:47 1996 +0100 @@ -135,7 +135,7 @@ in mk trans_thms end; (*Applies tactic and returns the first resulting state, FAILS if none!*) -fun one_result(tac,thm) = case Sequence.pull(tapply(tac,thm)) of +fun one_result(tac,thm) = case Sequence.pull(tac thm) of Some(thm',_) => thm' | None => raise THM("Simplifier: could not continue", 0, [thm]); @@ -211,7 +211,7 @@ resolve_tac congs 1 ORELSE refl1_tac | Free _ => resolve_tac congs 1 ORELSE refl1_tac | _ => refl1_tac)) - val Some(thm'',_) = Sequence.pull(tapply(add_norm_tac,thm')) + val Some(thm'',_) = Sequence.pull(add_norm_tac thm') in thm'' end; fun add_norm_tags congs = @@ -336,19 +336,19 @@ in find_if(tm,0) end; fun IF1_TAC cong_tac i = - let fun seq_try (ifth::ifths,ifc::ifcs) thm = tapply( - COND (if_rewritable ifc i) (DETERM(rtac ifth i)) - (Tactic(seq_try(ifths,ifcs))), thm) - | seq_try([],_) thm = tapply(no_tac,thm) - and try_rew thm = tapply(Tactic(seq_try(case_rews,case_consts)) - ORELSE Tactic one_subt, thm) + let fun seq_try (ifth::ifths,ifc::ifcs) thm = + (COND (if_rewritable ifc i) (DETERM(rtac ifth i)) + (seq_try(ifths,ifcs))) thm + | seq_try([],_) thm = no_tac thm + and try_rew thm = (seq_try(case_rews,case_consts) ORELSE one_subt) thm and one_subt thm = let val test = has_fewer_prems (nprems_of thm + 1) - fun loop thm = tapply(COND test no_tac - ((Tactic try_rew THEN DEPTH_FIRST test (refl_tac i)) - ORELSE (refl_tac i THEN Tactic loop)), thm) - in tapply(cong_tac THEN Tactic loop, thm) end - in COND (may_match(case_consts,i)) (Tactic try_rew) no_tac end; + fun loop thm = + COND test no_tac + ((try_rew THEN DEPTH_FIRST test (refl_tac i)) + ORELSE (refl_tac i THEN loop)) thm + in (cong_tac THEN loop) thm end + in COND (may_match(case_consts,i)) try_rew no_tac end; fun CASE_TAC (SS{cong_net,...}) i = let val cong_tac = net_tac cong_net i @@ -422,7 +422,7 @@ fun simp_lhs(thm,ss,anet,ats,cs) = if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs) - else case Sequence.pull(tapply(cong_tac i,thm)) of + else case Sequence.pull(cong_tac i thm) of Some(thm',_) => let val ps = prems_of thm and ps' = prems_of thm'; val n = length(ps')-length(ps); @@ -455,12 +455,12 @@ thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs) end | None => if more - then rew(tapply(lhs_net_tac anet i THEN assume_tac i,thm), + then rew((lhs_net_tac anet i THEN assume_tac i) thm, thm,ss,anet,ats,cs,false) else (ss,thm,anet,ats,cs); fun try_true(thm,ss,anet,ats,cs) = - case Sequence.pull(tapply(auto_tac i,thm)) of + case Sequence.pull(auto_tac i thm) of Some(thm',_) => (ss,thm',anet,ats,cs) | None => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs in if !tracing @@ -471,7 +471,7 @@ end; fun if_exp(thm,ss,anet,ats,cs) = - case Sequence.pull(tapply(IF1_TAC (cong_tac i) i,thm)) of + case Sequence.pull (IF1_TAC (cong_tac i) i thm) of Some(thm',_) => (SIMP_LHS::IF::ss,thm',anet,ats,cs) | None => (ss,thm,anet,ats,cs); @@ -479,7 +479,7 @@ MK_EQ => (ss, res1(thm,[red2],i), anet, ats, cs) | ASMS(a) => add_asms(ss,thm,a,anet,ats,cs) | SIMP_LHS => simp_lhs(thm,ss,anet,ats,cs) - | REW => rew(tapply(net_tac net i,thm),thm,ss,anet,ats,cs,true) + | REW => rew(net_tac net i thm,thm,ss,anet,ats,cs,true) | REFL => (ss, res1(thm,refl_thms,i), anet, ats, cs) | TRUE => try_true(res1(thm,refl_thms,i),ss,anet,ats,cs) | PROVE => (if if_fl then MK_EQ::SIMP_LHS::IF::TRUE::ss @@ -496,10 +496,11 @@ fun EXEC_TAC(ss,fl) (SS{auto_tac,cong_net,simp_net,...}) = let val cong_tac = net_tac cong_net -in fn i => Tactic(fn thm => - if i <= 0 orelse nprems_of thm < i then Sequence.null - else Sequence.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm))) - THEN TRY(auto_tac i) +in fn i => + (fn thm => + if i <= 0 orelse nprems_of thm < i then Sequence.null + else Sequence.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm))) + THEN TRY(auto_tac i) end; val SIMP_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,REFL,STOP],false); diff -r 09354d37a5ab -r ce37c64244c0 src/HOL/ex/meson.ML --- a/src/HOL/ex/meson.ML Fri Feb 16 17:24:51 1996 +0100 +++ b/src/HOL/ex/meson.ML Fri Feb 16 18:00:47 1996 +0100 @@ -158,12 +158,10 @@ val prop_of = #prop o rep_thm; (*Permits forward proof from rules that discharge assumptions*) -fun forward_res nf state = - case Sequence.pull - (tapply(ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)), - state)) +fun forward_res nf st = + case Sequence.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st) of Some(th,_) => th - | None => raise THM("forward_res", 0, [state]); + | None => raise THM("forward_res", 0, [st]); (*Negation Normal Form*) @@ -188,10 +186,10 @@ fun skolemize th = if not (has_consts ["Ex"] (prop_of th)) then th else skolemize (tryres(th, [choice, conj_exD1, conj_exD2, - disj_exD, disj_exD1, disj_exD2])) + disj_exD, disj_exD1, disj_exD2])) handle THM _ => skolemize (forward_res skolemize - (tryres (th, [conj_forward, disj_forward, all_forward]))) + (tryres (th, [conj_forward, disj_forward, all_forward]))) handle THM _ => forward_res skolemize (th RS ex_forward); @@ -243,8 +241,7 @@ (METAHYPS (resop (cnf_nil seen)) 1) THEN (STATE (fn st' => METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1)) - in Sequence.list_of_s (tapply(tac, th RS disj_forward)) @ ths - end + in Sequence.list_of_s (tac (th RS disj_forward)) @ ths end and cnf_nil seen th = cnf_aux seen (th,[]); (*Top-level call to cnf -- it's safe to reset name_ref*) @@ -266,13 +263,13 @@ qed "disj_forward2"; (*Forward proof, passing extra assumptions as theorems to the tactic*) -fun forward_res2 nf hyps state = +fun forward_res2 nf hyps st = case Sequence.pull - (tapply(REPEAT - (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1), - state)) + (REPEAT + (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1) + st) of Some(th,_) => th - | None => raise THM("forward_res2", 0, [state]); + | None => raise THM("forward_res2", 0, [st]); (*Remove duplicates in P|Q by assuming ~P in Q rls (initially []) accumulates assumptions of the form P==>False*) diff -r 09354d37a5ab -r ce37c64244c0 src/HOLCF/ax_ops/thy_ops.ML --- a/src/HOLCF/ax_ops/thy_ops.ML Fri Feb 16 17:24:51 1996 +0100 +++ b/src/HOLCF/ax_ops/thy_ops.ML Fri Feb 16 18:00:47 1996 +0100 @@ -8,21 +8,21 @@ For a short english description of the new sections write to regensbu@informatik.tu-muenchen.de. -TODO: vielleicht AST-Darstellung mit "op name" statt _I_... +TODO: maybe AST-representation with "op name" instead of _I_... *) signature THY_OPS = sig - (* continuous mixfixes (extension of datatype PrivateSyntax.Mixfix.mixfix) *) + (* continuous mixfixes (extension of datatype Mixfix.mixfix) *) datatype cmixfix = - Mixfix of PrivateSyntax.Mixfix.mixfix | + Mixfix of Mixfix.mixfix | CInfixl of int | CInfixr of int | CMixfix of string * int list *int; exception CINFIX of cmixfix; - val cmixfix_to_mixfix : cmixfix -> PrivateSyntax.Mixfix.mixfix; + val cmixfix_to_mixfix : cmixfix -> Mixfix.mixfix; (* theory extenders : *) val add_ops : {curried: bool, total: bool, strict: bool} -> @@ -54,7 +54,7 @@ (* the extended copy of mixfix *) datatype cmixfix = - Mixfix of PrivateSyntax.Mixfix.mixfix | + Mixfix of Mixfix.mixfix | CInfixl of int | CInfixr of int | CMixfix of string * int list *int; @@ -125,36 +125,36 @@ fun oldstyle ((name,typ,Mixfix(x))::tl) = (name,typ,x)::(oldstyle tl) | oldstyle ((name,typ,CInfixl(i))::tl) = - (mk_internal_name name,typ,PrivateSyntax.Mixfix.NoSyn):: + (mk_internal_name name,typ,Mixfix.NoSyn):: (oldstyle tl) | oldstyle ((name,typ,CInfixr(i))::tl) = - (mk_internal_name name,typ,PrivateSyntax.Mixfix.NoSyn):: + (mk_internal_name name,typ,Mixfix.NoSyn):: (oldstyle tl) | oldstyle ((name,typ,CMixfix(x))::tl) = - (name,typ,PrivateSyntax.Mixfix.NoSyn):: + (name,typ,Mixfix.NoSyn):: (oldstyle tl) | oldstyle [] = []; (* generating the external purely syntactical infix functions. Called by add_ext_axioms(_i) *) fun syn_decls curried sign ((name,typ,CInfixl(i))::tl) = - (name,op_to_fun curried sign typ,PrivateSyntax.Mixfix.Infixl(i)):: + (name,op_to_fun curried sign typ,Mixfix.Infixl(i)):: (syn_decls curried sign tl) | syn_decls curried sign ((name,typ,CInfixr(i))::tl) = - (name,op_to_fun curried sign typ,PrivateSyntax.Mixfix.Infixr(i)):: + (name,op_to_fun curried sign typ,Mixfix.Infixr(i)):: (syn_decls curried sign tl) | syn_decls curried sign ((name,typ,CMixfix(x))::tl) = (*#### - ("@"^name,op_to_fun curried sign typ,PrivateSyntax.Mixfix.Mixfix(x)):: + ("@"^name,op_to_fun curried sign typ,Mixfix.Mixfix(x)):: ####**) - (name,op_to_fun curried sign typ,PrivateSyntax.Mixfix.Mixfix(x)):: + (name,op_to_fun curried sign typ,Mixfix.Mixfix(x)):: (syn_decls curried sign tl) | syn_decls curried sign (_::tl) = syn_decls curried sign tl | syn_decls _ _ [] = []; (* generating the translation rules. Called by add_ext_axioms(_i) *) -local open PrivateSyntax.Ast in +local open Ast in fun xrules_of true ((name,typ,CInfixl(i))::tail) = ((mk_appl (Constant (mk_internal_name name)) [Variable "A",Variable "B"]) <-> (mk_appl (Constant "@fapp") [(mk_appl (Constant "@fapp") [ diff -r 09354d37a5ab -r ce37c64244c0 src/HOLCF/domain/theorems.ML --- a/src/HOLCF/domain/theorems.ML Fri Feb 16 17:24:51 1996 +0100 +++ b/src/HOLCF/domain/theorems.ML Fri Feb 16 18:00:47 1996 +0100 @@ -46,10 +46,10 @@ fun REPEAT_DETERM_UNTIL p tac = let fun drep st = if p st then Sequence.single st - else (case Sequence.pull(tapply(tac,st)) of + else (case Sequence.pull(tac st) of None => Sequence.null | Some(st',_) => drep st') -in Tactic drep end; +in drep end; val UNTIL_SOLVED = REPEAT_DETERM_UNTIL (has_fewer_prems 1); local val trueI2 = prove_goal HOL.thy "f~=x ==> True" (fn prems => [rtac TrueI 1]) in diff -r 09354d37a5ab -r ce37c64244c0 src/Provers/astar.ML --- a/src/Provers/astar.ML Fri Feb 16 17:24:51 1996 +0100 +++ b/src/Provers/astar.ML Fri Feb 16 18:00:47 1996 +0100 @@ -21,7 +21,7 @@ infix THEN_ASTAR; val trace_ASTAR = ref false; -fun (Tactic tf0) THEN_ASTAR (satp, costf, tac) = +fun tf0 THEN_ASTAR (satp, costf, tac) = let val tf = tracify trace_ASTAR tac; fun bfs (news,nprfs,level) = let fun cost thm = (level,costf level thm,thm) diff -r 09354d37a5ab -r ce37c64244c0 src/Provers/ind.ML --- a/src/Provers/ind.ML Fri Feb 16 17:24:51 1996 +0100 +++ b/src/Provers/ind.ML Fri Feb 16 18:00:47 1996 +0100 @@ -40,22 +40,23 @@ fun qnt_tac i = fn (tac,var) => tac THEN res_inst_tac [(a_name,var)] spec i; (*Generalizes over all free variables, with the named var outermost.*) -fun all_frees_tac (var:string) i = Tactic(fn thm => +fun all_frees_tac (var:string) i thm = let val tsig = #tsig(Sign.rep_sg(#sign(rep_thm thm))); val frees = add_term_frees tsig (nth_elem(i-1,prems_of thm),[var]); val frees' = sort(op>)(frees \ var) @ [var] - in tapply(foldl (qnt_tac i) (all_tac,frees'), thm) end); + in foldl (qnt_tac i) (all_tac,frees') thm end; fun REPEAT_SIMP_TAC simp_tac n i = -let fun repeat thm = tapply(COND (has_fewer_prems n) all_tac - let val k = length(prems_of thm) - in simp_tac i THEN COND (has_fewer_prems k) (Tactic repeat) all_tac - end, thm) -in Tactic repeat end; +let fun repeat thm = + (COND (has_fewer_prems n) all_tac + let val k = nprems_of thm + in simp_tac i THEN COND (has_fewer_prems k) repeat all_tac end) + thm +in repeat end; -fun ALL_IND_TAC sch simp_tac i = Tactic(fn thm => tapply( - resolve_tac [sch] i THEN - REPEAT_SIMP_TAC simp_tac (length(prems_of thm)) i, thm)); +fun ALL_IND_TAC sch simp_tac i thm = + (resolve_tac [sch] i THEN + REPEAT_SIMP_TAC simp_tac (nprems_of thm) i) thm; fun IND_TAC sch simp_tac var = all_frees_tac var THEN' ALL_IND_TAC sch simp_tac; diff -r 09354d37a5ab -r ce37c64244c0 src/Provers/simp.ML --- a/src/Provers/simp.ML Fri Feb 16 17:24:51 1996 +0100 +++ b/src/Provers/simp.ML Fri Feb 16 18:00:47 1996 +0100 @@ -129,7 +129,7 @@ in mk trans_thms end; (*Applies tactic and returns the first resulting state, FAILS if none!*) -fun one_result(tac,thm) = case Sequence.pull(tapply(tac,thm)) of +fun one_result(tac,thm) = case Sequence.pull(tac thm) of Some(thm',_) => thm' | None => raise THM("Simplifier: could not continue", 0, [thm]); @@ -205,7 +205,7 @@ resolve_tac congs 1 ORELSE refl1_tac | Free _ => resolve_tac congs 1 ORELSE refl1_tac | _ => refl1_tac)) - val Some(thm'',_) = Sequence.pull(tapply(add_norm_tac,thm')) + val Some(thm'',_) = Sequence.pull(add_norm_tac thm') in thm'' end; fun add_norm_tags congs = @@ -357,18 +357,18 @@ fun split_tac (cong_tac,splits,split_consts) i = let fun seq_try (split::splits,a::bs) thm = tapply( COND (splittable a i) (DETERM(resolve_tac[split]i)) - (Tactic(seq_try(splits,bs))), thm) - | seq_try([],_) thm = tapply(no_tac,thm) - and try_rew thm = tapply(Tactic(seq_try(splits,split_consts)) - ORELSE Tactic one_subt, thm) + ((seq_try(splits,bs))), thm) + | seq_try([],_) thm = no_tac thm + and try_rew thm = tapply((seq_try(splits,split_consts)) + ORELSE one_subt, thm) and one_subt thm = let val test = has_fewer_prems (nprems_of thm + 1) fun loop thm = tapply(COND test no_tac - ((Tactic try_rew THEN DEPTH_FIRST test (refl_tac i)) - ORELSE (refl_tac i THEN Tactic loop)), thm) - in tapply(cong_tac THEN Tactic loop, thm) end + ((try_rew THEN DEPTH_FIRST test (refl_tac i)) + ORELSE (refl_tac i THEN loop)), thm) + in (cong_tac THEN loop) thm end in if null splits then no_tac - else COND (may_match(split_consts,i)) (Tactic try_rew) no_tac + else COND (may_match(split_consts,i)) try_rew no_tac end; fun SPLIT_TAC (SS{cong_net,splits,split_consts,...}) i = @@ -443,7 +443,7 @@ fun simp_lhs(thm,ss,anet,ats,cs) = if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs) - else case Sequence.pull(tapply(cong_tac i,thm)) of + else case Sequence.pull(cong_tac i thm) of Some(thm',_) => let val ps = prems_of thm and ps' = prems_of thm'; val n = length(ps')-length(ps); @@ -481,7 +481,7 @@ else (ss,thm,anet,ats,cs); fun try_true(thm,ss,anet,ats,cs) = - case Sequence.pull(tapply(auto_tac i,thm)) of + case Sequence.pull(auto_tac i thm) of Some(thm',_) => (ss,thm',anet,ats,cs) | None => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs in if !tracing @@ -501,7 +501,7 @@ MK_EQ => (ss, res1(thm,[red2],i), anet, ats, cs) | ASMS(a) => add_asms(ss,thm,a,anet,ats,cs) | SIMP_LHS => simp_lhs(thm,ss,anet,ats,cs) - | REW => rew(tapply(net_tac net i,thm),thm,ss,anet,ats,cs,true) + | REW => rew(net_tac net i thm,thm,ss,anet,ats,cs,true) | REFL => (ss, res1(thm,refl_thms,i), anet, ats, cs) | TRUE => try_true(res1(thm,refl_thms,i),ss,anet,ats,cs) | PROVE => (if if_fl then MK_EQ::SIMP_LHS::SPLIT::TRUE::ss diff -r 09354d37a5ab -r ce37c64244c0 src/Provers/simplifier.ML --- a/src/Provers/simplifier.ML Fri Feb 16 17:24:51 1996 +0100 +++ b/src/Provers/simplifier.ML Fri Feb 16 18:00:47 1996 +0100 @@ -36,7 +36,7 @@ val Asm_full_simp_tac: int -> tactic end; -functor SimplifierFun():SIMPLIFIER = +structure Simplifier :SIMPLIFIER = struct datatype simpset = @@ -158,14 +158,11 @@ (fn n => if n<0 then all_tac else no_tac) in DEPTH_SOLVE(solve1_tac) end - fun simp_loop i thm = - tapply(asm_rewrite_goal_tac mode solve_all_tac mss i THEN - (finish_tac (prems_of_mss mss) i ORELSE looper i), - thm) + fun simp_loop_tac i thm = + (asm_rewrite_goal_tac mode solve_all_tac mss i THEN + (finish_tac (prems_of_mss mss) i ORELSE looper i)) thm and allsimp i n = EVERY(map (fn j => simp_loop_tac (i+j)) (n downto 0)) and looper i = TRY(NEWSUBGOALS (loop_tac i) (allsimp i)) - and simp_loop_tac i = Tactic(simp_loop i) - in simp_loop_tac end; val asm_full_simp_tac = gen_simp_tac (true,true); diff -r 09354d37a5ab -r ce37c64244c0 src/Pure/Thy/ROOT.ML --- a/src/Pure/Thy/ROOT.ML Fri Feb 16 17:24:51 1996 +0100 +++ b/src/Pure/Thy/ROOT.ML Fri Feb 16 18:00:47 1996 +0100 @@ -8,17 +8,10 @@ use "thy_scan.ML"; use "thy_parse.ML"; - -structure ThyScan = ThyScanFun(Scanner); -structure ThyParse = ThyParseFun(structure Symtab = Symtab - and ThyScan = ThyScan); - use "thy_syn.ML"; use "thm_database.ML"; use "../../Provers/simplifier.ML"; -structure Simplifier = SimplifierFun(); - use "thy_read.ML"; structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []); @@ -26,10 +19,6 @@ structure ReadThy = ReadthyFun(structure ThySyn = ThySyn and ThmDB = ThmDB); open ThmDB ReadThy; -(* hide functors; saves space in PolyML *) -functor ThyScanFun() = struct end; -functor ThyParseFun() = struct end; -functor SimplifierFun() = struct end; fun init_thy_reader () = use_string diff -r 09354d37a5ab -r ce37c64244c0 src/Pure/Thy/thm_database.ML --- a/src/Pure/Thy/thm_database.ML Fri Feb 16 17:24:51 1996 +0100 +++ b/src/Pure/Thy/thm_database.ML Fri Feb 16 18:00:47 1996 +0100 @@ -15,7 +15,7 @@ indexed by the constants they contain*) signature THMDB = -sig + sig val thm_db: thm_db_type ref val store_thm_db: string * thm -> thm val delete_thm_db: theory -> unit @@ -23,7 +23,7 @@ val findI: int -> (string * thm)list val findEs: int -> (string * thm)list val findE: int -> int -> (string * thm)list -end; + end; functor ThmDBFun(): THMDB = struct diff -r 09354d37a5ab -r ce37c64244c0 src/Pure/Thy/thy_parse.ML --- a/src/Pure/Thy/thy_parse.ML Fri Feb 16 17:24:51 1996 +0100 +++ b/src/Pure/Thy/thy_parse.ML Fri Feb 16 18:00:47 1996 +0100 @@ -10,7 +10,7 @@ infix 0 ||; signature THY_PARSE = -sig + sig type token val !! : ('a -> 'b * 'c) -> 'a -> 'b * 'c val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c @@ -66,9 +66,10 @@ val mk_pair: string * string -> string val mk_triple: string * string * string -> string val strip_quotes: string -> string -end; + end; -functor ThyParseFun(structure Symtab: SYMTAB and ThyScan: THY_SCAN): THY_PARSE= + +structure ThyParse : THY_PARSE= struct open ThyScan; @@ -517,5 +518,4 @@ axm_section "axclass" "|> AxClass.add_axclass" axclass_decl, section "instance" "" instance_decl]; - end; diff -r 09354d37a5ab -r ce37c64244c0 src/Pure/Thy/thy_scan.ML --- a/src/Pure/Thy/thy_scan.ML Fri Feb 16 17:24:51 1996 +0100 +++ b/src/Pure/Thy/thy_scan.ML Fri Feb 16 18:00:47 1996 +0100 @@ -6,17 +6,17 @@ *) signature THY_SCAN = -sig + sig datatype token_kind = Keyword | Ident | LongIdent | TypeVar | Nat | String | Verbatim | EOF val name_of_kind: token_kind -> string type lexicon val make_lexicon: string list -> lexicon val tokenize: lexicon -> string -> (token_kind * string * int) list -end; + end; -functor ThyScanFun(Scanner: SCANNER): THY_SCAN = +structure ThyScan : THY_SCAN = struct open Scanner; diff -r 09354d37a5ab -r ce37c64244c0 src/Pure/Thy/thy_syn.ML --- a/src/Pure/Thy/thy_syn.ML Fri Feb 16 17:24:51 1996 +0100 +++ b/src/Pure/Thy/thy_syn.ML Fri Feb 16 18:00:47 1996 +0100 @@ -6,26 +6,25 @@ *) signature THY_SYN_DATA = -sig + sig val user_keywords: string list val user_sections: (string * (ThyParse.token list -> (string * string) * ThyParse.token list)) list -end; + end; signature THY_SYN = -sig + sig val parse: string -> string -> string -end; + end; -functor ThySynFun(ThySynData: THY_SYN_DATA): THY_SYN = +functor ThySynFun (Data: THY_SYN_DATA): THY_SYN = struct -open ThyParse ThySynData; +val syntax = + ThyParse.make_syntax (ThyParse.pure_keywords @ Data.user_keywords) + (ThyParse.pure_sections @ Data.user_sections); -val syntax = - make_syntax (pure_keywords @ user_keywords) (pure_sections @ user_sections); - -val parse = parse_thy syntax; +val parse = ThyParse.parse_thy syntax; end; diff -r 09354d37a5ab -r ce37c64244c0 src/Tools/agrep --- a/src/Tools/agrep Fri Feb 16 17:24:51 1996 +0100 +++ b/src/Tools/agrep Fri Feb 16 18:00:47 1996 +0100 @@ -1,2 +1,2 @@ #! /bin/csh -grep "$*" {Pure/Syntax,Pure/Thy}/*ML */*ML */*/*ML +grep "$*" */*.ML */*/*.ML diff -r 09354d37a5ab -r ce37c64244c0 src/ZF/ROOT.ML --- a/src/ZF/ROOT.ML Fri Feb 16 17:24:51 1996 +0100 +++ b/src/ZF/ROOT.ML Fri Feb 16 18:00:47 1996 +0100 @@ -12,9 +12,8 @@ writeln banner; (*For Pure/tactic?? A crude way of adding structure to rules*) -fun CHECK_SOLVED (Tactic tf) = - Tactic (fn state => - case Sequence.pull (tf state) of +fun CHECK_SOLVED tac st = + case Sequence.pull (tac st) of None => error"DO_GOAL: tactic list failed" | Some(x,_) => if has_fewer_prems 1 x then @@ -22,7 +21,7 @@ else (writeln"DO_GOAL: unsolved goals!!"; writeln"Final proof state was ..."; print_goals (!goals_limit) x; - raise ERROR)); + raise ERROR); fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));