src/Tools/Code/code_ml.ML
changeset 48072 ace701efe203
parent 48003 1d11af40b106
child 48568 084cd758a8ab
     1.1 --- a/src/Tools/Code/code_ml.ML	Mon Jun 04 12:55:54 2012 +0200
     1.2 +++ b/src/Tools/Code/code_ml.ML	Tue Jun 05 07:05:56 2012 +0200
     1.3 @@ -28,9 +28,10 @@
     1.4  
     1.5  datatype ml_binding =
     1.6      ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
     1.7 -  | ML_Instance of string * ((class * (string * (vname * sort) list))
     1.8 -        * ((class * (string * (string * dict list list))) list
     1.9 -      * (((string * const) * (thm * bool)) list * ((string * const) * (thm * bool)) list)));
    1.10 +  | ML_Instance of string * { class: string, tyco: string, vs: (vname * sort) list,
    1.11 +        superinsts: (class * (string * (string * dict list list))) list,
    1.12 +        inst_params: ((string * const) * (thm * bool)) list,
    1.13 +        superinst_params: ((string * const) * (thm * bool)) list };
    1.14  
    1.15  datatype ml_stmt =
    1.16      ML_Exc of string * (typscheme * int)
    1.17 @@ -83,15 +84,15 @@
    1.18      and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
    1.19      val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
    1.20        (map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
    1.21 -    fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
    1.22 -          print_app is_pseudo_fun some_thm vars fxy (c, [])
    1.23 +    fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
    1.24 +          print_app is_pseudo_fun some_thm vars fxy (const, [])
    1.25        | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
    1.26            str "_"
    1.27        | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
    1.28            str (lookup_var vars v)
    1.29        | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
    1.30            (case Code_Thingol.unfold_const_app t
    1.31 -           of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts
    1.32 +           of SOME app => print_app is_pseudo_fun some_thm vars fxy app
    1.33              | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
    1.34                  print_term is_pseudo_fun some_thm vars BR t2])
    1.35        | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
    1.36 @@ -102,15 +103,15 @@
    1.37                #>> (fn p => concat [str "fn", p, str "=>"]);
    1.38              val (ps, vars') = fold_map print_abs binds vars;
    1.39            in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
    1.40 -      | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
    1.41 -          (case Code_Thingol.unfold_const_app t0
    1.42 -           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
    1.43 -                then print_case is_pseudo_fun some_thm vars fxy cases
    1.44 -                else print_app is_pseudo_fun some_thm vars fxy c_ts
    1.45 -            | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
    1.46 -    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (arg_tys, _)), _)), ts)) =
    1.47 +      | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
    1.48 +          (case Code_Thingol.unfold_const_app (#primitive case_expr)
    1.49 +           of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
    1.50 +                then print_case is_pseudo_fun some_thm vars fxy case_expr
    1.51 +                else print_app is_pseudo_fun some_thm vars fxy app
    1.52 +            | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
    1.53 +    and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
    1.54        if is_cons c then
    1.55 -        let val k = length arg_tys in
    1.56 +        let val k = length dom in
    1.57            if k < 2 orelse length ts = k
    1.58            then (str o deresolve) c
    1.59              :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
    1.60 @@ -118,14 +119,16 @@
    1.61          end
    1.62        else if is_pseudo_fun c
    1.63          then (str o deresolve) c @@ str "()"
    1.64 -      else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
    1.65 +      else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss
    1.66          @ map (print_term is_pseudo_fun some_thm vars BR) ts
    1.67      and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
    1.68        (print_term is_pseudo_fun) const_syntax some_thm vars
    1.69      and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
    1.70 -    and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
    1.71 +    and print_case is_pseudo_fun some_thm vars fxy { clauses = [], ... } =
    1.72 +          (concat o map str) ["raise", "Fail", "\"empty case\""]
    1.73 +      | print_case is_pseudo_fun some_thm vars fxy (case_expr as { clauses = [_], ... }) =
    1.74            let
    1.75 -            val (binds, body) = Code_Thingol.unfold_let (ICase cases);
    1.76 +            val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
    1.77              fun print_match ((pat, _), t) vars =
    1.78                vars
    1.79                |> print_bind is_pseudo_fun some_thm NOBR pat
    1.80 @@ -139,7 +142,7 @@
    1.81                str "end"
    1.82              ]
    1.83            end
    1.84 -      | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) =
    1.85 +      | print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } =
    1.86            let
    1.87              fun print_select delim (pat, body) =
    1.88                let
    1.89 @@ -154,9 +157,7 @@
    1.90                :: print_select "of" clause
    1.91                :: map (print_select "|") clauses
    1.92              )
    1.93 -          end
    1.94 -      | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) =
    1.95 -          (concat o map str) ["raise", "Fail", "\"empty case\""];
    1.96 +          end;
    1.97      fun print_val_decl print_typscheme (name, typscheme) = concat
    1.98        [str "val", str (deresolve name), str ":", print_typscheme typscheme];
    1.99      fun print_datatype_decl definer (tyco, (vs, cos)) =
   1.100 @@ -206,7 +207,7 @@
   1.101              ))
   1.102            end
   1.103        | print_def is_pseudo_fun _ definer
   1.104 -          (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
   1.105 +          (ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) =
   1.106            let
   1.107              fun print_super_instance (_, (classrel, x)) =
   1.108                concat [
   1.109 @@ -230,8 +231,8 @@
   1.110                    else print_dict_args vs)
   1.111                @ str "="
   1.112                :: enum "," "{" "}"
   1.113 -                (map print_super_instance super_instances
   1.114 -                  @ map print_classparam_instance classparam_instances)
   1.115 +                (map print_super_instance superinsts
   1.116 +                  @ map print_classparam_instance inst_params)
   1.117                :: str ":"
   1.118                @@ print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
   1.119              ))
   1.120 @@ -386,15 +387,15 @@
   1.121      and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
   1.122      val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
   1.123        (map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
   1.124 -    fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
   1.125 -          print_app is_pseudo_fun some_thm vars fxy (c, [])
   1.126 +    fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
   1.127 +          print_app is_pseudo_fun some_thm vars fxy (const, [])
   1.128        | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
   1.129            str "_"
   1.130        | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
   1.131            str (lookup_var vars v)
   1.132        | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
   1.133            (case Code_Thingol.unfold_const_app t
   1.134 -           of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts
   1.135 +           of SOME app => print_app is_pseudo_fun some_thm vars fxy app
   1.136              | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
   1.137                  print_term is_pseudo_fun some_thm vars BR t2])
   1.138        | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
   1.139 @@ -402,15 +403,15 @@
   1.140              val (binds, t') = Code_Thingol.unfold_pat_abs t;
   1.141              val (ps, vars') = fold_map (print_bind is_pseudo_fun some_thm BR o fst) binds vars;
   1.142            in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
   1.143 -      | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
   1.144 -          (case Code_Thingol.unfold_const_app t0
   1.145 -           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
   1.146 -                then print_case is_pseudo_fun some_thm vars fxy cases
   1.147 -                else print_app is_pseudo_fun some_thm vars fxy c_ts
   1.148 -            | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
   1.149 -    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (tys, _)), _)), ts)) =
   1.150 +      | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
   1.151 +          (case Code_Thingol.unfold_const_app (#primitive case_expr)
   1.152 +           of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
   1.153 +                then print_case is_pseudo_fun some_thm vars fxy case_expr
   1.154 +                else print_app is_pseudo_fun some_thm vars fxy app
   1.155 +            | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
   1.156 +    and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
   1.157        if is_cons c then
   1.158 -        let val k = length tys in
   1.159 +        let val k = length dom in
   1.160            if length ts = k
   1.161            then (str o deresolve) c
   1.162              :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
   1.163 @@ -418,14 +419,16 @@
   1.164          end
   1.165        else if is_pseudo_fun c
   1.166          then (str o deresolve) c @@ str "()"
   1.167 -      else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
   1.168 +      else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss
   1.169          @ map (print_term is_pseudo_fun some_thm vars BR) ts
   1.170      and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
   1.171        (print_term is_pseudo_fun) const_syntax some_thm vars
   1.172      and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
   1.173 -    and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
   1.174 +    and print_case is_pseudo_fun some_thm vars fxy { clauses = [], ... } =
   1.175 +          (concat o map str) ["failwith", "\"empty case\""]
   1.176 +      | print_case is_pseudo_fun some_thm vars fxy (case_expr as { clauses = [_], ... }) =
   1.177            let
   1.178 -            val (binds, body) = Code_Thingol.unfold_let (ICase cases);
   1.179 +            val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
   1.180              fun print_let ((pat, _), t) vars =
   1.181                vars
   1.182                |> print_bind is_pseudo_fun some_thm NOBR pat
   1.183 @@ -436,7 +439,7 @@
   1.184              brackify_block fxy (Pretty.chunks ps) []
   1.185                (print_term is_pseudo_fun some_thm vars' NOBR body)
   1.186            end
   1.187 -      | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) =
   1.188 +      | print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } =
   1.189            let
   1.190              fun print_select delim (pat, body) =
   1.191                let
   1.192 @@ -449,9 +452,7 @@
   1.193                :: print_select "with" clause
   1.194                :: map (print_select "|") clauses
   1.195              )
   1.196 -          end
   1.197 -      | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) =
   1.198 -          (concat o map str) ["failwith", "\"empty case\""];
   1.199 +          end;
   1.200      fun print_val_decl print_typscheme (name, typscheme) = concat
   1.201        [str "val", str (deresolve name), str ":", print_typscheme typscheme];
   1.202      fun print_datatype_decl definer (tyco, (vs, cos)) =
   1.203 @@ -546,7 +547,7 @@
   1.204              ))
   1.205            end
   1.206        | print_def is_pseudo_fun _ definer
   1.207 -            (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
   1.208 +          (ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) =
   1.209            let
   1.210              fun print_super_instance (_, (classrel, x)) =
   1.211                concat [
   1.212 @@ -570,8 +571,8 @@
   1.213                    else print_dict_args vs)
   1.214                @ str "="
   1.215                @@ brackets [
   1.216 -                enum_default "()" ";" "{" "}" (map print_super_instance super_instances
   1.217 -                  @ map print_classparam_instance classparam_instances),
   1.218 +                enum_default "()" ";" "{" "}" (map print_super_instance superinsts
   1.219 +                  @ map print_classparam_instance inst_params),
   1.220                  str ":",
   1.221                  print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
   1.222                ]
   1.223 @@ -731,7 +732,7 @@
   1.224                  | _ => (eqs, NONE)
   1.225                else (eqs, NONE)
   1.226            in (ML_Function (name, (tysm, eqs')), some_value_name) end
   1.227 -      | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) =
   1.228 +      | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as { vs, ... })) =
   1.229            (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)
   1.230        | ml_binding_of_stmt (name, _) =
   1.231            error ("Binding block containing illegal statement: " ^ labelled_name name)