Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Parser.thy
changeset 1287 8557af71724e
parent 1285 e3ac56d3b7af
child 1289 02eb0f600630
equal deleted inserted replaced
1286:87894b5156f4 1287:8557af71724e 
   124 
   124 
   125 ML {*
 
   125 ML {*
 
   126 fun raw_dts_decl dt_names dts lthy =
 
   126 fun raw_dts_decl dt_names dts lthy =
 
   127 let
 
   127 let
 
   128   val thy = ProofContext.theory_of lthy
 
   128   val thy = ProofContext.theory_of lthy
 
   129   val conf = Datatype.default_config
 
       
   130 
       
   131   val dt_names' = add_raws dt_names
 
       
   132   val dt_full_names = map (Sign.full_bname thy) dt_names 
   129   val dt_full_names = map (Sign.full_bname thy) dt_names 
   133   val dts' = raw_dts dt_full_names dts
 
   130   val raw_dts = raw_dts dt_full_names dts
 
   134 in
 
   131   val raw_dt_names = add_raws dt_names
 
   135   lthy
 
   132 in
 
   136   |> Local_Theory.theory_result (Datatype.add_datatype conf dt_names' dts')
 
   133   (raw_dt_names, raw_dts)
 
   137 end 
   134 end 
   138 *}
 
   135 *}
 
   139 
   136 
   140 ML {*
 
   137 ML {*
 
   141 fun raw_bn_fun_decl dt_names dts bn_funs bn_eqs lthy =
 
   138 fun raw_bn_fun_decl dt_names dts bn_funs bn_eqs lthy =
 
   169 *}
 
   166 *}
 
   170 
   167 
   171 ML {* 
   168 ML {* 
   172 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
 
   169 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
 
   173 let
 
   170 let
 
       
   171   val conf = Datatype.default_config
 
   174   val dts_names = map (fn (_, s, _, _) => Binding.name_of s) dts
 
   172   val dts_names = map (fn (_, s, _, _) => Binding.name_of s) dts
 
       
   173 
       
   174   val (raw_dt_names, raw_dts) = raw_dts_decl dts_names dts lthy
 
       
   175 
   175 in
 
   176 in
 
   176   lthy
 
   177   lthy
 
   177   |> raw_dts_decl dts_names dts
 
   178   |> Local_Theory.theory_result (Datatype.add_datatype conf raw_dt_names raw_dts)
 
   178   ||>> raw_bn_fun_decl dts_names dts bn_funs bn_eqs
 
   179   ||>> raw_bn_fun_decl dts_names dts bn_funs bn_eqs
 
   179 end
 
   180 end
 
   180 *}
 
   181 *}
 
   181 
   182 
   182 
   183 
   240 fun find_all eq xs k' = 
   241 fun find_all eq xs k' = 
   241   maps (fn (k, v) => if eq (k, k') then [v] else []) xs
 
   242   maps (fn (k, v) => if eq (k, k') then [v] else []) xs
 
   242 *}
 
   243 *}
 
   243 
   244 
   244 ML {*
 
   245 ML {*
 
       
   246 (* associates every SOME with the index in the list *)
 
   245 fun mk_env xs =
 
   247 fun mk_env xs =
 
   246   let
 
   248   let
 
   247     fun mapp (_: int) [] = []
 
   249     fun mapp (_: int) [] = []
 
   248       | mapp i (a :: xs) = 
   250       | mapp i (a :: xs) = 
   249          case a of
 
   251          case a of
 
   254 
   256 
   255 ML {*
 
   257 ML {*
 
   256 fun env_lookup xs x =
 
   258 fun env_lookup xs x =
 
   257   case AList.lookup (op =) xs x of
 
   259   case AList.lookup (op =) xs x of
 
   258     SOME x => x
 
   260     SOME x => x
 
   259   | NONE => error ("cannot find " ^ x ^ " in the binding specification.")  
   261   | NONE => error ("cannot find " ^ x ^ " in the binding specification.");
 
   260 *}
 
   262 *}
 
       
   263 
       
   264 
   261 
   265 
   262 ML {*
 
   266 ML {*
 
   263 fun prepare_binds dt_strs lthy = 
   267 fun prepare_binds dt_strs lthy = 
   264 let
 
   268 let
 
   265   fun extract_cnstrs dt_strs =
 
   269   fun extract_annos_binds dt_strs =
 
   266     map ((map (fn (_, antys, _, bns) => (antys, bns))) o forth) dt_strs
 
   270     map ((map (fn (_, antys, _, bns) => (map fst antys, bns))) o forth) dt_strs
 
   267 
   271 
   268   fun prep_bn env bn_str =
 
   272   fun prep_bn env bn_str =
 
   269     case (Syntax.read_term lthy bn_str) of
 
   273     case (Syntax.read_term lthy bn_str) of
 
   270        Free (x, _) => (env_lookup env x, NONE)
 
   274        Free (x, _) => (env_lookup env x, NONE)
 
   271      | Const (a, T) $ Free (x, _) => (env_lookup env x, SOME (Const (a, T)))
 
   275      | Const (a, T) $ Free (x, _) => (env_lookup env x, SOME (Const (a, T)))
 
   272      | _ => error (bn_str ^ " not allowed as binding specification.");  
   276      | _ => error (bn_str ^ " not allowed as binding specification.");  
   273  
   277  
   274   fun prep_typ env (opt_name, _) = 
   278   fun prep_typ env opt_name = 
   275     case opt_name of
 
   279     case opt_name of
 
   276       NONE => []
 
   280       NONE => []
 
   277     | SOME x => find_all (op=) env x;
 
   281     | SOME x => find_all (op=) env x;
 
   278         
   282         
   279   fun prep_binds (anno_tys, bind_strs) = 
   283   (* annos - list of annotation for each type (either NONE or SOME fo a type *)
 
       
   284   
       
   285   fun prep_binds (annos, bind_strs) = 
   280   let
 
   286   let
 
   281     val env = mk_env (map fst anno_tys)
 
   287     val env = mk_env annos (* for ever label the index *)
 
   282     val binds = map (fn (x, y) => (x, prep_bn env y)) bind_strs  
   288     val binds = map (fn (x, y) => (x, prep_bn env y)) bind_strs  
   283   in
 
   289   in
 
   284     map (prep_typ binds) anno_tys
 
   290     map (prep_typ binds) annos
 
   285   end
 
   291   end
 
   286 in
 
   292 
   287   map (map prep_binds) (extract_cnstrs dt_strs)
 
   293 in
 
       
   294   map (map prep_binds) (extract_annos_binds dt_strs)
 
   288 end
 
   295 end
 
   289 *}
 
   296 *}
 
   290 
   297 
   291 ML {*
 
   298 ML {*
 
   292 fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy =
 
   299 fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy =
nominal2