src/HOL/List.thy
changeset 46138 85f8d8a8c711
parent 46133 d9fe85d3d2cd
child 46143 c932c80d3eae
     1.1 --- a/src/HOL/List.thy	Fri Jan 06 16:45:19 2012 +0100
     1.2 +++ b/src/HOL/List.thy	Fri Jan 06 17:44:42 2012 +0100
     1.3 @@ -349,90 +349,91 @@
     1.4  mangled). In such cases it can be advisable to introduce separate
     1.5  definitions for the list comprehensions in question.  *}
     1.6  
     1.7 -nonterminal lc_gen and lc_qual and lc_quals
     1.8 +nonterminal lc_qual and lc_quals
     1.9  
    1.10  syntax
    1.11 -"_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  ("[_ . __")
    1.12 -"_lc_gen" :: "lc_gen \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _")
    1.13 -"_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")
    1.14 -(*"_lc_let" :: "letbinds => lc_qual"  ("let _")*)
    1.15 -"_lc_end" :: "lc_quals" ("]")
    1.16 -"_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __")
    1.17 -"_lc_abs" :: "'a => 'b list => 'b list"
    1.18 -"_strip_positions" :: "'a \<Rightarrow> lc_gen"  ("_")
    1.19 +  "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  ("[_ . __")
    1.20 +  "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ <- _")
    1.21 +  "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")
    1.22 +  (*"_lc_let" :: "letbinds => lc_qual"  ("let _")*)
    1.23 +  "_lc_end" :: "lc_quals" ("]")
    1.24 +  "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals"  (", __")
    1.25 +  "_lc_abs" :: "'a => 'b list => 'b list"
    1.26  
    1.27  (* These are easier than ML code but cannot express the optimized
    1.28     translation of [e. p<-xs]
    1.29  translations
    1.30 -"[e. p<-xs]" => "concat(map (_lc_abs p [e]) xs)"
    1.31 -"_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)"
    1.32 - => "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)"
    1.33 -"[e. P]" => "if P then [e] else []"
    1.34 -"_listcompr e (_lc_test P) (_lc_quals Q Qs)"
    1.35 - => "if P then (_listcompr e Q Qs) else []"
    1.36 -"_listcompr e (_lc_let b) (_lc_quals Q Qs)"
    1.37 - => "_Let b (_listcompr e Q Qs)"
    1.38 +  "[e. p<-xs]" => "concat(map (_lc_abs p [e]) xs)"
    1.39 +  "_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)"
    1.40 +   => "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)"
    1.41 +  "[e. P]" => "if P then [e] else []"
    1.42 +  "_listcompr e (_lc_test P) (_lc_quals Q Qs)"
    1.43 +   => "if P then (_listcompr e Q Qs) else []"
    1.44 +  "_listcompr e (_lc_let b) (_lc_quals Q Qs)"
    1.45 +   => "_Let b (_listcompr e Q Qs)"
    1.46  *)
    1.47  
    1.48  syntax (xsymbols)
    1.49 -"_lc_gen" :: "lc_gen \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
    1.50 +  "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ \<leftarrow> _")
    1.51  syntax (HTML output)
    1.52 -"_lc_gen" :: "lc_gen \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
    1.53 +  "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ \<leftarrow> _")
    1.54  
    1.55  parse_translation (advanced) {*
    1.56 -let
    1.57 -  val NilC = Syntax.const @{const_syntax Nil};
    1.58 -  val ConsC = Syntax.const @{const_syntax Cons};
    1.59 -  val mapC = Syntax.const @{const_syntax map};
    1.60 -  val concatC = Syntax.const @{const_syntax concat};
    1.61 -  val IfC = Syntax.const @{const_syntax If};
    1.62 -
    1.63 -  fun singl x = ConsC $ x $ NilC;
    1.64 -
    1.65 -  fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
    1.66 -    let
    1.67 -      (* FIXME proper name context!? *)
    1.68 -      val x = Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT);
    1.69 -      val e = if opti then singl e else e;
    1.70 -      val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e;
    1.71 -      val case2 =
    1.72 -        Syntax.const @{syntax_const "_case1"} $
    1.73 -          Syntax.const @{const_syntax dummy_pattern} $ NilC;
    1.74 -      val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
    1.75 -      val ft = Datatype_Case.case_tr false ctxt [x, cs];
    1.76 -    in lambda x ft end;
    1.77 -
    1.78 -  fun abs_tr ctxt (p as Free (s, T)) e opti =
    1.79 -        let
    1.80 -          val thy = Proof_Context.theory_of ctxt;
    1.81 -          val s' = Proof_Context.intern_const ctxt s;
    1.82 -        in
    1.83 -          if Sign.declared_const thy s'
    1.84 -          then (pat_tr ctxt p e opti, false)
    1.85 -          else (lambda p e, true)
    1.86 -        end
    1.87 -    | abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false);
    1.88 -
    1.89 -  fun lc_tr ctxt [e, Const (@{syntax_const "_lc_test"}, _) $ b, qs] =
    1.90 -        let
    1.91 -          val res =
    1.92 -            (case qs of
    1.93 -              Const (@{syntax_const "_lc_end"}, _) => singl e
    1.94 -            | Const (@{syntax_const "_lc_quals"}, _) $ q $ qs => lc_tr ctxt [e, q, qs]);
    1.95 -        in IfC $ b $ res $ NilC end
    1.96 -    | lc_tr ctxt
    1.97 -          [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
    1.98 -            Const(@{syntax_const "_lc_end"}, _)] =
    1.99 -        (case abs_tr ctxt p e true of
   1.100 -          (f, true) => mapC $ f $ es
   1.101 -        | (f, false) => concatC $ (mapC $ f $ es))
   1.102 -    | lc_tr ctxt
   1.103 -          [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
   1.104 -            Const (@{syntax_const "_lc_quals"}, _) $ q $ qs] =
   1.105 -        let val e' = lc_tr ctxt [e, q, qs];
   1.106 -        in concatC $ (mapC $ (fst (abs_tr ctxt p e' false)) $ es) end;
   1.107 -
   1.108 -in [(@{syntax_const "_listcompr"}, lc_tr)] end
   1.109 +  let
   1.110 +    val NilC = Syntax.const @{const_syntax Nil};
   1.111 +    val ConsC = Syntax.const @{const_syntax Cons};
   1.112 +    val mapC = Syntax.const @{const_syntax map};
   1.113 +    val concatC = Syntax.const @{const_syntax concat};
   1.114 +    val IfC = Syntax.const @{const_syntax If};
   1.115 +
   1.116 +    fun single x = ConsC $ x $ NilC;
   1.117 +
   1.118 +    fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
   1.119 +      let
   1.120 +        (* FIXME proper name context!? *)
   1.121 +        val x =
   1.122 +          Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT);
   1.123 +        val e = if opti then single e else e;
   1.124 +        val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e;
   1.125 +        val case2 =
   1.126 +          Syntax.const @{syntax_const "_case1"} $
   1.127 +            Syntax.const @{const_syntax dummy_pattern} $ NilC;
   1.128 +        val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
   1.129 +      in Syntax_Trans.abs_tr [x, Datatype_Case.case_tr false ctxt [x, cs]] end;
   1.130 +
   1.131 +    fun abs_tr ctxt p e opti =
   1.132 +      (case Term_Position.strip_positions p of
   1.133 +        Free (s, T) =>
   1.134 +          let
   1.135 +            val thy = Proof_Context.theory_of ctxt;
   1.136 +            val s' = Proof_Context.intern_const ctxt s;
   1.137 +          in
   1.138 +            if Sign.declared_const thy s'
   1.139 +            then (pat_tr ctxt p e opti, false)
   1.140 +            else (Syntax_Trans.abs_tr [p, e], true)
   1.141 +          end
   1.142 +      | _ => (pat_tr ctxt p e opti, false));
   1.143 +
   1.144 +    fun lc_tr ctxt [e, Const (@{syntax_const "_lc_test"}, _) $ b, qs] =
   1.145 +          let
   1.146 +            val res =
   1.147 +              (case qs of
   1.148 +                Const (@{syntax_const "_lc_end"}, _) => single e
   1.149 +              | Const (@{syntax_const "_lc_quals"}, _) $ q $ qs => lc_tr ctxt [e, q, qs]);
   1.150 +          in IfC $ b $ res $ NilC end
   1.151 +      | lc_tr ctxt
   1.152 +            [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
   1.153 +              Const(@{syntax_const "_lc_end"}, _)] =
   1.154 +          (case abs_tr ctxt p e true of
   1.155 +            (f, true) => mapC $ f $ es
   1.156 +          | (f, false) => concatC $ (mapC $ f $ es))
   1.157 +      | lc_tr ctxt
   1.158 +            [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
   1.159 +              Const (@{syntax_const "_lc_quals"}, _) $ q $ qs] =
   1.160 +          let val e' = lc_tr ctxt [e, q, qs];
   1.161 +          in concatC $ (mapC $ (fst (abs_tr ctxt p e' false)) $ es) end;
   1.162 +
   1.163 +  in [(@{syntax_const "_listcompr"}, lc_tr)] end
   1.164  *}
   1.165  
   1.166  ML {*