more appropriate syntax for IML abstraction
authorhaftmann
Fri Jun 19 17:26:40 2009 +0200 (2009-06-19)
changeset 317249b5a128cdb5c
parent 31723 f5cafe803b55
child 31725 f08507464b9d
more appropriate syntax for IML abstraction
src/HOL/Imperative_HOL/Heap_Monad.thy
src/Tools/code/code_haskell.ML
src/Tools/code/code_ml.ML
src/Tools/code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jun 19 17:23:21 2009 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jun 19 17:26:40 2009 +0200
     1.3 @@ -318,7 +318,7 @@
     1.4        val dummy_case_term = IVar dummy_name;
     1.5        (*assumption: dummy values are not relevant for serialization*)
     1.6        val unitt = IConst (unit', (([], []), []));
     1.7 -      fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t)
     1.8 +      fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
     1.9          | dest_abs (t, ty) =
    1.10              let
    1.11                val vs = Code_Thingol.fold_varnames cons t [];
    1.12 @@ -337,7 +337,7 @@
    1.13                  then tr_bind' [(x1, ty1), (x2, ty2)]
    1.14                  else force t
    1.15              | _ => force t;
    1.16 -    in (dummy_name, dummy_type) `|-> ICase (((IVar dummy_name, dummy_type),
    1.17 +    in (dummy_name, dummy_type) `|=> ICase (((IVar dummy_name, dummy_type),
    1.18        [(unitt, tr_bind' ts)]), dummy_case_term) end
    1.19    and imp_monad_bind' bind' return' unit' (const as (c, (_, tys))) ts = if c = bind' then case (ts, tys)
    1.20       of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)]
    1.21 @@ -349,7 +349,7 @@
    1.22      | imp_monad_bind bind' return' unit' (t as _ `$ _) = (case unfold_app t
    1.23         of (IConst const, ts) => imp_monad_bind' bind' return' unit' const ts
    1.24          | (t, ts) => imp_monad_bind bind' return' unit' t `$$ map (imp_monad_bind bind' return' unit') ts)
    1.25 -    | imp_monad_bind bind' return' unit' (v_ty `|-> t) = v_ty `|-> imp_monad_bind bind' return' unit' t
    1.26 +    | imp_monad_bind bind' return' unit' (v_ty `|=> t) = v_ty `|=> imp_monad_bind bind' return' unit' t
    1.27      | imp_monad_bind bind' return' unit' (ICase (((t, ty), pats), t0)) = ICase
    1.28          (((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);
    1.29  
     2.1 --- a/src/Tools/code/code_haskell.ML	Fri Jun 19 17:23:21 2009 +0200
     2.2 +++ b/src/Tools/code/code_haskell.ML	Fri Jun 19 17:26:40 2009 +0200
     2.3 @@ -70,7 +70,7 @@
     2.4                  ])
     2.5        | pr_term tyvars thm vars fxy (IVar v) =
     2.6            (str o Code_Printer.lookup_var vars) v
     2.7 -      | pr_term tyvars thm vars fxy (t as _ `|-> _) =
     2.8 +      | pr_term tyvars thm vars fxy (t as _ `|=> _) =
     2.9            let
    2.10              val (binds, t') = Code_Thingol.unfold_abs t;
    2.11              fun pr ((v, pat), ty) = pr_bind tyvars thm BR ((SOME v, pat), ty);
    2.12 @@ -240,7 +240,7 @@
    2.13            end
    2.14        | pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
    2.15            let
    2.16 -            val split_abs_pure = (fn (v, _) `|-> t => SOME (v, t) | _ => NONE);
    2.17 +            val split_abs_pure = (fn (v, _) `|=> t => SOME (v, t) | _ => NONE);
    2.18              val unfold_abs_pure = Code_Thingol.unfoldr split_abs_pure;
    2.19              val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
    2.20              fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam
     3.1 --- a/src/Tools/code/code_ml.ML	Fri Jun 19 17:23:21 2009 +0200
     3.2 +++ b/src/Tools/code/code_ml.ML	Fri Jun 19 17:26:40 2009 +0200
     3.3 @@ -92,7 +92,7 @@
     3.4             of SOME c_ts => pr_app is_closure thm vars fxy c_ts
     3.5              | NONE => brackify fxy
     3.6                 [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2])
     3.7 -      | pr_term is_closure thm vars fxy (t as _ `|-> _) =
     3.8 +      | pr_term is_closure thm vars fxy (t as _ `|=> _) =
     3.9            let
    3.10              val (binds, t') = Code_Thingol.unfold_abs t;
    3.11              fun pr ((v, pat), ty) =
    3.12 @@ -401,7 +401,7 @@
    3.13             of SOME c_ts => pr_app is_closure thm vars fxy c_ts
    3.14              | NONE =>
    3.15                  brackify fxy [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2])
    3.16 -      | pr_term is_closure thm vars fxy (t as _ `|-> _) =
    3.17 +      | pr_term is_closure thm vars fxy (t as _ `|=> _) =
    3.18            let
    3.19              val (binds, t') = Code_Thingol.unfold_abs t;
    3.20              fun pr ((v, pat), ty) = pr_bind is_closure thm BR ((SOME v, pat), ty);
     4.1 --- a/src/Tools/code/code_thingol.ML	Fri Jun 19 17:23:21 2009 +0200
     4.2 +++ b/src/Tools/code/code_thingol.ML	Fri Jun 19 17:26:40 2009 +0200
     4.3 @@ -8,8 +8,8 @@
     4.4  infix 8 `%%;
     4.5  infix 4 `$;
     4.6  infix 4 `$$;
     4.7 -infixr 3 `|->;
     4.8 -infixr 3 `|-->;
     4.9 +infixr 3 `|=>;
    4.10 +infixr 3 `|==>;
    4.11  
    4.12  signature BASIC_CODE_THINGOL =
    4.13  sig
    4.14 @@ -25,11 +25,11 @@
    4.15        IConst of const
    4.16      | IVar of vname
    4.17      | `$ of iterm * iterm
    4.18 -    | `|-> of (vname * itype) * iterm
    4.19 +    | `|=> of (vname * itype) * iterm
    4.20      | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
    4.21          (*((term, type), [(selector pattern, body term )]), primitive term)*)
    4.22    val `$$ : iterm * iterm list -> iterm;
    4.23 -  val `|--> : (vname * itype) list * iterm -> iterm;
    4.24 +  val `|==> : (vname * itype) list * iterm -> iterm;
    4.25    type typscheme = (vname * sort) list * itype;
    4.26  end;
    4.27  
    4.28 @@ -128,21 +128,21 @@
    4.29      IConst of const
    4.30    | IVar of vname
    4.31    | `$ of iterm * iterm
    4.32 -  | `|-> of (vname * itype) * iterm
    4.33 +  | `|=> of (vname * itype) * iterm
    4.34    | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
    4.35      (*see also signature*)
    4.36  
    4.37  val op `$$ = Library.foldl (op `$);
    4.38 -val op `|--> = Library.foldr (op `|->);
    4.39 +val op `|==> = Library.foldr (op `|=>);
    4.40  
    4.41  val unfold_app = unfoldl
    4.42    (fn op `$ t => SOME t
    4.43      | _ => NONE);
    4.44  
    4.45  val split_abs =
    4.46 -  (fn (v, ty) `|-> (t as ICase (((IVar w, _), [(p, t')]), _)) =>
    4.47 +  (fn (v, ty) `|=> (t as ICase (((IVar w, _), [(p, t')]), _)) =>
    4.48          if v = w then SOME (((v, SOME p), ty), t') else SOME (((v, NONE), ty), t)
    4.49 -    | (v, ty) `|-> t => SOME (((v, NONE), ty), t)
    4.50 +    | (v, ty) `|=> t => SOME (((v, NONE), ty), t)
    4.51      | _ => NONE);
    4.52  
    4.53  val unfold_abs = unfoldr split_abs;
    4.54 @@ -161,7 +161,7 @@
    4.55  fun fold_aiterms f (t as IConst _) = f t
    4.56    | fold_aiterms f (t as IVar _) = f t
    4.57    | fold_aiterms f (t1 `$ t2) = fold_aiterms f t1 #> fold_aiterms f t2
    4.58 -  | fold_aiterms f (t as _ `|-> t') = f t #> fold_aiterms f t'
    4.59 +  | fold_aiterms f (t as _ `|=> t') = f t #> fold_aiterms f t'
    4.60    | fold_aiterms f (ICase (_, t)) = fold_aiterms f t;
    4.61  
    4.62  fun fold_constnames f =
    4.63 @@ -173,7 +173,7 @@
    4.64  fun fold_varnames f =
    4.65    let
    4.66      fun add (IVar v) = f v
    4.67 -      | add ((v, _) `|-> _) = f v
    4.68 +      | add ((v, _) `|=> _) = f v
    4.69        | add _ = I;
    4.70    in fold_aiterms add end;
    4.71  
    4.72 @@ -182,7 +182,7 @@
    4.73      fun add _ (IConst _) = I
    4.74        | add vs (IVar v) = if not (member (op =) vs v) then f v else I
    4.75        | add vs (t1 `$ t2) = add vs t1 #> add vs t2
    4.76 -      | add vs ((v, _) `|-> t) = add (insert (op =) v vs) t
    4.77 +      | add vs ((v, _) `|=> t) = add (insert (op =) v vs) t
    4.78        | add vs (ICase (_, t)) = add vs t;
    4.79    in add [] end;
    4.80  
    4.81 @@ -204,7 +204,7 @@
    4.82      val l = k - j;
    4.83      val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
    4.84      val vs_tys = Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys);
    4.85 -  in vs_tys `|--> IConst c `$$ ts @ map (fn (v, _) => IVar v) vs_tys end;
    4.86 +  in vs_tys `|==> IConst c `$$ ts @ map (fn (v, _) => IVar v) vs_tys end;
    4.87  
    4.88  fun contains_dictvar t =
    4.89    let
    4.90 @@ -218,7 +218,7 @@
    4.91  fun locally_monomorphic (IConst _) = false
    4.92    | locally_monomorphic (IVar _) = true
    4.93    | locally_monomorphic (t `$ _) = locally_monomorphic t
    4.94 -  | locally_monomorphic (_ `|-> t) = locally_monomorphic t
    4.95 +  | locally_monomorphic (_ `|=> t) = locally_monomorphic t
    4.96    | locally_monomorphic (ICase ((_, ds), _)) = exists (locally_monomorphic o snd) ds;
    4.97  
    4.98  
    4.99 @@ -397,8 +397,8 @@
   4.100    | map_terms_bottom_up f (t as IVar _) = f t
   4.101    | map_terms_bottom_up f (t1 `$ t2) = f
   4.102        (map_terms_bottom_up f t1 `$ map_terms_bottom_up f t2)
   4.103 -  | map_terms_bottom_up f ((v, ty) `|-> t) = f
   4.104 -      ((v, ty) `|-> map_terms_bottom_up f t)
   4.105 +  | map_terms_bottom_up f ((v, ty) `|=> t) = f
   4.106 +      ((v, ty) `|=> map_terms_bottom_up f t)
   4.107    | map_terms_bottom_up f (ICase (((t, ty), ps), t0)) = f
   4.108        (ICase (((map_terms_bottom_up f t, ty), (map o pairself)
   4.109          (map_terms_bottom_up f) ps), map_terms_bottom_up f t0));
   4.110 @@ -581,7 +581,7 @@
   4.111        in
   4.112          translate_typ thy algbr funcgr ty
   4.113          ##>> translate_term thy algbr funcgr thm t
   4.114 -        #>> (fn (ty, t) => (v, ty) `|-> t)
   4.115 +        #>> (fn (ty, t) => (v, ty) `|=> t)
   4.116        end
   4.117    | translate_term thy algbr funcgr thm (t as _ $ _) =
   4.118        case strip_comb t
   4.119 @@ -636,12 +636,12 @@
   4.120        else map (uncurry mk_clause)
   4.121          (AList.make (Code.no_args thy) case_pats ~~ ts_clause);
   4.122      fun retermify ty (_, (IVar x, body)) =
   4.123 -          (x, ty) `|-> body
   4.124 +          (x, ty) `|=> body
   4.125        | retermify _ (_, (pat, body)) =
   4.126            let
   4.127              val (IConst (_, (_, tys)), ts) = unfold_app pat;
   4.128              val vs = map2 (fn IVar x => fn ty => (x, ty)) ts tys;
   4.129 -          in vs `|--> body end;
   4.130 +          in vs `|==> body end;
   4.131      fun mk_icase const t ty clauses =
   4.132        let
   4.133          val (ts1, ts2) = chop t_pos (map (retermify ty) clauses);
   4.134 @@ -668,7 +668,7 @@
   4.135      in
   4.136        fold_map (translate_typ thy algbr funcgr) tys
   4.137        ##>> translate_case thy algbr funcgr thm case_scheme ((c, ty), ts @ map Free vs)
   4.138 -      #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
   4.139 +      #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|==> t)
   4.140      end
   4.141    else if length ts > num_args then
   4.142      translate_case thy algbr funcgr thm case_scheme ((c, ty), Library.take (num_args, ts))
     5.1 --- a/src/Tools/nbe.ML	Fri Jun 19 17:23:21 2009 +0200
     5.2 +++ b/src/Tools/nbe.ML	Fri Jun 19 17:26:40 2009 +0200
     5.3 @@ -192,7 +192,7 @@
     5.4            in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
     5.5          and of_iapp match_cont (IConst (c, ((_, dss), _))) ts = constapp c dss ts
     5.6            | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound v) ts
     5.7 -          | of_iapp match_cont ((v, _) `|-> t) ts =
     5.8 +          | of_iapp match_cont ((v, _) `|=> t) ts =
     5.9                nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound v]) (of_iterm NONE t))) ts
    5.10            | of_iapp match_cont (ICase (((t, _), cs), t0)) ts =
    5.11                nbe_apps (ml_cases (of_iterm NONE t)