# HG changeset patch # User haftmann # Date 1246366440 -7200 # Node ID f172346ba8056c21a4976f32bb454eca53dd8b34 # Parent 00878e406bf5ab641cdfbc71b0d0177dd78c2277 simplified binding concept diff -r 00878e406bf5 -r f172346ba805 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Tue Jun 30 14:53:59 2009 +0200 +++ b/src/Tools/Code/code_haskell.ML Tue Jun 30 14:54:00 2009 +0200 @@ -25,10 +25,8 @@ fun pr_haskell_bind pr_term = let - fun pr_bind ((NONE, NONE), _) = str "_" - | pr_bind ((SOME v, NONE), _) = str v - | pr_bind ((NONE, SOME p), _) = p - | pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p]; + fun pr_bind (NONE, _) = str "_" + | pr_bind (SOME p, _) = p; in gen_pr_bind pr_bind pr_term end; fun pr_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const @@ -72,9 +70,8 @@ (str o Code_Printer.lookup_var vars) v | pr_term tyvars thm vars fxy (t as _ `|=> _) = let - val (binds, t') = Code_Thingol.unfold_abs t; - fun pr ((v, pat), ty) = pr_bind tyvars thm BR ((SOME v, pat), ty); - val (ps, vars') = fold_map pr binds vars; + val (binds, t') = Code_Thingol.unfold_pat_abs t; + val (ps, vars') = fold_map (pr_bind tyvars thm BR) binds vars; in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm vars' NOBR t') end | pr_term tyvars thm vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0 @@ -103,7 +100,7 @@ val (binds, body) = Code_Thingol.unfold_let (ICase cases); fun pr ((pat, ty), t) vars = vars - |> pr_bind tyvars thm BR ((NONE, SOME pat), ty) + |> pr_bind tyvars thm BR (SOME pat, ty) |>> (fn p => semicolon [p, str "=", pr_term tyvars thm vars NOBR t]) val (ps, vars') = fold_map pr binds vars; in brackify_block fxy (str "let {") @@ -114,7 +111,7 @@ let fun pr (pat, body) = let - val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars; + val (p, vars') = pr_bind tyvars thm NOBR (SOME pat, ty) vars; in semicolon [p, str "->", pr_term tyvars thm vars' NOBR body] end; in brackify_block fxy (concat [str "case", pr_term tyvars thm vars NOBR t, str "of", str "{"]) @@ -240,8 +237,6 @@ end | pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) = let - val split_abs_pure = (fn (v, _) `|=> t => SOME (v, t) | _ => NONE); - val unfold_abs_pure = Code_Thingol.unfoldr split_abs_pure; val tyvars = Code_Printer.intro_vars (map fst vs) init_syms; fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam of NONE => semicolon [ @@ -255,7 +250,7 @@ val const = if (is_some o syntax_const) c_inst_name then NONE else (SOME o Long_Name.base_name o deresolve) c_inst_name; val proto_rhs = Code_Thingol.eta_expand k (c_inst, []); - val (vs, rhs) = unfold_abs_pure proto_rhs; + val (vs, rhs) = (apfst o map) fst (Code_Thingol.unfold_abs proto_rhs); val vars = init_syms |> Code_Printer.intro_vars (the_list const) |> Code_Printer.intro_vars vs; @@ -447,16 +442,16 @@ fun pretty_haskell_monad c_bind = let - fun dest_bind t1 t2 = case Code_Thingol.split_abs t2 - of SOME (((v, pat), ty), t') => - SOME ((SOME (((SOME v, pat), ty), true), t1), t') + fun dest_bind t1 t2 = case Code_Thingol.split_pat_abs t2 + of SOME ((some_pat, ty), t') => + SOME ((SOME ((some_pat, ty), true), t1), t') | NONE => NONE; fun dest_monad c_bind_name (IConst (c, _) `$ t1 `$ t2) = if c = c_bind_name then dest_bind t1 t2 else NONE | dest_monad _ t = case Code_Thingol.split_let t of SOME (((pat, ty), tbind), t') => - SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t') + SOME ((SOME ((SOME pat, ty), false), tbind), t') | NONE => NONE; fun implode_monad c_bind_name = Code_Thingol.unfoldr (dest_monad c_bind_name); fun pr_monad pr_bind pr (NONE, t) vars = diff -r 00878e406bf5 -r f172346ba805 src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Tue Jun 30 14:53:59 2009 +0200 +++ b/src/Tools/Code/code_ml.ML Tue Jun 30 14:54:00 2009 +0200 @@ -94,9 +94,9 @@ [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2]) | pr_term is_closure thm vars fxy (t as _ `|=> _) = let - val (binds, t') = Code_Thingol.unfold_abs t; - fun pr ((v, pat), ty) = - pr_bind is_closure thm NOBR ((SOME v, pat), ty) + val (binds, t') = Code_Thingol.unfold_pat_abs t; + fun pr (some_pat, ty) = + pr_bind is_closure thm NOBR (some_pat, ty) #>> (fn p => concat [str "fn", p, str "=>"]); val (ps, vars') = fold_map pr binds vars; in brackets (ps @ [pr_term is_closure thm vars' NOBR t']) end @@ -122,17 +122,15 @@ :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts and pr_app is_closure thm vars = gen_pr_app (pr_app' is_closure) (pr_term is_closure) syntax_const thm vars - and pr_bind' ((NONE, NONE), _) = str "_" - | pr_bind' ((SOME v, NONE), _) = str v - | pr_bind' ((NONE, SOME p), _) = p - | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p] + and pr_bind' (NONE, _) = str "_" + | pr_bind' (SOME p, _) = p and pr_bind is_closure = gen_pr_bind pr_bind' (pr_term is_closure) and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) = let val (binds, body) = Code_Thingol.unfold_let (ICase cases); fun pr ((pat, ty), t) vars = vars - |> pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) + |> pr_bind is_closure thm NOBR (SOME pat, ty) |>> (fn p => semicolon [str "val", p, str "=", pr_term is_closure thm vars NOBR t]) val (ps, vars') = fold_map pr binds vars; in @@ -146,7 +144,7 @@ let fun pr delim (pat, body) = let - val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars; + val (p, vars') = pr_bind is_closure thm NOBR (SOME pat, ty) vars; in concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR body] end; @@ -403,9 +401,8 @@ brackify fxy [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2]) | pr_term is_closure thm vars fxy (t as _ `|=> _) = let - val (binds, t') = Code_Thingol.unfold_abs t; - fun pr ((v, pat), ty) = pr_bind is_closure thm BR ((SOME v, pat), ty); - val (ps, vars') = fold_map pr binds vars; + val (binds, t') = Code_Thingol.unfold_pat_abs t; + val (ps, vars') = fold_map (pr_bind is_closure thm BR) binds vars; in brackets (str "fun" :: ps @ str "->" @@ pr_term is_closure thm vars' NOBR t') end | pr_term is_closure thm vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0 of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c) @@ -427,17 +424,15 @@ :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts) and pr_app is_closure = gen_pr_app (pr_app' is_closure) (pr_term is_closure) syntax_const - and pr_bind' ((NONE, NONE), _) = str "_" - | pr_bind' ((SOME v, NONE), _) = str v - | pr_bind' ((NONE, SOME p), _) = p - | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v] + and pr_bind' (NONE, _) = str "_" + | pr_bind' (SOME p, _) = p and pr_bind is_closure = gen_pr_bind pr_bind' (pr_term is_closure) and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) = let val (binds, body) = Code_Thingol.unfold_let (ICase cases); fun pr ((pat, ty), t) vars = vars - |> pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) + |> pr_bind is_closure thm NOBR (SOME pat, ty) |>> (fn p => concat [str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"]) val (ps, vars') = fold_map pr binds vars; @@ -449,7 +444,7 @@ let fun pr delim (pat, body) = let - val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars; + val (p, vars') = pr_bind is_closure thm NOBR (SOME pat, ty) vars; in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR body] end; in brackets ( diff -r 00878e406bf5 -r f172346ba805 src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Tue Jun 30 14:53:59 2009 +0200 +++ b/src/Tools/Code/code_printer.ML Tue Jun 30 14:54:00 2009 +0200 @@ -68,10 +68,10 @@ -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T) -> (string -> const_syntax option) -> thm -> var_ctxt -> fixity -> const * iterm list -> Pretty.T - val gen_pr_bind: ((string option * Pretty.T option) * itype -> Pretty.T) + val gen_pr_bind: (Pretty.T option * itype -> Pretty.T) -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T) -> thm -> fixity - -> (string option * iterm option) * itype -> var_ctxt -> Pretty.T * var_ctxt + -> iterm option * itype -> var_ctxt -> Pretty.T * var_ctxt val mk_name_module: Name.context -> string option -> (string -> string option) -> 'a Graph.T -> string -> string @@ -216,16 +216,14 @@ else pr_term thm vars fxy (Code_Thingol.eta_expand k app) end; -fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) ((v, pat), ty : itype) vars = +fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) (some_pat, ty : itype) vars = let - val vs = case pat + val vs = case some_pat of SOME pat => Code_Thingol.fold_varnames (insert (op =)) pat [] | NONE => []; - val vars' = intro_vars (the_list v) vars; - val vars'' = intro_vars vs vars'; - val v' = Option.map (lookup_var vars') v; - val pat' = Option.map (pr_term thm vars'' fxy) pat; - in (pr_bind ((v', pat'), ty), vars'') end; + val vars' = intro_vars vs vars; + val some_pat' = Option.map (pr_term thm vars' fxy) some_pat; + in (pr_bind (some_pat', ty), vars') end; (* mixfix syntax *) diff -r 00878e406bf5 -r f172346ba805 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Tue Jun 30 14:53:59 2009 +0200 +++ b/src/Tools/Code/code_thingol.ML Tue Jun 30 14:54:00 2009 +0200 @@ -40,13 +40,12 @@ val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a val unfold_fun: itype -> itype list * itype val unfold_app: iterm -> iterm * iterm list - val split_abs: iterm -> (((vname * iterm option) * itype) * iterm) option - val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm + val unfold_abs: iterm -> (vname * itype) list * iterm val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm + val split_pat_abs: iterm -> ((iterm option * itype) * iterm) option + val unfold_pat_abs: iterm -> (iterm option * itype) list * iterm val unfold_const_app: iterm -> (const * iterm list) option - val collapse_let: ((vname * itype) * iterm) * iterm - -> (iterm * itype) * (iterm * iterm) list val eta_expand: int -> const * iterm list -> iterm val contains_dictvar: iterm -> bool val locally_monomorphic: iterm -> bool @@ -139,14 +138,10 @@ (fn op `$ t => SOME t | _ => NONE); -val split_abs = - (fn (v, ty) `|=> (t as ICase (((IVar w, _), [(p, t')]), _)) => - if v = w then SOME (((v, SOME p), ty), t') else SOME (((v, NONE), ty), t) - | (v, ty) `|=> t => SOME (((v, NONE), ty), t) +val unfold_abs = unfoldr + (fn op `|=> t => SOME t | _ => NONE); -val unfold_abs = unfoldr split_abs; - val split_let = (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t) | _ => NONE); @@ -186,17 +181,17 @@ | add vs (ICase (_, t)) = add vs t; in add [] end; -fun collapse_let (((v, ty), se), be as ICase (((IVar w, _), ds), _)) = - let - fun exists_v t = fold_unbound_varnames (fn w => fn b => - b orelse v = w) t false; - in if v = w andalso forall (fn (t1, t2) => - exists_v t1 orelse not (exists_v t2)) ds - then ((se, ty), ds) - else ((se, ty), [(IVar v, be)]) - end - | collapse_let (((v, ty), se), be) = - ((se, ty), [(IVar v, be)]) +fun exists_var t v = fold_unbound_varnames (fn w => fn b => v = w orelse b) t false; + +val split_pat_abs = (fn (v, ty) `|=> t => (case t + of ICase (((IVar w, _), [(p, t')]), _) => + if v = w andalso (exists_var p v orelse not (exists_var t' v)) + then SOME ((SOME p, ty), t') + else SOME ((SOME (IVar v), ty), t) + | _ => SOME ((if exists_var t v then SOME (IVar v) else NONE, ty), t)) + | _ => NONE); + +val unfold_pat_abs = unfoldr split_pat_abs; fun eta_expand k (c as (_, (_, tys)), ts) = let