--- a/src/HOLCF/adm_tac.ML Thu Jul 14 19:28:23 2005 +0200
+++ b/src/HOLCF/adm_tac.ML Thu Jul 14 19:28:24 2005 +0200
@@ -80,9 +80,9 @@
(*figure out internal names*)
-val chfin_pcpoS = Sign.intern_sort (sign_of HOLCF.thy) ["chfin", "pcpo"];
-val cont_name = Sign.intern_const (sign_of HOLCF.thy) "cont";
-val adm_name = Sign.intern_const (sign_of HOLCF.thy) "adm";
+val chfin_pcpoS = Sign.intern_sort (the_context ()) ["chfin", "pcpo"];
+val cont_name = Sign.intern_const (the_context ()) "cont";
+val adm_name = Sign.intern_const (the_context ()) "adm";
(*** check whether type of terms in list is chain finite ***)
--- a/src/HOLCF/cont_consts.ML Thu Jul 14 19:28:23 2005 +0200
+++ b/src/HOLCF/cont_consts.ML Thu Jul 14 19:28:24 2005 +0200
@@ -80,7 +80,7 @@
fun gen_add_consts prep_typ raw_decls thy =
let
- val decls = map (upd_second (Thm.typ_of o prep_typ (Theory.sign_of thy))) raw_decls;
+ val decls = map (upd_second (Thm.typ_of o prep_typ thy)) raw_decls;
val (contconst_decls, normal_decls) = List.partition is_contconst decls;
val transformed_decls = map transform contconst_decls;
in
--- a/src/HOLCF/domain/axioms.ML Thu Jul 14 19:28:23 2005 +0200
+++ b/src/HOLCF/domain/axioms.ML Thu Jul 14 19:28:24 2005 +0200
@@ -35,7 +35,7 @@
Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons));
fun con_def outer recu m n (_,args) = let
- fun idxs z x arg = (if is_lazy arg then fn t => %%:upN`t else Id)
+ fun idxs z x arg = (if is_lazy arg then fn t => %%:upN`t else I)
(if recu andalso is_rec arg then (cproj (Bound z) eqs
(rec_of arg))`Bound(z-x) else Bound(z-x));
fun parms [] = %%:ONE_N
@@ -47,7 +47,7 @@
val copy_def = ("copy_def", %%:(dname^"_copy") == /\"f" (dc_abs oo
Library.foldl (op `) (%%:(dname^"_when") ,
- mapn (con_def Id true (length cons)) 0 cons)));
+ mapn (con_def I true (length cons)) 0 cons)));
(* -- definitions concerning the constructors, discriminators and selectors - *)
@@ -75,7 +75,7 @@
mk_cRep_CFun(%%:(dname^"_when"),map
(fn (con',args) => if con'<>con then UU else
foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
- in List.mapPartial Id (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end;
+ in List.mapPartial I (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end;
(* ----- axiom and definitions concerning induction ------------------------- *)
--- a/src/HOLCF/domain/library.ML Thu Jul 14 19:28:23 2005 +0200
+++ b/src/HOLCF/domain/library.ML Thu Jul 14 19:28:24 2005 +0200
@@ -8,8 +8,6 @@
(* ----- general support ---------------------------------------------------- *)
-fun Id x = x;
-
fun mapn f n [] = []
| mapn f n (x::xs) = (f n x) :: mapn f (n+1) xs;
@@ -17,7 +15,7 @@
| itr [a] = f2 a
| itr (a::l) = f(a, itr l)
in itr l end;
-fun foldr' f l = foldr'' f (l,Id);
+fun foldr' f l = foldr'' f (l,I);
fun map_cumulr f start xs = foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) =>
(y::ys,res2)) ([],start) xs;
@@ -175,9 +173,9 @@
infixr 0 ==>; fun S ==> T = mk_trp S ===> mk_trp T;
infix 0 ==; fun S == T = %%:"==" $ S $ T;
infix 1 ===; fun S === T = %%:"op =" $ S $ T;
-infix 1 ~=; fun S ~= T = mk_not (S === T);
+infix 1 ~=; fun S ~= T = HOLogic.mk_not (S === T);
infix 1 <<; fun S << T = %%:lessN $ S $ T;
-infix 1 ~<<; fun S ~<< T = mk_not (S << T);
+infix 1 ~<<; fun S ~<< T = HOLogic.mk_not (S << T);
infix 9 ` ; fun f` x = %%:Rep_CFunN $ f $ x;
infix 9 `% ; fun f`% s = f` %: s;
@@ -186,7 +184,7 @@
fun con_app2 con f args = mk_cRep_CFun(%%:con,map f args);
fun con_app con = con_app2 con %#;
fun if_rec arg f y = if is_rec arg then f (rec_of arg) else y;
-fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) Id (%# arg);
+fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) I (%# arg);
fun prj _ _ x ( _::[]) _ = x
| prj f1 _ x (_::y::ys) 0 = f1 x y
| prj f1 f2 x (y:: ys) j = prj f1 f2 (f2 x y) ys (j-1);
@@ -195,11 +193,11 @@
fun proj x = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;
fun cproj x = prj (fn S => K(%%:cfstN`S)) (fn S => K(%%:csndN`S)) x;
fun prj' _ _ x ( _::[]) _ = x
-| prj' f1 _ x (_:: ys) 0 = f1 x (foldr' mk_prodT ys)
+| prj' f1 _ x (_:: ys) 0 = f1 x (foldr' HOLogic.mk_prodT ys)
| prj' f1 f2 x (y:: ys) j = prj' f1 f2 (f2 x y) ys (j-1);
fun cproj' T eqs = prj'
- (fn S => fn t => Const(cfstN,mk_prodT(dummyT,t)->>dummyT)`S)
- (fn S => fn t => Const(csndN,mk_prodT(t,dummyT)->>dummyT)`S)
+ (fn S => fn t => Const(cfstN, HOLogic.mk_prodT(dummyT,t)->>dummyT)`S)
+ (fn S => fn t => Const(csndN, HOLogic.mk_prodT(t,dummyT)->>dummyT)`S)
T (map ((fn tp => tp ->> tp) o Type o fix_tp o fst) eqs);
fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
@@ -215,7 +213,7 @@
| mk_ctuple (t::ts) = cpair (t, mk_ctuple ts);
fun mk_ctupleT [] = HOLogic.unitT (* used in match_defs *)
| mk_ctupleT (T::[]) = T
-| mk_ctupleT (T::Ts) = mk_prodT(T, mk_ctupleT Ts);
+| mk_ctupleT (T::Ts) = HOLogic.mk_prodT(T, mk_ctupleT Ts);
fun lift_defined f = lift (fn x => defined (f x));
fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);
@@ -236,13 +234,13 @@
| one_fun n (_,args) = let
val l2 = length args;
fun idxs m arg = (if is_lazy arg then fn x=> %%:fupN` %%:ID_N`x
- else Id) (Bound(l2-m));
+ else I) (Bound(l2-m));
in cont_eta_contract (foldr''
(fn (a,t) => %%:ssplitN`(/\# (a,t)))
(args,
fn a=> /\#(a,(mk_cRep_CFun(funarg(l2,n),mapn idxs 1 args))))
) end;
in (if length cons = 1 andalso length(snd(hd cons)) <= 1
- then fn t => %%:strictifyN`t else Id)
+ then fn t => %%:strictifyN`t else I)
(foldr' (fn (x,y)=> %%:sscaseN`x`y) (mapn one_fun 1 cons)) end;
end; (* struct *)
--- a/src/HOLCF/domain/syntax.ML Thu Jul 14 19:28:23 2005 +0200
+++ b/src/HOLCF/domain/syntax.ML Thu Jul 14 19:28:24 2005 +0200
@@ -105,8 +105,8 @@
let
val dtypes = map (Type o fst) eqs';
val boolT = HOLogic.boolT;
- val funprod = foldr' mk_prodT (map (fn tp => tp ->> tp ) dtypes);
- val relprod = foldr' mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
+ val funprod = foldr' HOLogic.mk_prodT (map (fn tp => tp ->> tp ) dtypes);
+ val relprod = foldr' HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
val const_copy = (comp_dnam^"_copy" ,funprod ->> funprod, NoSyn);
val const_bisim = (comp_dnam^"_bisim" ,relprod --> boolT , NoSyn);
val ctt = map (calc_syntax funprod) eqs';
--- a/src/HOLCF/domain/theorems.ML Thu Jul 14 19:28:23 2005 +0200
+++ b/src/HOLCF/domain/theorems.ML Thu Jul 14 19:28:24 2005 +0200
@@ -6,6 +6,7 @@
Proof generator for domain section.
*)
+val HOLCF_ss = simpset();
structure Domain_Theorems = struct
@@ -233,7 +234,7 @@
(List.nth(vns,n))] else [])
@ [asm_simp_tac(HOLCF_ss addsimps when_rews)1])end) cons;
in List.concat(map (fn (c,args) =>
- List.concat(List.mapPartial Id (mapn (fn n => fn arg => Option.map (one_sel c n) (sel_of arg)) 0 args))) cons) end;
+ List.concat(List.mapPartial I (mapn (fn n => fn arg => Option.map (one_sel c n) (sel_of arg)) 0 args))) cons) end;
val sel_defins = if length cons=1 then List.mapPartial (fn arg => Option.map (fn sel => pg [](defined(%:x_name)==>
defined(%%:sel`%x_name)) [
rtac casedist 1,
@@ -442,7 +443,7 @@
fun all_rec_to ns = rec_to forall not all_rec_to ns;
fun warn (n,cons) = if all_rec_to [] false (n,cons) then (warning
("domain "^List.nth(dnames,n)^" is empty!"); true) else false;
- fun lazy_rec_to ns = rec_to exists Id lazy_rec_to ns;
+ fun lazy_rec_to ns = rec_to exists I lazy_rec_to ns;
in val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
val is_emptys = map warn n__eqs;
--- a/src/Pure/Isar/obtain.ML Thu Jul 14 19:28:23 2005 +0200
+++ b/src/Pure/Isar/obtain.ML Thu Jul 14 19:28:24 2005 +0200
@@ -118,11 +118,10 @@
|> Method.proof (SOME (Method.Basic (K Method.succeed))) |> Seq.hd
|> Proof.fix_i [([thesisN], NONE)]
|> Proof.assume_i [((thatN, [ContextRules.intro_query_local NONE]), [(that_prop, ([], []))])]
- |> (fn state' =>
- state'
- |> Proof.from_facts chain_facts
- |> Proof.show_i (K I) after_qed false [(("", []), [(bound_thesis, ([], []))])] false
- |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts state')))))
+ |> `Proof.the_facts
+ ||> Proof.from_facts chain_facts
+ ||> Proof.show_i (K I) after_qed false [(("", []), [(bound_thesis, ([], []))])] false
+ |-> (fn facts => Method.refine (Method.Basic (K (Method.insert facts))))
end;
val obtain = gen_obtain ProofContext.read_vars ProofContext.read_propp;
--- a/src/Pure/Isar/skip_proof.ML Thu Jul 14 19:28:23 2005 +0200
+++ b/src/Pure/Isar/skip_proof.ML Thu Jul 14 19:28:24 2005 +0200
@@ -41,13 +41,13 @@
(* basic cheating *)
fun make_thm thy t =
- Thm.invoke_oracle_i thy "Pure.skip_proof" (Theory.sign_of thy, SkipProof t);
+ Thm.invoke_oracle_i thy "Pure.skip_proof" (thy, SkipProof t);
fun cheat_tac thy st =
ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
fun prove thy xs asms prop tac =
- Tactic.prove (Theory.sign_of thy) xs asms prop
+ Tactic.prove thy xs asms prop
(if ! quick_and_dirty then (K (cheat_tac thy)) else tac);
--- a/src/Pure/ROOT.ML Thu Jul 14 19:28:23 2005 +0200
+++ b/src/Pure/ROOT.ML Thu Jul 14 19:28:24 2005 +0200
@@ -1,9 +1,7 @@
(* Title: Pure/ROOT.ML
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-Root file for Pure Isabelle.
+Pure Isabelle.
*)
val banner = "Pure Isabelle";
@@ -93,10 +91,8 @@
(*configuration for Proof General*)
use "proof_general.ML";
-(* loading the Tools directory *)
cd "Tools"; use "ROOT.ML"; cd "..";
-(*the Pure theories*)
use_thy "Pure"; structure Pure = struct val thy = theory "Pure" end;
use_thy "CPure"; structure CPure = struct val thy = theory "CPure" end;
--- a/src/Pure/Tools/ROOT.ML Thu Jul 14 19:28:23 2005 +0200
+++ b/src/Pure/Tools/ROOT.ML Thu Jul 14 19:28:24 2005 +0200
@@ -1,8 +1,11 @@
(* Title: Pure/Tools/ROOT.ML
ID: $Id$
+
+Miscellaneous tools and packages for Pure Isabelle.
*)
+(*Steven Obua's evaluator*)
use "am_interpreter.ML";
-use "am_compiler.ML";
+use "am_compiler.ML";
use "am_util.ML";
use "compute.ML";
--- a/src/Pure/Tools/am_compiler.ML Thu Jul 14 19:28:23 2005 +0200
+++ b/src/Pure/Tools/am_compiler.ML Thu Jul 14 19:28:24 2005 +0200
@@ -5,14 +5,14 @@
signature COMPILING_AM =
sig
- include ABSTRACT_MACHINE
+ include ABSTRACT_MACHINE
- datatype closure = CVar of int | CConst of int
- | CApp of closure * closure | CAbs of closure | Closure of (closure list) * closure
+ datatype closure = CVar of int | CConst of int
+ | CApp of closure * closure | CAbs of closure | Closure of (closure list) * closure
- val set_compiled_rewriter : (term -> closure) -> unit
- val list_nth : 'a list * int -> 'a
- val list_map : ('a -> 'b) -> 'a list -> 'b list
+ val set_compiled_rewriter : (term -> closure) -> unit
+ val list_nth : 'a list * int -> 'a
+ val list_map : ('a -> 'b) -> 'a list -> 'b list
end
structure AM_Compiler :> COMPILING_AM = struct
@@ -25,7 +25,8 @@
datatype pattern = PVar | PConst of int * (pattern list)
datatype closure = CVar of int | CConst of int
- | CApp of closure * closure | CAbs of closure | Closure of (closure list) * closure
+ | CApp of closure * closure | CAbs of closure
+ | Closure of (closure list) * closure
val compiled_rewriter = ref (NONE:(term -> closure)Option.option)
@@ -47,19 +48,22 @@
| term_of_clos (CConst c) = Const c
| term_of_clos (CApp (u, v)) = App (term_of_clos u, term_of_clos v)
| term_of_clos (CAbs u) = Abs (term_of_clos u)
- | term_of_clos (Closure (e, u)) = raise (Run "internal error: closure in normalized term found")
+ | term_of_clos (Closure (e, u)) =
+ raise (Run "internal error: closure in normalized term found")
fun strip_closure args (CApp (a,b)) = strip_closure (b::args) a
| strip_closure args x = (x, args)
-(* Returns true iff at most 0 .. (free-1) occur unbound. therefore check_freevars 0 t iff t is closed *)
+(*Returns true iff at most 0 .. (free-1) occur unbound. therefore
+ check_freevars 0 t iff t is closed*)
fun check_freevars free (Var x) = x < free
| check_freevars free (Const c) = true
| check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
| check_freevars free (Abs m) = check_freevars (free+1) m
fun count_patternvars PVar = 1
- | count_patternvars (PConst (_, ps)) = List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
+ | count_patternvars (PConst (_, ps)) =
+ List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
fun print_rule (p, t) =
let
@@ -81,17 +85,22 @@
end
val (n, pattern) = print_pattern 0 p
- val pattern = if List.exists Char.isSpace (String.explode pattern) then "("^pattern^")" else pattern
+ val pattern =
+ if List.exists Char.isSpace (String.explode pattern) then "("^pattern^")"
+ else pattern
- fun print_term d (Var x) = (*if x < d then "Var "^(str x) else "x"^(str (n-(x-d)-1))*) "Var "^(str x)
- | print_term d (Const c) = "c"^(str c)
- | print_term d (App (a,b)) = "App ("^(print_term d a)^", "^(print_term d b)^")"
- | print_term d (Abs c) = "Abs ("^(print_term (d+1) c)^")"
+ fun print_term d (Var x) = (*if x < d then "Var "^(str x) else "x"^(str (n-(x-d)-1))*)
+ "Var " ^ str x
+ | print_term d (Const c) = "c" ^ str c
+ | print_term d (App (a,b)) = "App (" ^ print_term d a ^ ", " ^ print_term d b ^ ")"
+ | print_term d (Abs c) = "Abs (" ^ print_term (d + 1) c ^ ")"
fun listvars n = if n = 0 then "x0" else "x"^(str n)^", "^(listvars (n-1))
val term = print_term 0 t
- val term = if n > 0 then "Closure (["^(listvars (n-1))^"], "^term^")" else "Closure ([], "^term^")"
+ val term =
+ if n > 0 then "Closure (["^(listvars (n-1))^"], "^term^")"
+ else "Closure ([], "^term^")"
in
"lookup stack "^pattern^" = weak stack ("^term^")"
@@ -104,7 +113,7 @@
| remove_dups [] = []
fun constants_of PVar = []
- | constants_of (PConst (c, ps)) = c::(List.concat (map constants_of ps))
+ | constants_of (PConst (c, ps)) = c :: List.concat (map constants_of ps)
fun constants_of_term (Var _) = []
| constants_of_term (Abs m) = constants_of_term m
@@ -113,6 +122,7 @@
fun load_rules sname name prog =
let
+ (* FIXME consider using more readable/efficient Buffer.empty |> fold Buffer.add etc. *)
val buffer = ref ""
fun write s = (buffer := (!buffer)^s)
fun writeln s = (write s; write "\n")
@@ -210,11 +220,9 @@
in
()
end
-
- val dummy = (fn s => ())
in
compiled_rewriter := NONE;
- use_text (dummy, dummy) false (!buffer);
+ use_text (K (), K ()) false (!buffer);
case !compiled_rewriter of
NONE => raise (Compile "cannot communicate with compiled function")
| SOME r => (compiled_rewriter := NONE; fn t => term_of_clos (r t))
--- a/src/Pure/Tools/am_interpreter.ML Thu Jul 14 19:28:23 2005 +0200
+++ b/src/Pure/Tools/am_interpreter.ML Thu Jul 14 19:28:24 2005 +0200
@@ -3,7 +3,9 @@
Author: Steven Obua
*)
-signature ABSTRACT_MACHINE = sig
+signature ABSTRACT_MACHINE =
+sig
+
datatype term = Var of int | Const of int | App of term * term | Abs of term
datatype pattern = PVar | PConst of int * (pattern list)
@@ -12,7 +14,7 @@
exception Compile of string;
val compile : (pattern * term) list -> program
-
+
exception Run of string;
val run : program -> term -> term
@@ -25,8 +27,8 @@
datatype pattern = PVar | PConst of int * (pattern list)
datatype closure = CVar of int | CConst of int
- | CApp of closure * closure | CAbs of closure
- | Closure of (closure list) * closure
+ | CApp of closure * closure | CAbs of closure
+ | Closure of (closure list) * closure
structure prog_struct = TableFun(type key = int*int val ord = prod_ord int_ord int_ord);
@@ -57,22 +59,22 @@
(* earlier occurrence of PVar corresponds to higher de Bruijn index *)
fun pattern_match args PVar clos = SOME (clos::args)
- | pattern_match args (PConst (c, patterns)) clos =
+ | pattern_match args (PConst (c, patterns)) clos =
let
- val (f, closargs) = strip_closure [] clos
+ val (f, closargs) = strip_closure [] clos
in
- case f of
- CConst d =>
- if c = d then
- pattern_match_list args patterns closargs
- else
- NONE
- | _ => NONE
+ case f of
+ CConst d =>
+ if c = d then
+ pattern_match_list args patterns closargs
+ else
+ NONE
+ | _ => NONE
end
and pattern_match_list args [] [] = SOME args
- | pattern_match_list args (p::ps) (c::cs) =
+ | pattern_match_list args (p::ps) (c::cs) =
(case pattern_match args p c of
- NONE => NONE
+ NONE => NONE
| SOME args => pattern_match_list args ps cs)
| pattern_match_list _ _ _ = NONE
@@ -88,26 +90,26 @@
fun pattern_key (PConst (c, ps)) = (c, length ps)
| pattern_key _ = raise (Compile "pattern reduces to variable")
-fun compile eqs =
+fun compile eqs =
let
- val eqs = map (fn (p, r) => (check_freevars (count_patternvars p) r;
- (pattern_key p, (p, clos_of_term r)))) eqs
+ val eqs = map (fn (p, r) => (check_freevars (count_patternvars p) r;
+ (pattern_key p, (p, clos_of_term r)))) eqs
in
- prog_struct.make (map (fn (k, a) => (k, [a])) eqs)
- end
+ prog_struct.make (map (fn (k, a) => (k, [a])) eqs)
+ end
fun match_rules n [] clos = NONE
| match_rules n ((p,eq)::rs) clos =
case pattern_match [] p clos of
- NONE => match_rules (n+1) rs clos
+ NONE => match_rules (n+1) rs clos
| SOME args => SOME (Closure (args, eq))
-fun match_closure prog clos =
+fun match_closure prog clos =
case len_head_of_closure 0 clos of
- (len, CConst c) =>
- (case prog_struct.lookup (prog, (c, len)) of
- NONE => NONE
- | SOME rules => match_rules 0 rules clos)
+ (len, CConst c) =>
+ (case prog_struct.lookup (prog, (c, len)) of
+ NONE => NONE
+ | SOME rules => match_rules 0 rules clos)
| _ => NONE
fun lift n (c as (CConst _)) = c
@@ -121,21 +123,21 @@
| weak prog (SAppL (b, stack)) (Closure (e, CAbs m)) = weak prog stack (Closure (b::e, m))
| weak prog stack (Closure (e, CVar n)) = weak prog stack (List.nth (e, n) handle Subscript => (CVar (n-(length e))))
| weak prog stack (Closure (e, c as CConst _)) = weak prog stack c
- | weak prog stack clos =
+ | weak prog stack clos =
case match_closure prog clos of
- NONE => weak_last prog stack clos
+ NONE => weak_last prog stack clos
| SOME r => weak prog stack r
and weak_last prog (SAppR (a, stack)) b = weak prog stack (CApp (a,b))
| weak_last prog (s as (SAppL (b, stack))) a = weak prog (SAppR (a, stack)) b
- | weak_last prog stack c = (stack, c)
+ | weak_last prog stack c = (stack, c)
-fun strong prog stack (Closure (e, CAbs m)) =
+fun strong prog stack (Closure (e, CAbs m)) =
let
- val (stack', wnf) = weak prog SEmpty (Closure ((CVar 0)::(lift_env 0 e), m))
+ val (stack', wnf) = weak prog SEmpty (Closure ((CVar 0)::(lift_env 0 e), m))
in
- case stack' of
- SEmpty => strong prog (SAbs stack) wnf
- | _ => raise (Run "internal error in strong: weak failed")
+ case stack' of
+ SEmpty => strong prog (SAbs stack) wnf
+ | _ => raise (Run "internal error in strong: weak failed")
end
| strong prog stack (clos as (CApp (u, v))) = strong prog (SAppL (v, stack)) u
| strong prog stack clos = strong_last prog stack clos
@@ -144,17 +146,17 @@
| strong_last prog (SAppR (a, stack)) b = strong_last prog stack (CApp (a, b))
| strong_last prog stack clos = (stack, clos)
-fun run prog t =
+fun run prog t =
let
- val (stack, wnf) = weak prog SEmpty (Closure ([], clos_of_term t))
+ val (stack, wnf) = weak prog SEmpty (Closure ([], clos_of_term t))
in
- case stack of
- SEmpty => (case strong prog SEmpty wnf of
- (SEmpty, snf) => term_of_clos snf
- | _ => raise (Run "internal error in run: strong failed"))
- | _ => raise (Run "internal error in run: weak failed")
+ case stack of
+ SEmpty => (case strong prog SEmpty wnf of
+ (SEmpty, snf) => term_of_clos snf
+ | _ => raise (Run "internal error in run: strong failed"))
+ | _ => raise (Run "internal error in run: weak failed")
end
-
+
end
structure AbstractMachine = AM_Interpreter
--- a/src/Pure/Tools/am_util.ML Thu Jul 14 19:28:23 2005 +0200
+++ b/src/Pure/Tools/am_util.ML Thu Jul 14 19:28:24 2005 +0200
@@ -4,11 +4,11 @@
*)
signature AM_UTIL = sig
-
+
type naming = string -> int
exception Parse of string
- exception Tokenize
+ exception Tokenize
(* takes a naming for the constants *)
val read_rule : naming -> string -> AbstractMachine.pattern * AbstractMachine.term
@@ -25,7 +25,8 @@
fun term_ord (AbstractMachine.Var x, AbstractMachine.Var y) = int_ord (x,y)
| term_ord (AbstractMachine.Const c1, AbstractMachine.Const c2) = int_ord (c1, c2)
- | term_ord (AbstractMachine.App a1, AbstractMachine.App a2) = (prod_ord term_ord term_ord) (a1, a2)
+ | term_ord (AbstractMachine.App a1, AbstractMachine.App a2) =
+ prod_ord term_ord term_ord (a1, a2)
| term_ord (AbstractMachine.Abs m1, AbstractMachine.Abs m2) = term_ord (m1, m2)
| term_ord (AbstractMachine.Const _, _) = LESS
| term_ord (AbstractMachine.Var _, AbstractMachine.Const _ ) = GREATER
@@ -36,68 +37,72 @@
type naming = string -> int
-datatype token = TokenConst of string | TokenLeft | TokenRight | TokenVar of string | TokenLambda | TokenDot | TokenNone | TokenEq
+datatype token =
+ TokenConst of string | TokenLeft | TokenRight | TokenVar of string |
+ TokenLambda | TokenDot | TokenNone | TokenEq
exception Tokenize;
fun tokenize s =
let
- val s = String.explode s
- fun str c = Char.toString c
- fun app s c = s^(str c)
- fun tz TokenNone [] = []
- | tz x [] = [x]
- | tz TokenNone (c::cs) =
- if Char.isSpace c then tz TokenNone cs
- else if Char.isLower c then (tz (TokenVar (str c)) cs)
- else if Char.isAlphaNum c then (tz (TokenConst (str c)) cs)
- else if c = #"%" then (TokenLambda :: (tz TokenNone cs))
- else if c = #"." then (TokenDot :: (tz TokenNone cs))
- else if c = #"(" then (TokenLeft :: (tz TokenNone cs))
- else if c = #")" then (TokenRight :: (tz TokenNone cs))
- else if c = #"=" then (TokenEq :: (tz TokenNone cs))
- else raise Tokenize
- | tz (TokenConst s) (c::cs) =
- if Char.isAlphaNum c then (tz (TokenConst (app s c)) cs)
- else (TokenConst s)::(tz TokenNone (c::cs))
- | tz (TokenVar s) (c::cs) =
- if Char.isAlphaNum c then (tz (TokenVar (app s c)) cs)
- else (TokenVar s)::(tz TokenNone (c::cs))
- | tz _ _ = raise Tokenize
+ val s = String.explode s
+ fun str c = Char.toString c
+ fun app s c = s^(str c)
+ fun tz TokenNone [] = []
+ | tz x [] = [x]
+ | tz TokenNone (c::cs) =
+ if Char.isSpace c then tz TokenNone cs
+ else if Char.isLower c then (tz (TokenVar (str c)) cs)
+ else if Char.isAlphaNum c then (tz (TokenConst (str c)) cs)
+ else if c = #"%" then (TokenLambda :: (tz TokenNone cs))
+ else if c = #"." then (TokenDot :: (tz TokenNone cs))
+ else if c = #"(" then (TokenLeft :: (tz TokenNone cs))
+ else if c = #")" then (TokenRight :: (tz TokenNone cs))
+ else if c = #"=" then (TokenEq :: (tz TokenNone cs))
+ else raise Tokenize
+ | tz (TokenConst s) (c::cs) =
+ if Char.isAlphaNum c then (tz (TokenConst (app s c)) cs)
+ else (TokenConst s)::(tz TokenNone (c::cs))
+ | tz (TokenVar s) (c::cs) =
+ if Char.isAlphaNum c then (tz (TokenVar (app s c)) cs)
+ else (TokenVar s)::(tz TokenNone (c::cs))
+ | tz _ _ = raise Tokenize
in
- tz TokenNone s
+ tz TokenNone s
end
exception Parse of string;
-fun cons x xs = if List.exists (fn y => x = y) xs then raise (Parse ("variable occurs twice: "^x)) else (x::xs)
+fun cons x xs =
+ if List.exists (fn y => x = y) xs then raise (Parse ("variable occurs twice: "^x))
+ else (x::xs)
-fun parse_pattern f pvars ((TokenConst c)::ts) =
+fun parse_pattern f pvars ((TokenConst c)::ts) =
let
- val (pvars, ts, plist) = parse_pattern_list f pvars ts
+ val (pvars, ts, plist) = parse_pattern_list f pvars ts
in
- (pvars, ts, AbstractMachine.PConst (f c, plist))
+ (pvars, ts, AbstractMachine.PConst (f c, plist))
end
| parse_pattern _ _ _ = raise (Parse "parse_pattern: constant expected")
-and parse_pattern_single f pvars ((TokenVar x)::ts) = (cons x pvars, ts, AbstractMachine.PVar)
+and parse_pattern_single f pvars ((TokenVar x)::ts) = (cons x pvars, ts, AbstractMachine.PVar)
| parse_pattern_single f pvars ((TokenConst c)::ts) = (pvars, ts, AbstractMachine.PConst (f c, []))
- | parse_pattern_single f pvars (TokenLeft::ts) =
+ | parse_pattern_single f pvars (TokenLeft::ts) =
let
- val (pvars, ts, p) = parse_pattern f pvars ts
+ val (pvars, ts, p) = parse_pattern f pvars ts
in
- case ts of
- TokenRight::ts => (pvars, ts, p)
- | _ => raise (Parse "parse_pattern_single: closing bracket expected")
+ case ts of
+ TokenRight::ts => (pvars, ts, p)
+ | _ => raise (Parse "parse_pattern_single: closing bracket expected")
end
| parse_pattern_single _ _ _ = raise (Parse "parse_pattern_single: got stuck")
and parse_pattern_list f pvars (TokenEq::ts) = (pvars, TokenEq::ts, [])
| parse_pattern_list f pvars (TokenRight::ts) = (pvars, TokenRight::ts, [])
- | parse_pattern_list f pvars ts =
+ | parse_pattern_list f pvars ts =
let
- val (pvars, ts, p) = parse_pattern_single f pvars ts
- val (pvars, ts, ps) = parse_pattern_list f pvars ts
+ val (pvars, ts, p) = parse_pattern_single f pvars ts
+ val (pvars, ts, ps) = parse_pattern_list f pvars ts
in
- (pvars, ts, p::ps)
+ (pvars, ts, p::ps)
end
fun app_terms x (t::ts) = app_terms (AbstractMachine.App (x, t)) ts
@@ -105,66 +110,66 @@
fun parse_term_single f vars ((TokenConst c)::ts) = (ts, AbstractMachine.Const (f c))
| parse_term_single f vars ((TokenVar v)::ts) = (ts, AbstractMachine.Var (vars v))
- | parse_term_single f vars (TokenLeft::ts) =
+ | parse_term_single f vars (TokenLeft::ts) =
let
- val (ts, term) = parse_term f vars ts
+ val (ts, term) = parse_term f vars ts
in
- case ts of
- TokenRight::ts => (ts, term)
- | _ => raise Parse ("parse_term_single: closing bracket expected")
+ case ts of
+ TokenRight::ts => (ts, term)
+ | _ => raise Parse ("parse_term_single: closing bracket expected")
end
- | parse_term_single f vars (TokenLambda::(TokenVar x)::TokenDot::ts) =
+ | parse_term_single f vars (TokenLambda::(TokenVar x)::TokenDot::ts) =
let
- val (ts, term) = parse_term f (fn s => if s=x then 0 else (vars s)+1) ts
+ val (ts, term) = parse_term f (fn s => if s=x then 0 else (vars s)+1) ts
in
- (ts, AbstractMachine.Abs term)
+ (ts, AbstractMachine.Abs term)
end
| parse_term_single _ _ _ = raise Parse ("parse_term_single: got stuck")
and parse_term_list f vars [] = ([], [])
| parse_term_list f vars (TokenRight::ts) = (TokenRight::ts, [])
- | parse_term_list f vars ts =
+ | parse_term_list f vars ts =
let
- val (ts, term) = parse_term_single f vars ts
- val (ts, terms) = parse_term_list f vars ts
+ val (ts, term) = parse_term_single f vars ts
+ val (ts, terms) = parse_term_list f vars ts
in
- (ts, term::terms)
+ (ts, term::terms)
end
-and parse_term f vars ts =
+and parse_term f vars ts =
let
- val (ts, terms) = parse_term_list f vars ts
+ val (ts, terms) = parse_term_list f vars ts
in
- case terms of
- [] => raise (Parse "parse_term: no term found")
- | (t::terms) => (ts, app_terms t terms)
+ case terms of
+ [] => raise (Parse "parse_term: no term found")
+ | (t::terms) => (ts, app_terms t terms)
end
-fun read_rule f s =
+fun read_rule f s =
let
- val t = tokenize s
- val (v, ts, pattern) = parse_pattern f [] t
- fun vars [] (x:string) = raise (Parse "read_rule.vars: variable not found")
- | vars (v::vs) x = if v = x then 0 else (vars vs x)+1
+ val t = tokenize s
+ val (v, ts, pattern) = parse_pattern f [] t
+ fun vars [] (x:string) = raise (Parse "read_rule.vars: variable not found")
+ | vars (v::vs) x = if v = x then 0 else (vars vs x)+1
in
- case ts of
- TokenEq::ts =>
- let
- val (ts, term) = parse_term f (vars v) ts
- in
- case ts of
- [] => (pattern, term)
- | _ => raise (Parse "read_rule: still tokens left, end expected")
- end
- | _ => raise (Parse ("read_rule: = expected"))
+ case ts of
+ TokenEq::ts =>
+ let
+ val (ts, term) = parse_term f (vars v) ts
+ in
+ case ts of
+ [] => (pattern, term)
+ | _ => raise (Parse "read_rule: still tokens left, end expected")
+ end
+ | _ => raise (Parse ("read_rule: = expected"))
end
-fun read_term f g s =
+fun read_term f g s =
let
- val t = tokenize s
- val (ts, term) = parse_term f g t
+ val t = tokenize s
+ val (ts, term) = parse_term f g t
in
- case ts of
- [] => term
- | _ => raise (Parse ("read_term: still tokens left, end expected"))
+ case ts of
+ [] => term
+ | _ => raise (Parse ("read_term: still tokens left, end expected"))
end
end
--- a/src/Pure/library.ML Thu Jul 14 19:28:23 2005 +0200
+++ b/src/Pure/library.ML Thu Jul 14 19:28:24 2005 +0200
@@ -8,19 +8,20 @@
tables, balanced trees, orders, current directory, misc.
*)
-infix |> |-> ||> ||>> |>> |>>> #> #-> ~~ \ \\ ins ins_string ins_int orf andf prefix upto downto
- mem mem_int mem_string union union_int union_string inter inter_int
- inter_string subset subset_int subset_string;
+infix |> |-> ||> ||>> |>> |>>> #> #-> ~~ \ \\ ins ins_string ins_int
+ orf andf prefix upto downto mem mem_int mem_string union union_int
+ union_string inter inter_int inter_string subset subset_int
+ subset_string;
infix 3 oo ooo oooo;
signature BASIC_LIBRARY =
sig
(*functions*)
+ val I: 'a -> 'a
+ val K: 'a -> 'b -> 'a
val curry: ('a * 'b -> 'c) -> 'a -> 'b -> 'c
val uncurry: ('a -> 'b -> 'c) -> 'a * 'b -> 'c
- val I: 'a -> 'a
- val K: 'a -> 'b -> 'a
val |> : 'a * ('a -> 'b) -> 'b
val |-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b
val ||> : ('c * 'a) * ('a -> 'b) -> 'c * 'b
@@ -33,9 +34,9 @@
val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
+ val funpow: int -> ('a -> 'a) -> 'a -> 'a
val apl: 'a * ('a * 'b -> 'c) -> 'b -> 'c
val apr: ('a * 'b -> 'c) * 'b -> 'a -> 'c
- val funpow: int -> ('a -> 'a) -> 'a -> 'a
(*old options -- invalidated*)
datatype invalid = None of invalid
@@ -295,11 +296,10 @@
(** functions **)
-(*handy combinators*)
+fun I x = x;
+fun K x = fn _ => x;
fun curry f x y = f (x, y);
fun uncurry f (x, y) = f x y;
-fun I x = x;
-fun K x = fn _ => x;
(*reverse application and structured results*)
fun x |> f = f x;
@@ -308,25 +308,28 @@
fun (x, y) ||> f = (x, f y);
fun (x, y) |>>> f = let val (x', z) = f x in (x', (y, z)) end;
fun (x, y) ||>> f = let val (z, y') = f y in ((x, z), y') end;
+
+(*reverse composition*)
fun f #> g = g o f;
-fun f #-> g = fn s => let val (v, s') = f s in g v s' end;
-fun ` h = fn s => (h s, s)
+fun f #-> g = uncurry g o f;
+
+(*view results*)
+fun `f = fn x => (f x, x);
(*composition with multiple args*)
fun (f oo g) x y = f (g x y);
fun (f ooo g) x y z = f (g x y z);
fun (f oooo g) x y z w = f (g x y z w);
-(*application of (infix) operator to its left or right argument*)
-fun apl (x, f) y = f (x, y);
-fun apr (f, y) x = f (x, y);
-
(*function exponentiation: f(...(f x)...) with n applications of f*)
fun funpow n f x =
let fun rep (0, x) = x
| rep (n, x) = rep (n - 1, f x)
in rep (n, x) end;
+(*application of (infix) operator to its left or right argument*)
+fun apl (x, f) y = f (x, y);
+fun apr (f, y) x = f (x, y);
(** options **)
@@ -1268,12 +1271,13 @@
Preserves order of elements in both lists.*)
val partition = List.partition;
-
fun partition_eq (eq:'a * 'a -> bool) =
- let fun part [] = []
- | part (x::ys) = let val (xs, xs') = partition (apl(x, eq)) ys
- in (x::xs)::(part xs') end
- in part end;
+ let
+ fun part [] = []
+ | part (x :: ys) =
+ let val (xs, xs') = partition (fn y => eq (x, y)) ys
+ in (x::xs)::(part xs') end
+ in part end;
(*Partition a list into buckets [ bi, b(i+1), ..., bj ]
--- a/src/Pure/meta_simplifier.ML Thu Jul 14 19:28:23 2005 +0200
+++ b/src/Pure/meta_simplifier.ML Thu Jul 14 19:28:24 2005 +0200
@@ -419,7 +419,7 @@
andalso not(exists_subterm is_Var lhs)
orelse
*)
- exists (apl (lhs, Logic.occs)) (rhs :: prems)
+ exists (fn t => Logic.occs (lhs, t)) (rhs :: prems)
orelse
null prems andalso Pattern.matches (Sign.tsig_of thy) (lhs, rhs)
(*the condition "null prems" is necessary because conditional rewrites
--- a/src/Pure/net.ML Thu Jul 14 19:28:23 2005 +0200
+++ b/src/Pure/net.ML Thu Jul 14 19:28:24 2005 +0200
@@ -222,10 +222,10 @@
| subtr (Leaf _) (net as Net _) = subtr emptynet net
| subtr (Net {comb = comb1, var = var1, atoms = atoms1})
(Net {comb = comb2, var = var2, atoms = atoms2}) =
- Symtab.fold (fn (a, net) =>
- subtr (if_none (Symtab.lookup (atoms1, a)) emptynet) net) atoms2 o
- subtr var1 var2 o
- subtr comb1 comb2;
+ subtr comb1 comb2
+ #> subtr var1 var2
+ #> Symtab.fold (fn (a, net) =>
+ subtr (if_none (Symtab.lookup (atoms1, a)) emptynet) net) atoms2
in subtr net1 net2 [] end;
fun entries net = subtract (K false) empty net;