diff --git a/src/Pure/Isar/code.ML b/src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML +++ b/src/Pure/Isar/code.ML @@ -1,1587 +1,1587 @@ (* Title: Pure/Isar/code.ML Author: Florian Haftmann, TU Muenchen Abstract executable ingredients of theory. Management of data dependent on executable ingredients as synchronized cache; purged on any change of underlying executable ingredients. *) signature CODE = sig (*constants*) val check_const: theory -> term -> string val read_const: theory -> string -> string val string_of_const: theory -> string -> string val args_number: theory -> string -> int (*constructor sets*) val constrset_of_consts: theory -> (string * typ) list -> string * ((string * sort) list * (string * ((string * sort) list * typ list)) list) (*code equations and certificates*) val assert_eqn: theory -> thm * bool -> thm * bool val assert_abs_eqn: theory -> string option -> thm -> thm * (string * string) type cert val constrain_cert: theory -> sort list -> cert -> cert val conclude_cert: cert -> cert val typargs_deps_of_cert: theory -> cert -> (string * sort) list * (string * typ list) list val equations_of_cert: theory -> cert -> ((string * sort) list * typ) * (((term * string option) list * (term * string option)) * (thm option * bool)) list option val pretty_cert: theory -> cert -> Pretty.T list (*executable code*) type constructors type abs_type val type_interpretation: (string -> theory -> theory) -> theory -> theory val datatype_interpretation: (string * constructors -> theory -> theory) -> theory -> theory val abstype_interpretation: (string * abs_type -> theory -> theory) -> theory -> theory val declare_datatype_global: (string * typ) list -> theory -> theory val declare_datatype_cmd: string list -> theory -> theory val declare_abstype: thm -> local_theory -> local_theory val declare_abstype_global: thm -> theory -> theory val declare_default_eqns: (thm * bool) list -> local_theory -> local_theory val declare_default_eqns_global: (thm * bool) list -> theory -> theory val declare_eqns: (thm * bool) list -> local_theory -> local_theory val declare_eqns_global: (thm * bool) list -> theory -> theory val add_eqn_global: thm * bool -> theory -> theory val del_eqn_global: thm -> theory -> theory val declare_abstract_eqn: thm -> local_theory -> local_theory val declare_abstract_eqn_global: thm -> theory -> theory val declare_aborting_global: string -> theory -> theory val declare_unimplemented_global: string -> theory -> theory val declare_case_global: thm -> theory -> theory val declare_undefined_global: string -> theory -> theory val get_type: theory -> string -> constructors * bool val get_type_of_constr_or_abstr: theory -> string -> (string * bool) option val is_constr: theory -> string -> bool val is_abstr: theory -> string -> bool val get_cert: Proof.context -> ((thm * bool) list -> (thm * bool) list option) list -> string -> cert type case_schema val get_case_schema: theory -> string -> case_schema option val get_case_cong: theory -> string -> thm option val is_undefined: theory -> string -> bool val print_codesetup: theory -> unit end; signature CODE_DATA_ARGS = sig type T val empty: T end; signature CODE_DATA = sig type T val change: theory option -> (T -> T) -> T val change_yield: theory option -> (T -> 'a * T) -> 'a * T end; signature PRIVATE_CODE = sig include CODE val declare_data: Any.T -> serial val change_yield_data: serial * ('a -> Any.T) * (Any.T -> 'a) -> theory -> ('a -> 'b * 'a) -> 'b * 'a end; structure Code : PRIVATE_CODE = struct (** auxiliary **) (* printing *) fun string_of_typ thy = Syntax.string_of_typ (Config.put show_sorts true (Syntax.init_pretty_global thy)); fun string_of_const thy c = let val ctxt = Proof_Context.init_global thy in case Axclass.inst_of_param thy c of SOME (c, tyco) => Proof_Context.extern_const ctxt c ^ " " ^ enclose "[" "]" (Proof_Context.extern_type ctxt tyco) | NONE => Proof_Context.extern_const ctxt c end; (* constants *) fun const_typ thy = Type.strip_sorts o Sign.the_const_type thy; fun args_number thy = length o binder_types o const_typ thy; fun devarify ty = let - val tys = fold_atyps (fn TVar vi_sort => AList.update (op =) vi_sort) ty []; + val tys = build (fold_atyps (fn TVar vi_sort => AList.update (op =) vi_sort) ty); val vs = Name.invent Name.context Name.aT (length tys); val mapping = map2 (fn v => fn (vi, sort) => (vi, TFree (v, sort))) vs tys; in Term.typ_subst_TVars mapping ty end; fun typscheme thy (c, ty) = (map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty); fun typscheme_equiv (ty1, ty2) = Type.raw_instance (devarify ty1, ty2) andalso Type.raw_instance (devarify ty2, ty1); fun check_bare_const thy t = case try dest_Const t of SOME c_ty => c_ty | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t); fun check_unoverload thy (c, ty) = let val c' = Axclass.unoverload_const thy (c, ty); val ty_decl = const_typ thy c'; in if typscheme_equiv (ty_decl, Logic.varifyT_global ty) then c' else error ("Type\n" ^ string_of_typ thy ty ^ "\nof constant " ^ quote c ^ "\nis too specific compared to declared type\n" ^ string_of_typ thy ty_decl) end; fun check_const thy = check_unoverload thy o check_bare_const thy; fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy; fun read_const thy = check_unoverload thy o read_bare_const thy; (** executable specifications **) (* types *) datatype type_spec = Constructors of { constructors: (string * ((string * sort) list * typ list)) list, case_combinators: string list} | Abstractor of { abs_rep: thm, abstractor: string * ((string * sort) list * typ), projection: string, more_abstract_functions: string list}; fun concrete_constructors_of (Constructors {constructors, ...}) = constructors | concrete_constructors_of _ = []; fun constructors_of (Constructors {constructors, ...}) = (constructors, false) | constructors_of (Abstractor {abstractor = (co, (vs, ty)), ...}) = ([(co, (vs, [ty]))], true); fun case_combinators_of (Constructors {case_combinators, ...}) = case_combinators | case_combinators_of (Abstractor _) = []; fun add_case_combinator c (vs, Constructors {constructors, case_combinators}) = (vs, Constructors {constructors = constructors, case_combinators = insert (op =) c case_combinators}); fun projection_of (Constructors _) = NONE | projection_of (Abstractor {projection, ...}) = SOME projection; fun abstract_functions_of (Constructors _) = [] | abstract_functions_of (Abstractor {more_abstract_functions, projection, ...}) = projection :: more_abstract_functions; fun add_abstract_function c (vs, Abstractor {abs_rep, abstractor, projection, more_abstract_functions}) = (vs, Abstractor {abs_rep = abs_rep, abstractor = abstractor, projection = projection, more_abstract_functions = insert (op =) c more_abstract_functions}); fun join_same_types' (Constructors {constructors, case_combinators = case_combinators1}, Constructors {case_combinators = case_combinators2, ...}) = Constructors {constructors = constructors, case_combinators = merge (op =) (case_combinators1, case_combinators2)} | join_same_types' (Abstractor {abs_rep, abstractor, projection, more_abstract_functions = more_abstract_functions1}, Abstractor {more_abstract_functions = more_abstract_functions2, ...}) = Abstractor {abs_rep = abs_rep, abstractor = abstractor, projection = projection, more_abstract_functions = merge (op =) (more_abstract_functions1, more_abstract_functions2)}; fun join_same_types ((vs, spec1), (_, spec2)) = (vs, join_same_types' (spec1, spec2)); (* functions *) datatype fun_spec = Eqns of bool * (thm * bool) list | Proj of term * (string * string) | Abstr of thm * (string * string); val unimplemented = Eqns (true, []); fun is_unimplemented (Eqns (true, [])) = true | is_unimplemented _ = false; fun is_default (Eqns (true, _)) = true | is_default _ = false; val aborting = Eqns (false, []); fun associated_abstype (Proj (_, tyco_abs)) = SOME tyco_abs | associated_abstype (Abstr (_, tyco_abs)) = SOME tyco_abs | associated_abstype _ = NONE; (* cases *) type case_schema = int * (int * string option list); datatype case_spec = No_Case | Case of {schema: case_schema, tycos: string list, cong: thm} | Undefined; fun associated_datatypes (Case {tycos, schema = (_, (_, raw_cos)), ...}) = (tycos, map_filter I raw_cos) | associated_datatypes _ = ([], []); (** background theory data store **) (* historized declaration data *) structure History = struct type 'a T = { entry: 'a, suppressed: bool, (*incompatible entries are merely suppressed after theory merge but sustain*) history: serial list (*explicit trace of declaration history supports non-monotonic declarations*) } Symtab.table; fun some_entry (SOME {suppressed = false, entry, ...}) = SOME entry | some_entry _ = NONE; fun lookup table = Symtab.lookup table #> some_entry; fun register key entry table = if is_some (Symtab.lookup table key) then Symtab.map_entry key (fn {history, ...} => {entry = entry, suppressed = false, history = serial () :: history}) table else Symtab.update (key, {entry = entry, suppressed = false, history = [serial ()]}) table; fun modify_entry key f = Symtab.map_entry key (fn {entry, suppressed, history} => {entry = f entry, suppressed = suppressed, history = history}); fun all table = Symtab.dest table |> map_filter (fn (key, {entry, suppressed = false, ...}) => SOME (key, entry) | _ => NONE); local fun merge_history join_same ({entry = entry1, history = history1, ...}, {entry = entry2, history = history2, ...}) = let val history = merge (op =) (history1, history2); val entry = if hd history1 = hd history2 then join_same (entry1, entry2) else if hd history = hd history1 then entry1 else entry2; in {entry = entry, suppressed = false, history = history} end; in fun join join_same tables = Symtab.join (K (merge_history join_same)) tables; fun suppress key = Symtab.map_entry key (fn {entry, history, ...} => {entry = entry, suppressed = true, history = history}); fun suppress_except f = Symtab.map (fn key => fn {entry, suppressed, history} => {entry = entry, suppressed = suppressed orelse (not o f) (key, entry), history = history}); end; end; datatype specs = Specs of { types: ((string * sort) list * type_spec) History.T, pending_eqns: (thm * bool) list Symtab.table, functions: fun_spec History.T, cases: case_spec History.T }; fun types_of (Specs {types, ...}) = types; fun pending_eqns_of (Specs {pending_eqns, ...}) = pending_eqns; fun functions_of (Specs {functions, ...}) = functions; fun cases_of (Specs {cases, ...}) = cases; fun make_specs (types, ((pending_eqns, functions), cases)) = Specs {types = types, pending_eqns = pending_eqns, functions = functions, cases = cases}; val empty_specs = make_specs (Symtab.empty, ((Symtab.empty, Symtab.empty), Symtab.empty)); fun map_specs f (Specs {types = types, pending_eqns = pending_eqns, functions = functions, cases = cases}) = make_specs (f (types, ((pending_eqns, functions), cases))); fun merge_specs (Specs {types = types1, pending_eqns = _, functions = functions1, cases = cases1}, Specs {types = types2, pending_eqns = _, functions = functions2, cases = cases2}) = let val types = History.join join_same_types (types1, types2); val all_types = map (snd o snd) (History.all types); fun check_abstype (c, fun_spec) = case associated_abstype fun_spec of NONE => true | SOME (tyco, abs) => (case History.lookup types tyco of NONE => false | SOME (_, Constructors _) => false | SOME (_, Abstractor {abstractor = (abs', _), projection, more_abstract_functions, ...}) => abs = abs' andalso (c = projection orelse member (op =) more_abstract_functions c)); fun check_datatypes (_, case_spec) = let val (tycos, required_constructors) = associated_datatypes case_spec; val allowed_constructors = tycos |> maps (these o Option.map (concrete_constructors_of o snd) o History.lookup types) |> map fst; in subset (op =) (required_constructors, allowed_constructors) end; val all_constructors = maps (fst o constructors_of) all_types; val functions = History.join fst (functions1, functions2) |> fold (History.suppress o fst) all_constructors |> History.suppress_except check_abstype; val cases = History.join fst (cases1, cases2) |> History.suppress_except check_datatypes; in make_specs (types, ((Symtab.empty, functions), cases)) end; val map_types = map_specs o apfst; val map_pending_eqns = map_specs o apsnd o apfst o apfst; val map_functions = map_specs o apsnd o apfst o apsnd; val map_cases = map_specs o apsnd o apsnd; (* data slots dependent on executable code *) (*private copy avoids potential conflict of table exceptions*) structure Datatab = Table(type key = int val ord = int_ord); local type kind = {empty: Any.T}; val kinds = Synchronized.var "Code_Data" (Datatab.empty: kind Datatab.table); fun invoke f k = (case Datatab.lookup (Synchronized.value kinds) k of SOME kind => f kind | NONE => raise Fail "Invalid code data identifier"); in fun declare_data empty = let val k = serial (); val kind = {empty = empty}; val _ = Synchronized.change kinds (Datatab.update (k, kind)); in k end; fun invoke_init k = invoke (fn kind => #empty kind) k; end; (*local*) (* global theory store *) local type data = Any.T Datatab.table; fun make_dataref thy = (Context.theory_long_name thy, Synchronized.var "code data" (NONE : (data * Context.theory_id) option)); structure Code_Data = Theory_Data ( type T = specs * (string * (data * Context.theory_id) option Synchronized.var); val empty = (empty_specs, make_dataref (Context.the_global_context ())); fun merge ((specs1, dataref), (specs2, _)) = (merge_specs (specs1, specs2), dataref); ); fun init_dataref thy = if #1 (#2 (Code_Data.get thy)) = Context.theory_long_name thy then NONE else SOME ((Code_Data.map o apsnd) (fn _ => make_dataref thy) thy) in val _ = Theory.setup (Theory.at_begin init_dataref); (* access to executable specifications *) val specs_of : theory -> specs = fst o Code_Data.get; fun modify_specs f thy = Code_Data.map (fn (specs, _) => (f specs, make_dataref thy)) thy; (* access to data dependent on executable specifications *) fun change_yield_data (kind, mk, dest) theory f = let val dataref = #2 (#2 (Code_Data.get theory)); val (datatab, thy_id) = case Synchronized.value dataref of SOME (datatab, thy_id) => if Context.eq_thy_id (Context.theory_id theory, thy_id) then (datatab, thy_id) else (Datatab.empty, Context.theory_id theory) | NONE => (Datatab.empty, Context.theory_id theory) val data = case Datatab.lookup datatab kind of SOME data => data | NONE => invoke_init kind; val result as (_, data') = f (dest data); val _ = Synchronized.change dataref ((K o SOME) (Datatab.update (kind, mk data') datatab, thy_id)); in result end; end; (*local*) (* pending function equations *) (* Ideally, *all* equations implementing a functions would be treated as *one* atomic declaration; unfortunately, we cannot implement this: the too-well-established declaration interface are Isar attributes which operate on *one* single theorem. Hence we treat such Isar declarations as "pending" and historize them as proper declarations at the end of each theory. *) fun modify_pending_eqns c f specs = let val existing_eqns = case History.lookup (functions_of specs) c of SOME (Eqns (false, eqns)) => eqns | _ => []; in specs |> map_pending_eqns (Symtab.map_default (c, existing_eqns) f) end; fun register_fun_spec c spec = map_pending_eqns (Symtab.delete_safe c) #> map_functions (History.register c spec); fun lookup_fun_spec specs c = case Symtab.lookup (pending_eqns_of specs) c of SOME eqns => Eqns (false, eqns) | NONE => (case History.lookup (functions_of specs) c of SOME spec => spec | NONE => unimplemented); fun lookup_proper_fun_spec specs c = let val spec = lookup_fun_spec specs c in if is_unimplemented spec then NONE else SOME spec end; fun all_fun_specs specs = map_filter (fn c => Option.map (pair c) (lookup_proper_fun_spec specs c)) (union (op =) ((Symtab.keys o pending_eqns_of) specs) ((Symtab.keys o functions_of) specs)); fun historize_pending_fun_specs thy = let val pending_eqns = (pending_eqns_of o specs_of) thy; in if Symtab.is_empty pending_eqns then NONE else thy |> modify_specs (map_functions (Symtab.fold (fn (c, eqs) => History.register c (Eqns (false, eqs))) pending_eqns) #> map_pending_eqns (K Symtab.empty)) |> SOME end; val _ = Theory.setup (Theory.at_end historize_pending_fun_specs); (** foundation **) (* types *) fun no_constr thy s (c, ty) = error ("Not a datatype constructor:\n" ^ string_of_const thy c ^ " :: " ^ string_of_typ thy ty ^ "\n" ^ enclose "(" ")" s); fun analyze_constructor thy (c, ty) = let val _ = Thm.global_cterm_of thy (Const (c, ty)); val ty_decl = devarify (const_typ thy c); fun last_typ c_ty ty = let val tfrees = Term.add_tfreesT ty []; val (tyco, vs) = (apsnd o map) dest_TFree (dest_Type (body_type ty)) handle TYPE _ => no_constr thy "bad type" c_ty val _ = if tyco = "fun" then no_constr thy "bad type" c_ty else (); val _ = if has_duplicates (eq_fst (op =)) vs then no_constr thy "duplicate type variables in datatype" c_ty else (); val _ = if length tfrees <> length vs then no_constr thy "type variables missing in datatype" c_ty else (); in (tyco, vs) end; val (tyco, _) = last_typ (c, ty) ty_decl; val (_, vs) = last_typ (c, ty) ty; in ((tyco, map snd vs), (c, (map fst vs, ty))) end; fun constrset_of_consts thy consts = let val _ = map (fn (c, _) => if (is_some o Axclass.class_of_param thy) c then error ("Is a class parameter: " ^ string_of_const thy c) else ()) consts; val raw_constructors = map (analyze_constructor thy) consts; val tyco = case distinct (op =) (map (fst o fst) raw_constructors) of [tyco] => tyco | [] => error "Empty constructor set" | tycos => error ("Different type constructors in constructor set: " ^ commas_quote tycos) val vs = Name.invent Name.context Name.aT (Sign.arity_number thy tyco); fun inst vs' (c, (vs, ty)) = let val the_v = the o AList.lookup (op =) (vs ~~ vs'); val ty' = map_type_tfree (fn (v, _) => TFree (the_v v, [])) ty; val (vs'', ty'') = typscheme thy (c, ty'); in (c, (vs'', binder_types ty'')) end; val constructors = map (inst vs o snd) raw_constructors; in (tyco, (map (rpair []) vs, constructors)) end; fun lookup_vs_type_spec thy = History.lookup ((types_of o specs_of) thy); type constructors = (string * sort) list * (string * ((string * sort) list * typ list)) list; fun get_type thy tyco = case lookup_vs_type_spec thy tyco of SOME (vs, type_spec) => apfst (pair vs) (constructors_of type_spec) | NONE => Sign.arity_number thy tyco |> Name.invent Name.context Name.aT |> map (rpair []) |> rpair [] |> rpair false; type abs_type = (string * sort) list * {abs_rep: thm, abstractor: string * ((string * sort) list * typ), projection: string}; fun get_abstype_spec thy tyco = case lookup_vs_type_spec thy tyco of SOME (vs, Abstractor {abs_rep, abstractor, projection, ...}) => (vs, {abs_rep = abs_rep, abstractor = abstractor, projection = projection}) | _ => error ("Not an abstract type: " ^ tyco); fun get_type_of_constr_or_abstr thy c = case (body_type o const_typ thy) c of Type (tyco, _) => let val ((_, cos), abstract) = get_type thy tyco in if member (op =) (map fst cos) c then SOME (tyco, abstract) else NONE end | _ => NONE; fun is_constr thy c = case get_type_of_constr_or_abstr thy c of SOME (_, false) => true | _ => false; fun is_abstr thy c = case get_type_of_constr_or_abstr thy c of SOME (_, true) => true | _ => false; (* bare code equations *) (* convention for variables: ?x ?'a for free-floating theorems (e.g. in the data store) ?x 'a for certificates x 'a for final representation of equations *) exception BAD_THM of string; fun bad_thm msg = raise BAD_THM msg; datatype strictness = Silent | Liberal | Strict fun handle_strictness thm_of f strictness thy x = SOME (f x) handle BAD_THM msg => case strictness of Silent => NONE | Liberal => (warning (msg ^ ", in theorem:\n" ^ Thm.string_of_thm_global thy (thm_of x)); NONE) | Strict => error (msg ^ ", in theorem:\n" ^ Thm.string_of_thm_global thy (thm_of x)); fun is_linear thm = let val (_, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm in not (has_duplicates (op =) ((fold o fold_aterms) (fn Var (v, _) => cons v | _ => I) args [])) end; fun check_decl_ty thy (c, ty) = let val ty_decl = const_typ thy c; in if typscheme_equiv (ty_decl, ty) then () else bad_thm ("Type\n" ^ string_of_typ thy ty ^ "\nof constant " ^ quote c ^ "\nis too specific compared to declared type\n" ^ string_of_typ thy ty_decl) end; fun check_eqn thy {allow_nonlinear, allow_consts, allow_pats} thm (lhs, rhs) = let fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v | Free _ => bad_thm "Illegal free variable" | _ => I) t []; fun tvars_of t = fold_term_types (fn _ => fold_atyps (fn TVar (v, _) => insert (op =) v | TFree _ => bad_thm "Illegal free type variable")) t []; val lhs_vs = vars_of lhs; val rhs_vs = vars_of rhs; val lhs_tvs = tvars_of lhs; val rhs_tvs = tvars_of rhs; val _ = if null (subtract (op =) lhs_vs rhs_vs) then () else bad_thm "Free variables on right hand side of equation"; val _ = if null (subtract (op =) lhs_tvs rhs_tvs) then () else bad_thm "Free type variables on right hand side of equation"; val (head, args) = strip_comb lhs; val (c, ty) = case head of Const (c_ty as (_, ty)) => (Axclass.unoverload_const thy c_ty, ty) | _ => bad_thm "Equation not headed by constant"; fun check _ (Abs _) = bad_thm "Abstraction on left hand side of equation" | check 0 (Var _) = () | check _ (Var _) = bad_thm "Variable with application on left hand side of equation" | check n (t1 $ t2) = (check (n+1) t1; check 0 t2) | check n (Const (c_ty as (c, ty))) = if allow_pats then let val c' = Axclass.unoverload_const thy c_ty in if n = (length o binder_types) ty then if allow_consts orelse is_constr thy c' then () else bad_thm (quote c ^ " is not a constructor, on left hand side of equation") else bad_thm ("Partially applied constant " ^ quote c ^ " on left hand side of equation") end else bad_thm ("Pattern not allowed here, but constant " ^ quote c ^ " encountered on left hand side of equation") val _ = map (check 0) args; val _ = if allow_nonlinear orelse is_linear thm then () else bad_thm "Duplicate variables on left hand side of equation"; val _ = if (is_none o Axclass.class_of_param thy) c then () else bad_thm "Overloaded constant as head in equation"; val _ = if not (is_constr thy c) then () else bad_thm "Constructor as head in equation"; val _ = if not (is_abstr thy c) then () else bad_thm "Abstractor as head in equation"; val _ = check_decl_ty thy (c, ty); val _ = case strip_type ty of (Type (tyco, _) :: _, _) => (case lookup_vs_type_spec thy tyco of SOME (_, type_spec) => (case projection_of type_spec of SOME proj => if c = proj then bad_thm "Projection as head in equation" else () | _ => ()) | _ => ()) | _ => (); in () end; local fun raw_assert_eqn thy check_patterns (thm, proper) = let val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm handle TERM _ => bad_thm "Not an equation" | THM _ => bad_thm "Not a proper equation"; val _ = check_eqn thy {allow_nonlinear = not proper, allow_consts = not (proper andalso check_patterns), allow_pats = true} thm (lhs, rhs); in (thm, proper) end; fun raw_assert_abs_eqn thy some_tyco thm = let val (full_lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm handle TERM _ => bad_thm "Not an equation" | THM _ => bad_thm "Not a proper equation"; val (proj_t, lhs) = dest_comb full_lhs handle TERM _ => bad_thm "Not an abstract equation"; val (proj, ty) = dest_Const proj_t handle TERM _ => bad_thm "Not an abstract equation"; val (tyco, Ts) = (dest_Type o domain_type) ty handle TERM _ => bad_thm "Not an abstract equation" | TYPE _ => bad_thm "Not an abstract equation"; val _ = case some_tyco of SOME tyco' => if tyco = tyco' then () else bad_thm ("Abstract type mismatch:" ^ quote tyco ^ " vs. " ^ quote tyco') | NONE => (); val (vs, proj', (abs', _)) = case lookup_vs_type_spec thy tyco of SOME (vs, Abstractor spec) => (vs, #projection spec, #abstractor spec) | _ => bad_thm ("Not an abstract type: " ^ tyco); val _ = if proj = proj' then () else bad_thm ("Projection mismatch: " ^ quote proj ^ " vs. " ^ quote proj'); val _ = check_eqn thy {allow_nonlinear = false, allow_consts = false, allow_pats = false} thm (lhs, rhs); val _ = if ListPair.all (fn (T, (_, sort)) => Sign.of_sort thy (T, sort)) (Ts, vs) then () else error ("Type arguments do not satisfy sort constraints of abstype certificate."); in (thm, (tyco, abs')) end; in fun generic_assert_eqn strictness thy check_patterns eqn = handle_strictness fst (raw_assert_eqn thy check_patterns) strictness thy eqn; fun generic_assert_abs_eqn strictness thy check_patterns thm = handle_strictness I (raw_assert_abs_eqn thy check_patterns) strictness thy thm; end; fun assert_eqn thy = the o generic_assert_eqn Strict thy true; fun assert_abs_eqn thy some_tyco = the o generic_assert_abs_eqn Strict thy some_tyco; val head_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of; fun const_typ_eqn thy thm = let val (c, ty) = head_eqn thm; val c' = Axclass.unoverload_const thy (c, ty); (*permissive wrt. to overloaded constants!*) in (c', ty) end; fun const_eqn thy = fst o const_typ_eqn thy; fun const_abs_eqn thy = Axclass.unoverload_const thy o dest_Const o fst o strip_comb o snd o dest_comb o fst o Logic.dest_equals o Thm.plain_prop_of; fun mk_proj tyco vs ty abs rep = let val ty_abs = Type (tyco, map TFree vs); val xarg = Var (("x", 0), ty); in Logic.mk_equals (Const (rep, ty_abs --> ty) $ (Const (abs, ty --> ty_abs) $ xarg), xarg) end; (* technical transformations of code equations *) fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (Proof_Context.init_global thy); fun expand_eta thy k thm = let val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm; val (_, args) = strip_comb lhs; val l = if k = ~1 then (length o fst o strip_abs) rhs else Int.max (0, k - length args); val (raw_vars, _) = Term.strip_abs_eta l rhs; val vars = burrow_fst (Name.variant_list (map (fst o fst) (Term.add_vars lhs []))) raw_vars; fun expand (v, ty) thm = Drule.fun_cong_rule thm (Thm.global_cterm_of thy (Var ((v, 0), ty))); in thm |> fold expand vars |> Conv.fconv_rule Drule.beta_eta_conversion end; fun same_arity thy thms = let val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals; val k = fold (Integer.max o num_args_of o Thm.prop_of) thms 0; in map (expand_eta thy k) thms end; fun mk_desymbolization pre post mk vs = let val names = map (pre o fst o fst) vs |> map (Name.desymbolize (SOME false)) |> Name.variant_list [] |> map post; in map_filter (fn (((v, i), x), v') => if v = v' andalso i = 0 then NONE else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names) end; fun desymbolize_tvars thy thms = let - val tvs = fold (Term.add_tvars o Thm.prop_of) thms []; + val tvs = build (fold (Term.add_tvars o Thm.prop_of) thms); val instT = mk_desymbolization (unprefix "'") (prefix "'") (Thm.global_ctyp_of thy o TVar) tvs; in map (Thm.instantiate (TVars.make instT, Vars.empty)) thms end; fun desymbolize_vars thy thm = let val vs = Term.add_vars (Thm.prop_of thm) []; val inst = mk_desymbolization I I (Thm.global_cterm_of thy o Var) vs; in Thm.instantiate (TVars.empty, Vars.make inst) thm end; fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy); (* preparation and classification of code equations *) fun prep_eqn strictness thy = apfst (meta_rewrite thy) #> generic_assert_eqn strictness thy false #> Option.map (fn eqn => (const_eqn thy (fst eqn), eqn)); fun prep_eqns strictness thy = map_filter (prep_eqn strictness thy) #> AList.group (op =); fun prep_abs_eqn strictness thy = meta_rewrite thy #> generic_assert_abs_eqn strictness thy NONE #> Option.map (fn abs_eqn => (const_abs_eqn thy (fst abs_eqn), abs_eqn)); fun prep_maybe_abs_eqn thy raw_thm = let val thm = meta_rewrite thy raw_thm; val some_abs_thm = generic_assert_abs_eqn Silent thy NONE thm; in case some_abs_thm of SOME (thm, tyco) => SOME (const_abs_eqn thy thm, ((thm, true), SOME tyco)) | NONE => generic_assert_eqn Liberal thy false (thm, false) |> Option.map (fn (thm, _) => (const_eqn thy thm, ((thm, is_linear thm), NONE))) end; (* abstype certificates *) local fun raw_abstype_cert thy proto_thm = let val thm = (Axclass.unoverload (Proof_Context.init_global thy) o meta_rewrite thy) proto_thm; val (lhs, rhs) = Logic.dest_equals (Thm.plain_prop_of thm) handle TERM _ => bad_thm "Not an equation" | THM _ => bad_thm "Not a proper equation"; val ((abs, raw_ty), ((rep, rep_ty), param)) = (apsnd (apfst dest_Const o dest_comb) o apfst dest_Const o dest_comb) lhs handle TERM _ => bad_thm "Not an abstype certificate"; val _ = apply2 (fn c => if (is_some o Axclass.class_of_param thy) c then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep); val _ = check_decl_ty thy (abs, raw_ty); val _ = check_decl_ty thy (rep, rep_ty); val _ = if length (binder_types raw_ty) = 1 then () else bad_thm "Bad type for abstract constructor"; val _ = (fst o dest_Var) param handle TERM _ => bad_thm "Not an abstype certificate"; val _ = if param = rhs then () else bad_thm "Not an abstype certificate"; val ((tyco, sorts), (abs, (vs, ty'))) = analyze_constructor thy (abs, devarify raw_ty); val ty = domain_type ty'; val (vs', _) = typscheme thy (abs, ty'); in (tyco, (vs ~~ sorts, ((abs, (vs', ty)), (rep, thm)))) end; in fun check_abstype_cert strictness thy proto_thm = handle_strictness I (raw_abstype_cert thy) strictness thy proto_thm; end; (* code equation certificates *) fun build_head thy (c, ty) = Thm.global_cterm_of thy (Logic.mk_equals (Free ("HEAD", ty), Const (c, ty))); fun get_head thy cert_thm = let val [head] = Thm.chyps_of cert_thm; val (_, Const (c, ty)) = (Logic.dest_equals o Thm.term_of) head; in (typscheme thy (c, ty), head) end; fun typscheme_projection thy = typscheme thy o dest_Const o fst o dest_comb o fst o Logic.dest_equals; fun typscheme_abs thy = typscheme thy o dest_Const o fst o strip_comb o snd o dest_comb o fst o Logic.dest_equals o Thm.prop_of; fun constrain_thm thy vs sorts thm = let val mapping = map2 (fn (v, sort) => fn sort' => (v, Sorts.inter_sort (Sign.classes_of thy) (sort, sort'))) vs sorts; val instT = TVars.build (fold2 (fn (v, sort) => fn (_, sort') => TVars.add (((v, 0), sort), Thm.global_ctyp_of thy (TFree (v, sort')))) vs mapping); val subst = (Term.map_types o map_type_tfree) (fn (v, _) => TFree (v, the (AList.lookup (op =) mapping v))); in thm |> Thm.varifyT_global |> Thm.instantiate (instT, Vars.empty) |> pair subst end; fun concretify_abs thy tyco abs_thm = let val (_, {abstractor = (c_abs, _), abs_rep, ...}) = get_abstype_spec thy tyco; val lhs = (fst o Logic.dest_equals o Thm.prop_of) abs_thm val ty = fastype_of lhs; val ty_abs = (fastype_of o snd o dest_comb) lhs; val abs = Thm.global_cterm_of thy (Const (c_abs, ty --> ty_abs)); val raw_concrete_thm = Drule.transitive_thm OF [Thm.symmetric abs_rep, Thm.combination (Thm.reflexive abs) abs_thm]; in (c_abs, (Thm.varifyT_global o zero_var_indexes) raw_concrete_thm) end; fun add_rhss_of_eqn thy t = let val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals) t; fun add_const (Const (c, ty)) = insert (op =) (c, Sign.const_typargs thy (c, ty)) | add_const _ = I val add_consts = fold_aterms add_const in add_consts rhs o fold add_consts args end; val dest_eqn = apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify_global; abstype cert = Nothing of thm | Equations of thm * bool list | Projection of term * string | Abstract of thm * string with fun dummy_thm ctxt c = let val thy = Proof_Context.theory_of ctxt; val raw_ty = devarify (const_typ thy c); val (vs, _) = typscheme thy (c, raw_ty); val sortargs = case Axclass.class_of_param thy c of SOME class => [[class]] | NONE => (case get_type_of_constr_or_abstr thy c of SOME (tyco, _) => (map snd o fst o the) (AList.lookup (op =) ((snd o fst o get_type thy) tyco) c) | NONE => replicate (length vs) []); val the_sort = the o AList.lookup (op =) (map fst vs ~~ sortargs); val ty = map_type_tfree (fn (v, _) => TFree (v, the_sort v)) raw_ty val chead = build_head thy (c, ty); in Thm.weaken chead Drule.dummy_thm end; fun nothing_cert ctxt c = Nothing (dummy_thm ctxt c); fun cert_of_eqns ctxt c [] = Equations (dummy_thm ctxt c, []) | cert_of_eqns ctxt c raw_eqns = let val thy = Proof_Context.theory_of ctxt; val eqns = burrow_fst (canonize_thms thy) raw_eqns; val _ = map (assert_eqn thy) eqns; val (thms, propers) = split_list eqns; val _ = map (fn thm => if c = const_eqn thy thm then () else error ("Wrong head of code equation,\nexpected constant " ^ string_of_const thy c ^ "\n" ^ Thm.string_of_thm_global thy thm)) thms; val tvars_of = build_rev o Term.add_tvarsT; val vss = map (tvars_of o snd o head_eqn) thms; - fun inter_sorts vs = - fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs []; + val inter_sorts = + build o fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd); val sorts = map_transpose inter_sorts vss; val vts = Name.invent_names Name.context Name.aT sorts; fun instantiate vs = Thm.instantiate (TVars.make (vs ~~ map (Thm.ctyp_of ctxt o TFree) vts), Vars.empty); val thms' = map2 instantiate vss thms; val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms')))); fun head_conv ct = if can Thm.dest_comb ct then Conv.fun_conv head_conv ct else Conv.rewr_conv head_thm ct; val rewrite_head = Conv.fconv_rule (Conv.arg1_conv head_conv); val cert_thm = Conjunction.intr_balanced (map rewrite_head thms'); in Equations (cert_thm, propers) end; fun cert_of_proj ctxt proj tyco = let val thy = Proof_Context.theory_of ctxt val (vs, {abstractor = (abs, (_, ty)), projection = proj', ...}) = get_abstype_spec thy tyco; val _ = if proj = proj' then () else error ("Wrong head of projection,\nexpected constant " ^ string_of_const thy proj); in Projection (mk_proj tyco vs ty abs proj, tyco) end; fun cert_of_abs ctxt tyco c raw_abs_thm = let val thy = Proof_Context.theory_of ctxt; val abs_thm = singleton (canonize_thms thy) raw_abs_thm; val _ = assert_abs_eqn thy (SOME tyco) abs_thm; val _ = if c = const_abs_eqn thy abs_thm then () else error ("Wrong head of abstract code equation,\nexpected constant " ^ string_of_const thy c ^ "\n" ^ Thm.string_of_thm_global thy abs_thm); in Abstract (Thm.legacy_freezeT abs_thm, tyco) end; fun constrain_cert_thm thy sorts cert_thm = let val ((vs, _), head) = get_head thy cert_thm; val (subst, cert_thm') = cert_thm |> Thm.implies_intr head |> constrain_thm thy vs sorts; val head' = Thm.term_of head |> subst |> Thm.global_cterm_of thy; val cert_thm'' = cert_thm' |> Thm.elim_implies (Thm.assume head'); in cert_thm'' end; fun constrain_cert thy sorts (Nothing cert_thm) = Nothing (constrain_cert_thm thy sorts cert_thm) | constrain_cert thy sorts (Equations (cert_thm, propers)) = Equations (constrain_cert_thm thy sorts cert_thm, propers) | constrain_cert _ _ (cert as Projection _) = cert | constrain_cert thy sorts (Abstract (abs_thm, tyco)) = Abstract (snd (constrain_thm thy (fst (typscheme_abs thy abs_thm)) sorts abs_thm), tyco); fun conclude_cert (Nothing cert_thm) = Nothing (Thm.close_derivation \<^here> cert_thm) | conclude_cert (Equations (cert_thm, propers)) = Equations (Thm.close_derivation \<^here> cert_thm, propers) | conclude_cert (cert as Projection _) = cert | conclude_cert (Abstract (abs_thm, tyco)) = Abstract (Thm.close_derivation \<^here> abs_thm, tyco); fun typscheme_of_cert thy (Nothing cert_thm) = fst (get_head thy cert_thm) | typscheme_of_cert thy (Equations (cert_thm, _)) = fst (get_head thy cert_thm) | typscheme_of_cert thy (Projection (proj, _)) = typscheme_projection thy proj | typscheme_of_cert thy (Abstract (abs_thm, _)) = typscheme_abs thy abs_thm; fun typargs_deps_of_cert thy (Nothing cert_thm) = let val vs = (fst o fst) (get_head thy cert_thm); in (vs, []) end | typargs_deps_of_cert thy (Equations (cert_thm, propers)) = let val vs = (fst o fst) (get_head thy cert_thm); val equations = if null propers then [] else Thm.prop_of cert_thm |> Logic.dest_conjunction_balanced (length propers); - in (vs, fold (add_rhss_of_eqn thy) equations []) end + in (vs, build (fold (add_rhss_of_eqn thy) equations)) end | typargs_deps_of_cert thy (Projection (t, _)) = (fst (typscheme_projection thy t), add_rhss_of_eqn thy t []) | typargs_deps_of_cert thy (Abstract (abs_thm, tyco)) = let val vs = fst (typscheme_abs thy abs_thm); val (_, concrete_thm) = concretify_abs thy tyco abs_thm; in (vs, add_rhss_of_eqn thy (Logic.unvarify_types_global (Thm.prop_of concrete_thm)) []) end; fun equations_of_cert thy (cert as Nothing _) = (typscheme_of_cert thy cert, NONE) | equations_of_cert thy (cert as Equations (cert_thm, propers)) = let val tyscm = typscheme_of_cert thy cert; val thms = if null propers then [] else cert_thm |> Local_Defs.expand [snd (get_head thy cert_thm)] |> Thm.varifyT_global |> Conjunction.elim_balanced (length propers); fun abstractions (args, rhs) = (map (rpair NONE) args, (rhs, NONE)); in (tyscm, SOME (map (abstractions o dest_eqn o Thm.prop_of) thms ~~ (map SOME thms ~~ propers))) end | equations_of_cert thy (Projection (t, tyco)) = let val (_, {abstractor = (abs, _), ...}) = get_abstype_spec thy tyco; val tyscm = typscheme_projection thy t; val t' = Logic.varify_types_global t; fun abstractions (args, rhs) = (map (rpair (SOME abs)) args, (rhs, NONE)); in (tyscm, SOME [((abstractions o dest_eqn) t', (NONE, true))]) end | equations_of_cert thy (Abstract (abs_thm, tyco)) = let val tyscm = typscheme_abs thy abs_thm; val (abs, concrete_thm) = concretify_abs thy tyco abs_thm; fun abstractions (args, rhs) = (map (rpair NONE) args, (rhs, (SOME abs))); in (tyscm, SOME [((abstractions o dest_eqn o Thm.prop_of) concrete_thm, (SOME (Thm.varifyT_global abs_thm), true))]) end; fun pretty_cert _ (Nothing _) = [] | pretty_cert thy (cert as Equations _) = (map_filter (Option.map (Thm.pretty_thm_global thy o Axclass.overload (Proof_Context.init_global thy)) o fst o snd) o these o snd o equations_of_cert thy) cert | pretty_cert thy (Projection (t, _)) = [Syntax.pretty_term_global thy (Logic.varify_types_global t)] | pretty_cert thy (Abstract (abs_thm, _)) = [(Thm.pretty_thm_global thy o Axclass.overload (Proof_Context.init_global thy) o Thm.varifyT_global) abs_thm]; end; (* code certificate access with preprocessing *) fun eqn_conv conv ct = let fun lhs_conv ct = if can Thm.dest_comb ct then Conv.combination_conv lhs_conv conv ct else Conv.all_conv ct; in Conv.combination_conv (Conv.arg_conv lhs_conv) conv ct end; fun rewrite_eqn conv ctxt = singleton (Variable.trade (K (map (Conv.fconv_rule (conv (Simplifier.rewrite ctxt))))) ctxt) fun apply_functrans ctxt functrans = let fun trace_eqns s eqns = (Pretty.writeln o Pretty.chunks) (Pretty.str s :: map (Thm.pretty_thm ctxt o fst) eqns); val tracing = if Config.get ctxt simp_trace then trace_eqns else (K o K) (); in tap (tracing "before function transformation") #> (perhaps o perhaps_loop o perhaps_apply) functrans #> tap (tracing "after function transformation") end; fun preprocess conv ctxt = rewrite_eqn conv ctxt #> Axclass.unoverload ctxt; fun get_cert ctxt functrans c = case lookup_proper_fun_spec (specs_of (Proof_Context.theory_of ctxt)) c of NONE => nothing_cert ctxt c | SOME (Eqns (_, eqns)) => eqns |> (map o apfst) (Thm.transfer' ctxt) |> apply_functrans ctxt functrans |> (map o apfst) (preprocess eqn_conv ctxt) |> cert_of_eqns ctxt c | SOME (Proj (_, (tyco, _))) => cert_of_proj ctxt c tyco | SOME (Abstr (abs_thm, (tyco, _))) => abs_thm |> Thm.transfer' ctxt |> preprocess Conv.arg_conv ctxt |> cert_of_abs ctxt tyco c; (* case certificates *) local fun raw_case_cert thm = let val ((head, raw_case_expr), cases) = (apfst Logic.dest_equals o apsnd Logic.dest_conjunctions o Logic.dest_implies o Thm.plain_prop_of) thm; val _ = case head of Free _ => () | Var _ => () | _ => raise TERM ("case_cert", []); val ([(case_var, _)], case_expr) = Term.strip_abs_eta 1 raw_case_expr; val (Const (case_const, _), raw_params) = strip_comb case_expr; val n = find_index (fn Free (v, _) => v = case_var | _ => false) raw_params; val _ = if n = ~1 then raise TERM ("case_cert", []) else (); val params = map (fst o dest_Var) (nth_drop n raw_params); fun dest_case t = let val (head' $ t_co, rhs) = Logic.dest_equals t; val _ = if head' = head then () else raise TERM ("case_cert", []); val (Const (co, _), args) = strip_comb t_co; val (Var (param, _), args') = strip_comb rhs; val _ = if args' = args then () else raise TERM ("case_cert", []); in (param, co) end; fun analyze_cases cases = let - val co_list = fold (AList.update (op =) o dest_case) cases []; + val co_list = build (fold (AList.update (op =) o dest_case) cases); in map (AList.lookup (op =) co_list) params end; fun analyze_let t = let val (head' $ arg, Var (param', _) $ arg') = Logic.dest_equals t; val _ = if head' = head then () else raise TERM ("case_cert", []); val _ = if arg' = arg then () else raise TERM ("case_cert", []); val _ = if [param'] = params then () else raise TERM ("case_cert", []); in [] end; fun analyze (cases as [let_case]) = (analyze_cases cases handle Bind => analyze_let let_case) | analyze cases = analyze_cases cases; in (case_const, (n, analyze cases)) end; in fun case_cert thm = raw_case_cert thm handle Bind => error "bad case certificate" | TERM _ => error "bad case certificate"; end; fun lookup_case_spec thy = History.lookup ((cases_of o specs_of) thy); fun get_case_schema thy c = case lookup_case_spec thy c of SOME (Case {schema, ...}) => SOME schema | _ => NONE; fun get_case_cong thy c = case lookup_case_spec thy c of SOME (Case {cong, ...}) => SOME cong | _ => NONE; fun is_undefined thy c = case lookup_case_spec thy c of SOME Undefined => true | _ => false; (* diagnostic *) fun print_codesetup thy = let val ctxt = Proof_Context.init_global thy; val specs = specs_of thy; fun pretty_equations const thms = (Pretty.block o Pretty.fbreaks) (Pretty.str (string_of_const thy const) :: map (Thm.pretty_thm_item ctxt) thms); fun pretty_function (const, Eqns (_, eqns)) = pretty_equations const (map fst eqns) | pretty_function (const, Proj (proj, _)) = Pretty.block [Pretty.str (string_of_const thy const), Pretty.fbrk, Syntax.pretty_term ctxt proj] | pretty_function (const, Abstr (thm, _)) = pretty_equations const [thm]; fun pretty_typ (tyco, vs) = Pretty.str (string_of_typ thy (Type (tyco, map TFree vs))); fun pretty_type_spec (typ, (cos, abstract)) = if null cos then pretty_typ typ else (Pretty.block o Pretty.breaks) ( pretty_typ typ :: Pretty.str "=" :: (if abstract then [Pretty.str "(abstract)"] else []) @ separate (Pretty.str "|") (map (fn (c, (_, [])) => Pretty.str (string_of_const thy c) | (c, (_, tys)) => (Pretty.block o Pretty.breaks) (Pretty.str (string_of_const thy c) :: Pretty.str "of" :: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos) ); fun pretty_case_param NONE = "" | pretty_case_param (SOME c) = string_of_const thy c fun pretty_case (const, Case {schema = (_, (_, [])), ...}) = Pretty.str (string_of_const thy const) | pretty_case (const, Case {schema = (_, (_, cos)), ...}) = (Pretty.block o Pretty.breaks) [ Pretty.str (string_of_const thy const), Pretty.str "with", (Pretty.block o Pretty.commas o map (Pretty.str o pretty_case_param)) cos] | pretty_case (const, Undefined) = (Pretty.block o Pretty.breaks) [ Pretty.str (string_of_const thy const), Pretty.str ""]; val functions = all_fun_specs specs |> sort (string_ord o apply2 fst); val types = History.all (types_of specs) |> map (fn (tyco, (vs, spec)) => ((tyco, vs), constructors_of spec)) |> sort (string_ord o apply2 (fst o fst)); val cases = History.all (cases_of specs) |> filter (fn (_, No_Case) => false | _ => true) |> sort (string_ord o apply2 fst); in Pretty.writeln_chunks [ Pretty.block ( Pretty.str "types:" :: Pretty.fbrk :: (Pretty.fbreaks o map pretty_type_spec) types ), Pretty.block ( Pretty.str "functions:" :: Pretty.fbrk :: (Pretty.fbreaks o map pretty_function) functions ), Pretty.block ( Pretty.str "cases:" :: Pretty.fbrk :: (Pretty.fbreaks o map pretty_case) cases ) ] end; (** declaration of executable ingredients **) (* plugins for dependent applications *) structure Codetype_Plugin = Plugin(type T = string); val codetype_plugin = Plugin_Name.declare_setup \<^binding>\codetype\; fun type_interpretation f = Codetype_Plugin.interpretation codetype_plugin (fn tyco => Local_Theory.background_theory (fn thy => thy |> Sign.root_path |> Sign.add_path (Long_Name.qualifier tyco) |> f tyco |> Sign.restore_naming thy)); fun datatype_interpretation f = type_interpretation (fn tyco => fn thy => case get_type thy tyco of (spec, false) => f (tyco, spec) thy | (_, true) => thy ); fun abstype_interpretation f = type_interpretation (fn tyco => fn thy => case try (get_abstype_spec thy) tyco of SOME spec => f (tyco, spec) thy | NONE => thy ); fun register_tyco_for_plugin tyco = Named_Target.theory_map (Codetype_Plugin.data_default tyco); (* abstract code declarations *) local fun generic_code_declaration strictness lift_phi f x = Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => Context.mapping (f strictness (lift_phi phi x)) I); in fun silent_code_declaration lift_phi = generic_code_declaration Silent lift_phi; fun code_declaration lift_phi = generic_code_declaration Liberal lift_phi; end; (* types *) fun invalidate_constructors_of (_, type_spec) = fold (fn (c, _) => History.register c unimplemented) (fst (constructors_of type_spec)); fun invalidate_abstract_functions_of (_, type_spec) = fold (fn c => History.register c unimplemented) (abstract_functions_of type_spec); fun invalidate_case_combinators_of (_, type_spec) = fold (fn c => History.register c No_Case) (case_combinators_of type_spec); fun register_type (tyco, vs_typ_spec) specs = let val olds = the_list (History.lookup (types_of specs) tyco); in specs |> map_functions (fold invalidate_abstract_functions_of olds #> invalidate_constructors_of vs_typ_spec) |> map_cases (fold invalidate_case_combinators_of olds) |> map_types (History.register tyco vs_typ_spec) end; fun declare_datatype_global proto_constrs thy = let fun unoverload_const_typ (c, ty) = (Axclass.unoverload_const thy (c, ty), ty); val constrs = map unoverload_const_typ proto_constrs; val (tyco, (vs, cos)) = constrset_of_consts thy constrs; in thy |> modify_specs (register_type (tyco, (vs, Constructors {constructors = cos, case_combinators = []}))) |> register_tyco_for_plugin tyco end; fun declare_datatype_cmd raw_constrs thy = declare_datatype_global (map (read_bare_const thy) raw_constrs) thy; fun generic_declare_abstype strictness proto_thm thy = case check_abstype_cert strictness thy proto_thm of SOME (tyco, (vs, (abstractor as (abs, (_, ty)), (proj, abs_rep)))) => thy |> modify_specs (register_type (tyco, (vs, Abstractor {abstractor = abstractor, projection = proj, abs_rep = abs_rep, more_abstract_functions = []})) #> register_fun_spec proj (Proj (Logic.varify_types_global (mk_proj tyco vs ty abs proj), (tyco, abs)))) |> register_tyco_for_plugin tyco | NONE => thy; val declare_abstype_global = generic_declare_abstype Strict; val declare_abstype = code_declaration Morphism.thm generic_declare_abstype; (* functions *) (* strictness wrt. shape of theorem propositions: * default equations: silent * using declarations and attributes: warnings (after morphism application!) * using global declarations (... -> thy -> thy): strict * internal processing after storage: strict *) local fun subsumptive_add thy verbose (thm, proper) eqns = let val args_of = drop_prefix is_Var o rev o snd o strip_comb o Term.map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of o Thm.transfer thy; val args = args_of thm; val incr_idx = Logic.incr_indexes ([], [], Thm.maxidx_of thm + 1); fun matches_args args' = let val k = length args' - length args in if k >= 0 then Pattern.matchess thy (args, (map incr_idx o drop k) args') else false end; fun drop (thm', proper') = if (proper orelse not proper') andalso matches_args (args_of thm') then (if verbose then warning ("Code generator: dropping subsumed code equation\n" ^ Thm.string_of_thm_global thy thm') else (); true) else false; in (thm |> Thm.close_derivation \<^here> |> Thm.trim_context, proper) :: filter_out drop eqns end; fun add_eqn_for (c, eqn) thy = thy |> modify_specs (modify_pending_eqns c (subsumptive_add thy true eqn)); fun add_eqns_for default (c, proto_eqns) thy = thy |> modify_specs (fn specs => if is_default (lookup_fun_spec specs c) orelse not default then let val eqns = [] |> fold_rev (subsumptive_add thy (not default)) proto_eqns; in specs |> register_fun_spec c (Eqns (default, eqns)) end else specs); fun add_abstract_for (c, (thm, tyco_abs as (tyco, _))) = modify_specs (register_fun_spec c (Abstr (Thm.close_derivation \<^here> thm, tyco_abs)) #> map_types (History.modify_entry tyco (add_abstract_function c))) in fun generic_declare_eqns default strictness raw_eqns thy = fold (add_eqns_for default) (prep_eqns strictness thy raw_eqns) thy; fun generic_add_eqn strictness raw_eqn thy = fold add_eqn_for (the_list (prep_eqn strictness thy raw_eqn)) thy; fun generic_declare_abstract_eqn strictness raw_abs_eqn thy = fold add_abstract_for (the_list (prep_abs_eqn strictness thy raw_abs_eqn)) thy; fun add_maybe_abs_eqn_liberal thm thy = case prep_maybe_abs_eqn thy thm of SOME (c, (eqn, NONE)) => add_eqn_for (c, eqn) thy | SOME (c, ((thm, _), SOME tyco)) => add_abstract_for (c, (thm, tyco)) thy | NONE => thy; end; val declare_default_eqns_global = generic_declare_eqns true Silent; val declare_default_eqns = silent_code_declaration (map o apfst o Morphism.thm) (generic_declare_eqns true); val declare_eqns_global = generic_declare_eqns false Strict; val declare_eqns = code_declaration (map o apfst o Morphism.thm) (generic_declare_eqns false); val add_eqn_global = generic_add_eqn Strict; fun del_eqn_global thm thy = case prep_eqn Liberal thy (thm, false) of SOME (c, (thm, _)) => modify_specs (modify_pending_eqns c (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')))) thy | NONE => thy; val declare_abstract_eqn_global = generic_declare_abstract_eqn Strict; val declare_abstract_eqn = code_declaration Morphism.thm generic_declare_abstract_eqn; fun declare_aborting_global c = modify_specs (register_fun_spec c aborting); fun declare_unimplemented_global c = modify_specs (register_fun_spec c unimplemented); (* cases *) fun case_cong thy case_const (num_args, (pos, _)) = let val ([x, y], ctxt) = fold_map Name.variant ["A", "A'"] Name.context; val (zs, _) = fold_map Name.variant (replicate (num_args - 1) "") ctxt; val (ws, vs) = chop pos zs; val T = devarify (const_typ thy case_const); val Ts = binder_types T; val T_cong = nth Ts pos; fun mk_prem z = Free (z, T_cong); fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts); val (prem, concl) = apply2 Logic.mk_equals (apply2 mk_prem (x, y), apply2 mk_concl (x, y)); in Goal.prove_sorry_global thy (x :: y :: zs) [prem] concl (fn {context = ctxt', prems} => Simplifier.rewrite_goals_tac ctxt' prems THEN ALLGOALS (Proof_Context.fact_tac ctxt' [Drule.reflexive_thm])) end; fun declare_case_global thm thy = let val (case_const, (k, cos)) = case_cert thm; fun get_type_of_constr c = case get_type_of_constr_or_abstr thy c of SOME (c, false) => SOME c | _ => NONE; val cos_with_tycos = (map_filter o Option.map) (fn c => (c, get_type_of_constr c)) cos; val _ = case map_filter (fn (c, NONE) => SOME c | _ => NONE) cos_with_tycos of [] => () | cs => error ("Non-constructor(s) in case certificate: " ^ commas_quote cs); val tycos = distinct (op =) (map_filter snd cos_with_tycos); val schema = (1 + Int.max (1, length cos), (k, cos)); val cong = case_cong thy case_const schema; in thy |> modify_specs (map_cases (History.register case_const (Case {schema = schema, tycos = tycos, cong = cong})) #> map_types (fold (fn tyco => History.modify_entry tyco (add_case_combinator case_const)) tycos)) end; fun declare_undefined_global c = (modify_specs o map_cases) (History.register c Undefined); (* attributes *) fun code_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I); fun code_thm_attribute g f = Scan.lift (g |-- Scan.succeed (code_attribute f)); fun code_const_attribute g f = Scan.lift (g -- Args.colon) |-- Scan.repeat1 Args.term >> (fn ts => code_attribute (K (fold (fn t => fn thy => f ((check_const thy o Logic.unvarify_types_global) t) thy) ts))); val _ = Theory.setup (let val code_attribute_parser = code_thm_attribute (Args.$$$ "equation") (fn thm => generic_add_eqn Liberal (thm, true)) || code_thm_attribute (Args.$$$ "nbe") (fn thm => generic_add_eqn Liberal (thm, false)) || code_thm_attribute (Args.$$$ "abstract") (generic_declare_abstract_eqn Liberal) || code_thm_attribute (Args.$$$ "abstype") (generic_declare_abstype Liberal) || code_thm_attribute Args.del del_eqn_global || code_const_attribute (Args.$$$ "abort") declare_aborting_global || code_const_attribute (Args.$$$ "drop") declare_unimplemented_global || Scan.succeed (code_attribute add_maybe_abs_eqn_liberal); in Attrib.setup \<^binding>\code\ code_attribute_parser "declare theorems for code generation" end); end; (*struct*) (* type-safe interfaces for data dependent on executable code *) functor Code_Data(Data: CODE_DATA_ARGS): CODE_DATA = struct type T = Data.T; exception Data of T; fun dest (Data x) = x val kind = Code.declare_data (Data Data.empty); val data_op = (kind, Data, dest); fun change_yield (SOME thy) f = Code.change_yield_data data_op thy f | change_yield NONE f = f Data.empty fun change some_thy f = snd (change_yield some_thy (pair () o f)); end; structure Code : CODE = struct open Code; end; diff --git a/src/Tools/Code/code_namespace.ML b/src/Tools/Code/code_namespace.ML --- a/src/Tools/Code/code_namespace.ML +++ b/src/Tools/Code/code_namespace.ML @@ -1,466 +1,466 @@ (* Title: Tools/Code/code_namespace.ML Author: Florian Haftmann, TU Muenchen Mastering target language namespaces. *) signature CODE_NAMESPACE = sig val variant_case_insensitive: string -> Name.context -> string * Name.context datatype export = Private | Opaque | Public val is_public: export -> bool val not_private: export -> bool val join_exports: export list -> export type flat_program val flat_program: Proof.context -> { module_prefix: string, module_name: string, reserved: Name.context, identifiers: Code_Printer.identifiers, empty_nsp: 'a, namify_stmt: Code_Thingol.stmt -> string -> 'a -> string * 'a, modify_stmt: Code_Thingol.stmt -> Code_Thingol.stmt option } -> Code_Symbol.T list -> Code_Thingol.program -> { deresolver: string -> Code_Symbol.T -> string, flat_program: flat_program } datatype ('a, 'b) node = Dummy | Stmt of export * 'a | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T) type ('a, 'b) hierarchical_program val hierarchical_program: Proof.context -> { module_name: string, reserved: Name.context, identifiers: Code_Printer.identifiers, empty_nsp: 'c, namify_module: string -> 'c -> string * 'c, namify_stmt: Code_Thingol.stmt -> string -> 'c -> string * 'c, cyclic_modules: bool, class_transitive: bool, class_relation_public: bool, empty_data: 'b, memorize_data: Code_Symbol.T -> 'b -> 'b, modify_stmts: (Code_Symbol.T * (export * Code_Thingol.stmt)) list -> (export * 'a) option list } -> Code_Symbol.T list -> Code_Thingol.program -> { deresolver: string list -> Code_Symbol.T -> string, hierarchical_program: ('a, 'b) hierarchical_program } val print_hierarchical: { print_module: string list -> string -> 'b -> 'c list -> 'c, print_stmt: string list -> Code_Symbol.T * (export * 'a) -> 'c, lift_markup: (Pretty.T -> Pretty.T) -> 'c -> 'c } -> ('a, 'b) hierarchical_program -> 'c list end; structure Code_Namespace : CODE_NAMESPACE = struct (** name handling on case-insensitive file systems **) fun restore_for cs = if forall Symbol.is_ascii_upper cs then map Symbol.to_ascii_upper else if Symbol.is_ascii_upper (nth cs 0) then nth_map 0 Symbol.to_ascii_upper else I; fun variant_case_insensitive s ctxt = let val cs = Symbol.explode s; val s_lower = implode (map Symbol.to_ascii_lower cs); val restore = implode o restore_for cs o Symbol.explode; in ctxt |> Name.variant s_lower |>> restore end; (** export **) datatype export = Private | Opaque | Public; fun is_public Public = true | is_public _ = false; fun not_private Public = true | not_private Opaque = true | not_private _ = false; fun mark_export Public _ = Public | mark_export _ Public = Public | mark_export Opaque _ = Opaque | mark_export _ Opaque = Opaque | mark_export _ _ = Private; fun join_exports exports = fold mark_export exports Private; fun dependent_exports { program = program, class_transitive = class_transitive } = let fun is_datatype_or_class (Code_Symbol.Type_Constructor _) = true | is_datatype_or_class (Code_Symbol.Type_Class _) = true | is_datatype_or_class _ = false; fun is_relevant (Code_Symbol.Class_Relation _) = true | is_relevant sym = is_datatype_or_class sym; val proto_gr = Code_Symbol.Graph.restrict is_relevant program; val gr = proto_gr |> Code_Symbol.Graph.fold (fn (sym, (_, (_, deps))) => if is_relevant sym then I else Code_Symbol.Graph.new_node (sym, Code_Thingol.NoStmt) #> Code_Symbol.Graph.Keys.fold (fn sym' => if is_relevant sym' then Code_Symbol.Graph.add_edge (sym, sym') else I) deps) program |> class_transitive ? Code_Symbol.Graph.fold (fn (sym as Code_Symbol.Type_Class _, _) => fold (curry Code_Symbol.Graph.add_edge sym) ((remove (op =) sym o Code_Symbol.Graph.all_succs proto_gr) [sym]) | _ => I) proto_gr fun deps_of sym = let val succs = Code_Symbol.Graph.Keys.dest o Code_Symbol.Graph.imm_succs gr; val deps1 = succs sym; val deps2 = [] |> fold (union (op =)) (map succs deps1) |> subtract (op =) deps1 in (deps1, deps2) end; in { is_datatype_or_class = is_datatype_or_class, deps_of = deps_of } end; fun mark_exports_aux { program = program, prefix_of = prefix_of, map_export = map_export, is_datatype_or_class = is_datatype_or_class, deps_of = deps_of, class_relation_public = class_relation_public } prefix sym = let val export = (if is_datatype_or_class sym then Opaque else Public); val (dependent_export1, dependent_export2) = case Code_Symbol.Graph.get_node program sym of Code_Thingol.Fun _ => (SOME Opaque, NONE) | Code_Thingol.Classinst _ => (SOME Opaque, NONE) | Code_Thingol.Datatypecons _ => (SOME Public, SOME Opaque) | Code_Thingol.Classparam _ => (SOME Public, SOME Opaque) | Code_Thingol.Class _ => (SOME Opaque, NONE) | Code_Thingol.Classrel _ => (if class_relation_public then (SOME Public, SOME Opaque) else (SOME Opaque, NONE)) | _ => (NONE, NONE); val dependent_exports = case dependent_export1 of SOME export1 => (case dependent_export2 of SOME export2 => let val (deps1, deps2) = deps_of sym in map (rpair export1) deps1 @ map (rpair export2) deps2 end | NONE => map (rpair export1) (fst (deps_of sym))) | NONE => []; in map_export prefix sym (mark_export export) #> fold (fn (sym, export) => map_export (prefix_of sym) sym (mark_export export)) dependent_exports end; fun mark_exports { program = program, prefix_of = prefix_of, map_export = map_export, class_transitive = class_transitive, class_relation_public = class_relation_public } = let val { is_datatype_or_class, deps_of } = dependent_exports { program = program, class_transitive = class_transitive }; in mark_exports_aux { program = program, prefix_of = prefix_of, map_export = map_export, is_datatype_or_class = is_datatype_or_class, deps_of = deps_of, class_relation_public = class_relation_public } end; (** fundamental module name hierarchy **) fun module_fragments' { identifiers, reserved } name = case Code_Symbol.lookup_module_data identifiers name of SOME (fragments, _) => fragments | NONE => map (fn fragment => fst (Name.variant fragment reserved)) (Long_Name.explode name); fun module_fragments { module_name, identifiers, reserved } = if module_name = "" then module_fragments' { identifiers = identifiers, reserved = reserved } else K (Long_Name.explode module_name); fun build_module_namespace ctxt enforce_upper { module_prefix, module_name, identifiers, reserved } program = let - val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program []; + val module_names = build (Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program); val module_fragments' = module_fragments { module_name = module_name, identifiers = identifiers, reserved = reserved }; val adjust_case = if enforce_upper then map (Name.enforce_case true) else I; in fold (fn name => Symtab.update (name, adjust_case (Long_Name.explode module_prefix @ module_fragments' name))) module_names Symtab.empty end; fun prep_symbol ctxt { module_namespace, force_module, identifiers } sym = case Code_Symbol.lookup identifiers sym of NONE => ((the o Symtab.lookup module_namespace o Code_Symbol.default_prefix ctxt) sym, Code_Symbol.default_base sym) | SOME prefix_name => if null force_module then prefix_name else (force_module, snd prefix_name); fun has_priority identifiers = is_some o Code_Symbol.lookup identifiers; fun build_proto_program { empty, add_stmt, add_dep } program = empty |> Code_Symbol.Graph.fold (fn (sym, (stmt, _)) => add_stmt sym stmt) program |> Code_Symbol.Graph.fold (fn (sym, (_, (_, syms))) => Code_Symbol.Graph.Keys.fold (add_dep sym) syms) program; fun prioritize has_priority = uncurry append o List.partition has_priority; (** flat program structure **) type flat_program = ((string * (export * Code_Thingol.stmt) option) Code_Symbol.Graph.T * (string * Code_Symbol.T list) list) Graph.T; fun flat_program ctxt { module_prefix, module_name, reserved, identifiers, empty_nsp, namify_stmt, modify_stmt } exports program = let (* building module name hierarchy *) val module_namespace = build_module_namespace ctxt true { module_prefix = module_prefix, module_name = module_name, identifiers = identifiers, reserved = reserved } program; val prep_sym = prep_symbol ctxt { module_namespace = module_namespace, force_module = Long_Name.explode module_name, identifiers = identifiers } #>> Long_Name.implode; val sym_priority = has_priority identifiers; (* distribute statements over hierarchy *) val mark_exports = mark_exports { program = program, prefix_of = fst o prep_sym, map_export = fn module_name => fn sym => Graph.map_node module_name o apfst o Code_Symbol.Graph.map_node sym o apsnd o apfst, class_transitive = false, class_relation_public = false }; fun add_stmt sym stmt = let val (module_name, base) = prep_sym sym; in Graph.default_node (module_name, (Code_Symbol.Graph.empty, [])) #> (Graph.map_node module_name o apfst) (Code_Symbol.Graph.new_node (sym, (base, (if null exports then Public else Private, stmt)))) end; fun add_dep sym sym' = let val (module_name, _) = prep_sym sym; val (module_name', _) = prep_sym sym'; in if module_name = module_name' then (Graph.map_node module_name o apfst) (Code_Symbol.Graph.add_edge (sym, sym')) else (Graph.map_node module_name o apsnd) (AList.map_default (op =) (module_name', []) (insert (op =) sym')) #> mark_exports module_name' sym' end; val proto_program = build_proto_program { empty = Graph.empty, add_stmt = add_stmt, add_dep = add_dep } program |> fold (fn sym => mark_exports ((fst o prep_sym) sym) sym) exports; (* name declarations and statement modifications *) fun declare sym (base, (_, stmt)) (gr, nsp) = let val (base', nsp') = namify_stmt stmt base nsp; val gr' = (Code_Symbol.Graph.map_node sym o apfst) (K base') gr; in (gr', nsp') end; fun declarations gr = (gr, empty_nsp) |> fold (fn sym => declare sym (Code_Symbol.Graph.get_node gr sym)) (prioritize sym_priority (Code_Symbol.Graph.keys gr)) |> fst |> Code_Symbol.Graph.map_strong_conn (fn syms_bases_exports_stmts => map snd syms_bases_exports_stmts |> (map o apsnd) (fn (export, stmt) => Option.map (pair export) (modify_stmt stmt))); val flat_program = proto_program |> (Graph.map o K o apfst) declarations; (* qualified and unqualified imports, deresolving *) fun base_deresolver sym = fst (Code_Symbol.Graph.get_node (fst (Graph.get_node flat_program (fst (prep_sym sym)))) sym); fun classify_names gr imports = let val import_tab = maps (fn (module_name, syms) => map (rpair module_name) syms) imports; val imported_syms = map fst import_tab; val here_syms = Code_Symbol.Graph.keys gr; in Code_Symbol.Table.empty |> fold (fn sym => Code_Symbol.Table.update (sym, base_deresolver sym)) here_syms |> fold (fn sym => Code_Symbol.Table.update (sym, Long_Name.append (the (AList.lookup (op =) import_tab sym)) (base_deresolver sym))) imported_syms end; val deresolver_tab = Symtab.make (AList.make (uncurry classify_names o Graph.get_node flat_program) (Graph.keys flat_program)); fun deresolver "" sym = Long_Name.append (fst (prep_sym sym)) (base_deresolver sym) | deresolver module_name sym = the (Code_Symbol.Table.lookup (the (Symtab.lookup deresolver_tab module_name)) sym) handle Option.Option => error ("Unknown statement name: " ^ Code_Symbol.quote ctxt sym); in { deresolver = deresolver, flat_program = flat_program } end; (** hierarchical program structure **) datatype ('a, 'b) node = Dummy | Stmt of export * 'a | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T); type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Code_Symbol.Graph.T; fun the_stmt (Stmt (export, stmt)) = (export, stmt); fun map_module_content f (Module content) = Module (f content); fun map_module [] = I | map_module (name_fragment :: name_fragments) = apsnd o Code_Symbol.Graph.map_node (Code_Symbol.Module name_fragment) o apsnd o map_module_content o map_module name_fragments; fun map_module_stmts f_module f_stmts sym_base_nodes = let val some_modules = sym_base_nodes |> map (fn (_, (base, Module content)) => SOME (base, content) | _ => NONE) |> (burrow_options o map o apsnd) f_module; val some_export_stmts = sym_base_nodes |> map (fn (sym, (base, Stmt export_stmt)) => SOME ((sym, export_stmt), base) | _ => NONE) |> (burrow_options o burrow_fst) (fn [] => [] | xs => f_stmts xs) in map2 (fn SOME (base, content) => (K (base, Module content)) | NONE => fn SOME (some_export_stmt, base) => (base, case some_export_stmt of SOME export_stmt => Stmt export_stmt | NONE => Dummy)) some_modules some_export_stmts end; fun hierarchical_program ctxt { module_name, reserved, identifiers, empty_nsp, namify_module, namify_stmt, cyclic_modules, class_transitive, class_relation_public, empty_data, memorize_data, modify_stmts } exports program = let (* building module name hierarchy *) val module_namespace = build_module_namespace ctxt false { module_prefix = "", module_name = module_name, identifiers = identifiers, reserved = reserved } program; val prep_sym = prep_symbol ctxt { module_namespace = module_namespace, force_module = Long_Name.explode module_name, identifiers = identifiers } val sym_priority = has_priority identifiers; (* building empty module hierarchy *) val empty_module = (empty_data, Code_Symbol.Graph.empty); fun ensure_module name_fragment (data, nodes) = if can (Code_Symbol.Graph.get_node nodes) (Code_Symbol.Module name_fragment) then (data, nodes) else (data, nodes |> Code_Symbol.Graph.new_node (Code_Symbol.Module name_fragment, (name_fragment, Module empty_module))); fun allocate_module [] = I | allocate_module (name_fragment :: name_fragments) = ensure_module name_fragment #> (apsnd o Code_Symbol.Graph.map_node (Code_Symbol.Module name_fragment) o apsnd o map_module_content o allocate_module) name_fragments; val empty_program = empty_module |> Symtab.fold (fn (_, fragments) => allocate_module fragments) module_namespace |> Code_Symbol.Graph.fold (allocate_module o these o Option.map fst o Code_Symbol.lookup identifiers o fst) program; (* distribute statements over hierarchy *) val mark_exports = mark_exports { program = program, prefix_of = fst o prep_sym, map_export = fn name_fragments => fn sym => fn f => (map_module name_fragments o apsnd o Code_Symbol.Graph.map_node sym o apsnd) (fn Stmt (export, stmt) => Stmt (f export, stmt)), class_transitive = class_transitive, class_relation_public = class_relation_public }; fun add_stmt sym stmt = let val (name_fragments, base) = prep_sym sym; in (map_module name_fragments o apsnd) (Code_Symbol.Graph.new_node (sym, (base, Stmt (if null exports then Public else Private, stmt)))) end; fun add_edge_acyclic_error error_msg dep gr = Code_Symbol.Graph.add_edge_acyclic dep gr handle Code_Symbol.Graph.CYCLES _ => error (error_msg ()) fun add_dep sym sym' = let val (name_fragments, _) = prep_sym sym; val (name_fragments', _) = prep_sym sym'; val (name_fragments_common, (diff, diff')) = chop_common_prefix (op =) (name_fragments, name_fragments'); val is_cross_module = not (null diff andalso null diff'); val dep = apply2 hd (map Code_Symbol.Module diff @ [sym], map Code_Symbol.Module diff' @ [sym']); val add_edge = if is_cross_module andalso not cyclic_modules then add_edge_acyclic_error (fn _ => "Dependency " ^ Code_Symbol.quote ctxt sym ^ " -> " ^ Code_Symbol.quote ctxt sym' ^ " would result in module dependency cycle") dep else Code_Symbol.Graph.add_edge dep; in (map_module name_fragments_common o apsnd) add_edge #> (if is_cross_module then mark_exports name_fragments' sym' else I) end; val proto_program = build_proto_program { empty = empty_program, add_stmt = add_stmt, add_dep = add_dep } program |> fold (fn sym => mark_exports ((fst o prep_sym) sym) sym) exports; (* name declarations, data and statement modifications *) fun make_declarations nsps (data, nodes) = let val (module_fragments, stmt_syms) = Code_Symbol.Graph.keys nodes |> List.partition (fn sym => case Code_Symbol.Graph.get_node nodes sym of (_, Module _) => true | _ => false) |> apply2 (prioritize sym_priority) fun declare namify sym (nsps, nodes) = let val (base, node) = Code_Symbol.Graph.get_node nodes sym; val (base', nsps') = namify node base nsps; val nodes' = Code_Symbol.Graph.map_node sym (K (base', node)) nodes; in (nsps', nodes') end; val (nsps', nodes') = (nsps, nodes) |> fold (declare (K namify_module)) module_fragments |> fold (declare (namify_stmt o snd o the_stmt)) stmt_syms; fun modify_stmts' syms_stmts = let val stmts' = modify_stmts syms_stmts in stmts' @ replicate (length syms_stmts - length stmts') NONE end; val nodes'' = nodes' |> Code_Symbol.Graph.map_strong_conn (map_module_stmts (make_declarations nsps') modify_stmts'); val data' = fold memorize_data stmt_syms data; in (data', nodes'') end; val (_, hierarchical_program) = make_declarations empty_nsp proto_program; (* deresolving *) fun deresolver prefix_fragments sym = let val (name_fragments, _) = prep_sym sym; val (_, (_, remainder)) = chop_common_prefix (op =) (prefix_fragments, name_fragments); val nodes = fold (fn name_fragment => fn nodes => case Code_Symbol.Graph.get_node nodes (Code_Symbol.Module name_fragment) of (_, Module (_, nodes)) => nodes) name_fragments hierarchical_program; val (base', _) = Code_Symbol.Graph.get_node nodes sym; in Long_Name.implode (remainder @ [base']) end handle Code_Symbol.Graph.UNDEF _ => error ("Unknown statement name: " ^ Code_Symbol.quote ctxt sym); in { deresolver = deresolver, hierarchical_program = hierarchical_program } end; fun print_hierarchical { print_module, print_stmt, lift_markup } = let fun print_node _ (_, Dummy) = NONE | print_node prefix_fragments (sym, Stmt stmt) = SOME (lift_markup (Code_Printer.markup_stmt sym) (print_stmt prefix_fragments (sym, stmt))) | print_node prefix_fragments (Code_Symbol.Module name_fragment, Module (data, nodes)) = let val prefix_fragments' = prefix_fragments @ [name_fragment] in Option.map (print_module prefix_fragments' name_fragment data) (print_nodes prefix_fragments' nodes) end and print_nodes prefix_fragments nodes = let val xs = (map_filter (fn sym => print_node prefix_fragments (sym, snd (Code_Symbol.Graph.get_node nodes sym))) o rev o flat o Code_Symbol.Graph.strong_conn) nodes in if null xs then NONE else SOME xs end; in these o print_nodes [] end; end; diff --git a/src/Tools/Code/code_preproc.ML b/src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML +++ b/src/Tools/Code/code_preproc.ML @@ -1,648 +1,648 @@ (* Title: Tools/Code/code_preproc.ML Author: Florian Haftmann, TU Muenchen Preprocessing code equations into a well-sorted system in a graph with explicit dependencies. *) signature CODE_PREPROC = sig val map_pre: (Proof.context -> Proof.context) -> theory -> theory val map_post: (Proof.context -> Proof.context) -> theory -> theory val add_functrans: string * (Proof.context -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory val del_functrans: string -> theory -> theory val simple_functrans: (Proof.context -> thm list -> thm list option) -> Proof.context -> (thm * bool) list -> (thm * bool) list option val print_codeproc: Proof.context -> unit type code_algebra type code_graph val cert: code_graph -> string -> Code.cert val sortargs: code_graph -> string -> sort list val all: code_graph -> string list val pretty: Proof.context -> code_graph -> Pretty.T val obtain: bool -> { ctxt: Proof.context, consts: string list, terms: term list } -> { algebra: code_algebra, eqngr: code_graph } val dynamic_conv: Proof.context -> (code_algebra -> code_graph -> term -> conv) -> conv val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'b) -> (code_algebra -> code_graph -> term -> 'a) -> term -> 'b val static_conv: { ctxt: Proof.context, consts: string list } -> ({ algebra: code_algebra, eqngr: code_graph } -> Proof.context -> term -> conv) -> Proof.context -> conv val static_value: { ctxt: Proof.context, lift_postproc: ((term -> term) -> 'a -> 'b), consts: string list } -> ({ algebra: code_algebra, eqngr: code_graph } -> Proof.context -> term -> 'a) -> Proof.context -> term -> 'b val trace_none: Context.generic -> Context.generic val trace_all: Context.generic -> Context.generic val trace_only: string list -> Context.generic -> Context.generic val trace_only_ext: string list -> Context.generic -> Context.generic val timing: bool Config.T val timed: string -> ('a -> Proof.context) -> ('a -> 'b) -> 'a -> 'b val timed_exec: string -> (unit -> 'a) -> Proof.context -> 'a val timed_conv: string -> (Proof.context -> conv) -> Proof.context -> conv val timed_value: string -> (Proof.context -> term -> 'a) -> Proof.context -> term -> 'a end structure Code_Preproc : CODE_PREPROC = struct (** timing **) val timing = Attrib.setup_config_bool \<^binding>\code_timing\ (K false); fun timed msg ctxt_of f x = if Config.get (ctxt_of x) timing then timeap_msg msg f x else f x; fun timed_exec msg f ctxt = if Config.get ctxt timing then timeap_msg msg f () else f (); fun timed' msg f ctxt x = if Config.get ctxt timing then timeap_msg msg (f ctxt) x else f ctxt x; val timed_conv = timed'; val timed_value = timed'; (** preprocessor administration **) (* theory data *) datatype thmproc = Thmproc of { pre: simpset, post: simpset, functrans: (string * (serial * (Proof.context -> (thm * bool) list -> (thm * bool) list option))) list }; fun make_thmproc ((pre, post), functrans) = Thmproc { pre = pre, post = post, functrans = functrans }; fun map_thmproc f (Thmproc { pre, post, functrans }) = make_thmproc (f ((pre, post), functrans)); fun merge_thmproc (Thmproc { pre = pre1, post = post1, functrans = functrans1 }, Thmproc { pre = pre2, post = post2, functrans = functrans2 }) = let val pre = Simplifier.merge_ss (pre1, pre2); val post = Simplifier.merge_ss (post1, post2); val functrans = AList.merge (op =) (eq_fst (op =)) (functrans1, functrans2) handle AList.DUP => error ("Duplicate function transformer"); in make_thmproc ((pre, post), functrans) end; structure Code_Preproc_Data = Theory_Data ( type T = thmproc; val empty = make_thmproc ((Simplifier.empty_ss, Simplifier.empty_ss), []); val merge = merge_thmproc; ); fun the_thmproc thy = case Code_Preproc_Data.get thy of Thmproc x => x; fun delete_force msg key xs = if AList.defined (op =) xs key then AList.delete (op =) key xs else error ("No such " ^ msg ^ ": " ^ quote key); val map_data = Code_Preproc_Data.map o map_thmproc; val map_pre_post = map_data o apfst; fun map_simpset which f thy = map_pre_post (which (simpset_map (Proof_Context.init_global thy) f)) thy; val map_pre = map_simpset apfst; val map_post = map_simpset apsnd; fun process_unfold add_del = map_pre o add_del; fun process_post add_del = map_post o add_del; fun process_abbrev add_del raw_thm thy = let val ctxt = Proof_Context.init_global thy; val thm = Local_Defs.meta_rewrite_rule ctxt raw_thm; val thm_sym = Thm.symmetric thm; in thy |> map_pre_post (fn (pre, post) => (pre |> simpset_map ctxt (add_del thm_sym), post |> simpset_map ctxt (add_del thm))) end; fun add_functrans (name, f) = (map_data o apsnd) (AList.update (op =) (name, (serial (), f))); fun del_functrans name = (map_data o apsnd) (delete_force "function transformer" name); (* algebra of sandwiches: cterm transformations with pending postprocessors *) fun matches_transitive eq1 eq2 = Thm.rhs_of eq1 aconvc Thm.lhs_of eq2; fun trans_comb eq1 eq2 = (*explicit assertions: evaluation conversion stacks are error-prone*) if Thm.is_reflexive eq1 then (\<^assert> (matches_transitive eq1 eq2); eq2) else if Thm.is_reflexive eq2 then (\<^assert> (matches_transitive eq1 eq2); eq1) else Thm.transitive eq1 eq2; fun trans_conv_rule conv eq = trans_comb eq (conv (Thm.rhs_of eq)); structure Sandwich : sig type T = Proof.context -> cterm -> (Proof.context -> thm -> thm) * cterm; val chain: T -> T -> T val lift: (Proof.context -> cterm -> (Proof.context -> cterm -> thm) * thm) -> T val conversion: T -> (Proof.context -> term -> conv) -> Proof.context -> conv; val computation: T -> ((term -> term) -> 'a -> 'b) -> (Proof.context -> term -> 'a) -> Proof.context -> term -> 'b; end = struct type T = Proof.context -> cterm -> (Proof.context -> thm -> thm) * cterm; fun chain sandwich2 sandwich1 ctxt = sandwich1 ctxt ##>> sandwich2 ctxt #>> (fn (f, g) => fn ctxt => f ctxt o g ctxt); fun lift conv_sandwhich ctxt ct = let val (postproc_conv, eq) = conv_sandwhich ctxt ct; fun potentail_trans_comb eq1 eq2 = if matches_transitive eq1 eq2 then trans_comb eq1 eq2 else eq2; (*weakened protocol for plain term evaluation*) in (fn ctxt => trans_conv_rule (postproc_conv ctxt) o potentail_trans_comb eq, Thm.rhs_of eq) end; fun conversion sandwich conv ctxt ct = let val (postproc, ct') = sandwich ctxt ct; val thm = conv ctxt (Thm.term_of ct') ct'; val thm' = postproc ctxt thm; in thm' end; fun computation sandwich lift_postproc eval ctxt t = let val (postproc, ct') = sandwich ctxt (Thm.cterm_of ctxt t); val result = eval ctxt (Thm.term_of ct'); val result' = lift_postproc (Thm.term_of o Thm.rhs_of o postproc ctxt o Thm.reflexive o Thm.cterm_of ctxt) result in result' end; end; (* post- and preprocessing *) fun normalized_tfrees_sandwich ctxt ct = let val t = Thm.term_of ct; val vs_original = - fold_term_types (K (fold_atyps (insert (eq_fst op =) o dest_TFree))) t []; + build (fold_term_types (K (fold_atyps (insert (eq_fst op =) o dest_TFree))) t); val vs_normalized = Name.invent_names Name.context Name.aT (map snd vs_original); val normalize = map_type_tfree (TFree o the o AList.lookup (op =) (vs_original ~~ vs_normalized)); val normalization = map2 (fn (v, sort) => fn (v', _) => (((v', 0), sort), Thm.ctyp_of ctxt (TFree (v, sort)))) vs_original vs_normalized; in if eq_list (eq_fst (op =)) (vs_normalized, vs_original) then (K I, ct) else (K (Thm.instantiate (TVars.make normalization, Vars.empty) o Thm.varifyT_global), Thm.cterm_of ctxt (map_types normalize t)) end; fun no_variables_sandwich ctxt ct = let val all_vars = fold_aterms (fn t as Free _ => insert (op aconvc) (Thm.cterm_of ctxt t) | t as Var _ => insert (op aconvc) (Thm.cterm_of ctxt t) | _ => I) (Thm.term_of ct) []; fun apply_beta var thm = Thm.combination thm (Thm.reflexive var) |> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false))) |> Conv.fconv_rule (Conv.arg1_conv (Thm.beta_conversion false)); in if null all_vars then (K I, ct) else (K (fold apply_beta all_vars), fold_rev Thm.lambda all_vars ct) end; fun simplifier_conv_sandwich ctxt = let val thy = Proof_Context.theory_of ctxt; val pre = (#pre o the_thmproc) thy; val post = (#post o the_thmproc) thy; fun pre_conv ctxt' = Simplifier.rewrite (put_simpset pre ctxt') #> trans_conv_rule (Axclass.unoverload_conv ctxt') #> trans_conv_rule (Thm.eta_conversion); fun post_conv ctxt'' = Axclass.overload_conv ctxt'' #> trans_conv_rule (Simplifier.rewrite (put_simpset post ctxt'')); in fn ctxt' => timed_conv "preprocessing term" pre_conv ctxt' #> pair (timed_conv "postprocessing term" post_conv) end; fun simplifier_sandwich ctxt = Sandwich.lift (simplifier_conv_sandwich ctxt); fun value_sandwich ctxt = normalized_tfrees_sandwich |> Sandwich.chain no_variables_sandwich |> Sandwich.chain (simplifier_sandwich ctxt); fun print_codeproc ctxt = let val thy = Proof_Context.theory_of ctxt; val pre = (#pre o the_thmproc) thy; val post = (#post o the_thmproc) thy; val functrans = (map fst o #functrans o the_thmproc) thy; in Pretty.writeln_chunks [ Pretty.block [ Pretty.str "preprocessing simpset:", Pretty.fbrk, Simplifier.pretty_simpset true (put_simpset pre ctxt) ], Pretty.block [ Pretty.str "postprocessing simpset:", Pretty.fbrk, Simplifier.pretty_simpset true (put_simpset post ctxt) ], Pretty.block ( Pretty.str "function transformers:" :: Pretty.fbrk :: (Pretty.fbreaks o map Pretty.str) functrans ) ] end; fun simple_functrans f ctxt eqns = case f ctxt (map fst eqns) of SOME thms' => SOME (map (rpair (forall snd eqns)) thms') | NONE => NONE; (** sort algebra and code equation graph types **) type code_algebra = (sort -> sort) * Sorts.algebra; type code_graph = ((string * sort) list * Code.cert) Graph.T; fun get_node eqngr const = Graph.get_node eqngr const handle Graph.UNDEF _ => error ("No such constant in code equation graph: " ^ quote const); fun cert eqngr = snd o get_node eqngr; fun sortargs eqngr = map snd o fst o get_node eqngr; fun all eqngr = Graph.keys eqngr; fun pretty ctxt eqngr = let val thy = Proof_Context.theory_of ctxt; in AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr) |> (map o apfst) (Code.string_of_const thy) |> sort (string_ord o apply2 fst) |> (map o apsnd) (Code.pretty_cert thy) |> filter_out (null o snd) |> map (fn (s, ps) => (Pretty.block o Pretty.fbreaks) (Pretty.str s :: ps)) |> Pretty.chunks end; (** simplifier tracing **) structure Trace_Switch = Generic_Data ( type T = string list option; val empty = SOME []; fun merge (NONE, _) = NONE | merge (_, NONE) = NONE | merge (SOME cs1, SOME cs2) = SOME (Library.merge (op =) (cs1, cs2)); ); val trace_none = Trace_Switch.put (SOME []); val trace_all = Trace_Switch.put NONE; fun gen_trace_only prep_const raw_cs context = let val cs = map (prep_const (Context.theory_of context)) raw_cs; in Trace_Switch.put (SOME cs) context end; val trace_only = gen_trace_only (K I); val trace_only_ext = gen_trace_only Code.read_const; fun switch_trace c ctxt = let val d = Trace_Switch.get (Context.Proof ctxt); val switch = case d of NONE => true | SOME cs => member (op =) cs c; val _ = if switch then tracing ("Preprocessing function equations for " ^ Code.string_of_const (Proof_Context.theory_of ctxt) c) else (); in Config.put simp_trace switch ctxt end; (** the Waisenhaus algorithm **) (* auxiliary *) fun is_proper_class thy = can (Axclass.get_info thy); fun complete_proper_sort thy = Sign.complete_sort thy #> filter (is_proper_class thy); fun inst_params thy tyco = map (fn (c, _) => Axclass.param_of_inst thy (c, tyco)) o maps (#params o Axclass.get_info thy); (* data structures *) datatype const = Fun of string | Inst of class * string; fun const_ord (Fun c1, Fun c2) = fast_string_ord (c1, c2) | const_ord (Inst class_tyco1, Inst class_tyco2) = prod_ord fast_string_ord fast_string_ord (class_tyco1, class_tyco2) | const_ord (Fun _, Inst _) = LESS | const_ord (Inst _, Fun _) = GREATER; type var = const * int; structure Vargraph = Graph(type key = var val ord = prod_ord const_ord int_ord); datatype styp = Tyco of string * styp list | Var of var | Free; fun styp_of c_lhs (Type (tyco, tys)) = Tyco (tyco, map (styp_of c_lhs) tys) | styp_of c_lhs (TFree (v, _)) = case c_lhs of SOME (c, lhs) => Var (Fun c, find_index (fn (v', _) => v = v') lhs) | NONE => Free; type vardeps_data = ((string * styp list) list * class list) Vargraph.T * (((string * sort) list * Code.cert) Symtab.table * (class * string) list); val empty_vardeps_data : vardeps_data = (Vargraph.empty, (Symtab.empty, [])); (* retrieving equations and instances from the background context *) fun obtain_eqns ctxt eqngr c = case try (Graph.get_node eqngr) c of SOME (lhs, cert) => ((lhs, []), cert) | NONE => let val thy = Proof_Context.theory_of ctxt; val functrans = (map (fn (_, (_, f)) => f ctxt) o #functrans o the_thmproc) thy; val cert = Code.get_cert (switch_trace c ctxt) functrans c; val (lhs, rhss) = Code.typargs_deps_of_cert thy cert; in ((lhs, rhss), cert) end; fun obtain_instance ctxt arities (inst as (class, tyco)) = case AList.lookup (op =) arities inst of SOME classess => (classess, ([], [])) | NONE => let val thy = Proof_Context.theory_of ctxt; val all_classes = complete_proper_sort thy [class]; val super_classes = remove (op =) class all_classes; val classess = map (complete_proper_sort thy) (Proof_Context.arity_sorts ctxt tyco [class]); val inst_params = inst_params thy tyco all_classes; in (classess, (super_classes, inst_params)) end; (* computing instantiations *) fun add_classes ctxt arities eqngr c_k new_classes vardeps_data = let val (styps, old_classes) = Vargraph.get_node (fst vardeps_data) c_k; val diff_classes = new_classes |> subtract (op =) old_classes; in if null diff_classes then vardeps_data else let val c_ks = Vargraph.immediate_succs (fst vardeps_data) c_k |> insert (op =) c_k; in vardeps_data |> (apfst o Vargraph.map_node c_k o apsnd) (append diff_classes) |> fold (fn styp => fold (ensure_typmatch_inst ctxt arities eqngr styp) new_classes) styps |> fold (fn c_k => add_classes ctxt arities eqngr c_k diff_classes) c_ks end end and add_styp ctxt arities eqngr c_k new_tyco_styps vardeps_data = let val (old_tyco_stypss, classes) = Vargraph.get_node (fst vardeps_data) c_k; in if member (op =) old_tyco_stypss new_tyco_styps then vardeps_data else vardeps_data |> (apfst o Vargraph.map_node c_k o apfst) (cons new_tyco_styps) |> fold (ensure_typmatch_inst ctxt arities eqngr new_tyco_styps) classes end and add_dep ctxt arities eqngr c_k c_k' vardeps_data = let val (_, classes) = Vargraph.get_node (fst vardeps_data) c_k; in vardeps_data |> add_classes ctxt arities eqngr c_k' classes |> apfst (Vargraph.add_edge (c_k, c_k')) end and ensure_typmatch_inst ctxt arities eqngr (tyco, styps) class vardeps_data = if can (Proof_Context.arity_sorts ctxt tyco) [class] then vardeps_data |> ensure_inst ctxt arities eqngr (class, tyco) |> fold_index (fn (k, styp) => ensure_typmatch ctxt arities eqngr styp (Inst (class, tyco), k)) styps else vardeps_data (*permissive!*) and ensure_inst ctxt arities eqngr (inst as (class, tyco)) (vardeps_data as (_, (_, insts))) = if member (op =) insts inst then vardeps_data else let val (classess, (super_classes, inst_params)) = obtain_instance ctxt arities inst; in vardeps_data |> (apsnd o apsnd) (insert (op =) inst) |> fold_index (fn (k, _) => apfst (Vargraph.new_node ((Inst (class, tyco), k), ([] ,[])))) classess |> fold (fn super_class => ensure_inst ctxt arities eqngr (super_class, tyco)) super_classes |> fold (ensure_fun ctxt arities eqngr) inst_params |> fold_index (fn (k, classes) => add_classes ctxt arities eqngr (Inst (class, tyco), k) classes #> fold (fn super_class => add_dep ctxt arities eqngr (Inst (super_class, tyco), k) (Inst (class, tyco), k)) super_classes #> fold (fn inst_param => add_dep ctxt arities eqngr (Fun inst_param, k) (Inst (class, tyco), k) ) inst_params ) classess end and ensure_typmatch ctxt arities eqngr (Tyco tyco_styps) c_k vardeps_data = vardeps_data |> add_styp ctxt arities eqngr c_k tyco_styps | ensure_typmatch ctxt arities eqngr (Var c_k') c_k vardeps_data = vardeps_data |> add_dep ctxt arities eqngr c_k c_k' | ensure_typmatch ctxt arities eqngr Free c_k vardeps_data = vardeps_data and ensure_rhs ctxt arities eqngr (c', styps) vardeps_data = vardeps_data |> ensure_fun ctxt arities eqngr c' |> fold_index (fn (k, styp) => ensure_typmatch ctxt arities eqngr styp (Fun c', k)) styps and ensure_fun ctxt arities eqngr c (vardeps_data as (_, (eqntab, _))) = if Symtab.defined eqntab c then vardeps_data else let val ((lhs, rhss), eqns) = obtain_eqns ctxt eqngr c; val rhss' = (map o apsnd o map) (styp_of (SOME (c, lhs))) rhss; in vardeps_data |> (apsnd o apfst) (Symtab.update_new (c, (lhs, eqns))) |> fold_index (fn (k, _) => apfst (Vargraph.new_node ((Fun c, k), ([] ,[])))) lhs |> fold_index (fn (k, (_, sort)) => add_classes ctxt arities eqngr (Fun c, k) (complete_proper_sort (Proof_Context.theory_of ctxt) sort)) lhs |> fold (ensure_rhs ctxt arities eqngr) rhss' end; (* applying instantiations *) fun dicts_of ctxt (proj_sort, algebra) (T, sort) = let val thy = Proof_Context.theory_of ctxt; fun class_relation _ (x, _) _ = x; fun type_constructor (tyco, _) xs class = inst_params thy tyco (Sorts.complete_sort algebra [class]) @ (maps o maps) fst xs; fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort); in flat (Sorts.of_sort_derivation algebra { class_relation = K class_relation, type_constructor = type_constructor, type_variable = type_variable } (T, proj_sort sort) handle Sorts.CLASS_ERROR _ => [] (*permissive!*)) end; fun add_arity ctxt vardeps (class, tyco) = AList.default (op =) ((class, tyco), map_range (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k)) (Sign.arity_number (Proof_Context.theory_of ctxt) tyco)); fun add_cert ctxt vardeps (c, (proto_lhs, proto_cert)) (rhss, eqngr) = if can (Graph.get_node eqngr) c then (rhss, eqngr) else let val thy = Proof_Context.theory_of ctxt; val lhs = map_index (fn (k, (v, _)) => (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs; val cert = proto_cert |> Code.constrain_cert thy (map (Sign.minimize_sort thy o snd) lhs) |> Code.conclude_cert; val (vs, rhss') = Code.typargs_deps_of_cert thy cert; val eqngr' = Graph.new_node (c, (vs, cert)) eqngr; in (map (pair c) rhss' @ rhss, eqngr') end; fun extend_arities_eqngr raw_ctxt cs ts (arities, (eqngr : code_graph)) = let val thy = Proof_Context.theory_of raw_ctxt; val {pre, ...} = the_thmproc thy; val ctxt = put_simpset pre raw_ctxt; val cs_rhss = (fold o fold_aterms) (fn Const (c_ty as (c, _)) => insert (op =) (c, (map (styp_of NONE) o Sign.const_typargs thy) c_ty) | _ => I) ts []; val (vardeps, (eqntab, insts)) = empty_vardeps_data |> fold (ensure_fun ctxt arities eqngr) cs |> fold (ensure_rhs ctxt arities eqngr) cs_rhss; val arities' = fold (add_arity ctxt vardeps) insts arities; val algebra = Sorts.subalgebra (Context.Theory thy) (is_proper_class thy) (AList.lookup (op =) arities') (Sign.classes_of thy); val (rhss, eqngr') = Symtab.fold (add_cert ctxt vardeps) eqntab ([], eqngr); fun deps_of (c, rhs) = c :: maps (dicts_of ctxt algebra) (rhs ~~ sortargs eqngr' c); val eqngr'' = fold (fn (c, rhs) => fold (curry Graph.add_edge c) (deps_of rhs)) rhss eqngr'; in (algebra, (arities', eqngr'')) end; (** store for preprocessed arities and code equations **) structure Wellsorted = Code_Data ( type T = ((string * class) * sort list) list * code_graph; val empty = ([], Graph.empty); ); (** retrieval and evaluation interfaces **) (* naming conventions * evaluator "eval" is either * conversion "conv" * value computation "comp" * "evaluation" is a lifting of an evaluator *) fun obtain ignore_cache = timed "preprocessing equations" #ctxt (fn { ctxt, consts, terms } => apsnd snd (Wellsorted.change_yield (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt)) (extend_arities_eqngr ctxt consts terms))) #> (fn (algebra, eqngr) => { algebra = algebra, eqngr = eqngr }); fun dynamic_evaluation eval ctxt t = let val consts = fold_aterms (fn Const (c, _) => insert (op =) c | _ => I) t []; val { algebra, eqngr } = obtain false { ctxt = ctxt, consts = consts, terms = [t] }; in eval algebra eqngr t end; fun static_evaluation ctxt consts eval = eval (obtain true { ctxt = ctxt, consts = consts, terms = [] }); fun dynamic_conv ctxt conv = Sandwich.conversion (value_sandwich ctxt) (dynamic_evaluation conv) ctxt; fun dynamic_value ctxt lift_postproc evaluator = Sandwich.computation (value_sandwich ctxt) lift_postproc (dynamic_evaluation evaluator) ctxt; fun static_conv { ctxt, consts } conv = Sandwich.conversion (value_sandwich ctxt) (static_evaluation ctxt consts conv); fun static_value { ctxt, lift_postproc, consts } comp = Sandwich.computation (value_sandwich ctxt) lift_postproc (static_evaluation ctxt consts comp); (** setup **) val _ = Theory.setup ( let fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I); fun add_del_attribute_parser process = Attrib.add_del (mk_attribute (process Simplifier.add_simp)) (mk_attribute (process Simplifier.del_simp)); in Attrib.setup \<^binding>\code_unfold\ (add_del_attribute_parser process_unfold) "preprocessing equations for code generator" #> Attrib.setup \<^binding>\code_post\ (add_del_attribute_parser process_post) "postprocessing equations for code generator" #> Attrib.setup \<^binding>\code_abbrev\ (add_del_attribute_parser process_abbrev) "post- and preprocessing equations for code generator" #> Attrib.setup \<^binding>\code_preproc_trace\ ((Scan.lift (Args.$$$ "off" >> K trace_none) || (Scan.lift (Args.$$$ "only" |-- Args.colon |-- Scan.repeat1 Parse.term)) >> trace_only_ext || Scan.succeed trace_all) >> (Thm.declaration_attribute o K)) "tracing of the code generator preprocessor" end); val _ = Outer_Syntax.command \<^command_keyword>\print_codeproc\ "print code preprocessor setup" (Scan.succeed (Toplevel.keep (print_codeproc o Toplevel.context_of))); end; (*struct*) diff --git a/src/Tools/Code/code_printer.ML b/src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML +++ b/src/Tools/Code/code_printer.ML @@ -1,448 +1,448 @@ (* Title: Tools/Code/code_printer.ML Author: Florian Haftmann, TU Muenchen Generic operations for pretty printing of target language code. *) signature CODE_PRINTER = sig type itype = Code_Thingol.itype type iterm = Code_Thingol.iterm type const = Code_Thingol.const type dict = Code_Thingol.dict val eqn_error: theory -> thm option -> string -> 'a val @@ : 'a * 'a -> 'a list val @| : 'a list * 'a -> 'a list val str: string -> Pretty.T val concat: Pretty.T list -> Pretty.T val brackets: Pretty.T list -> Pretty.T val enclose: string -> string -> Pretty.T list -> Pretty.T val commas: Pretty.T list -> Pretty.T list val enum: string -> string -> string -> Pretty.T list -> Pretty.T val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T val semicolon: Pretty.T list -> Pretty.T val doublesemicolon: Pretty.T list -> Pretty.T val indent: int -> Pretty.T -> Pretty.T val markup_stmt: Code_Symbol.T -> Pretty.T -> Pretty.T val format: Code_Symbol.T list -> int -> Pretty.T -> string type var_ctxt val make_vars: string list -> var_ctxt val intro_vars: string list -> var_ctxt -> var_ctxt val lookup_var: var_ctxt -> string -> string val intro_base_names: (string -> bool) -> (string -> string) -> string list -> var_ctxt -> var_ctxt val intro_base_names_for: (string -> bool) -> (Code_Symbol.T -> string) -> iterm list -> var_ctxt -> var_ctxt val aux_params: var_ctxt -> iterm list list -> string list type literals val Literals: { literal_string: string -> string, literal_numeral: int -> string, literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string } -> literals val literal_string: literals -> string -> string val literal_numeral: literals -> int -> string val literal_list: literals -> Pretty.T list -> Pretty.T val infix_cons: literals -> int * string type lrx val L: lrx val R: lrx val X: lrx type fixity val BR: fixity val NOBR: fixity val INFX: int * lrx -> fixity val APP: fixity val brackify: fixity -> Pretty.T list -> Pretty.T val brackify_infix: int * lrx -> fixity -> Pretty.T * Pretty.T * Pretty.T -> Pretty.T val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T val gen_applify: bool -> string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T val tuplify: (fixity -> 'a -> Pretty.T) -> fixity -> 'a list -> Pretty.T option type raw_const_syntax val plain_const_syntax: string -> raw_const_syntax type simple_const_syntax val simple_const_syntax: simple_const_syntax -> raw_const_syntax type complex_const_syntax val complex_const_syntax: complex_const_syntax -> raw_const_syntax val parse_const_syntax: raw_const_syntax parser val requires_args: raw_const_syntax -> int datatype const_printer = Plain_printer of string | Complex_printer of (var_ctxt -> fixity -> iterm -> Pretty.T) -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T type const_syntax = int * const_printer val prep_const_syntax: theory -> literals -> string -> raw_const_syntax -> const_syntax type tyco_syntax val parse_tyco_syntax: tyco_syntax parser val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list) -> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T) -> (string -> const_syntax option) -> thm option -> var_ctxt -> fixity -> const * iterm list -> Pretty.T val gen_print_bind: (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T) -> thm option -> fixity -> iterm -> var_ctxt -> Pretty.T * var_ctxt type identifiers type printings type data val empty_data: data val map_data: (string list * identifiers * printings -> string list * identifiers * printings) -> data -> data val merge_data: data * data -> data val the_reserved: data -> string list; val the_identifiers: data -> identifiers; val the_printings: data -> printings; end; structure Code_Printer : CODE_PRINTER = struct open Basic_Code_Symbol; open Code_Thingol; (** generic nonsense *) fun eqn_error thy (SOME thm) s = error (s ^ ",\nin equation " ^ Thm.string_of_thm_global thy thm) | eqn_error _ NONE s = error s; val code_presentationN = "code_presentation"; val stmt_nameN = "stmt_name"; val _ = Markup.add_mode code_presentationN YXML.output_markup; (** assembling and printing text pieces **) infixr 5 @@; infixr 5 @|; fun x @@ y = [x, y]; fun xs @| y = xs @ [y]; fun with_no_print_mode f = Print_Mode.setmp [] f; val str = with_no_print_mode Pretty.str; val concat = Pretty.block o Pretty.breaks; val commas = with_no_print_mode Pretty.commas; fun enclose l r = with_no_print_mode (Pretty.enclose l r); val brackets = enclose "(" ")" o Pretty.breaks; fun enum sep l r = with_no_print_mode (Pretty.enum sep l r); fun enum_default default sep l r [] = str default | enum_default default sep l r xs = enum sep l r xs; fun semicolon ps = Pretty.block [concat ps, str ";"]; fun doublesemicolon ps = Pretty.block [concat ps, str ";;"]; fun indent i = with_no_print_mode (Pretty.indent i); fun with_presentation_marker f = Print_Mode.setmp [code_presentationN] f; fun markup_stmt sym = with_presentation_marker (Pretty.mark (code_presentationN, [(stmt_nameN, Code_Symbol.marker sym)])); fun filter_presentation [] xml = Buffer.build (fold XML.add_content xml) | filter_presentation presentation_syms xml = let val presentation_idents = map Code_Symbol.marker presentation_syms fun is_selected (name, attrs) = name = code_presentationN andalso member (op =) presentation_idents (the (Properties.get attrs stmt_nameN)); fun add_content_with_space tree (is_first, buf) = buf |> not is_first ? Buffer.add "\n\n" |> XML.add_content tree |> pair false; fun filter (XML.Elem (name_attrs, xs)) = fold (if is_selected name_attrs then add_content_with_space else filter) xs | filter (XML.Text _) = I; in snd (fold filter xml (true, Buffer.empty)) end; fun format presentation_names width = with_presentation_marker (Pretty.string_of_margin width) #> YXML.parse_body #> filter_presentation presentation_names #> Buffer.add "\n" #> Buffer.content; (** names and variable name contexts **) type var_ctxt = string Symtab.table * Name.context; fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty, Name.make_context names); fun intro_vars names (namemap, namectxt) = let val (names', namectxt') = fold_map Name.variant names namectxt; val namemap' = fold2 (curry Symtab.update) names names' namemap; in (namemap', namectxt') end; fun lookup_var (namemap, _) name = case Symtab.lookup namemap name of SOME name' => name' | NONE => error ("Invalid name in context: " ^ quote name); fun aux_params vars lhss = let fun fish_param _ (w as SOME _) = w | fish_param (IVar (SOME v)) NONE = SOME v | fish_param _ NONE = NONE; fun fillup_param _ (_, SOME v) = v | fillup_param x (i, NONE) = x ^ string_of_int i; val fished1 = fold (map2 fish_param) lhss (replicate (length (hd lhss)) NONE); val x = singleton (Name.variant_list (map_filter I fished1)) "x"; val fished2 = map_index (fillup_param x) fished1; val (fished3, _) = fold_map Name.variant fished2 Name.context; val vars' = intro_vars fished3 vars; in map (lookup_var vars') fished3 end; fun intro_base_names no_syntax deresolve = map_filter (fn name => if no_syntax name then let val name' = deresolve name in if Long_Name.is_qualified name' then NONE else SOME name' end else NONE) #> intro_vars; fun intro_base_names_for no_syntax deresolve ts = [] |> fold Code_Thingol.add_constsyms ts |> intro_base_names (fn Constant const => no_syntax const | _ => true) deresolve; (** pretty literals **) datatype literals = Literals of { literal_string: string -> string, literal_numeral: int -> string, literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string }; fun dest_Literals (Literals lits) = lits; val literal_string = #literal_string o dest_Literals; val literal_numeral = #literal_numeral o dest_Literals; val literal_list = #literal_list o dest_Literals; val infix_cons = #infix_cons o dest_Literals; (** syntax printer **) (* binding priorities *) datatype lrx = L | R | X; datatype fixity = BR | NOBR | INFX of (int * lrx); val APP = INFX (~1, L); fun fixity_lrx L L = false | fixity_lrx R R = false | fixity_lrx _ _ = true; fun fixity NOBR _ = false | fixity _ NOBR = false | fixity (INFX (pr, lr)) (INFX (pr_ctxt, lr_ctxt)) = pr < pr_ctxt orelse pr = pr_ctxt andalso fixity_lrx lr lr_ctxt orelse pr_ctxt = ~1 | fixity BR (INFX _) = false | fixity _ _ = true; fun gen_brackify _ [p] = p | gen_brackify true (ps as _::_) = enclose "(" ")" ps | gen_brackify false (ps as _::_) = Pretty.block ps; fun brackify fxy_ctxt = gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks; fun brackify_infix infx fxy_ctxt (l, m, r) = gen_brackify (fixity (INFX infx) fxy_ctxt) [l, str " ", m, Pretty.brk 1, r]; fun brackify_block fxy_ctxt p1 ps p2 = let val p = Pretty.block_enclose (p1, p2) ps in if fixity BR fxy_ctxt then enclose "(" ")" [p] else p end; fun gen_applify strict opn cls f fxy_ctxt p [] = if strict then gen_brackify (fixity BR fxy_ctxt) [p, str (opn ^ cls)] else p | gen_applify strict opn cls f fxy_ctxt p ps = gen_brackify (fixity BR fxy_ctxt) (p @@ enum "," opn cls (map f ps)); fun applify opn = gen_applify false opn; fun tuplify _ _ [] = NONE | tuplify print fxy [x] = SOME (print fxy x) | tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs)); (* generic syntax *) type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T) -> fixity -> (iterm * itype) list -> Pretty.T); type complex_const_syntax = int * (literals -> (var_ctxt -> fixity -> iterm -> Pretty.T) -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T); datatype raw_const_syntax = plain_const_syntax of string | complex_const_syntax of complex_const_syntax; fun simple_const_syntax syn = complex_const_syntax (apsnd (fn f => fn _ => fn print => fn _ => fn vars => f (print vars)) syn); fun requires_args (plain_const_syntax _) = 0 | requires_args (complex_const_syntax (k, _)) = k; datatype const_printer = Plain_printer of string | Complex_printer of (var_ctxt -> fixity -> iterm -> Pretty.T) -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T; type const_syntax = int * const_printer; fun prep_const_syntax thy literals c (plain_const_syntax s) = (Code.args_number thy c, Plain_printer s) | prep_const_syntax thy literals c (complex_const_syntax (n, f))= (n, Complex_printer (f literals)); fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy (app as ({ sym, dom, ... }, ts)) = case sym of Constant const => (case const_syntax const of NONE => brackify fxy (print_app_expr some_thm vars app) | SOME (_, Plain_printer s) => brackify fxy (str s :: map (print_term some_thm vars BR) ts) | SOME (k, Complex_printer print) => let fun print' fxy ts = print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom); in if k = length ts then print' fxy ts else if k < length ts then case chop k ts of (ts1, ts2) => brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2) else print_term some_thm vars fxy (Code_Thingol.eta_expand k app) end) | _ => brackify fxy (print_app_expr some_thm vars app); fun gen_print_bind print_term thm (fxy : fixity) pat vars = let - val vs = Code_Thingol.fold_varnames (insert (op =)) pat []; + val vs = build (Code_Thingol.fold_varnames (insert (op =)) pat); val vars' = intro_vars vs vars; in (print_term thm vars' fxy pat, vars') end; type tyco_syntax = int * ((fixity -> itype -> Pretty.T) -> fixity -> itype list -> Pretty.T); (* mixfix syntax *) datatype 'a mixfix = Arg of fixity | String of string | Break; fun printer_of_mixfix prep_arg (fixity_this, mfx) = let fun is_arg (Arg _) = true | is_arg _ = false; val i = (length o filter is_arg) mfx; fun fillin _ [] [] = [] | fillin print (Arg fxy :: mfx) (a :: args) = (print fxy o prep_arg) a :: fillin print mfx args | fillin print (String s :: mfx) args = str s :: fillin print mfx args | fillin print (Break :: mfx) args = Pretty.brk 1 :: fillin print mfx args; in (i, fn print => fn fixity_ctxt => fn args => gen_brackify (fixity fixity_this fixity_ctxt) (fillin print mfx args)) end; fun read_infix (fixity_this, i) s = let val l = case fixity_this of L => INFX (i, L) | _ => INFX (i, X); val r = case fixity_this of R => INFX (i, R) | _ => INFX (i, X); in (INFX (i, fixity_this), [Arg l, String " ", String s, Break, Arg r]) end; fun read_mixfix s = let val sym_any = Scan.one Symbol.not_eof; val parse = Scan.optional ($$ "!" >> K NOBR) BR -- Scan.repeat ( ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR)) || ($$ "_" >> K (Arg BR)) || ($$ "/" |-- Scan.repeat ($$ " ") >> (K Break)) || (Scan.repeat1 ( $$ "'" |-- sym_any || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")") sym_any) >> (String o implode))); fun err s (_, NONE) = (fn () => "malformed mixfix annotation: " ^ quote s) | err _ (_, SOME msg) = msg; in case Scan.finite Symbol.stopper parse (Symbol.explode s) of (fixity_mixfix, []) => fixity_mixfix | _ => Scan.!! (err s) Scan.fail () end; val parse_fixity = (\<^keyword>\infix\ >> K X) || (\<^keyword>\infixl\ >> K L) || (\<^keyword>\infixr\ >> K R) fun parse_mixfix x = (Parse.string >> read_mixfix || parse_fixity -- Parse.nat -- Parse.string >> (fn ((fixity, i), s) => read_infix (fixity, i) s)) x; fun syntax_of_mixfix of_plain of_printer prep_arg (BR, [String s]) = of_plain s | syntax_of_mixfix of_plain of_printer prep_arg (fixity, mfx) = of_printer (printer_of_mixfix prep_arg (fixity, mfx)); fun parse_tyco_syntax x = (parse_mixfix >> syntax_of_mixfix (fn s => (0, (K o K o K o str) s)) I I) x; val parse_const_syntax = parse_mixfix >> syntax_of_mixfix plain_const_syntax simple_const_syntax fst; (** custom data structure **) type identifiers = (string list * string, string list * string, string list * string, string list * string, string list * string, string list * string) Code_Symbol.data; type printings = (const_syntax, tyco_syntax, string, unit, unit, (Pretty.T * Code_Symbol.T list)) Code_Symbol.data; datatype data = Data of { reserved: string list, identifiers: identifiers, printings: printings }; fun make_data (reserved, identifiers, printings) = Data { reserved = reserved, identifiers = identifiers, printings = printings }; val empty_data = make_data ([], Code_Symbol.empty_data, Code_Symbol.empty_data); fun map_data f (Data { reserved, identifiers, printings }) = make_data (f (reserved, identifiers, printings)); fun merge_data (Data { reserved = reserved1, identifiers = identifiers1, printings = printings1 }, Data { reserved = reserved2, identifiers = identifiers2, printings = printings2 }) = make_data (merge (op =) (reserved1, reserved2), Code_Symbol.merge_data (identifiers1, identifiers2), Code_Symbol.merge_data (printings1, printings2)); fun the_reserved (Data { reserved, ... }) = reserved; fun the_identifiers (Data { identifiers , ... }) = identifiers; fun the_printings (Data { printings, ... }) = printings; end; (*struct*) diff --git a/src/Tools/Code/code_runtime.ML b/src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML +++ b/src/Tools/Code/code_runtime.ML @@ -1,885 +1,885 @@ (* Title: Tools/Code/code_runtime.ML Author: Florian Haftmann, TU Muenchen Runtime services building on code generation into implementation language SML. *) signature CODE_RUNTIME = sig val target: string val value: Proof.context -> (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string -> string * string -> 'a type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string val dynamic_value: 'a cookie -> Proof.context -> string option -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a option val dynamic_value_strict: 'a cookie -> Proof.context -> string option -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a val dynamic_value_exn: 'a cookie -> Proof.context -> string option -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a Exn.result val dynamic_holds_conv: Proof.context -> conv val code_reflect: (string * string list option) list -> string list -> string -> Path.binding option -> theory -> theory val code_reflect_cmd: (string * string list option) list -> string list -> string -> Path.binding option -> theory -> theory datatype truth = Holds val put_truth: (unit -> truth) -> Proof.context -> Proof.context val mount_computation: Proof.context -> (string * typ) list -> typ -> (term -> 'ml) -> ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a val mount_computation_conv: Proof.context -> (string * typ) list -> typ -> (term -> 'ml) -> (Proof.context -> 'ml -> conv) -> Proof.context -> conv val mount_computation_check: Proof.context -> (string * typ) list -> (term -> truth) -> Proof.context -> conv val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory val trace: bool Config.T end; structure Code_Runtime : CODE_RUNTIME = struct open Basic_Code_Symbol; (** ML compiler as evaluation environment **) (* technical prerequisites *) val thisN = "Code_Runtime"; val prefix_this = Long_Name.append thisN; val truthN = prefix_this "truth"; val HoldsN = prefix_this "Holds"; val target = "Eval"; datatype truth = Holds; val _ = Theory.setup (Code_Target.add_derived_target (target, [(Code_ML.target_SML, I)]) #> Code_Target.set_printings (Type_Constructor (\<^type_name>\prop\, [(target, SOME (0, (K o K o K) (Code_Printer.str truthN)))])) #> Code_Target.set_printings (Constant (\<^const_name>\Code_Generator.holds\, [(target, SOME (Code_Printer.plain_const_syntax HoldsN))])) #> Code_Target.add_reserved target thisN #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]); (*avoid further pervasive infix names*) val trace = Attrib.setup_config_bool \<^binding>\code_runtime_trace\ (K false); fun compile_ML verbose code context = (if Config.get_generic context trace then tracing code else (); Code_Preproc.timed "compiling ML" Context.proof_of (ML_Context.exec (fn () => ML_Compiler0.ML ML_Env.context {line = 0, file = "generated code", verbose = verbose, debug = false} code)) context); fun value ctxt (get, put, put_ml) (prelude, value) = let val code = prelude ^ "\nval _ = Context.put_generic_context (SOME (Context.map_proof (" ^ put_ml ^ " (fn () => " ^ value ^ ")) (Context.the_generic_context ())))"; val ctxt' = ctxt |> put (fn () => error ("Bad compilation for " ^ quote put_ml)) |> Context.proof_map (compile_ML false code); val computator = get ctxt'; in Code_Preproc.timed_exec "running ML" computator ctxt' end; (* evaluation into ML language values *) type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string; fun reject_vars ctxt t = ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t); fun build_compilation_text ctxt some_target program consts = Code_Target.compilation_text ctxt (the_default target some_target) program consts false #>> (fn ml_modules => space_implode "\n\n" (map snd ml_modules)); fun run_compilation_text cookie ctxt comp vs_t args = let val (program_code, value_name) = comp vs_t; val value_code = space_implode " " (value_name :: "()" :: map (enclose "(" ")") args); in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end; fun partiality_as_none e = SOME (Exn.release e) handle General.Match => NONE | General.Bind => NONE | General.Fail _ => NONE; fun dynamic_value_exn cookie ctxt some_target postproc t args = let val _ = reject_vars ctxt t; val _ = if Config.get ctxt trace then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term ctxt t)) else () fun comp program _ vs_ty_t deps = run_compilation_text cookie ctxt (build_compilation_text ctxt some_target program deps) vs_ty_t args; in Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) comp t end; fun dynamic_value_strict cookie ctxt some_target postproc t args = Exn.release (dynamic_value_exn cookie ctxt some_target postproc t args); fun dynamic_value cookie ctxt some_target postproc t args = partiality_as_none (dynamic_value_exn cookie ctxt some_target postproc t args); (* evaluation for truth or nothing *) structure Truth_Result = Proof_Data ( type T = unit -> truth; val empty: T = fn () => raise Fail "Truth_Result"; fun init _ = empty; ); val put_truth = Truth_Result.put; val truth_cookie = (Truth_Result.get, put_truth, prefix_this "put_truth"); local val reject_vars = fn ctxt => tap (reject_vars ctxt o Thm.term_of); fun check_holds ctxt evaluator vs_t ct = let val t = Thm.term_of ct; val _ = if fastype_of t <> propT then error ("Not a proposition: " ^ Syntax.string_of_term ctxt t) else (); val iff = Thm.cterm_of ctxt (Term.Const (\<^const_name>\Pure.eq\, propT --> propT --> propT)); val result = case partiality_as_none (run_compilation_text truth_cookie ctxt evaluator vs_t []) of SOME Holds => true | _ => false; in Thm.mk_binop iff ct (if result then \<^cprop>\PROP Code_Generator.holds\ else ct) end; val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (\<^binding>\holds_by_evaluation\, fn (ctxt, evaluator, vs_t, ct) => check_holds ctxt evaluator vs_t ct))); fun check_holds_oracle ctxt evaluator vs_ty_t ct = raw_check_holds_oracle (ctxt, evaluator, vs_ty_t, ct); in fun dynamic_holds_conv ctxt = Code_Thingol.dynamic_conv ctxt (fn program => fn vs_t => fn deps => check_holds_oracle ctxt (build_compilation_text ctxt NONE program deps) vs_t) o reject_vars ctxt; end; (*local*) (** generator for computations -- partial implementations of the universal morphism from Isabelle to ML terms **) (* auxiliary *) val generated_computationN = "Generated_Computation"; (* possible type signatures of constants *) fun typ_signatures' T = let val (Ts, T') = strip_type T; in map_range (fn n => (drop n Ts ---> T', take n Ts)) (length Ts + 1) end; fun typ_signatures cTs = let fun add (c, T) = fold (fn (T, Ts) => Typtab.map_default (T, []) (cons (c, Ts))) (typ_signatures' T); in Typtab.empty |> fold add cTs |> Typtab.lookup_list end; (* name mangling *) local fun tycos_of (Type (tyco, Ts)) = maps tycos_of Ts @ [tyco] | tycos_of _ = []; val ml_name_of = Name.desymbolize NONE o Long_Name.base_name; in val covered_constsN = "covered_consts"; fun of_term_for_typ Ts = let val names = Ts |> map (suffix "_of_term" o space_implode "_" o map ml_name_of o tycos_of) |> Name.variant_list []; in the o AList.lookup (op =) (Ts ~~ names) end; fun eval_for_const ctxt cTs = let fun symbol_list (c, T) = c :: maps tycos_of (Sign.const_typargs (Proof_Context.theory_of ctxt) (c, T)) val names = cTs |> map (prefix "eval_" o space_implode "_" o map ml_name_of o symbol_list) |> Name.variant_list []; in the o AList.lookup (op =) (cTs ~~ names) end; end; (* checks for input terms *) fun monomorphic T = fold_atyps ((K o K) false) T true; fun check_typ ctxt T t = Syntax.check_term ctxt (Type.constraint T t); fun check_computation_input ctxt cTs t = let fun check t = check_comb (strip_comb t) and check_comb (t as Abs _, _) = error ("Bad term, contains abstraction: " ^ Syntax.string_of_term ctxt t) | check_comb (t as Const (cT as (c, T)), ts) = let val _ = if not (member (op =) cTs cT) then error ("Bad term, computation cannot proceed on constant " ^ Syntax.string_of_term ctxt t) else (); val _ = if not (monomorphic T) then error ("Bad term, contains polymorphic constant " ^ Syntax.string_of_term ctxt t) else (); val _ = map check ts; in () end; val _ = check t; in t end; (* code generation for of the universal morphism *) val print_const = ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_typ; fun print_of_term_funs { typ_signatures_for, eval_for_const, of_term_for_typ } Ts = let val var_names = map_range (fn n => "t" ^ string_of_int (n + 1)); fun print_lhs c xs = "Const (" ^ quote c ^ ", _)" |> fold (fn x => fn s => s ^ " $ " ^ x) xs |> enclose "(" ")"; fun print_rhs c Ts T xs = eval_for_const (c, Ts ---> T) |> fold2 (fn T' => fn x => fn s => s ^ (" (" ^ of_term_for_typ T' ^ " " ^ x ^ ")")) Ts xs fun print_eq T (c, Ts) = let val xs = var_names (length Ts); in print_lhs c xs ^ " = " ^ print_rhs c Ts T xs end; fun print_eqs T = let val typ_signs = typ_signatures_for T; val name = of_term_for_typ T; in map (print_eq T) typ_signs |> map (prefix (name ^ " ")) |> space_implode "\n | " end; in map print_eqs Ts |> space_implode "\nand " |> prefix "fun " end; fun print_computation_code ctxt compiled_value [] requested_Ts = if null requested_Ts then ("", []) else error ("No equation available for requested type " ^ Syntax.string_of_typ ctxt (hd requested_Ts)) | print_computation_code ctxt compiled_value cTs requested_Ts = let val proper_cTs = map_filter I cTs; val typ_signatures_for = typ_signatures proper_cTs; fun add_typ T Ts = if member (op =) Ts T then Ts else case typ_signatures_for T of [] => error ("No equation available for requested type " ^ Syntax.string_of_typ ctxt T) | typ_signs => Ts |> cons T |> fold (fold add_typ o snd) typ_signs; - val required_Ts = fold add_typ requested_Ts []; + val required_Ts = build (fold add_typ requested_Ts); val of_term_for_typ' = of_term_for_typ required_Ts; val eval_for_const' = eval_for_const ctxt proper_cTs; val eval_for_const'' = the_default "_" o Option.map eval_for_const'; val eval_tuple = enclose "(" ")" (commas (map eval_for_const' proper_cTs)); fun mk_abs s = "fn " ^ s ^ " => "; val eval_abs = space_implode "" (map (mk_abs o eval_for_const'') cTs); val of_term_code = print_of_term_funs { typ_signatures_for = typ_signatures_for, eval_for_const = eval_for_const', of_term_for_typ = of_term_for_typ' } required_Ts; val of_term_names = map (Long_Name.append generated_computationN o of_term_for_typ') requested_Ts; in cat_lines [ "structure " ^ generated_computationN ^ " =", "struct", "", "val " ^ covered_constsN ^ " = " ^ ML_Syntax.print_list print_const proper_cTs ^ ";", "", "val " ^ eval_tuple ^ " = " ^ compiled_value ^ " ()", " (" ^ eval_abs, " " ^ eval_tuple ^ ");", "", of_term_code, "", "end" ] |> rpair of_term_names end; (* dedicated preprocessor for computations *) structure Computation_Preproc_Data = Theory_Data ( type T = thm list; val empty = []; val merge = Library.merge Thm.eq_thm_prop; ); local fun add thm thy = let val thms = Simplifier.mksimps (Proof_Context.init_global thy) thm; in thy |> Computation_Preproc_Data.map (fold (insert Thm.eq_thm_prop o Thm.trim_context) thms) end; fun get ctxt = Computation_Preproc_Data.get (Proof_Context.theory_of ctxt) |> map (Thm.transfer' ctxt) in fun preprocess_conv { ctxt } = let val rules = get ctxt; in fn ctxt' => Raw_Simplifier.rewrite ctxt' false rules end; fun preprocess_term { ctxt } = let val rules = map (Logic.dest_equals o Thm.plain_prop_of) (get ctxt); in fn ctxt' => Pattern.rewrite_term (Proof_Context.theory_of ctxt') rules [] end; val _ = Theory.setup (Attrib.setup \<^binding>\code_computation_unfold\ (Scan.succeed (Thm.declaration_attribute (fn thm => Context.mapping (add thm) I))) "preprocessing equations for computation"); end; (* mounting computations *) fun prechecked_computation T raw_computation ctxt = check_typ ctxt T #> reject_vars ctxt #> raw_computation ctxt; fun prechecked_conv T raw_conv ctxt = tap (check_typ ctxt T o reject_vars ctxt o Thm.term_of) #> raw_conv ctxt; fun checked_computation cTs raw_computation ctxt = check_computation_input ctxt cTs #> Exn.interruptible_capture raw_computation #> partiality_as_none; fun mount_computation ctxt cTs T raw_computation lift_postproc = let val preprocess = preprocess_term { ctxt = ctxt }; val computation = prechecked_computation T (Code_Preproc.static_value { ctxt = ctxt, lift_postproc = lift_postproc, consts = [] } (K (checked_computation cTs raw_computation))); in fn ctxt' => preprocess ctxt' #> computation ctxt' end; fun mount_computation_conv ctxt cTs T raw_computation conv = let val preprocess = preprocess_conv { ctxt = ctxt }; val computation_conv = prechecked_conv T (Code_Preproc.static_conv { ctxt = ctxt, consts = [] } (K (fn ctxt' => fn t => case checked_computation cTs raw_computation ctxt' t of SOME x => conv ctxt' x | NONE => Conv.all_conv))); in fn ctxt' => preprocess ctxt' then_conv computation_conv ctxt' end; local fun holds ct = Thm.mk_binop \<^cterm>\Pure.eq :: prop \ prop \ prop\ ct \<^cprop>\PROP Code_Generator.holds\; val (_, holds_oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (\<^binding>\holds\, holds))); in fun mount_computation_check ctxt cTs raw_computation = mount_computation_conv ctxt cTs \<^typ>\prop\ raw_computation ((K o K) holds_oracle); end; (** variants of universal runtime code generation **) (*FIXME consolidate variants*) fun runtime_code'' ctxt module_name program tycos consts = let val thy = Proof_Context.theory_of ctxt; val (ml_modules, target_names) = Code_Target.produce_code_for ctxt target module_name NONE [] program false (map Constant consts @ map Type_Constructor tycos); val ml_code = space_implode "\n\n" (map snd ml_modules); val (consts', tycos') = chop (length consts) target_names; val consts_map = map2 (fn const => fn NONE => error ("Constant " ^ (quote o Code.string_of_const thy) const ^ "\nhas a user-defined serialization") | SOME const' => (const, const')) consts consts' val tycos_map = map2 (fn tyco => fn NONE => error ("Type " ^ quote (Proof_Context.markup_type ctxt tyco) ^ "\nhas a user-defined serialization") | SOME tyco' => (tyco, tyco')) tycos tycos'; in (ml_code, (tycos_map, consts_map)) end; fun runtime_code' ctxt some_module_name named_tycos named_consts computation_Ts program evals vs_ty_evals deps = let val thy = Proof_Context.theory_of ctxt; fun the_const (Const cT) = cT | the_const t = error ("No constant after preprocessing: " ^ Syntax.string_of_term ctxt t) val raw_computation_cTs = case evals of Abs (_, _, t) => (map the_const o snd o strip_comb) t | _ => error ("Bad term after preprocessing: " ^ Syntax.string_of_term ctxt evals); val computation_cTs = fold_rev (fn cT => fn cTs => (if member (op =) cTs (SOME cT) then NONE else SOME cT) :: cTs) raw_computation_cTs []; val consts' = fold (fn NONE => I | SOME (c, _) => insert (op =) c) computation_cTs named_consts; val program' = Code_Thingol.consts_program ctxt consts'; (*FIXME insufficient interfaces require double invocation of code generator*) val program'' = Code_Symbol.Graph.merge (K true) (program, program'); val ((ml_modules, compiled_value), deresolve) = Code_Target.compilation_text' ctxt target some_module_name program'' (map Code_Symbol.Type_Constructor named_tycos @ map Code_Symbol.Constant consts' @ deps) true vs_ty_evals; (*FIXME constrain signature*) fun deresolve_tyco tyco = case (deresolve o Code_Symbol.Type_Constructor) tyco of NONE => error ("Type " ^ quote (Proof_Context.markup_type ctxt tyco) ^ "\nhas a user-defined serialization") | SOME c' => c'; fun deresolve_const c = case (deresolve o Code_Symbol.Constant) c of NONE => error ("Constant " ^ (quote o Code.string_of_const thy) c ^ "\nhas a user-defined serialization") | SOME c' => c'; val tyco_names = map deresolve_tyco named_tycos; val const_names = map deresolve_const named_consts; val generated_code = space_implode "\n\n" (map snd ml_modules); val (of_term_code, of_term_names) = print_computation_code ctxt compiled_value computation_cTs computation_Ts; val compiled_computation = generated_code ^ "\n" ^ of_term_code; in compiled_computation |> rpair { tyco_map = named_tycos ~~ tyco_names, const_map = named_consts ~~ const_names, of_term_map = computation_Ts ~~ of_term_names } end; fun funs_of_maps { tyco_map, const_map, of_term_map } = { name_for_tyco = the o AList.lookup (op =) tyco_map, name_for_const = the o AList.lookup (op =) const_map, of_term_for_typ = the o AList.lookup (op =) of_term_map }; fun runtime_code ctxt some_module_name named_tycos named_consts computation_Ts program evals vs_ty_evals deps = runtime_code' ctxt some_module_name named_tycos named_consts computation_Ts program evals vs_ty_evals deps ||> funs_of_maps; (** code and computation antiquotations **) local val mount_computationN = prefix_this "mount_computation"; val mount_computation_convN = prefix_this "mount_computation_conv"; val mount_computation_checkN = prefix_this "mount_computation_check"; structure Code_Antiq_Data = Proof_Data ( type T = { named_consts: string list, computation_Ts: typ list, computation_cTs: (string * typ) list, position_index: int, generated_code: (string * { name_for_tyco: string -> string, name_for_const: string -> string, of_term_for_typ: typ -> string }) lazy }; val empty: T = { named_consts = [], computation_Ts = [], computation_cTs = [], position_index = 0, generated_code = Lazy.lazy (fn () => raise Fail "empty") }; fun init _ = empty; ); val current_position_index = #position_index o Code_Antiq_Data.get; fun register { named_consts, computation_Ts, computation_cTs } ctxt = let val data = Code_Antiq_Data.get ctxt; val named_consts' = union (op =) named_consts (#named_consts data); val computation_Ts' = union (op =) computation_Ts (#computation_Ts data); val computation_cTs' = union (op =) computation_cTs (#computation_cTs data); val position_index' = #position_index data + 1; fun generated_code' () = let val evals = Abs ("eval", map snd computation_cTs' ---> Term.aT [], list_comb (Bound 0, map Const computation_cTs')) |> preprocess_term { ctxt = ctxt } ctxt in Code_Thingol.dynamic_value ctxt (K I) (runtime_code ctxt NONE [] named_consts' computation_Ts') evals end; in ctxt |> Code_Antiq_Data.put { named_consts = named_consts', computation_Ts = computation_Ts', computation_cTs = computation_cTs', position_index = position_index', generated_code = Lazy.lazy generated_code' } end; fun register_const const = register { named_consts = [const], computation_Ts = [], computation_cTs = [] }; fun register_computation cTs T = register { named_consts = [], computation_Ts = [T], computation_cTs = cTs }; fun print body_code_for ctxt ctxt' = let val position_index = current_position_index ctxt; val (code, name_ofs) = (Lazy.force o #generated_code o Code_Antiq_Data.get) ctxt'; val context_code = if position_index = 0 then code else ""; val body_code = body_code_for name_ofs (ML_Context.struct_name ctxt'); in (context_code, body_code) end; fun print_code ctxt const = print (fn { name_for_const, ... } => fn prfx => Long_Name.append prfx (name_for_const const)) ctxt; fun print_computation kind ctxt T = print (fn { of_term_for_typ, ... } => fn prfx => enclose "(" ")" (space_implode " " [ kind, "(Context.proof_of (Context.the_generic_context ()))", Long_Name.implode [prfx, generated_computationN, covered_constsN], (ML_Syntax.atomic o ML_Syntax.print_typ) T, Long_Name.append prfx (of_term_for_typ T) ])) ctxt; fun print_computation_check ctxt = print (fn { of_term_for_typ, ... } => fn prfx => enclose "(" ")" (space_implode " " [ mount_computation_checkN, "(Context.proof_of (Context.the_generic_context ()))", Long_Name.implode [prfx, generated_computationN, covered_constsN], Long_Name.append prfx (of_term_for_typ \<^typ>\prop\) ])) ctxt; fun add_all_constrs ctxt (dT as Type (tyco, Ts)) = case Code.get_type (Proof_Context.theory_of ctxt) tyco of ((vs, constrs), false) => let val subst_TFree = the o AList.lookup (op =) (map fst vs ~~ Ts); val cs = map (fn (c, (_, Ts')) => (c, (map o map_atyps) (fn TFree (v, _) => subst_TFree v) Ts' ---> dT)) constrs; in union (op =) cs #> fold (add_all_constrs ctxt) Ts end | (_, true) => I; fun prep_spec ctxt (raw_ts, raw_dTs) = let val ts = map (Syntax.check_term ctxt) raw_ts; val dTs = map (Syntax.check_typ ctxt) raw_dTs; in [] |> (fold o fold_aterms) (fn (t as Const (cT as (_, T))) => if not (monomorphic T) then error ("Polymorphic constant: " ^ Syntax.string_of_term ctxt t) else insert (op =) cT | _ => I) ts |> fold (fn dT => if not (monomorphic dT) then error ("Polymorphic datatype: " ^ Syntax.string_of_typ ctxt dT) else add_all_constrs ctxt dT) dTs end; in fun ml_code_antiq raw_const ctxt = let val thy = Proof_Context.theory_of ctxt; val const = Code.check_const thy raw_const; in (print_code ctxt const, register_const const ctxt) end; fun gen_ml_computation_antiq kind (raw_T, raw_spec) ctxt = let val cTs = prep_spec ctxt raw_spec; val T = Syntax.check_typ ctxt raw_T; val _ = if not (monomorphic T) then error ("Polymorphic type: " ^ Syntax.string_of_typ ctxt T) else (); in (print_computation kind ctxt T, register_computation cTs T ctxt) end; val ml_computation_antiq = gen_ml_computation_antiq mount_computationN; val ml_computation_conv_antiq = gen_ml_computation_antiq mount_computation_convN; fun ml_computation_check_antiq raw_spec ctxt = let val cTs = insert (op =) (dest_Const \<^Const>\holds\) (prep_spec ctxt raw_spec); in (print_computation_check ctxt, register_computation cTs \<^typ>\prop\ ctxt) end; end; (*local*) (** reflection support **) fun check_datatype thy tyco some_consts = let val declared_constrs = (map fst o snd o fst o Code.get_type thy) tyco; val constrs = case some_consts of SOME [] => [] | SOME consts => let val missing_constrs = subtract (op =) consts declared_constrs; val _ = if null missing_constrs then [] else error ("Missing constructor(s) " ^ commas_quote missing_constrs ^ " for datatype " ^ quote tyco); val false_constrs = subtract (op =) declared_constrs consts; val _ = if null false_constrs then [] else error ("Non-constructor(s) " ^ commas_quote false_constrs ^ " for datatype " ^ quote tyco) in consts end | NONE => declared_constrs; in (tyco, constrs) end; fun add_eval_tyco (tyco, tyco') thy = let val k = Sign.arity_number thy tyco; fun pr pr' _ [] = tyco' | pr pr' _ [ty] = Code_Printer.concat [pr' Code_Printer.BR ty, tyco'] | pr pr' _ tys = Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco'] in thy |> Code_Target.set_printings (Type_Constructor (tyco, [(target, SOME (k, pr))])) end; fun add_eval_constr (const, const') thy = let val k = Code.args_number thy const; fun pr pr' fxy ts = Code_Printer.brackify fxy (const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts))); in thy |> Code_Target.set_printings (Constant (const, [(target, SOME (Code_Printer.simple_const_syntax (k, pr)))])) end; fun add_eval_const (const, const') = Code_Target.set_printings (Constant (const, [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')))])); fun process_reflection (code, (tyco_map, (constr_map, const_map))) module_name NONE thy = thy |> Code_Target.add_reserved target module_name |> Context.theory_map (compile_ML true code) |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map |> fold (add_eval_const o apsnd Code_Printer.str) const_map | process_reflection (code, _) _ (SOME binding) thy = let val code_binding = Path.map_binding Code_Target.code_path binding; val preamble = "(* Generated from " ^ Path.implode (Resources.thy_path (Path.basic (Context.theory_name thy))) ^ "; DO NOT EDIT! *)"; val thy' = Code_Target.export code_binding (preamble ^ "\n\n" ^ code) thy; val _ = Code_Target.code_export_message thy'; in thy' end; fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name file_prefix thy = let val ctxt = Proof_Context.init_global thy; val datatypes = map (fn (raw_tyco, raw_cos) => (prep_type ctxt raw_tyco, (Option.map o map) (prep_const thy) raw_cos)) raw_datatypes; val (tycos, constrs) = map_split (uncurry (check_datatype thy)) datatypes |> apsnd flat; val functions = map (prep_const thy) raw_functions; val consts = constrs @ functions; val program = Code_Thingol.consts_program ctxt consts; val result = runtime_code'' ctxt module_name program tycos consts |> (apsnd o apsnd) (chop (length constrs)); in thy |> process_reflection result module_name file_prefix end; val code_reflect = gen_code_reflect Code_Target.cert_tyco (K I); val code_reflect_cmd = gen_code_reflect Code_Target.read_tyco Code.read_const; (** Isar setup **) local val parse_consts_spec = Scan.optional (Scan.lift (Args.$$$ "terms" -- Args.colon) |-- Scan.repeat1 Args.term) [] -- Scan.optional (Scan.lift (Args.$$$ "datatypes" -- Args.colon) |-- Scan.repeat1 Args.typ) []; in val _ = Theory.setup (ML_Antiquotation.declaration \<^binding>\code\ Args.term (K ml_code_antiq) #> ML_Antiquotation.declaration \<^binding>\computation\ (Args.typ -- parse_consts_spec) (K ml_computation_antiq) #> ML_Antiquotation.declaration \<^binding>\computation_conv\ (Args.typ -- parse_consts_spec) (K ml_computation_conv_antiq) #> ML_Antiquotation.declaration \<^binding>\computation_check\ parse_consts_spec (K ml_computation_check_antiq)); end; local val parse_datatype = Parse.name -- Scan.optional (\<^keyword>\=\ |-- (((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ())) || ((Parse.term ::: (Scan.repeat (\<^keyword>\|\ |-- Parse.term))) >> SOME))) (SOME []); in val _ = Outer_Syntax.command \<^command_keyword>\code_reflect\ "enrich runtime environment with generated code" (Parse.name -- Scan.optional (\<^keyword>\datatypes\ |-- Parse.!!! (parse_datatype ::: Scan.repeat (\<^keyword>\and\ |-- parse_datatype))) [] -- Scan.optional (\<^keyword>\functions\ |-- Parse.!!! (Scan.repeat1 Parse.name)) [] -- Scan.option (\<^keyword>\file_prefix\ |-- Parse.!!! (Parse.position Parse.embedded)) >> (fn (((module_name, raw_datatypes), raw_functions), file_prefix) => Toplevel.theory (fn thy => code_reflect_cmd raw_datatypes raw_functions module_name (Option.map Path.explode_binding file_prefix) thy))); end; (*local*) (** using external SML files as substitute for proper definitions -- only for polyml! **) local structure Loaded_Values = Theory_Data ( type T = string list val empty = [] fun merge data : T = Library.merge (op =) data ); fun notify_val (string, value) = let val _ = #enterVal ML_Env.name_space (string, value); val _ = Theory.setup (Loaded_Values.map (insert (op =) string)); in () end; fun abort _ = error "Only value bindings allowed."; val notifying_context : ML_Compiler0.context = {name_space = {lookupVal = #lookupVal ML_Env.name_space, lookupType = #lookupType ML_Env.name_space, lookupFix = #lookupFix ML_Env.name_space, lookupStruct = #lookupStruct ML_Env.name_space, lookupSig = #lookupSig ML_Env.name_space, lookupFunct = #lookupFunct ML_Env.name_space, enterVal = notify_val, enterType = abort, enterFix = abort, enterStruct = abort, enterSig = abort, enterFunct = abort, allVal = #allVal ML_Env.name_space, allType = #allType ML_Env.name_space, allFix = #allFix ML_Env.name_space, allStruct = #allStruct ML_Env.name_space, allSig = #allSig ML_Env.name_space, allFunct = #allFunct ML_Env.name_space}, print_depth = NONE, here = #here ML_Env.context, print = #print ML_Env.context, error = #error ML_Env.context}; in fun use_file filepath thy = let val thy' = Loaded_Values.put [] thy; val _ = Context.put_generic_context ((SOME o Context.Theory) thy'); val _ = ML_Compiler0.ML notifying_context {line = 0, file = Path.implode filepath, verbose = false, debug = false} (File.read filepath); val thy'' = Context.the_global_context (); val names = Loaded_Values.get thy''; in (names, thy'') end; end; fun add_definiendum (ml_name, (b, T)) thy = thy |> Code_Target.add_reserved target ml_name |> Specification.axiomatization [(b, SOME T, NoSyn)] [] [] [] |-> (fn ([Const (const, _)], _) => Code_Target.set_printings (Constant (const, [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))])) #> tap (fn thy => Code_Target.produce_code (Proof_Context.init_global thy) false [const] target Code_Target.generatedN NONE [])); fun process_file filepath (definienda, thy) = let val (ml_names, thy') = use_file filepath thy; val superfluous = subtract (fn ((name1, _), name2) => name1 = name2) definienda ml_names; val _ = if null superfluous then () else error ("Value binding(s) " ^ commas_quote superfluous ^ " found in external file " ^ Path.print filepath ^ " not present among the given contants binding(s)."); val these_definienda = AList.make (the o AList.lookup (op =) definienda) ml_names; val thy'' = fold add_definiendum these_definienda thy'; val definienda' = fold (AList.delete (op =)) ml_names definienda; in (definienda', thy'') end; fun polyml_as_definition bTs filepaths thy = let val definienda = map (fn bT => ((Binding.name_of o fst) bT, bT)) bTs; val (remaining, thy') = fold process_file filepaths (definienda, thy); val _ = if null remaining then () else error ("Constant binding(s) " ^ commas_quote (map fst remaining) ^ " not present in external file(s)."); in thy' end; end; (*struct*) diff --git a/src/Tools/Code/code_scala.ML b/src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML +++ b/src/Tools/Code/code_scala.ML @@ -1,490 +1,490 @@ (* Title: Tools/Code/code_scala.ML Author: Florian Haftmann, TU Muenchen Serializer for Scala. *) signature CODE_SCALA = sig val target: string end; structure Code_Scala : CODE_SCALA = struct open Basic_Code_Symbol; open Basic_Code_Thingol; open Code_Printer; infixr 5 @@; infixr 5 @|; (** Scala serializer **) val target = "Scala"; val print_scala_string = let fun chr i = "\\u" ^ align_right "0" 4 (Int.fmt StringCvt.HEX i) fun char c = if c = "'" then "\\'" else if c = "\"" then "\\\"" else if c = "\\" then "\\\\" else let val i = ord c in if i < 32 orelse i > 126 then chr i else if i >= 128 then error "non-ASCII byte in Scala string literal" else c end in quote o translate_string char end; datatype scala_stmt = Fun of typscheme * ((iterm list * iterm) * (thm option * bool)) list | Datatype of vname list * ((string * vname list) * itype list) list | Class of (vname * ((class * class) list * (string * itype) list)) * (string * { vs: (vname * sort) list, inst_params: ((string * (const * int)) * (thm * bool)) list, superinst_params: ((string * (const * int)) * (thm * bool)) list }) list; fun print_scala_stmt tyco_syntax const_syntax reserved args_num is_constr (deresolve, deresolve_full) = let val deresolve_const = deresolve o Constant; val deresolve_tyco = deresolve o Type_Constructor; val deresolve_class = deresolve o Type_Class; fun lookup_tyvar tyvars = lookup_var tyvars o Name.enforce_case true; fun intro_tyvars vs = intro_vars (map (Name.enforce_case true o fst) vs); fun print_tyco_expr tyvars fxy (sym, tys) = applify "[" "]" (print_typ tyvars NOBR) fxy ((str o deresolve) sym) tys and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco of NONE => print_tyco_expr tyvars fxy (Type_Constructor tyco, tys) | SOME (_, print) => print (print_typ tyvars) fxy tys) | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v; fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (Type_Class class, [ty]); fun print_tupled_typ tyvars ([], ty) = print_typ tyvars NOBR ty | print_tupled_typ tyvars ([ty1], ty2) = concat [print_typ tyvars BR ty1, str "=>", print_typ tyvars NOBR ty2] | print_tupled_typ tyvars (tys, ty) = concat [enum "," "(" ")" (map (print_typ tyvars NOBR) tys), str "=>", print_typ tyvars NOBR ty]; fun constraint p1 p2 = Pretty.block [p1, str ":", Pretty.brk 1, p2]; fun print_var vars NONE = str "_" | print_var vars (SOME v) = (str o lookup_var vars) v; fun applify_dict tyvars (Dict (_, d)) = applify_plain_dict tyvars d and applify_plain_dict tyvars (Dict_Const (inst, dss)) = applify_dictss tyvars ((str o deresolve o Class_Instance) inst) dss | applify_plain_dict tyvars (Dict_Var { var, class, ... }) = Pretty.block [str "implicitly", enclose "[" "]" [Pretty.block [(str o deresolve_class) class, enclose "[" "]" [(str o lookup_tyvar tyvars) var]]]] and applify_dictss tyvars p dss = applify "(" ")" (applify_dict tyvars) NOBR p (flat dss) fun print_term tyvars is_pat some_thm vars fxy (IConst const) = print_app tyvars is_pat some_thm vars fxy (const, []) | print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) = (case Code_Thingol.unfold_const_app t of SOME app => print_app tyvars is_pat some_thm vars fxy app | _ => applify "(" ")" (print_term tyvars is_pat some_thm vars NOBR) fxy (print_term tyvars is_pat some_thm vars BR t1) [t2]) | print_term tyvars is_pat some_thm vars fxy (IVar v) = print_var vars v | print_term tyvars is_pat some_thm vars fxy (t as _ `|=> _) = let val (vs_tys, body) = Code_Thingol.unfold_abs t; val (ps, vars') = fold_map (print_abs_head tyvars) vs_tys vars; in brackets (ps @| print_term tyvars false some_thm vars' NOBR body) end | print_term tyvars is_pat some_thm vars fxy (ICase case_expr) = (case Code_Thingol.unfold_const_app (#primitive case_expr) of SOME (app as ({ sym = Constant const, ... }, _)) => if is_none (const_syntax const) then print_case tyvars some_thm vars fxy case_expr else print_app tyvars is_pat some_thm vars fxy app | NONE => print_case tyvars some_thm vars fxy case_expr) and print_abs_head tyvars (some_v, ty) vars = let val vars' = intro_vars (the_list some_v) vars; in (concat [ enclose "(" ")" [constraint (print_var vars' some_v) (print_typ tyvars NOBR ty)], str "=>" ], vars') end and print_app tyvars is_pat some_thm vars fxy (app as ({ sym, typargs, dom, dicts, ... }, ts)) = let val k = length ts; val typargs' = if is_pat then [] else typargs; val syntax = case sym of Constant const => const_syntax const | _ => NONE; val applify_dicts = if is_pat orelse is_some syntax orelse is_constr sym orelse Code_Thingol.unambiguous_dictss dicts then fn p => K p else applify_dictss tyvars; val (l, print') = case syntax of NONE => (args_num sym, fn fxy => fn ts => applify_dicts (gen_applify (is_constr sym) "(" ")" (print_term tyvars is_pat some_thm vars NOBR) fxy (applify "[" "]" (print_typ tyvars NOBR) NOBR ((str o deresolve) sym) typargs') ts) dicts) | SOME (k, Plain_printer s) => (k, fn fxy => fn ts => applify_dicts (applify "(" ")" (print_term tyvars is_pat some_thm vars NOBR) fxy (applify "[" "]" (print_typ tyvars NOBR) NOBR (str s) typargs') ts) dicts) | SOME (k, Complex_printer print) => (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy (ts ~~ take k dom)) in if k = l then print' fxy ts else if k < l then print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app) else let val (ts1, ts23) = chop l ts; in Pretty.block (print' BR ts1 :: map (fn t => Pretty.block [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts23) end end and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars true) some_thm fxy p and print_case tyvars some_thm vars fxy { clauses = [], ... } = (brackify fxy o Pretty.breaks o map str) ["sys.error(\"empty case\")"] | print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) = let val (bind :: binds, body) = Code_Thingol.unfold_let (ICase case_expr); fun print_match_val ((pat, ty), t) vars = vars |> print_bind tyvars some_thm BR pat |>> (fn p => (false, concat [str "val", constraint p (print_typ tyvars NOBR ty), str "=", print_term tyvars false some_thm vars NOBR t])); fun print_match_seq t vars = ((true, print_term tyvars false some_thm vars NOBR t), vars); fun print_match is_first ((IVar NONE, ty), t) = if Code_Thingol.is_IAbs t andalso is_first then print_match_val ((IVar NONE, ty), t) else print_match_seq t | print_match _ ((pat, ty), t) = print_match_val ((pat, ty), t); val (seps_ps, vars') = vars |> print_match true bind ||>> fold_map (print_match false) binds |>> uncurry cons; val all_seps_ps = seps_ps @ [(true, print_term tyvars false some_thm vars' NOBR body)]; fun insert_seps [(_, p)] = [p] | insert_seps ((_, p) :: (seps_ps as (sep, _) :: _)) = (if sep then Pretty.block [p, str ";"] else p) :: insert_seps seps_ps in brackify_block fxy (str "{") (insert_seps all_seps_ps) (str "}") end | print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } = let fun print_select (pat, body) = let val (p_pat, vars') = print_bind tyvars some_thm NOBR pat vars; val p_body = print_term tyvars false some_thm vars' NOBR body in concat [str "case", p_pat, str "=>", p_body] end; in map print_select clauses |> Pretty.block_enclose (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"], str "}") |> single |> enclose "(" ")" end; fun print_context tyvars vs s = applify "[" "]" (fn (v, sort) => (Pretty.block o map str) (lookup_tyvar tyvars v :: maps (fn class => [" : ", deresolve_class class]) sort)) NOBR (str s) vs; fun print_defhead tyvars vars const vs params tys ty = concat [str "def", constraint (applify "(" ")" (fn (param, ty) => constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty)) NOBR (print_context tyvars vs (deresolve_const const)) (params ~~ tys)) (print_typ tyvars NOBR ty), str "="]; fun print_def const (vs, ty) [] = let val (tys, ty') = Code_Thingol.unfold_fun ty; val params = Name.invent (snd reserved) "a" (length tys); val tyvars = intro_tyvars vs reserved; val vars = intro_vars params reserved; in concat [print_defhead tyvars vars const vs params tys ty', str ("sys.error(" ^ print_scala_string const ^ ")")] end | print_def const (vs, ty) eqs = let - val tycos = fold (fn ((ts, t), _) => - fold Code_Thingol.add_tyconames (t :: ts)) eqs []; + val tycos = build (fold (fn ((ts, t), _) => + fold Code_Thingol.add_tyconames (t :: ts)) eqs); val tyvars = reserved |> intro_base_names (is_none o tyco_syntax) deresolve_tyco tycos |> intro_tyvars vs; val simple = case eqs of [((ts, _), _)] => forall Code_Thingol.is_IVar ts | _ => false; val vars1 = reserved |> intro_base_names_for (is_none o const_syntax) deresolve (map (snd o fst) eqs); val params = if simple then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs else aux_params vars1 (map (fst o fst) eqs); val vars2 = intro_vars params vars1; val (tys', ty') = Code_Thingol.unfold_fun_n (length params) ty; fun tuplify [p] = p | tuplify ps = enum "," "(" ")" ps; fun print_rhs vars' ((_, t), (some_thm, _)) = print_term tyvars false some_thm vars' NOBR t; fun print_clause (eq as ((ts, _), (some_thm, _))) = let val vars' = intro_vars ((fold o Code_Thingol.fold_varnames) (insert (op =)) ts []) vars1; in concat [str "case", tuplify (map (print_term tyvars true some_thm vars' NOBR) ts), str "=>", print_rhs vars' eq] end; val head = print_defhead tyvars vars2 const vs params tys' ty'; in if simple then concat [head, print_rhs vars2 (hd eqs)] else Pretty.block_enclose (concat [head, tuplify (map (str o lookup_var vars2) params), str "match", str "{"], str "}") (map print_clause eqs) end; val print_method = str o Library.enclose "`" "`" o deresolve_full o Constant; fun print_inst class (tyco, { vs, inst_params, superinst_params }) = let val tyvars = intro_tyvars vs reserved; val classtyp = (class, tyco `%% map (ITyVar o fst) vs); fun print_classparam_instance ((classparam, (const as { dom, ... }, dom_length)), (thm, _)) = let val aux_dom = Name.invent_names (snd reserved) "a" dom; val auxs = map fst aux_dom; val vars = intro_vars auxs reserved; val (aux_dom1, aux_dom2) = chop dom_length aux_dom; fun abstract_using [] = [] | abstract_using aux_dom = [enum "," "(" ")" (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux) (print_typ tyvars NOBR ty)) aux_dom), str "=>"]; val aux_abstr1 = abstract_using aux_dom1; val aux_abstr2 = abstract_using aux_dom2; in concat ([str "val", print_method classparam, str "="] @ aux_abstr1 @ aux_abstr2 @| print_app tyvars false (SOME thm) vars NOBR (const, map (IVar o SOME) auxs)) end; in Pretty.block_enclose (concat [str "implicit def", constraint (print_context tyvars vs ((Library.enclose "`" "`" o deresolve_full o Class_Instance) (tyco, class))) (print_dicttyp tyvars classtyp), str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}") (map print_classparam_instance (inst_params @ superinst_params)) end; fun print_stmt (Constant const, (_, Fun ((vs, ty), raw_eqs))) = print_def const (vs, ty) (filter (snd o snd) raw_eqs) | print_stmt (Type_Constructor tyco, (_, Datatype (vs, cos))) = let val tyvars = intro_tyvars (map (rpair []) vs) reserved; fun print_co ((co, vs_args), tys) = concat [Pretty.block ((applify "[" "]" (str o lookup_tyvar tyvars) NOBR (str ("final case class " ^ deresolve_const co)) vs_args) @@ enum "," "(" ")" (map (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg)) (Name.invent_names (snd reserved) "a" tys))), str "extends", applify "[" "]" (str o lookup_tyvar tyvars) NOBR ((str o deresolve_tyco) tyco) vs ]; in Pretty.chunks (applify "[" "]" (str o lookup_tyvar tyvars) NOBR (str ("abstract sealed class " ^ deresolve_tyco tyco)) vs :: map print_co cos) end | print_stmt (Type_Class class, (_, Class ((v, (classrels, classparams)), insts))) = let val tyvars = intro_tyvars [(v, [class])] reserved; fun add_typarg s = Pretty.block [str s, str "[", (str o lookup_tyvar tyvars) v, str "]"]; fun print_super_classes [] = NONE | print_super_classes classrels = SOME (concat (str "extends" :: separate (str "with") (map (add_typarg o deresolve_class o snd) classrels))); fun print_classparam_val (classparam, ty) = concat [str "val", constraint (print_method classparam) ((print_tupled_typ tyvars o Code_Thingol.unfold_fun) ty)]; fun print_classparam_def (classparam, ty) = let val (tys, ty) = Code_Thingol.unfold_fun ty; val [implicit_name] = Name.invent (snd reserved) (lookup_tyvar tyvars v) 1; val proto_vars = intro_vars [implicit_name] reserved; val auxs = Name.invent (snd proto_vars) "a" (length tys); val vars = intro_vars auxs proto_vars; in concat [str "def", constraint (Pretty.block [applify "(" ")" (fn (aux, ty) => constraint ((str o lookup_var vars) aux) (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_const classparam)) (auxs ~~ tys), str "(implicit ", str implicit_name, str ": ", add_typarg (deresolve_class class), str ")"]) (print_typ tyvars NOBR ty), str "=", applify "(" ")" (str o lookup_var vars) NOBR (Pretty.block [str implicit_name, str ".", print_method classparam]) auxs] end; in Pretty.chunks ( (Pretty.block_enclose (concat ([str "trait", (add_typarg o deresolve_class) class] @ the_list (print_super_classes classrels) @ [str "{"]), str "}") (map print_classparam_val classparams)) :: map print_classparam_def classparams @| Pretty.block_enclose (str ("object " ^ deresolve_class class ^ "{"), str "}") (map (print_inst class) insts) ) end; in print_stmt end; fun pickup_instances_for_class program = let val tab = Symtab.empty |> Code_Symbol.Graph.fold (fn (_, (Code_Thingol.Classinst { class, tyco, vs, inst_params, superinst_params, ... }, _)) => Symtab.map_default (class, []) (cons (tyco, { vs = vs, inst_params = inst_params, superinst_params = superinst_params })) | _ => I) program; in Symtab.lookup_list tab end; fun scala_program_of_program ctxt case_insensitive module_name reserved identifiers exports program = let val variant = if case_insensitive then Code_Namespace.variant_case_insensitive else Name.variant; fun namify_module name_fragment ((nsp_class, nsp_object), nsp_common) = let val declare = Name.declare name_fragment; in (name_fragment, ((declare nsp_class, declare nsp_object), declare nsp_common)) end; fun namify_class base ((nsp_class, nsp_object), nsp_common) = let val (base', nsp_class') = variant base nsp_class in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end; fun namify_object base ((nsp_class, nsp_object), nsp_common) = let val (base', nsp_object') = variant base nsp_object in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end; fun namify_common base ((nsp_class, nsp_object), nsp_common) = let val (base', nsp_common') = variant base nsp_common in (base', ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common')) end; fun namify_stmt (Code_Thingol.Fun _) = namify_object | namify_stmt (Code_Thingol.Datatype _) = namify_class | namify_stmt (Code_Thingol.Datatypecons _) = namify_common | namify_stmt (Code_Thingol.Class _) = namify_class | namify_stmt (Code_Thingol.Classrel _) = namify_object | namify_stmt (Code_Thingol.Classparam _) = namify_object | namify_stmt (Code_Thingol.Classinst _) = namify_common; val pickup_instances = pickup_instances_for_class program; fun modify_stmt (_, (_, Code_Thingol.Fun (_, SOME _))) = NONE | modify_stmt (_, (export, Code_Thingol.Fun (x, NONE))) = SOME (export, Fun x) | modify_stmt (_, (export, Code_Thingol.Datatype x)) = SOME (export, Datatype x) | modify_stmt (_, (_, Code_Thingol.Datatypecons _)) = NONE | modify_stmt (Type_Class class, (export, Code_Thingol.Class x)) = SOME (export, Class (x, pickup_instances class)) | modify_stmt (_, (_, Code_Thingol.Classrel _)) = NONE | modify_stmt (_, (_, Code_Thingol.Classparam _)) = NONE | modify_stmt (_, (_, Code_Thingol.Classinst _)) = NONE in Code_Namespace.hierarchical_program ctxt { module_name = module_name, reserved = reserved, identifiers = identifiers, empty_nsp = ((reserved, reserved), reserved), namify_module = namify_module, namify_stmt = namify_stmt, cyclic_modules = true, class_transitive = true, class_relation_public = false, empty_data = (), memorize_data = K I, modify_stmts = map modify_stmt } exports program end; fun serialize_scala case_insensitive ctxt { module_name, reserved_syms, identifiers, includes, class_syntax, tyco_syntax, const_syntax } program exports = let (* build program *) val { deresolver, hierarchical_program = scala_program } = scala_program_of_program ctxt case_insensitive module_name (Name.make_context reserved_syms) identifiers exports program; (* print statements *) fun lookup_constr tyco constr = case Code_Symbol.Graph.get_node program (Type_Constructor tyco) of Code_Thingol.Datatype (_, constrs) => the (AList.lookup (op = o apsnd fst) constrs constr); fun classparams_of_class class = case Code_Symbol.Graph.get_node program (Type_Class class) of Code_Thingol.Class (_, (_, classparams)) => classparams; fun args_num (sym as Constant const) = case Code_Symbol.Graph.get_node program sym of Code_Thingol.Fun (((_, ty), []), _) => (length o fst o Code_Thingol.unfold_fun) ty | Code_Thingol.Fun ((_, ((ts, _), _) :: _), _) => length ts | Code_Thingol.Datatypecons tyco => length (lookup_constr tyco const) | Code_Thingol.Classparam class => (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =) (classparams_of_class class)) const; fun print_stmt prefix_fragments = print_scala_stmt tyco_syntax const_syntax (make_vars reserved_syms) args_num (Code_Thingol.is_constr program) (deresolver prefix_fragments, deresolver []); (* print modules *) fun print_module _ base _ ps = Pretty.chunks2 (str ("object " ^ base ^ " {") :: ps @| str ("} /* object " ^ base ^ " */")); (* serialization *) val p = Pretty.chunks2 (map snd includes @ Code_Namespace.print_hierarchical { print_module = print_module, print_stmt = print_stmt, lift_markup = I } scala_program); in (Code_Target.Singleton ("scala", p), try (deresolver [])) end; val serializer : Code_Target.serializer = Code_Target.parse_args (Scan.optional (Args.$$$ "case_insensitive" >> K true) false >> (fn case_insensitive => serialize_scala case_insensitive)); val literals = let fun numeral_scala k = if ~2147483647 < k andalso k <= 2147483647 then signed_string_of_int k else quote (signed_string_of_int k) in Literals { literal_string = print_scala_string, literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")", literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps], infix_cons = (6, "::") } end; (** Isar setup **) val _ = Theory.setup (Code_Target.add_language (target, { serializer = serializer, literals = literals, check = { env_var = "SCALA_HOME", make_destination = fn p => p + Path.explode "ROOT.scala", make_command = fn _ => "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS ROOT.scala"}, evaluation_args = Token.explode0 Keyword.empty_keywords "case_insensitive"}) #> Code_Target.set_printings (Type_Constructor ("fun", [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => brackify_infix (1, R) fxy ( print_typ BR ty1 (*product type vs. tupled arguments!*), str "=>", print_typ (INFX (1, R)) ty2 )))])) #> fold (Code_Target.add_reserved target) [ "abstract", "case", "catch", "class", "def", "do", "else", "extends", "false", "final", "finally", "for", "forSome", "if", "implicit", "import", "lazy", "match", "new", "null", "object", "override", "package", "private", "protected", "requires", "return", "sealed", "super", "this", "throw", "trait", "try", "true", "type", "val", "var", "while", "with", "yield" ] #> fold (Code_Target.add_reserved target) [ "apply", "sys", "scala", "BigInt", "Nil", "List" ]); end; (*struct*) diff --git a/src/Tools/Code/code_thingol.ML b/src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML +++ b/src/Tools/Code/code_thingol.ML @@ -1,1060 +1,1060 @@ (* Title: Tools/Code/code_thingol.ML Author: Florian Haftmann, TU Muenchen Intermediate language ("Thin-gol") representing executable code. Representation and translation. *) infix 8 `%%; infix 4 `$; infix 4 `$$; infixr 3 `->; infixr 3 `|=>; infixr 3 `|==>; signature BASIC_CODE_THINGOL = sig type vname = string; datatype dict = Dict of (class * class) list * plain_dict and plain_dict = Dict_Const of (string * class) * dict list list | Dict_Var of { var: vname, index: int, length: int, class: class, unique: bool }; datatype itype = `%% of string * itype list | ITyVar of vname; type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list, dom: itype list, annotation: itype option }; datatype iterm = IConst of const | IVar of vname option | `$ of iterm * iterm | `|=> of (vname option * itype) * iterm | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm }; val `-> : itype * itype -> itype; val `$$ : iterm * iterm list -> iterm; val `|==> : (vname option * itype) list * iterm -> iterm; type typscheme = (vname * sort) list * itype; end; signature CODE_THINGOL = sig include BASIC_CODE_THINGOL val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a val unfold_fun: itype -> itype list * itype val unfold_fun_n: int -> itype -> itype list * itype val unfold_app: iterm -> iterm * iterm list val unfold_abs: iterm -> (vname option * itype) list * iterm val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option val split_let_no_pat: iterm -> (((string option * itype) * iterm) * iterm) option val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm val unfold_let_no_pat: iterm -> ((string option * itype) * iterm) list * iterm val split_pat_abs: iterm -> ((iterm * itype) * iterm) option val unfold_pat_abs: iterm -> (iterm * itype) list * iterm val unfold_const_app: iterm -> (const * iterm list) option val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm val is_IVar: iterm -> bool val is_IAbs: iterm -> bool val eta_expand: int -> const * iterm list -> iterm val contains_dict_var: iterm -> bool val unambiguous_dictss: dict list list -> bool val add_constsyms: iterm -> Code_Symbol.T list -> Code_Symbol.T list val add_tyconames: iterm -> string list -> string list val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a datatype stmt = NoStmt | Fun of (typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option | Datatype of vname list * ((string * vname list (*type argument wrt. canonical order*)) * itype list) list | Datatypecons of string | Class of vname * ((class * class) list * (string * itype) list) | Classrel of class * class | Classparam of class | Classinst of { class: string, tyco: string, vs: (vname * sort) list, superinsts: (class * dict list list) list, inst_params: ((string * (const * int)) * (thm * bool)) list, superinst_params: ((string * (const * int)) * (thm * bool)) list }; type program = stmt Code_Symbol.Graph.T val unimplemented: program -> string list val implemented_deps: program -> string list val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt val is_constr: program -> Code_Symbol.T -> bool val is_case: stmt -> bool val group_stmts: Proof.context -> program -> ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list * ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list)) list val read_const_exprs: Proof.context -> string list -> string list val consts_program: Proof.context -> string list -> program val dynamic_conv: Proof.context -> (program -> typscheme * iterm -> Code_Symbol.T list -> conv) -> conv val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> (program -> term -> typscheme * iterm -> Code_Symbol.T list -> 'a) -> term -> 'a val static_conv_thingol: { ctxt: Proof.context, consts: string list } -> ({ program: program, deps: string list } -> Proof.context -> typscheme * iterm -> Code_Symbol.T list -> conv) -> Proof.context -> conv val static_conv_isa: { ctxt: Proof.context, consts: string list } -> (program -> Proof.context -> term -> conv) -> Proof.context -> conv val static_value: { ctxt: Proof.context, lift_postproc: ((term -> term) -> 'a -> 'a), consts: string list } -> ({ program: program, deps: string list } -> Proof.context -> term -> typscheme * iterm -> Code_Symbol.T list -> 'a) -> Proof.context -> term -> 'a end; structure Code_Thingol : CODE_THINGOL = struct open Basic_Code_Symbol; (** auxiliary **) fun unfoldl dest x = case dest x of NONE => (x, []) | SOME (x1, x2) => let val (x', xs') = unfoldl dest x1 in (x', xs' @ [x2]) end; fun unfoldr dest x = case dest x of NONE => ([], x) | SOME (x1, x2) => let val (xs', x') = unfoldr dest x2 in (x1 :: xs', x') end; (** language core - types, terms **) type vname = string; datatype dict = Dict of (class * class) list * plain_dict and plain_dict = Dict_Const of (string * class) * dict list list | Dict_Var of { var: vname, index: int, length: int, class: class, unique: bool }; datatype itype = `%% of string * itype list | ITyVar of vname; fun ty1 `-> ty2 = "fun" `%% [ty1, ty2]; val unfold_fun = unfoldr (fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2) | _ => NONE); fun unfold_fun_n n ty = let val (tys1, ty1) = unfold_fun ty; val (tys3, tys2) = chop n tys1; val ty3 = Library.foldr (op `->) (tys2, ty1); in (tys3, ty3) end; type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list, dom: itype list, annotation: itype option }; datatype iterm = IConst of const | IVar of vname option | `$ of iterm * iterm | `|=> of (vname option * itype) * iterm | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm }; (*see also signature*) fun is_IVar (IVar _) = true | is_IVar _ = false; fun is_IAbs (_ `|=> _) = true | is_IAbs _ = false; val op `$$ = Library.foldl (op `$); val op `|==> = Library.foldr (op `|=>); val unfold_app = unfoldl (fn op `$ t => SOME t | _ => NONE); val unfold_abs = unfoldr (fn op `|=> t => SOME t | _ => NONE); val split_let = (fn ICase { term = t, typ = ty, clauses = [(p, body)], ... } => SOME (((p, ty), t), body) | _ => NONE); val split_let_no_pat = (fn ICase { term = t, typ = ty, clauses = [(IVar v, body)], ... } => SOME (((v, ty), t), body) | _ => NONE); val unfold_let = unfoldr split_let; val unfold_let_no_pat = unfoldr split_let_no_pat; fun unfold_const_app t = case unfold_app t of (IConst c, ts) => SOME (c, ts) | _ => NONE; fun fold_constexprs f = let fun fold' (IConst c) = f c | fold' (IVar _) = I | fold' (t1 `$ t2) = fold' t1 #> fold' t2 | fold' (_ `|=> t) = fold' t | fold' (ICase { term = t, clauses = clauses, ... }) = fold' t #> fold (fn (p, body) => fold' p #> fold' body) clauses in fold' end; val add_constsyms = fold_constexprs (fn { sym, ... } => insert (op =) sym); fun add_tycos (tyco `%% tys) = insert (op =) tyco #> fold add_tycos tys | add_tycos (ITyVar _) = I; val add_tyconames = fold_constexprs (fn { typargs = tys, ... } => fold add_tycos tys); fun fold_varnames f = let fun fold_aux add_vars f = let fun fold_term _ (IConst _) = I | fold_term vs (IVar (SOME v)) = if member (op =) vs v then I else f v | fold_term _ (IVar NONE) = I | fold_term vs (t1 `$ t2) = fold_term vs t1 #> fold_term vs t2 | fold_term vs ((SOME v, _) `|=> t) = fold_term (insert (op =) v vs) t | fold_term vs ((NONE, _) `|=> t) = fold_term vs t | fold_term vs (ICase { term = t, clauses = clauses, ... }) = fold_term vs t #> fold (fold_clause vs) clauses and fold_clause vs (p, t) = fold_term (add_vars p vs) t; in fold_term [] end fun add_vars t = fold_aux add_vars (insert (op =)) t; in fold_aux add_vars f end; fun exists_var t v = fold_varnames (fn w => fn b => v = w orelse b) t false; fun split_pat_abs ((NONE, ty) `|=> t) = SOME ((IVar NONE, ty), t) | split_pat_abs ((SOME v, ty) `|=> t) = SOME (case t of ICase { term = IVar (SOME w), clauses = [(p, body)], ... } => if v = w andalso (exists_var p v orelse not (exists_var body v)) then ((p, ty), body) else ((IVar (SOME v), ty), t) | _ => ((IVar (SOME v), ty), t)) | split_pat_abs _ = NONE; val unfold_pat_abs = unfoldr split_pat_abs; fun unfold_abs_eta [] t = ([], t) | unfold_abs_eta (_ :: tys) (v_ty `|=> t) = let val (vs_tys, t') = unfold_abs_eta tys t; in (v_ty :: vs_tys, t') end | unfold_abs_eta tys t = let val ctxt = fold_varnames Name.declare t Name.context; val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys); in (vs_tys, t `$$ map (IVar o fst) vs_tys) end; fun eta_expand k (const as { dom = tys, ... }, ts) = let val j = length ts; val l = k - j; val _ = if l > length tys then error "Impossible eta-expansion" else (); val vars = (fold o fold_varnames) Name.declare ts Name.context; val vs_tys = (map o apfst) SOME (Name.invent_names vars "a" ((take l o drop j) tys)); in vs_tys `|==> IConst const `$$ ts @ map (IVar o fst) vs_tys end; fun map_terms_bottom_up f (t as IConst _) = f t | map_terms_bottom_up f (t as IVar _) = f t | map_terms_bottom_up f (t1 `$ t2) = f (map_terms_bottom_up f t1 `$ map_terms_bottom_up f t2) | map_terms_bottom_up f ((v, ty) `|=> t) = f ((v, ty) `|=> map_terms_bottom_up f t) | map_terms_bottom_up f (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) = f (ICase { term = map_terms_bottom_up f t, typ = ty, clauses = (map o apply2) (map_terms_bottom_up f) clauses, primitive = map_terms_bottom_up f t0 }); fun adjungate_clause ctxt vs_map ts (body as IConst { sym = Constant c, ... }) = if Code.is_undefined (Proof_Context.theory_of ctxt) c then [] else [(ts, body)] | adjungate_clause ctxt vs_map ts (body as ICase { term = IVar (SOME v), clauses = clauses, ... }) = let - val vs = (fold o fold_varnames) (insert (op =)) ts []; + val vs = build ((fold o fold_varnames) (insert (op =)) ts); fun varnames_disjunctive pat = - null (inter (op =) vs (fold_varnames (insert (op =)) pat [])); + null (inter (op =) vs (build (fold_varnames (insert (op =)) pat))); fun purge_unused_vars_in t = let - val vs = fold_varnames (insert (op =)) t []; + val vs = build (fold_varnames (insert (op =)) t); in map_terms_bottom_up (fn IVar (SOME v) => IVar (if member (op =) vs v then SOME v else NONE) | t => t) end; in if forall (fn (pat', body') => exists_var pat' v orelse not (exists_var body' v)) clauses andalso forall (varnames_disjunctive o fst) clauses then case AList.lookup (op =) vs_map v of SOME i => clauses |> maps (fn (pat', body') => adjungate_clause ctxt (AList.delete (op =) v vs_map) (nth_map i (K pat') ts |> map (purge_unused_vars_in body')) body') | NONE => [(ts, body)] else [(ts, body)] end | adjungate_clause ctxt vs_map ts body = [(ts, body)]; fun exists_dict_var f (Dict (_, d)) = exists_plain_dict_var_pred f d and exists_plain_dict_var_pred f (Dict_Const (_, dss)) = exists_dictss_var f dss | exists_plain_dict_var_pred f (Dict_Var x) = f x and exists_dictss_var f dss = (exists o exists) (exists_dict_var f) dss; fun contains_dict_var (IConst { dicts = dss, ... }) = exists_dictss_var (K true) dss | contains_dict_var (IVar _) = false | contains_dict_var (t1 `$ t2) = contains_dict_var t1 orelse contains_dict_var t2 | contains_dict_var (_ `|=> t) = contains_dict_var t | contains_dict_var (ICase { primitive = t, ... }) = contains_dict_var t; val unambiguous_dictss = not o exists_dictss_var (fn { unique, ... } => not unique); (** statements, abstract programs **) type typscheme = (vname * sort) list * itype; datatype stmt = NoStmt | Fun of (typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option | Datatype of vname list * ((string * vname list) * itype list) list | Datatypecons of string | Class of vname * ((class * class) list * (string * itype) list) | Classrel of class * class | Classparam of class | Classinst of { class: string, tyco: string, vs: (vname * sort) list, superinsts: (class * dict list list) list, inst_params: ((string * (const * int)) * (thm * bool)) list, superinst_params: ((string * (const * int)) * (thm * bool)) list }; type program = stmt Code_Symbol.Graph.T; -fun unimplemented program = - Code_Symbol.Graph.fold (fn (Constant c, (NoStmt, _)) => cons c | _ => I) program []; +val unimplemented = + build o Code_Symbol.Graph.fold (fn (Constant c, (NoStmt, _)) => cons c | _ => I); fun implemented_deps program = Code_Symbol.Graph.keys program |> subtract (op =) (Code_Symbol.Graph.all_preds program (map Constant (unimplemented program))) |> map_filter (fn Constant c => SOME c | _ => NONE); fun map_classparam_instances_as_term f = (map o apfst o apsnd o apfst) (fn const => case f (IConst const) of IConst const' => const') fun map_terms_stmt f NoStmt = NoStmt | map_terms_stmt f (Fun ((tysm, eqs), case_cong)) = Fun ((tysm, (map o apfst) (fn (ts, t) => (map f ts, f t)) eqs), case_cong) | map_terms_stmt f (stmt as Datatype _) = stmt | map_terms_stmt f (stmt as Datatypecons _) = stmt | map_terms_stmt f (stmt as Class _) = stmt | map_terms_stmt f (stmt as Classrel _) = stmt | map_terms_stmt f (stmt as Classparam _) = stmt | map_terms_stmt f (Classinst { class, tyco, vs, superinsts, inst_params, superinst_params }) = Classinst { class = class, tyco = tyco, vs = vs, superinsts = superinsts, inst_params = map_classparam_instances_as_term f inst_params, superinst_params = map_classparam_instances_as_term f superinst_params }; fun is_constr program sym = case Code_Symbol.Graph.get_node program sym of Datatypecons _ => true | _ => false; fun is_case (Fun (_, SOME _)) = true | is_case _ = false; fun linear_stmts program = rev (Code_Symbol.Graph.strong_conn program) |> map (AList.make (Code_Symbol.Graph.get_node program)); fun group_stmts ctxt program = let fun is_fun (_, Fun _) = true | is_fun _ = false; fun is_datatypecons (_, Datatypecons _) = true | is_datatypecons _ = false; fun is_datatype (_, Datatype _) = true | is_datatype _ = false; fun is_class (_, Class _) = true | is_class _ = false; fun is_classrel (_, Classrel _) = true | is_classrel _ = false; fun is_classparam (_, Classparam _) = true | is_classparam _ = false; fun is_classinst (_, Classinst _) = true | is_classinst _ = false; fun group stmts = if forall (is_datatypecons orf is_datatype) stmts then (filter is_datatype stmts, [], ([], [])) else if forall (is_class orf is_classrel orf is_classparam) stmts then ([], filter is_class stmts, ([], [])) else if forall (is_fun orf is_classinst) stmts then ([], [], List.partition is_fun stmts) else error ("Illegal mutual dependencies: " ^ (commas o map (Code_Symbol.quote ctxt o fst)) stmts); in linear_stmts program |> map group end; (** translation kernel **) (* generic mechanisms *) fun ensure_stmt symbolize generate x (deps, program) = let val sym = symbolize x; val add_dep = case deps of [] => I | dep :: _ => Code_Symbol.Graph.add_edge (dep, sym); in if can (Code_Symbol.Graph.get_node program) sym then program |> add_dep |> pair deps |> pair x else program |> Code_Symbol.Graph.default_node (sym, NoStmt) |> add_dep |> curry generate (sym :: deps) ||> snd |-> (fn stmt => (Code_Symbol.Graph.map_node sym) (K stmt)) |> pair deps |> pair x end; exception PERMISSIVE of unit; fun translation_error ctxt permissive some_thm deps msg sub_msg = if permissive then raise PERMISSIVE () else let val thm_msg = Option.map (fn thm => "in code equation " ^ Thm.string_of_thm ctxt thm) some_thm; val dep_msg = if null (tl deps) then NONE else SOME ("with dependency " ^ space_implode " -> " (map (Code_Symbol.quote ctxt) (rev deps))); val thm_dep_msg = case (thm_msg, dep_msg) of (SOME thm_msg, SOME dep_msg) => "\n(" ^ thm_msg ^ ",\n" ^ dep_msg ^ ")" | (SOME thm_msg, NONE) => "\n(" ^ thm_msg ^ ")" | (NONE, SOME dep_msg) => "\n(" ^ dep_msg ^ ")" | (NONE, NONE) => "" in error (msg ^ thm_dep_msg ^ ":\n" ^ sub_msg) end; fun maybe_permissive f prgrm = f prgrm |>> SOME handle PERMISSIVE () => (NONE, prgrm); fun not_wellsorted ctxt permissive some_thm deps ty sort e = let val err_class = Sorts.class_error (Context.Proof ctxt) e; val err_typ = "Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^ Syntax.string_of_sort ctxt sort; in translation_error ctxt permissive some_thm deps "Wellsortedness error" (err_typ ^ "\n" ^ err_class) end; (* inference of type annotations for disambiguation with type classes *) fun mk_tagged_type (true, T) = Type ("", [T]) | mk_tagged_type (false, T) = T; fun dest_tagged_type (Type ("", [T])) = (true, T) | dest_tagged_type T = (false, T); val untag_term = map_types (snd o dest_tagged_type); fun tag_term (proj_sort, _) eqngr = let val has_sort_constraints = exists (not o null) o map proj_sort o Code_Preproc.sortargs eqngr; fun tag (Const (_, T')) (Const (c, T)) = Const (c, mk_tagged_type (not (null (Term.add_tvarsT T' [])) andalso has_sort_constraints c, T)) | tag (t1 $ u1) (t $ u) = tag t1 t $ tag u1 u | tag (Abs (_, _, t1)) (Abs (x, T, t)) = Abs (x, T, tag t1 t) | tag (Free _) (t as Free _) = t | tag (Var _) (t as Var _) = t | tag (Bound _) (t as Bound _) = t; in tag end fun annotate ctxt algbr eqngr (c, ty) args rhs = let val erase = map_types (fn _ => Type_Infer.anyT []); val reinfer = singleton (Type_Infer_Context.infer_types ctxt); val lhs = list_comb (Const (c, ty), map (map_types Type.strip_sorts o fst) args); val reinferred_rhs = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase rhs)))); in tag_term algbr eqngr reinferred_rhs rhs end fun annotate_eqns ctxt algbr eqngr (c, ty) eqns = let val ctxt' = ctxt |> Proof_Context.theory_of |> Proof_Context.init_global |> Config.put Type_Infer_Context.const_sorts false; (*avoid spurious fixed variables: there is no eigen context for equations*) in map (apfst (fn (args, (rhs, some_abs)) => (args, (annotate ctxt' algbr eqngr (c, ty) args rhs, some_abs)))) eqns end; (* preprocessing pattern schemas *) fun preprocess_pattern_schema ctxt (t_pos, case_pats) (c_ty, ts) = let val thy = Proof_Context.theory_of ctxt; val ty = nth (binder_types (snd c_ty)) t_pos; fun select_clauses xs = xs |> nth_drop t_pos |> curry (op ~~) case_pats |> map_filter (fn (NONE, _) => NONE | (SOME _, x) => SOME x); fun mk_constr c t = let val n = Code.args_number thy c; in ((c, (take n o binder_types o fastype_of o untag_term) t ---> ty), n) end; val constrs = if null case_pats then [] else map2 mk_constr (case_pats |> map_filter I) (select_clauses ts); val split_clauses = if null case_pats then (fn ts => (nth ts t_pos, nth_drop t_pos ts)) else (fn ts => (nth ts t_pos, select_clauses ts)); in (ty, constrs, split_clauses) end; (* abstract dictionary construction *) datatype typarg_witness = Weakening of (class * class) list * plain_typarg_witness and plain_typarg_witness = Global of (string * class) * typarg_witness list list | Local of { var: string, index: int, sort: sort, unique: bool }; fun brand_unique unique (w as Global _) = w | brand_unique unique (Local { var, index, sort, unique = _ }) = Local { var = var, index = index, sort = sort, unique = unique }; fun construct_dictionaries ctxt (proj_sort, algebra) permissive some_thm (ty, sort) (deps, program) = let fun class_relation unique (Weakening (classrels, x), sub_class) super_class = Weakening ((sub_class, super_class) :: classrels, brand_unique unique x); fun type_constructor (tyco, _) dss class = Weakening ([], Global ((tyco, class), (map o map) fst dss)); fun type_variable (TFree (v, sort)) = let val sort' = proj_sort sort; in map_index (fn (n, class) => (Weakening ([], Local { var = v, index = n, sort = sort', unique = true }), class)) sort' end; val typarg_witnesses = Sorts.of_sort_derivation algebra {class_relation = fn _ => fn unique => Sorts.classrel_derivation algebra (class_relation unique), type_constructor = type_constructor, type_variable = type_variable} (ty, proj_sort sort) handle Sorts.CLASS_ERROR e => not_wellsorted ctxt permissive some_thm deps ty sort e; in (typarg_witnesses, (deps, program)) end; (* translation *) fun ensure_tyco ctxt algbr eqngr permissive tyco = let val thy = Proof_Context.theory_of ctxt; val ((vs, cos), _) = Code.get_type thy tyco; val stmt_datatype = fold_map (translate_tyvar_sort ctxt algbr eqngr permissive) vs #>> map fst ##>> fold_map (fn (c, (vs, tys)) => ensure_const ctxt algbr eqngr permissive c ##>> pair (map (unprefix "'" o fst) vs) ##>> fold_map (translate_typ ctxt algbr eqngr permissive) tys) cos #>> Datatype; in ensure_stmt Type_Constructor stmt_datatype tyco end and ensure_const ctxt algbr eqngr permissive c = let val thy = Proof_Context.theory_of ctxt; fun stmt_datatypecons tyco = ensure_tyco ctxt algbr eqngr permissive tyco #>> Datatypecons; fun stmt_classparam class = ensure_class ctxt algbr eqngr permissive class #>> Classparam; fun stmt_fun cert = case Code.equations_of_cert thy cert of (_, NONE) => pair NoStmt | ((vs, ty), SOME eqns) => let val eqns' = annotate_eqns ctxt algbr eqngr (c, ty) eqns val some_case_cong = Code.get_case_cong thy c; in fold_map (translate_tyvar_sort ctxt algbr eqngr permissive) vs ##>> translate_typ ctxt algbr eqngr permissive ty ##>> translate_eqns ctxt algbr eqngr permissive eqns' #>> (fn (_, NONE) => NoStmt | (tyscm, SOME eqns) => Fun ((tyscm, eqns), some_case_cong)) end; val stmt_const = case Code.get_type_of_constr_or_abstr thy c of SOME (tyco, _) => stmt_datatypecons tyco | NONE => (case Axclass.class_of_param thy c of SOME class => stmt_classparam class | NONE => stmt_fun (Code_Preproc.cert eqngr c)) in ensure_stmt Constant stmt_const c end and ensure_class ctxt (algbr as (_, algebra)) eqngr permissive class = let val thy = Proof_Context.theory_of ctxt; val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class; val cs = #params (Axclass.get_info thy class); val stmt_class = fold_map (fn super_class => ensure_classrel ctxt algbr eqngr permissive (class, super_class)) super_classes ##>> fold_map (fn (c, ty) => ensure_const ctxt algbr eqngr permissive c ##>> translate_typ ctxt algbr eqngr permissive ty) cs #>> (fn info => Class (unprefix "'" Name.aT, info)) in ensure_stmt Type_Class stmt_class class end and ensure_classrel ctxt algbr eqngr permissive (sub_class, super_class) = let val stmt_classrel = ensure_class ctxt algbr eqngr permissive sub_class ##>> ensure_class ctxt algbr eqngr permissive super_class #>> Classrel; in ensure_stmt Class_Relation stmt_classrel (sub_class, super_class) end and ensure_inst ctxt (algbr as (_, algebra)) eqngr permissive (tyco, class) = let val thy = Proof_Context.theory_of ctxt; val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class; val these_class_params = these o try (#params o Axclass.get_info thy); val class_params = these_class_params class; val superclass_params = maps these_class_params ((Sorts.complete_sort algebra o Sorts.super_classes algebra) class); val vs = Name.invent_names Name.context "'a" (Sorts.mg_domain algebra tyco [class]); val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class]; val vs' = map2 (fn (v, sort1) => fn sort2 => (v, Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts'; val arity_typ = Type (tyco, map TFree vs); val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs'); fun translate_super_instance super_class = ensure_class ctxt algbr eqngr permissive super_class ##>> translate_dicts ctxt algbr eqngr permissive NONE (arity_typ, [super_class]) #>> (fn (super_class, [Dict ([], Dict_Const (_, dss))]) => (super_class, dss)); fun translate_classparam_instance (c, ty) = let val raw_const = Const (c, map_type_tfree (K arity_typ') ty); val dom_length = length (fst (strip_type ty)) val thm = Axclass.unoverload_conv ctxt (Thm.cterm_of ctxt raw_const); val const = (apsnd Logic.unvarifyT_global o dest_Const o snd o Logic.dest_equals o Thm.prop_of) thm; in ensure_const ctxt algbr eqngr permissive c ##>> translate_const ctxt algbr eqngr permissive (SOME thm) (const, NONE) #>> (fn (c, IConst const') => ((c, (const', dom_length)), (thm, true))) end; val stmt_inst = ensure_class ctxt algbr eqngr permissive class ##>> ensure_tyco ctxt algbr eqngr permissive tyco ##>> fold_map (translate_tyvar_sort ctxt algbr eqngr permissive) vs ##>> fold_map translate_super_instance super_classes ##>> fold_map translate_classparam_instance class_params ##>> fold_map translate_classparam_instance superclass_params #>> (fn (((((class, tyco), vs), superinsts), inst_params), superinst_params) => Classinst { class = class, tyco = tyco, vs = vs, superinsts = superinsts, inst_params = inst_params, superinst_params = superinst_params }); in ensure_stmt Class_Instance stmt_inst (tyco, class) end and translate_typ ctxt algbr eqngr permissive (TFree (v, _)) = pair (ITyVar (unprefix "'" v)) | translate_typ ctxt algbr eqngr permissive (Type (tyco, tys)) = ensure_tyco ctxt algbr eqngr permissive tyco ##>> fold_map (translate_typ ctxt algbr eqngr permissive) tys #>> (fn (tyco, tys) => tyco `%% tys) and translate_term ctxt algbr eqngr permissive some_thm (Const (c, ty), some_abs) = translate_app ctxt algbr eqngr permissive some_thm (((c, ty), []), some_abs) | translate_term ctxt algbr eqngr permissive some_thm (Free (v, _), some_abs) = pair (IVar (SOME v)) | translate_term ctxt algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) = let val ((v', _), t') = Term.dest_abs_global (Abs (Name.desymbolize (SOME false) v, ty, t)); val v'' = if Term.used_free v' t' then SOME v' else NONE in translate_typ ctxt algbr eqngr permissive ty ##>> translate_term ctxt algbr eqngr permissive some_thm (t', some_abs) #>> (fn (ty, t) => (v'', ty) `|=> t) end | translate_term ctxt algbr eqngr permissive some_thm (t as _ $ _, some_abs) = case strip_comb t of (Const (c, ty), ts) => translate_app ctxt algbr eqngr permissive some_thm (((c, ty), ts), some_abs) | (t', ts) => translate_term ctxt algbr eqngr permissive some_thm (t', some_abs) ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) ts #>> (fn (t, ts) => t `$$ ts) and translate_eqn ctxt algbr eqngr permissive ((args, (rhs, some_abs)), (some_thm, proper)) = fold_map (translate_term ctxt algbr eqngr permissive some_thm) args ##>> translate_term ctxt algbr eqngr permissive some_thm (rhs, some_abs) #>> rpair (some_thm, proper) and translate_eqns ctxt algbr eqngr permissive eqns = maybe_permissive (fold_map (translate_eqn ctxt algbr eqngr permissive) eqns) and translate_const ctxt algbr eqngr permissive some_thm ((c, ty), some_abs) (deps, program) = let val thy = Proof_Context.theory_of ctxt; val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs)) andalso Code.is_abstr thy c then translation_error ctxt permissive some_thm deps "Abstraction violation" ("constant " ^ Code.string_of_const thy c) else () in translate_const_proper ctxt algbr eqngr permissive some_thm (c, ty) (deps, program) end and translate_const_proper ctxt algbr eqngr permissive some_thm (c, ty) = let val thy = Proof_Context.theory_of ctxt; val (annotate, ty') = dest_tagged_type ty; val typargs = Sign.const_typargs thy (c, ty'); val sorts = Code_Preproc.sortargs eqngr c; val (dom, range) = Term.strip_type ty'; in ensure_const ctxt algbr eqngr permissive c ##>> fold_map (translate_typ ctxt algbr eqngr permissive) typargs ##>> fold_map (translate_dicts ctxt algbr eqngr permissive some_thm) (typargs ~~ sorts) ##>> fold_map (translate_typ ctxt algbr eqngr permissive) (ty' :: dom) #>> (fn (((c, typargs), dss), annotation :: dom) => IConst { sym = Constant c, typargs = typargs, dicts = dss, dom = dom, annotation = if annotate then SOME annotation else NONE }) end and translate_app_const ctxt algbr eqngr permissive some_thm ((c_ty, ts), some_abs) = translate_const ctxt algbr eqngr permissive some_thm (c_ty, some_abs) ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) ts #>> (fn (t, ts) => t `$$ ts) and translate_case ctxt algbr eqngr permissive some_thm (t_pos, case_pats) (c_ty, ts) = let val (ty, constrs, split_clauses) = preprocess_pattern_schema ctxt (t_pos, case_pats) (c_ty, ts); fun distill_clause tys t = let val (vs, body) = unfold_abs_eta tys t; val vs_map = - fold_index (fn (i, (SOME v, _)) => cons (v, i) | _ => I) vs []; + build (fold_index (fn (i, (SOME v, _)) => cons (v, i) | _ => I) vs); val ts = map (IVar o fst) vs; in adjungate_clause ctxt vs_map ts body end; fun mk_clauses [] ty (t, ts_clause) = (t, map (fn ([t], body) => (t, body)) (distill_clause [ty] (the_single ts_clause))) | mk_clauses constrs ty (t, ts_clause) = (t, maps (fn ((constr as IConst { dom = tys, ... }, n), t) => map (fn (ts, body) => (constr `$$ ts, body)) (distill_clause (take n tys) t)) (constrs ~~ ts_clause)); in translate_const ctxt algbr eqngr permissive some_thm (c_ty, NONE) ##>> fold_map (fn (constr, n) => translate_const ctxt algbr eqngr permissive some_thm (constr, NONE) #>> rpair n) constrs ##>> translate_typ ctxt algbr eqngr permissive ty ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) ts #>> (fn (((t_app, constrs), ty), ts) => case mk_clauses constrs ty (split_clauses ts) of (t, clauses) => ICase { term = t, typ = ty, clauses = clauses, primitive = t_app `$$ ts }) end and translate_app_case ctxt algbr eqngr permissive some_thm (num_args, pattern_schema) ((c, ty), ts) = if length ts < num_args then let val k = length ts; val tys = (take (num_args - k) o drop k o fst o strip_type) ty; val names = Name.build_context (ts |> (fold o fold_aterms) Term.declare_term_frees); val vs = Name.invent_names names "a" tys; in fold_map (translate_typ ctxt algbr eqngr permissive) tys ##>> translate_case ctxt algbr eqngr permissive some_thm pattern_schema ((c, ty), ts @ map Free vs) #>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t) end else if length ts > num_args then translate_case ctxt algbr eqngr permissive some_thm pattern_schema ((c, ty), take num_args ts) ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) (drop num_args ts) #>> (fn (t, ts) => t `$$ ts) else translate_case ctxt algbr eqngr permissive some_thm pattern_schema ((c, ty), ts) and translate_app ctxt algbr eqngr permissive some_thm (c_ty_ts as ((c, _), _), some_abs) = case Code.get_case_schema (Proof_Context.theory_of ctxt) c of SOME case_schema => translate_app_case ctxt algbr eqngr permissive some_thm case_schema c_ty_ts | NONE => translate_app_const ctxt algbr eqngr permissive some_thm (c_ty_ts, some_abs) and translate_tyvar_sort ctxt (algbr as (proj_sort, _)) eqngr permissive (v, sort) = fold_map (ensure_class ctxt algbr eqngr permissive) (proj_sort sort) #>> (fn sort => (unprefix "'" v, sort)) and translate_dicts ctxt algbr eqngr permissive some_thm (ty, sort) = let fun mk_dict (Weakening (classrels, d)) = fold_map (ensure_classrel ctxt algbr eqngr permissive) classrels ##>> mk_plain_dict d #>> Dict and mk_plain_dict (Global (inst, dss)) = ensure_inst ctxt algbr eqngr permissive inst ##>> (fold_map o fold_map) mk_dict dss #>> Dict_Const | mk_plain_dict (Local { var, index, sort, unique }) = ensure_class ctxt algbr eqngr permissive (nth sort index) #>> (fn class => Dict_Var { var = unprefix "'" var, index = index, length = length sort, class = class, unique = unique }) in construct_dictionaries ctxt algbr permissive some_thm (ty, sort) #-> (fn typarg_witnesses => fold_map mk_dict typarg_witnesses) end; (* store *) structure Program = Code_Data ( type T = program; val empty = Code_Symbol.Graph.empty; ); fun invoke_generation ignore_cache ctxt generate thing = Program.change_yield (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt)) (fn program => ([], program) |> generate thing |-> (fn thing => fn (_, program) => (thing, program))); (* program generation *) fun check_abstract_constructors thy consts = case filter (Code.is_abstr thy) consts of [] => () | abstrs => error ("Cannot export abstract constructor(s): " ^ commas (map (Code.string_of_const thy) abstrs)); fun invoke_generation_for_consts ctxt { ignore_cache, permissive } { algebra, eqngr } consts = let val thy = Proof_Context.theory_of ctxt; val _ = if permissive then () else check_abstract_constructors thy consts; in Code_Preproc.timed "translating program" #ctxt (fn { ctxt, algebra, eqngr, consts } => invoke_generation ignore_cache ctxt (fold_map (ensure_const ctxt algebra eqngr permissive)) consts) { ctxt = ctxt, algebra = algebra, eqngr = eqngr, consts = consts } end; fun invoke_generation_for_consts' ctxt ignore_cache_and_permissive consts = invoke_generation_for_consts ctxt { ignore_cache = ignore_cache_and_permissive, permissive = ignore_cache_and_permissive } (Code_Preproc.obtain ignore_cache_and_permissive { ctxt = ctxt, consts = consts, terms = []}) consts |> snd; fun invoke_generation_for_consts'' ctxt algebra_eqngr = invoke_generation_for_consts ctxt { ignore_cache = true, permissive = false } algebra_eqngr #> (fn (deps, program) => { deps = deps, program = program }); fun consts_program_permissive ctxt = invoke_generation_for_consts' ctxt true; fun consts_program ctxt consts = let fun project program = Code_Symbol.Graph.restrict (member (op =) (Code_Symbol.Graph.all_succs program (map Constant consts))) program; in invoke_generation_for_consts' ctxt false consts |> project end; (* value evaluation *) fun ensure_value ctxt algbr eqngr t = let val ty = fastype_of t; val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =) o dest_TFree))) t []; val t' = annotate ctxt algbr eqngr (\<^const_name>\Pure.dummy_pattern\, ty) [] t; val dummy_constant = Constant \<^const_name>\Pure.dummy_pattern\; val stmt_value = fold_map (translate_tyvar_sort ctxt algbr eqngr false) vs ##>> translate_typ ctxt algbr eqngr false ty ##>> translate_term ctxt algbr eqngr false NONE (t', NONE) #>> (fn ((vs, ty), t) => Fun (((vs, ty), [(([], t), (NONE, true))]), NONE)); fun term_value (_, program1) = let val Fun ((vs_ty, [(([], t), _)]), _) = Code_Symbol.Graph.get_node program1 dummy_constant; val deps' = Code_Symbol.Graph.immediate_succs program1 dummy_constant; val program2 = Code_Symbol.Graph.del_node dummy_constant program1; val deps_all = Code_Symbol.Graph.all_succs program2 deps'; val program3 = Code_Symbol.Graph.restrict (member (op =) deps_all) program2; in ((program3, ((vs_ty, t), deps')), (deps', program2)) end; in ensure_stmt Constant stmt_value \<^const_name>\Pure.dummy_pattern\ #> snd #> term_value end; fun dynamic_evaluation comp ctxt algebra eqngr t = let val ((program, (vs_ty_t', deps)), _) = Code_Preproc.timed "translating term" #ctxt (fn { ctxt, algebra, eqngr, t } => invoke_generation false ctxt (ensure_value ctxt algebra eqngr) t) { ctxt = ctxt, algebra = algebra, eqngr = eqngr, t = t }; in comp program t vs_ty_t' deps end; fun dynamic_conv ctxt conv = Code_Preproc.dynamic_conv ctxt (dynamic_evaluation (fn program => fn _ => conv program) ctxt); fun dynamic_value ctxt postproc comp = Code_Preproc.dynamic_value ctxt postproc (dynamic_evaluation comp ctxt); fun static_evaluation ctxt consts algebra_eqngr static_eval = static_eval (invoke_generation_for_consts'' ctxt algebra_eqngr consts); fun static_evaluation_thingol ctxt consts (algebra_eqngr as { algebra, eqngr }) static_eval = let fun evaluation program dynamic_eval ctxt t = let val ((_, ((vs_ty', t'), deps)), _) = Code_Preproc.timed "translating term" #ctxt (fn { ctxt, t } => ensure_value ctxt algebra eqngr t ([], program)) { ctxt = ctxt, t = t }; in dynamic_eval ctxt t (vs_ty', t') deps end; in static_evaluation ctxt consts algebra_eqngr (fn program_deps => evaluation (#program program_deps) (static_eval program_deps)) end; fun static_evaluation_isa ctxt consts algebra_eqngr static_eval = static_evaluation ctxt consts algebra_eqngr (fn program_deps => (static_eval (#program program_deps))); fun static_conv_thingol (ctxt_consts as { ctxt, consts }) conv = Code_Preproc.static_conv ctxt_consts (fn algebra_eqngr => static_evaluation_thingol ctxt consts algebra_eqngr (fn program_deps => let val static_conv = conv program_deps; in fn ctxt => fn _ => fn vs_ty => fn deps => static_conv ctxt vs_ty deps end)); fun static_conv_isa (ctxt_consts as { ctxt, consts }) conv = Code_Preproc.static_conv ctxt_consts (fn algebra_eqngr => static_evaluation_isa ctxt consts algebra_eqngr conv); fun static_value (ctxt_postproc_consts as { ctxt, consts, ... }) comp = Code_Preproc.static_value ctxt_postproc_consts (fn algebra_eqngr => static_evaluation_thingol ctxt consts algebra_eqngr comp); (** constant expressions **) fun read_const_exprs_internal ctxt = let val thy = Proof_Context.theory_of ctxt; fun this_theory name = if Context.theory_name thy = name then thy else Context.get_theory {long = false} thy name; fun consts_of thy' = fold (fn (c, (_, NONE)) => cons c | _ => I) (#constants (Consts.dest (Sign.consts_of thy'))) [] |> filter_out (Code.is_abstr thy); fun belongs_here thy' c = forall (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy'); fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy'); fun read_const_expr str = (case Syntax.parse_input ctxt (K NONE) (K Markup.empty) (SOME o Symbol_Pos.implode o #1) str of SOME "_" => ([], consts_of thy) | SOME s => (case try (unsuffix "._") s of SOME name => ([], consts_of_select (this_theory name)) | NONE => ([Code.read_const thy str], [])) | NONE => ([Code.read_const thy str], [])); in apply2 flat o split_list o map read_const_expr end; fun read_const_exprs_all ctxt = op @ o read_const_exprs_internal ctxt; fun read_const_exprs ctxt const_exprs = let val (consts, consts_permissive) = read_const_exprs_internal ctxt const_exprs; val consts' = consts_program_permissive ctxt consts_permissive |> implemented_deps |> filter_out (Code.is_abstr (Proof_Context.theory_of ctxt)); in union (op =) consts' consts end; (** diagnostic commands **) fun code_depgr ctxt consts = let val { eqngr, ... } = Code_Preproc.obtain true { ctxt = ctxt, consts = consts, terms = [] }; val all_consts = Graph.all_succs eqngr consts; in Graph.restrict (member (op =) all_consts) eqngr end; fun code_thms ctxt = Pretty.writeln o Code_Preproc.pretty ctxt o code_depgr ctxt; fun coalesce_strong_conn gr = let val xss = Graph.strong_conn gr; val xss_ys = map (fn xs => (xs, commas xs)) xss; val y_for = the o AList.lookup (op =) (maps (fn (xs, y) => map (fn x => (x, y)) xs) xss_ys); fun coalesced_succs_for xs = maps (Graph.immediate_succs gr) xs |> subtract (op =) xs |> map y_for |> distinct (op =); val succs = map (fn (xs, _) => (xs, coalesced_succs_for xs)) xss_ys; in map (fn (xs, y) => ((y, xs), (maps (Graph.get_node gr) xs, (the o AList.lookup (op =) succs) xs))) xss_ys end; fun code_deps ctxt consts = let val thy = Proof_Context.theory_of ctxt; fun mk_entry ((name, consts), (ps, deps)) = let val label = commas (map (Code.string_of_const thy) consts); in ((name, Graph_Display.content_node label (Pretty.str label :: ps)), deps) end; in code_depgr ctxt consts |> Graph.map (K (Code.pretty_cert thy o snd)) |> coalesce_strong_conn |> map mk_entry |> Graph_Display.display_graph end; local fun code_thms_cmd ctxt = code_thms ctxt o read_const_exprs_all ctxt; fun code_deps_cmd ctxt = code_deps ctxt o read_const_exprs_all ctxt; in val _ = Outer_Syntax.command \<^command_keyword>\code_thms\ "print system of code equations for code" (Scan.repeat1 Parse.term >> (fn cs => Toplevel.keep (fn st => code_thms_cmd (Toplevel.context_of st) cs))); val _ = Outer_Syntax.command \<^command_keyword>\code_deps\ "visualize dependencies of code equations for code" (Scan.repeat1 Parse.term >> (fn cs => Toplevel.keep (fn st => code_deps_cmd (Toplevel.context_of st) cs))); end; end; (*struct*) structure Basic_Code_Thingol: BASIC_CODE_THINGOL = Code_Thingol;