diff --git a/src/Tools/Code/code_haskell.ML b/src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML +++ b/src/Tools/Code/code_haskell.ML @@ -1,512 +1,511 @@ (* Title: Tools/Code/code_haskell.ML Author: Florian Haftmann, TU Muenchen Serializer for Haskell. *) signature CODE_HASKELL = sig val language_params: string val target: string val print_numeral: string -> int -> string end; structure Code_Haskell : CODE_HASKELL = struct val target = "Haskell"; val language_extensions = ["EmptyDataDecls", "RankNTypes", "ScopedTypeVariables"]; val language_pragma = "{-# LANGUAGE " ^ commas language_extensions ^ " #-}"; val language_params = space_implode " " (map (prefix "-X") language_extensions); open Basic_Code_Symbol; open Basic_Code_Thingol; open Code_Printer; infixr 5 @@; infixr 5 @|; (** Haskell serializer **) val print_haskell_string = quote o translate_string (fn c => if Symbol.is_ascii c then GHC.print_codepoint (ord c) else error "non-ASCII byte in Haskell string literal"); fun print_haskell_stmt class_syntax tyco_syntax const_syntax reserved deresolve deriving_show = let val deresolve_const = deresolve o Constant; val deresolve_tyco = deresolve o Type_Constructor; val deresolve_class = deresolve o Type_Class; fun class_name class = case class_syntax class of NONE => deresolve_class class | SOME class => class; fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs of [] => [] | constraints => enum "," "(" ")" ( map (fn (v, class) => str (class_name class ^ " " ^ lookup_var tyvars v)) constraints) @@ str " => "; fun print_typforall tyvars vs = case map fst vs of [] => [] | vnames => str "forall " :: Pretty.breaks (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1; fun print_tyco_expr tyvars fxy (tyco, tys) = brackify fxy (str tyco :: map (print_typ tyvars BR) tys) and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco of NONE => print_tyco_expr tyvars fxy (deresolve_tyco tyco, tys) | SOME (_, print) => print (print_typ tyvars) fxy tys) | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v; fun print_typdecl tyvars (tyco, vs) = print_tyco_expr tyvars NOBR (tyco, map ITyVar vs); fun print_typscheme tyvars (vs, ty) = Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty); fun print_term tyvars some_thm vars fxy (IConst const) = print_app tyvars some_thm vars fxy (const, []) | print_term tyvars some_thm vars fxy (t as (t1 `$ t2)) = (case Code_Thingol.unfold_const_app t of SOME app => print_app tyvars some_thm vars fxy app | _ => brackify fxy [ print_term tyvars some_thm vars NOBR t1, print_term tyvars some_thm vars BR t2 ]) | print_term tyvars some_thm vars fxy (IVar NONE) = str "_" | print_term tyvars some_thm vars fxy (IVar (SOME v)) = (str o lookup_var vars) v | print_term tyvars some_thm vars fxy (t as _ `|=> _) = let val (binds, t') = Code_Thingol.unfold_pat_abs t; val (ps, vars') = fold_map (print_bind tyvars some_thm BR o fst) binds vars; in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end | print_term tyvars 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 some_thm vars fxy app | NONE => print_case tyvars some_thm vars fxy case_expr) and print_app_expr tyvars some_thm vars ({ sym, annotation, ... }, ts) = let val printed_const = case annotation of SOME ty => brackets [(str o deresolve) sym, str "::", print_typ tyvars NOBR ty] | NONE => (str o deresolve) sym in printed_const :: map (print_term tyvars some_thm vars BR) ts end and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p and print_case tyvars some_thm vars fxy { clauses = [], ... } = (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""] | print_case tyvars some_thm vars fxy (case_expr as { clauses = [(IVar _, _)], ... }) = let val (vs, body) = Code_Thingol.unfold_let_no_pat (ICase case_expr); fun print_assignment ((some_v, _), t) vars = vars |> print_bind tyvars some_thm BR (IVar some_v) |>> (fn p => semicolon [p, str "=", print_term tyvars some_thm vars NOBR t]) val (ps, vars') = fold_map print_assignment vs vars; in brackify_block fxy (str "let {") ps (concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body]) end | print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } = let fun print_select (pat, body) = let val (p, vars') = print_bind tyvars some_thm NOBR pat vars; in semicolon [p, str "->", print_term tyvars some_thm vars' NOBR body] end; in Pretty.block_enclose (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})") (map print_select clauses) end; fun print_stmt (Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) = let val tyvars = intro_vars (map fst vs) reserved; fun print_err n = (semicolon o map str) ( deresolve_const const :: replicate n "_" @ "=" :: "error" @@ print_haskell_string const ); 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 ((fold o Code_Thingol.fold_varnames) - (insert (op =)) ts []); + |> intro_vars (build (fold Code_Thingol.add_varnames ts)); in semicolon ( (str o deresolve_const) const :: map (print_term tyvars some_thm vars BR) ts @ str "=" @@ print_term tyvars some_thm vars NOBR t ) end; in Pretty.chunks ( semicolon [ (str o suffix " ::" o deresolve_const) const, print_typscheme tyvars (vs, ty) ] :: (case filter (snd o snd) raw_eqs of [] => [print_err ((length o fst o Code_Thingol.unfold_fun) ty)] | eqs => map print_eqn eqs) ) end | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, [])) = let val tyvars = intro_vars vs reserved; in semicolon [ str "data", print_typdecl tyvars (deresolve_tyco tyco, vs) ] end | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, [((co, _), [ty])])) = let val tyvars = intro_vars vs reserved; in semicolon ( str "newtype" :: print_typdecl tyvars (deresolve_tyco tyco, vs) :: str "=" :: (str o deresolve_const) co :: print_typ tyvars BR ty :: (if deriving_show tyco then [str "deriving (Prelude.Read, Prelude.Show)"] else []) ) end | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, co :: cos)) = let val tyvars = intro_vars vs reserved; fun print_co ((co, _), tys) = concat ( (str o deresolve_const) co :: map (print_typ tyvars BR) tys ) in semicolon ( str "data" :: print_typdecl tyvars (deresolve_tyco tyco, vs) :: str "=" :: print_co co :: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos @ (if deriving_show tyco then [str "deriving (Prelude.Read, Prelude.Show)"] else []) ) end | print_stmt (Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) = let val tyvars = intro_vars [v] reserved; fun print_classparam (classparam, ty) = semicolon [ (str o deresolve_const) classparam, str "::", print_typ tyvars NOBR ty ] in Pretty.block_enclose ( Pretty.block [ str "class ", Pretty.block (print_typcontext tyvars [(v, map snd classrels)]), str (deresolve_class class ^ " " ^ lookup_var tyvars v), str " where {" ], str "};" ) (map print_classparam classparams) end | print_stmt (_, Code_Thingol.Classinst { class, tyco, vs, inst_params, ... }) = let val tyvars = intro_vars (map fst vs) reserved; fun print_classparam_instance ((classparam, (const, _)), (thm, _)) = case const_syntax classparam of NONE => semicolon [ (str o Long_Name.base_name o deresolve_const) classparam, str "=", print_app tyvars (SOME thm) reserved NOBR (const, []) ] | SOME (_, Code_Printer.Plain_printer s) => semicolon [ (str o Long_Name.base_name) s, str "=", print_app tyvars (SOME thm) reserved NOBR (const, []) ] | SOME (k, Code_Printer.Complex_printer _) => let val { sym = Constant c, dom, ... } = const; val (vs, rhs) = (apfst o map) fst (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, []))); val s = if (is_some o const_syntax) c then NONE else (SOME o Long_Name.base_name o deresolve_const) c; val vars = reserved |> intro_vars (map_filter I (s :: vs)); val lhs = IConst { sym = Constant classparam, typargs = [], dicts = [], dom = dom, annotation = NONE } `$$ map IVar vs; (*dictionaries are not relevant at this late stage, and these consts never need type annotations for disambiguation *) in semicolon [ print_term tyvars (SOME thm) vars NOBR lhs, str "=", print_term tyvars (SOME thm) vars NOBR rhs ] end; in Pretty.block_enclose ( Pretty.block [ str "instance ", Pretty.block (print_typcontext tyvars vs), str (class_name class ^ " "), print_typ tyvars BR (tyco `%% map (ITyVar o fst) vs), str " where {" ], str "};" ) (map print_classparam_instance inst_params) end; in print_stmt end; fun haskell_program_of_program ctxt module_prefix module_name reserved identifiers = let fun namify_fun upper base (nsp_fun, nsp_typ) = let val (base', nsp_fun') = Name.variant (Name.enforce_case upper base) nsp_fun; in (base', (nsp_fun', nsp_typ)) end; fun namify_typ base (nsp_fun, nsp_typ) = let val (base', nsp_typ') = Name.variant (Name.enforce_case true base) nsp_typ; in (base', (nsp_fun, nsp_typ')) end; fun namify_stmt (Code_Thingol.Fun (_, SOME _)) = pair | namify_stmt (Code_Thingol.Fun _) = namify_fun false | namify_stmt (Code_Thingol.Datatype _) = namify_typ | namify_stmt (Code_Thingol.Datatypecons _) = namify_fun true | namify_stmt (Code_Thingol.Class _) = namify_typ | namify_stmt (Code_Thingol.Classrel _) = pair | namify_stmt (Code_Thingol.Classparam _) = namify_fun false | namify_stmt (Code_Thingol.Classinst _) = pair; fun select_stmt (Code_Thingol.Fun (_, SOME _)) = false | select_stmt (Code_Thingol.Fun _) = true | select_stmt (Code_Thingol.Datatype _) = true | select_stmt (Code_Thingol.Datatypecons _) = false | select_stmt (Code_Thingol.Class _) = true | select_stmt (Code_Thingol.Classrel _) = false | select_stmt (Code_Thingol.Classparam _) = false | select_stmt (Code_Thingol.Classinst _) = true; in Code_Namespace.flat_program ctxt { module_prefix = module_prefix, module_name = module_name, reserved = reserved, identifiers = identifiers, empty_nsp = (reserved, reserved), namify_stmt = namify_stmt, modify_stmt = fn stmt => if select_stmt stmt then SOME stmt else NONE } end; val prelude_import_operators = [ "==", "/=", "<", "<=", ">=", ">", "+", "-", "*", "/", "**", ">>=", ">>", "=<<", "&&", "||", "^", "^^", ".", "$", "$!", "++", "!!" ]; val prelude_import_unqualified = [ "Eq", "error", "id", "return", "not", "fst", "snd", "map", "filter", "concat", "concatMap", "reverse", "zip", "null", "takeWhile", "dropWhile", "all", "any", "Integer", "negate", "abs", "divMod", "String" ]; val prelude_import_unqualified_constr = [ ("Bool", ["True", "False"]), ("Maybe", ["Nothing", "Just"]) ]; fun serialize_haskell module_prefix string_classes ctxt { module_name, reserved_syms, identifiers, includes, class_syntax, tyco_syntax, const_syntax } program exports = let (* build program *) val reserved = fold (insert (op =) o fst) includes reserved_syms; val { deresolver, flat_program = haskell_program } = haskell_program_of_program ctxt module_prefix module_name (Name.make_context reserved) identifiers exports program; (* print statements *) fun deriving_show tyco = let fun deriv _ "fun" = false | deriv tycos tyco = member (op =) tycos tyco orelse case try (Code_Symbol.Graph.get_node program) (Type_Constructor tyco) of SOME (Code_Thingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos)) (maps snd cs) | NONE => true and deriv' tycos (tyco `%% tys) = deriv tycos tyco andalso forall (deriv' tycos) tys | deriv' _ (ITyVar _) = true in deriv [] tyco end; fun print_stmt deresolve = print_haskell_stmt class_syntax tyco_syntax const_syntax (make_vars reserved) deresolve (if string_classes then deriving_show else K false); (* print modules *) fun module_names module_name = let val (xs, x) = split_last (Long_Name.explode module_name) in xs @ [x ^ ".hs"] end fun print_module_frame module_name header exports ps = (module_names module_name, Pretty.chunks2 ( header @ concat [str "module", case exports of SOME ps => Pretty.block [str module_name, enclose "(" ")" (commas ps)] | NONE => str module_name, str "where {" ] :: ps @| str "}" )); fun print_qualified_import module_name = semicolon [str "import qualified", str module_name]; val import_common_ps = enclose "import Prelude (" ");" (commas (map str (map (Library.enclose "(" ")") prelude_import_operators @ prelude_import_unqualified) @ map (fn (tyco, constrs) => (enclose (tyco ^ "(") ")" o commas o map str) constrs) prelude_import_unqualified_constr)) :: print_qualified_import "Prelude" :: map (print_qualified_import o fst) includes; fun print_module module_name (gr, imports) = let val deresolve = deresolver module_name; val deresolve_import = SOME o str o deresolve; val deresolve_import_attached = SOME o str o suffix "(..)" o deresolve; fun print_import (sym, (_, Code_Thingol.Fun _)) = deresolve_import sym | print_import (sym, (Code_Namespace.Public, Code_Thingol.Datatype _)) = deresolve_import_attached sym | print_import (sym, (Code_Namespace.Opaque, Code_Thingol.Datatype _)) = deresolve_import sym | print_import (sym, (Code_Namespace.Public, Code_Thingol.Class _)) = deresolve_import_attached sym | print_import (sym, (Code_Namespace.Opaque, Code_Thingol.Class _)) = deresolve_import sym | print_import (sym, (_, Code_Thingol.Classinst _)) = NONE; val import_ps = import_common_ps @ map (print_qualified_import o fst) imports; fun print_stmt' sym = case Code_Symbol.Graph.get_node gr sym of (_, NONE) => NONE | (_, SOME (export, stmt)) => SOME (if Code_Namespace.not_private export then print_import (sym, (export, stmt)) else NONE, markup_stmt sym (print_stmt deresolve (sym, stmt))); val (export_ps, body_ps) = (flat o rev o Code_Symbol.Graph.strong_conn) gr |> map_filter print_stmt' |> split_list |> apfst (map_filter I); in print_module_frame module_name [str language_pragma] (SOME export_ps) ((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps) end; in (Code_Target.Hierarchy (map (fn (module_name, content) => ([module_name ^ ".hs"], content)) includes @ map (fn module_name => print_module module_name (Graph.get_node haskell_program module_name)) ((flat o rev o Graph.strong_conn) haskell_program)), try (deresolver "")) end; val serializer : Code_Target.serializer = Code_Target.parse_args (Scan.optional (Args.$$$ "root" -- Args.colon |-- Args.name) "" -- Scan.optional (Args.$$$ "string_classes" >> K true) false >> (fn (module_prefix, string_classes) => serialize_haskell module_prefix string_classes)); fun print_numeral typ = Library.enclose "(" (" :: " ^ typ ^ ")") o signed_string_of_int; val literals = Literals { literal_string = print_haskell_string, literal_numeral = print_numeral "Integer", literal_list = enum "," "[" "]", infix_cons = (5, ":") }; (** optional monad syntax **) fun pretty_haskell_monad c_bind = let fun dest_bind t1 t2 = case Code_Thingol.split_pat_abs t2 of SOME ((pat, ty), t') => SOME ((SOME ((pat, ty), true), t1), t') | NONE => NONE; fun dest_monad (IConst { sym = Constant c, ... } `$ t1 `$ t2) = if c = c_bind then dest_bind t1 t2 else NONE | dest_monad t = case Code_Thingol.split_let_no_pat t of SOME (((some_v, ty), tbind), t') => SOME ((SOME ((IVar some_v, ty), false), tbind), t') | NONE => NONE; val implode_monad = Code_Thingol.unfoldr dest_monad; fun print_monad print_bind print_term (NONE, t) vars = (semicolon [print_term vars NOBR t], vars) | print_monad print_bind print_term (SOME ((bind, _), true), t) vars = vars |> print_bind NOBR bind |>> (fn p => semicolon [p, str "<-", print_term vars NOBR t]) | print_monad print_bind print_term (SOME ((bind, _), false), t) vars = vars |> print_bind NOBR bind |>> (fn p => semicolon [str "let", str "{", p, str "=", print_term vars NOBR t, str "}"]); fun pretty _ print_term thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2 of SOME (bind, t') => let val (binds, t'') = implode_monad t' val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term) (bind :: binds) vars; in brackify_block fxy (str "do { ") (ps @| print_term vars' NOBR t'') (str " }") end | NONE => brackify_infix (1, L) fxy (print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2) in (2, pretty) end; fun add_monad target' raw_c_bind thy = let val c_bind = Code.read_const thy raw_c_bind; in if target = target' then thy |> Code_Target.set_printings (Constant (c_bind, [(target, SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))])) else error "Only Haskell target allows for monad syntax" end; (** Isar setup **) val _ = Theory.setup (Code_Target.add_language (target, {serializer = serializer, literals = literals, check = { env_var = "ISABELLE_GHC", make_destination = I, make_command = fn module_name => "\"$ISABELLE_GHC\" " ^ language_params ^ " -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs"}, evaluation_args = []}) #> 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 (INFX (1, X)) ty1, str "->", print_typ (INFX (1, R)) ty2 )))])) #> fold (Code_Target.add_reserved target) [ "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr", "import", "default", "forall", "let", "in", "class", "qualified", "data", "newtype", "instance", "if", "then", "else", "type", "as", "do", "module" ] #> fold (Code_Target.add_reserved target) prelude_import_unqualified #> fold (Code_Target.add_reserved target o fst) prelude_import_unqualified_constr #> fold (fold (Code_Target.add_reserved target) o snd) prelude_import_unqualified_constr); val _ = Outer_Syntax.command \<^command_keyword>\code_monad\ "define code syntax for monads" (Parse.term -- Parse.name >> (fn (raw_bind, target) => Toplevel.theory (add_monad target raw_bind))); end; (*struct*) 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,911 +1,908 @@ (* 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, 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)) | 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 = dss, dom = dom, ... }, ts)) = if is_constr sym then let val k = length dom in if k < 2 orelse length ts = k 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.eta_expand k 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) dss @ 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 ((fold o Code_Thingol.fold_varnames) - (insert (op =)) 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)) | 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 = dss, dom = dom, ... }, ts)) = if is_constr sym then let val k = length dom in if length ts = k 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.eta_expand k 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) dss @ 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 ((fold o Code_Thingol.fold_varnames) - (insert (op =)) 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 ((fold o Code_Thingol.fold_varnames) - (insert (op =)) 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) = concat [ (str 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 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*), "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_printer.ML b/src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML +++ b/src/Tools/Code/code_printer.ML @@ -1,448 +1,448 @@ (* Title: Tools/Code/code_printer.ML Author: Florian Haftmann, TU Muenchen Generic operations for pretty printing of target language code. *) signature CODE_PRINTER = sig type itype = Code_Thingol.itype type iterm = Code_Thingol.iterm type const = Code_Thingol.const type dict = Code_Thingol.dict val eqn_error: theory -> thm option -> string -> 'a val @@ : 'a * 'a -> 'a list val @| : 'a list * 'a -> 'a list val str: string -> Pretty.T val concat: Pretty.T list -> Pretty.T val brackets: Pretty.T list -> Pretty.T val enclose: string -> string -> Pretty.T list -> Pretty.T val commas: Pretty.T list -> Pretty.T list val enum: string -> string -> string -> Pretty.T list -> Pretty.T val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T val semicolon: Pretty.T list -> Pretty.T val doublesemicolon: Pretty.T list -> Pretty.T val indent: int -> Pretty.T -> Pretty.T val markup_stmt: Code_Symbol.T -> Pretty.T -> Pretty.T val format: Code_Symbol.T list -> int -> Pretty.T -> string type var_ctxt val make_vars: string list -> var_ctxt val intro_vars: string list -> var_ctxt -> var_ctxt val lookup_var: var_ctxt -> string -> string val intro_base_names: (string -> bool) -> (string -> string) -> string list -> var_ctxt -> var_ctxt val intro_base_names_for: (string -> bool) -> (Code_Symbol.T -> string) -> iterm list -> var_ctxt -> var_ctxt val aux_params: var_ctxt -> iterm list list -> string list type literals val Literals: { literal_string: string -> string, literal_numeral: int -> string, literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string } -> literals val literal_string: literals -> string -> string val literal_numeral: literals -> int -> string val literal_list: literals -> Pretty.T list -> Pretty.T val infix_cons: literals -> int * string type lrx val L: lrx val R: lrx val X: lrx type fixity val BR: fixity val NOBR: fixity val INFX: int * lrx -> fixity val APP: fixity val brackify: fixity -> Pretty.T list -> Pretty.T val brackify_infix: int * lrx -> fixity -> Pretty.T * Pretty.T * Pretty.T -> Pretty.T val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T val gen_applify: bool -> string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T val tuplify: (fixity -> 'a -> Pretty.T) -> fixity -> 'a list -> Pretty.T option type raw_const_syntax val plain_const_syntax: string -> raw_const_syntax type simple_const_syntax val simple_const_syntax: simple_const_syntax -> raw_const_syntax type complex_const_syntax val complex_const_syntax: complex_const_syntax -> raw_const_syntax val parse_const_syntax: raw_const_syntax parser val requires_args: raw_const_syntax -> int datatype const_printer = Plain_printer of string | Complex_printer of (var_ctxt -> fixity -> iterm -> Pretty.T) -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T type const_syntax = int * const_printer val prep_const_syntax: theory -> literals -> string -> raw_const_syntax -> const_syntax type tyco_syntax val parse_tyco_syntax: tyco_syntax parser val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list) -> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T) -> (string -> const_syntax option) -> thm option -> var_ctxt -> fixity -> const * iterm list -> Pretty.T val gen_print_bind: (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T) -> thm option -> fixity -> iterm -> var_ctxt -> Pretty.T * var_ctxt type identifiers type printings type data val empty_data: data val map_data: (string list * identifiers * printings -> string list * identifiers * printings) -> data -> data val merge_data: data * data -> data val the_reserved: data -> string list; val the_identifiers: data -> identifiers; val the_printings: data -> printings; end; structure Code_Printer : CODE_PRINTER = struct open Basic_Code_Symbol; open Code_Thingol; (** generic nonsense *) fun eqn_error thy (SOME thm) s = error (s ^ ",\nin equation " ^ Thm.string_of_thm_global thy thm) | eqn_error _ NONE s = error s; val code_presentationN = "code_presentation"; val stmt_nameN = "stmt_name"; val _ = Markup.add_mode code_presentationN YXML.output_markup; (** assembling and printing text pieces **) infixr 5 @@; infixr 5 @|; fun x @@ y = [x, y]; fun xs @| y = xs @ [y]; fun with_no_print_mode f = Print_Mode.setmp [] f; val str = with_no_print_mode Pretty.str; val concat = Pretty.block o Pretty.breaks; val commas = with_no_print_mode Pretty.commas; fun enclose l r = with_no_print_mode (Pretty.enclose l r); val brackets = enclose "(" ")" o Pretty.breaks; fun enum sep l r = with_no_print_mode (Pretty.enum sep l r); fun enum_default default sep l r [] = str default | enum_default default sep l r xs = enum sep l r xs; fun semicolon ps = Pretty.block [concat ps, str ";"]; fun doublesemicolon ps = Pretty.block [concat ps, str ";;"]; fun indent i = with_no_print_mode (Pretty.indent i); fun with_presentation_marker f = Print_Mode.setmp [code_presentationN] f; fun markup_stmt sym = with_presentation_marker (Pretty.mark (code_presentationN, [(stmt_nameN, Code_Symbol.marker sym)])); fun filter_presentation [] xml = Buffer.build (fold XML.add_content xml) | filter_presentation presentation_syms xml = let val presentation_idents = map Code_Symbol.marker presentation_syms fun is_selected (name, attrs) = name = code_presentationN andalso member (op =) presentation_idents (the (Properties.get attrs stmt_nameN)); fun add_content_with_space tree (is_first, buf) = buf |> not is_first ? Buffer.add "\n\n" |> XML.add_content tree |> pair false; fun filter (XML.Elem (name_attrs, xs)) = fold (if is_selected name_attrs then add_content_with_space else filter) xs | filter (XML.Text _) = I; in snd (fold filter xml (true, Buffer.empty)) end; fun format presentation_names width = with_presentation_marker (Pretty.string_of_margin width) #> YXML.parse_body #> filter_presentation presentation_names #> Buffer.add "\n" #> Buffer.content; (** names and variable name contexts **) type var_ctxt = string Symtab.table * Name.context; fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty, Name.make_context names); fun intro_vars names (namemap, namectxt) = let val (names', namectxt') = fold_map Name.variant names namectxt; val namemap' = fold2 (curry Symtab.update) names names' namemap; in (namemap', namectxt') end; fun lookup_var (namemap, _) name = case Symtab.lookup namemap name of SOME name' => name' | NONE => error ("Invalid name in context: " ^ quote name); fun aux_params vars lhss = let fun fish_param _ (w as SOME _) = w | fish_param (IVar (SOME v)) NONE = SOME v | fish_param _ NONE = NONE; fun fillup_param _ (_, SOME v) = v | fillup_param x (i, NONE) = x ^ string_of_int i; val fished1 = fold (map2 fish_param) lhss (replicate (length (hd lhss)) NONE); val x = singleton (Name.variant_list (map_filter I fished1)) "x"; val fished2 = map_index (fillup_param x) fished1; val (fished3, _) = fold_map Name.variant fished2 Name.context; val vars' = intro_vars fished3 vars; in map (lookup_var vars') fished3 end; fun intro_base_names no_syntax deresolve = map_filter (fn name => if no_syntax name then let val name' = deresolve name in if Long_Name.is_qualified name' then NONE else SOME name' end else NONE) #> intro_vars; fun intro_base_names_for no_syntax deresolve ts = [] |> fold Code_Thingol.add_constsyms ts |> intro_base_names (fn Constant const => no_syntax const | _ => true) deresolve; (** pretty literals **) datatype literals = Literals of { literal_string: string -> string, literal_numeral: int -> string, literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string }; fun dest_Literals (Literals lits) = lits; val literal_string = #literal_string o dest_Literals; val literal_numeral = #literal_numeral o dest_Literals; val literal_list = #literal_list o dest_Literals; val infix_cons = #infix_cons o dest_Literals; (** syntax printer **) (* binding priorities *) datatype lrx = L | R | X; datatype fixity = BR | NOBR | INFX of (int * lrx); val APP = INFX (~1, L); fun fixity_lrx L L = false | fixity_lrx R R = false | fixity_lrx _ _ = true; fun fixity NOBR _ = false | fixity _ NOBR = false | fixity (INFX (pr, lr)) (INFX (pr_ctxt, lr_ctxt)) = pr < pr_ctxt orelse pr = pr_ctxt andalso fixity_lrx lr lr_ctxt orelse pr_ctxt = ~1 | fixity BR (INFX _) = false | fixity _ _ = true; fun gen_brackify _ [p] = p | gen_brackify true (ps as _::_) = enclose "(" ")" ps | gen_brackify false (ps as _::_) = Pretty.block ps; fun brackify fxy_ctxt = gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks; fun brackify_infix infx fxy_ctxt (l, m, r) = gen_brackify (fixity (INFX infx) fxy_ctxt) [l, str " ", m, Pretty.brk 1, r]; fun brackify_block fxy_ctxt p1 ps p2 = let val p = Pretty.block_enclose (p1, p2) ps in if fixity BR fxy_ctxt then enclose "(" ")" [p] else p end; fun gen_applify strict opn cls f fxy_ctxt p [] = if strict then gen_brackify (fixity BR fxy_ctxt) [p, str (opn ^ cls)] else p | gen_applify strict opn cls f fxy_ctxt p ps = gen_brackify (fixity BR fxy_ctxt) (p @@ enum "," opn cls (map f ps)); fun applify opn = gen_applify false opn; fun tuplify _ _ [] = NONE | tuplify print fxy [x] = SOME (print fxy x) | tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs)); (* generic syntax *) type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T) -> fixity -> (iterm * itype) list -> Pretty.T); type complex_const_syntax = int * (literals -> (var_ctxt -> fixity -> iterm -> Pretty.T) -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T); datatype raw_const_syntax = plain_const_syntax of string | complex_const_syntax of complex_const_syntax; fun simple_const_syntax syn = complex_const_syntax (apsnd (fn f => fn _ => fn print => fn _ => fn vars => f (print vars)) syn); fun requires_args (plain_const_syntax _) = 0 | requires_args (complex_const_syntax (k, _)) = k; datatype const_printer = Plain_printer of string | Complex_printer of (var_ctxt -> fixity -> iterm -> Pretty.T) -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T; type const_syntax = int * const_printer; fun prep_const_syntax thy literals c (plain_const_syntax s) = (Code.args_number thy c, Plain_printer s) | prep_const_syntax thy literals c (complex_const_syntax (n, f))= (n, Complex_printer (f literals)); fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy (app as ({ sym, dom, ... }, ts)) = case sym of Constant const => (case const_syntax const of NONE => brackify fxy (print_app_expr some_thm vars app) | SOME (_, Plain_printer s) => brackify fxy (str s :: map (print_term some_thm vars BR) ts) | SOME (k, Complex_printer print) => let fun print' fxy ts = print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom); in if k = length ts then print' fxy ts else if k < length ts then case chop k ts of (ts1, ts2) => brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2) else print_term some_thm vars fxy (Code_Thingol.eta_expand k app) end) | _ => brackify fxy (print_app_expr some_thm vars app); fun gen_print_bind print_term thm (fxy : fixity) pat vars = let - val vs = build (Code_Thingol.fold_varnames (insert (op =)) pat); + val vs = build (Code_Thingol.add_varnames pat); val vars' = intro_vars vs vars; in (print_term thm vars' fxy pat, vars') end; type tyco_syntax = int * ((fixity -> itype -> Pretty.T) -> fixity -> itype list -> Pretty.T); (* mixfix syntax *) datatype 'a mixfix = Arg of fixity | String of string | Break; fun printer_of_mixfix prep_arg (fixity_this, mfx) = let fun is_arg (Arg _) = true | is_arg _ = false; val i = (length o filter is_arg) mfx; fun fillin _ [] [] = [] | fillin print (Arg fxy :: mfx) (a :: args) = (print fxy o prep_arg) a :: fillin print mfx args | fillin print (String s :: mfx) args = str s :: fillin print mfx args | fillin print (Break :: mfx) args = Pretty.brk 1 :: fillin print mfx args; in (i, fn print => fn fixity_ctxt => fn args => gen_brackify (fixity fixity_this fixity_ctxt) (fillin print mfx args)) end; fun read_infix (fixity_this, i) s = let val l = case fixity_this of L => INFX (i, L) | _ => INFX (i, X); val r = case fixity_this of R => INFX (i, R) | _ => INFX (i, X); in (INFX (i, fixity_this), [Arg l, String " ", String s, Break, Arg r]) end; fun read_mixfix s = let val sym_any = Scan.one Symbol.not_eof; val parse = Scan.optional ($$ "!" >> K NOBR) BR -- Scan.repeat ( ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR)) || ($$ "_" >> K (Arg BR)) || ($$ "/" |-- Scan.repeat ($$ " ") >> (K Break)) || (Scan.repeat1 ( $$ "'" |-- sym_any || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")") sym_any) >> (String o implode))); fun err s (_, NONE) = (fn () => "malformed mixfix annotation: " ^ quote s) | err _ (_, SOME msg) = msg; in case Scan.finite Symbol.stopper parse (Symbol.explode s) of (fixity_mixfix, []) => fixity_mixfix | _ => Scan.!! (err s) Scan.fail () end; val parse_fixity = (\<^keyword>\infix\ >> K X) || (\<^keyword>\infixl\ >> K L) || (\<^keyword>\infixr\ >> K R) fun parse_mixfix x = (Parse.string >> read_mixfix || parse_fixity -- Parse.nat -- Parse.string >> (fn ((fixity, i), s) => read_infix (fixity, i) s)) x; fun syntax_of_mixfix of_plain of_printer prep_arg (BR, [String s]) = of_plain s | syntax_of_mixfix of_plain of_printer prep_arg (fixity, mfx) = of_printer (printer_of_mixfix prep_arg (fixity, mfx)); fun parse_tyco_syntax x = (parse_mixfix >> syntax_of_mixfix (fn s => (0, (K o K o K o str) s)) I I) x; val parse_const_syntax = parse_mixfix >> syntax_of_mixfix plain_const_syntax simple_const_syntax fst; (** custom data structure **) type identifiers = (string list * string, string list * string, string list * string, string list * string, string list * string, string list * string) Code_Symbol.data; type printings = (const_syntax, tyco_syntax, string, unit, unit, (Pretty.T * Code_Symbol.T list)) Code_Symbol.data; datatype data = Data of { reserved: string list, identifiers: identifiers, printings: printings }; fun make_data (reserved, identifiers, printings) = Data { reserved = reserved, identifiers = identifiers, printings = printings }; val empty_data = make_data ([], Code_Symbol.empty_data, Code_Symbol.empty_data); fun map_data f (Data { reserved, identifiers, printings }) = make_data (f (reserved, identifiers, printings)); fun merge_data (Data { reserved = reserved1, identifiers = identifiers1, printings = printings1 }, Data { reserved = reserved2, identifiers = identifiers2, printings = printings2 }) = make_data (merge (op =) (reserved1, reserved2), Code_Symbol.merge_data (identifiers1, identifiers2), Code_Symbol.merge_data (printings1, printings2)); fun the_reserved (Data { reserved, ... }) = reserved; fun the_identifiers (Data { identifiers , ... }) = identifiers; fun the_printings (Data { printings, ... }) = printings; end; (*struct*) diff --git a/src/Tools/Code/code_scala.ML b/src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML +++ b/src/Tools/Code/code_scala.ML @@ -1,490 +1,490 @@ (* Title: Tools/Code/code_scala.ML Author: Florian Haftmann, TU Muenchen Serializer for Scala. *) signature CODE_SCALA = sig val target: string end; structure Code_Scala : CODE_SCALA = struct open Basic_Code_Symbol; open Basic_Code_Thingol; open Code_Printer; infixr 5 @@; infixr 5 @|; (** Scala serializer **) val target = "Scala"; val print_scala_string = let fun chr i = "\\u" ^ align_right "0" 4 (Int.fmt StringCvt.HEX i) fun char c = if c = "'" then "\\'" else if c = "\"" then "\\\"" else if c = "\\" then "\\\\" else let val i = ord c in if i < 32 orelse i > 126 then chr i else if i >= 128 then error "non-ASCII byte in Scala string literal" else c end in quote o translate_string char end; datatype scala_stmt = Fun of typscheme * ((iterm list * iterm) * (thm option * bool)) list | Datatype of vname list * ((string * vname list) * itype list) list | Class of (vname * ((class * class) list * (string * itype) list)) * (string * { vs: (vname * sort) list, inst_params: ((string * (const * int)) * (thm * bool)) list, superinst_params: ((string * (const * int)) * (thm * bool)) list }) list; fun print_scala_stmt tyco_syntax const_syntax reserved args_num is_constr (deresolve, deresolve_full) = let val deresolve_const = deresolve o Constant; val deresolve_tyco = deresolve o Type_Constructor; val deresolve_class = deresolve o Type_Class; fun lookup_tyvar tyvars = lookup_var tyvars o Name.enforce_case true; fun intro_tyvars vs = intro_vars (map (Name.enforce_case true o fst) vs); fun print_tyco_expr tyvars fxy (sym, tys) = applify "[" "]" (print_typ tyvars NOBR) fxy ((str o deresolve) sym) tys and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco of NONE => print_tyco_expr tyvars fxy (Type_Constructor tyco, tys) | SOME (_, print) => print (print_typ tyvars) fxy tys) | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v; fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (Type_Class class, [ty]); fun print_tupled_typ tyvars ([], ty) = print_typ tyvars NOBR ty | print_tupled_typ tyvars ([ty1], ty2) = concat [print_typ tyvars BR ty1, str "=>", print_typ tyvars NOBR ty2] | print_tupled_typ tyvars (tys, ty) = concat [enum "," "(" ")" (map (print_typ tyvars NOBR) tys), str "=>", print_typ tyvars NOBR ty]; fun constraint p1 p2 = Pretty.block [p1, str ":", Pretty.brk 1, p2]; fun print_var vars NONE = str "_" | print_var vars (SOME v) = (str o lookup_var vars) v; fun applify_dict tyvars (Dict (_, d)) = applify_plain_dict tyvars d and applify_plain_dict tyvars (Dict_Const (inst, dss)) = applify_dictss tyvars ((str o deresolve o Class_Instance) inst) dss | applify_plain_dict tyvars (Dict_Var { var, class, ... }) = Pretty.block [str "implicitly", enclose "[" "]" [Pretty.block [(str o deresolve_class) class, enclose "[" "]" [(str o lookup_tyvar tyvars) var]]]] and applify_dictss tyvars p dss = applify "(" ")" (applify_dict tyvars) NOBR p (flat dss) fun print_term tyvars is_pat some_thm vars fxy (IConst const) = print_app tyvars is_pat some_thm vars fxy (const, []) | print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) = (case Code_Thingol.unfold_const_app t of SOME app => print_app tyvars is_pat some_thm vars fxy app | _ => applify "(" ")" (print_term tyvars is_pat some_thm vars NOBR) fxy (print_term tyvars is_pat some_thm vars BR t1) [t2]) | print_term tyvars is_pat some_thm vars fxy (IVar v) = print_var vars v | print_term tyvars is_pat some_thm vars fxy (t as _ `|=> _) = let val (vs_tys, body) = Code_Thingol.unfold_abs t; val (ps, vars') = fold_map (print_abs_head tyvars) vs_tys vars; in brackets (ps @| print_term tyvars false some_thm vars' NOBR body) end | print_term tyvars is_pat some_thm vars fxy (ICase case_expr) = (case Code_Thingol.unfold_const_app (#primitive case_expr) of SOME (app as ({ sym = Constant const, ... }, _)) => if is_none (const_syntax const) then print_case tyvars some_thm vars fxy case_expr else print_app tyvars is_pat some_thm vars fxy app | NONE => print_case tyvars some_thm vars fxy case_expr) and print_abs_head tyvars (some_v, ty) vars = let val vars' = intro_vars (the_list some_v) vars; in (concat [ enclose "(" ")" [constraint (print_var vars' some_v) (print_typ tyvars NOBR ty)], str "=>" ], vars') end and print_app tyvars is_pat some_thm vars fxy (app as ({ sym, typargs, dom, dicts, ... }, ts)) = let val k = length ts; val typargs' = if is_pat then [] else typargs; val syntax = case sym of Constant const => const_syntax const | _ => NONE; val applify_dicts = if is_pat orelse is_some syntax orelse is_constr sym orelse Code_Thingol.unambiguous_dictss dicts then fn p => K p else applify_dictss tyvars; val (l, print') = case syntax of NONE => (args_num sym, fn fxy => fn ts => applify_dicts (gen_applify (is_constr sym) "(" ")" (print_term tyvars is_pat some_thm vars NOBR) fxy (applify "[" "]" (print_typ tyvars NOBR) NOBR ((str o deresolve) sym) typargs') ts) dicts) | SOME (k, Plain_printer s) => (k, fn fxy => fn ts => applify_dicts (applify "(" ")" (print_term tyvars is_pat some_thm vars NOBR) fxy (applify "[" "]" (print_typ tyvars NOBR) NOBR (str s) typargs') ts) dicts) | SOME (k, Complex_printer print) => (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy (ts ~~ take k dom)) in if k = l then print' fxy ts else if k < l then print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app) else let val (ts1, ts23) = chop l ts; in Pretty.block (print' BR ts1 :: map (fn t => Pretty.block [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts23) end end and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars true) some_thm fxy p and print_case tyvars some_thm vars fxy { clauses = [], ... } = (brackify fxy o Pretty.breaks o map str) ["sys.error(\"empty case\")"] | print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) = let val (bind :: binds, body) = Code_Thingol.unfold_let (ICase case_expr); fun print_match_val ((pat, ty), t) vars = vars |> print_bind tyvars some_thm BR pat |>> (fn p => (false, concat [str "val", constraint p (print_typ tyvars NOBR ty), str "=", print_term tyvars false some_thm vars NOBR t])); fun print_match_seq t vars = ((true, print_term tyvars false some_thm vars NOBR t), vars); fun print_match is_first ((IVar NONE, ty), t) = if Code_Thingol.is_IAbs t andalso is_first then print_match_val ((IVar NONE, ty), t) else print_match_seq t | print_match _ ((pat, ty), t) = print_match_val ((pat, ty), t); val (seps_ps, vars') = vars |> print_match true bind ||>> fold_map (print_match false) binds |>> uncurry cons; val all_seps_ps = seps_ps @ [(true, print_term tyvars false some_thm vars' NOBR body)]; fun insert_seps [(_, p)] = [p] | insert_seps ((_, p) :: (seps_ps as (sep, _) :: _)) = (if sep then Pretty.block [p, str ";"] else p) :: insert_seps seps_ps in brackify_block fxy (str "{") (insert_seps all_seps_ps) (str "}") end | print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } = let fun print_select (pat, body) = let val (p_pat, vars') = print_bind tyvars some_thm NOBR pat vars; val p_body = print_term tyvars false some_thm vars' NOBR body in concat [str "case", p_pat, str "=>", p_body] end; in map print_select clauses |> Pretty.block_enclose (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"], str "}") |> single |> enclose "(" ")" end; fun print_context tyvars vs s = applify "[" "]" (fn (v, sort) => (Pretty.block o map str) (lookup_tyvar tyvars v :: maps (fn class => [" : ", deresolve_class class]) sort)) NOBR (str s) vs; fun print_defhead tyvars vars const vs params tys ty = concat [str "def", constraint (applify "(" ")" (fn (param, ty) => constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty)) NOBR (print_context tyvars vs (deresolve_const const)) (params ~~ tys)) (print_typ tyvars NOBR ty), str "="]; fun print_def const (vs, ty) [] = let val (tys, ty') = Code_Thingol.unfold_fun ty; val params = Name.invent (snd reserved) "a" (length tys); val tyvars = intro_tyvars vs reserved; val vars = intro_vars params reserved; in concat [print_defhead tyvars vars const vs params tys ty', str ("sys.error(" ^ print_scala_string const ^ ")")] end | print_def const (vs, ty) eqs = let val tycos = build (fold (fn ((ts, t), _) => fold Code_Thingol.add_tyconames (t :: ts)) eqs); val tyvars = reserved |> intro_base_names (is_none o tyco_syntax) deresolve_tyco tycos |> intro_tyvars vs; val simple = case eqs of [((ts, _), _)] => forall Code_Thingol.is_IVar ts | _ => false; val vars1 = reserved |> intro_base_names_for (is_none o const_syntax) deresolve (map (snd o fst) eqs); val params = if simple then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs else aux_params vars1 (map (fst o fst) eqs); val vars2 = intro_vars params vars1; val (tys', ty') = Code_Thingol.unfold_fun_n (length params) ty; fun tuplify [p] = p | tuplify ps = enum "," "(" ")" ps; fun print_rhs vars' ((_, t), (some_thm, _)) = print_term tyvars false some_thm vars' NOBR t; fun print_clause (eq as ((ts, _), (some_thm, _))) = let - val vars' = intro_vars ((fold o Code_Thingol.fold_varnames) - (insert (op =)) ts []) vars1; + 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", "extends", "false", "final", "finally", "for", "forSome", "if", "implicit", "import", "lazy", "match", "new", "null", "object", "override", "package", "private", "protected", "requires", "return", "sealed", "super", "this", "throw", "trait", "try", "true", "type", "val", "var", "while", "with", "yield" ] #> fold (Code_Target.add_reserved target) [ "apply", "sys", "scala", "BigInt", "Nil", "List" ]); end; (*struct*) diff --git a/src/Tools/Code/code_thingol.ML b/src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML +++ b/src/Tools/Code/code_thingol.ML @@ -1,1060 +1,1065 @@ (* Title: Tools/Code/code_thingol.ML Author: Florian Haftmann, TU Muenchen Intermediate language ("Thin-gol") representing executable code. Representation and translation. *) infix 8 `%%; infix 4 `$; infix 4 `$$; infixr 3 `->; infixr 3 `|=>; infixr 3 `|==>; signature BASIC_CODE_THINGOL = sig type vname = string; datatype dict = Dict of (class * class) list * plain_dict and plain_dict = Dict_Const of (string * class) * dict list list | Dict_Var of { var: vname, index: int, length: int, class: class, unique: bool }; datatype itype = `%% of string * itype list | ITyVar of vname; type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list, dom: itype list, annotation: itype option }; datatype iterm = IConst of const | IVar of vname option | `$ of iterm * iterm | `|=> of (vname option * itype) * iterm | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm }; val `-> : itype * itype -> itype; val `$$ : iterm * iterm list -> iterm; val `|==> : (vname option * itype) list * iterm -> iterm; type typscheme = (vname * sort) list * itype; end; signature CODE_THINGOL = sig include BASIC_CODE_THINGOL val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a val unfold_fun: itype -> itype list * itype val unfold_fun_n: int -> itype -> itype list * itype val unfold_app: iterm -> iterm * iterm list val unfold_abs: iterm -> (vname option * itype) list * iterm val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option val split_let_no_pat: iterm -> (((string option * itype) * iterm) * iterm) option val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm val unfold_let_no_pat: iterm -> ((string option * itype) * iterm) list * iterm val split_pat_abs: iterm -> ((iterm * itype) * iterm) option val unfold_pat_abs: iterm -> (iterm * itype) list * iterm val unfold_const_app: iterm -> (const * iterm list) option val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm val is_IVar: iterm -> bool val is_IAbs: iterm -> bool val eta_expand: int -> const * iterm list -> iterm val contains_dict_var: iterm -> bool val unambiguous_dictss: dict list list -> bool val add_constsyms: iterm -> Code_Symbol.T list -> Code_Symbol.T list val add_tyconames: iterm -> string list -> string list val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a + 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, inst_params: ((string * (const * int)) * (thm * bool)) list, superinst_params: ((string * (const * int)) * (thm * bool)) list }; type program = stmt Code_Symbol.Graph.T val unimplemented: program -> string list val implemented_deps: program -> string list val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt val is_constr: program -> Code_Symbol.T -> bool val is_case: stmt -> bool val group_stmts: Proof.context -> program -> ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list * ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list)) list val read_const_exprs: Proof.context -> string list -> string list val consts_program: Proof.context -> string list -> program val dynamic_conv: Proof.context -> (program -> typscheme * iterm -> Code_Symbol.T list -> conv) -> conv val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> (program -> term -> typscheme * iterm -> Code_Symbol.T list -> 'a) -> term -> 'a val static_conv_thingol: { ctxt: Proof.context, consts: string list } -> ({ program: program, deps: string list } -> Proof.context -> typscheme * iterm -> Code_Symbol.T list -> conv) -> Proof.context -> conv val static_conv_isa: { ctxt: Proof.context, consts: string list } -> (program -> Proof.context -> term -> conv) -> Proof.context -> conv val static_value: { ctxt: Proof.context, lift_postproc: ((term -> term) -> 'a -> 'a), consts: string list } -> ({ program: program, deps: string list } -> Proof.context -> term -> typscheme * iterm -> Code_Symbol.T list -> 'a) -> Proof.context -> term -> 'a end; structure Code_Thingol : CODE_THINGOL = struct open Basic_Code_Symbol; (** auxiliary **) fun unfoldl dest x = case dest x of NONE => (x, []) | SOME (x1, x2) => let val (x', xs') = unfoldl dest x1 in (x', xs' @ [x2]) end; fun unfoldr dest x = case dest x of NONE => ([], x) | SOME (x1, x2) => let val (xs', x') = unfoldr dest x2 in (x1 :: xs', x') end; (** language core - types, terms **) type vname = string; datatype dict = Dict of (class * class) list * plain_dict and plain_dict = Dict_Const of (string * class) * dict list list | Dict_Var of { var: vname, index: int, length: int, class: class, unique: bool }; datatype itype = `%% of string * itype list | ITyVar of vname; fun ty1 `-> ty2 = "fun" `%% [ty1, ty2]; val unfold_fun = unfoldr (fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2) | _ => NONE); fun unfold_fun_n n ty = let val (tys1, ty1) = unfold_fun ty; val (tys3, tys2) = chop n tys1; val ty3 = Library.foldr (op `->) (tys2, ty1); in (tys3, ty3) end; type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list, dom: itype list, annotation: itype option }; datatype iterm = IConst of const | IVar of vname option | `$ of iterm * iterm | `|=> of (vname option * itype) * iterm | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm }; (*see also signature*) fun is_IVar (IVar _) = true | is_IVar _ = false; fun is_IAbs (_ `|=> _) = true | is_IAbs _ = false; val op `$$ = Library.foldl (op `$); val op `|==> = Library.foldr (op `|=>); val unfold_app = unfoldl (fn op `$ t => SOME t | _ => NONE); val unfold_abs = unfoldr (fn op `|=> t => SOME t | _ => NONE); val split_let = (fn ICase { term = t, typ = ty, clauses = [(p, body)], ... } => SOME (((p, ty), t), body) | _ => NONE); val split_let_no_pat = (fn ICase { term = t, typ = ty, clauses = [(IVar v, body)], ... } => SOME (((v, ty), t), body) | _ => NONE); val unfold_let = unfoldr split_let; val unfold_let_no_pat = unfoldr split_let_no_pat; fun unfold_const_app t = case unfold_app t of (IConst c, ts) => SOME (c, ts) | _ => NONE; fun fold_constexprs f = let fun fold' (IConst c) = f c | fold' (IVar _) = I | fold' (t1 `$ t2) = fold' t1 #> fold' t2 | fold' (_ `|=> t) = fold' t | fold' (ICase { term = t, clauses = clauses, ... }) = fold' t #> fold (fn (p, body) => fold' p #> fold' body) clauses in fold' end; val add_constsyms = fold_constexprs (fn { sym, ... } => insert (op =) sym); fun add_tycos (tyco `%% tys) = insert (op =) tyco #> fold add_tycos tys | add_tycos (ITyVar _) = I; val add_tyconames = fold_constexprs (fn { typargs = tys, ... } => fold add_tycos tys); fun fold_varnames f = let fun fold_aux add_vars f = let fun fold_term _ (IConst _) = I | fold_term vs (IVar (SOME v)) = if member (op =) vs v then I else f v | fold_term _ (IVar NONE) = I | fold_term vs (t1 `$ t2) = fold_term vs t1 #> fold_term vs t2 | fold_term vs ((SOME v, _) `|=> t) = fold_term (insert (op =) v vs) t | fold_term vs ((NONE, _) `|=> t) = fold_term vs t | fold_term vs (ICase { term = t, clauses = clauses, ... }) = fold_term vs t #> fold (fold_clause vs) clauses and fold_clause vs (p, t) = fold_term (add_vars p vs) t; in fold_term [] end fun add_vars t = fold_aux add_vars (insert (op =)) t; in fold_aux add_vars f end; +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 split_pat_abs ((NONE, ty) `|=> t) = SOME ((IVar NONE, ty), t) | split_pat_abs ((SOME v, ty) `|=> t) = SOME (case t of ICase { term = IVar (SOME w), clauses = [(p, body)], ... } => if v = w andalso (exists_var p v orelse not (exists_var body v)) then ((p, ty), body) else ((IVar (SOME v), ty), t) | _ => ((IVar (SOME v), ty), t)) | split_pat_abs _ = NONE; val unfold_pat_abs = unfoldr split_pat_abs; fun unfold_abs_eta [] t = ([], t) | unfold_abs_eta (_ :: tys) (v_ty `|=> t) = let val (vs_tys, t') = unfold_abs_eta tys t; in (v_ty :: vs_tys, t') end | unfold_abs_eta tys t = let - val ctxt = fold_varnames Name.declare t Name.context; + val ctxt = Name.build_context (declare_varnames t); val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys); in (vs_tys, t `$$ map (IVar o fst) vs_tys) end; fun eta_expand k (const as { dom = tys, ... }, ts) = let val j = length ts; val l = k - j; val _ = if l > length tys then error "Impossible eta-expansion" else (); - val vars = (fold o fold_varnames) Name.declare ts Name.context; + val vars = Name.build_context (fold declare_varnames ts); val vs_tys = (map o apfst) SOME (Name.invent_names vars "a" ((take l o drop j) tys)); in vs_tys `|==> IConst const `$$ ts @ map (IVar o fst) vs_tys end; fun map_terms_bottom_up f (t as IConst _) = f t | map_terms_bottom_up f (t as IVar _) = f t | map_terms_bottom_up f (t1 `$ t2) = f (map_terms_bottom_up f t1 `$ map_terms_bottom_up f t2) | map_terms_bottom_up f ((v, ty) `|=> t) = f ((v, ty) `|=> map_terms_bottom_up f t) | map_terms_bottom_up f (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) = f (ICase { term = map_terms_bottom_up f t, typ = ty, clauses = (map o apply2) (map_terms_bottom_up f) clauses, primitive = map_terms_bottom_up f t0 }); fun distill_minimized_clause ctxt tys t = let fun distill vs_map pat_args (body as IConst { sym = Constant c, ... }) = if Code.is_undefined (Proof_Context.theory_of ctxt) c then [] else [(pat_args, body)] | distill vs_map pat_args (body as ICase { term = IVar (SOME v), clauses = clauses, ... }) = let - val vs = build ((fold o fold_varnames) (insert (op =)) pat_args); + val vs = build (fold add_varnames pat_args); fun varnames_disjunctive pat = - null (inter (op =) vs (build (fold_varnames (insert (op =)) pat))); + null (inter (op =) vs (build (add_varnames pat))); fun purge_unused_vars_in t = let - val vs = build (fold_varnames (insert (op =)) t); + val vs = build (add_varnames t); in map_terms_bottom_up (fn IVar (SOME v) => IVar (if member (op =) vs v then SOME v else NONE) | t => t) end; in if forall (fn (pat', body') => exists_var pat' v orelse not (exists_var body' v)) clauses andalso forall (varnames_disjunctive o fst) clauses then case AList.lookup (op =) vs_map v of SOME i => clauses |> maps (fn (pat', body') => distill (AList.delete (op =) v vs_map) (nth_map i (K pat') pat_args |> map (purge_unused_vars_in body')) body') | NONE => [(pat_args, body)] else [(pat_args, body)] end | 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); val pat_args = map (IVar o fst) vs; in distill vs_map pat_args 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 | exists_plain_dict_var_pred f (Dict_Var x) = f x and exists_dictss_var f dss = (exists o exists) (exists_dict_var f) dss; fun contains_dict_var (IConst { dicts = dss, ... }) = exists_dictss_var (K true) dss | contains_dict_var (IVar _) = false | contains_dict_var (t1 `$ t2) = contains_dict_var t1 orelse contains_dict_var t2 | contains_dict_var (_ `|=> t) = contains_dict_var t | contains_dict_var (ICase { primitive = t, ... }) = contains_dict_var t; val unambiguous_dictss = not o exists_dictss_var (fn { unique, ... } => not unique); (** statements, abstract programs **) type typscheme = (vname * sort) list * itype; datatype stmt = NoStmt | Fun of (typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option | Datatype of vname list * ((string * vname list) * itype list) list | Datatypecons of string | Class of vname * ((class * class) list * (string * itype) list) | Classrel of class * class | Classparam of class | Classinst of { class: string, tyco: string, vs: (vname * sort) list, superinsts: (class * dict list list) list, inst_params: ((string * (const * int)) * (thm * bool)) list, superinst_params: ((string * (const * int)) * (thm * bool)) list }; type program = stmt Code_Symbol.Graph.T; val unimplemented = build o Code_Symbol.Graph.fold (fn (Constant c, (NoStmt, _)) => cons c | _ => I); fun implemented_deps program = Code_Symbol.Graph.keys program |> subtract (op =) (Code_Symbol.Graph.all_preds program (map Constant (unimplemented program))) |> map_filter (fn Constant c => SOME c | _ => NONE); fun map_classparam_instances_as_term f = (map o apfst o apsnd o apfst) (fn const => case f (IConst const) of IConst const' => const') fun map_terms_stmt f NoStmt = NoStmt | map_terms_stmt f (Fun ((tysm, eqs), case_cong)) = Fun ((tysm, (map o apfst) (fn (ts, t) => (map f ts, f t)) eqs), case_cong) | map_terms_stmt f (stmt as Datatype _) = stmt | map_terms_stmt f (stmt as Datatypecons _) = stmt | map_terms_stmt f (stmt as Class _) = stmt | map_terms_stmt f (stmt as Classrel _) = stmt | map_terms_stmt f (stmt as Classparam _) = stmt | map_terms_stmt f (Classinst { class, tyco, vs, superinsts, inst_params, superinst_params }) = Classinst { class = class, tyco = tyco, vs = vs, superinsts = superinsts, inst_params = map_classparam_instances_as_term f inst_params, superinst_params = map_classparam_instances_as_term f superinst_params }; fun is_constr program sym = case Code_Symbol.Graph.get_node program sym of Datatypecons _ => true | _ => false; fun is_case (Fun (_, SOME _)) = true | is_case _ = false; fun linear_stmts program = rev (Code_Symbol.Graph.strong_conn program) |> map (AList.make (Code_Symbol.Graph.get_node program)); fun group_stmts ctxt program = let fun is_fun (_, Fun _) = true | is_fun _ = false; fun is_datatypecons (_, Datatypecons _) = true | is_datatypecons _ = false; fun is_datatype (_, Datatype _) = true | is_datatype _ = false; fun is_class (_, Class _) = true | is_class _ = false; fun is_classrel (_, Classrel _) = true | is_classrel _ = false; fun is_classparam (_, Classparam _) = true | is_classparam _ = false; fun is_classinst (_, Classinst _) = true | is_classinst _ = false; fun group stmts = if forall (is_datatypecons orf is_datatype) stmts then (filter is_datatype stmts, [], ([], [])) else if forall (is_class orf is_classrel orf is_classparam) stmts then ([], filter is_class stmts, ([], [])) else if forall (is_fun orf is_classinst) stmts then ([], [], List.partition is_fun stmts) else error ("Illegal mutual dependencies: " ^ (commas o map (Code_Symbol.quote ctxt o fst)) stmts); in linear_stmts program |> map group end; (** translation kernel **) (* generic mechanisms *) fun ensure_stmt symbolize generate x (deps, program) = let val sym = symbolize x; val add_dep = case deps of [] => I | dep :: _ => Code_Symbol.Graph.add_edge (dep, sym); in if can (Code_Symbol.Graph.get_node program) sym then program |> add_dep |> pair deps |> pair x else program |> Code_Symbol.Graph.default_node (sym, NoStmt) |> add_dep |> curry generate (sym :: deps) ||> snd |-> (fn stmt => (Code_Symbol.Graph.map_node sym) (K stmt)) |> pair deps |> pair x end; exception PERMISSIVE of unit; fun translation_error ctxt permissive some_thm deps msg sub_msg = if permissive then raise PERMISSIVE () else let val thm_msg = Option.map (fn thm => "in code equation " ^ Thm.string_of_thm ctxt thm) some_thm; val dep_msg = if null (tl deps) then NONE else SOME ("with dependency " ^ space_implode " -> " (map (Code_Symbol.quote ctxt) (rev deps))); val thm_dep_msg = case (thm_msg, dep_msg) of (SOME thm_msg, SOME dep_msg) => "\n(" ^ thm_msg ^ ",\n" ^ dep_msg ^ ")" | (SOME thm_msg, NONE) => "\n(" ^ thm_msg ^ ")" | (NONE, SOME dep_msg) => "\n(" ^ dep_msg ^ ")" | (NONE, NONE) => "" in error (msg ^ thm_dep_msg ^ ":\n" ^ sub_msg) end; fun maybe_permissive f prgrm = f prgrm |>> SOME handle PERMISSIVE () => (NONE, prgrm); fun not_wellsorted ctxt permissive some_thm deps ty sort e = let val err_class = Sorts.class_error (Context.Proof ctxt) e; val err_typ = "Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^ Syntax.string_of_sort ctxt sort; in translation_error ctxt permissive some_thm deps "Wellsortedness error" (err_typ ^ "\n" ^ err_class) end; (* inference of type annotations for disambiguation with type classes *) fun mk_tagged_type (true, T) = Type ("", [T]) | mk_tagged_type (false, T) = T; fun dest_tagged_type (Type ("", [T])) = (true, T) | dest_tagged_type T = (false, T); val untag_term = map_types (snd o dest_tagged_type); fun tag_term (proj_sort, _) eqngr = let val has_sort_constraints = exists (not o null) o map proj_sort o Code_Preproc.sortargs eqngr; fun tag (Const (_, T')) (Const (c, T)) = Const (c, mk_tagged_type (not (null (Term.add_tvarsT T' [])) andalso has_sort_constraints c, T)) | tag (t1 $ u1) (t $ u) = tag t1 t $ tag u1 u | tag (Abs (_, _, t1)) (Abs (x, T, t)) = Abs (x, T, tag t1 t) | tag (Free _) (t as Free _) = t | tag (Var _) (t as Var _) = t | tag (Bound _) (t as Bound _) = t; in tag end fun annotate ctxt algbr eqngr (c, ty) args rhs = let val erase = map_types (fn _ => Type_Infer.anyT []); val reinfer = singleton (Type_Infer_Context.infer_types ctxt); val lhs = list_comb (Const (c, ty), map (map_types Type.strip_sorts o fst) args); val reinferred_rhs = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase rhs)))); in tag_term algbr eqngr reinferred_rhs rhs end fun annotate_eqns ctxt algbr eqngr (c, ty) eqns = let val ctxt' = ctxt |> Proof_Context.theory_of |> Proof_Context.init_global |> Config.put Type_Infer_Context.const_sorts false; (*avoid spurious fixed variables: there is no eigen context for equations*) in map (apfst (fn (args, (rhs, some_abs)) => (args, (annotate ctxt' algbr eqngr (c, ty) args rhs, some_abs)))) eqns end; (* preprocessing pattern schemas *) fun preprocess_pattern_schema ctxt (t_pos, case_pats) (c_ty, ts) = let val thy = Proof_Context.theory_of ctxt; val ty = nth (binder_types (snd c_ty)) t_pos; fun select_clauses xs = xs |> nth_drop t_pos |> curry (op ~~) case_pats |> map_filter (fn (NONE, _) => NONE | (SOME _, x) => SOME x); fun mk_constr c t = let val n = Code.args_number thy c; in ((c, (take n o binder_types o fastype_of o untag_term) t ---> ty), n) end; val constrs = if null case_pats then [] else map2 mk_constr (case_pats |> map_filter I) (select_clauses ts); val split_clauses = if null case_pats then (fn ts => (nth ts t_pos, nth_drop t_pos ts)) else (fn ts => (nth ts t_pos, select_clauses ts)); in (ty, constrs, split_clauses) end; (* abstract dictionary construction *) datatype typarg_witness = Weakening of (class * class) list * plain_typarg_witness and plain_typarg_witness = Global of (string * class) * typarg_witness list list | Local of { var: string, index: int, sort: sort, unique: bool }; fun brand_unique unique (w as Global _) = w | brand_unique unique (Local { var, index, sort, unique = _ }) = Local { var = var, index = index, sort = sort, unique = unique }; fun construct_dictionaries ctxt (proj_sort, algebra) permissive some_thm (ty, sort) (deps, program) = let fun class_relation unique (Weakening (classrels, x), sub_class) super_class = Weakening ((sub_class, super_class) :: classrels, brand_unique unique x); fun type_constructor (tyco, _) dss class = Weakening ([], Global ((tyco, class), (map o map) fst dss)); fun type_variable (TFree (v, sort)) = let val sort' = proj_sort sort; in map_index (fn (n, class) => (Weakening ([], Local { var = v, index = n, sort = sort', unique = true }), class)) sort' end; val typarg_witnesses = Sorts.of_sort_derivation algebra {class_relation = fn _ => fn unique => Sorts.classrel_derivation algebra (class_relation unique), type_constructor = type_constructor, type_variable = type_variable} (ty, proj_sort sort) handle Sorts.CLASS_ERROR e => not_wellsorted ctxt permissive some_thm deps ty sort e; in (typarg_witnesses, (deps, program)) end; (* translation *) fun ensure_tyco ctxt algbr eqngr permissive tyco = let val thy = Proof_Context.theory_of ctxt; val ((vs, cos), _) = Code.get_type thy tyco; val stmt_datatype = fold_map (translate_tyvar_sort ctxt algbr eqngr permissive) vs #>> map fst ##>> fold_map (fn (c, (vs, tys)) => ensure_const ctxt algbr eqngr permissive c ##>> pair (map (unprefix "'" o fst) vs) ##>> fold_map (translate_typ ctxt algbr eqngr permissive) tys) cos #>> Datatype; in ensure_stmt Type_Constructor stmt_datatype tyco end and ensure_const ctxt algbr eqngr permissive c = let val thy = Proof_Context.theory_of ctxt; fun stmt_datatypecons tyco = ensure_tyco ctxt algbr eqngr permissive tyco #>> Datatypecons; fun stmt_classparam class = ensure_class ctxt algbr eqngr permissive class #>> Classparam; fun stmt_fun cert = case Code.equations_of_cert thy cert of (_, NONE) => pair NoStmt | ((vs, ty), SOME eqns) => let val eqns' = annotate_eqns ctxt algbr eqngr (c, ty) eqns val some_case_cong = Code.get_case_cong thy c; in fold_map (translate_tyvar_sort ctxt algbr eqngr permissive) vs ##>> translate_typ ctxt algbr eqngr permissive ty ##>> translate_eqns ctxt algbr eqngr permissive eqns' #>> (fn (_, NONE) => NoStmt | (tyscm, SOME eqns) => Fun ((tyscm, eqns), some_case_cong)) end; val stmt_const = case Code.get_type_of_constr_or_abstr thy c of SOME (tyco, _) => stmt_datatypecons tyco | NONE => (case Axclass.class_of_param thy c of SOME class => stmt_classparam class | NONE => stmt_fun (Code_Preproc.cert eqngr c)) in ensure_stmt Constant stmt_const c end and ensure_class ctxt (algbr as (_, algebra)) eqngr permissive class = let val thy = Proof_Context.theory_of ctxt; val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class; val cs = #params (Axclass.get_info thy class); val stmt_class = fold_map (fn super_class => ensure_classrel ctxt algbr eqngr permissive (class, super_class)) super_classes ##>> fold_map (fn (c, ty) => ensure_const ctxt algbr eqngr permissive c ##>> translate_typ ctxt algbr eqngr permissive ty) cs #>> (fn info => Class (unprefix "'" Name.aT, info)) in ensure_stmt Type_Class stmt_class class end and ensure_classrel ctxt algbr eqngr permissive (sub_class, super_class) = let val stmt_classrel = ensure_class ctxt algbr eqngr permissive sub_class ##>> ensure_class ctxt algbr eqngr permissive super_class #>> Classrel; in ensure_stmt Class_Relation stmt_classrel (sub_class, super_class) end and ensure_inst ctxt (algbr as (_, algebra)) eqngr permissive (tyco, class) = let val thy = Proof_Context.theory_of ctxt; val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class; val these_class_params = these o try (#params o Axclass.get_info thy); val class_params = these_class_params class; val superclass_params = maps these_class_params ((Sorts.complete_sort algebra o Sorts.super_classes algebra) class); val vs = Name.invent_names Name.context "'a" (Sorts.mg_domain algebra tyco [class]); val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class]; val vs' = map2 (fn (v, sort1) => fn sort2 => (v, Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts'; val arity_typ = Type (tyco, map TFree vs); val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs'); fun translate_super_instance super_class = ensure_class ctxt algbr eqngr permissive super_class ##>> translate_dicts ctxt algbr eqngr permissive NONE (arity_typ, [super_class]) #>> (fn (super_class, [Dict ([], Dict_Const (_, dss))]) => (super_class, dss)); fun translate_classparam_instance (c, ty) = let val raw_const = Const (c, map_type_tfree (K arity_typ') ty); val dom_length = length (fst (strip_type ty)) val thm = Axclass.unoverload_conv ctxt (Thm.cterm_of ctxt raw_const); val const = (apsnd Logic.unvarifyT_global o dest_Const o snd o Logic.dest_equals o Thm.prop_of) thm; in ensure_const ctxt algbr eqngr permissive c ##>> translate_const ctxt algbr eqngr permissive (SOME thm) (const, NONE) #>> (fn (c, IConst const') => ((c, (const', dom_length)), (thm, true))) end; val stmt_inst = ensure_class ctxt algbr eqngr permissive class ##>> ensure_tyco ctxt algbr eqngr permissive tyco ##>> fold_map (translate_tyvar_sort ctxt algbr eqngr permissive) vs ##>> fold_map translate_super_instance super_classes ##>> fold_map translate_classparam_instance class_params ##>> fold_map translate_classparam_instance superclass_params #>> (fn (((((class, tyco), vs), superinsts), inst_params), superinst_params) => Classinst { class = class, tyco = tyco, vs = vs, superinsts = superinsts, inst_params = inst_params, superinst_params = superinst_params }); in ensure_stmt Class_Instance stmt_inst (tyco, class) end and translate_typ ctxt algbr eqngr permissive (TFree (v, _)) = pair (ITyVar (unprefix "'" v)) | translate_typ ctxt algbr eqngr permissive (Type (tyco, tys)) = ensure_tyco ctxt algbr eqngr permissive tyco ##>> fold_map (translate_typ ctxt algbr eqngr permissive) tys #>> (fn (tyco, tys) => tyco `%% tys) and translate_term ctxt algbr eqngr permissive some_thm (Const (c, ty), some_abs) = translate_app ctxt algbr eqngr permissive some_thm (((c, ty), []), some_abs) | translate_term ctxt algbr eqngr permissive some_thm (Free (v, _), some_abs) = pair (IVar (SOME v)) | translate_term ctxt algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) = let val ((v', _), t') = Term.dest_abs_global (Abs (Name.desymbolize (SOME false) v, ty, t)); val v'' = if Term.used_free v' t' then SOME v' else NONE in translate_typ ctxt algbr eqngr permissive ty ##>> translate_term ctxt algbr eqngr permissive some_thm (t', some_abs) #>> (fn (ty, t) => (v'', ty) `|=> t) end | translate_term ctxt algbr eqngr permissive some_thm (t as _ $ _, some_abs) = case strip_comb t of (Const (c, ty), ts) => translate_app ctxt algbr eqngr permissive some_thm (((c, ty), ts), some_abs) | (t', ts) => translate_term ctxt algbr eqngr permissive some_thm (t', some_abs) ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) ts #>> (fn (t, ts) => t `$$ ts) and translate_eqn ctxt algbr eqngr permissive ((args, (rhs, some_abs)), (some_thm, proper)) = fold_map (translate_term ctxt algbr eqngr permissive some_thm) args ##>> translate_term ctxt algbr eqngr permissive some_thm (rhs, some_abs) #>> rpair (some_thm, proper) and translate_eqns ctxt algbr eqngr permissive eqns = maybe_permissive (fold_map (translate_eqn ctxt algbr eqngr permissive) eqns) and translate_const ctxt algbr eqngr permissive some_thm ((c, ty), some_abs) (deps, program) = let val thy = Proof_Context.theory_of ctxt; val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs)) andalso Code.is_abstr thy c then translation_error ctxt permissive some_thm deps "Abstraction violation" ("constant " ^ Code.string_of_const thy c) else () in translate_const_proper ctxt algbr eqngr permissive some_thm (c, ty) (deps, program) end and translate_const_proper ctxt algbr eqngr permissive some_thm (c, ty) = let val thy = Proof_Context.theory_of ctxt; val (annotate, ty') = dest_tagged_type ty; val typargs = Sign.const_typargs thy (c, ty'); val sorts = Code_Preproc.sortargs eqngr c; val (dom, range) = Term.strip_type ty'; in ensure_const ctxt algbr eqngr permissive c ##>> fold_map (translate_typ ctxt algbr eqngr permissive) typargs ##>> fold_map (translate_dicts ctxt algbr eqngr permissive some_thm) (typargs ~~ sorts) ##>> fold_map (translate_typ ctxt algbr eqngr permissive) (ty' :: dom) #>> (fn (((c, typargs), dss), annotation :: dom) => IConst { sym = Constant c, typargs = typargs, dicts = dss, dom = dom, annotation = if annotate then SOME annotation else NONE }) end and translate_app_const ctxt algbr eqngr permissive some_thm ((c_ty, ts), some_abs) = translate_const ctxt algbr eqngr permissive some_thm (c_ty, some_abs) ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) ts #>> (fn (t, ts) => t `$$ ts) and translate_case ctxt algbr eqngr permissive some_thm (t_pos, case_pats) (c_ty, ts) = let val (ty, constrs, split_clauses) = preprocess_pattern_schema ctxt (t_pos, case_pats) (c_ty, ts); fun mk_clauses [] ty (t, ts_clause) = (t, map (fn ([pat], body) => (pat, body)) (distill_minimized_clause ctxt [ty] (the_single ts_clause))) | mk_clauses constrs ty (t, ts_clause) = (t, maps (fn ((constr as IConst { dom = tys, ... }, n), t) => map (fn (pat_args, body) => (constr `$$ pat_args, body)) (distill_minimized_clause ctxt (take n tys) t)) (constrs ~~ ts_clause)); in translate_const ctxt algbr eqngr permissive some_thm (c_ty, NONE) ##>> fold_map (fn (constr, n) => translate_const ctxt algbr eqngr permissive some_thm (constr, NONE) #>> rpair n) constrs ##>> translate_typ ctxt algbr eqngr permissive ty ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) ts #>> (fn (((t_app, constrs), ty), ts) => case mk_clauses constrs ty (split_clauses ts) of (t, clauses) => ICase { term = t, typ = ty, clauses = clauses, primitive = t_app `$$ ts }) end and translate_app_case ctxt algbr eqngr permissive some_thm (num_args, pattern_schema) ((c, ty), ts) = if length ts < num_args then let val k = length ts; val tys = (take (num_args - k) o drop k o fst o strip_type) ty; val names = Name.build_context (ts |> (fold o fold_aterms) Term.declare_term_frees); val vs = Name.invent_names names "a" tys; in fold_map (translate_typ ctxt algbr eqngr permissive) tys ##>> translate_case ctxt algbr eqngr permissive some_thm pattern_schema ((c, ty), ts @ map Free vs) #>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t) end else if length ts > num_args then translate_case ctxt algbr eqngr permissive some_thm pattern_schema ((c, ty), take num_args ts) ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) (drop num_args ts) #>> (fn (t, ts) => t `$$ ts) else translate_case ctxt algbr eqngr permissive some_thm pattern_schema ((c, ty), ts) and translate_app ctxt algbr eqngr permissive some_thm (c_ty_ts as ((c, _), _), some_abs) = case Code.get_case_schema (Proof_Context.theory_of ctxt) c of SOME case_schema => translate_app_case ctxt algbr eqngr permissive some_thm case_schema c_ty_ts | NONE => translate_app_const ctxt algbr eqngr permissive some_thm (c_ty_ts, some_abs) and translate_tyvar_sort ctxt (algbr as (proj_sort, _)) eqngr permissive (v, sort) = fold_map (ensure_class ctxt algbr eqngr permissive) (proj_sort sort) #>> (fn sort => (unprefix "'" v, sort)) and translate_dicts ctxt algbr eqngr permissive some_thm (ty, sort) = let fun mk_dict (Weakening (classrels, d)) = fold_map (ensure_classrel ctxt algbr eqngr permissive) classrels ##>> mk_plain_dict d #>> Dict and mk_plain_dict (Global (inst, dss)) = ensure_inst ctxt algbr eqngr permissive inst ##>> (fold_map o fold_map) mk_dict dss #>> Dict_Const | mk_plain_dict (Local { var, index, sort, unique }) = ensure_class ctxt algbr eqngr permissive (nth sort index) #>> (fn class => Dict_Var { var = unprefix "'" var, index = index, length = length sort, class = class, unique = unique }) in construct_dictionaries ctxt algbr permissive some_thm (ty, sort) #-> (fn typarg_witnesses => fold_map mk_dict typarg_witnesses) end; (* store *) structure Program = Code_Data ( type T = program; val empty = Code_Symbol.Graph.empty; ); fun invoke_generation ignore_cache ctxt generate thing = Program.change_yield (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt)) (fn program => ([], program) |> generate thing |-> (fn thing => fn (_, program) => (thing, program))); (* program generation *) fun check_abstract_constructors thy consts = case filter (Code.is_abstr thy) consts of [] => () | abstrs => error ("Cannot export abstract constructor(s): " ^ commas (map (Code.string_of_const thy) abstrs)); fun invoke_generation_for_consts ctxt { ignore_cache, permissive } { algebra, eqngr } consts = let val thy = Proof_Context.theory_of ctxt; val _ = if permissive then () else check_abstract_constructors thy consts; in Code_Preproc.timed "translating program" #ctxt (fn { ctxt, algebra, eqngr, consts } => invoke_generation ignore_cache ctxt (fold_map (ensure_const ctxt algebra eqngr permissive)) consts) { ctxt = ctxt, algebra = algebra, eqngr = eqngr, consts = consts } end; fun invoke_generation_for_consts' ctxt ignore_cache_and_permissive consts = invoke_generation_for_consts ctxt { ignore_cache = ignore_cache_and_permissive, permissive = ignore_cache_and_permissive } (Code_Preproc.obtain ignore_cache_and_permissive { ctxt = ctxt, consts = consts, terms = []}) consts |> snd; fun invoke_generation_for_consts'' ctxt algebra_eqngr = invoke_generation_for_consts ctxt { ignore_cache = true, permissive = false } algebra_eqngr #> (fn (deps, program) => { deps = deps, program = program }); fun consts_program_permissive ctxt = invoke_generation_for_consts' ctxt true; fun consts_program ctxt consts = let fun project program = Code_Symbol.Graph.restrict (member (op =) (Code_Symbol.Graph.all_succs program (map Constant consts))) program; in invoke_generation_for_consts' ctxt false consts |> project end; (* value evaluation *) fun ensure_value ctxt algbr eqngr t = let val ty = fastype_of t; val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =) o dest_TFree))) t []; val t' = annotate ctxt algbr eqngr (\<^const_name>\Pure.dummy_pattern\, ty) [] t; val dummy_constant = Constant \<^const_name>\Pure.dummy_pattern\; val stmt_value = fold_map (translate_tyvar_sort ctxt algbr eqngr false) vs ##>> translate_typ ctxt algbr eqngr false ty ##>> translate_term ctxt algbr eqngr false NONE (t', NONE) #>> (fn ((vs, ty), t) => Fun (((vs, ty), [(([], t), (NONE, true))]), NONE)); fun term_value (_, program1) = let val Fun ((vs_ty, [(([], t), _)]), _) = Code_Symbol.Graph.get_node program1 dummy_constant; val deps' = Code_Symbol.Graph.immediate_succs program1 dummy_constant; val program2 = Code_Symbol.Graph.del_node dummy_constant program1; val deps_all = Code_Symbol.Graph.all_succs program2 deps'; val program3 = Code_Symbol.Graph.restrict (member (op =) deps_all) program2; in ((program3, ((vs_ty, t), deps')), (deps', program2)) end; in ensure_stmt Constant stmt_value \<^const_name>\Pure.dummy_pattern\ #> snd #> term_value end; fun dynamic_evaluation comp ctxt algebra eqngr t = let val ((program, (vs_ty_t', deps)), _) = Code_Preproc.timed "translating term" #ctxt (fn { ctxt, algebra, eqngr, t } => invoke_generation false ctxt (ensure_value ctxt algebra eqngr) t) { ctxt = ctxt, algebra = algebra, eqngr = eqngr, t = t }; in comp program t vs_ty_t' deps end; fun dynamic_conv ctxt conv = Code_Preproc.dynamic_conv ctxt (dynamic_evaluation (fn program => fn _ => conv program) ctxt); fun dynamic_value ctxt postproc comp = Code_Preproc.dynamic_value ctxt postproc (dynamic_evaluation comp ctxt); fun static_evaluation ctxt consts algebra_eqngr static_eval = static_eval (invoke_generation_for_consts'' ctxt algebra_eqngr consts); fun static_evaluation_thingol ctxt consts (algebra_eqngr as { algebra, eqngr }) static_eval = let fun evaluation program dynamic_eval ctxt t = let val ((_, ((vs_ty', t'), deps)), _) = Code_Preproc.timed "translating term" #ctxt (fn { ctxt, t } => ensure_value ctxt algebra eqngr t ([], program)) { ctxt = ctxt, t = t }; in dynamic_eval ctxt t (vs_ty', t') deps end; in static_evaluation ctxt consts algebra_eqngr (fn program_deps => evaluation (#program program_deps) (static_eval program_deps)) end; fun static_evaluation_isa ctxt consts algebra_eqngr static_eval = static_evaluation ctxt consts algebra_eqngr (fn program_deps => (static_eval (#program program_deps))); fun static_conv_thingol (ctxt_consts as { ctxt, consts }) conv = Code_Preproc.static_conv ctxt_consts (fn algebra_eqngr => static_evaluation_thingol ctxt consts algebra_eqngr (fn program_deps => let val static_conv = conv program_deps; in fn ctxt => fn _ => fn vs_ty => fn deps => static_conv ctxt vs_ty deps end)); fun static_conv_isa (ctxt_consts as { ctxt, consts }) conv = Code_Preproc.static_conv ctxt_consts (fn algebra_eqngr => static_evaluation_isa ctxt consts algebra_eqngr conv); fun static_value (ctxt_postproc_consts as { ctxt, consts, ... }) comp = Code_Preproc.static_value ctxt_postproc_consts (fn algebra_eqngr => static_evaluation_thingol ctxt consts algebra_eqngr comp); (** constant expressions **) fun read_const_exprs_internal ctxt = let val thy = Proof_Context.theory_of ctxt; fun this_theory name = if Context.theory_name thy = name then thy else Context.get_theory {long = false} thy name; fun consts_of thy' = fold (fn (c, (_, NONE)) => cons c | _ => I) (#constants (Consts.dest (Sign.consts_of thy'))) [] |> filter_out (Code.is_abstr thy); fun belongs_here thy' c = forall (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy'); fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy'); fun read_const_expr str = (case Syntax.parse_input ctxt (K NONE) (K Markup.empty) (SOME o Symbol_Pos.implode o #1) str of SOME "_" => ([], consts_of thy) | SOME s => (case try (unsuffix "._") s of SOME name => ([], consts_of_select (this_theory name)) | NONE => ([Code.read_const thy str], [])) | NONE => ([Code.read_const thy str], [])); in apply2 flat o split_list o map read_const_expr end; fun read_const_exprs_all ctxt = op @ o read_const_exprs_internal ctxt; fun read_const_exprs ctxt const_exprs = let val (consts, consts_permissive) = read_const_exprs_internal ctxt const_exprs; val consts' = consts_program_permissive ctxt consts_permissive |> implemented_deps |> filter_out (Code.is_abstr (Proof_Context.theory_of ctxt)); in union (op =) consts' consts end; (** diagnostic commands **) fun code_depgr ctxt consts = let val { eqngr, ... } = Code_Preproc.obtain true { ctxt = ctxt, consts = consts, terms = [] }; val all_consts = Graph.all_succs eqngr consts; in Graph.restrict (member (op =) all_consts) eqngr end; fun code_thms ctxt = Pretty.writeln o Code_Preproc.pretty ctxt o code_depgr ctxt; fun coalesce_strong_conn gr = let val xss = Graph.strong_conn gr; val xss_ys = map (fn xs => (xs, commas xs)) xss; val y_for = the o AList.lookup (op =) (maps (fn (xs, y) => map (fn x => (x, y)) xs) xss_ys); fun coalesced_succs_for xs = maps (Graph.immediate_succs gr) xs |> subtract (op =) xs |> map y_for |> distinct (op =); val succs = map (fn (xs, _) => (xs, coalesced_succs_for xs)) xss_ys; in map (fn (xs, y) => ((y, xs), (maps (Graph.get_node gr) xs, (the o AList.lookup (op =) succs) xs))) xss_ys end; fun code_deps ctxt consts = let val thy = Proof_Context.theory_of ctxt; fun mk_entry ((name, consts), (ps, deps)) = let val label = commas (map (Code.string_of_const thy) consts); in ((name, Graph_Display.content_node label (Pretty.str label :: ps)), deps) end; in code_depgr ctxt consts |> Graph.map (K (Code.pretty_cert thy o snd)) |> coalesce_strong_conn |> map mk_entry |> Graph_Display.display_graph end; local fun code_thms_cmd ctxt = code_thms ctxt o read_const_exprs_all ctxt; fun code_deps_cmd ctxt = code_deps ctxt o read_const_exprs_all ctxt; in val _ = Outer_Syntax.command \<^command_keyword>\code_thms\ "print system of code equations for code" (Scan.repeat1 Parse.term >> (fn cs => Toplevel.keep (fn st => code_thms_cmd (Toplevel.context_of st) cs))); val _ = Outer_Syntax.command \<^command_keyword>\code_deps\ "visualize dependencies of code equations for code" (Scan.repeat1 Parse.term >> (fn cs => Toplevel.keep (fn st => code_deps_cmd (Toplevel.context_of st) cs))); end; end; (*struct*) structure Basic_Code_Thingol: BASIC_CODE_THINGOL = Code_Thingol;