Nominal/Nominal2.thy
changeset 3091 578e0265b235
parent 3076 2b1b8404fe0d
child 3134 301b74fcd614
equal deleted inserted replaced
3090:19f5e7afad89 3091:578e0265b235
   524 end 
   524 end 
   525 *}
   525 *}
   526 
   526 
   527 
   527 
   528 section {* Preparing and parsing of the specification *}
   528 section {* Preparing and parsing of the specification *}
       
   529 
       
   530 ML {*
       
   531 (* adds the default sort @{sort fs} to nominal specifications *)
       
   532 
       
   533 fun augment_sort thy S = Sign.inter_sort thy (@{sort fs}, S)
       
   534 
       
   535 fun augment_sort_typ thy =
       
   536   map_type_tfree (fn (s, S) => TFree (s, augment_sort thy S))
       
   537 *}
       
   538 
   529 ML {* 
   539 ML {* 
   530 (* generates the parsed datatypes and 
   540 (* generates the parsed datatypes and declares the constructors *)
   531    declares the constructors 
       
   532 *)
       
   533 
   541 
   534 fun prepare_dts dt_strs thy = 
   542 fun prepare_dts dt_strs thy = 
   535 let
   543 let
   536   fun prep_spec ((tname, tvs, mx), constrs) =
   544   fun prep_spec ((tname, tvs, mx), constrs) =
   537     ((tname, tvs, mx), 
   545     ((tname, tvs, mx), constrs |> map (fn (c, atys, mx', _) => (c, map snd atys, mx')))
   538       constrs |> map (fn (c, Ts, mx', _) => (c, map snd Ts, mx')))
       
   539 
       
   540   fun mk_constr_trms ((tname, tvs, _), constrs) =
       
   541     let
       
   542       val full_tname = Sign.full_name thy tname
       
   543       val ty = Type (full_tname, map TFree tvs)
       
   544     in
       
   545       map (fn (c, tys, mx) => (c, (tys ---> ty), mx)) constrs
       
   546     end 
       
   547 
   546 
   548   val (dts, spec_ctxt) = 
   547   val (dts, spec_ctxt) = 
   549     Datatype.read_specs (map prep_spec dt_strs) thy
   548     Datatype.read_specs (map prep_spec dt_strs) thy
   550  
   549  
   551   val constr_trms = flat (map mk_constr_trms dts)
   550   fun augment ((tname, tvs, mx), constrs) =
   552  
   551     ((tname, map (apsnd (augment_sort thy)) tvs, mx), 
       
   552       constrs |> map (fn (c, tys, mx') => (c, map (augment_sort_typ thy) tys, mx')))
       
   553   
       
   554   val dts' = map augment dts
       
   555 
       
   556   fun mk_constr_trms ((tname, tvs, _), constrs) =
       
   557     let
       
   558       val ty = Type (Sign.full_name thy tname, map TFree tvs)
       
   559     in
       
   560       map (fn (c, tys, mx) => (c, (tys ---> ty), mx)) constrs
       
   561     end
       
   562 
       
   563   val constr_trms = flat (map mk_constr_trms dts')
       
   564   
       
   565   (* FIXME: local version *)
   553   (* val (_, spec_ctxt') = Proof_Context.add_fixes constr_trms spec_ctxt *)
   566   (* val (_, spec_ctxt') = Proof_Context.add_fixes constr_trms spec_ctxt *)
       
   567 
   554   val thy' = Sign.add_consts_i constr_trms (Proof_Context.theory_of spec_ctxt)
   568   val thy' = Sign.add_consts_i constr_trms (Proof_Context.theory_of spec_ctxt)
   555 
   569 in
   556 in
   570   (dts', thy')
   557   (dts, thy')
   571 end
   558 end
   572 *}
   559 *}
   573 
   560 
   574 ML {*
   561 ML {*
   575 (* parsing the binding function specifications and *)
   562 (* parsing the binding function specification and *)
   576 (* declaring the function constants                *)
   563 (* declaring the functions in the local theory    *)
       
   564 fun prepare_bn_funs bn_fun_strs bn_eq_strs thy =
   577 fun prepare_bn_funs bn_fun_strs bn_eq_strs thy =
   565 let
   578 let
   566   val lthy = Named_Target.theory_init thy
   579   val lthy = Named_Target.theory_init thy
   567 
   580 
   568   val ((bn_funs, bn_eqs), lthy') = 
   581   val ((bn_funs, bn_eqs), lthy') = 
   667 fun nominal_datatype2_cmd (opt_thms_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy = 
   680 fun nominal_datatype2_cmd (opt_thms_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy = 
   668 let
   681 let
   669   (* this theory is used just for parsing *)
   682   (* this theory is used just for parsing *)
   670   val thy = Proof_Context.theory_of lthy  
   683   val thy = Proof_Context.theory_of lthy  
   671 
   684 
   672   val (((dts, (bn_funs, bn_eqs)), bclauses), thy') = 
   685   val (((dts, (bn_funs, bn_eqs)), bclauses), _) = 
   673     thy
   686     thy
   674     |> prepare_dts dt_strs 
   687     |> prepare_dts dt_strs 
   675     ||>> prepare_bn_funs bn_fun_strs bn_eq_strs 
   688     ||>> prepare_bn_funs bn_fun_strs bn_eq_strs 
   676     ||>> prepare_bclauses dt_strs
   689     ||>> prepare_bclauses dt_strs
   677 
   690