src/Tools/Code/code_ml.ML
changeset 55150 0940309ed8f1
parent 55147 bce3dbc11f95
child 55657 d5ad50aea356
     1.1 --- a/src/Tools/Code/code_ml.ML	Sat Jan 25 23:50:49 2014 +0100
     1.2 +++ b/src/Tools/Code/code_ml.ML	Sat Jan 25 23:50:49 2014 +0100
     1.3 @@ -14,6 +14,7 @@
     1.4  structure Code_ML : CODE_ML =
     1.5  struct
     1.6  
     1.7 +open Basic_Code_Symbol;
     1.8  open Basic_Code_Thingol;
     1.9  open Code_Printer;
    1.10  
    1.11 @@ -36,7 +37,7 @@
    1.12  datatype ml_stmt =
    1.13      ML_Exc of string * (typscheme * int)
    1.14    | ML_Val of ml_binding
    1.15 -  | ML_Funs of ml_binding list * Code_Symbol.symbol list
    1.16 +  | ML_Funs of ml_binding list * Code_Symbol.T list
    1.17    | ML_Datas of (string * (vname list * ((string * vname list) * itype list) list)) list
    1.18    | ML_Class of string * (vname * ((class * class) list * (string * itype) list));
    1.19  
    1.20 @@ -53,21 +54,21 @@
    1.21  
    1.22  fun print_sml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
    1.23    let
    1.24 -    val deresolve_const = deresolve o Code_Symbol.Constant;
    1.25 -    val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
    1.26 -    val deresolve_class = deresolve o Code_Symbol.Type_Class;
    1.27 -    val deresolve_classrel = deresolve o Code_Symbol.Class_Relation;
    1.28 -    val deresolve_inst = deresolve o Code_Symbol.Class_Instance;
    1.29 +    val deresolve_const = deresolve o Constant;
    1.30 +    val deresolve_tyco = deresolve o Type_Constructor;
    1.31 +    val deresolve_class = deresolve o Type_Class;
    1.32 +    val deresolve_classrel = deresolve o Class_Relation;
    1.33 +    val deresolve_inst = deresolve o Class_Instance;
    1.34      fun print_tyco_expr (sym, []) = (str o deresolve) sym
    1.35        | print_tyco_expr (sym, [ty]) =
    1.36            concat [print_typ BR ty, (str o deresolve) sym]
    1.37        | print_tyco_expr (sym, tys) =
    1.38            concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym]
    1.39      and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
    1.40 -         of NONE => print_tyco_expr (Code_Symbol.Type_Constructor tyco, tys)
    1.41 +         of NONE => print_tyco_expr (Type_Constructor tyco, tys)
    1.42            | SOME (_, print) => print print_typ fxy tys)
    1.43        | print_typ fxy (ITyVar v) = str ("'" ^ v);
    1.44 -    fun print_dicttyp (class, ty) = print_tyco_expr (Code_Symbol.Type_Class class, [ty]);
    1.45 +    fun print_dicttyp (class, ty) = print_tyco_expr (Type_Class class, [ty]);
    1.46      fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
    1.47        (map_filter (fn (v, sort) =>
    1.48          (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
    1.49 @@ -81,7 +82,7 @@
    1.50        print_classrels fxy classrels (print_plain_dict is_pseudo_fun fxy x)
    1.51      and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
    1.52            ((str o deresolve_inst) inst ::
    1.53 -            (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
    1.54 +            (if is_pseudo_fun (Class_Instance inst) then [str "()"]
    1.55              else map_filter (print_dicts is_pseudo_fun BR) dss))
    1.56        | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
    1.57            [str (if k = 1 then first_upper v ^ "_"
    1.58 @@ -110,7 +111,7 @@
    1.59            in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
    1.60        | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
    1.61            (case Code_Thingol.unfold_const_app (#primitive case_expr)
    1.62 -           of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
    1.63 +           of SOME (app as ({ sym = Constant const, ... }, _)) =>
    1.64                  if is_none (const_syntax const)
    1.65                  then print_case is_pseudo_fun some_thm vars fxy case_expr
    1.66                  else print_app is_pseudo_fun some_thm vars fxy app
    1.67 @@ -174,7 +175,7 @@
    1.68        in
    1.69          concat (
    1.70            str definer
    1.71 -          :: print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs)
    1.72 +          :: print_tyco_expr (Type_Constructor tyco, map ITyVar vs)
    1.73            :: str "="
    1.74            :: separate (str "|") (map print_co cos)
    1.75          )
    1.76 @@ -195,7 +196,7 @@
    1.77                in
    1.78                  concat (
    1.79                    prolog
    1.80 -                  :: (if is_pseudo_fun (Code_Symbol.Constant const) then [str "()"]
    1.81 +                  :: (if is_pseudo_fun (Constant const) then [str "()"]
    1.82                        else print_dict_args vs
    1.83                          @ map (print_term is_pseudo_fun some_thm vars BR) ts)
    1.84                    @ str "="
    1.85 @@ -205,7 +206,7 @@
    1.86              val shift = if null eqs then I else
    1.87                map (Pretty.block o single o Pretty.block o single);
    1.88            in pair
    1.89 -            (print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty))
    1.90 +            (print_val_decl print_typscheme (Constant const, vs_ty))
    1.91              ((Pretty.block o Pretty.fbreaks o shift) (
    1.92                print_eqn definer eq
    1.93                :: map (print_eqn "|") eqs
    1.94 @@ -228,11 +229,11 @@
    1.95                ];
    1.96            in pair
    1.97              (print_val_decl print_dicttypscheme
    1.98 -              (Code_Symbol.Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
    1.99 +              (Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
   1.100              (concat (
   1.101                str definer
   1.102                :: (str o deresolve_inst) inst
   1.103 -              :: (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
   1.104 +              :: (if is_pseudo_fun (Class_Instance inst) then [str "()"]
   1.105                    else print_dict_args vs)
   1.106                @ str "="
   1.107                :: enum "," "{" "}"
   1.108 @@ -243,7 +244,7 @@
   1.109              ))
   1.110            end;
   1.111      fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair
   1.112 -          [print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty)]
   1.113 +          [print_val_decl print_typscheme (Constant const, vs_ty)]
   1.114            ((semicolon o map str) (
   1.115              (if n = 0 then "val" else "fun")
   1.116              :: deresolve_const const
   1.117 @@ -279,7 +280,7 @@
   1.118            end
   1.119       | print_stmt (ML_Datas [(tyco, (vs, []))]) =
   1.120            let
   1.121 -            val ty_p = print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs);
   1.122 +            val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs);
   1.123            in
   1.124              pair
   1.125              [concat [str "type", ty_p]]
   1.126 @@ -301,7 +302,7 @@
   1.127                (map str ["val", s, "=", "#" ^ s, ":"] @| p);
   1.128              fun print_super_class_decl (classrel as (_, super_class)) =
   1.129                print_val_decl print_dicttypscheme
   1.130 -                (Code_Symbol.Class_Relation classrel, ([(v, [class])], (super_class, ITyVar v)));
   1.131 +                (Class_Relation classrel, ([(v, [class])], (super_class, ITyVar v)));
   1.132              fun print_super_class_field (classrel as (_, super_class)) =
   1.133                print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v));
   1.134              fun print_super_class_proj (classrel as (_, super_class)) =
   1.135 @@ -309,7 +310,7 @@
   1.136                  (print_dicttypscheme ([(v, [class])], (super_class, ITyVar v)));
   1.137              fun print_classparam_decl (classparam, ty) =
   1.138                print_val_decl print_typscheme
   1.139 -                (Code_Symbol.Constant classparam, ([(v, [class])], ty));
   1.140 +                (Constant classparam, ([(v, [class])], ty));
   1.141              fun print_classparam_field (classparam, ty) =
   1.142                print_field (deresolve_const classparam) (print_typ NOBR ty);
   1.143              fun print_classparam_proj (classparam, ty) =
   1.144 @@ -359,21 +360,21 @@
   1.145  
   1.146  fun print_ocaml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
   1.147    let
   1.148 -    val deresolve_const = deresolve o Code_Symbol.Constant;
   1.149 -    val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
   1.150 -    val deresolve_class = deresolve o Code_Symbol.Type_Class;
   1.151 -    val deresolve_classrel = deresolve o Code_Symbol.Class_Relation;
   1.152 -    val deresolve_inst = deresolve o Code_Symbol.Class_Instance;
   1.153 +    val deresolve_const = deresolve o Constant;
   1.154 +    val deresolve_tyco = deresolve o Type_Constructor;
   1.155 +    val deresolve_class = deresolve o Type_Class;
   1.156 +    val deresolve_classrel = deresolve o Class_Relation;
   1.157 +    val deresolve_inst = deresolve o Class_Instance;
   1.158      fun print_tyco_expr (sym, []) = (str o deresolve) sym
   1.159        | print_tyco_expr (sym, [ty]) =
   1.160            concat [print_typ BR ty, (str o deresolve) sym]
   1.161        | print_tyco_expr (sym, tys) =
   1.162            concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym]
   1.163      and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
   1.164 -         of NONE => print_tyco_expr (Code_Symbol.Type_Constructor tyco, tys)
   1.165 +         of NONE => print_tyco_expr (Type_Constructor tyco, tys)
   1.166            | SOME (_, print) => print print_typ fxy tys)
   1.167        | print_typ fxy (ITyVar v) = str ("'" ^ v);
   1.168 -    fun print_dicttyp (class, ty) = print_tyco_expr (Code_Symbol.Type_Class class, [ty]);
   1.169 +    fun print_dicttyp (class, ty) = print_tyco_expr (Type_Class class, [ty]);
   1.170      fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
   1.171        (map_filter (fn (v, sort) =>
   1.172          (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
   1.173 @@ -386,7 +387,7 @@
   1.174        |> print_classrels classrels
   1.175      and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
   1.176            brackify BR ((str o deresolve_inst) inst ::
   1.177 -            (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
   1.178 +            (if is_pseudo_fun (Class_Instance inst) then [str "()"]
   1.179              else map_filter (print_dicts is_pseudo_fun BR) dss))
   1.180        | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
   1.181            str (if k = 1 then "_" ^ first_upper v
   1.182 @@ -412,7 +413,7 @@
   1.183            in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
   1.184        | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
   1.185            (case Code_Thingol.unfold_const_app (#primitive case_expr)
   1.186 -           of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
   1.187 +           of SOME (app as ({ sym = Constant const, ... }, _)) =>
   1.188                  if is_none (const_syntax const)
   1.189                  then print_case is_pseudo_fun some_thm vars fxy case_expr
   1.190                  else print_app is_pseudo_fun some_thm vars fxy app
   1.191 @@ -471,7 +472,7 @@
   1.192        in
   1.193          concat (
   1.194            str definer
   1.195 -          :: print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs)
   1.196 +          :: print_tyco_expr (Type_Constructor tyco, map ITyVar vs)
   1.197            :: str "="
   1.198            :: separate (str "|") (map print_co cos)
   1.199          )
   1.200 @@ -544,11 +545,11 @@
   1.201                concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty]
   1.202                  else (concat o map str) [definer, deresolve_const const];
   1.203            in pair
   1.204 -            (print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty))
   1.205 +            (print_val_decl print_typscheme (Constant const, vs_ty))
   1.206              (concat (
   1.207                prolog
   1.208                :: print_dict_args vs
   1.209 -              @| print_eqns (is_pseudo_fun (Code_Symbol.Constant const)) eqs
   1.210 +              @| print_eqns (is_pseudo_fun (Constant const)) eqs
   1.211              ))
   1.212            end
   1.213        | print_def is_pseudo_fun _ definer
   1.214 @@ -568,11 +569,11 @@
   1.215                ];
   1.216            in pair
   1.217              (print_val_decl print_dicttypscheme
   1.218 -              (Code_Symbol.Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
   1.219 +              (Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
   1.220              (concat (
   1.221                str definer
   1.222                :: (str o deresolve_inst) inst
   1.223 -              :: (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
   1.224 +              :: (if is_pseudo_fun (Class_Instance inst) then [str "()"]
   1.225                    else print_dict_args vs)
   1.226                @ str "="
   1.227                @@ brackets [
   1.228 @@ -584,7 +585,7 @@
   1.229              ))
   1.230            end;
   1.231       fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair
   1.232 -          [print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty)]
   1.233 +          [print_val_decl print_typscheme (Constant const, vs_ty)]
   1.234            ((doublesemicolon o map str) (
   1.235              "let"
   1.236              :: deresolve_const const
   1.237 @@ -619,7 +620,7 @@
   1.238            end
   1.239       | print_stmt (ML_Datas [(tyco, (vs, []))]) =
   1.240            let
   1.241 -            val ty_p = print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs);
   1.242 +            val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs);
   1.243            in
   1.244              pair
   1.245              [concat [str "type", ty_p]]
   1.246 @@ -641,7 +642,7 @@
   1.247                print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v));
   1.248              fun print_classparam_decl (classparam, ty) =
   1.249                print_val_decl print_typscheme
   1.250 -                (Code_Symbol.Constant classparam, ([(v, [class])], ty));
   1.251 +                (Constant classparam, ([(v, [class])], ty));
   1.252              fun print_classparam_field (classparam, ty) =
   1.253                print_field (deresolve_const classparam) (print_typ NOBR ty);
   1.254              val w = "_" ^ first_upper v;
   1.255 @@ -724,7 +725,7 @@
   1.256        | namify_stmt (Code_Thingol.Classrel _) = namify_const false
   1.257        | namify_stmt (Code_Thingol.Classparam _) = namify_const false
   1.258        | namify_stmt (Code_Thingol.Classinst _) = namify_const false;
   1.259 -    fun ml_binding_of_stmt (sym as Code_Symbol.Constant const, Code_Thingol.Fun ((tysm as (vs, ty), raw_eqs), _)) =
   1.260 +    fun ml_binding_of_stmt (sym as Constant const, Code_Thingol.Fun ((tysm as (vs, ty), raw_eqs), _)) =
   1.261            let
   1.262              val eqs = filter (snd o snd) raw_eqs;
   1.263              val (eqs', some_sym) = if null (filter_out (null o snd) vs) then case eqs
   1.264 @@ -734,7 +735,7 @@
   1.265                  | _ => (eqs, NONE)
   1.266                else (eqs, NONE)
   1.267            in (ML_Function (const, (tysm, eqs')), some_sym) end
   1.268 -      | ml_binding_of_stmt (sym as Code_Symbol.Class_Instance inst, Code_Thingol.Classinst (stmt as { vs, ... })) =
   1.269 +      | ml_binding_of_stmt (sym as Class_Instance inst, Code_Thingol.Classinst (stmt as { vs, ... })) =
   1.270            (ML_Instance (inst, stmt), if forall (null o snd) vs then SOME (sym, false) else NONE)
   1.271        | ml_binding_of_stmt (sym, _) =
   1.272            error ("Binding block containing illegal statement: " ^ 
   1.273 @@ -755,10 +756,10 @@
   1.274        (ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)))
   1.275      fun modify_datatypes stmts = single (SOME
   1.276        (ML_Datas (map_filter
   1.277 -        (fn (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype stmt) => SOME (tyco, stmt) | _ => NONE) stmts)))
   1.278 +        (fn (Type_Constructor tyco, Code_Thingol.Datatype stmt) => SOME (tyco, stmt) | _ => NONE) stmts)))
   1.279      fun modify_class stmts = single (SOME
   1.280        (ML_Class (the_single (map_filter
   1.281 -        (fn (Code_Symbol.Type_Class class, Code_Thingol.Class stmt) => SOME (class, stmt) | _ => NONE) stmts))))
   1.282 +        (fn (Type_Class class, Code_Thingol.Class stmt) => SOME (class, stmt) | _ => NONE) stmts))))
   1.283      fun modify_stmts ([stmt as (_, stmt' as Code_Thingol.Fun _)]) =
   1.284            if Code_Thingol.is_case stmt' then [] else [modify_fun stmt]
   1.285        | modify_stmts ((stmts as (_, Code_Thingol.Fun _) :: _)) =
   1.286 @@ -850,7 +851,7 @@
   1.287        check = { env_var = "ISABELLE_OCAML",
   1.288          make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
   1.289          make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } })
   1.290 -  #> Code_Target.set_printings (Code_Symbol.Type_Constructor ("fun",
   1.291 +  #> Code_Target.set_printings (Type_Constructor ("fun",
   1.292      [(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))]))
   1.293    #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
   1.294    #> fold (Code_Target.add_reserved target_SML)