src/Tools/code/code_printer.ML
changeset 28708 a1a436f09ec6
parent 28690 fc51fa5efea1
child 30161 c26e515f1c29
     1.1 --- a/src/Tools/code/code_printer.ML	Tue Oct 28 17:53:46 2008 +0100
     1.2 +++ b/src/Tools/code/code_printer.ML	Wed Oct 29 11:33:40 2008 +0100
     1.3 @@ -43,12 +43,12 @@
     1.4      -> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list
     1.5    val simple_const_syntax: (int * ((fixity -> iterm -> Pretty.T)
     1.6      -> fixity -> (iterm * itype) list -> Pretty.T)) option -> const_syntax option
     1.7 -  val gen_pr_app: (thm -> bool -> Code_Name.var_ctxt -> const * iterm list -> Pretty.T list)
     1.8 -    -> (thm -> bool -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
     1.9 -    -> (string -> const_syntax option) -> (string -> bool) -> Code_Thingol.naming
    1.10 -    -> thm -> bool -> Code_Name.var_ctxt -> fixity -> const * iterm list -> Pretty.T
    1.11 +  val gen_pr_app: (thm -> Code_Name.var_ctxt -> const * iterm list -> Pretty.T list)
    1.12 +    -> (thm -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
    1.13 +    -> (string -> const_syntax option) -> Code_Thingol.naming
    1.14 +    -> thm -> Code_Name.var_ctxt -> fixity -> const * iterm list -> Pretty.T
    1.15    val gen_pr_bind: ((string option * Pretty.T option) * itype -> Pretty.T)
    1.16 -    -> (thm -> bool -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
    1.17 +    -> (thm -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
    1.18      -> thm -> fixity
    1.19      -> (string option * iterm option) * itype -> Code_Name.var_ctxt -> Pretty.T * Code_Name.var_ctxt
    1.20  
    1.21 @@ -127,26 +127,23 @@
    1.22  type tyco_syntax = int * ((fixity -> itype -> Pretty.T)
    1.23    -> fixity -> itype list -> Pretty.T);
    1.24  type const_syntax = int * ((Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
    1.25 -  -> Code_Thingol.naming -> thm -> bool -> Code_Name.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
    1.26 +  -> Code_Thingol.naming -> thm -> Code_Name.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
    1.27  
    1.28  fun simple_const_syntax x = (Option.map o apsnd)
    1.29 -  (fn pretty => fn pr => fn naming => fn thm => fn pat => fn vars => pretty (pr vars)) x;
    1.30 +  (fn pretty => fn pr => fn naming => fn thm => fn vars => pretty (pr vars)) x;
    1.31  
    1.32 -fun gen_pr_app pr_app pr_term syntax_const is_cons naming thm pat
    1.33 -    vars fxy (app as ((c, (_, tys)), ts)) =
    1.34 +fun gen_pr_app pr_app pr_term syntax_const naming thm vars fxy (app as ((c, (_, tys)), ts)) =
    1.35    case syntax_const c
    1.36 -   of NONE => if pat andalso not (is_cons c) then
    1.37 -        nerror thm "Non-constructor in pattern"
    1.38 -        else brackify fxy (pr_app thm pat vars app)
    1.39 +   of NONE => brackify fxy (pr_app thm vars app)
    1.40      | SOME (k, pr) =>
    1.41          let
    1.42 -          fun pr' fxy ts = pr (pr_term thm pat) naming thm pat vars fxy (ts ~~ curry Library.take k tys);
    1.43 +          fun pr' fxy ts = pr (pr_term thm) naming thm vars fxy (ts ~~ curry Library.take k tys);
    1.44          in if k = length ts
    1.45            then pr' fxy ts
    1.46          else if k < length ts
    1.47            then case chop k ts of (ts1, ts2) =>
    1.48 -            brackify fxy (pr' APP ts1 :: map (pr_term thm pat vars BR) ts2)
    1.49 -          else pr_term thm pat vars fxy (Code_Thingol.eta_expand k app)
    1.50 +            brackify fxy (pr' APP ts1 :: map (pr_term thm vars BR) ts2)
    1.51 +          else pr_term thm vars fxy (Code_Thingol.eta_expand k app)
    1.52          end;
    1.53  
    1.54  fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) ((v, pat), ty : itype) vars =
    1.55 @@ -157,7 +154,7 @@
    1.56      val vars' = Code_Name.intro_vars (the_list v) vars;
    1.57      val vars'' = Code_Name.intro_vars vs vars';
    1.58      val v' = Option.map (Code_Name.lookup_var vars') v;
    1.59 -    val pat' = Option.map (pr_term thm true vars'' fxy) pat;
    1.60 +    val pat' = Option.map (pr_term thm vars'' fxy) pat;
    1.61    in (pr_bind ((v', pat'), ty), vars'') end;
    1.62  
    1.63