# HG changeset patch
# User haftmann
# Date 1160464689 -7200
# Node ID a81ce849e9f48e6b028fafa0cc4c05aefd4bf235
# Parent  041badc7fcaf6023a69578297b291a61a9708f7b
removed experimental codegen_simtype

diff -r 041badc7fcaf -r a81ce849e9f4 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Tue Oct 10 09:17:24 2006 +0200
+++ b/src/Pure/IsaMakefile	Tue Oct 10 09:18:09 2006 +0200
@@ -61,7 +61,7 @@
   Tools/codegen_names.ML	\
   Tools/class_package.ML Tools/codegen_data.ML	\
   Tools/codegen_package.ML Tools/codegen_serializer.ML				\
-  Tools/codegen_funcgr.ML Tools/codegen_simtype.ML				\
+  Tools/codegen_funcgr.ML				\
   Tools/codegen_thingol.ML Tools/compute.ML					\
   Tools/invoke.ML Tools/nbe.ML Tools/nbe_codegen.ML Tools/nbe_eval.ML		\
   Tools/xml_syntax.ML	\
diff -r 041badc7fcaf -r a81ce849e9f4 src/Pure/Tools/ROOT.ML
--- a/src/Pure/Tools/ROOT.ML	Tue Oct 10 09:17:24 2006 +0200
+++ b/src/Pure/Tools/ROOT.ML	Tue Oct 10 09:18:09 2006 +0200
@@ -14,7 +14,6 @@
 
 (*code generator, 2nd generation*)
 use "codegen_consts.ML";
-use "codegen_simtype.ML";
 use "codegen_data.ML";
 use "codegen_names.ML";
 use "codegen_funcgr.ML";
diff -r 041badc7fcaf -r a81ce849e9f4 src/Pure/Tools/codegen_simtype.ML
--- 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*)