src/Pure/Isar/expression.ML
changeset 49817 85b37aece3b3
parent 49749 f27c96e98672
child 49818 db42a1147986
equal deleted inserted replaced
49816:e63d6c55ad6d 49817:85b37aece3b3
   142 (* Parse positional or named instantiation *)
   142 (* Parse positional or named instantiation *)
   143 
   143 
   144 local
   144 local
   145 
   145 
   146 fun prep_inst prep_term ctxt parms (Positional insts) =
   146 fun prep_inst prep_term ctxt parms (Positional insts) =
   147       (insts ~~ parms) |> map (fn
   147       (insts ~~ parms) |> map
   148         (NONE, p) => Free (p, dummyT) |
   148         (fn (NONE, p) => Free (p, dummyT)
   149         (SOME t, _) => prep_term ctxt t)
   149           | (SOME t, _) => prep_term ctxt t)
   150   | prep_inst prep_term ctxt parms (Named insts) =
   150   | prep_inst prep_term ctxt parms (Named insts) =
   151       parms |> map (fn p => case AList.lookup (op =) insts p of
   151       parms |> map (fn p =>
   152         SOME t => prep_term ctxt t |
   152         (case AList.lookup (op =) insts p of
   153         NONE => Free (p, dummyT));
   153           SOME t => prep_term ctxt t |
       
   154           NONE => Free (p, dummyT)));
   154 
   155 
   155 in
   156 in
   156 
   157 
   157 fun parse_inst x = prep_inst Syntax.parse_term x;
   158 fun parse_inst x = prep_inst Syntax.parse_term x;
   158 fun make_inst x = prep_inst (K I) x;
   159 fun make_inst x = prep_inst (K I) x;
   284   | declare_elem _ (Notes _) ctxt = ctxt;
   285   | declare_elem _ (Notes _) ctxt = ctxt;
   285 
   286 
   286 
   287 
   287 (** Finish locale elements **)
   288 (** Finish locale elements **)
   288 
   289 
       
   290 fun finish_primitive parms _ (Fixes fixes) = Fixes (map (fn (binding, _, mx) =>
       
   291       let val x = Binding.name_of binding
       
   292       in (binding, AList.lookup (op =) parms x, mx) end) fixes)
       
   293   | finish_primitive _ _ (Constrains _) = Constrains []
       
   294   | finish_primitive _ close (Assumes asms) = close (Assumes asms)
       
   295   | finish_primitive _ close (Defines defs) = close (Defines defs)
       
   296   | finish_primitive _ _ (Notes facts) = Notes facts;
       
   297 
       
   298 local
       
   299 
   289 fun closeup _ _ false elem = elem
   300 fun closeup _ _ false elem = elem
   290   | closeup ctxt parms true elem =
   301   | closeup ctxt parms true elem =
   291       let
   302       let
   292         (* FIXME consider closing in syntactic phase -- before type checking *)
   303         (* FIXME consider closing in syntactic phase -- before type checking *)
   293         fun close_frees t =
   304         fun close_frees t =
   307             let val ((c, _), t') = Local_Defs.cert_def ctxt (close_frees t)
   318             let val ((c, _), t') = Local_Defs.cert_def ctxt (close_frees t)
   308             in ((Thm.def_binding_optional (Binding.name c) name, atts), (t', no_binds ps)) end))
   319             in ((Thm.def_binding_optional (Binding.name c) name, atts), (t', no_binds ps)) end))
   309         | e => e)
   320         | e => e)
   310       end;
   321       end;
   311 
   322 
   312 fun finish_primitive parms _ (Fixes fixes) = Fixes (map (fn (binding, _, mx) =>
   323 fun finish_elem ctxt parms do_close elem =
   313       let val x = Binding.name_of binding
   324   finish_primitive parms (closeup ctxt parms do_close) elem;
   314       in (binding, AList.lookup (op =) parms x, mx) end) fixes)
       
   315   | finish_primitive _ _ (Constrains _) = Constrains []
       
   316   | finish_primitive _ close (Assumes asms) = close (Assumes asms)
       
   317   | finish_primitive _ close (Defines defs) = close (Defines defs)
       
   318   | finish_primitive _ _ (Notes facts) = Notes facts;
       
   319 
   325 
   320 fun finish_inst ctxt (loc, (prfx, inst)) =
   326 fun finish_inst ctxt (loc, (prfx, inst)) =
   321   let
   327   let
   322     val thy = Proof_Context.theory_of ctxt;
   328     val thy = Proof_Context.theory_of ctxt;
   323     val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
   329     val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
   324     val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
   330     val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
   325   in (loc, morph) end;
   331   in (loc, morph) end;
   326 
   332 
   327 fun finish_elem ctxt parms do_close elem =
   333 in
   328   finish_primitive parms (closeup ctxt parms do_close) elem;
       
   329 
   334 
   330 fun finish ctxt parms do_close insts elems =
   335 fun finish ctxt parms do_close insts elems =
   331   let
   336   let
   332     val deps = map (finish_inst ctxt) insts;
   337     val deps = map (finish_inst ctxt) insts;
   333     val elems' = map (finish_elem ctxt parms do_close) elems;
   338     val elems' = map (finish_elem ctxt parms do_close) elems;
   334   in (deps, elems') end;
   339   in (deps, elems') end;
       
   340 
       
   341 end;
   335 
   342 
   336 
   343 
   337 (** Process full context statement: instantiations + elements + conclusion **)
   344 (** Process full context statement: instantiations + elements + conclusion **)
   338 
   345 
   339 (* Interleave incremental parsing and type inference over entire parsed stretch. *)
   346 (* Interleave incremental parsing and type inference over entire parsed stretch. *)
   426 
   433 
   427 local
   434 local
   428 
   435 
   429 fun prep_statement prep activate raw_elems raw_concl context =
   436 fun prep_statement prep activate raw_elems raw_concl context =
   430   let
   437   let
   431      val ((_, _, elems, concl), _) =
   438     val ((_, _, elems, concl), _) =
   432        prep {strict = true, do_close = false, fixed_frees = true}
   439       prep {strict = true, do_close = false, fixed_frees = true}
   433         ([], []) I raw_elems raw_concl context;
   440         ([], []) I raw_elems raw_concl context;
   434      val (_, context') = context |>
   441     val (_, context') = context
   435        Proof_Context.set_stmt true |>
   442       |> Proof_Context.set_stmt true
   436        fold_map activate elems;
   443       |> fold_map activate elems;
   437   in (concl, context') end;
   444   in (concl, context') end;
   438 
   445 
   439 in
   446 in
   440 
   447 
   441 fun cert_statement x = prep_statement cert_full_context_statement Element.activate_i x;
   448 fun cert_statement x = prep_statement cert_full_context_statement Element.activate_i x;