simplified binding concept
authorhaftmann
Tue Jun 30 14:54:00 2009 +0200 (2009-06-30)
changeset 31874f172346ba805
parent 31873 00878e406bf5
child 31875 3b08dcd74229
simplified binding concept
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_printer.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Tools/Code/code_haskell.ML	Tue Jun 30 14:53:59 2009 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Tue Jun 30 14:54:00 2009 +0200
     1.3 @@ -25,10 +25,8 @@
     1.4  
     1.5  fun pr_haskell_bind pr_term =
     1.6    let
     1.7 -    fun pr_bind ((NONE, NONE), _) = str "_"
     1.8 -      | pr_bind ((SOME v, NONE), _) = str v
     1.9 -      | pr_bind ((NONE, SOME p), _) = p
    1.10 -      | pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p];
    1.11 +    fun pr_bind (NONE, _) = str "_"
    1.12 +      | pr_bind (SOME p, _) = p;
    1.13    in gen_pr_bind pr_bind pr_term end;
    1.14  
    1.15  fun pr_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const
    1.16 @@ -72,9 +70,8 @@
    1.17            (str o Code_Printer.lookup_var vars) v
    1.18        | pr_term tyvars thm vars fxy (t as _ `|=> _) =
    1.19            let
    1.20 -            val (binds, t') = Code_Thingol.unfold_abs t;
    1.21 -            fun pr ((v, pat), ty) = pr_bind tyvars thm BR ((SOME v, pat), ty);
    1.22 -            val (ps, vars') = fold_map pr binds vars;
    1.23 +            val (binds, t') = Code_Thingol.unfold_pat_abs t;
    1.24 +            val (ps, vars') = fold_map (pr_bind tyvars thm BR) binds vars;
    1.25            in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm vars' NOBR t') end
    1.26        | pr_term tyvars thm vars fxy (ICase (cases as (_, t0))) =
    1.27            (case Code_Thingol.unfold_const_app t0
    1.28 @@ -103,7 +100,7 @@
    1.29              val (binds, body) = Code_Thingol.unfold_let (ICase cases);
    1.30              fun pr ((pat, ty), t) vars =
    1.31                vars
    1.32 -              |> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
    1.33 +              |> pr_bind tyvars thm BR (SOME pat, ty)
    1.34                |>> (fn p => semicolon [p, str "=", pr_term tyvars thm vars NOBR t])
    1.35              val (ps, vars') = fold_map pr binds vars;
    1.36            in brackify_block fxy (str "let {")
    1.37 @@ -114,7 +111,7 @@
    1.38            let
    1.39              fun pr (pat, body) =
    1.40                let
    1.41 -                val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
    1.42 +                val (p, vars') = pr_bind tyvars thm NOBR (SOME pat, ty) vars;
    1.43                in semicolon [p, str "->", pr_term tyvars thm vars' NOBR body] end;
    1.44            in brackify_block fxy
    1.45              (concat [str "case", pr_term tyvars thm vars NOBR t, str "of", str "{"])
    1.46 @@ -240,8 +237,6 @@
    1.47            end
    1.48        | pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
    1.49            let
    1.50 -            val split_abs_pure = (fn (v, _) `|=> t => SOME (v, t) | _ => NONE);
    1.51 -            val unfold_abs_pure = Code_Thingol.unfoldr split_abs_pure;
    1.52              val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
    1.53              fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam
    1.54               of NONE => semicolon [
    1.55 @@ -255,7 +250,7 @@
    1.56                      val const = if (is_some o syntax_const) c_inst_name
    1.57                        then NONE else (SOME o Long_Name.base_name o deresolve) c_inst_name;
    1.58                      val proto_rhs = Code_Thingol.eta_expand k (c_inst, []);
    1.59 -                    val (vs, rhs) = unfold_abs_pure proto_rhs;
    1.60 +                    val (vs, rhs) = (apfst o map) fst (Code_Thingol.unfold_abs proto_rhs);
    1.61                      val vars = init_syms
    1.62                        |> Code_Printer.intro_vars (the_list const)
    1.63                        |> Code_Printer.intro_vars vs;
    1.64 @@ -447,16 +442,16 @@
    1.65  
    1.66  fun pretty_haskell_monad c_bind =
    1.67    let
    1.68 -    fun dest_bind t1 t2 = case Code_Thingol.split_abs t2
    1.69 -     of SOME (((v, pat), ty), t') =>
    1.70 -          SOME ((SOME (((SOME v, pat), ty), true), t1), t')
    1.71 +    fun dest_bind t1 t2 = case Code_Thingol.split_pat_abs t2
    1.72 +     of SOME ((some_pat, ty), t') =>
    1.73 +          SOME ((SOME ((some_pat, ty), true), t1), t')
    1.74        | NONE => NONE;
    1.75      fun dest_monad c_bind_name (IConst (c, _) `$ t1 `$ t2) =
    1.76            if c = c_bind_name then dest_bind t1 t2
    1.77            else NONE
    1.78        | dest_monad _ t = case Code_Thingol.split_let t
    1.79           of SOME (((pat, ty), tbind), t') =>
    1.80 -              SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')
    1.81 +              SOME ((SOME ((SOME pat, ty), false), tbind), t')
    1.82            | NONE => NONE;
    1.83      fun implode_monad c_bind_name = Code_Thingol.unfoldr (dest_monad c_bind_name);
    1.84      fun pr_monad pr_bind pr (NONE, t) vars =
     2.1 --- a/src/Tools/Code/code_ml.ML	Tue Jun 30 14:53:59 2009 +0200
     2.2 +++ b/src/Tools/Code/code_ml.ML	Tue Jun 30 14:54:00 2009 +0200
     2.3 @@ -94,9 +94,9 @@
     2.4                 [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2])
     2.5        | pr_term is_closure thm vars fxy (t as _ `|=> _) =
     2.6            let
     2.7 -            val (binds, t') = Code_Thingol.unfold_abs t;
     2.8 -            fun pr ((v, pat), ty) =
     2.9 -              pr_bind is_closure thm NOBR ((SOME v, pat), ty)
    2.10 +            val (binds, t') = Code_Thingol.unfold_pat_abs t;
    2.11 +            fun pr (some_pat, ty) =
    2.12 +              pr_bind is_closure thm NOBR (some_pat, ty)
    2.13                #>> (fn p => concat [str "fn", p, str "=>"]);
    2.14              val (ps, vars') = fold_map pr binds vars;
    2.15            in brackets (ps @ [pr_term is_closure thm vars' NOBR t']) end
    2.16 @@ -122,17 +122,15 @@
    2.17            :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts
    2.18      and pr_app is_closure thm vars = gen_pr_app (pr_app' is_closure) (pr_term is_closure)
    2.19        syntax_const thm vars
    2.20 -    and pr_bind' ((NONE, NONE), _) = str "_"
    2.21 -      | pr_bind' ((SOME v, NONE), _) = str v
    2.22 -      | pr_bind' ((NONE, SOME p), _) = p
    2.23 -      | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
    2.24 +    and pr_bind' (NONE, _) = str "_"
    2.25 +      | pr_bind' (SOME p, _) = p
    2.26      and pr_bind is_closure = gen_pr_bind pr_bind' (pr_term is_closure)
    2.27      and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) =
    2.28            let
    2.29              val (binds, body) = Code_Thingol.unfold_let (ICase cases);
    2.30              fun pr ((pat, ty), t) vars =
    2.31                vars
    2.32 -              |> pr_bind is_closure thm NOBR ((NONE, SOME pat), ty)
    2.33 +              |> pr_bind is_closure thm NOBR (SOME pat, ty)
    2.34                |>> (fn p => semicolon [str "val", p, str "=", pr_term is_closure thm vars NOBR t])
    2.35              val (ps, vars') = fold_map pr binds vars;
    2.36            in
    2.37 @@ -146,7 +144,7 @@
    2.38            let
    2.39              fun pr delim (pat, body) =
    2.40                let
    2.41 -                val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
    2.42 +                val (p, vars') = pr_bind is_closure thm NOBR (SOME pat, ty) vars;
    2.43                in
    2.44                  concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR body]
    2.45                end;
    2.46 @@ -403,9 +401,8 @@
    2.47                  brackify fxy [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2])
    2.48        | pr_term is_closure thm vars fxy (t as _ `|=> _) =
    2.49            let
    2.50 -            val (binds, t') = Code_Thingol.unfold_abs t;
    2.51 -            fun pr ((v, pat), ty) = pr_bind is_closure thm BR ((SOME v, pat), ty);
    2.52 -            val (ps, vars') = fold_map pr binds vars;
    2.53 +            val (binds, t') = Code_Thingol.unfold_pat_abs t;
    2.54 +            val (ps, vars') = fold_map (pr_bind is_closure thm BR) binds vars;
    2.55            in brackets (str "fun" :: ps @ str "->" @@ pr_term is_closure thm vars' NOBR t') end
    2.56        | pr_term is_closure thm vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0
    2.57             of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
    2.58 @@ -427,17 +424,15 @@
    2.59          :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts)
    2.60      and pr_app is_closure = gen_pr_app (pr_app' is_closure) (pr_term is_closure)
    2.61        syntax_const
    2.62 -    and pr_bind' ((NONE, NONE), _) = str "_"
    2.63 -      | pr_bind' ((SOME v, NONE), _) = str v
    2.64 -      | pr_bind' ((NONE, SOME p), _) = p
    2.65 -      | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v]
    2.66 +    and pr_bind' (NONE, _) = str "_"
    2.67 +      | pr_bind' (SOME p, _) = p
    2.68      and pr_bind is_closure = gen_pr_bind pr_bind' (pr_term is_closure)
    2.69      and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) =
    2.70            let
    2.71              val (binds, body) = Code_Thingol.unfold_let (ICase cases);
    2.72              fun pr ((pat, ty), t) vars =
    2.73                vars
    2.74 -              |> pr_bind is_closure thm NOBR ((NONE, SOME pat), ty)
    2.75 +              |> pr_bind is_closure thm NOBR (SOME pat, ty)
    2.76                |>> (fn p => concat
    2.77                    [str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"])
    2.78              val (ps, vars') = fold_map pr binds vars;
    2.79 @@ -449,7 +444,7 @@
    2.80            let
    2.81              fun pr delim (pat, body) =
    2.82                let
    2.83 -                val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
    2.84 +                val (p, vars') = pr_bind is_closure thm NOBR (SOME pat, ty) vars;
    2.85                in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR body] end;
    2.86            in
    2.87              brackets (
     3.1 --- a/src/Tools/Code/code_printer.ML	Tue Jun 30 14:53:59 2009 +0200
     3.2 +++ b/src/Tools/Code/code_printer.ML	Tue Jun 30 14:54:00 2009 +0200
     3.3 @@ -68,10 +68,10 @@
     3.4      -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
     3.5      -> (string -> const_syntax option)
     3.6      -> thm -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
     3.7 -  val gen_pr_bind: ((string option * Pretty.T option) * itype -> Pretty.T)
     3.8 +  val gen_pr_bind: (Pretty.T option * itype -> Pretty.T)
     3.9      -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
    3.10      -> thm -> fixity
    3.11 -    -> (string option * iterm option) * itype -> var_ctxt -> Pretty.T * var_ctxt
    3.12 +    -> iterm option * itype -> var_ctxt -> Pretty.T * var_ctxt
    3.13  
    3.14    val mk_name_module: Name.context -> string option -> (string -> string option)
    3.15      -> 'a Graph.T -> string -> string
    3.16 @@ -216,16 +216,14 @@
    3.17            else pr_term thm vars fxy (Code_Thingol.eta_expand k app)
    3.18          end;
    3.19  
    3.20 -fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) ((v, pat), ty : itype) vars =
    3.21 +fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) (some_pat, ty : itype) vars =
    3.22    let
    3.23 -    val vs = case pat
    3.24 +    val vs = case some_pat
    3.25       of SOME pat => Code_Thingol.fold_varnames (insert (op =)) pat []
    3.26        | NONE => [];
    3.27 -    val vars' = intro_vars (the_list v) vars;
    3.28 -    val vars'' = intro_vars vs vars';
    3.29 -    val v' = Option.map (lookup_var vars') v;
    3.30 -    val pat' = Option.map (pr_term thm vars'' fxy) pat;
    3.31 -  in (pr_bind ((v', pat'), ty), vars'') end;
    3.32 +    val vars' = intro_vars vs vars;
    3.33 +    val some_pat' = Option.map (pr_term thm vars' fxy) some_pat;
    3.34 +  in (pr_bind (some_pat', ty), vars') end;
    3.35  
    3.36  
    3.37  (* mixfix syntax *)
     4.1 --- a/src/Tools/Code/code_thingol.ML	Tue Jun 30 14:53:59 2009 +0200
     4.2 +++ b/src/Tools/Code/code_thingol.ML	Tue Jun 30 14:54:00 2009 +0200
     4.3 @@ -40,13 +40,12 @@
     4.4    val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a
     4.5    val unfold_fun: itype -> itype list * itype
     4.6    val unfold_app: iterm -> iterm * iterm list
     4.7 -  val split_abs: iterm -> (((vname * iterm option) * itype) * iterm) option
     4.8 -  val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm
     4.9 +  val unfold_abs: iterm -> (vname * itype) list * iterm
    4.10    val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option
    4.11    val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm
    4.12 +  val split_pat_abs: iterm -> ((iterm option * itype) * iterm) option
    4.13 +  val unfold_pat_abs: iterm -> (iterm option * itype) list * iterm
    4.14    val unfold_const_app: iterm -> (const * iterm list) option
    4.15 -  val collapse_let: ((vname * itype) * iterm) * iterm
    4.16 -    -> (iterm * itype) * (iterm * iterm) list
    4.17    val eta_expand: int -> const * iterm list -> iterm
    4.18    val contains_dictvar: iterm -> bool
    4.19    val locally_monomorphic: iterm -> bool
    4.20 @@ -139,14 +138,10 @@
    4.21    (fn op `$ t => SOME t
    4.22      | _ => NONE);
    4.23  
    4.24 -val split_abs =
    4.25 -  (fn (v, ty) `|=> (t as ICase (((IVar w, _), [(p, t')]), _)) =>
    4.26 -        if v = w then SOME (((v, SOME p), ty), t') else SOME (((v, NONE), ty), t)
    4.27 -    | (v, ty) `|=> t => SOME (((v, NONE), ty), t)
    4.28 +val unfold_abs = unfoldr
    4.29 +  (fn op `|=> t => SOME t
    4.30      | _ => NONE);
    4.31  
    4.32 -val unfold_abs = unfoldr split_abs;
    4.33 -
    4.34  val split_let = 
    4.35    (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
    4.36      | _ => NONE);
    4.37 @@ -186,17 +181,17 @@
    4.38        | add vs (ICase (_, t)) = add vs t;
    4.39    in add [] end;
    4.40  
    4.41 -fun collapse_let (((v, ty), se), be as ICase (((IVar w, _), ds), _)) =
    4.42 -      let
    4.43 -        fun exists_v t = fold_unbound_varnames (fn w => fn b =>
    4.44 -          b orelse v = w) t false;
    4.45 -      in if v = w andalso forall (fn (t1, t2) =>
    4.46 -        exists_v t1 orelse not (exists_v t2)) ds
    4.47 -        then ((se, ty), ds)
    4.48 -        else ((se, ty), [(IVar v, be)])
    4.49 -      end
    4.50 -  | collapse_let (((v, ty), se), be) =
    4.51 -      ((se, ty), [(IVar v, be)])
    4.52 +fun exists_var t v = fold_unbound_varnames (fn w => fn b => v = w orelse b) t false;
    4.53 +
    4.54 +val split_pat_abs = (fn (v, ty) `|=> t => (case t
    4.55 +   of ICase (((IVar w, _), [(p, t')]), _) =>
    4.56 +        if v = w andalso (exists_var p v orelse not (exists_var t' v))
    4.57 +        then SOME ((SOME p, ty), t')
    4.58 +        else SOME ((SOME (IVar v), ty), t)
    4.59 +    | _ => SOME ((if exists_var t v then SOME (IVar v) else NONE, ty), t))
    4.60 +  | _ => NONE);
    4.61 +
    4.62 +val unfold_pat_abs = unfoldr split_pat_abs;
    4.63  
    4.64  fun eta_expand k (c as (_, (_, tys)), ts) =
    4.65    let