diff --git a/thys/Generic_Deriving/derive.ML b/thys/Generic_Deriving/derive.ML --- a/thys/Generic_Deriving/derive.ML +++ b/thys/Generic_Deriving/derive.ML @@ -1,926 +1,926 @@ open Derive_Util signature DERIVE = sig (* Adds functions that convert to and from a product-sum representation *) val define_prod_sum_conv : type_info -> bool -> Proof.context -> (Function_Common.info * Function_Common.info * Proof.context) (* define product-sum-representation type synonym *) val define_rep_type : string list -> ctr_info -> bool -> local_theory -> rep_type_info * local_theory (* define Mu-combinator type *) val define_combinator_type : string list -> (typ * class list) list -> rep_type_info -> local_theory -> comb_type_info option * local_theory (* instantiate a typeclass *) val generate_instance : string -> sort -> bool -> theory -> Proof.state val add_inst_info : string -> string -> thm list -> theory -> theory end structure Derive : DERIVE = struct fun get_type_info thy tname constr_names = Symreltab.lookup (Type_Data.get thy) (tname, Bool.toString constr_names) fun get_class_info thy classname = Symtab.lookup (Class_Data.get thy) classname fun get_inst_info thy classname tname = Symreltab.lookup (Instance_Data.get thy) (classname, tname) fun add_params_cl_info (cl_info : class_info) params = {classname = (#classname cl_info), class = (#class cl_info), params = SOME params, class_law = (#class_law cl_info), class_law_const = (#class_law_const cl_info), ops = (#ops cl_info), transfer_law = (#transfer_law cl_info), axioms = (#axioms cl_info), axioms_def = (#axioms_def cl_info), class_def = (#class_def cl_info), equivalence_thm = (#equivalence_thm cl_info)} fun mk_inst_info defs = {defs = defs} fun add_equivalence_cl_info (cl_info : class_info) equivalence_thm = {classname = (#classname cl_info), class = (#class cl_info), params = (#params cl_info), class_law = (#class_law cl_info), class_law_const = (#class_law_const cl_info), ops = (#ops cl_info), transfer_law = (#transfer_law cl_info), axioms = (#axioms cl_info), axioms_def = (#axioms_def cl_info), class_def = (#class_def cl_info), equivalence_thm = SOME equivalence_thm} fun make_rep T lthy conv_func (btype,bname) = let val term = case btype of (TFree _) => conv_func $ (Free (bname, T)) | (Type (_, _)) => if is_polymorphic btype then (get_mapping_function lthy btype) $ conv_func $ (Free (bname, dummyT)) else Free (bname, btype) | _ => Free (bname, btype) in hd (Type_Infer_Context.infer_types lthy [term]) end fun from_rep T lthy conv_func inner_term = let val term = case T of (TFree _) => conv_func $ inner_term | (Type (_, _)) => if is_polymorphic T then (get_mapping_function lthy T) $ conv_func $ inner_term else inner_term | _ => inner_term in hd (Type_Infer_Context.infer_types lthy [term]) end (* Generate instance for Mu-combinator type *) fun instantiate_combinator_type (ty_info : type_info) (cl_info : class_info) constr_names lthy = let val tname = #tname ty_info val ctr_type = #rep_type_instantiated (the (#comb_info ty_info)) val rep_type = #rep_type (#rep_info ty_info) val comb_type_name = #combname (the (#comb_info ty_info)) val comb_type_name_full = #combname_full (the (#comb_info ty_info)) val class = #class cl_info val params = the (#params cl_info) val sum_type_name = if constr_names then \<^type_name>\Tagged_Prod_Sum.sum\ else \<^type_name>\Sum_Type.sum\ val prod_type_name = if constr_names then \<^type_name>\Tagged_Prod_Sum.prod\ else \<^type_name>\Product_Type.prod\ val _ = ("Generating instance for type " ^ quote comb_type_name) |> writeln fun define_modular_sum_prod def vars opname opT opT_var is_sum lthy = let fun get_tvars vars = if null vars then ((TVar (("'a",0),class)),(TVar (("'b",0),class))) else let val var = hd vars val varTname = if is_typeT var then var |> dest_Type |> fst else "" in if is_sum then (if varTname = sum_type_name then var |> dest_Type |> snd |> (fn Ts => (hd Ts, hd (tl Ts))) else get_tvars ((var |> dest_Type |> snd)@(tl vars))) else (if varTname = prod_type_name then var |> dest_Type |> snd |> (fn Ts => (hd Ts, hd (tl Ts))) else get_tvars ((var |> dest_Type |> snd)@(tl vars))) end fun replace_tfree tfree replacement T = if T = tfree then replacement else T fun replace_op_call opname T replacement t = if t = Const (opname,T) then replacement else t fun is_TFree (TFree _) = true | is_TFree _ = false fun remove_constraints T = if is_TFree T then dest_TFree T |> apsnd (K \<^sort>\type\) |> TFree else T val varTs = map (dest_Var #> snd) vars val (left,right) = get_tvars (varTs @ [strip_type opT_var |> snd]) val op_tfree = Term.add_tfreesT opT [] |> hd |> TFree val left_opT = map_atyps (replace_tfree op_tfree left) opT val right_opT = map_atyps (replace_tfree op_tfree right) opT val opname_left = (Long_Name.base_name opname) ^ "_left" val opname_right = (Long_Name.base_name opname) ^ "_right" val var_left = (Var ((opname_left,0),left_opT)) val var_right = (Var ((opname_right,0),right_opT)) val def_left = map_aterms (replace_op_call opname left_opT var_left) def val def_right = map_aterms (replace_op_call opname right_opT var_right) def_left val return_type = strip_type opT_var |> snd val def_name = (Long_Name.base_name opname) ^ (if is_sum then "_sum_modular" else "_prod_modular") val eq_head = Free (def_name, ([left_opT,right_opT]@varTs) ---> return_type) |> Logic.unvarify_types_global val args = map Logic.unvarify_global ([var_left,var_right] @ vars) val eq = HOLogic.Trueprop $ HOLogic.mk_eq ((list_comb (eq_head,args)), Logic.unvarify_global def_right) val eq' = map_types (map_atyps remove_constraints) eq val ((_,(_,def_thm)),lthy') = Specification.definition NONE [] [] ((Binding.empty, []), eq') lthy val left = left |> dest_TVar |> (fn ((s,_),_) => TFree (s,\<^sort>\type\)) val right = right |> dest_TVar |> (fn ((s,_),_) => TFree (s,\<^sort>\type\)) val def_const = Thm.hyps_of def_thm |> hd |> Logic.dest_equals |> snd val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy') val def_thm = singleton (Proof_Context.export lthy' ctxt_thy) def_thm in (left,right,def_const,def_thm,lthy') end fun op_instance opname opT T = let fun replace_tfree tfree replacement T = if T = tfree then replacement else T val op_tfree = Term.add_tfreesT opT [] |> hd |> TFree val opT_new = map_atyps (replace_tfree op_tfree T) opT in Const (opname,opT_new) end fun sum_prod_instance term lvar rvar lT rT = let fun replace_vars var1 var2 replacement1 replacement2 T = if T = var1 then replacement1 else if T = var2 then replacement2 else T in map_types (map_atyps (replace_vars lvar rvar lT rT)) term end fun define_modular_instance T (lvs,rvs,sum_term) (lvp,rvp,prod_term) opname opT = if is_typeT T then let val (tname,Ts) = dest_Type T in if tname = sum_type_name then (sum_prod_instance sum_term lvs rvs (hd Ts) (hd (tl Ts))) $ (define_modular_instance (hd Ts) (lvs,rvs,sum_term) (lvp,rvp,prod_term) opname opT) $ (define_modular_instance (hd (tl Ts)) (lvs,rvs,sum_term) (lvp,rvp,prod_term) opname opT) else if tname = prod_type_name then (sum_prod_instance prod_term lvp rvp (hd Ts) (hd (tl Ts))) $ (define_modular_instance (hd Ts) (lvs,rvs,sum_term) (lvp,rvp,prod_term) opname opT) $ (define_modular_instance (hd (tl Ts)) (lvs,rvs,sum_term) (lvp,rvp,prod_term) opname opT) else (op_instance opname opT T) end else (op_instance opname opT T) fun change_constraints constrT term = let val constraint = Term.add_tfreesT constrT [] |> hd |> snd val unconstr_tfrees = Term.add_tfrees term [] |> map TFree val constr_names = Name.invent_names (Variable.names_of lthy) "a" (replicate (length unconstr_tfrees) constraint) val constr_tfrees = map TFree constr_names in subst_atomic_types (unconstr_tfrees ~~ constr_tfrees) term end fun define_operation_rec T (opname,t) lthy = let fun get_comb_params [] = [] | get_comb_params (ty::tys) = (case ty of Type (n,tys') => if n = comb_type_name_full then tys' else get_comb_params (tys@tys') | _ => get_comb_params tys) fun make_arg inConst ctr_type x = let val T = dest_Free x |> snd in if T = ctr_type then inConst $ x else (x |> dest_Free |> apsnd (K dummyT) |> Free) end val short_opname = Long_Name.base_name opname val fun_name = short_opname ^ "_" ^ comb_type_name val prod_def_name = short_opname ^ "_prod_def" val prod_thm = Proof_Context.get_thm lthy prod_def_name val prod_hd = (Thm.full_prop_of prod_thm) |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst val prod_const = prod_hd |> combs_to_list |> hd val prod_opT = prod_const |> dest_Const |> snd val prod_vars_raw = prod_hd |> combs_to_list |> tl val prod_def = (Thm.full_prop_of prod_thm) |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd val (lvp,rvp,prod_def_term,prod_def_thm,lthy') = define_modular_sum_prod prod_def prod_vars_raw opname t prod_opT false lthy val sum_def_name = short_opname ^ "_sum_def" val sum_thm = Proof_Context.get_thm lthy sum_def_name val sum_hd = (Thm.full_prop_of sum_thm) |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst val sum_const = sum_hd |> combs_to_list |> hd val sum_opT = sum_const |> dest_Const |> snd val sum_vars_raw = sum_hd |> combs_to_list |> tl val sum_def = (Thm.full_prop_of sum_thm) |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd val (lvs,rvs,sum_def_term,sum_def_thm,lthy'') = define_modular_sum_prod sum_def sum_vars_raw opname t sum_opT true lthy' val (binders, body) = (strip_type t) val tvar = get_tvar (body :: binders) val comb_params = get_comb_params [ctr_type] val T_params = dest_Type T |> snd val ctr_type' = typ_subst_atomic (comb_params ~~ T_params) ctr_type val body' = typ_subst_atomic [(tvar,dummyT)] body val binders' = map (typ_subst_atomic [(tvar,ctr_type')]) binders val opT = (replicate (length binders) dummyT) ---> body' val vars = (Name.invent_names (Variable.names_of lthy) "x" binders') val xs = map Free vars val inConst_name = Long_Name.qualify comb_type_name_full "In" val inConst = Const (inConst_name, ctr_type' --> dummyT) val xs_lhs = map (make_arg inConst ctr_type') xs val modular_instance = define_modular_instance rep_type (lvs,rvs,sum_def_term) (lvp,rvp,prod_def_term) opname t val xs_modular = map (apsnd (K dummyT) #> Free) vars val modular_folded_name = short_opname ^ "_modular_folded" val modularT = typ_subst_atomic [(tvar,rep_type)] t val modular_instance_eq = HOLogic.Trueprop $ HOLogic.mk_eq (Free (modular_folded_name, modularT),modular_instance) val modular_eq_constr = change_constraints t modular_instance_eq val ((_,(_,modular_folded_thm)),lthy''') = Specification.definition NONE [] [] ((Binding.empty, []), modular_eq_constr) lthy'' val modular_unfolded = Local_Defs.unfold lthy''' [prod_def_thm,sum_def_thm] modular_folded_thm |> Thm.full_prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd |> map_types (K dummyT) val lhs = list_comb (Free (fun_name, opT), xs_lhs) val rhs = if is_polymorphic body then inConst $ list_comb (modular_unfolded,xs_modular) else list_comb (modular_unfolded,xs_modular) val eq = HOLogic.Trueprop $ HOLogic.mk_eq (lhs, rhs) in if xs = [] then Specification.definition NONE [] [] ((Binding.empty, []), eq) lthy |> snd else if constr_names then Function.add_function [(Binding.name fun_name, NONE, NoSyn)] [((Binding.empty_atts, eq), [], [])] Function_Fun.fun_config (fn ctxt => Pat_Completeness.pat_completeness_tac ctxt 1 THEN auto_tac ctxt) lthy |> snd |> tagged_function_termination_tac |> snd else Function_Fun.add_fun [(Binding.name fun_name, NONE, NoSyn)] [((Binding.empty_atts, eq), [], [])] Function_Fun.fun_config lthy end fun instantiate_comb_type lthy = let - val thy = Named_Target.exit lthy + val thy = Local_Theory.exit_global lthy val (T,xs) = Derive_Util.typ_and_vs_of_typname thy comb_type_name_full class val filtered_params = params |> filter (fn (c,_) => not_instantiated thy comb_type_name_full c andalso not_instantiated thy tname c) fun define_operations_rec_aux _ [] lthy = lthy | define_operations_rec_aux ty (p::ps) lthy = define_operations_rec_aux ty ps (define_operation_rec ty p lthy) in Class.instantiation ([comb_type_name_full], xs, class) thy |> (define_operations_rec_aux T (map snd filtered_params)) end in instantiate_comb_type lthy end fun define_operation lthy tname T (opname,t) = let val from_name = "from_" ^ Long_Name.base_name tname val from_term = (Proof_Context.read_const {proper = true, strict = true} lthy from_name) |> dest_Const |> fst val from_func = Const (from_term, dummyT) val to_name = "to_" ^ Long_Name.base_name tname val to_term = (Proof_Context.read_const {proper = true, strict = true} lthy to_name) |> dest_Const |> fst val to_func = Const (to_term, dummyT) val (binders, body) = (strip_type t) val tvar = get_tvar (body :: binders) val body' = typ_subst_atomic [(tvar,dummyT)] body val binders' = map (typ_subst_atomic [(tvar,T)]) binders val newT = binders' ---> body' val vars = (Name.invent_names (Variable.names_of lthy) "x" binders') val names = map fst vars val xs = map Free vars val lhs = list_comb (Const (opname, newT), xs) val rhs_inner = list_comb (Const (opname, dummyT), map (make_rep T lthy from_func) (binders ~~ names)) val rhs = from_rep body lthy to_func rhs_inner val eq = HOLogic.Trueprop $ HOLogic.mk_eq (lhs, rhs) val ((_,(_,thm)),lthy') = (Specification.definition NONE [] [] ((Binding.empty, []), eq) lthy) in (thm,lthy') end fun define_operations ps ty lthy = let fun define_operations_aux [] _ thms lthy = (thms,lthy) | define_operations_aux (p::ps) (tname,T) thms lthy = if not_instantiated (Proof_Context.theory_of lthy) tname (fst p) then let val (thm,lthy') = define_operation lthy tname T (snd p) in define_operations_aux ps (tname,T) (thm :: thms) lthy' end else let val params = #defs (the_default {defs=[]} (get_inst_info (Proof_Context.theory_of lthy) (fst p) tname)) val names = map (Thm.full_prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst #> strip_comb #> fst #> dest_Const #> fst) params val thm = the (AList.lookup (op =) (names ~~ params) (fst (snd p))) in define_operations_aux ps (tname,T) (thm :: thms) lthy end in define_operations_aux ps ty [] lthy end fun abstract_over_vars vars t = let val varnames = map dest_Free vars |> map fst val varmapping = varnames ~~ (List.tabulate (length vars, I)) val increment_bounds = map (fn (v,n) => (v,n + 1)) fun insert_bounds varmapping (Free (s,T)) = (case AList.lookup (op =) varmapping s of NONE => Free (s,T) | SOME i => Bound i) | insert_bounds varmapping (Abs (x,T,t)) = Abs (x,T,insert_bounds (increment_bounds varmapping) t) | insert_bounds varmapping (s $ t) = (insert_bounds varmapping s) $ (insert_bounds varmapping t) | insert_bounds _ t = t fun abstract [] t = insert_bounds varmapping t | abstract (x::xs) t = (Const (\<^const_name>\Pure.all\,dummyT)) $ (Abs (x, dummyT, abstract xs t)) in if null vars then t else (abstract varnames t) end (* Adds functions that convert a type to and from its product-sum representation *) fun define_prod_sum_conv (ty_info : type_info) constr_names lthy = let val tnames = #mutual_tnames ty_info val Ts = #mutual_Ts ty_info val ctrs = #mutual_ctrs ty_info val sels = #mutual_sels ty_info val is_recursive = #is_rec ty_info val is_mutually_recursive = #is_mutually_rec ty_info val _ = map (fn tyco => "Generating conversions for type " ^ quote tyco) tnames |> cat_lines |> writeln (* Functions to deal with tagged products and sums *) val str_optT = \<^typ>\string option\ val none_str_opt = Const (\<^const_name>\None\, str_optT) fun some_str s = Const (\<^const_name>\Some\, \<^typ>\string\ --> str_optT) $ HOLogic.mk_string s val dummy_str_opt = (Term.dummy_pattern \<^typ>\string option\) val sum_type_name = if constr_names then \<^type_name>\Tagged_Prod_Sum.sum\ else \<^type_name>\Sum_Type.sum\ val prod_type_name = if constr_names then \<^type_name>\Tagged_Prod_Sum.prod\ else \<^type_name>\Product_Type.prod\ val prod_constr_name = if constr_names then \<^const_name>\Tagged_Prod_Sum.Prod\ else \<^const_name>\Product_Type.Pair\ val inl_constr_name = if constr_names then \<^const_name>\Tagged_Prod_Sum.Inl\ else \<^const_name>\Sum_Type.Inl\ val inr_constr_name = if constr_names then \<^const_name>\Tagged_Prod_Sum.Inr\ else \<^const_name>\Sum_Type.Inr\ fun mk_tagged_prodT (T1, T2) = Type (prod_type_name, [T1, T2]) fun mk_tagged_sumT LT RT = Type (sum_type_name, [LT, RT]) fun tagged_pair_const T1 T2 = Const (prod_constr_name, str_optT --> str_optT --> T1 --> T2 --> mk_tagged_prodT (T1, T2)); fun mk_tagged_prod ((t1,s1), (t2,s2)) = let val T1 = fastype_of t1 val T2 = fastype_of t2 val S1 = if s1 = "" then none_str_opt else some_str s1 val S2 = if s2 = "" then none_str_opt else some_str s2 in (tagged_pair_const T1 T2 $ S1 $ S2 $ t1 $ t2,"") end fun mk_tagged_prod_dummy (t1, t2) = let val T1 = fastype_of t1 and T2 = fastype_of t2 in tagged_pair_const T1 T2 $ dummy_str_opt $ dummy_str_opt $ t1 $ t2 end fun Inl_const LT RT = if constr_names then Const (inl_constr_name, str_optT --> LT --> mk_tagged_sumT LT RT) else BNF_FP_Util.Inl_const LT RT fun mk_tagged_Inl n RT t = Inl_const (fastype_of t) RT $ n $ t fun Inr_const LT RT = if constr_names then Const (inr_constr_name, str_optT --> RT --> mk_tagged_sumT LT RT) else BNF_FP_Util.Inr_const LT RT fun mk_tagged_tuple _ [] = HOLogic.unit | mk_tagged_tuple sels ts = fst (foldr1 mk_tagged_prod (ts ~~ sels)) fun mk_tagged_tuple_dummy [] = HOLogic.unit | mk_tagged_tuple_dummy ts = foldr1 mk_tagged_prod_dummy ts fun add_dummy_patterns (c $ _) = c $ dummy_str_opt | add_dummy_patterns t = t (* simple version for non-recursive types *) fun generate_conversion_eqs lthy prefix ((tyco,ctrs),T) sels = let fun mk_prod_listT [] = HOLogic.unitT | mk_prod_listT [x] = x | mk_prod_listT (x::xs) = mk_tagged_prodT (x, (mk_prod_listT xs)) fun generate_sum_prodT [] = HOLogic.unitT | generate_sum_prodT [x] = mk_prod_listT x | generate_sum_prodT (x::xs) = let val l = mk_prod_listT x val r = generate_sum_prodT xs in mk_tagged_sumT l r end fun generate_conversion_eq lthy prefix (cN, Ts) sels tail_ctrs = let val c = Const (cN, Ts ---> T) val sels = if null sels then replicate (length Ts) "" else sels val cN_opt = Const (\<^const_name>\Some\, \<^typ>\string\ --> str_optT) $ HOLogic.mk_string (Long_Name.base_name cN) val xs = map Free (Name.invent_names (Variable.names_of lthy) "x" Ts) val conv_inner = case tail_ctrs of [] => if constr_names then mk_tagged_tuple sels xs else HOLogic.mk_tuple xs | _ => if constr_names then mk_tagged_Inl cN_opt (generate_sum_prodT tail_ctrs) (mk_tagged_tuple sels xs) else BNF_FP_Util.mk_Inl (generate_sum_prodT tail_ctrs) (HOLogic.mk_tuple xs) val prefix = case tail_ctrs of [] => if constr_names andalso (not (HOLogic.is_unit (hd prefix))) then (let val (butlast,last) = split_last prefix in butlast @ [last |> dest_comb |> fst |> (fn t => t $ cN_opt)] end) else prefix | _ => prefix val conv = if HOLogic.is_unit (hd prefix) then conv_inner else Library.foldr (op $) (prefix,conv_inner) val conv_dummy = if constr_names then (let val conv_inner = case tail_ctrs of [] => mk_tagged_tuple sels xs| _ => mk_tagged_Inl (Term.dummy_pattern \<^typ>\string option\) (generate_sum_prodT tail_ctrs) (mk_tagged_tuple_dummy xs) in (if HOLogic.is_unit (hd prefix) then conv_inner else Library.foldr (op $) ((map add_dummy_patterns prefix), conv_inner)) end) else conv val lhs_from = (Free ("from_" ^ (Long_Name.base_name tyco), dummyT)) $ list_comb (c, xs) val lhs_to = (Free ("to_" ^ (Long_Name.base_name tyco), dummyT)) $ conv_dummy in (abstract_over_vars xs (HOLogic.Trueprop $ ((HOLogic.eq_const dummyT) $ lhs_from $ conv)), abstract_over_vars xs (HOLogic.Trueprop $ ((HOLogic.eq_const dummyT) $ lhs_to $ list_comb(c,xs)))) end in case ctrs of [] => ([],[]) | (c::cs) => let val s = if null sels then replicate (length (snd c)) "" else hd sels val ss = if null sels then [] else tl sels val new_prefix = if HOLogic.is_unit (hd prefix) then if constr_names then [(Inr_const (generate_sum_prodT [(snd c)]) (generate_sum_prodT (map snd cs))) $ Const (\<^const_name>\None\, str_optT)] else [(BNF_FP_Util.Inr_const (generate_sum_prodT [(snd c)]) (generate_sum_prodT (map snd cs)))] else prefix @ (if constr_names then [(Inr_const (generate_sum_prodT [(snd c)]) (generate_sum_prodT (map snd cs))) $ Const (\<^const_name>\None\, str_optT)] else [(BNF_FP_Util.Inr_const (generate_sum_prodT [(snd c)]) (generate_sum_prodT (map snd cs)))]) val (from_eq,to_eq) = generate_conversion_eq lthy prefix c s (map snd cs) val (from_eqs,to_eqs) = generate_conversion_eqs lthy new_prefix ((tyco,cs),T) ss in (from_eq :: from_eqs, to_eq :: to_eqs) end end (* version for recursive types *) fun generate_conversion_eqs_rec lthy Ts comb_type (((tyco,ctrs),T),prefix) sels = let fun replace_type_with_comb T = case List.find (fn x => x = T) Ts of NONE => T | _ => comb_type fun mk_prod_listT [] = HOLogic.unitT | mk_prod_listT [x] = replace_type_with_comb x | mk_prod_listT (x::xs) = mk_tagged_prodT (replace_type_with_comb x, (mk_prod_listT xs)) fun generate_sum_prodT [] = HOLogic.unitT | generate_sum_prodT [x] = mk_prod_listT x | generate_sum_prodT (x::xs) = let val l = mk_prod_listT x val r = generate_sum_prodT xs in mk_tagged_sumT l r end fun generate_conversion_eq lthy prefix (cN, Ts) sels tail_ctrs = let fun get_type_name T = case T of Type (s,_) => s | _ => "" fun find_type T tycos = List.find (fn x => x = (get_type_name T) andalso x <> "") tycos fun mk_comb_type v = Free (v |> dest_Free |> fst,comb_type) fun from_const tyco = Free ("from_" ^ (Long_Name.base_name tyco), dummyT --> dummyT) fun to_const tyco = Free ("to_" ^ (Long_Name.base_name tyco), dummyT --> dummyT) val c = Const (cN, Ts ---> T) val cN_opt = Const (\<^const_name>\Some\, \<^typ>\string\ --> str_optT) $ HOLogic.mk_string (Long_Name.base_name cN) val xs = map Free (Name.invent_names (Variable.names_of lthy) "x" Ts) val xs_from = map (fn (v,t) => case find_type t tnames of NONE => v | _ => (from_const (get_type_name t)) $ v) (xs ~~ Ts) val xs_to = map (fn (v,t) => case find_type t tnames of NONE => v | _ => (to_const (get_type_name t)) $ mk_comb_type v) (xs ~~ Ts) val xs_to' = map (fn (v,t) => case find_type t tnames of NONE => v | _ => mk_comb_type v) (xs ~~ Ts) val prefix = case tail_ctrs of [] => if constr_names andalso (not (HOLogic.is_unit (hd prefix))) then (let val (butlast,last) = split_last prefix in butlast @ [last |> dest_comb |> fst |> (fn t => t $ cN_opt)] end) else prefix | _ => prefix val conv_inner_from = case tail_ctrs of [] => if constr_names then mk_tagged_tuple sels xs_from else HOLogic.mk_tuple xs_from | _ => if constr_names then mk_tagged_Inl cN_opt (generate_sum_prodT tail_ctrs) (mk_tagged_tuple sels xs_from) else BNF_FP_Util.mk_Inl (generate_sum_prodT tail_ctrs) (HOLogic.mk_tuple xs_from) val conv_inner_to = case tail_ctrs of [] => if constr_names then mk_tagged_tuple_dummy xs_to' else HOLogic.mk_tuple xs_to' | _ => if constr_names then mk_tagged_Inl dummy_str_opt (generate_sum_prodT tail_ctrs) (mk_tagged_tuple_dummy xs_to') else BNF_FP_Util.mk_Inl (generate_sum_prodT tail_ctrs) (HOLogic.mk_tuple xs_to') val conv_from = if HOLogic.is_unit (hd prefix) then conv_inner_from else Library.foldr (op $) (prefix,conv_inner_from) val conv_to = if HOLogic.is_unit (hd prefix) then conv_inner_to else Library.foldr (op $) (prefix,conv_inner_to) val conv_dummy = if constr_names then (let val conv_inner = case tail_ctrs of [] => mk_tagged_tuple_dummy xs_to' | _ => mk_tagged_Inl dummy_str_opt (generate_sum_prodT tail_ctrs) (mk_tagged_tuple_dummy xs_to') in (if HOLogic.is_unit (hd prefix) then conv_inner else Library.foldr (op $) ((map add_dummy_patterns prefix), conv_inner)) end) else conv_to val lhs_from = (from_const tyco) $ list_comb (c, xs) val lhs_to = (to_const tyco) $ conv_dummy in (abstract_over_vars xs (HOLogic.Trueprop $ ((HOLogic.eq_const dummyT) $ lhs_from $ conv_from)), abstract_over_vars xs (HOLogic.Trueprop $ ((HOLogic.eq_const dummyT) $ lhs_to $ list_comb (c,xs_to)))) end in case ctrs of [] => ([],[]) | (c::cs) => let val s = if null sels then replicate (length (snd c)) "" else hd sels val ss = if null sels then [] else tl sels val new_prefix = if HOLogic.is_unit (hd prefix) then if constr_names then [(Inr_const (generate_sum_prodT [(snd c)]) (generate_sum_prodT (map snd cs))) $ Const (\<^const_name>\None\, str_optT)] else [(BNF_FP_Util.Inr_const (generate_sum_prodT [(snd c)]) (generate_sum_prodT (map snd cs)))] else prefix @ (if constr_names then [(Inr_const (generate_sum_prodT [(snd c)]) (generate_sum_prodT (map snd cs))) $ Const (\<^const_name>\None\, str_optT)] else [(BNF_FP_Util.Inr_const (generate_sum_prodT [(snd c)]) (generate_sum_prodT (map snd cs)))]) val (from_eq,to_eq) = generate_conversion_eq lthy prefix c s (map snd cs) val (from_eqs,to_eqs) = generate_conversion_eqs_rec lthy Ts comb_type (((tyco,cs),T),new_prefix) ss in (from_eq :: from_eqs, to_eq :: to_eqs) end end fun generate_mutual_prefixes inConst Ts mutual_rep_types = let fun generate_sumT [] = HOLogic.unitT | generate_sumT [x] = x | generate_sumT (x::xs) = mk_tagged_sumT x (generate_sumT xs) fun generate_mutual_prefix rep_types index = let fun generate_mutual_prefix_aux rep_types index = case index of 0 => if constr_names then [(Inl_const (hd rep_types) (generate_sumT (tl rep_types))) $ none_str_opt] else [Inl_const (hd rep_types) (generate_sumT (tl rep_types))] | n => let val inr = if constr_names then (Inr_const (hd rep_types) (generate_sumT (tl rep_types))) $ none_str_opt else Inr_const (hd rep_types) (generate_sumT (tl rep_types)) in if (length rep_types) > 2 then inr :: (generate_mutual_prefix_aux (tl rep_types) (n-1)) else [inr] end in inConst :: (generate_mutual_prefix_aux rep_types index) end val indices = List.tabulate (length Ts, fn x => x) in (map (generate_mutual_prefix mutual_rep_types) indices) end fun add_functions lthy = let val eqs = if is_recursive then let fun get_mutual_rep_types ty n = if n = 1 then [ty] else case ty of Type (tname, [LT, RT]) => if tname = sum_type_name then LT :: (get_mutual_rep_types RT (n-1)) else [Type (tname, [LT, RT])] | T => [T] val comb_type = #comb_type (the (#comb_info ty_info)) val inConst_free = #inConst_free (the (#comb_info ty_info)) val rep_type_inst = #rep_type_instantiated (the (#comb_info ty_info)) val mutual_rep_types = if is_mutually_recursive then get_mutual_rep_types rep_type_inst (length Ts) else [rep_type_inst] val prefixes = if is_mutually_recursive then generate_mutual_prefixes inConst_free Ts mutual_rep_types else replicate (length Ts) [inConst_free] in map2 (generate_conversion_eqs_rec lthy Ts comb_type) ((ctrs ~~ Ts) ~~ prefixes) (map snd sels) end else map2 (generate_conversion_eqs lthy [HOLogic.unit]) (ctrs ~~ Ts) (map snd sels) val from_eqs = flat (map fst eqs) val to_eqs = flat (map snd eqs) val (from_info,lthy') = add_fun' (map (fn tname => (Binding.name ("from_" ^ Long_Name.base_name tname), NONE, NoSyn)) tnames) (map (fn t => ((Binding.empty_atts, t), [], [])) from_eqs) Function_Fun.fun_config lthy val (to_info,lthy'') = add_fun' (map (fn tname => (Binding.name ("to_" ^ Long_Name.base_name tname), NONE, NoSyn)) tnames) (map (fn t => ((Binding.empty_atts, t), [], [])) to_eqs) Function_Fun.fun_config lthy' in (from_info,to_info,lthy'') end in add_functions lthy end fun define_rep_type tnames ctrs constr_names lthy = let val sum_type_name = if constr_names then \<^type_name>\Tagged_Prod_Sum.sum\ else \<^type_name>\Sum_Type.sum\ val prod_type_name = if constr_names then \<^type_name>\Tagged_Prod_Sum.prod\ else \<^type_name>\Product_Type.prod\ fun collect_tfree_names ctrs = fold Term.add_tfree_namesT (ctrs |> map (fn l => map snd (snd l)) |> flat |> flat) [] val tFree_renaming = let val used_tfrees = collect_tfree_names ctrs val ctxt = Name.make_context used_tfrees val ts = map Type ((map fst ctrs) ~~ (replicate (length ctrs) [])) val names = Name.invent_names ctxt "'a" ts |> map fst in ts ~~ (map TFree (names ~~ (replicate (length names) \<^sort>\type\))) end fun replace_types_tvars recTs T = (case T of Type (s,_) => perhaps (AList.lookup (op =) recTs) (Type (s, [])) | _ => T) fun mk_tagged_prodT (T1, T2) = Type (prod_type_name, [T1, T2]) fun mk_tagged_sumT LT RT = Type (sum_type_name, [LT, RT]) val rep_type = let val ctrs' = (ctrs |> map (fn l => map snd (snd l))) fun mk_prodT [] = HOLogic.unitT | mk_prodT [x] = replace_types_tvars tFree_renaming x | mk_prodT (x::xs) = mk_tagged_prodT (replace_types_tvars tFree_renaming x, (mk_prodT xs)) fun mk_sumT [] = HOLogic.unitT | mk_sumT [x] = x | mk_sumT (x::xs) = mk_tagged_sumT x (mk_sumT xs) fun generate_rep_type_aux [] = HOLogic.unitT | generate_rep_type_aux [x] = mk_prodT x | generate_rep_type_aux (x::xs) = let val l = mk_prodT x val r = generate_rep_type_aux xs in mk_tagged_sumT l r end in mk_sumT (map generate_rep_type_aux ctrs') end val rep_type_name = fold (curry (op ^)) (map Long_Name.base_name tnames) "" ^ "_rep" val tfrees = (collect_tfree_names ctrs) @ (map (snd #> (dest_TFree #> fst)) tFree_renaming) val _ = writeln ("Defining representation type " ^ rep_type_name) val (full_rep_name,lthy') = Typedecl.abbrev (Binding.name rep_type_name, tfrees, NoSyn) rep_type lthy in ({repname = full_rep_name, rep_type = rep_type, tFrees_mapping = tFree_renaming, from_info = NONE, to_info = NONE} : rep_type_info , lthy') end fun get_combinator_info comb_type_name ctr_type lthy = let val inConst = Proof_Context.read_const {proper = true, strict = true} lthy "In" val inConstType = inConst |> dest_Const |> snd |> Derive_Util.freeify_tvars val inConst_free = Const (inConst |> dest_Const |> fst, inConstType) val comb_type = inConstType |> body_type val comb_type_name_full = comb_type |> dest_Type |> fst val rep_type_instantiated = inConstType |> binder_types |> hd in {combname = comb_type_name, combname_full = comb_type_name_full, comb_type = comb_type, ctr_type = ctr_type, inConst = inConst, inConst_free = inConst_free, inConst_type = inConstType, rep_type_instantiated = rep_type_instantiated} : comb_type_info end fun define_combinator_type tnames tfrees (rep_info : rep_type_info) lthy = let val comb_type_name = "mu" ^ (fold (curry (op ^)) (map Long_Name.base_name tnames) "") ^ "F" val rec_tfrees = map (dest_TFree o snd) (#tFrees_mapping rep_info) val rec_tfree_names = map fst rec_tfrees val rep_tfree_names = (map (fst o dest_TFree o fst) tfrees) val comb_type_name_tvars = add_tvars comb_type_name rep_tfree_names val rec_type = (Type (comb_type_name,map fst tfrees)) val ctr_tfree_names = rep_tfree_names @ (replicate (length rec_tfree_names) comb_type_name_tvars) val ctr_type_name = add_tvars (#repname rep_info) ctr_tfree_names val ctr_type = map_type_tfree (fn (tfree,s) => case List.find (curry (op =) tfree) rec_tfree_names of SOME _ => rec_type | NONE => TFree (tfree,s)) (#rep_type rep_info) val ctr_typarams = ((replicate (length tfrees) (SOME Binding.empty)) ~~ (rep_tfree_names ~~ (replicate (length tfrees) NONE))) val ctr_specs = [(((Binding.empty, Binding.name "In"), [(Binding.empty, ctr_type_name)]), NoSyn)] val _ = writeln ("Defining combinator type " ^ comb_type_name) val lthy' = BNF_FP_Def_Sugar.co_datatype_cmd BNF_Util.Least_FP BNF_LFP.construct_lfp ((K Plugin_Name.default_filter, false), [(((((ctr_typarams, Binding.name comb_type_name), NoSyn), ctr_specs) ,(Binding.empty, Binding.empty, Binding.empty)) ,[])]) lthy val comb_info = get_combinator_info comb_type_name ctr_type lthy' in (SOME comb_info , lthy') end fun generate_type_info tname constr_names lthy = let val (tnames, Ts) = Derive_Util.mutual_recursive_types tname lthy (* get constructor and selector information from the BNF package *) fun get_ctrs t = (t,map (apsnd (map Derive_Util.freeify_tvars o fst o strip_type) o dest_Const) (Derive_Util.constr_terms lthy t)) fun get_sels t = (t,Ctr_Sugar.ctr_sugar_of lthy t |> the |> #selss |> (map (map (dest_Const #> fst #> Long_Name.base_name)))) val ctrs = map get_ctrs tnames val sels = map get_sels tnames val tfrees = collect_tfrees ctrs val is_mutually_rec = (length tnames) > 1 (* look for recursive constructor arguments *) val is_rec = ctrs_arguments ctrs |> filter is_typeT |> map (dest_Type #> fst) |> List.exists (fn n => is_some (List.find (curry (op =) n) tnames)) val (rep_info,lthy') = define_rep_type tnames ctrs constr_names lthy val (comb_info,lthy'') = if is_rec then define_combinator_type tnames tfrees rep_info lthy' else (NONE,lthy') in ({tname = tname, uses_metadata = constr_names, tfrees = tfrees, mutual_tnames = tnames, mutual_Ts = Ts, mutual_ctrs = ctrs, mutual_sels = sels, is_rec = is_rec, is_mutually_rec = is_mutually_rec, rep_info = rep_info, comb_info = comb_info, iso_thm = NONE} : type_info , lthy'') end fun generate_class_info class = {classname = hd class, class = class, params = NONE, class_law = NONE, class_law_const = NONE, ops = NONE, transfer_law = NONE, axioms = NONE, axioms_def = NONE, class_def = NONE, equivalence_thm = NONE} fun record_type_class_info ty_info cl_info inst_info thy = let fun add_info info thy = Type_Data.put (Symreltab.update ((#tname info, Bool.toString (#uses_metadata info)),info) (Type_Data.get thy)) thy fun add_inst_info classname tname thy = Instance_Data.put (Symreltab.update ((classname, tname), inst_info) (Instance_Data.get thy)) thy fun update_tname ({tname = _, uses_metadata = uses_metadata, tfrees = tfrees, mutual_tnames = mutual_tnames, mutual_Ts = mutual_Ts, mutual_ctrs = mutual_ctrs, mutual_sels = mutual_sels, is_rec = is_rec, is_mutually_rec = is_mutually_rec, rep_info = rep_info, comb_info = comb_info, iso_thm = iso_thm} : type_info) tname = {tname = tname, uses_metadata = uses_metadata, tfrees = tfrees, mutual_tnames = mutual_tnames, mutual_Ts = mutual_Ts, mutual_ctrs = mutual_ctrs, mutual_sels = mutual_sels, is_rec = is_rec, is_mutually_rec = is_mutually_rec, rep_info = rep_info, comb_info = comb_info, iso_thm = iso_thm} : type_info val infos = map (update_tname ty_info) (#mutual_tnames ty_info) in fold add_info infos thy |> Class_Data.put (Symtab.update ((#classname cl_info),cl_info) (Class_Data.get thy)) |> fold (add_inst_info (#classname cl_info)) (#mutual_tnames ty_info) end fun generate_instance tname class constr_names thy = let val (T,xs) = Derive_Util.typ_and_vs_of_typname thy tname class val has_law = has_class_law (hd class) thy val cl_info = case get_class_info thy (hd class) of NONE => if has_law then error ("Class " ^ (hd class) ^ "not set up for derivation, call derive_setup first") else generate_class_info class | SOME info => info val raw_params = map snd (Class.these_params thy class) val cl_info' = add_params_cl_info cl_info raw_params val thy' = Class_Data.put (Symtab.update ((#classname cl_info'),cl_info') (Class_Data.get thy)) thy val lthy = Named_Target.theory_init thy' val (ty_info,lthy') = case get_type_info thy tname constr_names of SOME info => let val _ = writeln ("Using existing type information for " ^ tname) in (info,lthy) end | NONE => let val (t_info,lthy) = generate_type_info tname constr_names lthy val (from_info,to_info,lthy') = define_prod_sum_conv t_info constr_names lthy val t_info' = add_conversion_info from_info to_info t_info val (iso_thm,lthy'') = if has_law then Derive_Laws.prove_isomorphism t_info' lthy' else (NONE,lthy') val t_info'' = add_iso_info iso_thm t_info' in (t_info'',lthy'') end val tnames = #mutual_tnames ty_info val Ts = (map (fn tn => Derive_Util.typ_and_vs_of_typname thy tn class) tnames) |> map fst fun define_operations_all_Ts _ lthy = let val (thms,lthy') = fold_map (define_operations raw_params) (tnames ~~ Ts) lthy |> apfst flat val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy') val thms_export = Proof_Context.export lthy' ctxt_thy thms val inst_info = mk_inst_info thms_export in (inst_info,lthy') end fun instantiate_and_prove _ lthy = Local_Theory.exit_global lthy |> (Class.instantiation (tnames, xs, class)) |> define_operations_all_Ts cl_info' |> (fn (inst_info,lthy) => (if has_law then let val equivalence_thm = (Derive_Laws.prove_equivalence_law cl_info inst_info lthy) val cl_info'' = add_equivalence_cl_info cl_info' equivalence_thm in (Class.prove_instantiation_exit (Derive_Laws.prove_instance_tac T cl_info'' inst_info ty_info) lthy) |> pair cl_info'' |> pair inst_info end else (Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt []) lthy) |> pair cl_info |> pair inst_info)) |> (fn (inst_info,(cl_info,thy)) => record_type_class_info ty_info cl_info inst_info thy) |> Proof_Context.init_global val empty_goal = [[]] (* Generate instance for Mu-combinator type if there is recursion *) val thy' = if (#is_rec ty_info) then (instantiate_combinator_type ty_info cl_info' constr_names lthy' |> (if is_some (#class_law cl_info') then Derive_Laws.prove_combinator_instance instantiate_and_prove else Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt []) #> Named_Target.theory_init #> Proof.theorem NONE instantiate_and_prove empty_goal)) else Proof.theorem NONE instantiate_and_prove empty_goal lthy' in thy' end fun generate_instance_cmd classname tyco constr_names thy = let val lthy = Proof_Context.init_global thy val T = Syntax.parse_typ lthy tyco |> dest_Type |> fst val class = Syntax.parse_sort (Proof_Context.init_global thy) classname in generate_instance T class constr_names thy end val parse_cmd = Scan.optional (Args.parens (Parse.reserved "metadata")) "" -- Parse.name -- Parse.type_const val _ = Outer_Syntax.command \<^command_keyword>\derive_generic\ "derives some sort" (parse_cmd >> (fn ((s,c),t) => let val meta = s = "metadata" in Toplevel.theory_to_proof (generate_instance_cmd c t meta) end )) fun add_inst_info classname tname thms thy = Instance_Data.put (Symreltab.update ((classname, tname) ,{defs = thms}) (Instance_Data.get thy)) thy end diff --git a/thys/Generic_Deriving/derive_setup.ML b/thys/Generic_Deriving/derive_setup.ML --- a/thys/Generic_Deriving/derive_setup.ML +++ b/thys/Generic_Deriving/derive_setup.ML @@ -1,137 +1,138 @@ open Derive_Util signature DERIVE_SETUP = sig val prove_class_transfer : string -> theory -> Proof.state val define_class_law : string -> Proof.context -> (thm * thm * thm option * term list * local_theory) end structure Derive_Setup : DERIVE_SETUP = struct fun get_class_info thy classname = Symtab.lookup (Class_Data.get thy) classname fun replace_superclasses lthy (s $ t) = replace_superclasses lthy s $ replace_superclasses lthy t | replace_superclasses lthy (Const (n,T)) = let val is_class = Long_Name.base_name n val class = Syntax.parse_sort lthy is_class handle ERROR _ => [] in if null class then Const (n,T) else let val class_data = get_class_info (Proof_Context.theory_of lthy) (hd class) in if is_some class_data then the (#class_law_const (the class_data)) else Const (n,T) end end | replace_superclasses _ t = t fun contains_axioms cn (s $ t) = contains_axioms cn s orelse contains_axioms cn t | contains_axioms cn (Const (n,_)) = let val is_class = Long_Name.base_name n in if is_class = cn ^ "_axioms" then true else false end | contains_axioms _ _ = false fun define_class_law classname lthy = let val class_def = Proof_Context.get_thm lthy ("class." ^ classname ^ "_def") val has_axioms = contains_axioms classname (class_def |> Thm.full_prop_of |> Logic.unvarify_global |> Logic.dest_equals |> snd) val (axioms_def,(vars,class_law)) = class_def |> (if has_axioms then let val axioms_def = Proof_Context.get_thm lthy ("class." ^ classname ^ "_axioms_def") in Local_Defs.unfold lthy [axioms_def] #> pair (SOME axioms_def) end else (pair NONE)) ||> Thm.full_prop_of ||> Logic.unvarify_global ||> Logic.dest_equals ||> apfst (strip_comb #> snd) ||> apsnd (replace_superclasses lthy) val class_law_name = classname ^ "_class_law" val class_law_lhs = list_comb ((Free (class_law_name,(map (dest_Free #> snd) vars) ---> \<^typ>\bool\)),vars) val class_law_eq = HOLogic.Trueprop $ HOLogic.mk_eq (class_law_lhs,class_law) val ((_,(_,class_law_thm)),lthy') = Specification.definition NONE [] [] ((Binding.empty, []), class_law_eq) lthy val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy') val class_law_thm_export = singleton (Proof_Context.export lthy' ctxt_thy) class_law_thm in (class_law_thm_export,class_def,axioms_def,vars,lthy') end fun transfer_op lthy from to var = let fun convert_arg (T,i) = case T of (TFree (_,_)) => from $ (Bound i) | _ => Bound i fun abstract [] t = t | abstract (x::xs) t = (Abs (x, dummyT, abstract xs t)) val (v,T) = dest_Free var val (binders,body) = strip_type T val argnames = Name.invent_names (Variable.names_of lthy) "x" binders |> map fst val args_converted = map convert_arg (binders ~~ (List.tabulate (length binders,fn n => (length binders)-(n+1)))) val op_call = list_comb ((Free (v,T)),args_converted) val op_converted = case body of (TFree (_,_)) => to $ op_call | _ => op_call in abstract argnames op_converted end fun prove_class_transfer classname thy = let fun add_info info thy = Class_Data.put (Symtab.update ((#classname info),info) (Class_Data.get thy)) thy val class = Syntax.parse_sort (Proof_Context.init_global thy) classname val classname_full = hd class val axioms = Axclass.get_info thy classname_full |> #axioms val (class_law,class_def,axioms_def,vars,lthy) = define_class_law classname (Named_Target.theory_init thy) - (* Exit so that class law is defined properly before the next step *) - val thy' = Named_Target.exit lthy + (* Exit so that class law is defined properly before the next step + FIXME use begin / end block instead (?) *) + val thy' = Local_Theory.exit_global lthy val lthy' = Named_Target.theory_init thy' val tfree_dt = get_tvar (map (dest_Free #> snd) vars) val tfree_rep = let val (n,s) = tfree_dt |> dest_TFree in Name.invent_names (Name.make_context [n]) "'a" [s] end |> hd |> TFree val from = Free ("from",tfree_rep --> tfree_dt) val to = Free ("to",tfree_dt --> tfree_rep) val class_law_const = Thm.full_prop_of class_law |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst |> strip_comb |> fst val class_law_const_dummy = dest_Const class_law_const |> apsnd (K dummyT) |> Const val class_law_var = (Term.add_tvars class_law_const []) |> hd |> fst val class_law_const_dt = subst_vars ([(class_law_var,tfree_dt)],[]) class_law_const val class_law_const_rep = subst_vars ([(class_law_var,tfree_rep)],[]) class_law_const val assm_iso = HOLogic.mk_Trueprop (Const (\<^const_name>\Derive.iso\,dummyT) $ from $ to) val assm_class = HOLogic.mk_Trueprop (list_comb (class_law_const_dt,vars)) val vars_transfer = map (transfer_op lthy' from to) vars val transfer_concl = HOLogic.mk_Trueprop (list_comb (class_law_const_rep,vars_transfer)) val transfer_term = Logic.mk_implies (assm_iso, (Logic.mk_implies (assm_class, transfer_concl))) val transfer_term_inf = Type_Infer_Context.infer_types lthy' [transfer_term] |> hd fun after_qed thms lthy = (fold_map (fn lthy => fn thm => (Local_Theory.note ((Binding.name (classname ^ "_transfer"),[]), lthy) thm)) thms lthy) |> (fn (thms,lthy) => Local_Theory.background_theory (add_info {classname = classname_full, class = class, params = NONE, class_law = SOME class_law, class_law_const = SOME class_law_const_dummy, ops = SOME vars, transfer_law = SOME thms, axioms = SOME axioms, axioms_def = axioms_def, class_def = SOME class_def, equivalence_thm = NONE}) lthy) |> Local_Theory.exit in Proof.theorem NONE after_qed [[(transfer_term_inf, [])]] lthy' end val _ = Outer_Syntax.command \<^command_keyword>\derive_generic_setup\ "prepare a class for derivation" (Parse.name >> (fn c => Toplevel.theory_to_proof (fn thy => if has_class_law c thy then prove_class_transfer c thy else error ("Class " ^ c ^ " has no associated laws, no need to call derive_setup")))) end \ No newline at end of file diff --git a/thys/Isabelle_C/C11-FrontEnd/src/C_Command.thy b/thys/Isabelle_C/C11-FrontEnd/src/C_Command.thy --- a/thys/Isabelle_C/C11-FrontEnd/src/C_Command.thy +++ b/thys/Isabelle_C/C11-FrontEnd/src/C_Command.thy @@ -1,963 +1,963 @@ (****************************************************************************** * Isabelle/C * * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: * * * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above * copyright notice, this list of conditions and the following * disclaimer in the documentation and/or other materials provided * with the distribution. * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) section \Interface: Inner and Outer Commands\ theory C_Command imports C_Eval keywords "C" :: thy_decl % "ML" and "C_file" :: thy_load % "ML" and "C_export_boot" :: thy_decl % "ML" and "C_export_file" :: thy_decl and "C_prf" :: prf_decl % "proof" (* FIXME % "ML" ?? *) and "C_val" :: diag % "ML" begin subsection \Parsing Entry-Point: Error and Acceptance Cases\ ML \ \\<^file>\~~/src/Pure/Tools/ghc.ML\\ (* Author: Frédéric Tuong, Université Paris-Saclay *) (* Title: Pure/Tools/ghc.ML Author: Makarius Support for GHC: Glasgow Haskell Compiler. *) \ structure C_Serialize = struct (** string literals **) fun print_codepoint c = (case c of 10 => "\\n" | 9 => "\\t" | 11 => "\\v" | 8 => "\\b" | 13 => "\\r" | 12 => "\\f" | 7 => "\\a" | 27 => "\\e" | 92 => "\\\\" | 63 => "\\?" | 39 => "\\'" | 34 => "\\\"" | c => if c >= 32 andalso c < 127 then chr c else error "Not yet implemented"); fun print_symbol sym = (case Symbol.decode sym of Symbol.Char s => print_codepoint (ord s) | Symbol.UTF8 s => UTF8.decode_permissive s |> map print_codepoint |> implode | Symbol.Sym s => "\\092<" ^ s ^ ">" | Symbol.Control s => "\\092<^" ^ s ^ ">" | _ => translate_string (print_codepoint o ord) sym); val print_string = quote o implode o map print_symbol o Symbol.explode; end \ ML \ \\<^file>\~~/src/Pure/Tools/generated_files.ML\\ (* Author: Frédéric Tuong, Université Paris-Saclay *) (* Title: Pure/Tools/generated_files.ML Author: Makarius Generated source files for other languages: with antiquotations, without Isabelle symbols. *) \ structure C_Generated_Files = struct val c_dir = "C"; val c_ext = "c"; val c_make_comment = enclose "/*" "*/"; (** context data **) (* file types *) fun get_file_type ext = if ext = "" then error "Bad file extension" else if c_ext = ext then () else error ("Unknown file type for extension " ^ quote ext); (** Isar commands **) (* generate_file *) fun generate_file (binding, src_content) lthy = let val (path, pos) = Path.dest_binding binding; val () = get_file_type (#2 (Path.split_ext path)) handle ERROR msg => error (msg ^ Position.here pos); val header = c_make_comment " generated by Isabelle "; val content = header ^ "\n" ^ src_content; in lthy |> (Local_Theory.background_theory o Generated_Files.add_files) (binding, content) end; (** concrete file types **) val _ = Theory.setup (Generated_Files.file_type \<^binding>\C\ {ext = c_ext, make_comment = c_make_comment, make_string = C_Serialize.print_string}); end \ ML \ \\<^theory>\Isabelle_C.C_Eval\\ \ structure C_Module = struct structure Data_In_Source = Generic_Data (type T = Input.source list val empty = [] val extend = I val merge = K empty) structure Data_In_Env = Generic_Data (type T = C_Env.env_lang val empty = C_Env.empty_env_lang val extend = I val merge = K empty) structure Data_Accept = Generic_Data (type T = C_Grammar_Rule.start_happy -> C_Env.env_lang -> Context.generic -> Context.generic fun empty _ _ = I val extend = I val merge = #2) structure Data_Term = Generic_Data (type T = (C_Grammar_Rule.start_happy -> C_Env.env_lang -> local_theory -> term) Symtab.table val empty = Symtab.empty val extend = I val merge = #2) structure C_Term = struct val key_translation_unit = \translation_unit\ val key_external_declaration = \external_declaration\ val key_statement = \statement\ val key_expression = \expression\ val key_default = \default\ local val source_content = Input.source_content #> #1 in val key0_translation_unit = source_content key_translation_unit val key0_external_declaration = source_content key_external_declaration val key0_statement = source_content key_statement val key0_expression = source_content key_expression val key0_default = source_content key_default end val tok0_translation_unit = (key0_translation_unit, C_Grammar.Tokens.start_translation_unit) val tok0_external_declaration = ( key0_external_declaration , C_Grammar.Tokens.start_external_declaration) val tok0_statement = (key0_statement, C_Grammar.Tokens.start_statement) val tok0_expression = (key0_expression, C_Grammar.Tokens.start_expression) val tok_translation_unit = (key_translation_unit, C_Grammar.Tokens.start_translation_unit) val tok_external_declaration = ( key_external_declaration , C_Grammar.Tokens.start_external_declaration) val tok_statement = (key_statement, C_Grammar.Tokens.start_statement) val tok_expression = (key_expression, C_Grammar.Tokens.start_expression) val tokens = [ tok0_translation_unit , tok0_external_declaration , tok0_statement , tok0_expression ] local fun map_upd0 key v = Context.theory_map (Data_Term.map (Symtab.update (key, v))) fun map_upd key start f = map_upd0 key (f o the o start) in val map_translation_unit = map_upd key0_translation_unit C_Grammar_Rule.start_happy1 val map_external_declaration = map_upd key0_external_declaration C_Grammar_Rule.start_happy2 val map_statement = map_upd key0_statement C_Grammar_Rule.start_happy3 val map_expression = map_upd key0_expression C_Grammar_Rule.start_happy4 val map_default = map_upd0 key0_default end end fun env0 ctxt = case Config.get ctxt C_Options.starting_env of "last" => Data_In_Env.get (Context.Proof ctxt) | "empty" => C_Env.empty_env_lang | s => error ("Unknown option: " ^ s ^ Position.here (Config.pos_of C_Options.starting_env)) val env = env0 o Context.proof_of fun start source context = Input.range_of source |> let val s = Config.get (Context.proof_of context) C_Options.starting_rule in case AList.lookup (op =) C_Term.tokens s of SOME tok => tok | NONE => error ("Unknown option: " ^ s ^ Position.here (Config.pos_of C_Options.starting_rule)) end fun err0 _ _ pos = C_Env.map_error_lines (cons ("Parser: No matching grammar rule" ^ Position.here pos)) val err = pair () oooo err0 fun accept0 f env_lang ast = Data_In_Env.put env_lang #> (fn context => f context ast env_lang (Data_Accept.get context ast env_lang context)) fun accept env_lang (_, (ast, _, _)) = pair () o C_Env.map_context (accept0 (K (K (K I))) env_lang ast) val eval_source = C_Context.eval_source env start err accept fun c_enclose bg en source = C_Lex.@@ ( C_Lex.@@ (C_Lex.read bg, C_Lex.read_source source) , C_Lex.read en); structure C_Term' = struct val err = pair Term.dummy oooo err0 fun accept ctxt start_rule = let val (key, start) = case start_rule of NONE => (C_Term.key_default, start) | SOME (key, start_rule) => (key, fn source => fn _ => start_rule (Input.range_of source)) val (key, pos) = Input.source_content key in ( start , fn env_lang => fn (_, (ast, _, _)) => C_Env.map_context' (accept0 (fn context => pair oo (case Symtab.lookup (Data_Term.get context) key of NONE => tap (fn _ => warning ("Representation function associated to\ \ \"" ^ key ^ "\"" ^ Position.here pos ^ " not found (returning a dummy term)")) (fn _ => fn _ => @{term "()"}) | SOME f => fn ast => fn env_lang => f ast env_lang ctxt)) env_lang ast)) end fun eval_in text context env start_rule = let val (start, accept) = accept (Context.proof_of context) start_rule in C_Context.eval_in (SOME context) env (start text) err accept end fun parse_translation l = l |> map (apsnd (fn start_rule => fn ctxt => fn args => let val msg = (case start_rule of NONE => C_Term.key_default | SOME (key, _) => key) |> Input.source_content |> #1 fun err () = raise TERM (msg, args) in case args of [(c as Const (\<^syntax_const>\_constrain\, _)) $ Free (s, _) $ p] => (case Term_Position.decode_position p of SOME (pos, _) => c $ let val src = uncurry (Input.source false) let val s0 = Symbol_Pos.explode (s, pos) val s = Symbol_Pos.cartouche_content s0 in ( Symbol_Pos.implode s , case s of [] => Position.no_range | (_, pos0) :: _ => Position.range (pos0, s0 |> List.last |> snd)) end in eval_in src (case Context.get_generic_context () of NONE => Context.Proof ctxt | SOME context => Context.mapping I (K ctxt) context) (C_Stack.Data_Lang.get #> (fn NONE => env0 ctxt | SOME (_, env_lang) => env_lang)) start_rule (c_enclose "" "" src) end $ p | NONE => err ()) | _ => err () end)) end fun eval_in text ctxt = C_Context.eval_in ctxt env (start text) err accept fun exec_eval source = Data_In_Source.map (cons source) #> ML_Context.exec (fn () => eval_source source) fun C_prf source = Proof.map_context (Context.proof_map (exec_eval source)) #> Proof.propagate_ml_env fun C_export_boot source context = context |> Config.put_generic ML_Env.ML_environment ML_Env.Isabelle |> Config.put_generic ML_Env.ML_write_global true |> exec_eval source |> Config.restore_generic ML_Env.ML_write_global context |> Config.restore_generic ML_Env.ML_environment context |> Local_Theory.propagate_ml_env fun C source = exec_eval source #> Local_Theory.propagate_ml_env fun C' env_lang src context = context |> C_Env.empty_env_tree |> C_Context.eval_source' env_lang (fn src => start src context) err accept src |> (fn (_, {context, reports_text, error_lines}) => tap (fn _ => case error_lines of [] => () | l => warning (cat_lines (rev l))) (C_Stack.Data_Tree.map (curry C_Stack.Data_Tree_Args.merge (reports_text, [])) context)) fun C_export_file (pos, _) lthy = let val c_sources = Data_In_Source.get (Context.Proof lthy) val binding = Path.binding ( Path.appends [ Path.basic C_Generated_Files.c_dir , Path.basic (string_of_int (length c_sources)) , lthy |> Proof_Context.theory_of |> Context.theory_name |> Path.explode |> Path.ext C_Generated_Files.c_ext ] , pos) in lthy |> C_Generated_Files.generate_file (binding, rev c_sources |> map (Input.source_content #> #1) |> cat_lines) |> tap (Proof_Context.theory_of #> (fn thy => let val file = Generated_Files.get_file thy binding in Generated_Files.export_file thy file; writeln (Export.message thy Path.current); writeln (prefix " " (Generated_Files.print_file file)) end)) end end \ subsection \Definitions of Inner Directive Commands\ subsubsection \Initialization\ ML \ \\<^theory>\Pure\\ \ structure C_Directive = struct local fun directive_update keyword data = C_Context.directive_update keyword (data, K (K (K I))) fun return f (env_cond, env) = ([], (env_cond, f env)) fun directive_update_define pos f_toks f_antiq = directive_update ("define", pos) (return o (fn C_Lex.Define (_, C_Lex.Group1 ([], [tok3]), NONE, C_Lex.Group1 ([], toks)) => let val map_ctxt = case (tok3, toks) of (C_Lex.Token ((pos, _), (C_Lex.Ident, ident)), [C_Lex.Token (_, (C_Lex.Integer (_, C_Lex.Repr_decimal, []), integer))]) => C_Env.map_context (Context.map_theory (Named_Target.theory_map (Specification.definition_cmd (SOME (Binding.make (ident, pos), NONE, NoSyn)) [] [] (Binding.empty_atts, ident ^ " \ " ^ integer) true #> tap (fn ((_, (_, t)), ctxt) => Output.information ("Generating " ^ Pretty.string_of (Syntax.pretty_term ctxt (Thm.prop_of t)) ^ Position.here (Position.range_position ( C_Lex.pos_of tok3 , C_Lex.end_pos_of (List.last toks))))) #> #2))) | _ => I in fn (env_dir, env_tree) => let val name = C_Lex.content_of tok3 val pos = [C_Lex.pos_of tok3] val data = (pos, serial (), (C_Scan.Left (f_toks toks), f_antiq)) in ( Symtab.update (name, data) env_dir , env_tree |> C_Context.markup_directive_define false (C_Ast.Left (data, C_Env_Ext.list_lookup env_dir name)) pos name |> map_ctxt) end end | C_Lex.Define (_, C_Lex.Group1 ([], [tok3]), SOME (C_Lex.Group1 (_ :: toks_bl, _)), _) => tap (fn _ => (* not yet implemented *) warning ("Ignored functional macro directive" ^ Position.here (Position.range_position (C_Lex.pos_of tok3, C_Lex.end_pos_of (List.last toks_bl))))) | _ => I)) in val setup_define = Context.theory_map o C_Context0.Directives.map ooo directive_update_define val _ = Theory.setup (Context.theory_map (C_Context0.Directives.map (directive_update_define \<^here> (K o pair) (K I) #> directive_update ("undef", \<^here>) (return o (fn C_Lex.Undef (C_Lex.Group2 (_, _, [tok])) => (fn (env_dir, env_tree) => let val name = C_Lex.content_of tok val pos1 = [C_Lex.pos_of tok] val data = Symtab.lookup env_dir name in ( (case data of NONE => env_dir | SOME _ => Symtab.delete name env_dir) , C_Context.markup_directive_define true (C_Ast.Right (pos1, data)) pos1 name env_tree) end) | _ => I))))) end end \ subsection \Definitions of Inner Annotation Commands\ subsubsection \Library\ ML \ \\<^file>\~~/src/Pure/Isar/toplevel.ML\\ \ structure C_Inner_Toplevel = struct val theory = Context.map_theory fun local_theory' target f gthy = let - val (finish, lthy) = Named_Target.switch target gthy; + val (finish, lthy) = Target_Context.switch_named_cmd target gthy; val lthy' = lthy |> Local_Theory.new_group |> f false |> Local_Theory.reset_group; in finish lthy' end val generic_theory = I fun keep'' f = tap (f o Context.proof_of) end \ ML \ \\<^file>\~~/src/Pure/Isar/isar_cmd.ML\\ \ structure C_Inner_Isar_Cmd = struct (** theory declarations **) (* generic setup *) fun setup0 f_typ f_val src = fn NONE => let val setup = "setup" in C_Context.expression "C_Ast" (Input.range_of src) setup (f_typ "C_Stack.stack_data" "C_Stack.stack_data_elem -> C_Env.env_lang -> Context.generic -> Context.generic") ("fn context => \ \let val (stack, env_lang) = C_Stack.Data_Lang.get' context \ \in " ^ f_val setup "stack" ^ " (stack |> hd) env_lang end context") (ML_Lex.read_source src) end | SOME rule => let val hook = "hook" in C_Context.expression "C_Ast" (Input.range_of src) hook (f_typ "C_Stack.stack_data" (C_Grammar_Rule.type_reduce rule ^ " C_Stack.stack_elem -> C_Env.env_lang -> Context.generic -> Context.generic")) ("fn context => \ \let val (stack, env_lang) = C_Stack.Data_Lang.get' context \ \in " ^ f_val hook "stack" ^ " " ^ "(stack \ \|> hd \ \|> C_Stack.map_svalue0 C_Grammar_Rule.reduce" ^ Int.toString rule ^ ")\ \env_lang \ \end \ \ context") (ML_Lex.read_source src) end val setup = setup0 (fn a => fn b => a ^ " -> " ^ b) (fn a => fn b => a ^ " " ^ b) val setup' = setup0 (K I) K (* print theorems, terms, types etc. *) local fun string_of_term ctxt s = let val t = Syntax.read_term ctxt s; val T = Term.type_of t; val ctxt' = Proof_Context.augment t ctxt; in Pretty.string_of (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t), Pretty.fbrk, Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)]) end; fun print_item string_of (modes, arg) ctxt = Print_Mode.with_modes modes (fn () => writeln (string_of ctxt arg)) (); in val print_term = print_item string_of_term; end; end \ ML \ \\<^file>\~~/src/Pure/Isar/outer_syntax.ML\\ \ structure C_Inner_Syntax = struct val drop1 = fn C_Scan.Left f => C_Scan.Left (K o f) | C_Scan.Right (f, dir) => C_Scan.Right (K o f, dir) val drop2 = fn C_Scan.Left f => C_Scan.Left (K o K o f) | C_Scan.Right (f, dir) => C_Scan.Right (K o K o f, dir) val bottom_up = C_Env.Bottom_up o C_Env.Exec_annotation (**) fun pref_lex name = "#" ^ name val pref_bot = I fun pref_top name = name ^ "\" (**) fun command2' cmd f (pos_bot, pos_top) = let fun cmd' dir = cmd (C_Scan.Right (f, dir)) Keyword.thy_decl in cmd' bottom_up (pref_bot, pos_bot) #> cmd' C_Env.Top_down (pref_top, pos_top) end fun command3' cmd f (pos_lex, pos_bot, pos_top) = cmd (C_Scan.Left f) (pref_lex, pos_lex) #> command2' (K o cmd) f (pos_bot, pos_top) fun command2 cmd f (name, pos_bot, pos_top) = command2' (fn f => fn kind => fn (name_pref, pos) => cmd f kind (name_pref name, pos)) f (pos_bot, pos_top) fun command3 cmd f (name, pos_lex, pos_bot, pos_top) = command3' (fn f => fn (name_pref, pos) => cmd f (name_pref name, pos)) f (pos_lex, pos_bot, pos_top) (**) fun command00 f kind scan name = C_Annotation.command'' kind name "" (case f of C_Scan.Left f => (fn _ => C_Parse.range scan >> (fn (src, range) => C_Env.Lexing (range, f src range))) | C_Scan.Right (f, dir) => fn ((stack1, (to_delay, stack2)), _) => C_Parse.range scan >> (fn (src, range) => C_Env.Parsing ((stack1, stack2), (range, dir (f src range), Symtab.empty, to_delay)))) fun command00_no_range f kind name = C_Annotation.command'' kind name "" (case f of C_Scan.Left f => (fn (_, range) => Scan.succeed () >> K (C_Env.Lexing (range, f range))) | C_Scan.Right (f, dir) => fn ((stack1, (to_delay, stack2)), range) => Scan.succeed () >> K (C_Env.Parsing ((stack1, stack2), (range, dir (f range), Symtab.empty, to_delay)))) (**) fun command' f = command00 (drop1 f) Keyword.thy_decl fun command f scan = command2 (fn f => fn kind => command00 f kind scan) (K o f) fun command_range f = command00_no_range f Keyword.thy_decl val command_range' = command3 (command_range o drop1) fun command_no_range' f = command00_no_range (drop1 f) Keyword.thy_decl fun command_no_range f = command2 command00_no_range (K f) fun command0 f scan = command3 (fn f => command' (drop1 f) scan) f fun local_command' (name, pos_lex, pos_bot, pos_top) scan f = command3' (fn f => fn (name_pref, pos) => command' (drop1 f) (C_Token.syntax' (Parse.opt_target -- scan name_pref)) (name_pref name, pos)) (fn (target, arg) => C_Inner_Toplevel.local_theory' target (f arg)) (pos_lex, pos_bot, pos_top) fun local_command'' spec = local_command' spec o K val command0_no_range = command_no_range' o drop1 fun command0' f kind scan = command3 (fn f => fn (name, pos) => command00 (drop2 f) kind (scan name) (name, pos)) f end \ ML \ \\<^file>\~~/src/Pure/ML/ml_file.ML\\ \ structure C_Inner_File = struct fun command_c ({lines, pos, ...}: Token.file) = C_Module.C (Input.source true (cat_lines lines) (pos, pos)); fun C files gthy = command_c (hd (files (Context.theory_of gthy))) gthy; fun command_ml environment debug files gthy = let val file: Token.file = hd (files (Context.theory_of gthy)); val source = Token.file_source file; val _ = Thy_Output.check_comments (Context.proof_of gthy) (Input.source_explode source); val flags: ML_Compiler.flags = {environment = environment, redirect = true, verbose = true, debug = debug, writeln = writeln, warning = warning}; in gthy |> ML_Context.exec (fn () => ML_Context.eval_source flags source) |> Local_Theory.propagate_ml_env end; val ML = command_ml ""; val SML = command_ml ML_Env.SML; end; \ subsubsection \Initialization\ setup \ \\<^theory>\Pure\\ \ C_Thy_Header.add_keywords_minor (maps (fn ((name, pos_lex, pos_bot, pos_top), ty) => [ ((C_Inner_Syntax.pref_lex name, pos_lex), ty) , ((C_Inner_Syntax.pref_bot name, pos_bot), ty) , ((C_Inner_Syntax.pref_top name, pos_top), ty) ]) [ (("apply", \<^here>, \<^here>, \<^here>), ((Keyword.prf_script, []), ["proof"])) , (("by", \<^here>, \<^here>, \<^here>), ((Keyword.qed, []), ["proof"])) , (("done", \<^here>, \<^here>, \<^here>), ((Keyword.qed_script, []), ["proof"])) ]) \ ML \ \\<^theory>\Pure\\ \ local val semi = Scan.option (C_Parse.$$$ ";"); structure C_Isar_Cmd = struct fun ML source = ML_Context.exec (fn () => ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) #> Local_Theory.propagate_ml_env fun theorem schematic ((long, binding, includes, elems, concl), (l_meth, o_meth)) int lthy = (if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd) long Thm.theoremK NONE (K I) binding includes elems concl int lthy |> fold (fn m => tap (fn _ => Method.report m) #> Proof.apply m #> Seq.the_result "") l_meth |> (case o_meth of NONE => Proof.global_done_proof | SOME (m1, m2) => tap (fn _ => (Method.report m1; Option.map Method.report m2)) #> Proof.global_terminal_proof (m1, m2)) fun definition (((decl, spec), prems), params) = #2 oo Specification.definition_cmd decl params prems spec fun declare (facts, fixes) = #2 oo Specification.theorems_cmd "" [(Binding.empty_atts, flat facts)] fixes end local val long_keyword = Parse_Spec.includes >> K "" || Parse_Spec.long_statement_keyword; val long_statement = Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) Binding.empty_atts -- Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement >> (fn ((binding, includes), (elems, concl)) => (true, binding, includes, elems, concl)); val short_statement = Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes >> (fn ((shows, assumes), fixes) => (false, Binding.empty_atts, [], [Element.Fixes fixes, Element.Assumes assumes], Element.Shows shows)); in fun theorem spec schematic = C_Inner_Syntax.local_command' spec (fn name_pref => (long_statement || short_statement) -- let val apply = Parse.$$$ (name_pref "apply") |-- Method.parse in Scan.repeat1 apply -- (Parse.$$$ (name_pref "done") >> K NONE) || Scan.repeat apply -- (Parse.$$$ (name_pref "by") |-- Method.parse -- Scan.option Method.parse >> SOME) end) (C_Isar_Cmd.theorem schematic) end val opt_modes = Scan.optional (\<^keyword>\(\ |-- Parse.!!! (Scan.repeat1 Parse.name --| \<^keyword>\)\)) []; val _ = Theory.setup ( C_Inner_Syntax.command (C_Inner_Toplevel.generic_theory oo C_Inner_Isar_Cmd.setup) C_Parse.ML_source ("\setup", \<^here>, \<^here>) #> C_Inner_Syntax.command0 (C_Inner_Toplevel.theory o Isar_Cmd.setup) C_Parse.ML_source ("setup", \<^here>, \<^here>, \<^here>) #> C_Inner_Syntax.command0 (C_Inner_Toplevel.generic_theory o C_Isar_Cmd.ML) C_Parse.ML_source ("ML", \<^here>, \<^here>, \<^here>) #> C_Inner_Syntax.command0 (C_Inner_Toplevel.generic_theory o C_Module.C) C_Parse.C_source ("C", \<^here>, \<^here>, \<^here>) #> C_Inner_Syntax.command0' (C_Inner_Toplevel.generic_theory o C_Inner_File.ML NONE) Keyword.thy_load (fn name => C_Resources.parse_files name --| semi) ("ML_file", \<^here>, \<^here>, \<^here>) #> C_Inner_Syntax.command0' (C_Inner_Toplevel.generic_theory o C_Inner_File.C) Keyword.thy_load (fn name => C_Resources.parse_files name --| semi) ("C_file", \<^here>, \<^here>, \<^here>) #> C_Inner_Syntax.command0 (C_Inner_Toplevel.generic_theory o C_Module.C_export_boot) C_Parse.C_source ("C_export_boot", \<^here>, \<^here>, \<^here>) #> C_Inner_Syntax.command_range' (Context.map_theory o Named_Target.theory_map o C_Module.C_export_file) ("C_export_file", \<^here>, \<^here>, \<^here>) #> C_Inner_Syntax.command_no_range (C_Inner_Toplevel.generic_theory oo C_Inner_Isar_Cmd.setup \fn ((_, (_, pos1, pos2)) :: _) => (fn _ => fn _ => tap (fn _ => Position.reports_text [((Position.range (pos1, pos2) |> Position.range_position, Markup.intensify), "")])) | _ => fn _ => fn _ => I\) ("highlight", \<^here>, \<^here>) #> theorem ("theorem", \<^here>, \<^here>, \<^here>) false #> theorem ("lemma", \<^here>, \<^here>, \<^here>) false #> theorem ("corollary", \<^here>, \<^here>, \<^here>) false #> theorem ("proposition", \<^here>, \<^here>, \<^here>) false #> theorem ("schematic_goal", \<^here>, \<^here>, \<^here>) true #> C_Inner_Syntax.local_command'' ("definition", \<^here>, \<^here>, \<^here>) (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) -- Parse_Spec.if_assumes -- Parse.for_fixes) C_Isar_Cmd.definition #> C_Inner_Syntax.local_command'' ("declare", \<^here>, \<^here>, \<^here>) (Parse.and_list1 Parse.thms1 -- Parse.for_fixes) C_Isar_Cmd.declare #> C_Inner_Syntax.command0 (C_Inner_Toplevel.keep'' o C_Inner_Isar_Cmd.print_term) (C_Token.syntax' (opt_modes -- Parse.term)) ("term", \<^here>, \<^here>, \<^here>)) in end \ subsection \Definitions of Outer Classical Commands\ subsubsection \Library\ (* Author: Frédéric Tuong, Université Paris-Saclay *) (* Title: Pure/Pure.thy Author: Makarius The Pure theory, with definitions of Isar commands and some lemmas. *) ML \ \\<^file>\~~/src/Pure/Isar/parse.ML\\ \ structure C_Outer_Parse = struct val C_source = Parse.input (Parse.group (fn () => "C source") Parse.text) end \ ML \ \\<^file>\~~/src/Pure/Isar/outer_syntax.ML\\ \ structure C_Outer_Syntax = struct val _ = Outer_Syntax.command \<^command_keyword>\C\ "" (C_Outer_Parse.C_source >> (Toplevel.generic_theory o C_Module.C)); end \ ML \ \\<^file>\~~/src/Pure/Isar/isar_cmd.ML\\ \ structure C_Outer_Isar_Cmd = struct (* diagnostic ML evaluation *) structure Diag_State = Proof_Data ( type T = Toplevel.state option; fun init _ = NONE; ); fun C_diag source state = let val opt_ctxt = try Toplevel.generic_theory_of state |> Option.map (Context.proof_of #> Diag_State.put (SOME state)); in Context.setmp_generic_context (Option.map Context.Proof opt_ctxt) (fn () => C_Module.eval_source source) () end; fun diag_state ctxt = (case Diag_State.get ctxt of SOME st => st | NONE => Toplevel.init_toplevel ()); val diag_goal = Proof.goal o Toplevel.proof_of o diag_state; val _ = Theory.setup (ML_Antiquotation.value (Binding.qualify true "Isar" \<^binding>\C_state\) (Scan.succeed "C_Outer_Isar_Cmd.diag_state ML_context") #> ML_Antiquotation.value (Binding.qualify true "Isar" \<^binding>\C_goal\) (Scan.succeed "C_Outer_Isar_Cmd.diag_goal ML_context")); end \ ML \ \\<^file>\~~/src/Pure/ML/ml_file.ML\\ \ structure C_Outer_File = struct fun command_c ({src_path, lines, digest, pos}: Token.file) = let val provide = Resources.provide (src_path, digest); in I #> C_Module.C (Input.source true (cat_lines lines) (pos, pos)) #> Context.mapping provide (Local_Theory.background_theory provide) end; fun C files gthy = command_c (hd (files (Context.theory_of gthy))) gthy; end; \ subsubsection \Initialization\ ML \ \\<^theory>\Pure\\ \ local val semi = Scan.option \<^keyword>\;\; val _ = Outer_Syntax.command \<^command_keyword>\C_file\ "read and evaluate Isabelle/C file" (Resources.parse_files "C_file" --| semi >> (Toplevel.generic_theory o C_Outer_File.C)); val _ = Outer_Syntax.command \<^command_keyword>\C_export_boot\ "C text within theory or local theory, and export to bootstrap environment" (C_Outer_Parse.C_source >> (Toplevel.generic_theory o C_Module.C_export_boot)); val _ = Outer_Syntax.command \<^command_keyword>\C_prf\ "C text within proof" (C_Outer_Parse.C_source >> (Toplevel.proof o C_Module.C_prf)); val _ = Outer_Syntax.command \<^command_keyword>\C_val\ "diagnostic C text" (C_Outer_Parse.C_source >> (Toplevel.keep o C_Outer_Isar_Cmd.C_diag)); val _ = Outer_Syntax.local_theory \<^command_keyword>\C_export_file\ "diagnostic C text" (Scan.succeed () >> K (C_Module.C_export_file Position.no_range)); in end\ subsection \Syntax for Pure Term\ syntax "_C_translation_unit" :: \cartouche_position \ string\ ("\<^C>\<^sub>u\<^sub>n\<^sub>i\<^sub>t _") syntax "_C_external_declaration" :: \cartouche_position \ string\ ("\<^C>\<^sub>d\<^sub>e\<^sub>c\<^sub>l _") syntax "_C_expression" :: \cartouche_position \ string\ ("\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r _") syntax "_C_statement" :: \cartouche_position \ string\ ("\<^C>\<^sub>s\<^sub>t\<^sub>m\<^sub>t _") syntax "_C" :: \cartouche_position \ string\ ("\<^C> _") parse_translation \ C_Module.C_Term'.parse_translation [ (\<^syntax_const>\_C_translation_unit\, SOME C_Module.C_Term.tok_translation_unit) , (\<^syntax_const>\_C_external_declaration\, SOME C_Module.C_Term.tok_external_declaration) , (\<^syntax_const>\_C_expression\, SOME C_Module.C_Term.tok_expression) , (\<^syntax_const>\_C_statement\, SOME C_Module.C_Term.tok_statement) , (\<^syntax_const>\_C\, NONE) ] \ end diff --git a/thys/Isabelle_Meta_Model/toy_example/embedding/Generator_dynamic_sequential.thy b/thys/Isabelle_Meta_Model/toy_example/embedding/Generator_dynamic_sequential.thy --- a/thys/Isabelle_Meta_Model/toy_example/embedding/Generator_dynamic_sequential.thy +++ b/thys/Isabelle_Meta_Model/toy_example/embedding/Generator_dynamic_sequential.thy @@ -1,1716 +1,1716 @@ (****************************************************************************** * Citadelle * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France * 2013-2017 IRT SystemX, France * 2011-2015 Achim D. Brucker, Germany * 2016-2018 The University of Sheffield, UK * 2016-2017 Nanyang Technological University, Singapore * 2017-2018 Virginia Tech, USA * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: * * * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above * copyright notice, this list of conditions and the following * disclaimer in the documentation and/or other materials provided * with the distribution. * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) section\Dynamic Meta Embedding with Reflection\ theory Generator_dynamic_sequential imports Printer "../../isabelle_home/src/HOL/Isabelle_Main2" (*<*) keywords (* Toy language *) "Between" "Attributes" "Operations" "Constraints" "Role" "Ordered" "Subsets" "Union" "Redefines" "Derived" "Qualifier" "Existential" "Inv" "Pre" "Post" "self" "Nonunique" "Sequence_" (* Isabelle syntax *) "output_directory" "THEORY" "IMPORTS" "SECTION" "SORRY" "no_dirty" "deep" "shallow" "syntax_print" "skip_export" "generation_semantics" "flush_all" (* Isabelle semantics (parameterizing the semantics of Toy language) *) "design" "analysis" "oid_start" and (* Toy language *) "Enum" "Abstract_class" "Class" "Association" "Composition" "Aggregation" "Abstract_associationclass" "Associationclass" "Context" "End" "Instance" "BaseType" "State" "PrePost" (* Isabelle syntax *) "generation_syntax" :: thy_decl (*>*) begin text\In the ``dynamic'' solution: the exportation is automatically handled inside Isabelle/jEdit. Inputs are provided using the syntax of the Toy Language, and in output we basically have two options: \begin{itemize} \item The first is to generate an Isabelle file for inspection or debugging. The generated file can interactively be loaded in Isabelle/jEdit, or saved to the hard disk. This mode is called the ``deep exportation'' mode or shortly the ``deep'' mode. The aim is to maximally automate the process one is manually performing in @{file \Generator_static.thy\}. \item On the other hand, it is also possible to directly execute in Isabelle/jEdit the generated file from the random access memory. This mode corresponds to the ``shallow reflection'' mode or shortly ``shallow'' mode. \end{itemize} In both modes, the reflection is necessary since the main part used by both was defined at Isabelle side. As a consequence, experimentations in ``deep'' and ``shallow'' are performed without leaving the editing session, in the same as the one the meta-compiler is actually running.\ apply_code_printing_reflect \ val stdout_file = Unsynchronized.ref "" \ text\This variable is not used in this theory (only in @{file \Generator_static.thy\}), but needed for well typechecking the reflected SML code.\ code_reflect' open META functions (* executing the compiler as monadic combinators for deep and shallow *) fold_thy_deep fold_thy_shallow (* printing the HOL AST to (shallow Isabelle) string *) write_file (* manipulating the compiling environment *) compiler_env_config_reset_all compiler_env_config_update oidInit D_output_header_thy_update map2_ctxt_term check_export_code (* printing the TOY AST to (deep Isabelle) string *) isabelle_apply isabelle_of_compiler_env_config subsection\Interface Between the Reflected and the Native\ ML\ val To_string0 = META.meta_of_logic \ ML\ structure From = struct val string = META.SS_base o META.ST val binding = string o Binding.name_of (*fun term ctxt s = string (XML.content_of (YXML.parse_body (Syntax.string_of_term ctxt s)))*) val internal_oid = META.Oid o Code_Numeral.natural_of_integer val option = Option.map val list = List.map fun pair f1 f2 (x, y) = (f1 x, f2 y) fun pair3 f1 f2 f3 (x, y, z) = (f1 x, f2 y, f3 z) structure Pure = struct val indexname = pair string Code_Numeral.natural_of_integer val class = string val sort = list class fun typ e = (fn Type (s, l) => (META.Type o pair string (list typ)) (s, l) | TFree (s, s0) => (META.TFree o pair string sort) (s, s0) | TVar (i, s0) => (META.TVar o pair indexname sort) (i, s0) ) e fun term e = (fn Const (s, t) => (META.Const o pair string typ) (s, t) | Free (s, t) => (META.Free o pair string typ) (s, t) | Var (i, t) => (META.Var o pair indexname typ) (i, t) | Bound i => (META.Bound o Code_Numeral.natural_of_integer) i | Abs (s, ty, t) => (META.Abs o pair3 string typ term) (s, ty, t) | op $ (term1, term2) => (META.App o pair term term) (term1, term2) ) e end fun toy_ctxt_term thy expr = META.T_pure (Pure.term (Syntax.read_term (Proof_Context.init_global thy) expr)) end \ ML\fun List_mapi f = META.mapi (f o Code_Numeral.integer_of_natural)\ ML\ structure Ty' = struct fun check l_oid l = let val Mp = META.map_prod val Me = String.explode val Mi = String.implode val Ml = map in META.check_export_code (writeln o Mi) (warning o Mi) (fn s => writeln (Markup.markup (Markup.bad ()) (Mi s))) (error o To_string0) (Ml (Mp I Me) l_oid) ((META.SS_base o META.ST) l) end end \ subsection\Binding of the Reflected API to the Native API\ ML\ structure META_overload = struct val of_semi__typ = META.of_semi_typ To_string0 val of_semi__term = META.of_semi_terma To_string0 val of_semi__term' = META.of_semi_term To_string0 val fold = fold end \ ML\ structure Bind_Isabelle = struct fun To_binding s = Binding.make (s, Position.none) val To_sbinding = To_binding o To_string0 fun semi__method_simp g f = Method.Basic (fn ctxt => SIMPLE_METHOD (g (asm_full_simp_tac (f ctxt)))) val semi__method_simp_one = semi__method_simp (fn f => f 1) val semi__method_simp_all = semi__method_simp (CHANGED_PROP o PARALLEL_ALLGOALS) datatype semi__thm' = Thms_single' of thm | Thms_mult' of thm list fun semi__thm_attribute ctxt = let open META open META_overload val S = fn Thms_single' t => t val M = fn Thms_mult' t => t in fn Thm_thm s => Thms_single' (Proof_Context.get_thm ctxt (To_string0 s)) | Thm_thms s => Thms_mult' (Proof_Context.get_thms ctxt (To_string0 s)) | Thm_THEN (e1, e2) => (case (semi__thm_attribute ctxt e1, semi__thm_attribute ctxt e2) of (Thms_single' e1, Thms_single' e2) => Thms_single' (e1 RSN (1, e2)) | (Thms_mult' e1, Thms_mult' e2) => Thms_mult' (e1 RLN (1, e2))) | Thm_simplified (e1, e2) => Thms_single' (asm_full_simplify (clear_simpset ctxt addsimps [S (semi__thm_attribute ctxt e2)]) (S (semi__thm_attribute ctxt e1))) | Thm_OF (e1, e2) => Thms_single' ([S (semi__thm_attribute ctxt e2)] MRS (S (semi__thm_attribute ctxt e1))) | Thm_where (nth, l) => Thms_single' (Rule_Insts.where_rule ctxt (List.map (fn (var, expr) => (((To_string0 var, 0), Position.none), of_semi__term expr)) l) [] (S (semi__thm_attribute ctxt nth))) | Thm_symmetric e1 => let val e2 = S (semi__thm_attribute ctxt (Thm_thm (From.string "sym"))) in case semi__thm_attribute ctxt e1 of Thms_single' e1 => Thms_single' (e1 RSN (1, e2)) | Thms_mult' e1 => Thms_mult' (e1 RLN (1, [e2])) end | Thm_of (nth, l) => Thms_single' (Rule_Insts.of_rule ctxt (List.map (SOME o of_semi__term) l, []) [] (S (semi__thm_attribute ctxt nth))) end fun semi__thm_attribute_single ctxt s = case (semi__thm_attribute ctxt s) of Thms_single' t => t fun semi__thm_mult ctxt = let fun f thy = case (semi__thm_attribute ctxt thy) of Thms_mult' t => t | Thms_single' t => [t] in fn META.Thms_single thy => f thy | META.Thms_mult thy => f thy end fun semi__thm_mult_l ctxt l = List.concat (map (semi__thm_mult ctxt) l) fun semi__method_simp_only l ctxt = clear_simpset ctxt addsimps (semi__thm_mult_l ctxt l) fun semi__method_simp_add_del_split (l_add, l_del, l_split) ctxt = fold Splitter.add_split (semi__thm_mult_l ctxt l_split) (ctxt addsimps (semi__thm_mult_l ctxt l_add) delsimps (semi__thm_mult_l ctxt l_del)) fun semi__method expr = let open META open Method open META_overload in case expr of Method_rule o_s => Basic (fn ctxt => METHOD (HEADGOAL o Classical.rule_tac ctxt (case o_s of NONE => [] | SOME s => [semi__thm_attribute_single ctxt s]))) | Method_drule s => Basic (fn ctxt => drule ctxt 0 [semi__thm_attribute_single ctxt s]) | Method_erule s => Basic (fn ctxt => erule ctxt 0 [semi__thm_attribute_single ctxt s]) | Method_elim s => Basic (fn ctxt => elim ctxt [semi__thm_attribute_single ctxt s]) | Method_intro l => Basic (fn ctxt => intro ctxt (map (semi__thm_attribute_single ctxt) l)) | Method_subst (asm, l, s) => Basic (fn ctxt => SIMPLE_METHOD' ((if asm then EqSubst.eqsubst_asm_tac else EqSubst.eqsubst_tac) ctxt (map (fn s => case Int.fromString (To_string0 s) of SOME i => i) l) [semi__thm_attribute_single ctxt s])) | Method_insert l => Basic (fn ctxt => insert (semi__thm_mult_l ctxt l)) | Method_plus t => Combinator ( no_combinator_info , Repeat1 , [Combinator (no_combinator_info, Then, List.map semi__method t)]) | Method_option t => Combinator ( no_combinator_info , Try , [Combinator (no_combinator_info, Then, List.map semi__method t)]) | Method_or t => Combinator (no_combinator_info, Orelse, List.map semi__method t) | Method_one (Method_simp_only l) => semi__method_simp_one (semi__method_simp_only l) | Method_one (Method_simp_add_del_split l) => semi__method_simp_one (semi__method_simp_add_del_split l) | Method_all (Method_simp_only l) => semi__method_simp_all (semi__method_simp_only l) | Method_all (Method_simp_add_del_split l) => semi__method_simp_all (semi__method_simp_add_del_split l) | Method_auto_simp_add_split (l_simp, l_split) => Basic (fn ctxt => SIMPLE_METHOD (auto_tac (fold (fn (f, l) => fold f l) [(Simplifier.add_simp, semi__thm_mult_l ctxt l_simp) ,(Splitter.add_split, List.map (Proof_Context.get_thm ctxt o To_string0) l_split)] ctxt))) | Method_rename_tac l => Basic (K (SIMPLE_METHOD' (Tactic.rename_tac (List.map To_string0 l)))) | Method_case_tac e => Basic (fn ctxt => SIMPLE_METHOD' (Induct_Tacs.case_tac ctxt (of_semi__term e) [] NONE)) | Method_blast n => Basic (case n of NONE => SIMPLE_METHOD' o blast_tac | SOME lim => fn ctxt => SIMPLE_METHOD' (depth_tac ctxt (Code_Numeral.integer_of_natural lim))) | Method_clarify => Basic (fn ctxt => (SIMPLE_METHOD' (fn i => CHANGED_PROP (clarify_tac ctxt i)))) | Method_metis (l_opt, l) => Basic (fn ctxt => (METHOD oo Metis_Tactic.metis_method) ( (if l_opt = [] then NONE else SOME (map To_string0 l_opt), NONE) , map (semi__thm_attribute_single ctxt) l) ctxt) end fun then_tactic l = let open Method in (Combinator (no_combinator_info, Then, map semi__method l), (Position.none, Position.none)) end fun local_terminal_proof o_by = let open META in case o_by of Command_done => Proof.local_done_proof | Command_sorry => Proof.local_skip_proof true | Command_by l_apply => Proof.local_terminal_proof (then_tactic l_apply, NONE) end fun global_terminal_proof o_by = let open META in case o_by of Command_done => Proof.global_done_proof | Command_sorry => Proof.global_skip_proof true | Command_by l_apply => Proof.global_terminal_proof (then_tactic l_apply, NONE) end fun proof_show_gen f (thes, thes_when) st = st |> Proof.proof (SOME ( Method.Source [Token.make_string ("-", Position.none)] , (Position.none, Position.none))) |> Seq.the_result "" |> f |> Proof.show_cmd (thes_when = []) NONE (K I) [] (if thes_when = [] then [] else [(Binding.empty_atts, map (fn t => (t, [])) thes_when)]) [(Binding.empty_atts, [(thes, [])])] true |> snd val semi__command_state = let open META_overload in fn META.Command_apply_end l => (fn st => st |> Proof.apply_end (then_tactic l) |> Seq.the_result "") end val semi__command_proof = let open META_overload val thesis = "?thesis" fun proof_show f = proof_show_gen f (thesis, []) in fn META.Command_apply l => (fn st => st |> Proof.apply (then_tactic l) |> Seq.the_result "") | META.Command_using l => (fn st => let val ctxt = Proof.context_of st in Proof.using [map (fn s => ([ s], [])) (semi__thm_mult_l ctxt l)] st end) | META.Command_unfolding l => (fn st => let val ctxt = Proof.context_of st in Proof.unfolding [map (fn s => ([s], [])) (semi__thm_mult_l ctxt l)] st end) | META.Command_let (e1, e2) => proof_show (Proof.let_bind_cmd [([of_semi__term e1], of_semi__term e2)]) | META.Command_have (n, b, e, e_pr) => proof_show (fn st => st |> Proof.have_cmd true NONE (K I) [] [] [( (To_sbinding n, if b then [[Token.make_string ("simp", Position.none)]] else []) , [(of_semi__term e, [])])] true |> snd |> local_terminal_proof e_pr) | META.Command_fix_let (l, l_let, o_exp, _) => proof_show_gen ( fold (fn (e1, e2) => Proof.let_bind_cmd [([of_semi__term e1], of_semi__term e2)]) l_let o Proof.fix_cmd (List.map (fn i => (To_sbinding i, NONE, NoSyn)) l)) ( case o_exp of NONE => thesis | SOME (l_spec, _) => (String.concatWith (" \ ") (List.map of_semi__term l_spec)) , case o_exp of NONE => [] | SOME (_, l_when) => List.map of_semi__term l_when) end fun semi__theory in_theory in_local = let open META open META_overload in (*let val f = *)fn Theory_datatype (Datatype (n, l)) => in_local (BNF_FP_Def_Sugar.co_datatype_cmd BNF_Util.Least_FP BNF_LFP.construct_lfp (Ctr_Sugar.default_ctr_options_cmd, [( ( ( (([], To_sbinding n), NoSyn) , List.map (fn (n, l) => ( ( (To_binding "", To_sbinding n) , List.map (fn s => (To_binding "", of_semi__typ s)) l) , NoSyn)) l) , (To_binding "", To_binding "", To_binding "")) , [])])) | Theory_type_synonym (Type_synonym (n, v, l)) => in_theory (fn thy => let val s_bind = To_sbinding n in (snd o Typedecl.abbrev_global (s_bind, map To_string0 v, NoSyn) (Isabelle_Typedecl.abbrev_cmd0 (SOME s_bind) thy (of_semi__typ l))) thy end) | Theory_type_notation (Type_notation (n, e)) => in_local (Specification.type_notation_cmd true ("", true) [(To_string0 n, Mixfix (Input.string (To_string0 e), [], 1000, Position.no_range))]) | Theory_instantiation (Instantiation (n, n_def, expr)) => in_theory (fn thy => let val name = To_string0 n val tycos = [ let val Term.Type (s, _) = (Isabelle_Typedecl.abbrev_cmd0 NONE thy name) in s end ] in thy |> Class.instantiation (tycos, [], Syntax.read_sort (Proof_Context.init_global thy) "object") |> fold_map (fn _ => fn thy => let val ((_, (_, ty)), thy) = Specification.definition_cmd NONE [] [] ((To_binding (To_string0 n_def ^ "_" ^ name ^ "_def"), []) , of_semi__term expr) false thy in (ty, thy) end) tycos |-> Class.prove_instantiation_exit_result (map o Morphism.thm) (fn ctxt => fn thms => Class.intro_classes_tac ctxt [] THEN ALLGOALS (Proof_Context.fact_tac ctxt thms)) |-> K I end) | Theory_overloading (Overloading (n_c, e_c, n, e)) => in_theory (fn thy => thy |> Overloading.overloading_cmd [(To_string0 n_c, of_semi__term e_c, true)] |> snd o Specification.definition_cmd NONE [] [] ((To_sbinding n, []), of_semi__term e) false |> Local_Theory.exit_global) | Theory_consts (Consts (n, ty, symb)) => in_theory (Sign.add_consts_cmd [( To_sbinding n , of_semi__typ ty , Mixfix (Input.string ("(_) " ^ To_string0 symb), [], 1000, Position.no_range))]) | Theory_definition def => in_local let val (def, e) = case def of Definition e => (NONE, e) | Definition_where1 (name, (abbrev, prio), e) => (SOME ( To_sbinding name , NONE , Mixfix (Input.string ("(1" ^ of_semi__term abbrev ^ ")"), [], Code_Numeral.integer_of_natural prio, Position.no_range)), e) | Definition_where2 (name, abbrev, e) => (SOME ( To_sbinding name , NONE , Mixfix (Input.string ("(" ^ of_semi__term abbrev ^ ")"), [], 1000, Position.no_range)), e) in (snd o Specification.definition_cmd def [] [] (Binding.empty_atts, of_semi__term e) false) end | Theory_lemmas (Lemmas_simp_thm (simp, s, l)) => in_local (fn lthy => (snd o Specification.theorems Thm.theoremK [((To_sbinding s, List.map (fn s => Attrib.check_src lthy [Token.make_string (s, Position.none)]) (if simp then ["simp", "code_unfold"] else [])), List.map (fn x => ([semi__thm_attribute_single lthy x], [])) l)] [] false) lthy) | Theory_lemmas (Lemmas_simp_thms (s, l)) => in_local (fn lthy => (snd o Specification.theorems Thm.theoremK [((To_sbinding s, List.map (fn s => Attrib.check_src lthy [Token.make_string (s, Position.none)]) ["simp", "code_unfold"]), List.map (fn x => (Proof_Context.get_thms lthy (To_string0 x), [])) l)] [] false) lthy) | Theory_lemma (Lemma (n, l_spec, l_apply, o_by)) => in_local (fn lthy => Specification.theorem_cmd true Thm.theoremK NONE (K I) Binding.empty_atts [] [] (Element.Shows [((To_sbinding n, []) ,[((String.concatWith (" \ ") (List.map of_semi__term l_spec)), [])])]) false lthy |> fold (semi__command_proof o META.Command_apply) l_apply |> global_terminal_proof o_by) | Theory_lemma (Lemma_assumes (n, l_spec, concl, l_apply, o_by)) => in_local (fn lthy => lthy |> Specification.theorem_cmd true Thm.theoremK NONE (K I) (To_sbinding n, []) [] (List.map (fn (n, (b, e)) => Element.Assumes [( ( To_sbinding n , if b then [[Token.make_string ("simp", Position.none)]] else []) , [(of_semi__term e, [])])]) l_spec) (Element.Shows [(Binding.empty_atts, [(of_semi__term concl, [])])]) false |> fold semi__command_proof l_apply |> (case map_filter (fn META.Command_let _ => SOME [] | META.Command_have _ => SOME [] | META.Command_fix_let (_, _, _, l) => SOME l | _ => NONE) (rev l_apply) of [] => global_terminal_proof o_by | _ :: l => let val arg = (NONE, true) in fn st => st |> local_terminal_proof o_by |> fold (fn l => fold semi__command_state l o Proof.local_qed arg) l |> Proof.global_qed arg end)) | Theory_axiomatization (Axiomatization (n, e)) => in_theory (#2 o Specification.axiomatization_cmd [] [] [] [((To_sbinding n, []), of_semi__term e)]) | Theory_section _ => in_theory I | Theory_text _ => in_theory I | Theory_ML (SML ml) => in_theory (Code_printing.reflect_ml (Input.source false (of_semi__term' ml) (Position.none, Position.none))) | Theory_setup (Setup ml) => in_theory (Isar_Cmd.setup (Input.source false (of_semi__term' ml) (Position.none, Position.none))) | Theory_thm (Thm thm) => in_local (fn lthy => let val () = writeln (Pretty.string_of (Proof_Context.pretty_fact lthy ("", List.map (semi__thm_attribute_single lthy) thm))) in lthy end) | Theory_interpretation (Interpretation (n, loc_n, loc_param, o_by)) => in_local (fn lthy => lthy |> Interpretation.interpretation_cmd ( [ ( (To_string0 loc_n, Position.none) , ( (To_string0 n, true) , (if loc_param = [] then Expression.Named [] else Expression.Positional (map (SOME o of_semi__term) loc_param), [])))] , []) |> global_terminal_proof o_by) (*in fn t => fn thy => f t thy handle ERROR s => (warning s; thy) end*) end end structure Bind_META = struct open Bind_Isabelle fun all_meta aux ret = let open META open META_overload in fn META_semi_theories thy => ret o (case thy of Theories_one thy => semi__theory I Named_Target.theory_map thy | Theories_locale (data, l) => fn thy => thy |> ( Expression.add_locale_cmd (To_sbinding (META.holThyLocale_name data)) Binding.empty ([], []) (List.concat (map (fn (fixes, assumes) => List.concat [ map (fn (e,ty) => Element.Fixes [( To_binding (of_semi__term e) , SOME (of_semi__typ ty) , NoSyn)]) fixes , case assumes of NONE => [] | SOME (n, e) => [Element.Assumes [( (To_sbinding n, []) , [(of_semi__term e, [])])]]]) (META.holThyLocale_header data))) #> snd) |> fold (fold (semi__theory Local_Theory.background_theory (fn f => Local_Theory.new_group #> f #> Local_Theory.reset_group #> (fn lthy => - #1 (Named_Target.switch NONE (Context.Proof lthy)) lthy + #1 (Target_Context.switch_named_cmd NONE (Context.Proof lthy)) lthy |> Context.the_proof)))) l |> Local_Theory.exit_global) | META_boot_generation_syntax _ => ret o I | META_boot_setup_env _ => ret o I | META_all_meta_embedding meta => fn thy => aux (map2_ctxt_term (fn T_pure x => T_pure x | e => let fun aux e = case e of T_to_be_parsed (s, _) => SOME let val t = Syntax.read_term (Proof_Context.init_global thy) (To_string0 s) in (t, Term.add_frees t []) end | T_lambda (a, e) => Option.map (fn (e, l_free) => let val a = To_string0 a val (t, l_free) = case List.partition (fn (x, _) => x = a) l_free of ([], l_free) => (Term.TFree ("'a", ["HOL.type"]), l_free) | ([(_, t)], l_free) => (t, l_free) in (lambda (Term.Free (a, t)) e, l_free) end) (aux e) | _ => NONE in case aux e of NONE => error "nested pure expression not expected" | SOME (e, _) => META.T_pure (From.Pure.term e) end) meta) thy end end \ (*<*) subsection\Directives of Compilation for Target Languages\ ML\ structure Deep0 = struct fun apply_hs_code_identifiers ml_module thy = let fun mod_hs (fic, ml_module) = Code_Symbol.Module (fic, [("Haskell", SOME ml_module)]) in fold (Code_Target.set_identifiers o mod_hs) (map (fn x => (Context.theory_name x, ml_module)) (* list of .hs files that will be merged together in "ml_module" *) ( thy :: (* we over-approximate the set of compiler files *) Context.ancestors_of thy)) thy end val default_key = "" structure Export_code_env = struct structure Isabelle = struct val function = "write_file" val argument_main = "main" end structure Haskell = struct val function = "Function" val argument = "Argument" val main = "Main" structure Filename = struct fun hs_function ext = function ^ "." ^ ext fun hs_argument ext = argument ^ "." ^ ext fun hs_main ext = main ^ "." ^ ext end end structure OCaml = struct val make = "write" structure Filename = struct fun function ext = "function." ^ ext fun argument ext = "argument." ^ ext fun main_fic ext = "main." ^ ext fun makefile ext = make ^ "." ^ ext end end structure Scala = struct structure Filename = struct fun function ext = "Function." ^ ext fun argument ext = "Argument." ^ ext end end structure SML = struct val main = "Run" structure Filename = struct fun function ext = "Function." ^ ext fun argument ext = "Argument." ^ ext fun stdout ext = "Stdout." ^ ext fun main_fic ext = main ^ "." ^ ext end end datatype file_input = File | Directory end fun compile l cmd = let val (l, rc) = fold (fn cmd => (fn (l, 0) => let val {out, err, rc, ...} = Bash.process cmd in ((out, err) :: l, rc) end | x => x)) l ([], 0) val l = rev l in if rc = 0 then (l, Isabelle_System.bash_output cmd) else let val () = fold (fn (out, err) => K (warning err; writeln out)) l () in error "Compilation failed" end end val check = fold (fn (cmd, msg) => fn () => let val (out, rc) = Isabelle_System.bash_output cmd in if rc = 0 then () else ( writeln out ; error msg) end) val compiler = let open Export_code_env in [ let val ml_ext = "hs" in ( "Haskell", ml_ext, Directory, Haskell.Filename.hs_function , check [("ghc --version", "ghc is not installed (required for compiling a Haskell project)")] , (fn mk_fic => fn ml_module => fn mk_free => fn thy => File.write (mk_fic ("Main." ^ ml_ext)) (String.concatWith "; " [ "import qualified Unsafe.Coerce" , "import qualified " ^ Haskell.function , "import qualified " ^ Haskell.argument , "main :: IO ()" , "main = " ^ Haskell.function ^ "." ^ Isabelle.function ^ " (Unsafe.Coerce.unsafeCoerce " ^ Haskell.argument ^ "." ^ mk_free (Proof_Context.init_global thy) Isabelle.argument_main ([]: (string * string) list) ^ ")"])) , fn tmp_export_code => fn tmp_file => compile [ "mv " ^ tmp_file ^ "/" ^ Haskell.Filename.hs_argument ml_ext ^ " " ^ Path.implode tmp_export_code , "cd " ^ Path.implode tmp_export_code ^ " && ghc -outputdir _build " ^ Haskell.Filename.hs_main ml_ext ] (Path.implode (Path.append tmp_export_code (Path.make [Haskell.main])))) end , let val ml_ext = "ml" in ( "OCaml", ml_ext, File, OCaml.Filename.function , check [("ocp-build -version", "ocp-build is not installed (required for compiling an OCaml project)") ,("ocamlopt -version", "ocamlopt is not installed (required for compiling an OCaml project)")] , fn mk_fic => fn ml_module => fn mk_free => fn thy => let val () = File.write (mk_fic (OCaml.Filename.makefile "ocp")) (String.concat [ "comp += \"-g\" link += \"-g\" " , "begin generated = true begin library \"nums\" end end " , "begin program \"", OCaml.make, "\" sort = true files = [ \"", OCaml.Filename.function ml_ext , "\" \"", OCaml.Filename.argument ml_ext , "\" \"", OCaml.Filename.main_fic ml_ext , "\" ]" , "requires = [\"nums\"] " , "end" ]) in File.write (mk_fic (OCaml.Filename.main_fic ml_ext)) ("let _ = Function." ^ ml_module ^ "." ^ Isabelle.function ^ " (Obj.magic (Argument." ^ ml_module ^ "." ^ mk_free (Proof_Context.init_global thy) Isabelle.argument_main ([]: (string * string) list) ^ "))") end , fn tmp_export_code => fn tmp_file => compile [ "mv " ^ tmp_file ^ " " ^ Path.implode (Path.append tmp_export_code (Path.make [OCaml.Filename.argument ml_ext])) , "cd " ^ Path.implode tmp_export_code ^ " && ocp-build -init -scan -no-bytecode 2>&1" ] (Path.implode (Path.append tmp_export_code (Path.make [ "_obuild" , OCaml.make , OCaml.make ^ ".asm"])))) end , let val ml_ext = "scala" val ml_module = Unsynchronized.ref ("", "") in ( "Scala", ml_ext, File, Scala.Filename.function , check [("scala -e 0", "scala is not installed (required for compiling a Scala project)")] , (fn _ => fn ml_mod => fn mk_free => fn thy => ml_module := (ml_mod, mk_free (Proof_Context.init_global thy) Isabelle.argument_main ([]: (string * string) list))) , fn tmp_export_code => fn tmp_file => let val l = File.read_lines (Path.explode tmp_file) val (ml_module, ml_main) = Unsynchronized.! ml_module val () = File.write_list (Path.append tmp_export_code (Path.make [Scala.Filename.argument ml_ext])) (List.map (fn s => s ^ "\n") ("object " ^ ml_module ^ " { def main (__ : Array [String]) = " ^ ml_module ^ "." ^ Isabelle.function ^ " (" ^ ml_module ^ "." ^ ml_main ^ ")" :: l @ ["}"])) in compile [] ("scala -nowarn " ^ Path.implode (Path.append tmp_export_code (Path.make [Scala.Filename.argument ml_ext]))) end) end , let val ml_ext_thy = "thy" val ml_ext_ml = "ML" in ( "SML", ml_ext_ml, File, SML.Filename.function , check [ let val isa = "isabelle" in ( Path.implode (Path.expand (Path.append (Path.variable "ISABELLE_HOME") (Path.make ["bin", isa]))) ^ " version" , isa ^ " is not installed (required for compiling a SML project)") end ] , fn mk_fic => fn ml_module => fn mk_free => fn thy => let val esc_star = "*" fun ml l = List.concat [ [ "ML{" ^ esc_star ] , map (fn s => s ^ ";") l , [ esc_star ^ "}"] ] val () = let val fic = mk_fic (SML.Filename.function ml_ext_ml) in (* replace ("\\" ^ "<") by ("\\\060") in 'fic' *) File.write_list fic (map (fn s => (if s = "" then "" else String.concatWith "\\" (map (fn s => let val l = String.size s in if l > 0 andalso String.sub (s,0) = #"<" then "\\060" ^ String.substring (s, 1, String.size s - 1) else s end) (String.fields (fn c => c = #"\\") s))) ^ "\n") (File.read_lines fic)) end in File.write_list (mk_fic (SML.Filename.main_fic ml_ext_thy)) (map (fn s => s ^ "\n") (List.concat [ [ "theory " ^ SML.main , "imports Main" , "begin" , "declare [[ML_print_depth = 500]]" (* any large number so that @{make_string} displays all the expression *) ] , ml [ "val stdout_file = Unsynchronized.ref (File.read (Path.make [\"" ^ SML.Filename.stdout ml_ext_ml ^ "\"]))" , "use \"" ^ SML.Filename.argument ml_ext_ml ^ "\"" ] , ml let val arg = "argument" in [ "val " ^ arg ^ " = XML.content_of (YXML.parse_body (@{make_string} (" ^ ml_module ^ "." ^ mk_free (Proof_Context.init_global thy) Isabelle.argument_main ([]: (string * string) list) ^ ")))" , "use \"" ^ SML.Filename.function ml_ext_ml ^ "\"" , "ML_Context.eval_source (ML_Compiler.verbose false ML_Compiler.flags) (Input.source false (\"let open " ^ ml_module ^ " in " ^ Isabelle.function ^ " (\" ^ " ^ arg ^ " ^ \") end\") (Position.none, Position.none) )" ] end , [ "end" ]])) end , fn tmp_export_code => fn tmp_file => let val stdout_file = Isabelle_System.create_tmp_path "stdout_file" "thy" val () = File.write (Path.append tmp_export_code (Path.make [SML.Filename.stdout ml_ext_ml])) (Path.implode (Path.expand stdout_file)) val (l, (_, exit_st)) = compile [ "mv " ^ tmp_file ^ " " ^ Path.implode (Path.append tmp_export_code (Path.make [SML.Filename.argument ml_ext_ml])) , "cd " ^ Path.implode tmp_export_code ^ " && echo 'use_thy \"" ^ SML.main ^ "\";' | " ^ Path.implode (Path.expand (Path.append (Path.variable "ISABELLE_HOME") (Path.make ["bin", "isabelle"]))) ^ " console" ] "true" val stdout = case try File.read stdout_file of SOME s => let val () = File.rm stdout_file in s end | NONE => "" in (l, (stdout, if List.exists (fn (err, _) => List.exists (fn "*** Error" => true | _ => false) (String.tokens (fn #"\n" => true | _ => false) err)) l then let val () = fold (fn (out, err) => K (warning err; writeln out)) l () in 1 end else exit_st)) end) end ] end structure Find = struct fun ext ml_compiler = case List.find (fn (ml_compiler0, _, _, _, _, _, _) => ml_compiler0 = ml_compiler) compiler of SOME (_, ext, _, _, _, _, _) => ext fun export_mode ml_compiler = case List.find (fn (ml_compiler0, _, _, _, _, _, _) => ml_compiler0 = ml_compiler) compiler of SOME (_, _, mode, _, _, _, _) => mode fun function ml_compiler = case List.find (fn (ml_compiler0, _, _, _, _, _, _) => ml_compiler0 = ml_compiler) compiler of SOME (_, _, _, f, _, _, _) => f fun check_compil ml_compiler = case List.find (fn (ml_compiler0, _, _, _, _, _, _) => ml_compiler0 = ml_compiler) compiler of SOME (_, _, _, _, build, _, _) => build fun init ml_compiler = case List.find (fn (ml_compiler0, _, _, _, _, _, _) => ml_compiler0 = ml_compiler) compiler of SOME (_, _, _, _, _, build, _) => build fun build ml_compiler = case List.find (fn (ml_compiler0, _, _, _, _, _, _) => ml_compiler0 = ml_compiler) compiler of SOME (_, _, _, _, _, _, build) => build end end \ ML\ structure Deep = struct fun absolute_path filename thy = Path.implode (Path.append (Resources.master_directory thy) (Path.explode filename)) fun export_code_tmp_file seris g = fold (fn ((ml_compiler, ml_module), export_arg) => fn f => fn g => f (fn accu => let val tmp_name = Context.theory_name @{theory} in (if Deep0.Find.export_mode ml_compiler = Deep0.Export_code_env.Directory then Isabelle_System.with_tmp_dir tmp_name else Isabelle_System.with_tmp_file tmp_name (Deep0.Find.ext ml_compiler)) (fn filename => g (((((ml_compiler, ml_module), Path.implode filename), export_arg) :: accu))) end)) seris (fn f => f []) (g o rev) fun mk_path_export_code tmp_export_code ml_compiler i = Path.append tmp_export_code (Path.make [ml_compiler ^ Int.toString i]) fun export_code_cmd' seris tmp_export_code f_err filename_thy raw_cs thy = export_code_tmp_file seris (fn seris => let val mem_scala = List.exists (fn ((("Scala", _), _), _) => true | _ => false) seris val thy' (* FIXME unused *) = Isabelle_Code_Target.export_code_cmd false (if mem_scala then Deep0.Export_code_env.Isabelle.function :: raw_cs else raw_cs) ((map o apfst o apsnd) SOME seris) (let val v = Deep0.apply_hs_code_identifiers Deep0.Export_code_env.Haskell.argument thy in if mem_scala then Code_printing.apply_code_printing v else v end) in List_mapi (fn i => fn seri => case seri of (((ml_compiler, _), filename), _) => let val (l, (out, err)) = Deep0.Find.build ml_compiler (mk_path_export_code tmp_export_code ml_compiler i) filename val _ = f_err seri err in (l, out) end) seris end) fun mk_term ctxt s = fst (Scan.pass (Context.Proof ctxt) Args.term (Token.explode0 (Thy_Header.get_keywords' ctxt) s)) fun mk_free ctxt s l = let val t_s = mk_term ctxt s in if Term.is_Free t_s then s else let val l = (s, "") :: l in mk_free ctxt (fst (hd (Term.variant_frees t_s l))) l end end val list_all_eq = fn x0 :: xs => List.all (fn x1 => x0 = x1) xs end \ subsection\Saving the History of Meta Commands\ ML\ fun p_gen f g = f "[" "]" g (*|| f "{" "}" g*) || f "(" ")" g fun paren f = p_gen (fn s1 => fn s2 => fn f => Parse.$$$ s1 |-- f --| Parse.$$$ s2) f fun parse_l f = Parse.$$$ "[" |-- Parse.!!! (Parse.list f --| Parse.$$$ "]") fun parse_l' f = Parse.$$$ "[" |-- Parse.list f --| Parse.$$$ "]" fun parse_l1' f = Parse.$$$ "[" |-- Parse.list1 f --| Parse.$$$ "]" fun annot_ty f = Parse.$$$ "(" |-- f --| Parse.$$$ "::" -- Parse.binding --| Parse.$$$ ")" \ ML\ structure Generation_mode = struct datatype internal_deep = Internal_deep of (string * (string list (* imports *) * string (* import optional (bootstrap) *))) option * ((bstring (* compiler *) * bstring (* main module *) ) * Token.T list) list (* seri_args *) * bstring option (* filename_thy *) * Path.T (* tmp dir export_code *) * bool (* true: skip preview of code exportation *) datatype 'a generation_mode = Gen_deep of unit META.compiler_env_config_ext * internal_deep | Gen_shallow of unit META.compiler_env_config_ext * 'a (* theory init *) | Gen_syntax_print of int option structure Data_gen = Theory_Data (type T = theory generation_mode list Symtab.table val empty = Symtab.empty val extend = I val merge = Symtab.merge (K true)) val code_expr_argsP = Scan.optional (@{keyword "("} |-- Parse.args --| @{keyword ")"}) [] val parse_scheme = @{keyword "design"} >> K META.Gen_only_design || @{keyword "analysis"} >> K META.Gen_only_analysis val parse_sorry_mode = Scan.optional ( @{keyword "SORRY"} >> K (SOME META.Gen_sorry) || @{keyword "no_dirty"} >> K (SOME META.Gen_no_dirty)) NONE val parse_deep = Scan.optional (@{keyword "skip_export"} >> K true) false -- Scan.optional (((Parse.$$$ "(" -- @{keyword "THEORY"}) |-- Parse.name -- ((Parse.$$$ ")" -- Parse.$$$ "(" -- @{keyword "IMPORTS"}) |-- parse_l' Parse.name -- Parse.name) --| Parse.$$$ ")") >> SOME) NONE -- Scan.optional (@{keyword "SECTION"} >> K true) false -- parse_sorry_mode -- (* code_expr_inP *) parse_l1' (@{keyword "in"} |-- (Parse.name -- Scan.optional (@{keyword "module_name"} |-- Parse.name) "" -- code_expr_argsP)) -- Scan.optional ((Parse.$$$ "(" -- @{keyword "output_directory"}) |-- Parse.name --| Parse.$$$ ")" >> SOME) NONE val parse_semantics = let val z = 0 in Scan.optional (paren (@{keyword "generation_semantics"} |-- paren (parse_scheme -- Scan.optional ((Parse.$$$ "," -- @{keyword "oid_start"}) |-- Parse.nat) z))) (META.Gen_default, z) end val mode = let fun mk_env output_disable_thy output_header_thy oid_start design_analysis sorry_mode dirty = META.compiler_env_config_empty output_disable_thy (From.option (From.pair From.string (From.pair (From.list From.string) From.string)) output_header_thy) (META.oidInit (From.internal_oid oid_start)) design_analysis (sorry_mode, dirty) in @{keyword "deep"} |-- parse_semantics -- parse_deep >> (fn ( (design_analysis, oid_start) , ( ((((skip_exportation, output_header_thy), output_disable_thy), sorry_mode), seri_args) , filename_thy)) => fn ctxt => Gen_deep ( mk_env (not output_disable_thy) output_header_thy oid_start design_analysis sorry_mode (Config.get ctxt quick_and_dirty) , Internal_deep ( output_header_thy , seri_args , filename_thy , Isabelle_System.create_tmp_path "deep_export_code" "" , skip_exportation))) || @{keyword "shallow"} |-- parse_semantics -- parse_sorry_mode >> (fn ((design_analysis, oid_start), sorry_mode) => fn ctxt => Gen_shallow ( mk_env true NONE oid_start design_analysis sorry_mode (Config.get ctxt quick_and_dirty) , ())) || (@{keyword "syntax_print"} |-- Scan.optional (Parse.number >> SOME) NONE) >> (fn n => K (Gen_syntax_print (case n of NONE => NONE | SOME n => Int.fromString n))) end fun f_command l_mode = Toplevel.theory (fn thy => let val (l_mode, thy) = META.mapM (fn Gen_shallow (env, ()) => let val thy0 = thy in fn thy => (Gen_shallow (env, thy0), thy) end | Gen_syntax_print n => (fn thy => (Gen_syntax_print n, thy)) | Gen_deep (env, Internal_deep ( output_header_thy , seri_args , filename_thy , tmp_export_code , skip_exportation)) => fn thy => let val _ = warning ("After closing Isabelle/jEdit, we may still need to remove this directory (by hand): " ^ Path.implode (Path.expand tmp_export_code)) val seri_args' = List_mapi (fn i => fn ((ml_compiler, ml_module), export_arg) => let val tmp_export_code = Deep.mk_path_export_code tmp_export_code ml_compiler i fun mk_fic s = Path.append tmp_export_code (Path.make [s]) val () = Deep0.Find.check_compil ml_compiler () val _ = Isabelle_System.make_directory tmp_export_code in ((( (ml_compiler, ml_module) , Path.implode (if Deep0.Find.export_mode ml_compiler = Deep0.Export_code_env.Directory then tmp_export_code else mk_fic (Deep0.Find.function ml_compiler (Deep0.Find.ext ml_compiler)))) , export_arg), mk_fic) end) seri_args val thy' (* FIXME unused *) = Isabelle_Code_Target.export_code_cmd (List.exists (fn (((("SML", _), _), _), _) => true | _ => false) seri_args') [Deep0.Export_code_env.Isabelle.function] (List.map ((apfst o apsnd) SOME o fst) seri_args') (Code_printing.apply_code_printing (Deep0.apply_hs_code_identifiers Deep0.Export_code_env.Haskell.function thy)) val () = fold (fn ((((ml_compiler, ml_module), _), _), mk_fic) => fn _ => Deep0.Find.init ml_compiler mk_fic ml_module Deep.mk_free thy) seri_args' () in (Gen_deep (env, Internal_deep ( output_header_thy , seri_args , filename_thy , tmp_export_code , skip_exportation)), thy) end) let val ctxt = Proof_Context.init_global thy in map (fn f => f ctxt) l_mode end thy in Data_gen.map (Symtab.map_default (Deep0.default_key, l_mode) (fn _ => l_mode)) thy end) fun update_compiler_config f = Data_gen.map (Symtab.map_entry Deep0.default_key (fn l_mode => map (fn Gen_deep (env, d) => Gen_deep (META.compiler_env_config_update f env, d) | Gen_shallow (env, thy) => Gen_shallow (META.compiler_env_config_update f env, thy) | Gen_syntax_print n => Gen_syntax_print n) l_mode)) end \ subsection\Factoring All Meta Commands Together\ setup\ML_Antiquotation.inline @{binding mk_string} (Scan.succeed "(fn ctxt => fn x => ML_Pretty.string_of_polyml (ML_system_pretty (x, FixedInt.fromInt (Config.get ctxt (ML_Print_Depth.print_depth)))))") \ ML\ fun exec_deep (env, output_header_thy, seri_args, filename_thy, tmp_export_code, l_obj) thy0 = let open Generation_mode in let val of_arg = META.isabelle_of_compiler_env_config META.isabelle_apply I in let fun def s = Named_Target.theory_map (snd o Specification.definition_cmd NONE [] [] (Binding.empty_atts, s) false) in let val name_main = Deep.mk_free (Proof_Context.init_global thy0) Deep0.Export_code_env.Isabelle.argument_main [] in thy0 |> def (String.concatWith " " ( "(" (* polymorphism weakening needed by export_code *) ^ name_main ^ " :: (_ \ abr_string option) compiler_env_config_scheme)" :: "=" :: To_string0 (of_arg (META.compiler_env_config_more_map (fn () => (l_obj, From.option From.string (Option.map (fn filename_thy => Deep.absolute_path filename_thy thy0) filename_thy))) env)) :: [])) |> Deep.export_code_cmd' seri_args tmp_export_code (fn (((_, _), msg), _) => fn err => if err <> 0 then error msg else ()) filename_thy [name_main] |> (fn l => let val (l_warn, l) = (map fst l, map snd l) in if Deep.list_all_eq l then (List.concat l_warn, hd l) else error "There is an extracted language which does not produce a similar Isabelle content as the others" end) |> (fn (l_warn, s) => let val () = writeln (case (output_header_thy, filename_thy) of (SOME _, SOME _) => s | _ => String.concat (map ( (fn s => s ^ "\n") o Active.sendback_markup_command o trim_line) (String.tokens (fn c => c = #"\t") s))) in fold (fn (out, err) => K ( writeln (Markup.markup Markup.keyword2 err) ; case trim_line out of "" => () | out => writeln (Markup.markup Markup.keyword1 out))) l_warn () end) end end end end fun outer_syntax_command0 mk_string cmd_spec cmd_descr parser get_all_meta_embed = let open Generation_mode in Outer_Syntax.command cmd_spec cmd_descr (parser >> (fn name => Toplevel.theory (fn thy => let val (env, thy) = META.mapM let val get_all_meta_embed = get_all_meta_embed name in fn Gen_syntax_print n => (fn thy => let val _ = writeln (mk_string (Proof_Context.init_global (case n of NONE => thy | SOME n => Config.put_global ML_Print_Depth.print_depth n thy)) name) in (Gen_syntax_print n, thy) end) | Gen_deep (env, Internal_deep ( output_header_thy , seri_args , filename_thy , tmp_export_code , skip_exportation)) => (fn thy0 => let val l_obj = get_all_meta_embed thy0 in thy0 |> (if skip_exportation then K () else exec_deep ( META.d_output_header_thy_update (fn _ => NONE) env , output_header_thy , seri_args , NONE , tmp_export_code , l_obj)) |> K (Gen_deep ( META.fold_thy_deep l_obj env , Internal_deep ( output_header_thy , seri_args , filename_thy , tmp_export_code , skip_exportation)), thy0) end) | Gen_shallow (env, thy0) => fn thy => let fun aux (env, thy) x = META.fold_thy_shallow (fn f => f () handle ERROR e => ( warning "Shallow Backtracking: (true) Isabelle declarations occurring among the META-simulated ones are ignored (if any)" (* TODO automatically determine if there is such Isabelle declarations, for raising earlier a specific error message *) ; error e)) (fn _ => fn _ => thy0) (fn l => fn (env, thy) => Bind_META.all_meta (fn x => fn thy => aux (env, thy) [x]) (pair env) l thy) x (env, thy) val (env, thy) = aux (env, thy) (get_all_meta_embed thy) in (Gen_shallow (env, thy0), thy) end end (case Symtab.lookup (Data_gen.get thy) Deep0.default_key of SOME l => l | _ => [Gen_syntax_print NONE]) thy in Data_gen.map (Symtab.update (Deep0.default_key, env)) thy end))) end fun outer_syntax_command mk_string cmd_spec cmd_descr parser get_all_meta_embed = outer_syntax_command0 mk_string cmd_spec cmd_descr parser (fn a => fn thy => [get_all_meta_embed a thy]) \ subsection\Parameterizing the Semantics of Embedded Languages\ ML\ val () = let open Generation_mode in Outer_Syntax.command @{command_keyword generation_syntax} "set the generating list" (( mode >> (fn x => SOME [x]) || parse_l' mode >> SOME || @{keyword "deep"} -- @{keyword "flush_all"} >> K NONE) >> (fn SOME x => f_command x | NONE => Toplevel.theory (fn thy => let val l = case Symtab.lookup (Data_gen.get thy) Deep0.default_key of SOME l => l | _ => [] val l = List.concat (List.map (fn Gen_deep x => [x] | _ => []) l) val _ = case l of [] => warning "Nothing to perform." | _ => () val thy = fold (fn (env, Internal_deep (output_header_thy, seri_args, filename_thy, tmp_export_code, _)) => fn thy0 => thy0 |> let val (env, l_exec) = META.compiler_env_config_reset_all env in exec_deep (env, output_header_thy, seri_args, filename_thy, tmp_export_code, l_exec) end |> K thy0) l thy in thy end))) end \ subsection\Common Parser for Toy\ ML\ structure TOY_parse = struct datatype ('a, 'b) use_context = TOY_context_invariant of 'a | TOY_context_pre_post of 'b fun optional f = Scan.optional (f >> SOME) NONE val colon = Parse.$$$ ":" fun repeat2 scan = scan ::: Scan.repeat1 scan fun xml_unescape s = (XML.content_of (YXML.parse_body s), Position.none) |> Symbol_Pos.explode |> Symbol_Pos.implode |> From.string fun outer_syntax_command2 mk_string cmd_spec cmd_descr parser v_true v_false get_all_meta_embed = outer_syntax_command mk_string cmd_spec cmd_descr (optional (paren @{keyword "shallow"}) -- parser) (fn (is_shallow, use) => fn thy => get_all_meta_embed (if is_shallow = NONE then ( fn s => META.T_to_be_parsed ( From.string s , xml_unescape s) , v_true) else (From.toy_ctxt_term thy, v_false)) use) (* *) val ident_dot_dot = let val f = Parse.sym_ident >> (fn "\" => "\" | _ => Scan.fail "Syntax error") in f -- f end val ident_star = Parse.sym_ident (* "*" *) (* *) val unlimited_natural = ident_star >> (fn "*" => META.Mult_star | "\" => META.Mult_infinity | _ => Scan.fail "Syntax error") || Parse.number >> (fn s => META.Mult_nat (case Int.fromString s of SOME i => Code_Numeral.natural_of_integer i | NONE => Scan.fail "Syntax error")) val term_base = Parse.number >> (META.ToyDefInteger o From.string) || Parse.float_number >> (META.ToyDefReal o (From.pair From.string From.string o (fn s => case String.tokens (fn #"." => true | _ => false) s of [l1,l2] => (l1,l2) | _ => Scan.fail "Syntax error"))) || Parse.string >> (META.ToyDefString o From.string) val multiplicity = parse_l' (unlimited_natural -- optional (ident_dot_dot |-- unlimited_natural)) fun toy_term x = ( term_base >> META.ShallB_term || Parse.binding >> (META.ShallB_str o From.binding) || @{keyword "self"} |-- Parse.nat >> (fn n => META.ShallB_self (From.internal_oid n)) || paren (Parse.list toy_term) >> (* untyped, corresponds to Set, Sequence or Pair *) (* WARNING for Set: we are describing a finite set *) META.ShallB_list) x val name_object = optional (Parse.list1 Parse.binding --| colon) -- Parse.binding val type_object_weak = let val name_object = Parse.binding >> (fn s => (NONE, s)) in name_object -- Scan.repeat (Parse.$$$ "<" |-- Parse.list1 name_object) >> let val f = fn (_, s) => META.ToyTyCore_pre (From.binding s) in fn (s, l) => META.ToyTyObj (f s, map (map f) l) end end val type_object = name_object -- Scan.repeat (Parse.$$$ "<" |-- Parse.list1 name_object) >> let val f = fn (_, s) => META.ToyTyCore_pre (From.binding s) in fn (s, l) => META.ToyTyObj (f s, map (map f) l) end val category = multiplicity -- optional (@{keyword "Role"} |-- Parse.binding) -- Scan.repeat ( @{keyword "Ordered"} >> K META.Ordered0 || @{keyword "Subsets"} |-- Parse.binding >> K META.Subsets0 || @{keyword "Union"} >> K META.Union0 || @{keyword "Redefines"} |-- Parse.binding >> K META.Redefines0 || @{keyword "Derived"} -- Parse.$$$ "=" |-- Parse.term >> K META.Derived0 || @{keyword "Qualifier"} |-- Parse.term >> K META.Qualifier0 || @{keyword "Nonunique"} >> K META.Nonunique0 || @{keyword "Sequence_"} >> K META.Sequence) >> (fn ((l_mult, role), l) => META.Toy_multiplicity_ext (l_mult, From.option From.binding role, l, ())) val type_base = Parse.reserved "Void" >> K META.ToyTy_base_void || Parse.reserved "Boolean" >> K META.ToyTy_base_boolean || Parse.reserved "Integer" >> K META.ToyTy_base_integer || Parse.reserved "UnlimitedNatural" >> K META.ToyTy_base_unlimitednatural || Parse.reserved "Real" >> K META.ToyTy_base_real || Parse.reserved "String" >> K META.ToyTy_base_string fun use_type_gen type_object v = ((* collection *) Parse.reserved "Set" |-- use_type >> (fn l => META.ToyTy_collection (META.Toy_multiplicity_ext ([], NONE, [META.Set], ()), l)) || Parse.reserved "Sequence" |-- use_type >> (fn l => META.ToyTy_collection (META.Toy_multiplicity_ext ([], NONE, [META.Sequence], ()), l)) || category -- use_type >> META.ToyTy_collection (* pair *) || Parse.reserved "Pair" |-- ( use_type -- use_type || Parse.$$$ "(" |-- use_type --| Parse.$$$ "," -- use_type --| Parse.$$$ ")") >> META.ToyTy_pair (* base *) || type_base (* raw HOL *) || Parse.sym_ident (* "\" *) |-- Parse.typ --| Parse.sym_ident (* "\" *) >> (META.ToyTy_raw o xml_unescape) (* object type *) || type_object >> META.ToyTy_object || ((Parse.$$$ "(" |-- Parse.list ( (Parse.binding --| colon >> (From.option From.binding o SOME)) -- ( Parse.$$$ "(" |-- use_type --| Parse.$$$ ")" || use_type_gen type_object_weak) >> META.ToyTy_binding ) --| Parse.$$$ ")" >> (fn ty_arg => case rev ty_arg of [] => META.ToyTy_base_void | ty_arg => fold (fn x => fn acc => META.ToyTy_pair (x, acc)) (tl ty_arg) (hd ty_arg))) -- optional (colon |-- use_type)) >> (fn (ty_arg, ty_out) => case ty_out of NONE => ty_arg | SOME ty_out => META.ToyTy_arrow (ty_arg, ty_out)) || (Parse.$$$ "(" |-- use_type --| Parse.$$$ ")" >> (fn s => META.ToyTy_binding (NONE, s)))) v and use_type x = use_type_gen type_object x val use_prop = (optional (optional (Parse.binding >> From.binding) --| Parse.$$$ ":") >> (fn NONE => NONE | SOME x => x)) -- Parse.term --| optional (Parse.$$$ ";") >> (fn (n, e) => fn from_expr => META.ToyProp_ctxt (n, from_expr e)) (* *) val association_end = type_object -- category --| optional (Parse.$$$ ";") val association = optional @{keyword "Between"} |-- Scan.optional (repeat2 association_end) [] val invariant = optional @{keyword "Constraints"} |-- Scan.optional (@{keyword "Existential"} >> K true) false --| @{keyword "Inv"} -- use_prop structure Outer_syntax_Association = struct fun make ass_ty l = META.Toy_association_ext (ass_ty, META.ToyAssRel l, ()) end (* *) val context = Scan.repeat (( optional (@{keyword "Operations"} || Parse.$$$ "::") |-- Parse.binding -- use_type --| optional (Parse.$$$ "=" |-- Parse.term || Parse.term) -- Scan.repeat ( (@{keyword "Pre"} || @{keyword "Post"}) -- use_prop >> TOY_context_pre_post || invariant >> TOY_context_invariant) --| optional (Parse.$$$ ";")) >> (fn ((name_fun, ty), expr) => fn from_expr => META.Ctxt_pp (META.Toy_ctxt_pre_post_ext ( From.binding name_fun , ty , From.list (fn TOY_context_pre_post (pp, expr) => META.T_pp (if pp = "Pre" then META.ToyCtxtPre else META.ToyCtxtPost, expr from_expr) | TOY_context_invariant (b, expr) => META.T_invariant (META.T_inv (b, expr from_expr))) expr , ()))) || invariant >> (fn (b, expr) => fn from_expr => META.Ctxt_inv (META.T_inv (b, expr from_expr)))) val class = optional @{keyword "Attributes"} |-- Scan.repeat (Parse.binding --| colon -- use_type --| optional (Parse.$$$ ";")) -- context datatype use_classDefinition = TOY_class | TOY_class_abstract datatype ('a, 'b) use_classDefinition_content = TOY_class_content of 'a | TOY_class_synonym of 'b structure Outer_syntax_Class = struct fun make from_expr abstract ty_object attribute oper = META.Toy_class_raw_ext ( ty_object , From.list (From.pair From.binding I) attribute , From.list (fn f => f from_expr) oper , abstract , ()) end (* *) val term_object = parse_l ( optional ( Parse.$$$ "(" |-- Parse.binding --| Parse.$$$ "," -- Parse.binding --| Parse.$$$ ")" --| (Parse.sym_ident >> (fn "|=" => Scan.succeed | _ => Scan.fail ""))) -- Parse.binding -- ( Parse.$$$ "=" |-- toy_term)) val list_attr' = term_object >> (fn res => (res, [] : binding list)) fun object_cast e = ( annot_ty term_object -- Scan.repeat ( (Parse.sym_ident >> (fn "->" => Scan.succeed | "\" => Scan.succeed | "\" => Scan.succeed | _ => Scan.fail "")) |-- ( Parse.reserved "toyAsType" |-- Parse.$$$ "(" |-- Parse.binding --| Parse.$$$ ")" || Parse.binding)) >> (fn ((res, x), l) => (res, rev (x :: l)))) e val object_cast' = object_cast >> (fn (res, l) => (res, rev l)) fun get_toyinst l _ = META.ToyInstance (map (fn ((name,typ), (l_attr, is_cast)) => let val f = map (fn ((pre_post, attr), data) => ( From.option (From.pair From.binding From.binding) pre_post , ( From.binding attr , data))) val l_attr = fold (fn b => fn acc => META.ToyAttrCast (From.binding b, acc, [])) is_cast (META.ToyAttrNoCast (f l_attr)) in META.Toy_instance_single_ext (From.option From.binding name, From.option From.binding typ, l_attr, ()) end) l) val parse_instance = (Parse.binding >> SOME) -- optional (@{keyword "::"} |-- Parse.binding) --| @{keyword "="} -- (list_attr' || object_cast') (* *) datatype state_content = ST_l_attr of (((binding * binding) option * binding) * META.toy_data_shallow) list * binding list | ST_binding of binding val state_parse = parse_l' ( object_cast >> ST_l_attr || Parse.binding >> ST_binding) fun mk_state thy = map (fn ST_l_attr l => META.ToyDefCoreAdd (case get_toyinst (map (fn (l_i, l_ty) => ((NONE, SOME (hd l_ty)), (l_i, rev (tl l_ty)))) [l]) thy of META.ToyInstance [x] => x) | ST_binding b => META.ToyDefCoreBinding (From.binding b)) (* *) datatype state_pp_content = ST_PP_l_attr of state_content list | ST_PP_binding of binding val state_pp_parse = state_parse >> ST_PP_l_attr || Parse.binding >> ST_PP_binding fun mk_pp_state thy = fn ST_PP_l_attr l => META.ToyDefPPCoreAdd (mk_state thy l) | ST_PP_binding s => META.ToyDefPPCoreBinding (From.binding s) end \ subsection\Setup of Meta Commands for Toy: Enum\ ML\ val () = outer_syntax_command @{mk_string} @{command_keyword Enum} "" (Parse.binding -- parse_l1' Parse.binding) (fn (n1, n2) => K (META.META_enum (META.ToyEnum (From.binding n1, From.list From.binding n2)))) \ subsection\Setup of Meta Commands for Toy: (abstract) Class\ ML\ local open TOY_parse fun mk_classDefinition abstract cmd_spec = outer_syntax_command2 @{mk_string} cmd_spec "Class generation" ( Parse.binding --| Parse.$$$ "=" -- TOY_parse.type_base >> TOY_class_synonym || type_object -- class >> TOY_class_content) (curry META.META_class_raw META.Floor1) (curry META.META_class_raw META.Floor2) (fn (from_expr, META_class_raw) => fn TOY_class_content (ty_object, (attribute, oper)) => META_class_raw (Outer_syntax_Class.make from_expr (abstract = TOY_class_abstract) ty_object attribute oper) | TOY_class_synonym (n1, n2) => META.META_class_synonym (META.ToyClassSynonym (From.binding n1, n2))) in val () = mk_classDefinition TOY_class @{command_keyword Class} val () = mk_classDefinition TOY_class_abstract @{command_keyword Abstract_class} end \ subsection\Setup of Meta Commands for Toy: Association, Composition, Aggregation\ ML\ local open TOY_parse fun mk_associationDefinition ass_ty cmd_spec = outer_syntax_command @{mk_string} cmd_spec "" ( repeat2 association_end || optional Parse.binding |-- association) (fn l => fn _ => META.META_association (Outer_syntax_Association.make ass_ty l)) in val () = mk_associationDefinition META.ToyAssTy_association @{command_keyword Association} val () = mk_associationDefinition META.ToyAssTy_composition @{command_keyword Composition} val () = mk_associationDefinition META.ToyAssTy_aggregation @{command_keyword Aggregation} end \ subsection\Setup of Meta Commands for Toy: (abstract) Associationclass\ ML\ local open TOY_parse datatype use_associationClassDefinition = TOY_associationclass | TOY_associationclass_abstract fun mk_associationClassDefinition abstract cmd_spec = outer_syntax_command2 @{mk_string} cmd_spec "" ( type_object -- association -- class -- optional (Parse.reserved "aggregation" || Parse.reserved "composition")) (curry META.META_ass_class META.Floor1) (curry META.META_ass_class META.Floor2) (fn (from_expr, META_ass_class) => fn (((ty_object, l_ass), (attribute, oper)), assty) => META_ass_class (META.ToyAssClass ( Outer_syntax_Association.make (case assty of SOME "aggregation" => META.ToyAssTy_aggregation | SOME "composition" => META.ToyAssTy_composition | _ => META.ToyAssTy_association) l_ass , Outer_syntax_Class.make from_expr (abstract = TOY_associationclass_abstract) ty_object attribute oper))) in val () = mk_associationClassDefinition TOY_associationclass @{command_keyword Associationclass} val () = mk_associationClassDefinition TOY_associationclass_abstract @{command_keyword Abstract_associationclass} end \ subsection\Setup of Meta Commands for Toy: Context\ ML\ local open TOY_parse in val () = outer_syntax_command2 @{mk_string} @{command_keyword Context} "" (optional (Parse.list1 Parse.binding --| colon) -- Parse.binding -- context) (curry META.META_ctxt META.Floor1) (curry META.META_ctxt META.Floor2) (fn (from_expr, META_ctxt) => (fn ((l_param, name), l) => META_ctxt (META.Toy_ctxt_ext ( case l_param of NONE => [] | SOME l => From.list From.binding l , META.ToyTyObj (META.ToyTyCore_pre (From.binding name), []) , From.list (fn f => f from_expr) l , ())))) end \ subsection\Setup of Meta Commands for Toy: End\ ML\ val () = outer_syntax_command0 @{mk_string} @{command_keyword End} "Class generation" (Scan.optional ( Parse.$$$ "[" -- Parse.reserved "forced" -- Parse.$$$ "]" >> K true || Parse.$$$ "!" >> K true) false) (fn b => fn _ => if b then [META.META_flush_all META.ToyFlushAll] else []) \ subsection\Setup of Meta Commands for Toy: BaseType, Instance, State\ ML\ val () = outer_syntax_command @{mk_string} @{command_keyword BaseType} "" (parse_l' TOY_parse.term_base) (K o META.META_def_base_l o META.ToyDefBase) local open TOY_parse in val () = outer_syntax_command @{mk_string} @{command_keyword Instance} "" (Scan.optional (parse_instance -- Scan.repeat (optional @{keyword "and"} |-- parse_instance) >> (fn (x, xs) => x :: xs)) []) (META.META_instance oo get_toyinst) val () = outer_syntax_command @{mk_string} @{command_keyword State} "" (TOY_parse.optional (paren @{keyword "shallow"}) -- Parse.binding --| @{keyword "="} -- state_parse) (fn ((is_shallow, name), l) => fn thy => META.META_def_state ( if is_shallow = NONE then META.Floor1 else META.Floor2 , META.ToyDefSt (From.binding name, mk_state thy l))) end \ subsection\Setup of Meta Commands for Toy: PrePost\ ML\ local open TOY_parse in val () = outer_syntax_command @{mk_string} @{command_keyword PrePost} "" (TOY_parse.optional (paren @{keyword "shallow"}) -- TOY_parse.optional (Parse.binding --| @{keyword "="}) -- state_pp_parse -- TOY_parse.optional state_pp_parse) (fn (((is_shallow, n), s_pre), s_post) => fn thy => META.META_def_pre_post ( if is_shallow = NONE then META.Floor1 else META.Floor2 , META.ToyDefPP ( From.option From.binding n , mk_pp_state thy s_pre , From.option (mk_pp_state thy) s_post))) end (*val _ = print_depth 100*) \ (*>*) end