# HG changeset patch # User haftmann # Date 1230553433 -3600 # Node ID ee8572f3bb5710dd4b189e2f549d9442bd16984a # Parent ff41885a12346968d25fb38d9ebea7725eea979c eliminated fun/val confusion diff -r ff41885a1234 -r ee8572f3bb57 src/Tools/code/code_ml.ML --- a/src/Tools/code/code_ml.ML Sun Dec 28 14:41:47 2008 -0800 +++ b/src/Tools/code/code_ml.ML Mon Dec 29 13:23:53 2008 +0100 @@ -1,5 +1,4 @@ (* Title: Tools/code/code_ml.ML - ID: $Id$ Author: Florian Haftmann, TU Muenchen Serializer for SML and OCaml. @@ -25,17 +24,21 @@ val target_OCaml = "OCaml"; datatype ml_stmt = - MLFuns of ((string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)) * bool (*val flag*)) list + MLExc of string * int + | MLVal of string * ((typscheme * iterm) * (thm * bool)) + | MLFuns of (string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)) list * string 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 o fst) fs +fun stmt_names_of (MLExc (name, _)) = [name] + | stmt_names_of (MLVal (name, _)) = [name] + | stmt_names_of (MLFuns (fs, _)) = map fst fs | stmt_names_of (MLDatas ds) = map fst ds - | stmt_names_of (MLClass (c, _)) = [c] - | stmt_names_of (MLClassinst (i, _)) = [i]; + | stmt_names_of (MLClass (name, _)) = [name] + | stmt_names_of (MLClassinst (name, _)) = [name]; (** SML serailizer **) @@ -157,73 +160,83 @@ ) end | pr_case is_closure thm vars fxy ((_, []), _) = str "raise Fail \"empty case\""; - fun pr_stmt (MLFuns (funns as (funn :: funns'))) = + fun pr_stmt (MLExc (name, n)) = + let + val exc_str = + (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name; + in + concat ( + str (if n = 0 then "val" else "fun") + :: (str o deresolve) name + :: map str (replicate n "_") + @ str "=" + :: str "raise" + :: str "(Fail" + @@ str (exc_str ^ ")") + ) + end + | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) = let - val definer = + val consts = map_filter + (fn c => if (is_some o syntax_const) c + then NONE else (SOME o NameSpace.base o deresolve) c) + (Code_Thingol.fold_constnames (insert (op =)) t []); + val vars = reserved_names + |> Code_Name.intro_vars consts; + in + concat [ + str "val", + (str o deresolve) name, + str ":", + pr_typ NOBR ty, + str "=", + pr_term (K false) thm vars NOBR t + ] + end + | pr_stmt (MLFuns (funn :: funns, pseudo_funs)) = + let + fun pr_funn definer (name, ((vs, ty), eqs as eq :: eqs')) = let - fun no_args _ (((ts, _), _) :: _) = length ts - | no_args ty [] = (length o fst o Code_Thingol.unfold_fun) ty; - fun mk 0 [] = "val" - | 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) = - 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 o fst) funns)); - in the (fold chk funns NONE) end; - fun pr_funn definer ((name, ((vs, ty), [])), _) = + val vs_dict = filter_out (null o snd) vs; + val shift = if null eqs' then I else + map (Pretty.block o single o Pretty.block o single); + fun pr_eq definer ((ts, t), (thm, _)) = let - val vs_dict = filter_out (null o snd) vs; - val n = length vs_dict + (length o fst o Code_Thingol.unfold_fun) ty; - val exc_str = - (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name; + val consts = map_filter + (fn c => if (is_some o syntax_const) c + then NONE else (SOME o NameSpace.base o deresolve) c) + ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []); + val vars = reserved_names + |> Code_Name.intro_vars consts + |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames) + (insert (op =)) ts []); in concat ( str definer :: (str o deresolve) name - :: map str (replicate n "_") + :: (if member (op =) pseudo_funs name then [str "()"] + else pr_tyvar_dicts vs_dict + @ map (pr_term (member (op =) pseudo_funs) thm vars BR) ts) @ str "=" - :: str "raise" - :: str "(Fail" - @@ str (exc_str ^ ")") + @@ pr_term (member (op =) pseudo_funs) thm vars NOBR t ) end - | 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 - map (Pretty.block o single o Pretty.block o single); - fun pr_eq definer ((ts, t), (thm, _)) = - let - val consts = map_filter - (fn c => if (is_some o syntax_const) c - then NONE else (SOME o NameSpace.base o deresolve) c) - ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []); - val vars = reserved_names - |> Code_Name.intro_vars consts - |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames) - (insert (op =)) ts []); - in - concat ( - [str definer, (str o deresolve) name] - @ (if null ts andalso null vs_dict - then [str ":", pr_typ NOBR ty] - else - pr_tyvar_dicts vs_dict - @ map (pr_term (K false) thm vars BR) ts) - @ [str "=", pr_term (K false) thm vars NOBR t] - ) - end - in - (Pretty.block o Pretty.fbreaks o shift) ( - pr_eq definer eq - :: map (pr_eq "|") eqs' - ) - end; - val (ps, p) = split_last (pr_funn definer funn :: map (pr_funn "and") funns'); - in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end + in + (Pretty.block o Pretty.fbreaks o shift) ( + pr_eq definer eq + :: map (pr_eq "|") eqs' + ) + end; + fun pr_pseudo_fun name = concat [ + str "val", + (str o deresolve) name, + str "=", + (str o deresolve) name, + str "();" + ]; + val (ps, p) = split_last (pr_funn "fun" funn :: map (pr_funn "and") funns); + val pseudo_ps = map pr_pseudo_fun pseudo_funs; + in Pretty.chunks (ps @ Pretty.block ([p, str ";"]) :: pseudo_ps) end | pr_stmt (MLDatas (datas as (data :: datas'))) = let fun pr_co (co, []) = @@ -250,7 +263,7 @@ ); val (ps, p) = split_last (pr_data "datatype" data :: map (pr_data "and") datas'); - in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end + in Pretty.chunks (ps @| Pretty.block ([p, str ";"])) end | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) = let val w = Code_Name.first_upper v ^ "_"; @@ -457,7 +470,39 @@ val (fished3, _) = Name.variants fished2 Name.context; val vars' = Code_Name.intro_vars fished3 vars; in map (Code_Name.lookup_var vars') fished3 end; - fun pr_stmt (MLFuns (funns as funn :: funns')) = + fun pr_stmt (MLExc (name, n)) = + let + val exc_str = + (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name; + in + concat ( + str "let" + :: (str o deresolve) name + :: map str (replicate n "_") + @ str "=" + :: str "failwith" + @@ str exc_str + ) + end + | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) = + let + val consts = map_filter + (fn c => if (is_some o syntax_const) c + then NONE else (SOME o NameSpace.base o deresolve) c) + (Code_Thingol.fold_constnames (insert (op =)) t []); + val vars = reserved_names + |> Code_Name.intro_vars consts; + in + concat [ + str "let", + (str o deresolve) name, + str ":", + pr_typ NOBR ty, + str "=", + pr_term (K false) thm vars NOBR t + ] + end + | pr_stmt (MLFuns (funn :: funns, pseudo_funs)) = let fun pr_eq ((ts, t), (thm, _)) = let @@ -470,24 +515,12 @@ |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames) (insert (op =)) ts []); in concat [ - (Pretty.block o Pretty.commas) (map (pr_term (K false) thm vars NOBR) ts), + (Pretty.block o Pretty.commas) + (map (pr_term (member (op =) pseudo_funs) thm vars NOBR) ts), str "->", - pr_term (K false) thm vars NOBR t + pr_term (member (op =) pseudo_funs) thm vars NOBR t ] end; - fun pr_eqs name ty [] = - let - val n = (length o fst o Code_Thingol.unfold_fun) ty; - val exc_str = - (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name; - in - concat ( - map str (replicate n "_") - @ str "=" - :: str "failwith" - @@ str exc_str - ) - end - | pr_eqs _ _ [((ts, t), (thm, _))] = + fun pr_eqs is_pseudo [((ts, t), (thm, _))] = let val consts = map_filter (fn c => if (is_some o syntax_const) c @@ -499,12 +532,13 @@ (insert (op =)) ts []); in concat ( - map (pr_term (K false) thm vars BR) ts + (if is_pseudo then [str "()"] + else map (pr_term (member (op =) pseudo_funs) thm vars BR) ts) @ str "=" - @@ pr_term (K false) thm vars NOBR t + @@ pr_term (member (op =) pseudo_funs) thm vars NOBR t ) end - | pr_eqs _ _ (eqs as (eq as (([_], _), _)) :: eqs') = + | pr_eqs _ (eqs as (eq as (([_], _), _)) :: eqs') = Pretty.block ( str "=" :: Pretty.brk 1 @@ -514,7 +548,7 @@ :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1] o single o pr_eq) eqs' ) - | pr_eqs _ _ (eqs as eq :: eqs') = + | pr_eqs _ (eqs as eq :: eqs') = let val consts = map_filter (fn c => if (is_some o syntax_const) c @@ -541,16 +575,25 @@ 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 :: pr_tyvar_dicts (filter_out (null o snd) vs) - @| pr_eqs name ty eqs + @| pr_eqs (member (op =) pseudo_funs name) eqs ); + fun pr_pseudo_fun name = concat [ + str "let", + (str o deresolve) name, + str "=", + (str o deresolve) name, + str "();;" + ]; + val (ps, p) = split_last (pr_funn "fun" funn :: map (pr_funn "and") funns); val (ps, p) = split_last - (pr_funn "let rec" funn :: map (pr_funn "and") funns'); - in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end + (pr_funn "let rec" funn :: map (pr_funn "and") funns); + val pseudo_ps = map pr_pseudo_fun pseudo_funs; + in Pretty.chunks (ps @ Pretty.block ([p, str ";;"]) :: pseudo_ps) end | pr_stmt (MLDatas (datas as (data :: datas'))) = let fun pr_co (co, []) = @@ -577,7 +620,7 @@ ); val (ps, p) = split_last (pr_data "type" data :: map (pr_data "and") datas'); - in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end + in Pretty.chunks (ps @| Pretty.block ([p, str ";;"])) end | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) = let val w = "_" ^ Code_Name.first_upper v; @@ -729,15 +772,33 @@ val base' = if upper then Code_Name.first_upper base else base; val ([base''], nsp') = Name.variants [base'] nsp; in (base'', nsp') end; - fun add_funs stmts = - fold_map + fun rearrange_fun name (tysm as (vs, ty), raw_eqs) = + let + val eqs = filter (snd o snd) raw_eqs; + val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs + of [(([], t), thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty + then ([(([IVar "x"], t `$ IVar "x"), thm)], false) + else (eqs, not (Code_Thingol.fold_constnames + (fn name' => fn b => b orelse name = name') t false)) + | _ => (eqs, false) + else (eqs, false) + in ((name, (tysm, eqs')), is_value) end; + fun check_kind [((name, (tysm, [(([], t), thm)])), true)] = MLVal (name, ((tysm, t), thm)) + | check_kind [((name, ((vs, ty), [])), _)] = + MLExc (name, (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty) + | check_kind funns = + MLFuns (map fst funns, map_filter + (fn ((name, ((vs, _), [(([], _), _)])), _) => + if null (filter_out (null o snd) vs) then SOME name else NONE + | _ => NONE) funns); + fun add_funs stmts = 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))), false) + map_nsp_fun_yield (mk_name_stmt false name) + #>> rpair (rearrange_fun name stmt) | (name, _) => error ("Function block containing illegal statement: " ^ labelled_name name) ) stmts - #>> (split_list #> apsnd MLFuns); + #>> (split_list #> apsnd check_kind); fun add_datatypes stmts = fold_map (fn (name, Code_Thingol.Datatype (_, stmt)) =>