theory FSet3imports "../../../Nominal/FSet"begin(* TBD *)text {* syntax for fset comprehensions (adapted from lists) *}nonterminals fsc_qual fsc_qualssyntax"_fsetcompr" :: "'a \<Rightarrow> fsc_qual \<Rightarrow> fsc_quals \<Rightarrow> 'a fset" ("{|_ . __")"_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ <- _")"_fsc_test" :: "bool \<Rightarrow> fsc_qual" ("_")"_fsc_end" :: "fsc_quals" ("|}")"_fsc_quals" :: "fsc_qual \<Rightarrow> fsc_quals \<Rightarrow> fsc_quals" (", __")"_fsc_abs" :: "'a => 'b fset => 'b fset"syntax (xsymbols)"_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ \<leftarrow> _")syntax (HTML output)"_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ \<leftarrow> _")parse_translation (advanced) {*let val femptyC = Syntax.const @{const_name fempty}; val finsertC = Syntax.const @{const_name finsert}; val fmapC = Syntax.const @{const_name fmap}; val fconcatC = Syntax.const @{const_name fconcat}; val IfC = Syntax.const @{const_name If}; fun fsingl x = finsertC $ x $ femptyC; fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *) let val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT); val e = if opti then fsingl e else e; val case1 = Syntax.const "_case1" $ p $ e; val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN $ femptyC; val cs = Syntax.const "_case2" $ case1 $ case2 val ft = Datatype_Case.case_tr false Datatype.info_of_constr ctxt [x, cs] in lambda x ft end; fun abs_tr ctxt (p as Free(s,T)) e opti = let val thy = ProofContext.theory_of ctxt; val s' = Sign.intern_const thy s in if Sign.declared_const thy s' then (pat_tr ctxt p e opti, false) else (lambda p e, true) end | abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false); fun fsc_tr ctxt [e, Const("_fsc_test",_) $ b, qs] = let val res = case qs of Const("_fsc_end",_) => fsingl e | Const("_fsc_quals",_)$ q $ qs => fsc_tr ctxt [e, q, qs]; in IfC $ b $ res $ femptyC end | fsc_tr ctxt [e, Const("_fsc_gen",_) $ p $ es, Const("_fsc_end",_)] = (case abs_tr ctxt p e true of (f,true) => fmapC $ f $ es | (f, false) => fconcatC $ (fmapC $ f $ es)) | fsc_tr ctxt [e, Const("_fsc_gen",_) $ p $ es, Const("_fsc_quals",_) $ q $ qs] = let val e' = fsc_tr ctxt [e, q, qs]; in fconcatC $ (fmapC $ (fst (abs_tr ctxt p e' false)) $ es) endin [("_fsetcompr", fsc_tr)] end*}(* NEEDS FIXING *)(* examles *)(*term "{|(x,y,z). b|}"term "{|x. x \<leftarrow> xs|}"term "{|(x,y,z). x\<leftarrow>xs|}"term "{|e x y. x\<leftarrow>xs, y\<leftarrow>ys|}"term "{|(x,y,z). x<a, x>b|}"term "{|(x,y,z). x\<leftarrow>xs, x>b|}"term "{|(x,y,z). x<a, x\<leftarrow>xs|}"term "{|(x,y). Cons True x \<leftarrow> xs|}"term "{|(x,y,z). Cons x [] \<leftarrow> xs|}"term "{|(x,y,z). x<a, x>b, x=d|}"term "{|(x,y,z). x<a, x>b, y\<leftarrow>ys|}"term "{|(x,y,z). x<a, x\<leftarrow>xs,y>b|}"term "{|(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys|}"term "{|(x,y,z). x\<leftarrow>xs, x>b, y<a|}"term "{|(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys|}"term "{|(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x|}"term "{|(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs|}"*)(* BELOW CONSTRUCTION SITE *)end