# HG changeset patch # User ballarin # Date 1192006537 -7200 # Node ID 9ab032df81c8c435787faa3fb7188725e644feb5 # Parent 8f9dea697b8d5076ca28847d4813a722666788bf Prepare proper interface of interpretation_i, interpret_i. diff -r 8f9dea697b8d -r 9ab032df81c8 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Wed Oct 10 10:50:11 2007 +0200 +++ b/src/Pure/Isar/locale.ML Wed Oct 10 10:55:37 2007 +0200 @@ -2107,45 +2107,48 @@ add_local_equation x; -fun read_termT ctxt (t, T) = - Syntax.parse_term ctxt t |> TypeInfer.constrain (TypeInfer.paramify_vars T); - -fun read_instantiations ctxt parms (insts, eqns) = +fun prep_instantiations parse_term parse_prop ctxt parms (insts, eqns) = let - val thy = ProofContext.theory_of ctxt; + (* parameters *) + val (parm_names, parm_types) = parms |> split_list + ||> map (TypeInfer.paramify_vars o Logic.varifyT); + val type_parms = fold Term.add_tvarsT parm_types [] |> map TVar; + val type_parm_names = fold Term.add_tfreesT (map snd parms) [] |> map fst; (* parameter instantiations *) - val parms' = map (apsnd Logic.varifyT) parms; val d = length parms - length insts; val insts = if d < 0 then error "More arguments than parameters in instantiation." else insts @ replicate d NONE; - - val given = (parms' ~~ insts) |> map_filter - (fn (_, NONE) => NONE - | ((x, T), SOME inst) => SOME (x, (inst, T))); - val (given_ps, given_insts) = split_list given; - - (* read given insts / eqns *) - val all_vs = (map (read_termT ctxt) given_insts @ map (Syntax.read_prop ctxt) eqns) - |> Syntax.check_terms ctxt; - val ctxt' = ctxt |> fold Variable.declare_term all_vs; - val (vs, eqns') = all_vs |> chop (length given_insts); - - (* infer parameter types *) - val tyenv = fold (fn ((_, T), t) => Sign.typ_match thy (T, Term.fastype_of t)) - (given_insts ~~ vs) Vartab.empty; - val looseTs = fold (Term.add_tvarsT o Envir.typ_subst_TVars tyenv o #2) parms' []; - val (fixedTs, _) = Variable.invent_types (map #2 looseTs) ctxt'; - val tyenv' = - fold (fn ((xi, S), v) => Vartab.update_new (xi, (S, TFree v))) (looseTs ~~ fixedTs) tyenv; - - (*results*) - val instT = Vartab.fold (fn ((a, 0), (S, T)) => - if T = TFree (a, S) then I else Symtab.update (a, T)) tyenv' Symtab.empty; - val inst = Symtab.make (given_ps ~~ vs); - in ((instT, inst), eqns') end; - + val (given_ps, given_insts) = + ((parm_names ~~ parm_types) ~~ insts) |> map_filter + (fn (_, NONE) => NONE + | ((n, T), SOME inst) => SOME ((n, T), inst)) + |> split_list; + val (given_parm_names, given_parm_types) = given_ps |> split_list; + + (* prepare insts / eqns *) + val given_insts' = map (parse_term ctxt) given_insts; + val eqns' = map (parse_prop ctxt) eqns; + + (* infer types *) + val res = Syntax.check_terms ctxt + (map Logic.mk_type type_parms @ + map (uncurry TypeInfer.constrain) (given_parm_types ~~ given_insts') @ + eqns'); + val ctxt' = ctxt |> fold Variable.auto_fixes res; + + (* results *) + val (type_parms'', res') = chop (length type_parms) res; + val (given_insts'', eqns'') = chop (length given_insts) res'; + val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms''); + val inst = Symtab.make (given_parm_names ~~ given_insts''); + val standard = Variable.export_morphism ctxt' ctxt; + in ((instT, inst), eqns'') end; + + +val read_instantiations = prep_instantiations Syntax.parse_term Syntax.parse_prop; +val cert_instantiations = prep_instantiations Syntax.check_term Syntax.check_prop; fun gen_prep_registration mk_ctxt test_reg activate prep_attr prep_expr prep_insts @@ -2227,11 +2230,19 @@ val prep_global_registration = gen_prep_global_registration Attrib.intern_src intern_expr read_instantiations; +(* FIXME: NEW +val prep_global_registration_i = gen_prep_global_registration + (K I) (K I) cert_instantiations; +*) val prep_global_registration_i = gen_prep_global_registration (K I) (K I) ((K o K) I); val prep_local_registration = gen_prep_local_registration Attrib.intern_src intern_expr read_instantiations; +(* FIXME: NEW +val prep_local_registration_i = gen_prep_local_registration + (K I) (K I) cert_instantiations; +*) val prep_local_registration_i = gen_prep_local_registration (K I) (K I) ((K o K) I);