--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Jun 19 17:23:21 2009 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Jun 19 17:26:40 2009 +0200
@@ -318,7 +318,7 @@
val dummy_case_term = IVar dummy_name;
(*assumption: dummy values are not relevant for serialization*)
val unitt = IConst (unit', (([], []), []));
- fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t)
+ fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
| dest_abs (t, ty) =
let
val vs = Code_Thingol.fold_varnames cons t [];
@@ -337,7 +337,7 @@
then tr_bind' [(x1, ty1), (x2, ty2)]
else force t
| _ => force t;
- in (dummy_name, dummy_type) `|-> ICase (((IVar dummy_name, dummy_type),
+ in (dummy_name, dummy_type) `|=> ICase (((IVar dummy_name, dummy_type),
[(unitt, tr_bind' ts)]), dummy_case_term) end
and imp_monad_bind' bind' return' unit' (const as (c, (_, tys))) ts = if c = bind' then case (ts, tys)
of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)]
@@ -349,7 +349,7 @@
| imp_monad_bind bind' return' unit' (t as _ `$ _) = (case unfold_app t
of (IConst const, ts) => imp_monad_bind' bind' return' unit' const ts
| (t, ts) => imp_monad_bind bind' return' unit' t `$$ map (imp_monad_bind bind' return' unit') ts)
- | imp_monad_bind bind' return' unit' (v_ty `|-> t) = v_ty `|-> imp_monad_bind bind' return' unit' t
+ | imp_monad_bind bind' return' unit' (v_ty `|=> t) = v_ty `|=> imp_monad_bind bind' return' unit' t
| imp_monad_bind bind' return' unit' (ICase (((t, ty), pats), t0)) = ICase
(((imp_monad_bind bind' return' unit' t, ty), (map o pairself) (imp_monad_bind bind' return' unit') pats), imp_monad_bind bind' return' unit' t0);
--- a/src/Tools/code/code_haskell.ML Fri Jun 19 17:23:21 2009 +0200
+++ b/src/Tools/code/code_haskell.ML Fri Jun 19 17:26:40 2009 +0200
@@ -70,7 +70,7 @@
])
| pr_term tyvars thm vars fxy (IVar v) =
(str o Code_Printer.lookup_var vars) v
- | pr_term tyvars thm vars fxy (t as _ `|-> _) =
+ | pr_term tyvars thm vars fxy (t as _ `|=> _) =
let
val (binds, t') = Code_Thingol.unfold_abs t;
fun pr ((v, pat), ty) = pr_bind tyvars thm BR ((SOME v, pat), ty);
@@ -240,7 +240,7 @@
end
| pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
let
- val split_abs_pure = (fn (v, _) `|-> t => SOME (v, t) | _ => NONE);
+ val split_abs_pure = (fn (v, _) `|=> t => SOME (v, t) | _ => NONE);
val unfold_abs_pure = Code_Thingol.unfoldr split_abs_pure;
val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam
--- a/src/Tools/code/code_ml.ML Fri Jun 19 17:23:21 2009 +0200
+++ b/src/Tools/code/code_ml.ML Fri Jun 19 17:26:40 2009 +0200
@@ -92,7 +92,7 @@
of SOME c_ts => pr_app is_closure thm vars fxy c_ts
| NONE => brackify fxy
[pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2])
- | pr_term is_closure thm vars fxy (t as _ `|-> _) =
+ | pr_term is_closure thm vars fxy (t as _ `|=> _) =
let
val (binds, t') = Code_Thingol.unfold_abs t;
fun pr ((v, pat), ty) =
@@ -401,7 +401,7 @@
of SOME c_ts => pr_app is_closure thm vars fxy c_ts
| NONE =>
brackify fxy [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2])
- | pr_term is_closure thm vars fxy (t as _ `|-> _) =
+ | pr_term is_closure thm vars fxy (t as _ `|=> _) =
let
val (binds, t') = Code_Thingol.unfold_abs t;
fun pr ((v, pat), ty) = pr_bind is_closure thm BR ((SOME v, pat), ty);
--- a/src/Tools/code/code_thingol.ML Fri Jun 19 17:23:21 2009 +0200
+++ b/src/Tools/code/code_thingol.ML Fri Jun 19 17:26:40 2009 +0200
@@ -8,8 +8,8 @@
infix 8 `%%;
infix 4 `$;
infix 4 `$$;
-infixr 3 `|->;
-infixr 3 `|-->;
+infixr 3 `|=>;
+infixr 3 `|==>;
signature BASIC_CODE_THINGOL =
sig
@@ -25,11 +25,11 @@
IConst of const
| IVar of vname
| `$ of iterm * iterm
- | `|-> of (vname * itype) * iterm
+ | `|=> of (vname * itype) * iterm
| ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
(*((term, type), [(selector pattern, body term )]), primitive term)*)
val `$$ : iterm * iterm list -> iterm;
- val `|--> : (vname * itype) list * iterm -> iterm;
+ val `|==> : (vname * itype) list * iterm -> iterm;
type typscheme = (vname * sort) list * itype;
end;
@@ -128,21 +128,21 @@
IConst of const
| IVar of vname
| `$ of iterm * iterm
- | `|-> of (vname * itype) * iterm
+ | `|=> of (vname * itype) * iterm
| ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
(*see also signature*)
val op `$$ = Library.foldl (op `$);
-val op `|--> = Library.foldr (op `|->);
+val op `|==> = Library.foldr (op `|=>);
val unfold_app = unfoldl
(fn op `$ t => SOME t
| _ => NONE);
val split_abs =
- (fn (v, ty) `|-> (t as ICase (((IVar w, _), [(p, t')]), _)) =>
+ (fn (v, ty) `|=> (t as ICase (((IVar w, _), [(p, t')]), _)) =>
if v = w then SOME (((v, SOME p), ty), t') else SOME (((v, NONE), ty), t)
- | (v, ty) `|-> t => SOME (((v, NONE), ty), t)
+ | (v, ty) `|=> t => SOME (((v, NONE), ty), t)
| _ => NONE);
val unfold_abs = unfoldr split_abs;
@@ -161,7 +161,7 @@
fun fold_aiterms f (t as IConst _) = f t
| fold_aiterms f (t as IVar _) = f t
| fold_aiterms f (t1 `$ t2) = fold_aiterms f t1 #> fold_aiterms f t2
- | fold_aiterms f (t as _ `|-> t') = f t #> fold_aiterms f t'
+ | fold_aiterms f (t as _ `|=> t') = f t #> fold_aiterms f t'
| fold_aiterms f (ICase (_, t)) = fold_aiterms f t;
fun fold_constnames f =
@@ -173,7 +173,7 @@
fun fold_varnames f =
let
fun add (IVar v) = f v
- | add ((v, _) `|-> _) = f v
+ | add ((v, _) `|=> _) = f v
| add _ = I;
in fold_aiterms add end;
@@ -182,7 +182,7 @@
fun add _ (IConst _) = I
| add vs (IVar v) = if not (member (op =) vs v) then f v else I
| add vs (t1 `$ t2) = add vs t1 #> add vs t2
- | add vs ((v, _) `|-> t) = add (insert (op =) v vs) t
+ | add vs ((v, _) `|=> t) = add (insert (op =) v vs) t
| add vs (ICase (_, t)) = add vs t;
in add [] end;
@@ -204,7 +204,7 @@
val l = k - j;
val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
val vs_tys = Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys);
- in vs_tys `|--> IConst c `$$ ts @ map (fn (v, _) => IVar v) vs_tys end;
+ in vs_tys `|==> IConst c `$$ ts @ map (fn (v, _) => IVar v) vs_tys end;
fun contains_dictvar t =
let
@@ -218,7 +218,7 @@
fun locally_monomorphic (IConst _) = false
| locally_monomorphic (IVar _) = true
| locally_monomorphic (t `$ _) = locally_monomorphic t
- | locally_monomorphic (_ `|-> t) = locally_monomorphic t
+ | locally_monomorphic (_ `|=> t) = locally_monomorphic t
| locally_monomorphic (ICase ((_, ds), _)) = exists (locally_monomorphic o snd) ds;
@@ -397,8 +397,8 @@
| map_terms_bottom_up f (t as IVar _) = f t
| map_terms_bottom_up f (t1 `$ t2) = f
(map_terms_bottom_up f t1 `$ map_terms_bottom_up f t2)
- | map_terms_bottom_up f ((v, ty) `|-> t) = f
- ((v, ty) `|-> map_terms_bottom_up f t)
+ | map_terms_bottom_up f ((v, ty) `|=> t) = f
+ ((v, ty) `|=> map_terms_bottom_up f t)
| map_terms_bottom_up f (ICase (((t, ty), ps), t0)) = f
(ICase (((map_terms_bottom_up f t, ty), (map o pairself)
(map_terms_bottom_up f) ps), map_terms_bottom_up f t0));
@@ -581,7 +581,7 @@
in
translate_typ thy algbr funcgr ty
##>> translate_term thy algbr funcgr thm t
- #>> (fn (ty, t) => (v, ty) `|-> t)
+ #>> (fn (ty, t) => (v, ty) `|=> t)
end
| translate_term thy algbr funcgr thm (t as _ $ _) =
case strip_comb t
@@ -636,12 +636,12 @@
else map (uncurry mk_clause)
(AList.make (Code.no_args thy) case_pats ~~ ts_clause);
fun retermify ty (_, (IVar x, body)) =
- (x, ty) `|-> body
+ (x, ty) `|=> body
| retermify _ (_, (pat, body)) =
let
val (IConst (_, (_, tys)), ts) = unfold_app pat;
val vs = map2 (fn IVar x => fn ty => (x, ty)) ts tys;
- in vs `|--> body end;
+ in vs `|==> body end;
fun mk_icase const t ty clauses =
let
val (ts1, ts2) = chop t_pos (map (retermify ty) clauses);
@@ -668,7 +668,7 @@
in
fold_map (translate_typ thy algbr funcgr) tys
##>> translate_case thy algbr funcgr thm case_scheme ((c, ty), ts @ map Free vs)
- #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
+ #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|==> t)
end
else if length ts > num_args then
translate_case thy algbr funcgr thm case_scheme ((c, ty), Library.take (num_args, ts))
--- a/src/Tools/nbe.ML Fri Jun 19 17:23:21 2009 +0200
+++ b/src/Tools/nbe.ML Fri Jun 19 17:26:40 2009 +0200
@@ -192,7 +192,7 @@
in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
and of_iapp match_cont (IConst (c, ((_, dss), _))) ts = constapp c dss ts
| of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound v) ts
- | of_iapp match_cont ((v, _) `|-> t) ts =
+ | of_iapp match_cont ((v, _) `|=> t) ts =
nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound v]) (of_iterm NONE t))) ts
| of_iapp match_cont (ICase (((t, _), cs), t0)) ts =
nbe_apps (ml_cases (of_iterm NONE t)