# HG changeset patch # User haftmann # Date 1241629754 -7200 # Node ID 841c9f67f9e7afe966e2ecd9b54d92da7d0ff59e # Parent b7e1c065b6e41e5bd1b6eb62cfd3b66fbbb857f2 explicit type arguments in constants diff -r b7e1c065b6e4 -r 841c9f67f9e7 src/Tools/code/code_haskell.ML --- a/src/Tools/code/code_haskell.ML Wed May 06 19:09:14 2009 +0200 +++ b/src/Tools/code/code_haskell.ML Wed May 06 19:09:14 2009 +0200 @@ -31,7 +31,7 @@ | pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p]; in gen_pr_bind pr_bind pr_term end; -fun pr_haskell_stmt naming labelled_name syntax_class syntax_tyco syntax_const +fun pr_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const init_syms deresolve is_cons contr_classparam_typs deriving_show = let val deresolve_base = Long_Name.base_name o deresolve; @@ -96,7 +96,7 @@ (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys) else (str o deresolve) c :: map (pr_term tyvars thm vars BR) ts end - and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const naming + and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const and pr_bind tyvars = pr_haskell_bind (pr_term tyvars) and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) = let @@ -336,7 +336,7 @@ fun serialize_haskell module_prefix raw_module_name string_classes labelled_name raw_reserved_names includes raw_module_alias - syntax_class syntax_tyco syntax_const naming program cs destination = + syntax_class syntax_tyco syntax_const program cs destination = let val stmt_names = Code_Target.stmt_names_of_destination destination; val module_name = if null stmt_names then raw_module_name else SOME "Code"; @@ -358,7 +358,7 @@ | deriv' _ (ITyVar _) = true in deriv [] tyco end; val reserved_names = Code_Printer.make_vars reserved_names; - fun pr_stmt qualified = pr_haskell_stmt naming labelled_name + fun pr_stmt qualified = pr_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const reserved_names (if qualified then deresolver else Long_Name.base_name o deresolver) is_cons contr_classparam_typs @@ -469,14 +469,14 @@ | pr_monad pr_bind pr (SOME (bind, false), t) vars = vars |> pr_bind NOBR bind |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]); - fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2 + fun pretty _ [c_bind'] pr thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2 of SOME (bind, t') => let - val (binds, t'') = implode_monad ((the o Code_Thingol.lookup_const naming) c_bind) t' + val (binds, t'') = implode_monad c_bind' t' val (ps, vars') = fold_map (pr_monad (pr_haskell_bind (K pr) thm) pr) (bind :: binds) vars; in (brackify fxy o single o Pretty.enclose "do {" "}" o Pretty.breaks) (ps @| pr vars' NOBR t'') end | NONE => brackify_infix (1, L) fxy [pr vars (INFX (1, L)) t1, str ">>=", pr vars (INFX (1, X)) t2] - in (2, pretty) end; + in (2, ([c_bind], pretty)) end; fun add_monad target' raw_c_bind thy = let diff -r b7e1c065b6e4 -r 841c9f67f9e7 src/Tools/code/code_ml.ML --- a/src/Tools/code/code_ml.ML Wed May 06 19:09:14 2009 +0200 +++ b/src/Tools/code/code_ml.ML Wed May 06 19:09:14 2009 +0200 @@ -45,7 +45,7 @@ (** SML serailizer **) -fun pr_sml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons = +fun pr_sml_stmt labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons = let val pr_label_classrel = translate_string (fn "." => "__" | c => c) o Long_Name.qualifier; @@ -124,7 +124,7 @@ (str o deresolve) c :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts and pr_app is_closure thm vars = gen_pr_app (pr_app' is_closure) (pr_term is_closure) - syntax_const naming thm vars + syntax_const thm vars and pr_bind' ((NONE, NONE), _) = str "_" | pr_bind' ((SOME v, NONE), _) = str v | pr_bind' ((NONE, SOME p), _) = p @@ -360,7 +360,7 @@ (** OCaml serializer **) -fun pr_ocaml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons = +fun pr_ocaml_stmt labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons = let fun pr_dicts fxy ds = let @@ -428,7 +428,7 @@ else (str o deresolve) c :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts) and pr_app is_closure = gen_pr_app (pr_app' is_closure) (pr_term is_closure) - syntax_const naming + syntax_const and pr_bind' ((NONE, NONE), _) = str "_" | pr_bind' ((SOME v, NONE), _) = str v | pr_bind' ((NONE, SOME p), _) = p @@ -909,7 +909,7 @@ in (deresolver, nodes) end; fun serialize_ml target compile pr_module pr_stmt raw_module_name labelled_name reserved_names includes raw_module_alias - _ syntax_tyco syntax_const naming program stmt_names destination = + _ syntax_tyco syntax_const program stmt_names destination = let val is_cons = Code_Thingol.is_cons program; val present_stmt_names = Code_Target.stmt_names_of_destination destination; @@ -924,7 +924,7 @@ (null o filter (member (op =) present_stmt_names) o stmt_names_of) stmt then NONE else SOME - (pr_stmt naming labelled_name syntax_tyco syntax_const reserved_names + (pr_stmt labelled_name syntax_tyco syntax_const reserved_names (deresolver prefix) is_cons stmt) | pr_node prefix (Module (module_name, (_, nodes))) = separate (str "") diff -r b7e1c065b6e4 -r 841c9f67f9e7 src/Tools/code/code_thingol.ML --- a/src/Tools/code/code_thingol.ML Wed May 06 19:09:14 2009 +0200 +++ b/src/Tools/code/code_thingol.ML Wed May 06 19:09:14 2009 +0200 @@ -61,6 +61,7 @@ val lookup_tyco: naming -> string -> string option val lookup_instance: naming -> class * string -> string option val lookup_const: naming -> string -> string option + val ensure_declared_const: theory -> string -> naming -> string * naming datatype stmt = NoStmt @@ -359,6 +360,11 @@ fun declare_const thy = declare thy map_const lookup_const Symtab.update_new namify_const; +fun ensure_declared_const thy const naming = + case lookup_const naming const + of SOME const' => (const', naming) + | NONE => declare_const thy const naming; + val unfold_fun = unfoldr (fn "Pure.fun.tyco" `%% [ty1, ty2] => SOME (ty1, ty2) | _ => NONE); (*depends on suffix_tyco and namify_tyco!*)