--- a/src/Pure/Tools/codegen_simtype.ML Tue Oct 10 09:17:24 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,85 +0,0 @@
-(* Title: Pure/Tools/codegen_simtype.ML
- ID: $Id$
- Author: Florian Haftmann, TU Muenchen
-
-Axiomatic extension of code generator: implement ("simulate") types
-by other type expressions. Requires user proof but does not use
-the proven theorems!
-*)
-
-signature CODEGEN_SIMTYPE =
-sig
-end;
-
-structure CodegenSimtype: CODEGEN_SIMTYPE =
-struct
-
-local
-
-fun gen_simtype prep_term do_proof (raw_repm, raw_absm) (raw_repi, raw_absi) raw_repe thy =
- let
- val repm = prep_term thy raw_repm;
- val absm = prep_term thy raw_absm;
- val repi = prep_term thy raw_repi;
- val absi = prep_term thy raw_absi;
- val (repe, repe_ty) = (dest_Const o prep_term thy) raw_repe;
- val repe_ty' = (snd o strip_type) repe_ty;
- fun dest_fun (Type ("fun", [ty1, ty2])) = (ty1, ty2)
- | dest_fun ty = raise TYPE ("dest_fun", [ty], []);
- val PROP = ObjectLogic.ensure_propT thy
- val (ty_abs, ty_rep) = (dest_fun o fastype_of) repm;
- val (tyco_abs, ty_parms) = dest_Type ty_abs;
- val _ = if exists (fn TFree _ => false | _ => true) ty_parms then raise TYPE ("no TFree", ty_parms, []) else ();
- val repv = Free ("x", ty_rep);
- val absv = Free ("x", ty_abs);
- val rep_mor = Logic.mk_implies
- (PROP (absi $ absv), Logic.mk_equals (absm $ (repm $ absv), absv));
- val abs_mor = Logic.mk_implies
- (PROP (repi $ repv), PROP (Const (repe, ty_rep --> ty_rep --> repe_ty') $ (repm $ (absm $ repv)) $ repv));
- val rep_inv = Logic.mk_implies
- (PROP (absi $ absv), PROP (repi $ (repm $ absv)));
- val abs_inv = Logic.mk_implies
- (PROP (repi $ repv), PROP (absi $ (absm $ repv)));
- in
- thy
- |> do_proof (K I) [rep_mor, abs_mor, rep_inv, abs_inv]
- end;
-
-fun gen_e_simtype do_proof = gen_simtype Sign.read_term do_proof;
-fun gen_i_simtype do_proof = gen_simtype Sign.cert_term do_proof;
-
-fun setup_proof after_qed props thy =
- thy
- |> ProofContext.init
- |> Proof.theorem_i PureThy.internalK NONE after_qed NONE ("", [])
- (map (fn t => (("", []), [(t, [])])) props);
-
-in
-
-val simtype = gen_e_simtype setup_proof;
-val simtype_i = gen_i_simtype setup_proof;
-
-end; (*local*)
-
-local
-
-structure P = OuterParse
-and K = OuterKeyword
-
-in
-
-val simtypeK = "code_simtype"
-
-val simtypeP =
- OuterSyntax.command simtypeK "simulate type in executable code" K.thy_goal (
- (P.term -- P.term -- P.term -- P.term -- P.term)
- >> (fn ((((raw_repm, raw_absm), raw_repi), raw_absi), raw_repe) =>
- (Toplevel.print oo Toplevel.theory_to_proof)
- (simtype (raw_repm, raw_absm) (raw_repi, raw_absi) raw_repe))
- );
-
-val _ = OuterSyntax.add_parsers [simtypeP];
-
-end; (*local*)
-
-end; (*struct*)