src/Tools/Code/code_ml.ML
changeset 32913 3e9809678574
parent 32908 9aa8dfef16ff
child 32924 d2e9b2dab760
equal deleted inserted replaced
32910:d61e303fc7e5 32913:3e9809678574
   173               @@ exc_str
   173               @@ exc_str
   174             )
   174             )
   175           end
   175           end
   176       | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) =
   176       | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) =
   177           let
   177           let
   178             val consts = map_filter
   178             val consts = Code_Thingol.add_constnames t [];
   179               (fn c => if (is_some o syntax_const) c
       
   180                 then NONE else (SOME o Long_Name.base_name o deresolve) c)
       
   181                 (Code_Thingol.add_constnames t []);
       
   182             val vars = reserved_names
   179             val vars = reserved_names
   183               |> Code_Printer.intro_vars consts;
   180               |> Code_Printer.intro_base_names
       
   181                   (is_none o syntax_const) deresolve consts;
   184           in
   182           in
   185             concat [
   183             concat [
   186               str "val",
   184               str "val",
   187               (str o deresolve) name,
   185               (str o deresolve) name,
   188               str ":",
   186               str ":",
   198                 val vs_dict = filter_out (null o snd) vs;
   196                 val vs_dict = filter_out (null o snd) vs;
   199                 val shift = if null eqs' then I else
   197                 val shift = if null eqs' then I else
   200                   map (Pretty.block o single o Pretty.block o single);
   198                   map (Pretty.block o single o Pretty.block o single);
   201                 fun pr_eq definer ((ts, t), (thm, _)) =
   199                 fun pr_eq definer ((ts, t), (thm, _)) =
   202                   let
   200                   let
   203                     val consts = map_filter
   201                     val consts = fold Code_Thingol.add_constnames (t :: ts) [];
   204                       (fn c => if (is_some o syntax_const) c
       
   205                         then NONE else (SOME o Long_Name.base_name o deresolve) c)
       
   206                         (fold Code_Thingol.add_constnames (t :: ts) []);
       
   207                     val vars = reserved_names
   202                     val vars = reserved_names
   208                       |> Code_Printer.intro_vars consts
   203                       |> Code_Printer.intro_base_names
       
   204                            (is_none o syntax_const) deresolve consts
   209                       |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
   205                       |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
   210                            (insert (op =)) ts []);
   206                            (insert (op =)) ts []);
   211                   in
   207                   in
   212                     concat (
   208                     concat (
   213                       str definer
   209                       str definer
   470               @@ exc_str
   466               @@ exc_str
   471             )
   467             )
   472           end
   468           end
   473       | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) =
   469       | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) =
   474           let
   470           let
   475             val consts = map_filter
   471             val consts = Code_Thingol.add_constnames t [];
   476               (fn c => if (is_some o syntax_const) c
       
   477                 then NONE else (SOME o Long_Name.base_name o deresolve) c)
       
   478                 (Code_Thingol.add_constnames t []);
       
   479             val vars = reserved_names
   472             val vars = reserved_names
   480               |> Code_Printer.intro_vars consts;
   473               |> Code_Printer.intro_base_names
       
   474                   (is_none o syntax_const) deresolve consts;
   481           in
   475           in
   482             concat [
   476             concat [
   483               str "let",
   477               str "let",
   484               (str o deresolve) name,
   478               (str o deresolve) name,
   485               str ":",
   479               str ":",
   490           end
   484           end
   491       | pr_stmt (MLFuns (funn :: funns, pseudo_funs)) =
   485       | pr_stmt (MLFuns (funn :: funns, pseudo_funs)) =
   492           let
   486           let
   493             fun pr_eq ((ts, t), (thm, _)) =
   487             fun pr_eq ((ts, t), (thm, _)) =
   494               let
   488               let
   495                 val consts = map_filter
   489                 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
   496                   (fn c => if (is_some o syntax_const) c
       
   497                     then NONE else (SOME o Long_Name.base_name o deresolve) c)
       
   498                     (fold Code_Thingol.add_constnames (t :: ts) []);
       
   499                 val vars = reserved_names
   490                 val vars = reserved_names
   500                   |> Code_Printer.intro_vars consts
   491                   |> Code_Printer.intro_base_names
       
   492                       (is_none o syntax_const) deresolve consts
   501                   |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
   493                   |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
   502                       (insert (op =)) ts []);
   494                       (insert (op =)) ts []);
   503               in concat [
   495               in concat [
   504                 (Pretty.block o Pretty.commas)
   496                 (Pretty.block o Pretty.commas)
   505                   (map (pr_term (member (op =) pseudo_funs) thm vars NOBR) ts),
   497                   (map (pr_term (member (op =) pseudo_funs) thm vars NOBR) ts),
   506                 str "->",
   498                 str "->",
   507                 pr_term (member (op =) pseudo_funs) thm vars NOBR t
   499                 pr_term (member (op =) pseudo_funs) thm vars NOBR t
   508               ] end;
   500               ] end;
   509             fun pr_eqs is_pseudo [((ts, t), (thm, _))] =
   501             fun pr_eqs is_pseudo [((ts, t), (thm, _))] =
   510                   let
   502                   let
   511                     val consts = map_filter
   503                     val consts = fold Code_Thingol.add_constnames (t :: ts) [];
   512                       (fn c => if (is_some o syntax_const) c
       
   513                         then NONE else (SOME o Long_Name.base_name o deresolve) c)
       
   514                         (fold Code_Thingol.add_constnames (t :: ts) []);
       
   515                     val vars = reserved_names
   504                     val vars = reserved_names
   516                       |> Code_Printer.intro_vars consts
   505                       |> Code_Printer.intro_base_names
       
   506                           (is_none o syntax_const) deresolve consts
   517                       |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
   507                       |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
   518                           (insert (op =)) ts []);
   508                           (insert (op =)) ts []);
   519                   in
   509                   in
   520                     concat (
   510                     concat (
   521                       (if is_pseudo then [str "()"]
   511                       (if is_pseudo then [str "()"]
   534                     :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
   524                     :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
   535                           o single o pr_eq) eqs'
   525                           o single o pr_eq) eqs'
   536                   )
   526                   )
   537               | pr_eqs _ (eqs as eq :: eqs') =
   527               | pr_eqs _ (eqs as eq :: eqs') =
   538                   let
   528                   let
   539                     val consts = map_filter
   529                     val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) [];
   540                       (fn c => if (is_some o syntax_const) c
       
   541                         then NONE else (SOME o Long_Name.base_name o deresolve) c)
       
   542                         (fold Code_Thingol.add_constnames (map (snd o fst) eqs) []);
       
   543                     val vars = reserved_names
   530                     val vars = reserved_names
   544                       |> Code_Printer.intro_vars consts;
   531                   |> Code_Printer.intro_base_names
       
   532                       (is_none o syntax_const) deresolve consts;
   545                     val dummy_parms = (map str o Code_Printer.aux_params vars o map (fst o fst)) eqs;
   533                     val dummy_parms = (map str o Code_Printer.aux_params vars o map (fst o fst)) eqs;
   546                   in
   534                   in
   547                     Pretty.block (
   535                     Pretty.block (
   548                       Pretty.breaks dummy_parms
   536                       Pretty.breaks dummy_parms
   549                       @ Pretty.brk 1
   537                       @ Pretty.brk 1