# HG changeset patch
# User haftmann
# Date 1189877369 -7200
# Node ID dfea1edbf711ba1521ad4043c289806c0f176232
# Parent  6509626eb2c953c5eb5e31e863486082b28c3693
added rudimentary instantiation stub

diff -r 6509626eb2c9 -r dfea1edbf711 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Sat Sep 15 19:27:50 2007 +0200
+++ b/src/Pure/IsaMakefile	Sat Sep 15 19:29:29 2007 +0200
@@ -35,7 +35,7 @@
   Isar/antiquote.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML		\
   Isar/calculation.ML Isar/class.ML Isar/code.ML Isar/code_unit.ML		\
   Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML			\
-  Isar/find_theorems.ML Isar/induct_attrib.ML Isar/isar_cmd.ML			\
+  Isar/find_theorems.ML Isar/induct_attrib.ML Isar/instance.ML Isar/isar_cmd.ML	\
   Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML			\
   Isar/local_theory.ML Isar/locale.ML Isar/method.ML Isar/net_rules.ML		\
   Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML			\
diff -r 6509626eb2c9 -r dfea1edbf711 src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Sat Sep 15 19:27:50 2007 +0200
+++ b/src/Pure/Isar/ROOT.ML	Sat Sep 15 19:29:29 2007 +0200
@@ -56,6 +56,7 @@
 (*local theories and specifications*)
 use "local_theory.ML";
 use "theory_target.ML";
+use "instance.ML";
 use "spec_parse.ML";
 use "specification.ML";
 use "constdefs.ML";
diff -r 6509626eb2c9 -r dfea1edbf711 src/Pure/Isar/instance.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/instance.ML	Sat Sep 15 19:29:29 2007 +0200
@@ -0,0 +1,82 @@
+(*  Title:      Pure/Isar/instance.ML
+    ID:         $Id$
+    Author:     Florian Haftmann, TU Muenchen
+
+User-level instantiation interface for classes.
+FIXME not operative for the moment
+*)
+
+signature INSTANCE =
+sig
+  val begin_instantiation: arity list -> theory -> local_theory
+  val begin_instantiation_cmd: (xstring * string list * string) list
+    -> theory -> local_theory
+  val proof_instantiation: local_theory -> Proof.state
+end;
+
+structure Instance : INSTANCE =
+struct
+
+structure Instantiation = ProofDataFun(
+struct
+  type T = ((string * (string * sort) list) * sort) list * ((string * typ) * string) list;
+  fun init _ = ([], []);
+end);
+
+local
+
+fun gen_begin_instantiation prep_arity raw_arities thy =
+  let
+    fun prep_arity' raw_arity names =
+      let
+        val arity as (tyco, sorts, sort) = prep_arity thy raw_arity;
+        val (vs, names') = Name.variants (replicate (length sorts) "'a") names;
+      in (((tyco, vs ~~ sorts), sort), names') end;
+    val (arities, _) = fold_map prep_arity' raw_arities Name.context;
+    fun get_param tyco ty_subst (param, (c, ty)) =
+      ((param ^ "_" ^ NameSpace.base tyco, map_atyps (K ty_subst) ty),
+        Class.unoverload_const thy (c, ty));
+    fun get_params ((tyco, vs), sort) =
+      Class.params_of_sort thy sort
+      |> map (get_param tyco (Type (tyco, map TFree vs)));
+    val params = maps get_params arities;
+    val ctxt =
+      ProofContext.init thy
+      |> Instantiation.put (arities, params);
+    val thy_target = TheoryTarget.begin "" ctxt;
+    val operations = {
+        pretty = LocalTheory.pretty,
+        consts = LocalTheory.consts,
+        axioms = LocalTheory.axioms,
+        abbrev = LocalTheory.abbrev,
+        defs = LocalTheory.defs,
+        notes = LocalTheory.notes,
+        type_syntax = LocalTheory.type_syntax,
+        term_syntax = LocalTheory.term_syntax,
+        declaration = LocalTheory.pretty,
+        target_morphism = LocalTheory.target_morphism,
+        target_naming = LocalTheory.target_naming,
+        reinit = LocalTheory.reinit,
+        exit = LocalTheory.exit
+      };
+  in TheoryTarget.begin "" ctxt end;
+
+in
+
+val begin_instantiation = gen_begin_instantiation Sign.cert_arity;
+val begin_instantiation_cmd = gen_begin_instantiation Sign.read_arity;
+
+end;
+
+fun gen_proof_instantiation do_proof after_qed lthy =
+  let
+    val ctxt = LocalTheory.target_of lthy;
+    val arities = case Instantiation.get ctxt
+     of ([], _) => error "no instantiation target"
+      | (arities, _) => map (fn ((tyco, vs), sort) => (tyco, map snd vs, sort)) arities;
+    val thy = ProofContext.theory_of ctxt;
+  in (do_proof after_qed arities) thy end;
+
+val proof_instantiation = gen_proof_instantiation Class.instance_arity I;
+
+end;