explicit type arguments in constants
authorhaftmann
Wed May 06 19:09:14 2009 +0200 (2009-05-06)
changeset 31054841c9f67f9e7
parent 31053 b7e1c065b6e4
child 31055 2cf6efca6c71
explicit type arguments in constants
src/Tools/code/code_haskell.ML
src/Tools/code/code_ml.ML
src/Tools/code/code_thingol.ML
     1.1 --- a/src/Tools/code/code_haskell.ML	Wed May 06 19:09:14 2009 +0200
     1.2 +++ b/src/Tools/code/code_haskell.ML	Wed May 06 19:09:14 2009 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4        | pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p];
     1.5    in gen_pr_bind pr_bind pr_term end;
     1.6  
     1.7 -fun pr_haskell_stmt naming labelled_name syntax_class syntax_tyco syntax_const
     1.8 +fun pr_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const
     1.9      init_syms deresolve is_cons contr_classparam_typs deriving_show =
    1.10    let
    1.11      val deresolve_base = Long_Name.base_name o deresolve;
    1.12 @@ -96,7 +96,7 @@
    1.13              (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys)
    1.14            else (str o deresolve) c :: map (pr_term tyvars thm vars BR) ts
    1.15          end
    1.16 -    and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const naming
    1.17 +    and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const
    1.18      and pr_bind tyvars = pr_haskell_bind (pr_term tyvars)
    1.19      and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
    1.20            let
    1.21 @@ -336,7 +336,7 @@
    1.22  
    1.23  fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
    1.24      raw_reserved_names includes raw_module_alias
    1.25 -    syntax_class syntax_tyco syntax_const naming program cs destination =
    1.26 +    syntax_class syntax_tyco syntax_const program cs destination =
    1.27    let
    1.28      val stmt_names = Code_Target.stmt_names_of_destination destination;
    1.29      val module_name = if null stmt_names then raw_module_name else SOME "Code";
    1.30 @@ -358,7 +358,7 @@
    1.31            | deriv' _ (ITyVar _) = true
    1.32        in deriv [] tyco end;
    1.33      val reserved_names = Code_Printer.make_vars reserved_names;
    1.34 -    fun pr_stmt qualified = pr_haskell_stmt naming labelled_name
    1.35 +    fun pr_stmt qualified = pr_haskell_stmt labelled_name
    1.36        syntax_class syntax_tyco syntax_const reserved_names
    1.37        (if qualified then deresolver else Long_Name.base_name o deresolver)
    1.38        is_cons contr_classparam_typs
    1.39 @@ -469,14 +469,14 @@
    1.40        | pr_monad pr_bind pr (SOME (bind, false), t) vars = vars
    1.41            |> pr_bind NOBR bind
    1.42            |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
    1.43 -    fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
    1.44 +    fun pretty _ [c_bind'] pr thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
    1.45       of SOME (bind, t') => let
    1.46 -          val (binds, t'') = implode_monad ((the o Code_Thingol.lookup_const naming) c_bind) t'
    1.47 +          val (binds, t'') = implode_monad c_bind' t'
    1.48            val (ps, vars') = fold_map (pr_monad (pr_haskell_bind (K pr) thm) pr) (bind :: binds) vars;
    1.49          in (brackify fxy o single o Pretty.enclose "do {" "}" o Pretty.breaks) (ps @| pr vars' NOBR t'') end
    1.50        | NONE => brackify_infix (1, L) fxy
    1.51            [pr vars (INFX (1, L)) t1, str ">>=", pr vars (INFX (1, X)) t2]
    1.52 -  in (2, pretty) end;
    1.53 +  in (2, ([c_bind], pretty)) end;
    1.54  
    1.55  fun add_monad target' raw_c_bind thy =
    1.56    let
     2.1 --- a/src/Tools/code/code_ml.ML	Wed May 06 19:09:14 2009 +0200
     2.2 +++ b/src/Tools/code/code_ml.ML	Wed May 06 19:09:14 2009 +0200
     2.3 @@ -45,7 +45,7 @@
     2.4  
     2.5  (** SML serailizer **)
     2.6  
     2.7 -fun pr_sml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
     2.8 +fun pr_sml_stmt labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
     2.9    let
    2.10      val pr_label_classrel = translate_string (fn "." => "__" | c => c)
    2.11        o Long_Name.qualifier;
    2.12 @@ -124,7 +124,7 @@
    2.13          (str o deresolve) c
    2.14            :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts
    2.15      and pr_app is_closure thm vars = gen_pr_app (pr_app' is_closure) (pr_term is_closure)
    2.16 -      syntax_const naming thm vars
    2.17 +      syntax_const thm vars
    2.18      and pr_bind' ((NONE, NONE), _) = str "_"
    2.19        | pr_bind' ((SOME v, NONE), _) = str v
    2.20        | pr_bind' ((NONE, SOME p), _) = p
    2.21 @@ -360,7 +360,7 @@
    2.22  
    2.23  (** OCaml serializer **)
    2.24  
    2.25 -fun pr_ocaml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
    2.26 +fun pr_ocaml_stmt labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
    2.27    let
    2.28      fun pr_dicts fxy ds =
    2.29        let
    2.30 @@ -428,7 +428,7 @@
    2.31        else (str o deresolve) c
    2.32          :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts)
    2.33      and pr_app is_closure = gen_pr_app (pr_app' is_closure) (pr_term is_closure)
    2.34 -      syntax_const naming
    2.35 +      syntax_const
    2.36      and pr_bind' ((NONE, NONE), _) = str "_"
    2.37        | pr_bind' ((SOME v, NONE), _) = str v
    2.38        | pr_bind' ((NONE, SOME p), _) = p
    2.39 @@ -909,7 +909,7 @@
    2.40    in (deresolver, nodes) end;
    2.41  
    2.42  fun serialize_ml target compile pr_module pr_stmt raw_module_name labelled_name reserved_names includes raw_module_alias
    2.43 -  _ syntax_tyco syntax_const naming program stmt_names destination =
    2.44 +  _ syntax_tyco syntax_const program stmt_names destination =
    2.45    let
    2.46      val is_cons = Code_Thingol.is_cons program;
    2.47      val present_stmt_names = Code_Target.stmt_names_of_destination destination;
    2.48 @@ -924,7 +924,7 @@
    2.49            (null o filter (member (op =) present_stmt_names) o stmt_names_of) stmt
    2.50            then NONE
    2.51            else SOME
    2.52 -            (pr_stmt naming labelled_name syntax_tyco syntax_const reserved_names
    2.53 +            (pr_stmt labelled_name syntax_tyco syntax_const reserved_names
    2.54                (deresolver prefix) is_cons stmt)
    2.55        | pr_node prefix (Module (module_name, (_, nodes))) =
    2.56            separate (str "")
     3.1 --- a/src/Tools/code/code_thingol.ML	Wed May 06 19:09:14 2009 +0200
     3.2 +++ b/src/Tools/code/code_thingol.ML	Wed May 06 19:09:14 2009 +0200
     3.3 @@ -61,6 +61,7 @@
     3.4    val lookup_tyco: naming -> string -> string option
     3.5    val lookup_instance: naming -> class * string -> string option
     3.6    val lookup_const: naming -> string -> string option
     3.7 +  val ensure_declared_const: theory -> string -> naming -> string * naming
     3.8  
     3.9    datatype stmt =
    3.10        NoStmt
    3.11 @@ -359,6 +360,11 @@
    3.12  fun declare_const thy = declare thy map_const
    3.13    lookup_const Symtab.update_new namify_const;
    3.14  
    3.15 +fun ensure_declared_const thy const naming =
    3.16 +  case lookup_const naming const
    3.17 +   of SOME const' => (const', naming)
    3.18 +    | NONE => declare_const thy const naming;
    3.19 +
    3.20  val unfold_fun = unfoldr
    3.21    (fn "Pure.fun.tyco" `%% [ty1, ty2] => SOME (ty1, ty2)
    3.22      | _ => NONE); (*depends on suffix_tyco and namify_tyco!*)