# HG changeset patch # User Christian Urban # Date 1257151169 -3600 # Node ID 264c7b9d19f4a3784db7dc4c32ae9a0d199e8c2f # Parent 77ff9624cfd6494d5d2a4ce89cf57047faa8412b# Parent e169a99c6ada483ec30c794e90c0906109514f97 merged diff -r e169a99c6ada -r 264c7b9d19f4 FSet.thy --- a/FSet.thy Sat Oct 31 11:20:55 2009 +0100 +++ b/FSet.thy Mon Nov 02 09:39:29 2009 +0100 @@ -44,7 +44,7 @@ thm EMPTY_def quotient_def (for "'a fset") - INSERT :: "'a \ 'a fset \ 'a fet" + INSERT :: "'a \ 'a fset \ 'a fset" where "INSERT \ op #" @@ -168,10 +168,10 @@ thm fold_def (* FIXME: does not work yet for all types*) -quotient_def (for "'a fset") - fmap::"('a \ 'a) \ 'a fset \ 'a fset" +quotient_def (for "'a fset" "'b fset") + fmap::"('a \ 'b) \ 'a fset \ 'b fset" where - "fmap \ (map::('a \ 'a) \ 'a list \ 'a list)" + "fmap \ map" term map term fmap @@ -296,6 +296,9 @@ by simp (rule list_eq_refl) +print_quotients + + ML {* val qty = @{typ "'a fset"} *} ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "fset" *} diff -r e169a99c6ada -r 264c7b9d19f4 QuotMain.thy --- a/QuotMain.thy Sat Oct 31 11:20:55 2009 +0100 +++ b/QuotMain.thy Mon Nov 02 09:39:29 2009 +0100 @@ -159,17 +159,13 @@ section {* lifting of constants *} ML {* -(* whether ty1 is an instance of ty2 *) -fun matches (ty1, ty2) = - Type.raw_instance (ty1, Logic.varifyT ty2) - fun lookup_snd _ [] _ = NONE | lookup_snd eq ((value, key)::xs) key' = if eq (key', key) then SOME value else lookup_snd eq xs key'; fun lookup_qenv qenv qty = - (case (AList.lookup matches qenv qty) of + (case (AList.lookup (op =) qenv qty) of SOME rty => SOME (qty, rty) | NONE => NONE) *} @@ -225,7 +221,7 @@ fun mk_identity ty = Abs ("", ty, Bound 0) in - if (AList.defined matches qenv ty) + if (AList.defined (op =) qenv ty) then (get_const flag (the (lookup_qenv qenv ty))) else (case ty of TFree _ => (mk_identity ty, (ty, ty)) @@ -259,11 +255,10 @@ end *} -ML {* lookup_snd *} ML {* fun exchange_ty qenv ty = - case (lookup_snd matches qenv ty) of + case (lookup_snd (op =) qenv ty) of SOME qty => qty | NONE => (case ty of @@ -272,6 +267,18 @@ ) *} +ML {* +fun ppair lthy (ty1, ty2) = + "(" ^ (Syntax.string_of_typ lthy ty1) ^ "," ^ (Syntax.string_of_typ lthy ty2) ^ ")" +*} + +ML {* +fun print_env qenv lthy = + map (ppair lthy) qenv + |> commas + |> tracing +*} + ML {* fun make_const_def nconst_bname otrm mx qenv lthy = let @@ -279,6 +286,11 @@ val nconst_ty = exchange_ty qenv otrm_ty val nconst = Const (Binding.name_of nconst_bname, nconst_ty) val def_trm = get_const_def nconst otrm qenv lthy + + val _ = print_env qenv lthy + val _ = Syntax.string_of_typ lthy otrm_ty |> tracing + val _ = Syntax.string_of_typ lthy nconst_ty |> tracing + val _ = Syntax.string_of_term lthy def_trm |> tracing in define (nconst_bname, mx, def_trm) lthy end @@ -288,46 +300,37 @@ fun build_qenv lthy qtys = let val qenv = map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) (quotdata_lookup lthy) - - fun find_assoc qty = - case (AList.lookup matches qenv qty) of - SOME rty => (qty, rty) - | NONE => error (implode - ["Quotient type ", - quote (Syntax.string_of_typ lthy qty), - " does not exists"]) + val tsig = Sign.tsig_of (ProofContext.theory_of lthy) + + fun find_assoc ((qty', rty')::rest) qty = + let + val inst = Type.typ_match tsig (qty', qty) Vartab.empty + in + (Envir.norm_type inst qty, Envir.norm_type inst rty') + end + | find_assoc [] qty = + let + val qtystr = quote (Syntax.string_of_typ lthy qty) + in + error (implode ["Quotient type ", qtystr, " does not exists"]) + end in - map find_assoc qtys + map (find_assoc qenv) qtys end *} ML {* -(* taken from isar_syn.ML *) -val constdecl = - OuterParse.binding -- - (OuterParse.where_ >> K (NONE, NoSyn) || - OuterParse.$$$ "::" |-- OuterParse.!!! ((OuterParse.typ >> SOME) -- - OuterParse.opt_mixfix' --| OuterParse.where_) || - Scan.ahead (OuterParse.$$$ "(") |-- - OuterParse.!!! (OuterParse.mixfix' --| OuterParse.where_ >> pair NONE)) -*} - -ML {* val qd_parser = (Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) -- - (constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop)) -*} - -ML {* -fun pair lthy (ty1, ty2) = - "(" ^ (Syntax.string_of_typ lthy ty1) ^ "," ^ (Syntax.string_of_typ lthy ty2) ^ ")" + (SpecParse.constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop)) *} ML {* -fun parse_qd_spec (qtystrs, ((bind, (typstr__, mx)), (attr__, propstr))) lthy = +fun parse_qd_spec (qtystrs, ((bind, tystr, mx), (attr__, propstr))) lthy = let val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystrs val qenv = build_qenv lthy qtys + val qty = Syntax.parse_typ lthy (the tystr) |> Syntax.check_typ lthy val prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy val (lhs, rhs) = Logic.dest_equals prop in @@ -340,6 +343,8 @@ OuterKeyword.thy_decl (qd_parser >> parse_qd_spec) *} +(* ML {* show_all_types := true *} *) + section {* ATOMIZE *} text {* diff -r e169a99c6ada -r 264c7b9d19f4 QuotTest.thy --- a/QuotTest.thy Sat Oct 31 11:20:55 2009 +0100 +++ b/QuotTest.thy Mon Nov 02 09:39:29 2009 +0100 @@ -2,6 +2,7 @@ imports QuotMain begin + section {* various tests for quotient types*} datatype trm = var "nat" diff -r e169a99c6ada -r 264c7b9d19f4 quotient.ML --- a/quotient.ML Sat Oct 31 11:20:55 2009 +0100 +++ b/quotient.ML Mon Nov 02 09:39:29 2009 +0100 @@ -6,7 +6,7 @@ val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory val note: binding * thm -> local_theory -> thm * local_theory - val maps_lookup: theory -> string -> maps_info option + val maps_lookup_thy: theory -> string -> maps_info option val maps_update_thy: string -> maps_info -> theory -> theory val maps_update: string -> maps_info -> Proof.context -> Proof.context val print_quotdata: Proof.context -> unit @@ -32,7 +32,9 @@ val extend = I fun merge _ = Symtab.merge (K true)) -val maps_lookup = Symtab.lookup o MapsData.get +val maps_lookup_thy = Symtab.lookup o MapsData.get + + fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) @@ -242,7 +244,7 @@ val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name (* storing the quot-info *) - val lthy3 = quotdata_update (abs_ty, rty, rel, equiv_thm) lthy2 + val lthy3 = quotdata_update (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 (* interpretation *) val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))