# HG changeset patch # User haftmann # Date 1230391716 -3600 # Node ID f1ce1e2229c6a76f3ae7643e5511e93cc63a789c # Parent d4058295affbdc5b4194d57a2dfacec94b23df67# Parent 27cd8cce605e8074661e6c02cec14a1fa22e1fd5 merged diff -r d4058295affb -r f1ce1e2229c6 src/Tools/code/code_ml.ML --- a/src/Tools/code/code_ml.ML Sat Dec 27 14:57:30 2008 +0100 +++ b/src/Tools/code/code_ml.ML Sat Dec 27 16:28:36 2008 +0100 @@ -25,14 +25,14 @@ val target_OCaml = "OCaml"; datatype ml_stmt = - MLFuns of (string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)) list + MLFuns of ((string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)) * bool (*val flag*)) list | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list | MLClass of string * (vname * ((class * string) list * (string * itype) list)) | MLClassinst of string * ((class * (string * (vname * sort) list)) * ((class * (string * (string * dict list list))) list * ((string * const) * (thm * bool)) list)); -fun stmt_names_of (MLFuns fs) = map fst fs +fun stmt_names_of (MLFuns fs) = map (fst o fst) fs | stmt_names_of (MLDatas ds) = map fst ds | stmt_names_of (MLClass (c, _)) = [c] | stmt_names_of (MLClassinst (i, _)) = [i]; @@ -81,77 +81,82 @@ of NONE => pr_tycoexpr fxy (tyco, tys) | SOME (i, pr) => pr pr_typ fxy tys) | pr_typ fxy (ITyVar v) = str ("'" ^ v); - fun pr_term thm vars fxy (IConst c) = - pr_app thm vars fxy (c, []) - | pr_term thm vars fxy (IVar v) = + fun pr_term is_closure thm vars fxy (IConst c) = + pr_app is_closure thm vars fxy (c, []) + | pr_term is_closure thm vars fxy (IVar v) = str (Code_Name.lookup_var vars v) - | pr_term thm vars fxy (t as t1 `$ t2) = + | pr_term is_closure thm vars fxy (t as t1 `$ t2) = (case Code_Thingol.unfold_const_app t - of SOME c_ts => pr_app thm vars fxy c_ts - | NONE => - brackify fxy [pr_term thm vars NOBR t1, pr_term thm vars BR t2]) - | pr_term thm vars fxy (t as _ `|-> _) = + of SOME c_ts => pr_app is_closure thm vars fxy c_ts + | NONE => 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 thm NOBR ((SOME v, pat), ty) + pr_bind is_closure thm NOBR ((SOME v, pat), ty) #>> (fn p => concat [str "fn", p, str "=>"]); val (ps, vars') = fold_map pr binds vars; - in brackets (ps @ [pr_term thm vars' NOBR t']) end - | pr_term thm vars fxy (ICase (cases as (_, t0))) = + in brackets (ps @ [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) - then pr_case thm vars fxy cases - else pr_app thm vars fxy c_ts - | NONE => pr_case thm vars fxy cases) - and pr_app' thm vars (app as ((c, (iss, tys)), ts)) = - if is_cons c then let - val k = length tys - in if k < 2 then - (str o deresolve) c :: map (pr_term thm vars BR) ts - else if k = length ts then - [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term thm vars NOBR) ts)] - else [pr_term thm vars BR (Code_Thingol.eta_expand k app)] end else + then pr_case is_closure thm vars fxy cases + else pr_app is_closure thm vars fxy c_ts + | NONE => pr_case is_closure thm vars fxy cases) + and pr_app' is_closure thm vars (app as ((c, (iss, tys)), ts)) = + if is_cons c then + let + val k = length tys + in if k < 2 then + (str o deresolve) c :: map (pr_term is_closure thm vars BR) ts + else if k = length ts then + [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term is_closure thm vars NOBR) ts)] + else [pr_term is_closure thm vars BR (Code_Thingol.eta_expand k app)] end + else if is_closure c + then (str o deresolve) c @@ str "()" + else (str o deresolve) c - :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm vars BR) ts - and pr_app thm vars = gen_pr_app pr_app' pr_term syntax_const naming thm vars + :: (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 naming 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 thm = gen_pr_bind pr_bind' pr_term thm - and pr_case thm vars fxy (cases as ((_, [_]), _)) = + 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, t') = Code_Thingol.unfold_let (ICase cases); fun pr ((pat, ty), t) vars = vars - |> pr_bind thm NOBR ((NONE, SOME pat), ty) - |>> (fn p => semicolon [str "val", p, str "=", pr_term thm vars NOBR t]) + |> pr_bind is_closure thm NOBR ((NONE, 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 Pretty.chunks [ [str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block, - [str ("in"), Pretty.fbrk, pr_term thm vars' NOBR t'] |> Pretty.block, + [str ("in"), Pretty.fbrk, pr_term is_closure thm vars' NOBR t'] |> Pretty.block, str ("end") ] end - | pr_case thm vars fxy (((td, ty), b::bs), _) = + | pr_case is_closure thm vars fxy (((td, ty), b::bs), _) = let fun pr delim (pat, t) = let - val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars; + val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars; in - concat [str delim, p, str "=>", pr_term thm vars' NOBR t] + concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR t] end; in (Pretty.enclose "(" ")" o single o brackify fxy) ( str "case" - :: pr_term thm vars NOBR td + :: pr_term is_closure thm vars NOBR td :: pr "of" b :: map (pr "|") bs ) end - | pr_case thm vars fxy ((_, []), _) = str "raise Fail \"empty case\""; + | pr_case is_closure thm vars fxy ((_, []), _) = str "raise Fail \"empty case\""; fun pr_stmt (MLFuns (funns as (funn :: funns'))) = let val definer = @@ -162,13 +167,13 @@ | mk 0 vs = if (null o filter_out (null o snd)) vs then "val" else "fun" | mk k _ = "fun"; - fun chk (_, ((vs, ty), eqs)) NONE = SOME (mk (no_args ty eqs) vs) - | chk (_, ((vs, ty), eqs)) (SOME defi) = + fun chk ((_, ((vs, ty), eqs)), _) NONE = SOME (mk (no_args ty eqs) vs) + | chk ((_, ((vs, ty), eqs)), _) (SOME defi) = if defi = mk (no_args ty eqs) vs then SOME defi else error ("Mixing simultaneous vals and funs not implemented: " - ^ commas (map (labelled_name o fst) funns)); + ^ commas (map (labelled_name o fst o fst) funns)); in the (fold chk funns NONE) end; - fun pr_funn definer (name, ((vs, ty), [])) = + fun pr_funn definer ((name, ((vs, ty), [])), _) = let val vs_dict = filter_out (null o snd) vs; val n = length vs_dict + (length o fst o Code_Thingol.unfold_fun) ty; @@ -185,7 +190,7 @@ @@ str (exc_str ^ ")") ) end - | pr_funn definer (name, ((vs, ty), eqs as eq :: eqs')) = + | pr_funn definer ((name, ((vs, ty), eqs as eq :: eqs')), _) = let val vs_dict = filter_out (null o snd) vs; val shift = if null eqs' then I else @@ -207,8 +212,8 @@ then [str ":", pr_typ NOBR ty] else pr_tyvar_dicts vs_dict - @ map (pr_term thm vars BR) ts) - @ [str "=", pr_term thm vars NOBR t] + @ map (pr_term (K false) thm vars BR) ts) + @ [str "=", pr_term (K false) thm vars NOBR t] ) end in @@ -301,7 +306,7 @@ concat [ (str o pr_label_classparam) classparam, str "=", - pr_app thm reserved_names NOBR (c_inst, []) + pr_app (K false) thm reserved_names NOBR (c_inst, []) ]; in semicolon ([ @@ -374,68 +379,71 @@ of NONE => pr_tycoexpr fxy (tyco, tys) | SOME (i, pr) => pr pr_typ fxy tys) | pr_typ fxy (ITyVar v) = str ("'" ^ v); - fun pr_term thm vars fxy (IConst c) = - pr_app thm vars fxy (c, []) - | pr_term thm vars fxy (IVar v) = + fun pr_term is_closure thm vars fxy (IConst c) = + pr_app is_closure thm vars fxy (c, []) + | pr_term is_closure thm vars fxy (IVar v) = str (Code_Name.lookup_var vars v) - | pr_term thm vars fxy (t as t1 `$ t2) = + | pr_term is_closure thm vars fxy (t as t1 `$ t2) = (case Code_Thingol.unfold_const_app t - of SOME c_ts => pr_app thm vars fxy c_ts + of SOME c_ts => pr_app is_closure thm vars fxy c_ts | NONE => - brackify fxy [pr_term thm vars NOBR t1, pr_term thm vars BR t2]) - | pr_term thm vars fxy (t as _ `|-> _) = + 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 thm BR ((SOME v, pat), ty); + fun pr ((v, pat), ty) = pr_bind is_closure thm BR ((SOME v, pat), ty); val (ps, vars') = fold_map pr binds vars; - in brackets (str "fun" :: ps @ str "->" @@ pr_term thm vars' NOBR t') end - | pr_term thm vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0 + 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) - then pr_case thm vars fxy cases - else pr_app thm vars fxy c_ts - | NONE => pr_case thm vars fxy cases) - and pr_app' thm vars (app as ((c, (iss, tys)), ts)) = + then pr_case is_closure thm vars fxy cases + else pr_app is_closure thm vars fxy c_ts + | NONE => pr_case is_closure thm vars fxy cases) + and pr_app' is_closure thm vars (app as ((c, (iss, tys)), ts)) = if is_cons c then if length tys = length ts then case ts of [] => [(str o deresolve) c] - | [t] => [(str o deresolve) c, pr_term thm vars BR t] + | [t] => [(str o deresolve) c, pr_term is_closure thm vars BR t] | _ => [(str o deresolve) c, Pretty.enum "," "(" ")" - (map (pr_term thm vars NOBR) ts)] - else [pr_term thm vars BR (Code_Thingol.eta_expand (length tys) app)] + (map (pr_term is_closure thm vars NOBR) ts)] + else [pr_term is_closure thm vars BR (Code_Thingol.eta_expand (length tys) app)] + else if is_closure c + then (str o deresolve) c @@ str "()" else (str o deresolve) c - :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm vars BR) ts) - and pr_app thm vars = gen_pr_app pr_app' pr_term syntax_const naming thm vars + :: ((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 naming 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 thm = gen_pr_bind pr_bind' pr_term thm - and pr_case thm vars fxy (cases as ((_, [_]), _)) = + 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, t') = Code_Thingol.unfold_let (ICase cases); fun pr ((pat, ty), t) vars = vars - |> pr_bind thm NOBR ((NONE, SOME pat), ty) + |> pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) |>> (fn p => concat - [str "let", p, str "=", pr_term thm vars NOBR t, str "in"]) + [str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"]) val (ps, vars') = fold_map pr binds vars; - in Pretty.chunks (ps @| pr_term thm vars' NOBR t') end - | pr_case thm vars fxy (((td, ty), b::bs), _) = + in Pretty.chunks (ps @| pr_term is_closure thm vars' NOBR t') end + | pr_case is_closure thm vars fxy (((td, ty), b::bs), _) = let fun pr delim (pat, t) = let - val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars; - in concat [str delim, p, str "->", pr_term thm vars' NOBR t] end; + val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars; + in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR t] end; in (Pretty.enclose "(" ")" o single o brackify fxy) ( str "match" - :: pr_term thm vars NOBR td + :: pr_term is_closure thm vars NOBR td :: pr "with" b :: map (pr "|") bs ) end - | pr_case thm vars fxy ((_, []), _) = str "failwith \"empty case\""; + | pr_case is_closure thm vars fxy ((_, []), _) = str "failwith \"empty case\""; fun fish_params vars eqs = let fun fish_param _ (w as SOME _) = w @@ -462,9 +470,9 @@ |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames) (insert (op =)) ts []); in concat [ - (Pretty.block o Pretty.commas) (map (pr_term thm vars NOBR) ts), + (Pretty.block o Pretty.commas) (map (pr_term (K false) thm vars NOBR) ts), str "->", - pr_term thm vars NOBR t + pr_term (K false) thm vars NOBR t ] end; fun pr_eqs name ty [] = let @@ -491,9 +499,9 @@ (insert (op =)) ts []); in concat ( - map (pr_term thm vars BR) ts + map (pr_term (K false) thm vars BR) ts @ str "=" - @@ pr_term thm vars NOBR t + @@ pr_term (K false) thm vars NOBR t ) end | pr_eqs _ _ (eqs as (eq as (([_], _), _)) :: eqs') = @@ -533,7 +541,7 @@ o single o pr_eq) eqs' ) end; - fun pr_funn definer (name, ((vs, ty), eqs)) = + fun pr_funn definer ((name, ((vs, ty), eqs)), _) = concat ( str definer :: (str o deresolve) name @@ -613,7 +621,7 @@ concat [ (str o deresolve) classparam, str "=", - pr_app thm reserved_names NOBR (c_inst, []) + pr_app (K false) thm reserved_names NOBR (c_inst, []) ]; in concat ( @@ -725,7 +733,7 @@ fold_map (fn (name, Code_Thingol.Fun (_, stmt)) => map_nsp_fun_yield (mk_name_stmt false name) #>> - rpair (name, stmt |> apsnd (filter (snd o snd))) + rpair ((name, stmt |> apsnd (filter (snd o snd))), false) | (name, _) => error ("Function block containing illegal statement: " ^ labelled_name name) ) stmts