nominal2: comparison Nominal/Parser.thy

equal deleted inserted replaced

-:ea46a354f382
+:6a133abb7633
 ^^^^^^^^^
 the equations of the binding functions
 (Trueprop equations)
 *}
+ML {*
+*}
 text {*****************************************************}
 ML {*
 (* nominal datatype parser *)
 local
 structure P = OuterParse
 fun tuple ((x, y, z), u) = (x, y, z, u)
+fun tswap (((x, y), z), u) = (x, y, u, z)
 in
 val _ = OuterKeyword.keyword "bind"
 val anno_typ = Scan.option (P.name --| P.$$$ "::") -- P.typ
 (* binding specification *)
 (* maybe use and_list *)
 val bind_parser =
-P.enum "," ((P.$$$ "bind" |-- P.term) -- (P.$$$ "in" |-- P.name))
+P.enum "," ((P.$$$ "bind" |-- P.term) -- (P.$$$ "in" |-- P.name) >> swap)
 val constr_parser =
 P.binding -- Scan.repeat anno_typ
 (* datatype parser *)
 val dt_parser =
-(P.type_args -- P.binding -- P.opt_infix >> P.triple1) --
+(P.type_args -- P.binding -- P.opt_mixfix >> P.triple1) --
-(P.$$$ "=" |-- P.enum1 "|" (constr_parser -- bind_parser -- P.opt_mixfix >> P.triple_swap)) >> tuple
+(P.$$$ "=" |-- P.enum1 "|" (constr_parser -- bind_parser -- P.opt_mixfix >> tswap)) >> tuple
 (* function equation parser *)
 val fun_parser =
 Scan.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([],[])
 in
 lthy
 |> Local_Theory.theory_result (Datatype.add_datatype conf dt_names' dts')
 end
 *}
+ML {* Primrec.add_primrec *}
 ML {*
 fun raw_bn_fun_decl dt_names dts bn_funs bn_eqs lthy =
 let
 val thy = ProofContext.theory_of lthy
 val bn_fun_strs = get_bn_fun_strs bn_funs
 val bn_fun_strs' = add_raws bn_fun_strs
 val bn_fun_env = bn_fun_strs ~~ bn_fun_strs'
-val bn_funs' = map (fn (bn, opt_ty, mx) =>
+val bn_funs' = map (fn (bn, ty, mx) =>
-(raw_bind bn, Option.map (replace_typ (dt_full_names ~~ dt_full_names')) opt_ty, mx)) bn_funs
+(raw_bind bn, SOME (replace_typ dt_env ty), mx)) bn_funs
 val bn_eqs' = map (fn trm =>
 (Attrib.empty_binding, replace_term (ctrs_env @ bn_fun_env) dt_env trm)) bn_eqs
 in
 if null bn_eqs
 ||>> raw_bn_fun_decl dts_names dts bn_funs bn_eqs
 end
 *}
 ML {*
-fun get_constrs2 thy dts =
+fun get_constrs2 lthy dts =
 let
+val thy = ProofContext.theory_of lthy
 (* makes a full named type out of a binding with tvars applied to it *)
 fun mk_type thy bind tvrs =
 Type (Sign.full_name thy bind, map (fn s => TVar ((s, 0), [])) tvrs)
 val dts' = map (fn (tvrs, tname, _, constrs) => (mk_type thy tname tvrs, constrs)) dts
 in
 flat (map (fn (ty, constrs) => map (fn (bn, tys, mx) =>  (bn, tys ---> ty, mx)) constrs) dts')
 end
 *}
+ML {*
+fun find_all _ [] _ = []
+| find_all eq ((y, z)::xs) x =
+if eq (x, y)
+then z::find_all eq xs x
+else find_all eq xs x
+*}
+ML {*
+fun mk_env xs =
+let
+fun mapp (_: int) [] = []
+| mapp i ((a, _) :: xs) =
+case a of
+NONE => mapp (i + 1) xs
+| SOME x => (x, i) :: mapp (i + 1) xs
+in mapp 0 xs end
+fun env_lookup xs x =
+case AList.lookup (op =) xs x of
+SOME x => x
+| NONE => error ("cannot find " ^ x ^ " in the binding specification.")
+*}
 ML {*
 fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy =
 let
-val thy = ProofContext.theory_of lthy
 fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx);
 (* adding the types for parsing datatypes *)
-val lthy_tmp = lthy
+val lthy_tmp1 = lthy
 |> Local_Theory.theory (Sign.add_types (map prep_typ dt_strs))
-fun prep_cnstr lthy (((cname, atys), mx), binders) =
+(* parsing the datatypes *)
-(cname, map (Syntax.read_typ lthy o snd) atys, mx)
+val dts_prep =
+let
+fun prep_cnstr lthy (cname, anno_tys, mx, _) =
+(cname, map (Syntax.read_typ lthy o snd) anno_tys, mx)
 fun prep_dt lthy (tvs, tname, mx, cnstrs) =
 (tvs, tname, mx, map (prep_cnstr lthy) cnstrs)
+in
-(* parsing the datatypes *)
+map (prep_dt lthy_tmp1) dt_strs
-val dts_prep = map (prep_dt lthy_tmp) dt_strs
+end
 (* adding constructors for parsing functions *)
-val lthy_tmp2 = lthy_tmp
+val lthy_tmp2 = lthy_tmp1
-|> Local_Theory.theory (Sign.add_consts_i (get_constrs2 thy dts_prep))
+|> Local_Theory.theory (Sign.add_consts_i (get_constrs2 lthy dts_prep))
-val (bn_fun_aux, bn_eq_aux) = fst (Specification.read_spec bn_fun_strs bn_eq_strs lthy_tmp2)
+(* parsing the function specification *)
+val (bn_fun_prep, bn_eq_prep) =
-fun prep_bn_fun ((bn, T), mx) = (bn, SOME T, mx)
+let
+val ((bn_fun_aux, bn_eq_aux), _) = Specification.read_spec bn_fun_strs bn_eq_strs lthy_tmp2
-fun prep_bn_eq (attr, t) = t
+fun prep_bn_fun ((bn, T), mx) = (bn, T, mx)
-val bn_fun_prep = map prep_bn_fun bn_fun_aux
+fun prep_bn_eq (attr, t) = t
-val bn_eq_prep = map prep_bn_eq bn_eq_aux
+in
-in
+(map prep_bn_fun bn_fun_aux, map prep_bn_eq bn_eq_aux)
-nominal_datatype2 dts_prep bn_fun_prep bn_eq_prep lthy |> snd
+end
+(* adding functions for parsing binders *)
+val lthy_tmp3 = lthy_tmp2
+|> Local_Theory.theory (Sign.add_consts_i bn_fun_prep)
+(* parsing the binding structure *)
+val binds =
+let
+fun prep_bn env str =
+(case Syntax.read_term lthy_tmp3 str of
+Free (x, _) => (env_lookup env x, NONE)
+| Const (a, T) $ Free (x, _) => (env_lookup env x, SOME (Const (a, T)))
+| _ => error (str ^ " not allowed as binding specification."))
+fun prep_typ env (opt_name, _) =
+(case opt_name of
+NONE => []
+| SOME x => find_all (op=) env x)
+fun prep_binds (_, anno_tys, _, bind_strs) =
+let
+val env = mk_env anno_tys
+val binds = map (fn (x, y) => (x, prep_bn env y)) bind_strs
+in
+map (prep_typ binds) anno_tys
+end
+in
+map ((map prep_binds) o #4) dt_strs
+end
+val _ = tracing (PolyML.makestring binds)
+in
+nominal_datatype2 dts_prep bn_fun_prep bn_eq_prep lthy |> snd
 end
 *}
 (* Command Keyword *)
 ML {*
 let
 val kind = OuterKeyword.thy_decl
 in
 OuterSyntax.local_theory "nominal_datatype" "test" kind

changeset 1283	6a133abb7633
parent 1266	b0a120469041
child 1284	212f3ab40cc2