# HG changeset patch
# User haftmann
# Date 1245425200 -7200
# Node ID 9b5a128cdb5c63a8a2a00537b02ac888e78f26cd
# Parent  f5cafe803b55a2b48f79ab4071c40362e282182c
more appropriate syntax for IML abstraction

diff -r f5cafe803b55 -r 9b5a128cdb5c src/HOL/Imperative_HOL/Heap_Monad.thy
--- 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);
 
diff -r f5cafe803b55 -r 9b5a128cdb5c src/Tools/code/code_haskell.ML
--- 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
diff -r f5cafe803b55 -r 9b5a128cdb5c src/Tools/code/code_ml.ML
--- 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);
diff -r f5cafe803b55 -r 9b5a128cdb5c src/Tools/code/code_thingol.ML
--- 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))
diff -r f5cafe803b55 -r 9b5a128cdb5c src/Tools/nbe.ML
--- 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)