added rudimentary instantiation stub
authorhaftmann
Sat Sep 15 19:29:29 2007 +0200 (2007-09-15)
changeset 24592dfea1edbf711
parent 24591 6509626eb2c9
child 24593 1547ea587f5a
added rudimentary instantiation stub
src/Pure/IsaMakefile
src/Pure/Isar/ROOT.ML
src/Pure/Isar/instance.ML
     1.1 --- a/src/Pure/IsaMakefile	Sat Sep 15 19:27:50 2007 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Sat Sep 15 19:29:29 2007 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4    Isar/antiquote.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML		\
     1.5    Isar/calculation.ML Isar/class.ML Isar/code.ML Isar/code_unit.ML		\
     1.6    Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML			\
     1.7 -  Isar/find_theorems.ML Isar/induct_attrib.ML Isar/isar_cmd.ML			\
     1.8 +  Isar/find_theorems.ML Isar/induct_attrib.ML Isar/instance.ML Isar/isar_cmd.ML	\
     1.9    Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML			\
    1.10    Isar/local_theory.ML Isar/locale.ML Isar/method.ML Isar/net_rules.ML		\
    1.11    Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML			\
     2.1 --- a/src/Pure/Isar/ROOT.ML	Sat Sep 15 19:27:50 2007 +0200
     2.2 +++ b/src/Pure/Isar/ROOT.ML	Sat Sep 15 19:29:29 2007 +0200
     2.3 @@ -56,6 +56,7 @@
     2.4  (*local theories and specifications*)
     2.5  use "local_theory.ML";
     2.6  use "theory_target.ML";
     2.7 +use "instance.ML";
     2.8  use "spec_parse.ML";
     2.9  use "specification.ML";
    2.10  use "constdefs.ML";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Isar/instance.ML	Sat Sep 15 19:29:29 2007 +0200
     3.3 @@ -0,0 +1,82 @@
     3.4 +(*  Title:      Pure/Isar/instance.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Florian Haftmann, TU Muenchen
     3.7 +
     3.8 +User-level instantiation interface for classes.
     3.9 +FIXME not operative for the moment
    3.10 +*)
    3.11 +
    3.12 +signature INSTANCE =
    3.13 +sig
    3.14 +  val begin_instantiation: arity list -> theory -> local_theory
    3.15 +  val begin_instantiation_cmd: (xstring * string list * string) list
    3.16 +    -> theory -> local_theory
    3.17 +  val proof_instantiation: local_theory -> Proof.state
    3.18 +end;
    3.19 +
    3.20 +structure Instance : INSTANCE =
    3.21 +struct
    3.22 +
    3.23 +structure Instantiation = ProofDataFun(
    3.24 +struct
    3.25 +  type T = ((string * (string * sort) list) * sort) list * ((string * typ) * string) list;
    3.26 +  fun init _ = ([], []);
    3.27 +end);
    3.28 +
    3.29 +local
    3.30 +
    3.31 +fun gen_begin_instantiation prep_arity raw_arities thy =
    3.32 +  let
    3.33 +    fun prep_arity' raw_arity names =
    3.34 +      let
    3.35 +        val arity as (tyco, sorts, sort) = prep_arity thy raw_arity;
    3.36 +        val (vs, names') = Name.variants (replicate (length sorts) "'a") names;
    3.37 +      in (((tyco, vs ~~ sorts), sort), names') end;
    3.38 +    val (arities, _) = fold_map prep_arity' raw_arities Name.context;
    3.39 +    fun get_param tyco ty_subst (param, (c, ty)) =
    3.40 +      ((param ^ "_" ^ NameSpace.base tyco, map_atyps (K ty_subst) ty),
    3.41 +        Class.unoverload_const thy (c, ty));
    3.42 +    fun get_params ((tyco, vs), sort) =
    3.43 +      Class.params_of_sort thy sort
    3.44 +      |> map (get_param tyco (Type (tyco, map TFree vs)));
    3.45 +    val params = maps get_params arities;
    3.46 +    val ctxt =
    3.47 +      ProofContext.init thy
    3.48 +      |> Instantiation.put (arities, params);
    3.49 +    val thy_target = TheoryTarget.begin "" ctxt;
    3.50 +    val operations = {
    3.51 +        pretty = LocalTheory.pretty,
    3.52 +        consts = LocalTheory.consts,
    3.53 +        axioms = LocalTheory.axioms,
    3.54 +        abbrev = LocalTheory.abbrev,
    3.55 +        defs = LocalTheory.defs,
    3.56 +        notes = LocalTheory.notes,
    3.57 +        type_syntax = LocalTheory.type_syntax,
    3.58 +        term_syntax = LocalTheory.term_syntax,
    3.59 +        declaration = LocalTheory.pretty,
    3.60 +        target_morphism = LocalTheory.target_morphism,
    3.61 +        target_naming = LocalTheory.target_naming,
    3.62 +        reinit = LocalTheory.reinit,
    3.63 +        exit = LocalTheory.exit
    3.64 +      };
    3.65 +  in TheoryTarget.begin "" ctxt end;
    3.66 +
    3.67 +in
    3.68 +
    3.69 +val begin_instantiation = gen_begin_instantiation Sign.cert_arity;
    3.70 +val begin_instantiation_cmd = gen_begin_instantiation Sign.read_arity;
    3.71 +
    3.72 +end;
    3.73 +
    3.74 +fun gen_proof_instantiation do_proof after_qed lthy =
    3.75 +  let
    3.76 +    val ctxt = LocalTheory.target_of lthy;
    3.77 +    val arities = case Instantiation.get ctxt
    3.78 +     of ([], _) => error "no instantiation target"
    3.79 +      | (arities, _) => map (fn ((tyco, vs), sort) => (tyco, map snd vs, sort)) arities;
    3.80 +    val thy = ProofContext.theory_of ctxt;
    3.81 +  in (do_proof after_qed arities) thy end;
    3.82 +
    3.83 +val proof_instantiation = gen_proof_instantiation Class.instance_arity I;
    3.84 +
    3.85 +end;