src/Pure/Proof/extraction.ML
changeset 16458 4c6fd0c01d28
parent 16363 c686a606dfba
child 16486 1a12cdb6ee6b
     1.1 --- a/src/Pure/Proof/extraction.ML	Fri Jun 17 18:33:42 2005 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Fri Jun 17 18:35:27 2005 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature EXTRACTION =
     1.6  sig
     1.7 -  val set_preprocessor : (Sign.sg -> Proofterm.proof -> Proofterm.proof) -> theory -> theory
     1.8 +  val set_preprocessor : (theory -> Proofterm.proof -> Proofterm.proof) -> theory -> theory
     1.9    val add_realizes_eqns_i : ((term * term) list * (term * term)) list -> theory -> theory
    1.10    val add_realizes_eqns : string list -> theory -> theory
    1.11    val add_typeof_eqns_i : ((term * term) list * (term * term)) list -> theory -> theory
    1.12 @@ -86,9 +86,9 @@
    1.13    ({next, rs = rs1, net} : rules) ({next = next2, rs = rs2, ...} : rules) =
    1.14    foldr add_rule {next = next, rs = rs1, net = net} (rs2 \\ rs1);
    1.15  
    1.16 -fun condrew sign rules procs =
    1.17 +fun condrew thy rules procs =
    1.18    let
    1.19 -    val tsig = Sign.tsig_of sign;
    1.20 +    val tsig = Sign.tsig_of thy;
    1.21  
    1.22      fun rew tm =
    1.23        Pattern.rewrite_term tsig [] (condrew' :: procs) tm
    1.24 @@ -112,7 +112,7 @@
    1.25                (~1, map (Int.max o pairself maxidx_of_term) prems'),
    1.26               iTs = Tenv, asol = tenv};
    1.27            val env'' = Library.foldl (fn (env, p) =>
    1.28 -            Pattern.unify (sign, env, [pairself (lookup rew) p])) (env', prems')
    1.29 +            Pattern.unify (thy, env, [pairself (lookup rew) p])) (env', prems')
    1.30          in SOME (Envir.norm_term env'' (inc (ren tm2)))
    1.31          end handle Pattern.MATCH => NONE | Pattern.Unif => NONE)
    1.32            (sort (Int.compare o pairself fst)
    1.33 @@ -178,8 +178,8 @@
    1.34  
    1.35  (* data kind 'Pure/extraction' *)
    1.36  
    1.37 -structure ExtractionArgs =
    1.38 -struct
    1.39 +structure ExtractionData = TheoryDataFun
    1.40 +(struct
    1.41    val name = "Pure/extraction";
    1.42    type T =
    1.43      {realizes_eqns : rules,
    1.44 @@ -189,7 +189,7 @@
    1.45       realizers : (string list * (term * proof)) list Symtab.table,
    1.46       defs : thm list,
    1.47       expand : (string * term) list,
    1.48 -     prep : (Sign.sg -> proof -> proof) option}
    1.49 +     prep : (theory -> proof -> proof) option}
    1.50  
    1.51    val empty =
    1.52      {realizes_eqns = empty_rules,
    1.53 @@ -200,9 +200,9 @@
    1.54       expand = [],
    1.55       prep = NONE};
    1.56    val copy = I;
    1.57 -  val prep_ext = I;
    1.58 +  val extend = I;
    1.59  
    1.60 -  fun merge
    1.61 +  fun merge _
    1.62      (({realizes_eqns = realizes_eqns1, typeof_eqns = typeof_eqns1, types = types1,
    1.63         realizers = realizers1, defs = defs1, expand = expand1, prep = prep1},
    1.64        {realizes_eqns = realizes_eqns2, typeof_eqns = typeof_eqns2, types = types2,
    1.65 @@ -216,16 +216,15 @@
    1.66       expand = merge_lists expand1 expand2,
    1.67       prep = (case prep1 of NONE => prep2 | _ => prep1)};
    1.68  
    1.69 -  fun print sg (x : T) = ();
    1.70 -end;
    1.71 +  fun print _ _ = ();
    1.72 +end);
    1.73  
    1.74 -structure ExtractionData = TheoryDataFun(ExtractionArgs);
    1.75  val _ = Context.add_setup [ExtractionData.init];
    1.76  
    1.77  fun read_condeq thy =
    1.78 -  let val sg = sign_of (add_syntax thy)
    1.79 +  let val thy' = add_syntax thy
    1.80    in fn s =>
    1.81 -    let val t = Logic.varify (term_of (read_cterm sg (s, propT)))
    1.82 +    let val t = Logic.varify (term_of (read_cterm thy' (s, propT)))
    1.83      in (map Logic.dest_equals (Logic.strip_imp_prems t),
    1.84        Logic.dest_equals (Logic.strip_imp_concl t))
    1.85      end handle TERM _ => error ("Not a (conditional) meta equality:\n" ^ s)
    1.86 @@ -286,13 +285,13 @@
    1.87  fun freeze_thaw f x =
    1.88    map_term_types thaw (f (map_term_types freeze x));
    1.89  
    1.90 -fun etype_of sg vs Ts t =
    1.91 +fun etype_of thy vs Ts t =
    1.92    let
    1.93 -    val {typeof_eqns, ...} = ExtractionData.get_sg sg;
    1.94 +    val {typeof_eqns, ...} = ExtractionData.get thy;
    1.95      fun err () = error ("Unable to determine type of extracted program for\n" ^
    1.96 -      Sign.string_of_term sg t)
    1.97 -  in case strip_abs_body (freeze_thaw (condrew sg (#net typeof_eqns)
    1.98 -    [typeof_proc (Sign.defaultS sg) vs]) (list_abs (map (pair "x") (rev Ts),
    1.99 +      Sign.string_of_term thy t)
   1.100 +  in case strip_abs_body (freeze_thaw (condrew thy (#net typeof_eqns)
   1.101 +    [typeof_proc (Sign.defaultS thy) vs]) (list_abs (map (pair "x") (rev Ts),
   1.102        Const ("typeof", fastype_of1 (Ts, t) --> Type ("Type", [])) $ t))) of
   1.103        Const ("Type", _) $ u => (Logic.dest_type u handle TERM _ => err ())
   1.104      | _ => err ()
   1.105 @@ -319,28 +318,26 @@
   1.106      val rtypes = map fst types;
   1.107      val eqns = Net.merge (#net realizes_eqns, #net typeof_eqns, K false);
   1.108      val thy' = add_syntax thy;
   1.109 -    val sign = sign_of thy';
   1.110 -    val tsg = Sign.tsig_of sign;
   1.111      val rd = ProofSyntax.read_proof thy' false
   1.112    in fn (thm, (vs, s1, s2)) =>
   1.113      let
   1.114        val name = Thm.name_of_thm thm;
   1.115        val _ = assert (name <> "") "add_realizers: unnamed theorem";
   1.116 -      val prop = Pattern.rewrite_term tsg
   1.117 +      val prop = Pattern.rewrite_term (Sign.tsig_of thy')
   1.118          (map (Logic.dest_equals o prop_of) defs) [] (prop_of thm);
   1.119        val vars = vars_of prop;
   1.120        val vars' = filter_out (fn v =>
   1.121          tname_of (body_type (fastype_of v)) mem rtypes) vars;
   1.122 -      val T = etype_of sign vs [] prop;
   1.123 +      val T = etype_of thy' vs [] prop;
   1.124        val (T', thw) = Type.freeze_thaw_type
   1.125          (if T = nullT then nullT else map fastype_of vars' ---> T);
   1.126 -      val t = map_term_types thw (term_of (read_cterm sign (s1, T')));
   1.127 -      val r' = freeze_thaw (condrew sign eqns
   1.128 -        (procs @ [typeof_proc (Sign.defaultS sign) vs, rlz_proc]))
   1.129 +      val t = map_term_types thw (term_of (read_cterm thy' (s1, T')));
   1.130 +      val r' = freeze_thaw (condrew thy' eqns
   1.131 +        (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
   1.132            (Const ("realizes", T --> propT --> propT) $
   1.133              (if T = nullT then t else list_comb (t, vars')) $ prop);
   1.134        val r = foldr forall_intr r' (map (get_var_type r') vars);
   1.135 -      val prf = Reconstruct.reconstruct_proof sign r (rd s2);
   1.136 +      val prf = Reconstruct.reconstruct_proof thy' r (rd s2);
   1.137      in (name, (vs, (t, prf))) end
   1.138    end;
   1.139  
   1.140 @@ -351,15 +348,14 @@
   1.141  fun realizes_of thy vs t prop =
   1.142    let
   1.143      val thy' = add_syntax thy;
   1.144 -    val sign = sign_of thy';
   1.145      val {realizes_eqns, typeof_eqns, defs, types, ...} =
   1.146        ExtractionData.get thy';
   1.147      val procs = List.concat (map (fst o snd) types);
   1.148      val eqns = Net.merge (#net realizes_eqns, #net typeof_eqns, K false);
   1.149 -    val prop' = Pattern.rewrite_term (Sign.tsig_of sign)
   1.150 +    val prop' = Pattern.rewrite_term (Sign.tsig_of thy')
   1.151        (map (Logic.dest_equals o prop_of) defs) [] prop;
   1.152 -  in freeze_thaw (condrew sign eqns
   1.153 -    (procs @ [typeof_proc (Sign.defaultS sign) vs, rlz_proc]))
   1.154 +  in freeze_thaw (condrew thy' eqns
   1.155 +    (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
   1.156        (Const ("realizes", fastype_of t --> propT --> propT) $ t $ prop')
   1.157    end;
   1.158  
   1.159 @@ -403,7 +399,7 @@
   1.160    in
   1.161      ExtractionData.put
   1.162        {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns,
   1.163 -       types = map (apfst (Sign.intern_type (sign_of thy))) tys @ types,
   1.164 +       types = map (apfst (Sign.intern_type thy)) tys @ types,
   1.165         realizers = realizers, defs = defs, expand = expand, prep = prep} thy
   1.166    end;
   1.167  
   1.168 @@ -466,15 +462,14 @@
   1.169  
   1.170  fun extract thms thy =
   1.171    let
   1.172 -    val sg = sign_of (add_syntax thy);
   1.173 -    val tsg = Sign.tsig_of sg;
   1.174 +    val thy' = add_syntax thy;
   1.175      val {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} =
   1.176        ExtractionData.get thy;
   1.177      val procs = List.concat (map (fst o snd) types);
   1.178      val rtypes = map fst types;
   1.179 -    val typroc = typeof_proc (Sign.defaultS sg);
   1.180 -    val prep = getOpt (prep, K I) sg o ProofRewriteRules.elim_defs sg false defs o
   1.181 -      Reconstruct.expand_proof sg (("", NONE) :: map (apsnd SOME) expand);
   1.182 +    val typroc = typeof_proc (Sign.defaultS thy');
   1.183 +    val prep = getOpt (prep, K I) thy' o ProofRewriteRules.elim_defs thy' false defs o
   1.184 +      Reconstruct.expand_proof thy' (("", NONE) :: map (apsnd SOME) expand);
   1.185      val rrews = Net.merge (#net realizes_eqns, #net typeof_eqns, K false);
   1.186  
   1.187      fun find_inst prop Ts ts vs =
   1.188 @@ -485,7 +480,7 @@
   1.189  
   1.190          fun add_args ((Var ((a, i), _), t), (vs', tye)) =
   1.191            if a mem rvs then
   1.192 -            let val T = etype_of sg vs Ts t
   1.193 +            let val T = etype_of thy' vs Ts t
   1.194              in if T = nullT then (vs', tye)
   1.195                 else (a :: vs', (("'" ^ a, i), T) :: tye)
   1.196              end
   1.197 @@ -497,7 +492,7 @@
   1.198      fun find' s = map snd o List.filter (equal s o fst)
   1.199  
   1.200      fun app_rlz_rews Ts vs t = strip_abs (length Ts) (freeze_thaw
   1.201 -      (condrew sg rrews (procs @ [typroc vs, rlz_proc])) (list_abs
   1.202 +      (condrew thy' rrews (procs @ [typroc vs, rlz_proc])) (list_abs
   1.203          (map (pair "x") (rev Ts), t)));
   1.204  
   1.205      fun realizes_null vs prop = app_rlz_rews [] vs
   1.206 @@ -513,7 +508,7 @@
   1.207  
   1.208        | corr d defs vs ts Ts hs (AbsP (s, SOME prop, prf)) (AbsP (_, _, prf')) t =
   1.209            let
   1.210 -            val T = etype_of sg vs Ts prop;
   1.211 +            val T = etype_of thy' vs Ts prop;
   1.212              val u = if T = nullT then 
   1.213                  (case t of SOME u => SOME (incr_boundvars 1 u) | NONE => NONE)
   1.214                else (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE);
   1.215 @@ -537,7 +532,7 @@
   1.216                 else (case t' of SOME (u $ _) => SOME u | _ => NONE));
   1.217              val u = if not (tname_of T mem rtypes) then t else
   1.218                let
   1.219 -                val eT = etype_of sg vs Ts t;
   1.220 +                val eT = etype_of thy' vs Ts t;
   1.221                  val (r, Us') = if eT = nullT then (nullt, Us) else
   1.222                    (Bound (length Us), eT :: Us);
   1.223                  val u = list_comb (incr_boundvars (length Us') t,
   1.224 @@ -551,7 +546,7 @@
   1.225        | corr d defs vs ts Ts hs (prf1 %% prf2) (prf1' %% prf2') t =
   1.226            let
   1.227              val prop = Reconstruct.prop_of' hs prf2';
   1.228 -            val T = etype_of sg vs Ts prop;
   1.229 +            val T = etype_of thy' vs Ts prop;
   1.230              val (defs1, f, u) = if T = nullT then (defs, t, NONE) else
   1.231                (case t of
   1.232                   SOME (f $ u) => (defs, SOME f, SOME u)
   1.233 @@ -569,7 +564,7 @@
   1.234            let
   1.235              val (vs', tye) = find_inst prop Ts ts vs;
   1.236              val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye;
   1.237 -            val T = etype_of sg vs' [] prop;
   1.238 +            val T = etype_of thy' vs' [] prop;
   1.239              val defs' = if T = nullT then defs
   1.240                else fst (extr d defs vs ts Ts hs prf0)
   1.241            in
   1.242 @@ -582,7 +577,7 @@
   1.243                      val _ = msg d ("Building correctness proof for " ^ quote name ^
   1.244                        (if null vs' then ""
   1.245                         else " (relevant variables: " ^ commas_quote vs' ^ ")"));
   1.246 -                    val prf' = prep (Reconstruct.reconstruct_proof sg prop prf);
   1.247 +                    val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf);
   1.248                      val (defs'', corr_prf) =
   1.249                        corr (d + 1) defs' vs' [] [] [] prf' prf' NONE;
   1.250                      val corr_prop = Reconstruct.prop_of corr_prf;
   1.251 @@ -599,7 +594,7 @@
   1.252              | SOME rs => (case find vs' rs of
   1.253                  SOME (_, prf') => (defs', prf_subst_TVars tye' prf')
   1.254                | NONE => error ("corr: no realizer for instance of theorem " ^
   1.255 -                  quote name ^ ":\n" ^ Sign.string_of_term sg (Envir.beta_norm
   1.256 +                  quote name ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
   1.257                      (Reconstruct.prop_of (proof_combt (prf0, ts))))))
   1.258            end
   1.259  
   1.260 @@ -608,12 +603,12 @@
   1.261              val (vs', tye) = find_inst prop Ts ts vs;
   1.262              val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
   1.263            in
   1.264 -            if etype_of sg vs' [] prop = nullT andalso
   1.265 +            if etype_of thy' vs' [] prop = nullT andalso
   1.266                realizes_null vs' prop aconv prop then (defs, prf0)
   1.267              else case find vs' (Symtab.lookup_multi (realizers, s)) of
   1.268                SOME (_, prf) => (defs, prf_subst_TVars tye' prf)
   1.269              | NONE => error ("corr: no realizer for instance of axiom " ^
   1.270 -                quote s ^ ":\n" ^ Sign.string_of_term sg (Envir.beta_norm
   1.271 +                quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
   1.272                    (Reconstruct.prop_of (proof_combt (prf0, ts)))))
   1.273            end
   1.274  
   1.275 @@ -628,7 +623,7 @@
   1.276  
   1.277        | extr d defs vs ts Ts hs (AbsP (s, SOME t, prf)) =
   1.278            let
   1.279 -            val T = etype_of sg vs Ts t;
   1.280 +            val T = etype_of thy' vs Ts t;
   1.281              val (defs', t) = extr d defs vs [] (T :: Ts) (t :: hs)
   1.282                (incr_pboundvars 0 1 prf)
   1.283            in (defs',
   1.284 @@ -646,7 +641,7 @@
   1.285            let
   1.286              val (defs', f) = extr d defs vs [] Ts hs prf1;
   1.287              val prop = Reconstruct.prop_of' hs prf2;
   1.288 -            val T = etype_of sg vs Ts prop
   1.289 +            val T = etype_of thy' vs Ts prop
   1.290            in
   1.291              if T = nullT then (defs', f) else
   1.292                let val (defs'', t) = extr d defs' vs [] Ts hs prf2
   1.293 @@ -665,7 +660,7 @@
   1.294                      val _ = msg d ("Extracting " ^ quote s ^
   1.295                        (if null vs' then ""
   1.296                         else " (relevant variables: " ^ commas_quote vs' ^ ")"));
   1.297 -                    val prf' = prep (Reconstruct.reconstruct_proof sg prop prf);
   1.298 +                    val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf);
   1.299                      val (defs', t) = extr (d + 1) defs vs' [] [] [] prf';
   1.300                      val (defs'', corr_prf) =
   1.301                        corr (d + 1) defs' vs' [] [] [] prf' prf' (SOME t);
   1.302 @@ -708,7 +703,7 @@
   1.303              | SOME rs => (case find vs' rs of
   1.304                  SOME (t, _) => (defs, subst_TVars tye' t)
   1.305                | NONE => error ("extr: no realizer for instance of theorem " ^
   1.306 -                  quote s ^ ":\n" ^ Sign.string_of_term sg (Envir.beta_norm
   1.307 +                  quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
   1.308                      (Reconstruct.prop_of (proof_combt (prf0, ts))))))
   1.309            end
   1.310  
   1.311 @@ -720,7 +715,7 @@
   1.312              case find vs' (Symtab.lookup_multi (realizers, s)) of
   1.313                SOME (t, _) => (defs, subst_TVars tye' t)
   1.314              | NONE => error ("extr: no realizer for instance of axiom " ^
   1.315 -                quote s ^ ":\n" ^ Sign.string_of_term sg (Envir.beta_norm
   1.316 +                quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
   1.317                    (Reconstruct.prop_of (proof_combt (prf0, ts)))))
   1.318            end
   1.319  
   1.320 @@ -731,7 +726,7 @@
   1.321          val {prop, der = (_, prf), sign, ...} = rep_thm thm;
   1.322          val name = Thm.name_of_thm thm;
   1.323          val _ = assert (name <> "") "extraction: unnamed theorem";
   1.324 -        val _ = assert (etype_of sg vs [] prop <> nullT) ("theorem " ^
   1.325 +        val _ = assert (etype_of thy' vs [] prop <> nullT) ("theorem " ^
   1.326            quote name ^ " has no computational content")
   1.327        in (Reconstruct.reconstruct_proof sign prop prf, vs) end;
   1.328  
   1.329 @@ -739,7 +734,7 @@
   1.330        fst (extr 0 defs vs [] [] [] prf)) ([], map prep_thm thms);
   1.331  
   1.332      fun add_def (s, (vs, ((t, u), (prf, _)))) thy =
   1.333 -      (case Sign.const_type (sign_of thy) (extr_name s vs) of
   1.334 +      (case Sign.const_type thy (extr_name s vs) of
   1.335           NONE =>
   1.336             let
   1.337               val corr_prop = Reconstruct.prop_of prf;
   1.338 @@ -798,6 +793,6 @@
   1.339  
   1.340  val _ = OuterSyntax.add_parsers [realizersP, realizabilityP, typeofP, extractP];
   1.341  
   1.342 -val etype_of = etype_of o sign_of o add_syntax;
   1.343 +val etype_of = etype_of o add_syntax;
   1.344  
   1.345  end;