src/Tools/Code/code_ml.ML
changeset 38923 79d7f2b4cf71
parent 38922 ec2a8efd8990
child 38924 fcd1d0457e27
     1.1 --- a/src/Tools/Code/code_ml.ML	Tue Aug 31 13:15:35 2010 +0200
     1.2 +++ b/src/Tools/Code/code_ml.ML	Tue Aug 31 13:29:38 2010 +0200
     1.3 @@ -59,14 +59,14 @@
     1.4  
     1.5  (** SML serializer **)
     1.6  
     1.7 -fun print_sml_stmt labelled_name syntax_tyco syntax_const reserved is_cons deresolve =
     1.8 +fun print_sml_stmt labelled_name tyco_syntax const_syntax reserved is_cons deresolve =
     1.9    let
    1.10      fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
    1.11        | print_tyco_expr fxy (tyco, [ty]) =
    1.12            concat [print_typ BR ty, (str o deresolve) tyco]
    1.13        | print_tyco_expr fxy (tyco, tys) =
    1.14            concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
    1.15 -    and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
    1.16 +    and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
    1.17           of NONE => print_tyco_expr fxy (tyco, tys)
    1.18            | SOME (i, print) => print print_typ fxy tys)
    1.19        | print_typ fxy (ITyVar v) = str ("'" ^ v);
    1.20 @@ -114,7 +114,7 @@
    1.21            in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
    1.22        | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
    1.23            (case Code_Thingol.unfold_const_app t0
    1.24 -           of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
    1.25 +           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
    1.26                  then print_case is_pseudo_fun some_thm vars fxy cases
    1.27                  else print_app is_pseudo_fun some_thm vars fxy c_ts
    1.28              | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
    1.29 @@ -131,7 +131,7 @@
    1.30        else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
    1.31          @ map (print_term is_pseudo_fun some_thm vars BR) ts
    1.32      and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
    1.33 -      (print_term is_pseudo_fun) syntax_const some_thm vars
    1.34 +      (print_term is_pseudo_fun) const_syntax some_thm vars
    1.35      and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
    1.36      and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
    1.37            let
    1.38 @@ -190,7 +190,7 @@
    1.39                  val consts = fold Code_Thingol.add_constnames (t :: ts) [];
    1.40                  val vars = reserved
    1.41                    |> intro_base_names
    1.42 -                       (is_none o syntax_const) deresolve consts
    1.43 +                       (is_none o const_syntax) deresolve consts
    1.44                    |> intro_vars ((fold o Code_Thingol.fold_varnames)
    1.45                         (insert (op =)) ts []);
    1.46                  val prolog = if needs_typ then
    1.47 @@ -365,14 +365,14 @@
    1.48  
    1.49  (** OCaml serializer **)
    1.50  
    1.51 -fun print_ocaml_stmt labelled_name syntax_tyco syntax_const reserved is_cons deresolve =
    1.52 +fun print_ocaml_stmt labelled_name tyco_syntax const_syntax reserved is_cons deresolve =
    1.53    let
    1.54      fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
    1.55        | print_tyco_expr fxy (tyco, [ty]) =
    1.56            concat [print_typ BR ty, (str o deresolve) tyco]
    1.57        | print_tyco_expr fxy (tyco, tys) =
    1.58            concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
    1.59 -    and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
    1.60 +    and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
    1.61           of NONE => print_tyco_expr fxy (tyco, tys)
    1.62            | SOME (i, print) => print print_typ fxy tys)
    1.63        | print_typ fxy (ITyVar v) = str ("'" ^ v);
    1.64 @@ -412,7 +412,7 @@
    1.65            in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
    1.66        | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
    1.67            (case Code_Thingol.unfold_const_app t0
    1.68 -           of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
    1.69 +           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
    1.70                  then print_case is_pseudo_fun some_thm vars fxy cases
    1.71                  else print_app is_pseudo_fun some_thm vars fxy c_ts
    1.72              | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
    1.73 @@ -429,7 +429,7 @@
    1.74        else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
    1.75          @ map (print_term is_pseudo_fun some_thm vars BR) ts
    1.76      and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
    1.77 -      (print_term is_pseudo_fun) syntax_const some_thm vars
    1.78 +      (print_term is_pseudo_fun) const_syntax some_thm vars
    1.79      and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
    1.80      and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
    1.81            let
    1.82 @@ -495,7 +495,7 @@
    1.83                      val consts = fold Code_Thingol.add_constnames (t :: ts) [];
    1.84                      val vars = reserved
    1.85                        |> intro_base_names
    1.86 -                          (is_none o syntax_const) deresolve consts
    1.87 +                          (is_none o const_syntax) deresolve consts
    1.88                        |> intro_vars ((fold o Code_Thingol.fold_varnames)
    1.89                            (insert (op =)) ts []);
    1.90                    in
    1.91 @@ -521,7 +521,7 @@
    1.92                      val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) [];
    1.93                      val vars = reserved
    1.94                        |> intro_base_names
    1.95 -                          (is_none o syntax_const) deresolve consts;
    1.96 +                          (is_none o const_syntax) deresolve consts;
    1.97                      val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs;
    1.98                    in
    1.99                      Pretty.block (
   1.100 @@ -903,7 +903,7 @@
   1.101    in (deresolver, nodes) end;
   1.102  
   1.103  fun serialize_ml target print_module print_stmt module_name with_signatures labelled_name
   1.104 -  reserved includes module_alias _ syntax_tyco syntax_const program
   1.105 +  reserved includes module_alias _ tyco_syntax const_syntax program
   1.106    (stmt_names, presentation_stmt_names) =
   1.107    let
   1.108      val is_cons = Code_Thingol.is_cons program;
   1.109 @@ -916,7 +916,7 @@
   1.110        | print_node prefix (Stmt (_, stmt)) = if is_presentation andalso
   1.111            (null o filter (member (op =) presentation_stmt_names) o stmt_names_of) stmt
   1.112            then NONE
   1.113 -          else SOME (print_stmt labelled_name syntax_tyco syntax_const reserved is_cons (deresolver prefix) stmt)
   1.114 +          else SOME (print_stmt labelled_name tyco_syntax const_syntax reserved is_cons (deresolver prefix) stmt)
   1.115        | print_node prefix (Module (module_name, (_, nodes))) =
   1.116            let
   1.117              val (decls, body) = print_nodes (prefix @ [module_name]) nodes;
   1.118 @@ -960,13 +960,13 @@
   1.119      (target_OCaml, { serializer = isar_serializer_ocaml, literals = literals_ocaml,
   1.120        check = { env_var = "EXEC_OCAML", make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
   1.121          make_command = fn ocaml => fn _ => ocaml ^ " -w pu nums.cma ROOT.ocaml" } })
   1.122 -  #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   1.123 +  #> Code_Target.add_tyco_syntax target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   1.124        brackify_infix (1, R) fxy (
   1.125          print_typ (INFX (1, X)) ty1,
   1.126          str "->",
   1.127          print_typ (INFX (1, R)) ty2
   1.128        )))
   1.129 -  #> Code_Target.add_syntax_tyco target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   1.130 +  #> Code_Target.add_tyco_syntax target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   1.131        brackify_infix (1, R) fxy (
   1.132          print_typ (INFX (1, X)) ty1,
   1.133          str "->",