diff --git a/src/Tools/Code/code_ml.ML b/src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML +++ b/src/Tools/Code/code_ml.ML @@ -1,912 +1,912 @@ (* Title: Tools/Code/code_ml.ML Author: Florian Haftmann, TU Muenchen Serializer for SML and OCaml. *) signature CODE_ML = sig val target_SML: string val target_OCaml: string end; structure Code_ML : CODE_ML = struct open Basic_Code_Symbol; open Basic_Code_Thingol; open Code_Printer; infixr 5 @@; infixr 5 @|; (** generic **) val target_SML = "SML"; val target_OCaml = "OCaml"; datatype ml_binding = ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list) | ML_Instance of (string * class) * { class: class, tyco: string, vs: (vname * sort) list, - superinsts: (class * dict list list) list, + superinsts: (class * (itype * dict list) list) list, inst_params: ((string * (const * int)) * (thm * bool)) list, superinst_params: ((string * (const * int)) * (thm * bool)) list }; datatype ml_stmt = ML_Exc of string * (typscheme * int) | ML_Val of ml_binding | ML_Funs of (Code_Namespace.export * ml_binding) list * Code_Symbol.T list | ML_Datas of (string * (vname list * ((string * vname list) * itype list) list)) list | ML_Class of string * (vname * ((class * class) list * (string * itype) list)); fun print_product _ [] = NONE | print_product print [x] = SOME (print x) | print_product print xs = (SOME o enum " *" "" "") (map print xs); fun tuplify _ _ [] = NONE | tuplify print fxy [x] = SOME (print fxy x) | tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs)); (** SML serializer **) fun print_sml_char c = if c = "\\" then "\\092" (*produce strings suitable for both SML as well as Isabelle/ML*) else if Symbol.is_ascii c then ML_Syntax.print_symbol_char c else error "non-ASCII byte in SML string literal"; val print_sml_string = quote o translate_string print_sml_char; fun print_sml_stmt tyco_syntax const_syntax reserved is_constr deresolve = let val deresolve_const = deresolve o Constant; val deresolve_classrel = deresolve o Class_Relation; val deresolve_inst = deresolve o Class_Instance; fun print_tyco_expr (sym, []) = (str o deresolve) sym | print_tyco_expr (sym, [ty]) = concat [print_typ BR ty, (str o deresolve) sym] | print_tyco_expr (sym, tys) = concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym] and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco of NONE => print_tyco_expr (Type_Constructor tyco, tys) | SOME (_, print) => print print_typ fxy tys) | print_typ fxy (ITyVar v) = str ("'" ^ v); fun print_dicttyp (class, ty) = print_tyco_expr (Type_Class class, [ty]); fun print_typscheme_prefix (vs, p) = enum " ->" "" "" (map_filter (fn (v, sort) => (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p); fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty); fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty); fun print_classrels fxy [] ps = brackify fxy ps | print_classrels fxy [classrel] ps = brackify fxy [(str o deresolve_classrel) classrel, brackify BR ps] | print_classrels fxy classrels ps = brackify fxy [enum " o" "(" ")" (map (str o deresolve_classrel) classrels), brackify BR ps] fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) = print_classrels fxy classrels (print_plain_dict is_pseudo_fun fxy x) and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) = ((str o deresolve_inst) inst :: (if is_pseudo_fun (Class_Instance inst) then [str "()"] - else map_filter (print_dicts is_pseudo_fun BR) dss)) + else map_filter (print_dicts is_pseudo_fun BR o snd) dss)) | print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length, ... }) = [str (if length = 1 then Name.enforce_case true var ^ "_" else Name.enforce_case true var ^ string_of_int (index + 1) ^ "_")] and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun); val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR (map_index (fn (i, _) => Dict ([], Dict_Var { var = v, index = i, length = length sort, class = nth sort i, unique = true })) sort)); fun print_term is_pseudo_fun some_thm vars fxy (IConst const) = print_app is_pseudo_fun some_thm vars fxy (const, []) | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) = str "_" | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) = str (lookup_var vars v) | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) = (case Code_Thingol.unfold_const_app t of SOME app => print_app is_pseudo_fun some_thm vars fxy app | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1, print_term is_pseudo_fun some_thm vars BR t2]) | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) = let val (binds, t') = Code_Thingol.unfold_pat_abs t; fun print_abs (pat, ty) = print_bind is_pseudo_fun some_thm NOBR pat #>> (fn p => concat [str "fn", p, str "=>"]); val (ps, vars') = fold_map print_abs binds vars; in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end | print_term is_pseudo_fun 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 is_pseudo_fun some_thm vars fxy case_expr else print_app is_pseudo_fun some_thm vars fxy app | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr) and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts, dom, ... }, ts)) = if is_constr sym then let val wanted = length dom in if wanted < 2 orelse length ts = wanted then (str o deresolve) sym :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts) else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.saturated_application wanted app)] end else if is_pseudo_fun sym then (str o deresolve) sym @@ str "()" else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts @ map (print_term is_pseudo_fun some_thm vars BR) ts and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun) (print_term is_pseudo_fun) const_syntax some_thm vars and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun) and print_case is_pseudo_fun some_thm vars fxy { clauses = [], ... } = (concat o map str) ["raise", "Fail", "\"empty case\""] | print_case is_pseudo_fun some_thm vars fxy (case_expr as { clauses = [_], ... }) = let val (binds, body) = Code_Thingol.unfold_let (ICase case_expr); fun print_match ((pat, _), t) vars = vars |> print_bind is_pseudo_fun some_thm NOBR pat |>> (fn p => semicolon [str "val", p, str "=", print_term is_pseudo_fun some_thm vars NOBR t]) val (ps, vars') = fold_map print_match binds vars; in Pretty.chunks [ Pretty.block [str "let", Pretty.fbrk, Pretty.chunks ps], Pretty.block [str "in", Pretty.fbrk, print_term is_pseudo_fun some_thm vars' NOBR body], str "end" ] end | print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } = let fun print_select delim (pat, body) = let val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars; in concat [str delim, p, str "=>", print_term is_pseudo_fun some_thm vars' NOBR body] end; in brackets ( str "case" :: print_term is_pseudo_fun some_thm vars NOBR t :: print_select "of" clause :: map (print_select "|") clauses ) end; fun print_val_decl print_typscheme (sym, typscheme) = concat [str "val", str (deresolve sym), str ":", print_typscheme typscheme]; fun print_datatype_decl definer (tyco, (vs, cos)) = let fun print_co ((co, _), []) = str (deresolve_const co) | print_co ((co, _), tys) = concat [str (deresolve_const co), str "of", enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; in concat ( str definer :: print_tyco_expr (Type_Constructor tyco, map ITyVar vs) :: str "=" :: separate (str "|") (map print_co cos) ) end; fun print_def is_pseudo_fun needs_typ definer (ML_Function (const, (vs_ty as (vs, ty), eq :: eqs))) = let fun print_eqn definer ((ts, t), (some_thm, _)) = let val vars = reserved |> intro_base_names_for (is_none o const_syntax) deresolve (t :: ts) |> intro_vars (build (fold Code_Thingol.add_varnames ts)); val prolog = if needs_typ then concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty] else (concat o map str) [definer, deresolve_const const]; in concat ( prolog :: (if is_pseudo_fun (Constant const) then [str "()"] else print_dict_args vs @ map (print_term is_pseudo_fun some_thm vars BR) ts) @ str "=" @@ print_term is_pseudo_fun some_thm vars NOBR t ) end val shift = if null eqs then I else map (Pretty.block o single o Pretty.block o single); in pair (print_val_decl print_typscheme (Constant const, vs_ty)) ((Pretty.block o Pretty.fbreaks o shift) ( print_eqn definer eq :: map (print_eqn "|") eqs )) end | print_def is_pseudo_fun _ definer (ML_Instance (inst as (tyco, class), { vs, superinsts, inst_params, ... })) = let fun print_super_instance (super_class, x) = concat [ (str o Long_Name.base_name o deresolve_classrel) (class, super_class), str "=", print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), x))) ]; fun print_classparam_instance ((classparam, (const, _)), (thm, _)) = concat [ (str o Long_Name.base_name o deresolve_const) classparam, str "=", print_app (K false) (SOME thm) reserved NOBR (const, []) ]; in pair (print_val_decl print_dicttypscheme (Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs)))) (concat ( str definer :: (str o deresolve_inst) inst :: (if is_pseudo_fun (Class_Instance inst) then [str "()"] else print_dict_args vs) @ str "=" :: enum "," "{" "}" (map print_super_instance superinsts @ map print_classparam_instance inst_params) :: str ":" @@ print_dicttyp (class, tyco `%% map (ITyVar o fst) vs) )) end; fun print_stmt _ (ML_Exc (const, (vs_ty, n))) = pair [print_val_decl print_typscheme (Constant const, vs_ty)] ((semicolon o map str) ( (if n = 0 then "val" else "fun") :: deresolve_const const :: replicate n "_" @ "=" :: "raise" :: "Fail" @@ print_sml_string const )) | print_stmt _ (ML_Val binding) = let val (sig_p, p) = print_def (K false) true "val" binding in pair [sig_p] (semicolon [p]) end | print_stmt _ (ML_Funs ((export, binding) :: exports_bindings, pseudo_funs)) = let val print_def' = print_def (member (op =) pseudo_funs) false; fun print_pseudo_fun sym = concat [ str "val", (str o deresolve) sym, str "=", (str o deresolve) sym, str "();" ]; val (sig_ps, (ps, p)) = (apsnd split_last o split_list) (print_def' "fun" binding :: map (print_def' "and" o snd) exports_bindings); val pseudo_ps = map print_pseudo_fun pseudo_funs; in pair (map_filter (fn (export, p) => if Code_Namespace.not_private export then SOME p else NONE) ((export :: map fst exports_bindings) ~~ sig_ps)) (Pretty.chunks (ps @ semicolon [p] :: pseudo_ps)) end | print_stmt _ (ML_Datas [(tyco, (vs, []))]) = let val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs); in pair [concat [str "type", ty_p]] (semicolon [str "datatype", ty_p, str "=", str "EMPTY__"]) end | print_stmt export (ML_Datas (data :: datas)) = let val decl_ps = print_datatype_decl "datatype" data :: map (print_datatype_decl "and") datas; val (ps, p) = split_last decl_ps; in pair (if Code_Namespace.is_public export then decl_ps else map (fn (tyco, (vs, _)) => concat [str "type", print_tyco_expr (Type_Constructor tyco, map ITyVar vs)]) (data :: datas)) (Pretty.chunks (ps @| semicolon [p])) end | print_stmt export (ML_Class (class, (v, (classrels, classparams)))) = let fun print_field s p = concat [str s, str ":", p]; fun print_proj s p = semicolon (map str ["val", s, "=", "#" ^ s, ":"] @| p); fun print_super_class_decl (classrel as (_, super_class)) = print_val_decl print_dicttypscheme (Class_Relation classrel, ([(v, [class])], (super_class, ITyVar v))); fun print_super_class_field (classrel as (_, super_class)) = print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v)); fun print_super_class_proj (classrel as (_, super_class)) = print_proj (deresolve_classrel classrel) (print_dicttypscheme ([(v, [class])], (super_class, ITyVar v))); fun print_classparam_decl (classparam, ty) = print_val_decl print_typscheme (Constant classparam, ([(v, [class])], ty)); fun print_classparam_field (classparam, ty) = print_field (deresolve_const classparam) (print_typ NOBR ty); fun print_classparam_proj (classparam, ty) = print_proj (deresolve_const classparam) (print_typscheme ([(v, [class])], ty)); in pair (concat [str "type", print_dicttyp (class, ITyVar v)] :: (if Code_Namespace.is_public export then map print_super_class_decl classrels @ map print_classparam_decl classparams else [])) (Pretty.chunks ( concat [ str "type", print_dicttyp (class, ITyVar v), str "=", enum "," "{" "};" ( map print_super_class_field classrels @ map print_classparam_field classparams ) ] :: map print_super_class_proj classrels @ map print_classparam_proj classparams )) end; in print_stmt end; fun print_sml_module name decls body = Pretty.chunks2 ( Pretty.chunks [ str ("structure " ^ name ^ " : sig"), (indent 2 o Pretty.chunks) decls, str "end = struct" ] :: body @| str ("end; (*struct " ^ name ^ "*)") ); val literals_sml = Literals { literal_string = print_sml_string, literal_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)", literal_list = enum "," "[" "]", infix_cons = (7, "::") }; (** OCaml serializer **) val print_ocaml_string = let fun chr i = let val xs = string_of_int i; val ys = replicate_string (3 - length (raw_explode xs)) "0"; in "\\" ^ ys ^ xs end; fun char c = let val i = ord c; val s = if i >= 128 then error "non-ASCII byte in OCaml string literal" else if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126 then chr i else c in s end; in quote o translate_string char end; fun print_ocaml_stmt tyco_syntax const_syntax reserved is_constr deresolve = let val deresolve_const = deresolve o Constant; val deresolve_classrel = deresolve o Class_Relation; val deresolve_inst = deresolve o Class_Instance; fun print_tyco_expr (sym, []) = (str o deresolve) sym | print_tyco_expr (sym, [ty]) = concat [print_typ BR ty, (str o deresolve) sym] | print_tyco_expr (sym, tys) = concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym] and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco of NONE => print_tyco_expr (Type_Constructor tyco, tys) | SOME (_, print) => print print_typ fxy tys) | print_typ fxy (ITyVar v) = str ("'" ^ v); fun print_dicttyp (class, ty) = print_tyco_expr (Type_Class class, [ty]); fun print_typscheme_prefix (vs, p) = enum " ->" "" "" (map_filter (fn (v, sort) => (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p); fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty); fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty); val print_classrels = fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve_classrel) classrel]) fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) = print_plain_dict is_pseudo_fun fxy x |> print_classrels classrels and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) = brackify BR ((str o deresolve_inst) inst :: (if is_pseudo_fun (Class_Instance inst) then [str "()"] - else map_filter (print_dicts is_pseudo_fun BR) dss)) + else map_filter (print_dicts is_pseudo_fun BR o snd) dss)) | print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length, ... }) = str (if length = 1 then "_" ^ Name.enforce_case true var else "_" ^ Name.enforce_case true var ^ string_of_int (index + 1)) and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun); val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR (map_index (fn (i, _) => Dict ([], Dict_Var { var = v, index = i, length = length sort, class = nth sort i, unique = true })) sort)); fun print_term is_pseudo_fun some_thm vars fxy (IConst const) = print_app is_pseudo_fun some_thm vars fxy (const, []) | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) = str "_" | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) = str (lookup_var vars v) | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) = (case Code_Thingol.unfold_const_app t of SOME app => print_app is_pseudo_fun some_thm vars fxy app | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1, print_term is_pseudo_fun some_thm vars BR t2]) | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) = let val (binds, t') = Code_Thingol.unfold_pat_abs t; val (ps, vars') = fold_map (print_bind is_pseudo_fun some_thm BR o fst) binds vars; in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end | print_term is_pseudo_fun 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 is_pseudo_fun some_thm vars fxy case_expr else print_app is_pseudo_fun some_thm vars fxy app | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr) and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts, dom, ... }, ts)) = if is_constr sym then let val wanted = length dom in if length ts = wanted then (str o deresolve) sym :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts) else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.saturated_application wanted app)] end else if is_pseudo_fun sym then (str o deresolve) sym @@ str "()" else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts @ map (print_term is_pseudo_fun some_thm vars BR) ts and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun) (print_term is_pseudo_fun) const_syntax some_thm vars and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun) and print_case is_pseudo_fun some_thm vars fxy { clauses = [], ... } = (concat o map str) ["failwith", "\"empty case\""] | print_case is_pseudo_fun some_thm vars fxy (case_expr as { clauses = [_], ... }) = let val (binds, body) = Code_Thingol.unfold_let (ICase case_expr); fun print_let ((pat, _), t) vars = vars |> print_bind is_pseudo_fun some_thm NOBR pat |>> (fn p => concat [str "let", p, str "=", print_term is_pseudo_fun some_thm vars NOBR t, str "in"]) val (ps, vars') = fold_map print_let binds vars; in brackets [Pretty.chunks ps, print_term is_pseudo_fun some_thm vars' NOBR body] end | print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } = let fun print_select delim (pat, body) = let val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars; in concat [str delim, p, str "->", print_term is_pseudo_fun some_thm vars' NOBR body] end; in brackets ( str "match" :: print_term is_pseudo_fun some_thm vars NOBR t :: print_select "with" clause :: map (print_select "|") clauses ) end; fun print_val_decl print_typscheme (sym, typscheme) = concat [str "val", str (deresolve sym), str ":", print_typscheme typscheme]; fun print_datatype_decl definer (tyco, (vs, cos)) = let fun print_co ((co, _), []) = str (deresolve_const co) | print_co ((co, _), tys) = concat [str (deresolve_const co), str "of", enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; in concat ( str definer :: print_tyco_expr (Type_Constructor tyco, map ITyVar vs) :: str "=" :: separate (str "|") (map print_co cos) ) end; fun print_def is_pseudo_fun needs_typ definer (ML_Function (const, (vs_ty as (vs, ty), eqs))) = let fun print_eqn ((ts, t), (some_thm, _)) = let val vars = reserved |> intro_base_names_for (is_none o const_syntax) deresolve (t :: ts) |> intro_vars (build (fold Code_Thingol.add_varnames ts)); in concat [ (Pretty.block o commas) (map (print_term is_pseudo_fun some_thm vars NOBR) ts), str "->", print_term is_pseudo_fun some_thm vars NOBR t ] end; fun print_eqns is_pseudo [((ts, t), (some_thm, _))] = let val vars = reserved |> intro_base_names_for (is_none o const_syntax) deresolve (t :: ts) |> intro_vars (build (fold Code_Thingol.add_varnames ts)); in concat ( (if is_pseudo then [str "()"] else map (print_term is_pseudo_fun some_thm vars BR) ts) @ str "=" @@ print_term is_pseudo_fun some_thm vars NOBR t ) end | print_eqns _ ((eq as (([_], _), _)) :: eqs) = Pretty.block ( str "=" :: Pretty.brk 1 :: str "function" :: Pretty.brk 1 :: print_eqn eq :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1] o single o print_eqn) eqs ) | print_eqns _ (eqs as eq :: eqs') = let val vars = reserved |> intro_base_names_for (is_none o const_syntax) deresolve (map (snd o fst) eqs) val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs; in Pretty.block ( Pretty.breaks dummy_parms @ Pretty.brk 1 :: str "=" :: Pretty.brk 1 :: str "match" :: Pretty.brk 1 :: (Pretty.block o commas) dummy_parms :: Pretty.brk 1 :: str "with" :: Pretty.brk 1 :: print_eqn eq :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1] o single o print_eqn) eqs' ) end; val prolog = if needs_typ then concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty] else (concat o map str) [definer, deresolve_const const]; in pair (print_val_decl print_typscheme (Constant const, vs_ty)) (concat ( prolog :: print_dict_args vs @| print_eqns (is_pseudo_fun (Constant const)) eqs )) end | print_def is_pseudo_fun _ definer (ML_Instance (inst as (tyco, class), { vs, superinsts, inst_params, ... })) = let - fun print_super_instance (super_class, x) = + fun print_super_instance (super_class, dss) = concat [ (str o deresolve_classrel) (class, super_class), str "=", - print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), x))) + print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), dss))) ]; fun print_classparam_instance ((classparam, (const, _)), (thm, _)) = concat [ (str o deresolve_const) classparam, str "=", print_app (K false) (SOME thm) reserved NOBR (const, []) ]; in pair (print_val_decl print_dicttypscheme (Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs)))) (concat ( str definer :: (str o deresolve_inst) inst :: (if is_pseudo_fun (Class_Instance inst) then [str "()"] else print_dict_args vs) @ str "=" @@ brackets [ enum_default "()" ";" "{" "}" (map print_super_instance superinsts @ map print_classparam_instance inst_params), str ":", print_dicttyp (class, tyco `%% map (ITyVar o fst) vs) ] )) end; fun print_stmt _ (ML_Exc (const, (vs_ty, n))) = pair [print_val_decl print_typscheme (Constant const, vs_ty)] ((doublesemicolon o map str) ( "let" :: deresolve_const const :: replicate n "_" @ "=" :: "failwith" @@ print_ocaml_string const )) | print_stmt _ (ML_Val binding) = let val (sig_p, p) = print_def (K false) true "let" binding in pair [sig_p] (doublesemicolon [p]) end | print_stmt _ (ML_Funs ((export, binding) :: exports_bindings, pseudo_funs)) = let val print_def' = print_def (member (op =) pseudo_funs) false; fun print_pseudo_fun sym = concat [ str "let", (str o deresolve) sym, str "=", (str o deresolve) sym, str "();;" ]; val (sig_ps, (ps, p)) = (apsnd split_last o split_list) (print_def' "let rec" binding :: map (print_def' "and" o snd) exports_bindings); val pseudo_ps = map print_pseudo_fun pseudo_funs; in pair (map_filter (fn (export, p) => if Code_Namespace.not_private export then SOME p else NONE) ((export :: map fst exports_bindings) ~~ sig_ps)) (Pretty.chunks (ps @ doublesemicolon [p] :: pseudo_ps)) end | print_stmt _ (ML_Datas [(tyco, (vs, []))]) = let val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs); in pair [concat [str "type", ty_p]] (doublesemicolon [str "type", ty_p, str "=", str "EMPTY__"]) end | print_stmt export (ML_Datas (data :: datas)) = let val decl_ps = print_datatype_decl "type" data :: map (print_datatype_decl "and") datas; val (ps, p) = split_last decl_ps; in pair (if Code_Namespace.is_public export then decl_ps else map (fn (tyco, (vs, _)) => concat [str "type", print_tyco_expr (Type_Constructor tyco, map ITyVar vs)]) (data :: datas)) (Pretty.chunks (ps @| doublesemicolon [p])) end | print_stmt export (ML_Class (class, (v, (classrels, classparams)))) = let fun print_field s p = concat [str s, str ":", p]; fun print_super_class_field (classrel as (_, super_class)) = print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v)); fun print_classparam_decl (classparam, ty) = print_val_decl print_typscheme (Constant classparam, ([(v, [class])], ty)); fun print_classparam_field (classparam, ty) = print_field (deresolve_const classparam) (print_typ NOBR ty); val w = "_" ^ Name.enforce_case true v; fun print_classparam_proj (classparam, _) = (concat o map str) ["let", deresolve_const classparam, w, "=", w ^ "." ^ deresolve_const classparam ^ ";;"]; val type_decl_p = concat [ str "type", print_dicttyp (class, ITyVar v), str "=", enum_default "unit" ";" "{" "}" ( map print_super_class_field classrels @ map print_classparam_field classparams ) ]; in pair (if Code_Namespace.is_public export then type_decl_p :: map print_classparam_decl classparams else if null classrels andalso null classparams then [type_decl_p] (*work around weakness in export calculation*) else [concat [str "type", print_dicttyp (class, ITyVar v)]]) (Pretty.chunks ( doublesemicolon [type_decl_p] :: map print_classparam_proj classparams )) end; in print_stmt end; fun print_ocaml_module name decls body = Pretty.chunks2 ( Pretty.chunks [ str ("module " ^ name ^ " : sig"), (indent 2 o Pretty.chunks) decls, str "end = struct" ] :: body @| str ("end;; (*struct " ^ name ^ "*)") ); val literals_ocaml = let fun numeral_ocaml k = if k < 0 then "(Z.neg " ^ numeral_ocaml (~ k) ^ ")" else if k <= 1073741823 then "(Z.of_int " ^ string_of_int k ^ ")" else "(Z.of_string " ^ quote (string_of_int k) ^ ")" in Literals { literal_string = print_ocaml_string, literal_numeral = numeral_ocaml, literal_list = enum ";" "[" "]", infix_cons = (6, "::") } end; (** SML/OCaml generic part **) fun ml_program_of_program ctxt module_name reserved identifiers = let fun namify_const upper base (nsp_const, nsp_type) = let val (base', nsp_const') = Name.variant (Name.enforce_case upper base) nsp_const in (base', (nsp_const', nsp_type)) end; fun namify_type base (nsp_const, nsp_type) = let val (base', nsp_type') = Name.variant (Name.enforce_case false base) nsp_type in (base', (nsp_const, nsp_type')) end; fun namify_stmt (Code_Thingol.Fun _) = namify_const false | namify_stmt (Code_Thingol.Datatype _) = namify_type | namify_stmt (Code_Thingol.Datatypecons _) = namify_const true | namify_stmt (Code_Thingol.Class _) = namify_type | namify_stmt (Code_Thingol.Classrel _) = namify_const false | namify_stmt (Code_Thingol.Classparam _) = namify_const false | namify_stmt (Code_Thingol.Classinst _) = namify_const false; fun ml_binding_of_stmt (sym as Constant const, (export, Code_Thingol.Fun ((tysm as (vs, ty), raw_eqs), _))) = let val eqs = filter (snd o snd) raw_eqs; val (eqs', some_sym) = if null (filter_out (null o snd) vs) then case eqs of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE) else (eqs, SOME (sym, member (op =) (Code_Thingol.add_constsyms t []) sym)) | _ => (eqs, NONE) else (eqs, NONE) in ((export, ML_Function (const, (tysm, eqs'))), some_sym) end | ml_binding_of_stmt (sym as Class_Instance inst, (export, Code_Thingol.Classinst (stmt as { vs, ... }))) = ((export, ML_Instance (inst, stmt)), if forall (null o snd) vs then SOME (sym, false) else NONE) | ml_binding_of_stmt (sym, _) = error ("Binding block containing illegal statement: " ^ Code_Symbol.quote ctxt sym) fun modify_fun (sym, (export, stmt)) = let val ((export', binding), some_value_sym) = ml_binding_of_stmt (sym, (export, stmt)); val ml_stmt = case binding of ML_Function (const, ((vs, ty), [])) => ML_Exc (const, ((vs, ty), (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty)) | _ => case some_value_sym of NONE => ML_Funs ([(export', binding)], []) | SOME (sym, true) => ML_Funs ([(export, binding)], [sym]) | SOME (sym, false) => ML_Val binding in SOME (export, ml_stmt) end; fun modify_funs stmts = single (SOME (Code_Namespace.Opaque, ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst))) fun modify_datatypes stmts = let val datas = map_filter (fn (Type_Constructor tyco, (export, Code_Thingol.Datatype stmt)) => SOME (export, (tyco, stmt)) | _ => NONE) stmts in if null datas then [] (*for abstract types wrt. code_reflect*) else datas |> split_list |> apfst Code_Namespace.join_exports |> apsnd ML_Datas |> SOME |> single end; fun modify_class stmts = the_single (map_filter (fn (Type_Class class, (export, Code_Thingol.Class stmt)) => SOME (export, (class, stmt)) | _ => NONE) stmts) |> apsnd ML_Class |> SOME |> single; fun modify_stmts ([stmt as (_, (_, stmt' as Code_Thingol.Fun _))]) = if Code_Thingol.is_case stmt' then [] else [modify_fun stmt] | modify_stmts ((stmts as (_, (_, Code_Thingol.Fun _)) :: _)) = modify_funs (filter_out (Code_Thingol.is_case o snd o snd) stmts) | modify_stmts ((stmts as (_, (_, Code_Thingol.Datatypecons _)) :: _)) = modify_datatypes stmts | modify_stmts ((stmts as (_, (_, Code_Thingol.Datatype _)) :: _)) = modify_datatypes stmts | modify_stmts ((stmts as (_, (_, Code_Thingol.Class _)) :: _)) = modify_class stmts | modify_stmts ((stmts as (_, (_, Code_Thingol.Classrel _)) :: _)) = modify_class stmts | modify_stmts ((stmts as (_, (_, Code_Thingol.Classparam _)) :: _)) = modify_class stmts | modify_stmts ([stmt as (_, (_, Code_Thingol.Classinst _))]) = [modify_fun stmt] | modify_stmts ((stmts as (_, (_, Code_Thingol.Classinst _)) :: _)) = modify_funs stmts | modify_stmts stmts = error ("Illegal mutual dependencies: " ^ (Library.commas o map (Code_Symbol.quote ctxt o fst)) stmts); in Code_Namespace.hierarchical_program ctxt { module_name = module_name, reserved = reserved, identifiers = identifiers, empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt, cyclic_modules = false, class_transitive = true, class_relation_public = true, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } end; fun serialize_ml print_ml_module print_ml_stmt ml_extension ctxt { module_name, reserved_syms, identifiers, includes, class_syntax, tyco_syntax, const_syntax } program exports = let (* build program *) val { deresolver, hierarchical_program = ml_program } = ml_program_of_program ctxt module_name (Name.make_context reserved_syms) identifiers exports program; (* print statements *) fun print_stmt prefix_fragments (_, (export, stmt)) = print_ml_stmt tyco_syntax const_syntax (make_vars reserved_syms) (Code_Thingol.is_constr program) (deresolver prefix_fragments) export stmt |> apfst (fn decl => if Code_Namespace.not_private export then SOME decl else NONE); (* print modules *) fun print_module _ base _ xs = let val (raw_decls, body) = split_list xs; val decls = maps these raw_decls in (NONE, print_ml_module base decls body) end; (* serialization *) val p = Pretty.chunks2 (map snd includes @ map snd (Code_Namespace.print_hierarchical { print_module = print_module, print_stmt = print_stmt, lift_markup = apsnd } ml_program)); in (Code_Target.Singleton (ml_extension, p), try (deresolver [])) end; val serializer_sml : Code_Target.serializer = Code_Target.parse_args (Scan.succeed ()) #> K (serialize_ml print_sml_module print_sml_stmt "ML"); val serializer_ocaml : Code_Target.serializer = Code_Target.parse_args (Scan.succeed ()) #> K (serialize_ml print_ocaml_module print_ocaml_stmt "ocaml"); (** Isar setup **) fun fun_syntax print_typ fxy [ty1, ty2] = brackify_infix (1, R) fxy ( print_typ (INFX (1, X)) ty1, str "->", print_typ (INFX (1, R)) ty2 ); val _ = Theory.setup (Code_Target.add_language (target_SML, {serializer = serializer_sml, literals = literals_sml, check = {env_var = "", make_destination = fn p => p + Path.explode "ROOT.ML", make_command = fn _ => "isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure"}, evaluation_args = []}) #> Code_Target.add_language (target_OCaml, {serializer = serializer_ocaml, literals = literals_ocaml, check = {env_var = "ISABELLE_OCAMLFIND", make_destination = fn p => p + Path.explode "ROOT.ml" (*extension demanded by OCaml compiler*), make_command = fn _ => "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg ROOT.ml Code_Target.set_printings (Type_Constructor ("fun", [(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))])) #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names #> fold (Code_Target.add_reserved target_SML) [ "ref", (*rebinding is illegal*) "o", (*dictionary projections use it already*) "nil", (*predefined constructor*) "Fail", "div", "mod", (*standard infixes*) "IntInf"] #> fold (Code_Target.add_reserved target_OCaml) [ "and", "as", "assert", "begin", "class", "constraint", "do", "done", "downto", "else", "end", "exception", "external", "false", "for", "fun", "function", "functor", "if", "in", "include", "inherit", "initializer", "lazy", "let", "match", "method", "module", "mutable", "new", "object", "of", "open", "or", "private", "rec", "sig", "struct", "then", "to", "true", "try", "type", "val", "virtual", "when", "while", "with" ] #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Z"]); 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,492 +1,492 @@ (* 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_dictss tyvars ((str o deresolve o Class_Instance) inst) (map snd 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 (const as { sym, typargs, dom, dicts, ... }, ts)) = let 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 (wanted, 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)) val ((vs_tys, (ts1, rty)), ts2) = Code_Thingol.satisfied_application wanted app; in if null vs_tys then if null ts2 then print' fxy ts else Pretty.block (print' BR ts1 :: map (fn t => Pretty.block [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts2) else print_term tyvars is_pat some_thm vars fxy (vs_tys `|==> (IConst const `$$ ts1, rty)) 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", p, str "=", constraint (print_term tyvars false some_thm vars NOBR t) (print_typ tyvars BR ty)])); 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 = 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 (build (fold Code_Thingol.add_varnames 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", "enum", "export", "extends", "false", "final", "finally", "for", "forSome", "given", "if", "implicit", "import", "lazy", "match", "new", "null", "object", "override", "package", "private", "protected", "requires", "return", "sealed", "super", "then", "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,1107 +1,1109 @@ (* 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 `|=>; infixr 3 `|==>; signature BASIC_CODE_THINGOL = sig type vname = string + datatype itype = + `%% of string * itype list + | ITyVar of vname datatype dict = Dict of (class * class) list * plain_dict and plain_dict = - Dict_Const of (string * class) * dict list list + Dict_Const of (string * class) * (itype * 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, range: itype, annotation: itype option } datatype iterm = IConst of const | IVar of vname option | `$ of iterm * iterm | `|=> of (vname option * itype) * (iterm * itype) | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm } val `-> : itype * itype -> itype val `--> : itype list * itype -> itype val `$$ : iterm * iterm list -> iterm val `|==> : (vname option * itype) list * (iterm * itype) -> 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 unfold_abs_typed: iterm -> ((vname option * itype) list * (iterm * itype)) option 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 is_IVar: iterm -> bool val is_IAbs: iterm -> bool val satisfied_application: int -> const * iterm list -> ((vname option * itype) list * (iterm list * itype)) * iterm list val saturated_application: 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 val add_varnames: iterm -> string list -> string list 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, + superinsts: (class * (itype * 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 itype = + `%% of string * itype list + | ITyVar of vname; + datatype dict = Dict of (class * class) list * plain_dict and plain_dict = - Dict_Const of (string * class) * dict list list + Dict_Const of (string * class) * (itype * 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 op `--> = Library.foldr (op `->); 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; in (tys3, tys2 `--> ty1) end; type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list, dom: itype list, range: itype, annotation: itype option }; datatype iterm = IConst of const | IVar of vname option | `$ of iterm * iterm | `|=> of (vname option * itype) * (iterm * itype) | 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 `$); fun vs_tys `|==> body = Library.foldr (fn (v_ty as (_, ty), body as (_, rty)) => (v_ty `|=> body, ty `-> rty)) (vs_tys, body) |> fst; val unfold_app = unfoldl (fn op `$ t_t => SOME t_t | _ => NONE); val unfold_abs = unfoldr (fn (v `|=> (t, _)) => SOME (v, t) | _ => NONE); fun unfold_abs_typed (v_ty `|=> body) = unfoldr (fn (v_ty `|=> body, _) => SOME (v_ty, body) | _ => NONE) body |> apfst (cons v_ty) |> SOME | unfold_abs_typed _ = NONE fun split_let (ICase { term = t, typ = ty, clauses = [(p, body)], ... }) = SOME (((p, ty), t), body) | split_let _ = NONE; fun split_let_no_pat (ICase { term = t, typ = ty, clauses = [(IVar v, body)], ... }) = SOME (((v, ty), t), body) | split_let_no_pat _ = 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; val add_varnames = fold_varnames (insert (op =)); val declare_varnames = fold_varnames Name.declare; fun exists_var t v = fold_varnames (fn w => fn b => v = w orelse b) t false; fun invent_params used tys = Name.invent_names (Name.build_context used) "a" tys; 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, _) `|=> (t, _)) = let val (vs, t') = unfold_abs_eta tys t; in (v :: vs, t') end | unfold_abs_eta tys t = let val vs = map (SOME o fst) (invent_params (declare_varnames t) tys); in (vs, t `$$ map IVar vs) end; fun satisfied_application wanted ({ dom, range, ... }, ts) = let val given = length ts; val delta = wanted - given; val (_, rty) = unfold_fun_n wanted range; in if delta = 0 then (([], (ts, rty)), []) else if delta < 0 then let val (ts1, ts2) = chop wanted ts in (([], (ts1, rty)), ts2) end else let val vs_tys = invent_params (fold declare_varnames ts) (((take delta o drop given) dom)) |> (map o apfst) SOME; in ((vs_tys, (ts @ map (IVar o fst) vs_tys, rty)), []) end end fun saturated_application wanted (const, ts) = let val ((vs_tys, (ts', rty)), []) = satisfied_application wanted (const, ts) in vs_tys `|==> (IConst const `$$ ts', rty) 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, rty)) = f ((v, ty) `|=> (map_terms_bottom_up f t, rty)) | 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 distill_minimized_clause tys t = let fun restrict_vars_to vs = map_terms_bottom_up (fn IVar (SOME v) => IVar (if member (op =) vs v then SOME v else NONE) | t => t); fun purge_unused_vars_in t = restrict_vars_to (build (add_varnames t)); fun distill' vs_map pat_args v i clauses = let val pat_vs = build (fold add_varnames (nth_drop i pat_args)); fun varnames_disjunctive pat = null (inter (op =) pat_vs (build (add_varnames pat))); in if forall (fn (pat', body') => varnames_disjunctive pat' (*prevent mingled scopes resulting in duplicated variables in pattern arguments*) andalso (exists_var pat' v (*reducible if shadowed by pattern*) orelse not (exists_var body' v))) clauses (*reducible if absent in body*) then clauses |> maps (fn (pat', body') => distill vs_map (nth_map i (K pat') pat_args |> map (purge_unused_vars_in body')) body') |> SOME else NONE end and distill vs_map pat_args (body as ICase { term = IVar (SOME v), clauses = clauses, ... }) = (case AList.lookup (op =) vs_map v of SOME i => distill' (AList.delete (op =) v vs_map) pat_args v i clauses |> the_default [(pat_args, body)] | NONE => [(pat_args, body)]) | distill vs_map pat_args body = [(pat_args, body)]; val (vs, body) = unfold_abs_eta tys t; val vs_map = build (fold_index (fn (i, SOME v) => cons (v, i) | _ => I) vs); in distill vs_map (map IVar vs) body end; 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 +and exists_plain_dict_var_pred f (Dict_Const (_, dss)) = exists_dictss_var f (map snd 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; +and exists_dictss_var f = (exists o exists) (exists_dict_var f); 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, + superinsts: (class * (itype * 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 = 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 fastype_of_tagged_term = fastype_of o 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 snd) 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, (some_abs, rhs)) => (args, (some_abs, annotate ctxt' algbr eqngr (c, ty) args rhs)))) eqns 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 + Global of (string * class) * (typ * 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_constructor (tyco, typs) dss class = + Weakening ([], Global ((tyco, class), typs ~~ (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 is_undefined_clause ctxt (_, IConst { sym = Constant c, ... }) = Code.is_undefined (Proof_Context.theory_of ctxt) c | is_undefined_clause ctxt _ = false; fun satisfied_app wanted (ty, ts) = let val given = length ts; val delta = wanted - given; val rty = (drop delta o binder_types) ty ---> body_type ty; in if delta = 0 then (([], (ts, rty)), []) else if delta < 0 then let val (ts1, ts2) = chop wanted ts in (([], (ts1, rty)), ts2) end else let val tys = (take delta o drop given o binder_types) ty; val vs_tys = invent_params ((fold o fold_aterms) Term.declare_term_frees ts) tys; in ((vs_tys, (ts @ map Free vs_tys, rty)), []) end end 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 Name.aT (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 (binder_types 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) NONE const #>> (fn (c, 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 some_abs (Const (c, ty)) = translate_app ctxt algbr eqngr permissive some_thm some_abs ((c, ty), []) | translate_term ctxt algbr eqngr permissive some_thm some_abs (Free (v, _)) = pair (IVar (SOME v)) | translate_term ctxt algbr eqngr permissive some_thm some_abs (Abs (v, ty, t)) = 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 val rty = fastype_of_tagged_term t' in translate_typ ctxt algbr eqngr permissive ty ##>> translate_typ ctxt algbr eqngr permissive rty ##>> translate_term ctxt algbr eqngr permissive some_thm some_abs t' #>> (fn ((ty, rty), t) => (v'', ty) `|=> (t, rty)) end | translate_term ctxt algbr eqngr permissive some_thm some_abs (t as _ $ _) = case strip_comb t of (Const (c, ty), ts) => translate_app ctxt algbr eqngr permissive some_thm some_abs ((c, ty), ts) | (t', ts) => translate_term ctxt algbr eqngr permissive some_thm some_abs t' ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm NONE) ts #>> (fn (t, ts) => t `$$ ts) and translate_eqn ctxt algbr eqngr permissive ((args, (some_abs, rhs)), (some_thm, proper)) = fold_map (uncurry (translate_term ctxt algbr eqngr permissive some_thm)) args ##>> translate_term ctxt algbr eqngr permissive some_thm some_abs rhs #>> 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 some_abs (c, ty) (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) (range :: dom) #>> (fn (((c, typargs), dss), range :: dom) => { sym = Constant c, typargs = typargs, dicts = dss, dom = dom, range = range, annotation = if annotate then SOME (dom `--> range) else NONE }) end and translate_case ctxt algbr eqngr permissive some_thm (t_pos, []) (c_ty, ts) = let fun project_term xs = nth xs t_pos; val project_clause = the_single o nth_drop t_pos; val ty_case = project_term (binder_types (snd c_ty)); fun distill_clauses ty_case t = map (fn ([pat], body) => (pat, body)) (distill_minimized_clause [ty_case] t) in translate_const ctxt algbr eqngr permissive some_thm NONE c_ty ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm NONE) ts ##>> translate_typ ctxt algbr eqngr permissive ty_case #>> (fn ((const, ts), ty_case) => ICase { term = project_term ts, typ = ty_case, clauses = (filter_out (is_undefined_clause ctxt) o distill_clauses ty_case o project_clause) ts, primitive = IConst const `$$ ts }) end | translate_case ctxt algbr eqngr permissive some_thm (t_pos, case_pats) (c_ty, ts) = let fun project_term xs = nth xs t_pos; fun project_cases xs = xs |> nth_drop t_pos |> curry (op ~~) case_pats |> map_filter (fn (NONE, _) => NONE | (SOME _, x) => SOME x); val ty_case = project_term (binder_types (snd c_ty)); val constrs = map_filter I case_pats ~~ project_cases ts |> map (fn ((c, n), t) => ((c, (take n o binder_types o fastype_of_tagged_term) t ---> ty_case), n)); fun distill_clauses constrs ts_clause = maps (fn ((constr as { dom = tys, ... }, n), t) => map (fn (pat_args, body) => (IConst constr `$$ pat_args, body)) (distill_minimized_clause (take n tys) t)) (constrs ~~ ts_clause); in translate_const ctxt algbr eqngr permissive some_thm NONE c_ty ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm NONE) ts ##>> translate_typ ctxt algbr eqngr permissive ty_case ##>> fold_map (fn (c_ty, n) => translate_const ctxt algbr eqngr permissive some_thm NONE c_ty #>> rpair n) constrs #>> (fn (((const, ts), ty_case), constrs) => ICase { term = project_term ts, typ = ty_case, clauses = (filter_out (is_undefined_clause ctxt) o distill_clauses constrs o project_cases) ts, primitive = IConst const `$$ ts }) end and translate_app_case ctxt algbr eqngr permissive some_thm pattern_schema c_ty ((vs_tys, (ts1, rty)), ts2) = fold_map (fn (v, ty) => translate_typ ctxt algbr eqngr permissive ty #>> pair (SOME v)) vs_tys ##>> translate_case ctxt algbr eqngr permissive some_thm pattern_schema (c_ty, ts1) ##>> translate_typ ctxt algbr eqngr permissive rty ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm NONE) ts2 #>> (fn (((vs_tys, t), rty), ts) => (vs_tys `|==> (t, rty)) `$$ ts) and translate_app ctxt algbr eqngr permissive some_thm some_abs (c_ty as (c, ty), ts) = case Code.get_case_schema (Proof_Context.theory_of ctxt) c of SOME (wanted, pattern_schema) => translate_app_case ctxt algbr eqngr permissive some_thm pattern_schema c_ty (satisfied_app wanted (ty, ts)) | NONE => translate_const ctxt algbr eqngr permissive some_thm some_abs c_ty ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm NONE) ts #>> (fn (const, ts) => IConst const `$$ ts) 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)) = + fun translate_dict (Weakening (classrels, d)) = fold_map (ensure_classrel ctxt algbr eqngr permissive) classrels - ##>> mk_plain_dict d + ##>> translate_plain_dict d #>> Dict - and mk_plain_dict (Global (inst, dss)) = + and translate_plain_dict (Global (inst, dss)) = ensure_inst ctxt algbr eqngr permissive inst - ##>> (fold_map o fold_map) mk_dict dss + ##>> fold_map (fn (ty, ds) => + translate_typ ctxt algbr eqngr permissive ty + ##>> fold_map translate_dict ds) dss #>> Dict_Const - | mk_plain_dict (Local { var, index, sort, unique }) = + | translate_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) + #-> (fn typarg_witnesses => fold_map translate_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 NONE t' #>> (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; diff --git a/src/Tools/nbe.ML b/src/Tools/nbe.ML --- a/src/Tools/nbe.ML +++ b/src/Tools/nbe.ML @@ -1,623 +1,623 @@ (* Title: Tools/nbe.ML Authors: Klaus Aehlig, LMU Muenchen; Tobias Nipkow, Florian Haftmann, TU Muenchen Normalization by evaluation, based on generic code generator. *) signature NBE = sig val dynamic_conv: Proof.context -> conv val dynamic_value: Proof.context -> term -> term val static_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv val static_value: { ctxt: Proof.context, consts: string list } -> Proof.context -> term -> term datatype Univ = Const of int * Univ list (*named (uninterpreted) constants*) | DFree of string * int (*free (uninterpreted) dictionary parameters*) | BVar of int * Univ list | Abs of (int * (Univ list -> Univ)) * Univ list val apps: Univ -> Univ list -> Univ (*explicit applications*) val abss: int -> (Univ list -> Univ) -> Univ (*abstractions as closures*) val same: Univ * Univ -> bool val put_result: (unit -> Univ list -> Univ list) -> Proof.context -> Proof.context val trace: bool Config.T val add_const_alias: thm -> theory -> theory end; structure Nbe: NBE = struct (* generic non-sense *) val trace = Attrib.setup_config_bool \<^binding>\nbe_trace\ (K false); fun traced ctxt f x = if Config.get ctxt trace then (tracing (f x); x) else x; (** certificates and oracle for "trivial type classes" **) structure Triv_Class_Data = Theory_Data ( type T = (class * thm) list; val empty = []; fun merge data : T = AList.merge (op =) (K true) data; ); fun add_const_alias thm thy = let val (ofclass, eqn) = case try Logic.dest_equals (Thm.prop_of thm) of SOME ofclass_eq => ofclass_eq | _ => error ("Bad certificate: " ^ Thm.string_of_thm_global thy thm); val (T, class) = case try Logic.dest_of_class ofclass of SOME T_class => T_class | _ => error ("Bad certificate: " ^ Thm.string_of_thm_global thy thm); val tvar = case try Term.dest_TVar T of SOME (tvar as (_, sort)) => if null (filter (can (Axclass.get_info thy)) sort) then tvar else error ("Bad sort: " ^ Thm.string_of_thm_global thy thm) | _ => error ("Bad type: " ^ Thm.string_of_thm_global thy thm); val _ = if Term.add_tvars eqn [] = [tvar] then () else error ("Inconsistent type: " ^ Thm.string_of_thm_global thy thm); val lhs_rhs = case try Logic.dest_equals eqn of SOME lhs_rhs => lhs_rhs | _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn); val c_c' = case try (apply2 (Axclass.unoverload_const thy o dest_Const)) lhs_rhs of SOME c_c' => c_c' | _ => error ("Not an equation with two constants: " ^ Syntax.string_of_term_global thy eqn); val _ = if the_list (Axclass.class_of_param thy (snd c_c')) = [class] then () else error ("Inconsistent class: " ^ Thm.string_of_thm_global thy thm); in Triv_Class_Data.map (AList.update (op =) (class, Thm.trim_context thm)) thy end; local val get_triv_classes = map fst o Triv_Class_Data.get; val (_, triv_of_class) = Context.>>> (Context.map_theory_result (Thm.add_oracle (\<^binding>\triv_of_class\, fn (thy, T, class) => Thm.global_cterm_of thy (Logic.mk_of_class (T, class))))); in fun lift_triv_classes_conv orig_ctxt conv ct = let val thy = Proof_Context.theory_of orig_ctxt; val ctxt = Proof_Context.init_global thy; (*FIXME quasi-global context*) val algebra = Sign.classes_of thy; val triv_classes = get_triv_classes thy; fun additional_classes sort = filter_out (fn class => Sorts.sort_le algebra (sort, [class])) triv_classes; fun mk_entry (v, sort) = let val T = TFree (v, sort); val cT = Thm.ctyp_of ctxt T; val triv_sort = additional_classes sort; in (v, (Sorts.inter_sort algebra (sort, triv_sort), (cT, AList.make (fn class => Thm.of_class (cT, class)) sort @ AList.make (fn class => triv_of_class (thy, T, class)) triv_sort))) end; val vs_tab = map mk_entry (Term.add_tfrees (Thm.term_of ct) []); fun instantiate thm = let val tvars = Term.add_tvars (#1 (Logic.dest_equals (Logic.strip_imp_concl (Thm.prop_of thm)))) []; val instT = map2 (fn v => fn (_, (_, (cT, _))) => (v, cT)) tvars vs_tab; in Thm.instantiate (TVars.make instT, Vars.empty) thm end; fun of_class (TFree (v, _), class) = the (AList.lookup (op =) ((snd o snd o the o AList.lookup (op =) vs_tab) v) class) | of_class (T, _) = error ("Bad type " ^ Syntax.string_of_typ ctxt T); fun strip_of_class thm = let val prems_of_class = Thm.prop_of thm |> Logic.strip_imp_prems |> map (Logic.dest_of_class #> of_class); in fold Thm.elim_implies prems_of_class thm end; in ct |> Thm.term_of |> (map_types o map_type_tfree) (fn (v, _) => TFree (v, (fst o the o AList.lookup (op =) vs_tab) v)) |> Thm.cterm_of ctxt |> conv ctxt |> Thm.strip_shyps |> Thm.varifyT_global |> Thm.unconstrainT |> instantiate |> strip_of_class end; fun lift_triv_classes_rew ctxt rew t = let val thy = Proof_Context.theory_of ctxt; val algebra = Sign.classes_of thy; val triv_classes = get_triv_classes thy; val vs = Term.add_tfrees t []; in t |> (map_types o map_type_tfree) (fn (v, sort) => TFree (v, Sorts.inter_sort algebra (sort, triv_classes))) |> rew |> (map_types o map_type_tfree) (fn (v, sort) => TFree (v, the_default sort (AList.lookup (op =) vs v))) end; end; (** the semantic universe **) (* Functions are given by their semantical function value. To avoid trouble with the ML-type system, these functions have the most generic type, that is "Univ list -> Univ". The calling convention is that the arguments come as a list, the last argument first. In other words, a function call that usually would look like f x_1 x_2 ... x_n or f(x_1,x_2, ..., x_n) would be in our convention called as f [x_n,..,x_2,x_1] Moreover, to handle functions that are still waiting for some arguments we have additionally a list of arguments collected to far and the number of arguments we're still waiting for. *) datatype Univ = Const of int * Univ list (*named (uninterpreted) constants*) | DFree of string * int (*free (uninterpreted) dictionary parameters*) | BVar of int * Univ list (*bound variables, named*) | Abs of (int * (Univ list -> Univ)) * Univ list (*abstractions as closures*); (* constructor functions *) fun abss n f = Abs ((n, f), []); fun apps (Abs ((n, f), xs)) ys = let val k = n - length ys in case int_ord (k, 0) of EQUAL => f (ys @ xs) | LESS => let val (zs, ws) = chop (~ k) ys in apps (f (ws @ xs)) zs end | GREATER => Abs ((k, f), ys @ xs) (*note: reverse convention also for apps!*) end | apps (Const (name, xs)) ys = Const (name, ys @ xs) | apps (BVar (n, xs)) ys = BVar (n, ys @ xs); fun same (Const (k, xs), Const (l, ys)) = k = l andalso eq_list same (xs, ys) | same (DFree (s, k), DFree (t, l)) = s = t andalso k = l | same (BVar (k, xs), BVar (l, ys)) = k = l andalso eq_list same (xs, ys) | same _ = false; (** assembling and compiling ML code from terms **) (* abstract ML syntax *) infix 9 `$` `$$`; fun e1 `$` e2 = "(" ^ e1 ^ " " ^ e2 ^ ")"; fun e `$$` [] = e | e `$$` es = "(" ^ e ^ " " ^ space_implode " " es ^ ")"; fun ml_abs v e = "(fn " ^ v ^ " => " ^ e ^ ")"; fun ml_cases t cs = "(case " ^ t ^ " of " ^ space_implode " | " (map (fn (p, t) => p ^ " => " ^ t) cs) ^ ")"; fun ml_Let d e = "let\n" ^ d ^ " in " ^ e ^ " end"; fun ml_as v t = "(" ^ v ^ " as " ^ t ^ ")"; fun ml_and [] = "true" | ml_and [x] = x | ml_and xs = "(" ^ space_implode " andalso " xs ^ ")"; fun ml_if b x y = "(if " ^ b ^ " then " ^ x ^ " else " ^ y ^ ")"; fun ml_list es = "[" ^ commas es ^ "]"; fun ml_fundefs ([(name, [([], e)])]) = "val " ^ name ^ " = " ^ e ^ "\n" | ml_fundefs (eqs :: eqss) = let fun fundef (name, eqs) = let fun eqn (es, e) = name ^ " " ^ space_implode " " es ^ " = " ^ e in space_implode "\n | " (map eqn eqs) end; in (prefix "fun " o fundef) eqs :: map (prefix "and " o fundef) eqss |> cat_lines |> suffix "\n" end; (* nbe specific syntax and sandbox communication *) structure Univs = Proof_Data ( type T = unit -> Univ list -> Univ list; val empty: T = fn () => raise Fail "Univs"; fun init _ = empty; ); val get_result = Univs.get; val put_result = Univs.put; local val prefix = "Nbe."; val name_put = prefix ^ "put_result"; val name_const = prefix ^ "Const"; val name_abss = prefix ^ "abss"; val name_apps = prefix ^ "apps"; val name_same = prefix ^ "same"; in val univs_cookie = (get_result, put_result, name_put); fun nbe_fun idx_of 0 (Code_Symbol.Constant "") = "nbe_value" | nbe_fun idx_of i sym = "c_" ^ string_of_int (idx_of sym) ^ "_" ^ Code_Symbol.default_base sym ^ "_" ^ string_of_int i; fun nbe_dict v n = "d_" ^ v ^ "_" ^ string_of_int n; fun nbe_bound v = "v_" ^ v; fun nbe_bound_optional NONE = "_" | nbe_bound_optional (SOME v) = nbe_bound v; fun nbe_default v = "w_" ^ v; (*note: these three are the "turning spots" where proper argument order is established!*) fun nbe_apps t [] = t | nbe_apps t ts = name_apps `$$` [t, ml_list (rev ts)]; fun nbe_apps_local idx_of i c ts = nbe_fun idx_of i c `$` ml_list (rev ts); fun nbe_apps_constr ctxt idx_of c ts = let val c' = if Config.get ctxt trace then string_of_int (idx_of c) ^ " (*" ^ Code_Symbol.default_base c ^ "*)" else string_of_int (idx_of c); in name_const `$` ("(" ^ c' ^ ", " ^ ml_list (rev ts) ^ ")") end; fun nbe_abss 0 f = f `$` ml_list [] | nbe_abss n f = name_abss `$$` [string_of_int n, f]; fun nbe_same (v1, v2) = "(" ^ name_same ^ " (" ^ nbe_bound v1 ^ ", " ^ nbe_bound v2 ^ "))"; end; open Basic_Code_Symbol; open Basic_Code_Thingol; (* code generation *) fun assemble_eqnss ctxt idx_of deps eqnss = let fun prep_eqns (c, (vs, eqns)) = let val dicts = maps (fn (v, sort) => map_index (nbe_dict v o fst) sort) vs; val num_args = length dicts + ((length o fst o hd) eqns); in (c, (num_args, (dicts, eqns))) end; val eqnss' = map prep_eqns eqnss; fun assemble_constapp sym dss ts = let val ts' = (maps o map) assemble_dict dss @ ts; in case AList.lookup (op =) eqnss' sym of SOME (num_args, _) => if num_args <= length ts' then let val (ts1, ts2) = chop num_args ts' in nbe_apps (nbe_apps_local idx_of 0 sym ts1) ts2 end else nbe_apps (nbe_abss num_args (nbe_fun idx_of 0 sym)) ts' | NONE => if member (op =) deps sym then nbe_apps (nbe_fun idx_of 0 sym) ts' else nbe_apps_constr ctxt idx_of sym ts' end and assemble_classrels classrels = fold_rev (fn classrel => assemble_constapp (Class_Relation classrel) [] o single) classrels and assemble_dict (Dict (classrels, x)) = assemble_classrels classrels (assemble_plain_dict x) and assemble_plain_dict (Dict_Const (inst, dss)) = - assemble_constapp (Class_Instance inst) dss [] + assemble_constapp (Class_Instance inst) (map snd dss) [] | assemble_plain_dict (Dict_Var { var, index, ... }) = nbe_dict var index fun assemble_iterm constapp = let fun of_iterm match_cont t = let val (t', ts) = Code_Thingol.unfold_app t in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end and of_iapp match_cont (IConst { sym, dicts = dss, ... }) ts = constapp sym dss ts | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts | of_iapp match_cont ((v, _) `|=> (t, _)) ts = nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts | of_iapp match_cont (ICase { term = t, clauses = clauses, primitive = t0, ... }) ts = nbe_apps (ml_cases (of_iterm NONE t) (map (fn (p, t) => (of_iterm NONE p, of_iterm match_cont t)) clauses @ [("_", case match_cont of SOME s => s | NONE => of_iterm NONE t0)])) ts in of_iterm end; fun subst_nonlin_vars args = let val vs = (fold o Code_Thingol.fold_varnames) (fn v => AList.map_default (op =) (v, 0) (Integer.add 1)) args []; val names = Name.make_context (map fst vs); fun declare v k ctxt = let val vs = Name.invent ctxt v k in (vs, fold Name.declare vs ctxt) end; val (vs_renames, _) = fold_map (fn (v, k) => if k > 1 then declare v (k - 1) #>> (fn vs => (v, vs)) else pair (v, [])) vs names; val samepairs = maps (fn (v, vs) => map (pair v) vs) vs_renames; fun subst_vars (t as IConst _) samepairs = (t, samepairs) | subst_vars (t as IVar NONE) samepairs = (t, samepairs) | subst_vars (t as IVar (SOME v)) samepairs = (case AList.lookup (op =) samepairs v of SOME v' => (IVar (SOME v'), AList.delete (op =) v samepairs) | NONE => (t, samepairs)) | subst_vars (t1 `$ t2) samepairs = samepairs |> subst_vars t1 ||>> subst_vars t2 |>> (op `$) | subst_vars (ICase { primitive = t, ... }) samepairs = subst_vars t samepairs; val (args', _) = fold_map subst_vars args samepairs; in (samepairs, args') end; fun assemble_eqn sym dicts default_args (i, (args, rhs)) = let val match_cont = if Code_Symbol.is_value sym then NONE else SOME (nbe_apps_local idx_of (i + 1) sym (dicts @ default_args)); val assemble_arg = assemble_iterm (fn sym' => fn dss => fn ts => nbe_apps_constr ctxt idx_of sym' ((maps o map) (K "_") dss @ ts)) NONE; val assemble_rhs = assemble_iterm assemble_constapp match_cont; val (samepairs, args') = subst_nonlin_vars args; val s_args = map assemble_arg args'; val s_rhs = if null samepairs then assemble_rhs rhs else ml_if (ml_and (map nbe_same samepairs)) (assemble_rhs rhs) (the match_cont); val eqns = case match_cont of NONE => [([ml_list (rev (dicts @ s_args))], s_rhs)] | SOME default_rhs => [([ml_list (rev (dicts @ map2 ml_as default_args s_args))], s_rhs), ([ml_list (rev (dicts @ default_args))], default_rhs)] in (nbe_fun idx_of i sym, eqns) end; fun assemble_eqns (sym, (num_args, (dicts, eqns))) = let val default_args = map nbe_default (Name.invent Name.context "a" (num_args - length dicts)); val eqns' = map_index (assemble_eqn sym dicts default_args) eqns @ (if Code_Symbol.is_value sym then [] else [(nbe_fun idx_of (length eqns) sym, [([ml_list (rev (dicts @ default_args))], nbe_apps_constr ctxt idx_of sym (dicts @ default_args))])]); in (eqns', nbe_abss num_args (nbe_fun idx_of 0 sym)) end; val (fun_vars, fun_vals) = map_split assemble_eqns eqnss'; val deps_vars = ml_list (map (nbe_fun idx_of 0) deps); in ml_abs deps_vars (ml_Let (ml_fundefs (flat fun_vars)) (ml_list fun_vals)) end; (* compilation of equations *) fun compile_eqnss ctxt nbe_program raw_deps [] = [] | compile_eqnss ctxt nbe_program raw_deps eqnss = let val (deps, deps_vals) = split_list (map_filter (fn dep => Option.map (fn univ => (dep, univ)) (fst ((Code_Symbol.Graph.get_node nbe_program dep)))) raw_deps); val idx_of = raw_deps |> map (fn dep => (dep, snd (Code_Symbol.Graph.get_node nbe_program dep))) |> AList.lookup (op =) |> (fn f => the o f); val s = assemble_eqnss ctxt idx_of deps eqnss; val cs = map fst eqnss; in s |> traced ctxt (fn s => "\n--- code to be evaluated:\n" ^ s) |> pair "" |> Code_Runtime.value ctxt univs_cookie |> (fn f => f deps_vals) |> (fn univs => cs ~~ univs) end; (* extraction of equations from statements *) fun dummy_const sym dss = IConst { sym = sym, typargs = [], dicts = dss, dom = [], annotation = NONE, range = ITyVar "" }; fun eqns_of_stmt (_, Code_Thingol.NoStmt) = [] | eqns_of_stmt (_, Code_Thingol.Fun ((_, []), _)) = [] | eqns_of_stmt (sym_const, Code_Thingol.Fun (((vs, _), eqns), _)) = [(sym_const, (vs, map fst eqns))] | eqns_of_stmt (_, Code_Thingol.Datatypecons _) = [] | eqns_of_stmt (_, Code_Thingol.Datatype _) = [] | eqns_of_stmt (sym_class, Code_Thingol.Class (v, (classrels, classparams))) = let val syms = map Class_Relation classrels @ map (Constant o fst) classparams; val params = Name.invent Name.context "d" (length syms); fun mk (k, sym) = (sym, ([(v, [])], [([dummy_const sym_class [] `$$ map (IVar o SOME) params], IVar (SOME (nth params k)))])); in map_index mk syms end | eqns_of_stmt (_, Code_Thingol.Classrel _) = [] | eqns_of_stmt (_, Code_Thingol.Classparam _) = [] | eqns_of_stmt (sym_inst, Code_Thingol.Classinst { class, tyco, vs, superinsts, inst_params, ... }) = [(sym_inst, (vs, [([], dummy_const (Type_Class class) [] `$$ - map (fn (class, dss) => dummy_const (Class_Instance (tyco, class)) dss) superinsts + map (fn (class, dss) => dummy_const (Class_Instance (tyco, class)) (map snd dss)) superinsts @ map (IConst o fst o snd o fst) inst_params)]))]; (* compilation of whole programs *) fun ensure_const_idx name (nbe_program, (maxidx, idx_tab)) = if can (Code_Symbol.Graph.get_node nbe_program) name then (nbe_program, (maxidx, idx_tab)) else (Code_Symbol.Graph.new_node (name, (NONE, maxidx)) nbe_program, (maxidx + 1, Inttab.update_new (maxidx, name) idx_tab)); fun compile_stmts ctxt stmts_deps = let val names = map (fst o fst) stmts_deps; val names_deps = map (fn ((name, _), deps) => (name, deps)) stmts_deps; val eqnss = maps (eqns_of_stmt o fst) stmts_deps; val refl_deps = names_deps |> maps snd |> distinct (op =) |> fold (insert (op =)) names; fun compile nbe_program = eqnss |> compile_eqnss ctxt nbe_program refl_deps |> rpair nbe_program; in fold ensure_const_idx refl_deps #> apfst (fold (fn (name, deps) => fold (curry Code_Symbol.Graph.add_edge name) deps) names_deps #> compile #-> fold (fn (name, univ) => (Code_Symbol.Graph.map_node name o apfst) (K (SOME univ)))) end; fun compile_program { ctxt, program } = let fun add_stmts names (nbe_program, (maxidx, idx_tab)) = if exists ((can o Code_Symbol.Graph.get_node) nbe_program) names then (nbe_program, (maxidx, idx_tab)) else (nbe_program, (maxidx, idx_tab)) |> compile_stmts ctxt (map (fn name => ((name, Code_Symbol.Graph.get_node program name), Code_Symbol.Graph.immediate_succs program name)) names); in fold_rev add_stmts (Code_Symbol.Graph.strong_conn program) end; (** normalization **) (* compilation and reconstruction of terms *) fun compile_term { ctxt, nbe_program, deps, term = (vs, t) } = let val dict_frees = maps (fn (v, sort) => map_index (curry DFree v o fst) sort) vs; in (Code_Symbol.value, (vs, [([], t)])) |> singleton (compile_eqnss ctxt nbe_program deps) |> snd |> (fn t => apps t (rev dict_frees)) end; fun reconstruct_term ctxt (idx_tab : Code_Symbol.T Inttab.table) t = let fun take_until f [] = [] | take_until f (x :: xs) = if f x then [] else x :: take_until f xs; fun is_dict (Const (idx, _)) = (case Inttab.lookup idx_tab idx of SOME (Constant _) => false | _ => true) | is_dict (DFree _) = true | is_dict _ = false; fun const_of_idx idx = case Inttab.lookup idx_tab idx of SOME (Constant const) => const; fun of_apps bounds (t, ts) = fold_map (of_univ bounds) ts #>> (fn ts' => list_comb (t, rev ts')) and of_univ bounds (Const (idx, ts)) typidx = let val ts' = take_until is_dict ts; val const = const_of_idx idx; val T = map_type_tvar (fn ((v, i), _) => Type_Infer.param typidx (v ^ string_of_int i, [])) (Sign.the_const_type (Proof_Context.theory_of ctxt) const); val typidx' = typidx + 1; in of_apps bounds (Term.Const (const, T), ts') typidx' end | of_univ bounds (BVar (n, ts)) typidx = of_apps bounds (Bound (bounds - n - 1), ts) typidx | of_univ bounds (t as Abs _) typidx = typidx |> of_univ (bounds + 1) (apps t [BVar (bounds, [])]) |-> (fn t' => pair (Term.Abs ("u", dummyT, t'))) in of_univ 0 t 0 |> fst end; fun compile_and_reconstruct_term { ctxt, nbe_program, idx_tab, deps, term } = compile_term { ctxt = ctxt, nbe_program = nbe_program, deps = deps, term = term } |> reconstruct_term ctxt idx_tab; fun normalize_term (nbe_program, idx_tab) raw_ctxt t_original ((vs, ty) : typscheme, t) deps = let val ctxt = Syntax.init_pretty_global (Proof_Context.theory_of raw_ctxt); val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt); fun type_infer t' = Syntax.check_term (ctxt |> Config.put Type_Infer.object_logic false |> Config.put Type_Infer_Context.const_sorts false) (Type.constraint (fastype_of t_original) t'); fun check_tvars t' = if null (Term.add_tvars t' []) then t' else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t'); in Code_Preproc.timed "computing NBE expression" #ctxt compile_and_reconstruct_term { ctxt = ctxt, nbe_program = nbe_program, idx_tab = idx_tab, deps = deps, term = (vs, t) } |> traced ctxt (fn t => "Normalized:\n" ^ string_of_term t) |> type_infer |> traced ctxt (fn t => "Types inferred:\n" ^ string_of_term t) |> check_tvars |> traced ctxt (fn _ => "---\n") end; (* function store *) structure Nbe_Functions = Code_Data ( type T = (Univ option * int) Code_Symbol.Graph.T * (int * Code_Symbol.T Inttab.table); val empty = (Code_Symbol.Graph.empty, (0, Inttab.empty)); ); fun compile ignore_cache ctxt program = let val (nbe_program, (_, idx_tab)) = Nbe_Functions.change (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt)) (Code_Preproc.timed "compiling NBE program" #ctxt compile_program { ctxt = ctxt, program = program }); in (nbe_program, idx_tab) end; (* evaluation oracle *) fun mk_equals ctxt lhs raw_rhs = let val ty = Thm.typ_of_cterm lhs; val eq = Thm.cterm_of ctxt \<^Const>\Pure.eq ty\; val rhs = Thm.cterm_of ctxt raw_rhs; in Thm.mk_binop eq lhs rhs end; val (_, raw_oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (\<^binding>\normalization_by_evaluation\, fn (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct) => mk_equals ctxt ct (normalize_term nbe_program_idx_tab ctxt (Thm.term_of ct) vs_ty_t deps)))); fun oracle nbe_program_idx_tab ctxt vs_ty_t deps ct = raw_oracle (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct); fun dynamic_conv ctxt = lift_triv_classes_conv ctxt (fn ctxt' => Code_Thingol.dynamic_conv ctxt' (fn program => oracle (compile false ctxt program) ctxt')); fun dynamic_value ctxt = lift_triv_classes_rew ctxt (Code_Thingol.dynamic_value ctxt I (fn program => normalize_term (compile false ctxt program) ctxt)); fun static_conv (ctxt_consts as { ctxt, ... }) = let val conv = Code_Thingol.static_conv_thingol ctxt_consts (fn { program, deps = _ } => oracle (compile true ctxt program)); in fn ctxt' => lift_triv_classes_conv ctxt' conv end; fun static_value { ctxt, consts } = let val comp = Code_Thingol.static_value { ctxt = ctxt, lift_postproc = I, consts = consts } (fn { program, deps = _ } => normalize_term (compile false ctxt program)); in fn ctxt' => lift_triv_classes_rew ctxt' (comp ctxt') end; end;