# HG changeset patch # User nipkow # Date 1528043018 -7200 # Node ID 23b2fad1729a35b85fd2d01f769a8780202d5bb5 # Parent 20375f232f3bfb7ebcea2e7efa2517cb2905f30d# Parent 27237ee2e8898794edf3b08c4b102a818666e6f5 merged diff -r 20375f232f3b -r 23b2fad1729a src/HOL/List.thy --- a/src/HOL/List.thy Sun Jun 03 15:22:30 2018 +0100 +++ b/src/HOL/List.thy Sun Jun 03 18:23:38 2018 +0200 @@ -433,75 +433,70 @@ syntax (ASCII) "_lc_gen" :: "'a \ 'a list \ lc_qual" ("_ <- _") -(* These are easier than ML code but cannot express the optimized - translation of [e. p<-xs] -translations - "[e. p<-xs]" => "concat(map (_lc_abs p [e]) xs)" - "_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)" - => "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)" - "[e. P]" => "if P then [e] else []" - "_listcompr e (_lc_test P) (_lc_quals Q Qs)" - => "if P then (_listcompr e Q Qs) else []" - "_listcompr e (_lc_let b) (_lc_quals Q Qs)" - => "_Let b (_listcompr e Q Qs)" -*) - parse_translation \ - let - val NilC = Syntax.const @{const_syntax Nil}; - val ConsC = Syntax.const @{const_syntax Cons}; - val mapC = Syntax.const @{const_syntax map}; - val concatC = Syntax.const @{const_syntax concat}; - val IfC = Syntax.const @{const_syntax If}; - - fun single x = ConsC $ x $ NilC; - - fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *) - let - (* FIXME proper name context!? *) - val x = - Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT); - val e = if opti then single e else e; - val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e; - val case2 = - Syntax.const @{syntax_const "_case1"} $ - Syntax.const @{const_syntax Pure.dummy_pattern} $ NilC; - val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2; - in Syntax_Trans.abs_tr [x, Case_Translation.case_tr false ctxt [x, cs]] end; - - fun abs_tr ctxt p e opti = - (case Term_Position.strip_positions p of - Free (s, T) => - let - val thy = Proof_Context.theory_of ctxt; - val s' = Proof_Context.intern_const ctxt s; - in - if Sign.declared_const thy s' - then (pat_tr ctxt p e opti, false) - else (Syntax_Trans.abs_tr [p, e], true) - end - | _ => (pat_tr ctxt p e opti, false)); - - fun lc_tr ctxt [e, Const (@{syntax_const "_lc_test"}, _) $ b, qs] = - let - val res = - (case qs of - Const (@{syntax_const "_lc_end"}, _) => single e - | Const (@{syntax_const "_lc_quals"}, _) $ q $ qs => lc_tr ctxt [e, q, qs]); - in IfC $ b $ res $ NilC end - | lc_tr ctxt - [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es, - Const(@{syntax_const "_lc_end"}, _)] = - (case abs_tr ctxt p e true of - (f, true) => mapC $ f $ es - | (f, false) => concatC $ (mapC $ f $ es)) - | lc_tr ctxt - [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es, - Const (@{syntax_const "_lc_quals"}, _) $ q $ qs] = - let val e' = lc_tr ctxt [e, q, qs]; - in concatC $ (mapC $ (fst (abs_tr ctxt p e' false)) $ es) end; - - in [(@{syntax_const "_listcompr"}, lc_tr)] end +let + val NilC = Syntax.const @{const_syntax Nil}; + val ConsC = Syntax.const @{const_syntax Cons}; + val mapC = Syntax.const @{const_syntax map}; + val concatC = Syntax.const @{const_syntax concat}; + val IfC = Syntax.const @{const_syntax If}; + val dummyC = Syntax.const @{const_syntax Pure.dummy_pattern} + + fun single x = ConsC $ x $ NilC; + + fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *) + let + (* FIXME proper name context!? *) + val x = + Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT); + val e = if opti then single e else e; + val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e; + val case2 = + Syntax.const @{syntax_const "_case1"} $ dummyC $ NilC; + val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2; + in Syntax_Trans.abs_tr [x, Case_Translation.case_tr false ctxt [x, cs]] end; + + fun pair_pat_tr (x as Free _) e = Syntax_Trans.abs_tr [x, e] + | pair_pat_tr (_ $ p1 $ p2) e = + Syntax.const @{const_syntax case_prod} $ pair_pat_tr p1 (pair_pat_tr p2 e) + | pair_pat_tr dummy e = Syntax_Trans.abs_tr [Syntax.const "_idtdummy", e] + + fun pair_pat ctxt (Const (@{const_syntax "Pair"},_) $ s $ t) = + pair_pat ctxt s andalso pair_pat ctxt t + | pair_pat ctxt (Free (s,_)) = + let + val thy = Proof_Context.theory_of ctxt; + val s' = Proof_Context.intern_const ctxt s; + in not (Sign.declared_const thy s') end + | pair_pat _ t = (t = dummyC); + + fun abs_tr ctxt p e opti = + let val p = Term_Position.strip_positions p + in if pair_pat ctxt p + then (pair_pat_tr p e, true) + else (pat_tr ctxt p e opti, false) + end + + fun lc_tr ctxt [e, Const (@{syntax_const "_lc_test"}, _) $ b, qs] = + let + val res = + (case qs of + Const (@{syntax_const "_lc_end"}, _) => single e + | Const (@{syntax_const "_lc_quals"}, _) $ q $ qs => lc_tr ctxt [e, q, qs]); + in IfC $ b $ res $ NilC end + | lc_tr ctxt + [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es, + Const(@{syntax_const "_lc_end"}, _)] = + (case abs_tr ctxt p e true of + (f, true) => mapC $ f $ es + | (f, false) => concatC $ (mapC $ f $ es)) + | lc_tr ctxt + [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es, + Const (@{syntax_const "_lc_quals"}, _) $ q $ qs] = + let val e' = lc_tr ctxt [e, q, qs]; + in concatC $ (mapC $ (fst (abs_tr ctxt p e' false)) $ es) end; + +in [(@{syntax_const "_listcompr"}, lc_tr)] end \ ML_val \ @@ -513,8 +508,8 @@ quote (Input.source_content s1) ^ Position.here_list [Input.pos_of s1, Input.pos_of s2]); in check \[(x,y,z). b]\ \if b then [(x, y, z)] else []\; - check \[(x,y,z). x\xs]\ \map (\x. (x, y, z)) xs\; - check \[e x y. x\xs, y\ys]\ \concat (map (\x. map (\y. e x y) ys) xs)\; + check \[(x,y,z). (x,_,y)\xs]\ \map (\(x,_,y). (x, y, z)) xs\; + check \[e x y. (x,_)\xs, y\ys]\ \concat (map (\(x,_). map (\y. e x y) ys) xs)\; check \[(x,y,z). xb]\ \if x < a then if b < x then [(x, y, z)] else [] else []\; check \[(x,y,z). x\xs, x>b]\ \concat (map (\x. if b < x then [(x, y, z)] else []) xs)\; check \[(x,y,z). xxs]\ \if x < a then map (\x. (x, y, z)) xs else []\; @@ -526,26 +521,21 @@ \if x < a then if b < x then if x = d then [(x, y, z)] else [] else [] else []\; check \[(x,y,z). xb, y\ys]\ \if x < a then if b < x then map (\y. (x, y, z)) ys else [] else []\; - check \[(x,y,z). xxs,y>b]\ - \if x < a then concat (map (\x. if b < y then [(x, y, z)] else []) xs) else []\; + check \[(x,y,z). xxs,y>b]\ + \if x < a then concat (map (\(_,x). if b < y then [(x, y, z)] else []) xs) else []\; check \[(x,y,z). xxs, y\ys]\ \if x < a then concat (map (\x. map (\y. (x, y, z)) ys) xs) else []\; check \[(x,y,z). x\xs, x>b, y \concat (map (\x. if b < x then if y < a then [(x, y, z)] else [] else []) xs)\; check \[(x,y,z). x\xs, x>b, y\ys]\ \concat (map (\x. if b < x then map (\y. (x, y, z)) ys else []) xs)\; - check \[(x,y,z). x\xs, y\ys,y>x]\ - \concat (map (\x. concat (map (\y. if x < y then [(x, y, z)] else []) ys)) xs)\; + check \[(x,y,z). x\xs, (y,_)\ys,y>x]\ + \concat (map (\x. concat (map (\(y,_). if x < y then [(x, y, z)] else []) ys)) xs)\; check \[(x,y,z). x\xs, y\ys,z\zs]\ \concat (map (\x. concat (map (\y. map (\z. (x, y, z)) zs) ys)) xs)\ end; \ -(* -term "[(x,y). x\xs, let xx = x+x, y\ys, y \ xx]" -*) - - ML \ (* Simproc for rewriting list comprehensions applied to List.set to set comprehension. *)