make ctxt the first parameter
authorkuncar
Fri Dec 09 14:14:37 2011 +0100 (2011-12-09)
changeset 45797977cf00fb8d3
parent 45796 b2205eb270e3
child 45798 2373d86cf2e8
make ctxt the first parameter
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Quotient/quotient_def.ML
src/HOL/Tools/Quotient/quotient_term.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Dec 09 14:12:02 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Dec 09 14:14:37 2011 +0100
     1.3 @@ -720,12 +720,12 @@
     1.4    | is_rep_fun _ _ = false
     1.5  fun is_quot_abs_fun ctxt (x as (_, Type (@{type_name fun},
     1.6                                           [_, abs_T as Type (s', _)]))) =
     1.7 -    try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s'
     1.8 +    try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.AbsF) s'
     1.9      = SOME (Const x) andalso not (is_codatatype ctxt abs_T)
    1.10    | is_quot_abs_fun _ _ = false
    1.11  fun is_quot_rep_fun ctxt (x as (_, Type (@{type_name fun},
    1.12                                           [abs_T as Type (s', _), _]))) =
    1.13 -    try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s'
    1.14 +    try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.RepF) s'
    1.15      = SOME (Const x) andalso not (is_codatatype ctxt abs_T)
    1.16    | is_quot_rep_fun _ _ = false
    1.17  
     2.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Fri Dec 09 14:12:02 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Fri Dec 09 14:14:37 2011 +0100
     2.3 @@ -64,7 +64,7 @@
     2.4            else error_msg binding lhs_str
     2.5        | _ => raise Match)
     2.6  
     2.7 -    val absrep_trm = Quotient_Term.absrep_fun Quotient_Term.AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
     2.8 +    val absrep_trm = Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (fastype_of rhs, lhs_ty) $ rhs
     2.9      val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
    2.10      val (_, prop') = Local_Defs.cert_def lthy prop
    2.11      val (_, newrhs) = Local_Defs.abs_def prop'
     3.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Fri Dec 09 14:12:02 2011 +0100
     3.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Fri Dec 09 14:14:37 2011 +0100
     3.3 @@ -11,11 +11,11 @@
     3.4  
     3.5    datatype flag = AbsF | RepF
     3.6  
     3.7 -  val absrep_fun: flag -> Proof.context -> typ * typ -> term
     3.8 -  val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term
     3.9 +  val absrep_fun: Proof.context -> flag -> typ * typ -> term
    3.10 +  val absrep_fun_chk: Proof.context -> flag -> typ * typ -> term
    3.11  
    3.12    (* Allows Nitpick to represent quotient types as single elements from raw type *)
    3.13 -  val absrep_const_chk: flag -> Proof.context -> string -> term
    3.14 +  val absrep_const_chk: Proof.context -> flag -> string -> term
    3.15  
    3.16    val equiv_relation: Proof.context -> typ * typ -> term
    3.17    val equiv_relation_chk: Proof.context -> typ * typ -> term
    3.18 @@ -98,7 +98,7 @@
    3.19    end
    3.20  
    3.21  (* produces the rep or abs constant for a qty *)
    3.22 -fun absrep_const flag ctxt qty_str =
    3.23 +fun absrep_const ctxt flag qty_str =
    3.24    let
    3.25      (* FIXME *)
    3.26      fun mk_dummyT (Const (c, _)) = Const (c, dummyT)
    3.27 @@ -114,8 +114,8 @@
    3.28    end
    3.29    
    3.30  (* Lets Nitpick represent elements of quotient types as elements of the raw type *)
    3.31 -fun absrep_const_chk flag ctxt qty_str =
    3.32 -  Syntax.check_term ctxt (absrep_const flag ctxt qty_str)
    3.33 +fun absrep_const_chk ctxt flag qty_str =
    3.34 +  Syntax.check_term ctxt (absrep_const ctxt flag qty_str)
    3.35  
    3.36  fun absrep_match_err ctxt ty_pat ty =
    3.37    let
    3.38 @@ -170,26 +170,26 @@
    3.39       identity maps.
    3.40  *)
    3.41  
    3.42 -fun absrep_fun flag ctxt (rty, qty) =
    3.43 +fun absrep_fun ctxt flag (rty, qty) =
    3.44    let
    3.45      fun absrep_args tys tys' variances =
    3.46        let
    3.47          fun absrep_arg (types, (_, variant)) =
    3.48            (case variant of
    3.49              (false, false) => []
    3.50 -          | (true, false) => [(absrep_fun flag ctxt types)]
    3.51 -          | (false, true) => [(absrep_fun (negF flag) ctxt types)]
    3.52 -          | (true, true) => [(absrep_fun flag ctxt types),(absrep_fun (negF flag) ctxt types)])
    3.53 +          | (true, false) => [(absrep_fun ctxt flag types)]
    3.54 +          | (false, true) => [(absrep_fun ctxt (negF flag) types)]
    3.55 +          | (true, true) => [(absrep_fun ctxt flag types),(absrep_fun ctxt (negF flag) types)])
    3.56        in
    3.57          maps absrep_arg ((tys ~~ tys') ~~ variances)
    3.58        end
    3.59      fun test_identities tys rtys' s s' =
    3.60        let
    3.61 -        val args = map (absrep_fun flag ctxt) (tys ~~ rtys')
    3.62 +        val args = map (absrep_fun ctxt flag) (tys ~~ rtys')
    3.63        in
    3.64          if forall is_identity args
    3.65          then 
    3.66 -          absrep_const flag ctxt s'
    3.67 +          absrep_const ctxt flag s'
    3.68          else 
    3.69            raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
    3.70        end
    3.71 @@ -228,12 +228,12 @@
    3.72                    val args = absrep_args tys rtys' variances
    3.73                  in
    3.74                    if forall is_identity args
    3.75 -                  then absrep_const flag ctxt s'
    3.76 +                  then absrep_const ctxt flag s'
    3.77                    else
    3.78                      let
    3.79                        val result = list_comb (map_fun, args)
    3.80                      in
    3.81 -                      mk_fun_compose flag (absrep_const flag ctxt s', result)
    3.82 +                      mk_fun_compose flag (absrep_const ctxt flag s', result)
    3.83                      end
    3.84                  end
    3.85              end
    3.86 @@ -245,13 +245,12 @@
    3.87        | _ => raise (LIFT_MATCH "absrep_fun (default)")
    3.88    end
    3.89  
    3.90 -fun absrep_fun_chk flag ctxt (rty, qty) =
    3.91 -  absrep_fun flag ctxt (rty, qty)
    3.92 +fun absrep_fun_chk ctxt flag (rty, qty) =
    3.93 +  absrep_fun ctxt flag (rty, qty)
    3.94    |> Syntax.check_term ctxt
    3.95  
    3.96  
    3.97  
    3.98 -
    3.99  (*** Aggregate Equivalence Relation ***)
   3.100  
   3.101  
   3.102 @@ -646,7 +645,7 @@
   3.103  *)
   3.104  
   3.105  fun mk_repabs ctxt (T, T') trm =
   3.106 -  absrep_fun RepF ctxt (T, T') $ (absrep_fun AbsF ctxt (T, T') $ trm)
   3.107 +  absrep_fun ctxt RepF (T, T') $ (absrep_fun ctxt AbsF (T, T') $ trm)
   3.108  
   3.109  fun inj_repabs_err ctxt msg rtrm qtrm =
   3.110    let