- exported functions etype_of and mk_typ
authorberghofe
Wed Nov 13 15:36:06 2002 +0100 (2002-11-13)
changeset 13714bdd483321f4b
parent 13713 34ef15959ce7
child 13715 61bfaa892a41
- exported functions etype_of and mk_typ
- new function realizes_of
src/Pure/Proof/extraction.ML
     1.1 --- a/src/Pure/Proof/extraction.ML	Wed Nov 13 15:35:15 2002 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Wed Nov 13 15:36:06 2002 +0100
     1.3 @@ -21,6 +21,9 @@
     1.4    val extract : thm list -> theory -> theory
     1.5    val nullT : typ
     1.6    val nullt : term
     1.7 +  val mk_typ : typ -> term
     1.8 +  val etype_of : theory -> string list -> typ list -> term -> typ
     1.9 +  val realizes_of: theory -> string list -> term -> term -> term
    1.10    val parsers: OuterSyntax.parser list
    1.11    val setup: (theory -> theory) list
    1.12  end;
    1.13 @@ -95,13 +98,14 @@
    1.14          fun ren t = if_none (Term.rename_abs tm1 tm t) t;
    1.15          val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1);
    1.16          val env as (Tenv, tenv) = Pattern.match tsig (inc tm1, tm);
    1.17 -        val prems' = map (pairself (rew o subst_vars env o inc o ren)) prems;
    1.18 +        val prems' = map (pairself (subst_vars env o inc o ren)) prems;
    1.19          val env' = Envir.Envir
    1.20            {maxidx = foldl Int.max
    1.21              (~1, map (Int.max o pairself maxidx_of_term) prems'),
    1.22 -           iTs = Vartab.make Tenv, asol = Vartab.make tenv}
    1.23 -      in Some (Envir.norm_term
    1.24 -        (Pattern.unify (sign, env', prems')) (inc (ren tm2)))
    1.25 +           iTs = Vartab.make Tenv, asol = Vartab.make tenv};
    1.26 +        val env'' = foldl (fn (env, p) =>
    1.27 +          Pattern.unify (sign, env, [pairself rew p])) (env', prems')
    1.28 +      in Some (Envir.norm_term env'' (inc (ren tm2)))
    1.29        end handle Pattern.MATCH => None | Pattern.Unif => None)
    1.30          (sort (int_ord o pairself fst)
    1.31            (Net.match_term rules (Pattern.eta_contract tm)));
    1.32 @@ -316,6 +320,20 @@
    1.33    (fn _ => fn (name, (vs, t, prf)) => (name, (vs, (t, prf))));
    1.34  val add_realizers = gen_add_realizers prep_realizer;
    1.35  
    1.36 +fun realizes_of thy vs t prop =
    1.37 +  let
    1.38 +    val thy' = add_syntax thy;
    1.39 +    val sign = sign_of thy';
    1.40 +    val {realizes_eqns, typeof_eqns, defs, ...} =
    1.41 +      ExtractionData.get thy';
    1.42 +    val eqns = Net.merge (#net realizes_eqns, #net typeof_eqns, K false);
    1.43 +    val prop' = Pattern.rewrite_term (Sign.tsig_of sign)
    1.44 +      (map (Logic.dest_equals o prop_of) defs) [] prop;
    1.45 +  in freeze_thaw
    1.46 +    (condrew sign eqns [typeof_proc (Sign.defaultS sign) vs, rlz_proc])
    1.47 +      (Const ("realizes", fastype_of t --> propT --> propT) $ t $ prop')
    1.48 +  end;
    1.49 +
    1.50  (** expanding theorems / definitions **)
    1.51  
    1.52  fun add_expand_thm (thy, thm) =
    1.53 @@ -710,6 +728,8 @@
    1.54         (Attrib.no_args add_expand_thm, K Attrib.undef_local_attribute),
    1.55         "specify theorems / definitions to be expanded during extraction")]];
    1.56  
    1.57 +val etype_of = etype_of o sign_of o add_syntax;
    1.58 +
    1.59  end;
    1.60  
    1.61  OuterSyntax.add_parsers Extraction.parsers;