respecting isabelle's programming style in the quotient package by simplifying map_lookup function for data access
authorbulwahn
Thu Oct 27 13:50:55 2011 +0200 (2011-10-27)
changeset 45273728ed9d28c63
parent 45272 5995ab88a00f
child 45274 252cd58847e0
respecting isabelle's programming style in the quotient package by simplifying map_lookup function for data access
src/HOL/Tools/Quotient/quotient_info.ML
src/HOL/Tools/Quotient/quotient_term.ML
     1.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Oct 27 13:50:54 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Oct 27 13:50:55 2011 +0200
     1.3 @@ -12,8 +12,7 @@
     1.4  
     1.5    type maps_info = {mapfun: string, relmap: string}
     1.6    val maps_defined: theory -> string -> bool
     1.7 -  (* FIXME functions called "lookup" must return option, not raise exception! *)
     1.8 -  val maps_lookup: theory -> string -> maps_info     (* raises NotFound *)
     1.9 +  val maps_lookup: theory -> string -> maps_info option
    1.10    val maps_update_thy: string -> maps_info -> theory -> theory
    1.11    val maps_update: string -> maps_info -> Proof.context -> Proof.context
    1.12    val print_mapsinfo: Proof.context -> unit
    1.13 @@ -28,6 +27,7 @@
    1.14  
    1.15    type qconsts_info = {qconst: term, rconst: term, def: thm}
    1.16    val transform_qconsts: morphism -> qconsts_info -> qconsts_info
    1.17 +  (* FIXME functions called "lookup" must return option, not raise exception! *)
    1.18    val qconsts_lookup: theory -> term -> qconsts_info     (* raises NotFound *)
    1.19    val qconsts_update_thy: string -> qconsts_info -> theory -> theory
    1.20    val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic
    1.21 @@ -67,13 +67,9 @@
    1.22    fun merge data = Symtab.merge (K true) data
    1.23  )
    1.24  
    1.25 -fun maps_defined thy s =
    1.26 -  Symtab.defined (MapsData.get thy) s
    1.27 +fun maps_defined thy s = Symtab.defined (MapsData.get thy) s
    1.28  
    1.29 -fun maps_lookup thy s =
    1.30 -  (case Symtab.lookup (MapsData.get thy) s of
    1.31 -    SOME map_fun => map_fun
    1.32 -  | NONE => raise NotFound)
    1.33 +fun maps_lookup thy s = Symtab.lookup (MapsData.get thy) s
    1.34  
    1.35  fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
    1.36  fun maps_update k minfo = Proof_Context.background_theory (maps_update_thy k minfo)  (* FIXME *)
     2.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Oct 27 13:50:54 2011 +0200
     2.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu Oct 27 13:50:55 2011 +0200
     2.3 @@ -63,13 +63,9 @@
     2.4    | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1
     2.5  
     2.6  fun get_mapfun ctxt s =
     2.7 -  let
     2.8 -    val thy = Proof_Context.theory_of ctxt
     2.9 -    val mapfun = #mapfun (Quotient_Info.maps_lookup thy s) handle Quotient_Info.NotFound =>
    2.10 -      raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
    2.11 -  in
    2.12 -    Const (mapfun, dummyT)
    2.13 -  end
    2.14 +  case Quotient_Info.maps_lookup (Proof_Context.theory_of ctxt) s of
    2.15 +    SOME map_data => Const (#mapfun map_data, dummyT)
    2.16 +  | NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
    2.17  
    2.18  (* makes a Free out of a TVar *)
    2.19  fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
    2.20 @@ -275,13 +271,9 @@
    2.21    Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
    2.22  
    2.23  fun get_relmap ctxt s =
    2.24 -  let
    2.25 -    val thy = Proof_Context.theory_of ctxt
    2.26 -    val relmap = #relmap (Quotient_Info.maps_lookup thy s) handle Quotient_Info.NotFound =>
    2.27 -      raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
    2.28 -  in
    2.29 -    Const (relmap, dummyT)
    2.30 -  end
    2.31 +  case Quotient_Info.maps_lookup (Proof_Context.theory_of ctxt) s of
    2.32 +    SOME map_data => Const (#relmap map_data, dummyT)
    2.33 +  | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
    2.34  
    2.35  fun mk_relmap ctxt vs rty =
    2.36    let