# HG changeset patch # User haftmann # Date 1224677745 -7200 # Node ID bd8438543bf2fcb274b52ca34d171841a28e03f2 # Parent 64ab5bb68d4c7ea5908ae94a3868d3828a971b6b code identifier namings are no longer imperative diff -r 64ab5bb68d4c -r bd8438543bf2 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Wed Oct 22 14:15:44 2008 +0200 +++ b/src/HOL/HOL.thy Wed Oct 22 14:15:45 2008 +0200 @@ -1692,8 +1692,7 @@ use "~~/src/HOL/Tools/recfun_codegen.ML" setup {* - Code_Name.setup - #> Code_ML.setup + Code_ML.setup #> Code_Haskell.setup #> Nbe.setup #> Codegen.setup diff -r 64ab5bb68d4c -r bd8438543bf2 src/HOL/Library/Heap_Monad.thy --- a/src/HOL/Library/Heap_Monad.thy Wed Oct 22 14:15:44 2008 +0200 +++ b/src/HOL/Library/Heap_Monad.thy Wed Oct 22 14:15:45 2008 +0200 @@ -296,66 +296,66 @@ code_const "Heap_Monad.Fail" (OCaml "Failure") code_const "Heap_Monad.raise_exc" (OCaml "!(fun/ ()/ ->/ raise/ _)") -ML {* -local +setup {* let + open Code_Thingol; -open Code_Thingol; - -val bind' = Code_Name.const @{theory} @{const_name bindM}; -val return' = Code_Name.const @{theory} @{const_name return}; -val unit' = Code_Name.const @{theory} @{const_name Unity}; + fun lookup naming = the o Code_Thingol.lookup_const naming; -fun imp_monad_bind'' ts = - let - val dummy_name = ""; - val dummy_type = ITyVar dummy_name; - val dummy_case_term = IVar dummy_name; - (*assumption: dummy values are not relevant for serialization*) - val unitt = IConst (unit', ([], [])); - fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t) - | dest_abs (t, ty) = - let - val vs = Code_Thingol.fold_varnames cons t []; - val v = Name.variant vs "x"; - val ty' = (hd o fst o Code_Thingol.unfold_fun) ty; - in ((v, ty'), t `$ IVar v) end; - fun force (t as IConst (c, _) `$ t') = if c = return' - then t' else t `$ unitt - | force t = t `$ unitt; - fun tr_bind' [(t1, _), (t2, ty2)] = - let - val ((v, ty), t) = dest_abs (t2, ty2); - in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end - and tr_bind'' t = case Code_Thingol.unfold_app t - of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind' - then tr_bind' [(x1, ty1), (x2, ty2)] - else force t - | _ => force t; - in (dummy_name, dummy_type) `|-> ICase (((IVar dummy_name, dummy_type), - [(unitt, tr_bind' ts)]), dummy_case_term) end -and imp_monad_bind' (const as (c, (_, tys))) ts = if c = bind' then case (ts, tys) - of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] - | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3 - | (ts, _) => imp_monad_bind (eta_expand 2 (const, ts)) - else IConst const `$$ map imp_monad_bind ts -and imp_monad_bind (IConst const) = imp_monad_bind' const [] - | imp_monad_bind (t as IVar _) = t - | imp_monad_bind (t as _ `$ _) = (case unfold_app t - of (IConst const, ts) => imp_monad_bind' const ts - | (t, ts) => imp_monad_bind t `$$ map imp_monad_bind ts) - | imp_monad_bind (v_ty `|-> t) = v_ty `|-> imp_monad_bind t - | imp_monad_bind (ICase (((t, ty), pats), t0)) = ICase - (((imp_monad_bind t, ty), (map o pairself) imp_monad_bind pats), imp_monad_bind t0); + fun imp_monad_bind'' bind' return' unit' ts = + let + val dummy_name = ""; + val dummy_type = ITyVar dummy_name; + val dummy_case_term = IVar dummy_name; + (*assumption: dummy values are not relevant for serialization*) + val unitt = IConst (unit', ([], [])); + fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t) + | dest_abs (t, ty) = + let + val vs = Code_Thingol.fold_varnames cons t []; + val v = Name.variant vs "x"; + val ty' = (hd o fst o Code_Thingol.unfold_fun) ty; + in ((v, ty'), t `$ IVar v) end; + fun force (t as IConst (c, _) `$ t') = if c = return' + then t' else t `$ unitt + | force t = t `$ unitt; + fun tr_bind' [(t1, _), (t2, ty2)] = + let + val ((v, ty), t) = dest_abs (t2, ty2); + in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end + and tr_bind'' t = case Code_Thingol.unfold_app t + of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind' + then tr_bind' [(x1, ty1), (x2, ty2)] + else force t + | _ => force t; + in (dummy_name, dummy_type) `|-> ICase (((IVar dummy_name, dummy_type), + [(unitt, tr_bind' ts)]), dummy_case_term) end + and imp_monad_bind' bind' return' unit' (const as (c, (_, tys))) ts = if c = bind' then case (ts, tys) + of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)] + | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)] `$ t3 + | (ts, _) => imp_monad_bind bind' return' unit' (eta_expand 2 (const, ts)) + else IConst const `$$ map (imp_monad_bind bind' return' unit') ts + and imp_monad_bind bind' return' unit' (IConst const) = imp_monad_bind' bind' return' unit' const [] + | imp_monad_bind bind' return' unit' (t as IVar _) = t + | imp_monad_bind bind' return' unit' (t as _ `$ _) = (case unfold_app t + of (IConst const, ts) => imp_monad_bind' bind' return' unit' const ts + | (t, ts) => imp_monad_bind bind' return' unit' t `$$ map (imp_monad_bind bind' return' unit') ts) + | imp_monad_bind bind' return' unit' (v_ty `|-> t) = v_ty `|-> imp_monad_bind bind' return' unit' t + | imp_monad_bind bind' return' unit' (ICase (((t, ty), pats), t0)) = ICase + (((imp_monad_bind bind' return' unit' t, ty), (map o pairself) (imp_monad_bind bind' return' unit') pats), imp_monad_bind bind' return' unit' t0); + + fun imp_program naming = (Graph.map_nodes o map_terms_stmt) + (imp_monad_bind (lookup naming @{const_name bindM}) + (lookup naming @{const_name return}) + (lookup naming @{const_name Unity})); in -val imp_program = (Graph.map_nodes o map_terms_stmt) imp_monad_bind; + Code_Target.extend_target ("SML_imp", ("SML", imp_program)) + #> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program)) end *} -setup {* Code_Target.extend_target ("SML_imp", ("SML", imp_program)) *} -setup {* Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program)) *} code_reserved OCaml Failure raise diff -r 64ab5bb68d4c -r bd8438543bf2 src/HOL/List.thy --- a/src/HOL/List.thy Wed Oct 22 14:15:44 2008 +0200 +++ b/src/HOL/List.thy Wed Oct 22 14:15:45 2008 +0200 @@ -3520,20 +3520,8 @@ local open Basic_Code_Thingol; -val nil' = Code_Name.const @{theory} @{const_name Nil}; -val cons' = Code_Name.const @{theory} @{const_name Cons}; -val char' = Code_Name.const @{theory} @{const_name Char} -val nibbles' = map (Code_Name.const @{theory}) - [@{const_name Nibble0}, @{const_name Nibble1}, - @{const_name Nibble2}, @{const_name Nibble3}, - @{const_name Nibble4}, @{const_name Nibble5}, - @{const_name Nibble6}, @{const_name Nibble7}, - @{const_name Nibble8}, @{const_name Nibble9}, - @{const_name NibbleA}, @{const_name NibbleB}, - @{const_name NibbleC}, @{const_name NibbleD}, - @{const_name NibbleE}, @{const_name NibbleF}]; - -fun implode_list t = + +fun implode_list (nil', cons') t = let fun dest_cons (IConst (c, _) `$ t1 `$ t2) = if c = cons' @@ -3546,19 +3534,19 @@ | _ => NONE end; -fun decode_char (IConst (c1, _), IConst (c2, _)) = +fun decode_char nibbles' (IConst (c1, _), IConst (c2, _)) = let fun idx c = find_index (curry (op =) c) nibbles'; fun decode ~1 _ = NONE | decode _ ~1 = NONE | decode n m = SOME (chr (n * 16 + m)); in decode (idx c1) (idx c2) end - | decode_char _ = NONE; - -fun implode_string mk_char mk_string ts = + | decode_char _ _ = NONE; + +fun implode_string (char', nibbles') mk_char mk_string ts = let fun implode_char (IConst (c, _) `$ t1 `$ t2) = - if c = char' then decode_char (t1, t2) else NONE + if c = char' then decode_char nibbles' (t1, t2) else NONE | implode_char _ = NONE; val ts' = map implode_char ts; in if forall is_some ts' @@ -3566,6 +3554,20 @@ else NONE end; +fun list_names naming = pairself (the o Code_Thingol.lookup_const naming) + (@{const_name Nil}, @{const_name Cons}); +fun char_name naming = (the o Code_Thingol.lookup_const naming) + @{const_name Char} +fun nibble_names naming = map (the o Code_Thingol.lookup_const naming) + [@{const_name Nibble0}, @{const_name Nibble1}, + @{const_name Nibble2}, @{const_name Nibble3}, + @{const_name Nibble4}, @{const_name Nibble5}, + @{const_name Nibble6}, @{const_name Nibble7}, + @{const_name Nibble8}, @{const_name Nibble9}, + @{const_name NibbleA}, @{const_name NibbleB}, + @{const_name NibbleC}, @{const_name NibbleD}, + @{const_name NibbleE}, @{const_name NibbleF}]; + fun default_list (target_fxy, target_cons) pr fxy t1 t2 = Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy [ pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1, @@ -3576,8 +3578,8 @@ fun pretty_list literals = let val mk_list = Code_Printer.literal_list literals; - fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] = - case Option.map (cons t1) (implode_list t2) + fun pretty pr naming thm pat vars fxy [(t1, _), (t2, _)] = + case Option.map (cons t1) (implode_list (list_names naming) t2) of SOME ts => mk_list (map (pr vars Code_Printer.NOBR) ts) | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2; in (2, pretty) end; @@ -3587,9 +3589,9 @@ val mk_list = Code_Printer.literal_list literals; val mk_char = Code_Printer.literal_char literals; val mk_string = Code_Printer.literal_string literals; - fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] = - case Option.map (cons t1) (implode_list t2) - of SOME ts => (case implode_string mk_char mk_string ts + fun pretty pr naming thm pat vars fxy [(t1, _), (t2, _)] = + case Option.map (cons t1) (implode_list (list_names naming) t2) + of SOME ts => (case implode_string (char_name naming, nibble_names naming) mk_char mk_string ts of SOME p => p | NONE => mk_list (map (pr vars Code_Printer.NOBR) ts)) | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2; @@ -3598,8 +3600,8 @@ fun pretty_char literals = let val mk_char = Code_Printer.literal_char literals; - fun pretty _ thm _ _ _ [(t1, _), (t2, _)] = - case decode_char (t1, t2) + fun pretty _ naming thm _ _ _ [(t1, _), (t2, _)] = + case decode_char (nibble_names naming) (t1, t2) of SOME c => (Code_Printer.str o mk_char) c | NONE => Code_Printer.nerror thm "Illegal character expression"; in (2, pretty) end; @@ -3608,9 +3610,9 @@ let val mk_char = Code_Printer.literal_char literals; val mk_string = Code_Printer.literal_string literals; - fun pretty _ thm _ _ _ [(t, _)] = - case implode_list t - of SOME ts => (case implode_string mk_char mk_string ts + fun pretty _ naming thm _ _ _ [(t, _)] = + case implode_list (list_names naming) t + of SOME ts => (case implode_string (char_name naming, nibble_names naming) mk_char mk_string ts of SOME p => p | NONE => Code_Printer.nerror thm "Illegal message expression") | NONE => Code_Printer.nerror thm "Illegal message expression"; diff -r 64ab5bb68d4c -r bd8438543bf2 src/HOL/Tools/numeral.ML --- a/src/HOL/Tools/numeral.ML Wed Oct 22 14:15:44 2008 +0200 +++ b/src/HOL/Tools/numeral.ML Wed Oct 22 14:15:45 2008 +0200 @@ -59,25 +59,28 @@ fun add_code number_of negative unbounded target thy = let - val pls' = Code_Name.const thy @{const_name Int.Pls}; - val min' = Code_Name.const thy @{const_name Int.Min}; - val bit0' = Code_Name.const thy @{const_name Int.Bit0}; - val bit1' = Code_Name.const thy @{const_name Int.Bit1}; val pr_numeral = (Code_Printer.literal_numeral o Code_Target.the_literals thy) target; - fun dest_bit thm (IConst (c, _)) = if c = bit0' then 0 - else if c = bit1' then 1 - else Code_Printer.nerror thm "Illegal numeral expression: illegal bit" - | dest_bit thm _ = Code_Printer.nerror thm "Illegal numeral expression: illegal bit"; - fun dest_numeral thm (IConst (c, _)) = if c = pls' then SOME 0 - else if c = min' then - if negative then SOME ~1 else NONE - else Code_Printer.nerror thm "Illegal numeral expression: illegal leading digit" - | dest_numeral thm (t1 `$ t2) = - let val (n, b) = (dest_numeral thm t2, dest_bit thm t1) - in case n of SOME n => SOME (2 * n + b) | NONE => NONE end - | dest_numeral thm _ = Code_Printer.nerror thm "Illegal numeral expression: illegal term"; - fun pretty _ thm _ _ _ [(t, _)] = - (Code_Printer.str o pr_numeral unbounded o the_default 0 o dest_numeral thm) t; + fun dest_numeral naming thm = + let + val SOME pls' = Code_Thingol.lookup_const naming @{const_name Int.Pls}; + val SOME min' = Code_Thingol.lookup_const naming @{const_name Int.Min}; + val SOME bit0' = Code_Thingol.lookup_const naming @{const_name Int.Bit0}; + val SOME bit1' = Code_Thingol.lookup_const naming @{const_name Int.Bit1}; + fun dest_bit (IConst (c, _)) = if c = bit0' then 0 + else if c = bit1' then 1 + else Code_Printer.nerror thm "Illegal numeral expression: illegal bit" + | dest_bit _ = Code_Printer.nerror thm "Illegal numeral expression: illegal bit"; + fun dest_num (IConst (c, _)) = if c = pls' then SOME 0 + else if c = min' then + if negative then SOME ~1 else NONE + else Code_Printer.nerror thm "Illegal numeral expression: illegal leading digit" + | dest_num (t1 `$ t2) = + let val (n, b) = (dest_num t2, dest_bit t1) + in case n of SOME n => SOME (2 * n + b) | NONE => NONE end + | dest_num _ = Code_Printer.nerror thm "Illegal numeral expression: illegal term"; + in dest_num end; + fun pretty _ naming thm _ _ _ [(t, _)] = + (Code_Printer.str o pr_numeral unbounded o the_default 0 o dest_numeral naming thm) t; in thy |> Code_Target.add_syntax_const target number_of (SOME (1, pretty)) diff -r 64ab5bb68d4c -r bd8438543bf2 src/HOL/ex/Codegenerator_Pretty.thy --- a/src/HOL/ex/Codegenerator_Pretty.thy Wed Oct 22 14:15:44 2008 +0200 +++ b/src/HOL/ex/Codegenerator_Pretty.thy Wed Oct 22 14:15:45 2008 +0200 @@ -17,7 +17,6 @@ nonfix upto; *} -export_code "RType.*" -- "workaround for cache problem" export_code * in SML module_name CodegenTest in OCaml module_name CodegenTest file - in Haskell file - diff -r 64ab5bb68d4c -r bd8438543bf2 src/Tools/code/code_haskell.ML --- a/src/Tools/code/code_haskell.ML Wed Oct 22 14:15:44 2008 +0200 +++ b/src/Tools/code/code_haskell.ML Wed Oct 22 14:15:45 2008 +0200 @@ -32,7 +32,7 @@ | pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p]; in gen_pr_bind pr_bind pr_term end; -fun pr_haskell_stmt syntax_class syntax_tyco syntax_const labelled_name +fun pr_haskell_stmt naming labelled_name syntax_class syntax_tyco syntax_const init_syms deresolve is_cons contr_classparam_typs deriving_show = let val deresolve_base = NameSpace.base o deresolve; @@ -42,24 +42,24 @@ fun classparam_name class classparam = case syntax_class class of NONE => deresolve_base classparam | SOME (_, classparam_syntax) => case classparam_syntax classparam - of NONE => (snd o dest_name) classparam + of NONE => (snd o Code_Name.dest_name) classparam | SOME classparam => classparam; fun pr_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs of [] => [] | classbinds => Pretty.enum "," "(" ")" ( map (fn (v, class) => - str (class_name class ^ " " ^ lookup_var tyvars v)) classbinds) + str (class_name class ^ " " ^ Code_Name.lookup_var tyvars v)) classbinds) @@ str " => "; fun pr_typforall tyvars vs = case map fst vs of [] => [] | vnames => str "forall " :: Pretty.breaks - (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1; + (map (str o Code_Name.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1; fun pr_tycoexpr tyvars fxy (tyco, tys) = brackify fxy (str tyco :: map (pr_typ tyvars BR) tys) and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco of NONE => pr_tycoexpr tyvars fxy (deresolve tyco, tys) | SOME (i, pr) => pr (pr_typ tyvars) fxy tys) - | pr_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v; + | pr_typ tyvars fxy (ITyVar v) = (str o Code_Name.lookup_var tyvars) v; fun pr_typdecl tyvars (vs, tycoexpr) = Pretty.block (pr_typcontext tyvars vs @| pr_tycoexpr tyvars NOBR tycoexpr); fun pr_typscheme tyvars (vs, ty) = @@ -75,7 +75,7 @@ pr_term tyvars thm pat vars BR t2 ]) | pr_term tyvars thm pat vars fxy (IVar v) = - (str o lookup_var vars) v + (str o Code_Name.lookup_var vars) v | pr_term tyvars thm pat vars fxy (t as _ `|-> _) = let val (binds, t') = Code_Thingol.unfold_abs t; @@ -102,7 +102,7 @@ (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys) else (str o deresolve) c :: map (pr_term tyvars thm pat vars BR) ts end - and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const is_cons + and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const is_cons naming and pr_bind tyvars = pr_haskell_bind (pr_term tyvars) and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) = let @@ -131,9 +131,9 @@ ) (map pr bs) end | pr_case tyvars thm vars fxy ((_, []), _) = str "error \"empty case\""; - fun pr_stmt (name, Code_Thingol.Fun ((vs, ty), [])) = + fun pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), []))) = let - val tyvars = intro_vars (map fst vs) init_syms; + val tyvars = Code_Name.intro_vars (map fst vs) init_syms; val n = (length o fst o Code_Thingol.unfold_fun) ty; in Pretty.chunks [ @@ -153,10 +153,10 @@ ) ] end - | pr_stmt (name, Code_Thingol.Fun ((vs, ty), raw_eqs)) = + | pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) = let val eqs = filter (snd o snd) raw_eqs; - val tyvars = intro_vars (map fst vs) init_syms; + val tyvars = Code_Name.intro_vars (map fst vs) init_syms; fun pr_eq ((ts, t), (thm, _)) = let val consts = map_filter @@ -164,8 +164,8 @@ then NONE else (SOME o NameSpace.base o deresolve) c) ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []); val vars = init_syms - |> intro_vars consts - |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames) + |> Code_Name.intro_vars consts + |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames) (insert (op =)) ts []); in semicolon ( @@ -186,18 +186,18 @@ :: map pr_eq eqs ) end - | pr_stmt (name, Code_Thingol.Datatype (vs, [])) = + | pr_stmt (name, Code_Thingol.Datatype (_, (vs, []))) = let - val tyvars = intro_vars (map fst vs) init_syms; + val tyvars = Code_Name.intro_vars (map fst vs) init_syms; in semicolon [ str "data", pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs)) ] end - | pr_stmt (name, Code_Thingol.Datatype (vs, [(co, [ty])])) = + | pr_stmt (name, Code_Thingol.Datatype (_, (vs, [(co, [ty])]))) = let - val tyvars = intro_vars (map fst vs) init_syms; + val tyvars = Code_Name.intro_vars (map fst vs) init_syms; in semicolon ( str "newtype" @@ -208,9 +208,9 @@ :: (if deriving_show name then [str "deriving (Read, Show)"] else []) ) end - | pr_stmt (name, Code_Thingol.Datatype (vs, co :: cos)) = + | pr_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) = let - val tyvars = intro_vars (map fst vs) init_syms; + val tyvars = Code_Name.intro_vars (map fst vs) init_syms; fun pr_co (co, tys) = concat ( (str o deresolve_base) co @@ -226,9 +226,9 @@ @ (if deriving_show name then [str "deriving (Read, Show)"] else []) ) end - | pr_stmt (name, Code_Thingol.Class (v, (superclasses, classparams))) = + | pr_stmt (name, Code_Thingol.Class (_, (v, (superclasses, classparams)))) = let - val tyvars = intro_vars [v] init_syms; + val tyvars = Code_Name.intro_vars [v] init_syms; fun pr_classparam (classparam, ty) = semicolon [ (str o classparam_name name) classparam, @@ -240,7 +240,7 @@ Pretty.block [ str "class ", Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]), - str (deresolve_base name ^ " " ^ lookup_var tyvars v), + str (deresolve_base name ^ " " ^ Code_Name.lookup_var tyvars v), str " where {" ], str "};" @@ -248,7 +248,7 @@ end | pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) = let - val tyvars = intro_vars (map fst vs) init_syms; + val tyvars = Code_Name.intro_vars (map fst vs) init_syms; fun pr_instdef ((classparam, c_inst), (thm, _)) = semicolon [ (str o classparam_name class) classparam, @@ -273,20 +273,20 @@ let val module_alias = if is_some module_name then K module_name else raw_module_alias; val reserved_names = Name.make_context reserved_names; - val mk_name_module = mk_name_module reserved_names module_prefix module_alias program; + val mk_name_module = Code_Name.mk_name_module reserved_names module_prefix module_alias program; fun add_stmt (name, (stmt, deps)) = let - val (module_name, base) = dest_name name; + val (module_name, base) = Code_Name.dest_name name; val module_name' = mk_name_module module_name; val mk_name_stmt = yield_singleton Name.variants; fun add_fun upper (nsp_fun, nsp_typ) = let val (base', nsp_fun') = - mk_name_stmt (if upper then first_upper base else base) nsp_fun + mk_name_stmt (if upper then Code_Name.first_upper base else base) nsp_fun in (base', (nsp_fun', nsp_typ)) end; fun add_typ (nsp_fun, nsp_typ) = let - val (base', nsp_typ') = mk_name_stmt (first_upper base) nsp_typ + val (base', nsp_typ') = mk_name_stmt (Code_Name.first_upper base) nsp_typ in (base', (nsp_fun, nsp_typ')) end; val add_name = case stmt of Code_Thingol.Fun _ => add_fun false @@ -314,15 +314,14 @@ val hs_program = fold add_stmt (AList.make (fn name => (Graph.get_node program name, Graph.imm_succs program name)) (Graph.strong_conn program |> flat)) Symtab.empty; - fun deresolver name = - (fst o the o AList.lookup (op =) ((fst o snd o the - o Symtab.lookup hs_program) ((mk_name_module o fst o dest_name) name))) name - handle Option => error ("Unknown statement name: " ^ labelled_name name); + fun deresolver name = (fst o the o AList.lookup (op =) ((fst o snd o the + o Symtab.lookup hs_program) ((mk_name_module o fst o Code_Name.dest_name) name))) name + handle Option => error ("Unknown statement name: " ^ labelled_name name); in (deresolver, hs_program) end; fun serialize_haskell module_prefix raw_module_name string_classes labelled_name reserved_names includes raw_module_alias - syntax_class syntax_tyco syntax_const program cs destination = + syntax_class syntax_tyco syntax_const naming program cs destination = let val stmt_names = Code_Target.stmt_names_of_destination destination; val module_name = if null stmt_names then raw_module_name else SOME "Code"; @@ -335,16 +334,16 @@ fun deriv _ "fun" = false | deriv tycos tyco = member (op =) tycos tyco orelse case try (Graph.get_node program) tyco - of SOME (Code_Thingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos)) + of SOME (Code_Thingol.Datatype (_, (_, cs))) => forall (deriv' (tyco :: tycos)) (maps snd cs) | NONE => true and deriv' tycos (tyco `%% tys) = deriv tycos tyco andalso forall (deriv' tycos) tys | deriv' _ (ITyVar _) = true in deriv [] tyco end; - val reserved_names = make_vars reserved_names; - fun pr_stmt qualified = pr_haskell_stmt syntax_class syntax_tyco - syntax_const labelled_name reserved_names + val reserved_names = Code_Name.make_vars reserved_names; + fun pr_stmt qualified = pr_haskell_stmt naming labelled_name + syntax_class syntax_tyco syntax_const reserved_names (if qualified then deresolver else NameSpace.base o deresolver) is_cons contr_classparam_typs (if string_classes then deriving_show else K false); @@ -432,14 +431,14 @@ of SOME (((v, pat), ty), t') => SOME ((SOME (((SOME v, pat), ty), true), t1), t') | NONE => NONE; - fun dest_monad (IConst (c, _) `$ t1 `$ t2) = - if c = c_bind then dest_bind t1 t2 + 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 + | dest_monad _ t = case Code_Thingol.split_let t of SOME (((pat, ty), tbind), t') => SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t') | NONE => NONE; - val implode_monad = Code_Thingol.unfoldr dest_monad; + fun implode_monad c_bind_name = Code_Thingol.unfoldr (dest_monad c_bind_name); fun pr_monad pr_bind pr (NONE, t) vars = (semicolon [pr vars NOBR t], vars) | pr_monad pr_bind pr (SOME (bind, true), t) vars = vars @@ -448,9 +447,9 @@ | pr_monad pr_bind pr (SOME (bind, false), t) vars = vars |> pr_bind NOBR bind |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]); - fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2 + fun pretty pr naming thm pat vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2 of SOME (bind, t') => let - val (binds, t'') = implode_monad t' + val (binds, t'') = implode_monad ((the o Code_Thingol.lookup_const naming) c_bind) t' val (ps, vars') = fold_map (pr_monad (pr_haskell_bind (K (K pr)) thm) pr) (bind :: binds) vars; in (brackify fxy o single o Pretty.enclose "do {" "}" o Pretty.breaks) (ps @| pr vars' NOBR t'') end | NONE => brackify_infix (1, L) fxy @@ -460,11 +459,10 @@ fun add_monad target' raw_c_bind thy = let val c_bind = Code_Unit.read_const thy raw_c_bind; - val c_bind' = Code_Name.const thy c_bind; in if target = target' then thy |> Code_Target.add_syntax_const target c_bind - (SOME (pretty_haskell_monad c_bind')) + (SOME (pretty_haskell_monad c_bind)) else error "Only Haskell target allows for monad syntax" end; diff -r 64ab5bb68d4c -r bd8438543bf2 src/Tools/code/code_ml.ML --- a/src/Tools/code/code_ml.ML Wed Oct 22 14:15:44 2008 +0200 +++ b/src/Tools/code/code_ml.ML Wed Oct 22 14:15:45 2008 +0200 @@ -42,15 +42,15 @@ (** SML serailizer **) -fun pr_sml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons = +fun pr_sml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons = let val pr_label_classrel = translate_string (fn "." => "__" | c => c) o NameSpace.qualifier; val pr_label_classparam = NameSpace.base o NameSpace.qualifier; fun pr_dicts fxy ds = let - fun pr_dictvar (v, (_, 1)) = first_upper v ^ "_" - | pr_dictvar (v, (i, _)) = first_upper v ^ string_of_int (i+1) ^ "_"; + fun pr_dictvar (v, (_, 1)) = Code_Name.first_upper v ^ "_" + | pr_dictvar (v, (i, _)) = Code_Name.first_upper v ^ string_of_int (i+1) ^ "_"; fun pr_proj [] p = p | pr_proj [p'] p = @@ -86,7 +86,7 @@ fun pr_term thm pat vars fxy (IConst c) = pr_app thm pat vars fxy (c, []) | pr_term thm pat vars fxy (IVar v) = - str (lookup_var vars v) + str (Code_Name.lookup_var vars v) | pr_term thm pat vars fxy (t as t1 `$ t2) = (case Code_Thingol.unfold_const_app t of SOME c_ts => pr_app thm pat vars fxy c_ts @@ -116,7 +116,7 @@ else [pr_term thm pat vars BR (Code_Thingol.eta_expand k app)] end else (str o deresolve) c :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts - and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars + and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons naming thm pat vars and pr_bind' ((NONE, NONE), _) = str "_" | pr_bind' ((SOME v, NONE), _) = str v | pr_bind' ((NONE, SOME p), _) = p @@ -199,8 +199,8 @@ then NONE else (SOME o NameSpace.base o deresolve) c) ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []); val vars = reserved_names - |> intro_vars consts - |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames) + |> Code_Name.intro_vars consts + |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames) (insert (op =)) ts []); in concat ( @@ -250,7 +250,7 @@ in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) = let - val w = first_upper v ^ "_"; + val w = Code_Name.first_upper v ^ "_"; fun pr_superclass_field (class, classrel) = (concat o map str) [ pr_label_classrel classrel, ":", "'" ^ v, deresolve class @@ -342,12 +342,12 @@ (** OCaml serializer **) -fun pr_ocaml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons = +fun pr_ocaml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons = let fun pr_dicts fxy ds = let - fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v - | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1); + fun pr_dictvar (v, (_, 1)) = "_" ^ Code_Name.first_upper v + | pr_dictvar (v, (i, _)) = "_" ^ Code_Name.first_upper v ^ string_of_int (i+1); fun pr_proj ps p = fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p fun pr_dict fxy (DictConst (inst, dss)) = @@ -379,7 +379,7 @@ fun pr_term thm pat vars fxy (IConst c) = pr_app thm pat vars fxy (c, []) | pr_term thm pat vars fxy (IVar v) = - str (lookup_var vars v) + str (Code_Name.lookup_var vars v) | pr_term thm pat vars fxy (t as t1 `$ t2) = (case Code_Thingol.unfold_const_app t of SOME c_ts => pr_app thm pat vars fxy c_ts @@ -407,7 +407,7 @@ else [pr_term thm pat vars BR (Code_Thingol.eta_expand (length tys) app)] else (str o deresolve) c :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts) - and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars + and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons naming thm pat vars and pr_bind' ((NONE, NONE), _) = str "_" | pr_bind' ((SOME v, NONE), _) = str v | pr_bind' ((NONE, SOME p), _) = p @@ -449,8 +449,8 @@ val x = Name.variant (map_filter I fished1) "x"; val fished2 = map_index (fillup_param x) fished1; val (fished3, _) = Name.variants fished2 Name.context; - val vars' = intro_vars fished3 vars; - in map (lookup_var vars') fished3 end; + 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')) = let fun pr_eq ((ts, t), (thm, _)) = @@ -460,8 +460,8 @@ then NONE else (SOME o NameSpace.base o deresolve) c) ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []); val vars = reserved_names - |> intro_vars consts - |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames) + |> Code_Name.intro_vars consts + |> 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 true vars NOBR) ts), @@ -488,8 +488,8 @@ then NONE else (SOME o NameSpace.base o deresolve) c) ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []); val vars = reserved_names - |> intro_vars consts - |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames) + |> Code_Name.intro_vars consts + |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames) (insert (op =)) ts []); in concat ( @@ -516,7 +516,7 @@ ((fold o Code_Thingol.fold_constnames) (insert (op =)) (map (snd o fst) eqs) []); val vars = reserved_names - |> intro_vars consts; + |> Code_Name.intro_vars consts; val dummy_parms = (map str o fish_params vars o map (fst o fst)) eqs; in Pretty.block ( @@ -574,7 +574,7 @@ in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) = let - val w = "_" ^ first_upper v; + val w = "_" ^ Code_Name.first_upper v; fun pr_superclass_field (class, classrel) = (concat o map str) [ deresolve classrel, ":", "'" ^ v, deresolve class @@ -716,16 +716,16 @@ let val (x, nsp_typ') = f nsp_typ in (x, (nsp_fun, nsp_typ')) end; - val mk_name_module = mk_name_module reserved_names NONE module_alias program; + val mk_name_module = Code_Name.mk_name_module reserved_names NONE module_alias program; fun mk_name_stmt upper name nsp = let - val (_, base) = dest_name name; - val base' = if upper then first_upper base else base; + val (_, base) = Code_Name.dest_name name; + 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 - (fn (name, Code_Thingol.Fun stmt) => + (fn (name, Code_Thingol.Fun (_, stmt)) => map_nsp_fun_yield (mk_name_stmt false name) #>> rpair (name, stmt |> apsnd (filter (snd o snd))) | (name, _) => @@ -734,7 +734,7 @@ #>> (split_list #> apsnd MLFuns); fun add_datatypes stmts = fold_map - (fn (name, Code_Thingol.Datatype stmt) => + (fn (name, Code_Thingol.Datatype (_, stmt)) => map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt)) | (name, Code_Thingol.Datatypecons _) => map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE @@ -747,8 +747,8 @@ | stmts => MLDatas stmts))); fun add_class stmts = fold_map - (fn (name, Code_Thingol.Class info) => - map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, info)) + (fn (name, Code_Thingol.Class (_, stmt)) => + map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt)) | (name, Code_Thingol.Classrel _) => map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE | (name, Code_Thingol.Classparam _) => @@ -786,7 +786,7 @@ [] |> fold (fold (insert (op =)) o Graph.imm_succs program) names |> subtract (op =) names; - val (module_names, _) = (split_list o map dest_name) names; + val (module_names, _) = (split_list o map Code_Name.dest_name) names; val module_name = (the_single o distinct (op =) o map mk_name_module) module_names handle Empty => error ("Different namespace prefixes for mutual dependencies:\n" @@ -796,7 +796,7 @@ val module_name_path = NameSpace.explode module_name; fun add_dep name name' = let - val module_name' = (mk_name_module o fst o dest_name) name'; + val module_name' = (mk_name_module o fst o Code_Name.dest_name) name'; in if module_name = module_name' then map_node module_name_path (Graph.add_edge (name, name')) else let @@ -824,7 +824,7 @@ (rev (Graph.strong_conn program))); fun deresolver prefix name = let - val module_name = (fst o dest_name) name; + val module_name = (fst o Code_Name.dest_name) name; val module_name' = (NameSpace.explode o mk_name_module) module_name; val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name'); val stmt_name = @@ -840,19 +840,19 @@ in (deresolver, nodes) end; fun serialize_ml target compile pr_module pr_stmt raw_module_name labelled_name reserved_names includes raw_module_alias - _ syntax_tyco syntax_const program cs destination = + _ syntax_tyco syntax_const naming program cs destination = let val is_cons = Code_Thingol.is_cons program; val stmt_names = Code_Target.stmt_names_of_destination destination; val module_name = if null stmt_names then raw_module_name else SOME "Code"; val (deresolver, nodes) = ml_node_of_program labelled_name module_name reserved_names raw_module_alias program; - val reserved_names = make_vars reserved_names; + val reserved_names = Code_Name.make_vars reserved_names; fun pr_node prefix (Dummy _) = NONE | pr_node prefix (Stmt (_, stmt)) = if null stmt_names orelse (not o null o filter (member (op =) stmt_names) o stmt_names_of) stmt then SOME - (pr_stmt syntax_tyco syntax_const labelled_name reserved_names + (pr_stmt naming labelled_name syntax_tyco syntax_const reserved_names (deresolver prefix) is_cons stmt) else NONE | pr_node prefix (Module (module_name, (_, nodes))) = @@ -861,8 +861,8 @@ o rev o flat o Graph.strong_conn) nodes) |> (if null stmt_names then pr_module module_name else Pretty.chunks) |> SOME; - val cs' = map_filter (try (deresolver (if is_some module_name then the_list module_name else []))) - cs; + val cs' = (map o try) + (deresolver (if is_some module_name then the_list module_name else [])) cs; val p = Pretty.chunks (separate (str "") (map snd includes @ (map_filter (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes)); in @@ -877,8 +877,8 @@ (** ML (system language) code for evaluation and instrumentalization **) -fun ml_code_of thy = Code_Target.serialize_custom thy - (target_SML, (fn _ => fn [] => serialize_ml target_SML (SOME (K ())) (K Pretty.chunks) pr_sml_stmt (SOME ""), +fun ml_code_of thy = Code_Target.serialize_custom thy (target_SML, + (fn _ => fn [] => serialize_ml target_SML (SOME (K ())) (K Pretty.chunks) pr_sml_stmt (SOME ""), literals_sml)); @@ -890,15 +890,16 @@ val _ = if null (term_frees (term_of ct)) then () else error ("Term " ^ quote (Syntax.string_of_term_global thy (term_of ct)) ^ " to be evaluated contains free variables"); - fun eval' program ((vs, ty), t) deps = + fun eval' naming program ((vs, ty), t) deps = let val _ = if Code_Thingol.contains_dictvar t then error "Term to be evaluated constains free dictionaries" else (); + val value_name = "Value.VALUE.value" val program' = program - |> Graph.new_node (Code_Name.value_name, - Code_Thingol.Fun (([], ty), [(([], t), (Drule.dummy_thm, true))])) - |> fold (curry Graph.add_edge Code_Name.value_name) deps; - val (value_code, [value_name']) = ml_code_of thy program' [Code_Name.value_name]; + |> Graph.new_node (value_name, + Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (Drule.dummy_thm, true))]))) + |> fold (curry Graph.add_edge value_name) deps; + val (value_code, [SOME value_name']) = ml_code_of thy naming program' [value_name]; val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name' ^ space_implode " " (map (enclose "(" ")") args) ^ " end"; in ML_Context.evaluate ctxt Output.ml_output false reff sml_code end; @@ -922,12 +923,13 @@ fun delayed_code thy consts () = let - val (consts', program) = Code_Thingol.consts_program thy consts; - val (ml_code, consts'') = ml_code_of thy program consts'; - val _ = if length consts <> length consts'' then - error ("One of the constants " ^ commas (map (quote o Code_Unit.string_of_const thy) consts) - ^ "\nhas a user-defined serialization") else (); - in (ml_code, consts ~~ consts'') end; + val (consts', (naming, program)) = Code_Thingol.consts_program thy consts; + val (ml_code, consts'') = ml_code_of thy naming program consts'; + val const_tab = map2 (fn const => fn NONE => + error ("Constant " ^ (quote o Code_Unit.string_of_const thy) const + ^ "\nhas a user-defined serialization") + | SOME const' => (const, const')) consts consts'' + in (ml_code, const_tab) end; fun register_const const ctxt = let diff -r 64ab5bb68d4c -r bd8438543bf2 src/Tools/code/code_name.ML --- a/src/Tools/code/code_name.ML Wed Oct 22 14:15:44 2008 +0200 +++ b/src/Tools/code/code_name.ML Wed Oct 22 14:15:45 2008 +0200 @@ -2,62 +2,45 @@ ID: $Id$ Author: Florian Haftmann, TU Muenchen -Naming policies for code generation: prefixing any name by corresponding -theory name, conversion to alphanumeric representation. -Mappings are incrementally cached. Assumes non-concurrent processing -inside a single theory. +Some code generator infrastructure concerning names. *) signature CODE_NAME = sig - val read_const_exprs: theory -> string list -> string list * string list + structure StringPairTab: TABLE + val first_upper: string -> string + val first_lower: string -> string + val dest_name: string -> string * string val purify_var: string -> string val purify_tvar: string -> string val purify_sym: string -> string + val purify_base: bool -> string -> string val check_modulename: string -> string - val class: theory -> class -> class - val class_rev: theory -> class -> class option - val classrel: theory -> class * class -> string - val classrel_rev: theory -> string -> (class * class) option - val tyco: theory -> string -> string - val tyco_rev: theory -> string -> string option - val instance: theory -> class * string -> string - val instance_rev: theory -> string -> (class * string) option - val const: theory -> string -> string - val const_rev: theory -> string -> string option - val value_name: string - val labelled_name: theory -> string -> string + type var_ctxt + val make_vars: string list -> var_ctxt + val intro_vars: string list -> var_ctxt -> var_ctxt + val lookup_var: var_ctxt -> string -> string - val setup: theory -> theory + val read_const_exprs: theory -> string list -> string list * string list + val mk_name_module: Name.context -> string option -> (string -> string option) + -> 'a Graph.T -> string -> string end; structure Code_Name: CODE_NAME = struct -(** constant expressions **) +(** auxiliary **) + +structure StringPairTab = + TableFun(type key = string * string val ord = prod_ord fast_string_ord fast_string_ord); -fun read_const_exprs thy = - let - fun consts_of some_thyname = - let - val thy' = case some_thyname - of SOME thyname => ThyInfo.the_theory thyname thy - | NONE => thy; - val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I) - ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') []; - fun belongs_here c = - not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy')) - in case some_thyname - of NONE => cs - | SOME thyname => filter belongs_here cs - end; - fun read_const_expr "*" = ([], consts_of NONE) - | read_const_expr s = if String.isSuffix ".*" s - then ([], consts_of (SOME (unsuffix ".*" s))) - else ([Code_Unit.read_const thy s], []); - in pairself flat o split_list o map read_const_expr end; +val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode; +val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode; + +val dest_name = + apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode; (** purification **) @@ -92,82 +75,16 @@ | purify_tvar v = (unprefix "'" #> explode #> filter Symbol.is_ascii_letter #> cons "'" #> implode) v; -fun check_modulename mn = - let - val mns = NameSpace.explode mn; - val mns' = map (purify_name true false) mns; - in - if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n" - ^ "perhaps try " ^ quote (NameSpace.implode mns')) - end; - - -(** global names (identifiers) **) - -(* identifier categories *) - -val suffix_class = "class"; -val suffix_classrel = "classrel" -val suffix_tyco = "tyco"; -val suffix_instance = "inst"; -val suffix_const = "const"; - -fun string_of_classrel (class, superclass) = class ^ " < " ^ superclass; -fun string_of_instance (class, tyco) = tyco ^ " :: " ^ class; - -fun add_suffix nsp name = - NameSpace.append name nsp; - -fun dest_suffix nsp name = - if NameSpace.base name = nsp - then SOME (NameSpace.qualifier name) - else NONE; - -local - -val name_mapping = [ - (suffix_class, "class"), - (suffix_classrel, "subclass relation"), - (suffix_tyco, "type constructor"), - (suffix_instance, "instance"), - (suffix_const, "constant") -] - -in - -val category_of = the o AList.lookup (op =) name_mapping o NameSpace.base; - -end; - - -(* theory name lookup *) - -local - fun thyname_of thy f x = the (AList.lookup (op =) (f x) Markup.theory_nameN); -in - fun thyname_of_class thy = - thyname_of thy (ProofContext.query_class (ProofContext.init thy)); - fun thyname_of_tyco thy = - thyname_of thy (Type.the_tags (Sign.tsig_of thy)); - fun thyname_of_instance thy a = case AxClass.arity_property thy a Markup.theory_nameN - of [] => error ("no such instance: " ^ (quote o string_of_instance) a) - | thyname :: _ => thyname; - fun thyname_of_const thy = - thyname_of thy (Consts.the_tags (Sign.consts_of thy)); -end; - - -(* naming policies *) - val purify_prefix = explode - (*should disappear as soon as hierarchical theory name spaces are available*) + (*FIMXE should disappear as soon as hierarchical theory name spaces are available*) #> Symbol.scanner "Malformed name" (Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.is_regular)) #> implode #> NameSpace.explode #> map (purify_name true false); +(*FIMXE non-canonical function treating non-canonical names*) fun purify_base _ "op &" = "and" | purify_base _ "op |" = "or" | purify_base _ "op -->" = "implies" @@ -183,227 +100,73 @@ val purify_sym = purify_base false; -fun default_policy thy get_basename get_thyname name = +fun check_modulename mn = let - val prefix = (purify_prefix o get_thyname thy) name; - val base = (purify_base true o get_basename) name; - in NameSpace.implode (prefix @ [base]) end; - -fun class_policy thy = default_policy thy NameSpace.base thyname_of_class; -fun classrel_policy thy = default_policy thy (fn (class1, class2) => - NameSpace.base class2 ^ "_" ^ NameSpace.base class1) (fn thy => thyname_of_class thy o fst); - (*order fits nicely with composed projections*) -fun tyco_policy thy = default_policy thy NameSpace.base thyname_of_tyco; -fun instance_policy thy = default_policy thy (fn (class, tyco) => - NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance; - -fun force_thyname thy c = case Code.get_datatype_of_constr thy c - of SOME dtco => SOME (thyname_of_tyco thy dtco) - | NONE => (case AxClass.class_of_param thy c - of SOME class => SOME (thyname_of_class thy class) - | NONE => (case AxClass.inst_of_param thy c - of SOME (c, tyco) => SOME (thyname_of_instance thy - ((the o AxClass.class_of_param thy) c, tyco)) - | NONE => NONE)); - -fun const_policy thy c = - case force_thyname thy c - of NONE => default_policy thy NameSpace.base thyname_of_const c - | SOME thyname => let - val prefix = purify_prefix thyname; - val base = (purify_base true o NameSpace.base) c; - in NameSpace.implode (prefix @ [base]) end; - - -(* theory and code data *) - -type tyco = string; -type const = string; - -structure StringPairTab = - TableFun( - type key = string * string; - val ord = prod_ord fast_string_ord fast_string_ord; - ); - -datatype names = Names of { - class: class Symtab.table * class Symtab.table, - classrel: string StringPairTab.table * (class * class) Symtab.table, - tyco: tyco Symtab.table * tyco Symtab.table, - instance: string StringPairTab.table * (class * tyco) Symtab.table -} - -val empty_names = Names { - class = (Symtab.empty, Symtab.empty), - classrel = (StringPairTab.empty, Symtab.empty), - tyco = (Symtab.empty, Symtab.empty), - instance = (StringPairTab.empty, Symtab.empty) -}; - -local - fun mk_names (class, classrel, tyco, instance) = - Names { class = class, classrel = classrel, tyco = tyco, instance = instance }; - fun map_names f (Names { class, classrel, tyco, instance }) = - mk_names (f (class, classrel, tyco, instance)); -in - fun merge_names (Names { class = (class1, classrev1), - classrel = (classrel1, classrelrev1), tyco = (tyco1, tycorev1), - instance = (instance1, instancerev1) }, - Names { class = (class2, classrev2), - classrel = (classrel2, classrelrev2), tyco = (tyco2, tycorev2), - instance = (instance2, instancerev2) }) = - mk_names ((Symtab.merge (op =) (class1, class2), Symtab.merge (op =) (classrev1, classrev2)), - (StringPairTab.merge (op =) (classrel1, classrel2), Symtab.merge (op =) (classrelrev1, classrelrev2)), - (Symtab.merge (op =) (tyco1, tyco2), Symtab.merge (op =) (tycorev1, tycorev2)), - (StringPairTab.merge (op =) (instance1, instance2), Symtab.merge (op =) (instancerev1, instancerev2))); - fun map_class f = map_names - (fn (class, classrel, tyco, inst) => (f class, classrel, tyco, inst)); - fun map_classrel f = map_names - (fn (class, classrel, tyco, inst) => (class, f classrel, tyco, inst)); - fun map_tyco f = map_names - (fn (class, classrel, tyco, inst) => (class, classrel, f tyco, inst)); - fun map_instance f = map_names - (fn (class, classrel, tyco, inst) => (class, classrel, tyco, f inst)); -end; (*local*) - -structure Code_Name = TheoryDataFun -( - type T = names ref; - val empty = ref empty_names; - fun copy (ref names) = ref names; - val extend = copy; - fun merge _ (ref names1, ref names2) = ref (merge_names (names1, names2)); -); - -structure ConstName = CodeDataFun -( - type T = const Symtab.table * string Symtab.table; - val empty = (Symtab.empty, Symtab.empty); - fun purge _ cs (const, constrev) = (fold Symtab.delete_safe cs const, - fold Symtab.delete_safe (map_filter (Symtab.lookup const) cs) constrev); -); - -val setup = Code_Name.init; - - -(* forward lookup with cache update *) - -fun get thy get_tabs get upd_names upd policy x = - let - val names_ref = Code_Name.get thy; - val (Names names) = ! names_ref; - val tabs = get_tabs names; - fun declare name = - let - val names' = upd_names (K (upd (x, name) (fst tabs), - Symtab.update_new (name, x) (snd tabs))) (Names names) - in (names_ref := names'; name) end; - in case get (fst tabs) x - of SOME name => name - | NONE => - x - |> policy thy - |> Name.variant (Symtab.keys (snd tabs)) - |> declare - end; - -fun get_const thy const = - let - val tabs = ConstName.get thy; - fun declare name = - let - val names' = (Symtab.update (const, name) (fst tabs), - Symtab.update_new (name, const) (snd tabs)) - in (ConstName.change thy (K names'); name) end; - in case Symtab.lookup (fst tabs) const - of SOME name => name - | NONE => - const - |> const_policy thy - |> Name.variant (Symtab.keys (snd tabs)) - |> declare + val mns = NameSpace.explode mn; + val mns' = map (purify_name true false) mns; + in + if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n" + ^ "perhaps try " ^ quote (NameSpace.implode mns')) end; -(* backward lookup *) +(** variable name contexts **) + +type var_ctxt = string Symtab.table * Name.context; -fun rev thy get_tabs name = +fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty, + Name.make_context names); + +fun intro_vars names (namemap, namectxt) = let - val names_ref = Code_Name.get thy - val (Names names) = ! names_ref; - val tab = (snd o get_tabs) names; - in case Symtab.lookup tab name - of SOME x => x - | NONE => error ("No such " ^ category_of name ^ ": " ^ quote name) - end; + val (names', namectxt') = Name.variants names namectxt; + val namemap' = fold2 (curry Symtab.update) names names' namemap; + in (namemap', namectxt') end; -fun rev_const thy name = - let - val tab = snd (ConstName.get thy); - in case Symtab.lookup tab name - of SOME const => const - | NONE => error ("No such " ^ category_of name ^ ": " ^ quote name) - end; +fun lookup_var (namemap, _) name = case Symtab.lookup namemap name + of SOME name' => name' + | NONE => error ("Invalid name in context: " ^ quote name); -(* external interfaces *) - -fun class thy = - get thy #class Symtab.lookup map_class Symtab.update class_policy - #> add_suffix suffix_class; -fun classrel thy = - get thy #classrel StringPairTab.lookup map_classrel StringPairTab.update classrel_policy - #> add_suffix suffix_classrel; -fun tyco thy = - get thy #tyco Symtab.lookup map_tyco Symtab.update tyco_policy - #> add_suffix suffix_tyco; -fun instance thy = - get thy #instance StringPairTab.lookup map_instance StringPairTab.update instance_policy - #> add_suffix suffix_instance; -fun const thy = - get_const thy - #> add_suffix suffix_const; +(** misc **) -fun class_rev thy = - dest_suffix suffix_class - #> Option.map (rev thy #class); -fun classrel_rev thy = - dest_suffix suffix_classrel - #> Option.map (rev thy #classrel); -fun tyco_rev thy = - dest_suffix suffix_tyco - #> Option.map (rev thy #tyco); -fun instance_rev thy = - dest_suffix suffix_instance - #> Option.map (rev thy #instance); -fun const_rev thy = - dest_suffix suffix_const - #> Option.map (rev_const thy); - -local +fun read_const_exprs thy = + let + fun consts_of some_thyname = + let + val thy' = case some_thyname + of SOME thyname => ThyInfo.the_theory thyname thy + | NONE => thy; + val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I) + ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') []; + fun belongs_here c = + not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy')) + in case some_thyname + of NONE => cs + | SOME thyname => filter belongs_here cs + end; + fun read_const_expr "*" = ([], consts_of NONE) + | read_const_expr s = if String.isSuffix ".*" s + then ([], consts_of (SOME (unsuffix ".*" s))) + else ([Code_Unit.read_const thy s], []); + in pairself flat o split_list o map read_const_expr end; -val f_mapping = [ - (suffix_class, class_rev), - (suffix_classrel, Option.map string_of_classrel oo classrel_rev), - (suffix_tyco, tyco_rev), - (suffix_instance, Option.map string_of_instance oo instance_rev), - (suffix_const, fn thy => Option.map (Code_Unit.string_of_const thy) o const_rev thy) -]; - -in - -val value_name = "Isabelle_Eval.EVAL.EVAL" - -fun labelled_name thy suffix_name = if suffix_name = value_name then "" else +fun mk_name_module reserved_names module_prefix module_alias program = let - val category = category_of suffix_name; - val name = NameSpace.qualifier suffix_name; - val suffix = NameSpace.base suffix_name - in case (the o AList.lookup (op =) f_mapping) suffix thy suffix_name - of SOME thing => category ^ " " ^ quote thing - | NONE => error ("Unknown name: " ^ quote name) - end; + fun mk_alias name = case module_alias name + of SOME name' => name' + | NONE => name + |> NameSpace.explode + |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names)) + |> NameSpace.implode; + fun mk_prefix name = case module_prefix + of SOME module_prefix => NameSpace.append module_prefix name + | NONE => name; + val tab = + Symtab.empty + |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name)) + o fst o dest_name o fst) + program + in the o Symtab.lookup tab end; end; - -end; diff -r 64ab5bb68d4c -r bd8438543bf2 src/Tools/code/code_printer.ML --- a/src/Tools/code/code_printer.ML Wed Oct 22 14:15:44 2008 +0200 +++ b/src/Tools/code/code_printer.ML Wed Oct 22 14:15:45 2008 +0200 @@ -7,15 +7,7 @@ signature CODE_PRINTER = sig - val first_upper: string -> string - val first_lower: string -> string - val dest_name: string -> string * string - val mk_name_module: Name.context -> string option -> (string -> string option) - -> 'a Graph.T -> string -> string - type var_ctxt; - val make_vars: string list -> var_ctxt; - val intro_vars: string list -> var_ctxt -> var_ctxt; - val lookup_var: var_ctxt -> string -> string; + val nerror: thm -> string -> 'a val @@ : 'a * 'a -> 'a list val @| : 'a list * 'a -> 'a list @@ -45,19 +37,21 @@ type tyco_syntax type const_syntax val parse_infix: ('a -> 'b) -> lrx * int -> string - -> int * ((fixity -> 'b -> Pretty.T) -> fixity -> 'a list -> Pretty.T) + -> int * ((fixity -> 'b -> Pretty.T) + -> fixity -> 'a list -> Pretty.T) val parse_syntax: ('a -> 'b) -> OuterParse.token list - -> (int * ((fixity -> 'b -> Pretty.T) -> fixity -> 'a list -> Pretty.T)) option - * OuterParse.token list - val simple_const_syntax: (int * ((fixity -> iterm -> Pretty.T) -> fixity - -> (iterm * itype) list -> Pretty.T)) option -> const_syntax option - val gen_pr_app: (thm -> bool -> var_ctxt -> const * iterm list -> Pretty.T list) - -> (thm -> bool -> var_ctxt -> fixity -> iterm -> Pretty.T) - -> (string -> const_syntax option) -> (string -> bool) - -> thm -> bool -> var_ctxt -> fixity -> const * iterm list -> Pretty.T + -> (int * ((fixity -> 'b -> Pretty.T) + -> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list + val simple_const_syntax: (int * ((fixity -> iterm -> Pretty.T) + -> fixity -> (iterm * itype) list -> Pretty.T)) option -> const_syntax option + val gen_pr_app: (thm -> bool -> Code_Name.var_ctxt -> const * iterm list -> Pretty.T list) + -> (thm -> bool -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T) + -> (string -> const_syntax option) -> (string -> bool) -> Code_Thingol.naming + -> thm -> bool -> Code_Name.var_ctxt -> fixity -> const * iterm list -> Pretty.T val gen_pr_bind: ((string option * Pretty.T option) * itype -> Pretty.T) - -> (thm -> bool -> var_ctxt -> fixity -> iterm -> Pretty.T) - -> thm -> fixity -> (string option * iterm option) * itype -> var_ctxt -> Pretty.T * var_ctxt + -> (thm -> bool -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T) + -> thm -> fixity + -> (string option * iterm option) * itype -> Code_Name.var_ctxt -> Pretty.T * Code_Name.var_ctxt type literals val Literals: { literal_char: string -> string, literal_string: string -> string, @@ -68,8 +62,6 @@ val literal_numeral: literals -> bool -> int -> string val literal_list: literals -> Pretty.T list -> Pretty.T val infix_cons: literals -> int * string - - val nerror: thm -> string -> 'a end; structure Code_Printer : CODE_PRINTER = @@ -79,52 +71,6 @@ fun nerror thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm thm); -(** names and naming **) - -(* auxiliary *) - -val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode; -val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode; - -val dest_name = - apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode; - -fun mk_name_module reserved_names module_prefix module_alias program = - let - fun mk_alias name = case module_alias name - of SOME name' => name' - | NONE => name - |> NameSpace.explode - |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names)) - |> NameSpace.implode; - fun mk_prefix name = case module_prefix - of SOME module_prefix => NameSpace.append module_prefix name - | NONE => name; - val tab = - Symtab.empty - |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name)) - o fst o dest_name o fst) - program - in the o Symtab.lookup tab end; - -(* variable name contexts *) - -type var_ctxt = string Symtab.table * Name.context; - -fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty, - Name.make_context names); - -fun intro_vars names (namemap, namectxt) = - let - val (names', namectxt') = Name.variants names namectxt; - val namemap' = fold2 (curry Symtab.update) names names' namemap; - in (namemap', namectxt') end; - -fun lookup_var (namemap, _) name = case Symtab.lookup namemap name - of SOME name' => name' - | NONE => error ("Invalid name in context: " ^ quote name); - - (** assembling text pieces **) infixr 5 @@; @@ -182,19 +128,13 @@ type class_syntax = string * (string -> string option); type tyco_syntax = int * ((fixity -> itype -> Pretty.T) -> fixity -> itype list -> Pretty.T); -type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T) - -> thm -> bool -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T); +type const_syntax = int * ((Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T) + -> Code_Thingol.naming -> thm -> bool -> Code_Name.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T); fun simple_const_syntax x = (Option.map o apsnd) - (fn pretty => fn pr => fn thm => fn pat => fn vars => pretty (pr vars)) x; - -(*int * ((var_ctxt -> fixity -> iterm -> Pretty.T) - -> ) + (fn pretty => fn pr => fn naming => fn thm => fn pat => fn vars => pretty (pr vars)) x; -('a * ('b -> thm -> bool -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T)) option -*** -> ('a * (('d -> 'b) -> 'e -> 'f -> 'd -> 'c)) option*) - -fun gen_pr_app pr_app pr_term syntax_const is_cons thm pat +fun gen_pr_app pr_app pr_term syntax_const is_cons naming thm pat vars fxy (app as ((c, (_, tys)), ts)) = case syntax_const c of NONE => if pat andalso not (is_cons c) then @@ -202,7 +142,7 @@ else brackify fxy (pr_app thm pat vars app) | SOME (k, pr) => let - fun pr' fxy ts = pr (pr_term thm pat) thm pat vars fxy (ts ~~ curry Library.take k tys); + fun pr' fxy ts = pr (pr_term thm pat) naming thm pat vars fxy (ts ~~ curry Library.take k tys); in if k = length ts then pr' fxy ts else if k < length ts @@ -216,9 +156,9 @@ val vs = case 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 vars' = Code_Name.intro_vars (the_list v) vars; + val vars'' = Code_Name.intro_vars vs vars'; + val v' = Option.map (Code_Name.lookup_var vars') v; val pat' = Option.map (pr_term thm true vars'' fxy) pat; in (pr_bind ((v', pat'), ty), vars'') end; diff -r 64ab5bb68d4c -r bd8438543bf2 src/Tools/code/code_target.ML --- a/src/Tools/code/code_target.ML Wed Oct 22 14:15:44 2008 +0200 +++ b/src/Tools/code/code_target.ML Wed Oct 22 14:15:45 2008 +0200 @@ -11,7 +11,8 @@ type serializer val add_target: string * (serializer * literals) -> theory -> theory - val extend_target: string * (string * (Code_Thingol.program -> Code_Thingol.program)) + val extend_target: string * + (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program)) -> theory -> theory val assert_target: theory -> string -> string @@ -24,20 +25,18 @@ val code_writeln: Pretty.T -> unit val mk_serialization: string -> ('a -> unit) option -> (Path.T option -> 'a -> unit) - -> ('a -> string * string list) + -> ('a -> string * string option list) -> 'a -> serialization val serialize: theory -> string -> string option -> Args.T list - -> Code_Thingol.program -> string list -> serialization + -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization val serialize_custom: theory -> string * (serializer * literals) - -> Code_Thingol.program -> string list -> string * string list + -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list val the_literals: theory -> string -> literals val compile: serialization -> unit val export: serialization -> unit val file: Path.T -> serialization -> unit val string: string list -> serialization -> string - val code_of: theory -> string -> string -> string list -> string list -> string - val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit val code_width: int ref val allow_abort: string -> theory -> theory @@ -45,11 +44,7 @@ -> (string * (string * string) list) option -> theory -> theory val add_syntax_inst: string -> string * class -> bool -> theory -> theory val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory - val add_syntax_tycoP: string -> string -> OuterParse.token list - -> (theory -> theory) * OuterParse.token list val add_syntax_const: string -> string -> const_syntax option -> theory -> theory - val add_syntax_constP: string -> string -> OuterParse.token list - -> (theory -> theory) * OuterParse.token list val add_reserved: string -> string -> theory -> theory end; @@ -62,7 +57,7 @@ (** basics **) datatype destination = Compile | Export | File of Path.T | String of string list; -type serialization = destination -> (string * string list) option; +type serialization = destination -> (string * string option list) option; val code_width = ref 80; (*FIXME after Pretty module no longer depends on print mode*) fun code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin (!code_width) f); @@ -87,22 +82,24 @@ (** theory data **) +structure StringPairTab = Code_Name.StringPairTab; + datatype name_syntax_table = NameSyntaxTable of { class: class_syntax Symtab.table, - inst: unit Symtab.table, + instance: unit StringPairTab.table, tyco: tyco_syntax Symtab.table, const: const_syntax Symtab.table }; -fun mk_name_syntax_table ((class, inst), (tyco, const)) = - NameSyntaxTable { class = class, inst = inst, tyco = tyco, const = const }; -fun map_name_syntax_table f (NameSyntaxTable { class, inst, tyco, const }) = - mk_name_syntax_table (f ((class, inst), (tyco, const))); -fun merge_name_syntax_table (NameSyntaxTable { class = class1, inst = inst1, tyco = tyco1, const = const1 }, - NameSyntaxTable { class = class2, inst = inst2, tyco = tyco2, const = const2 }) = +fun mk_name_syntax_table ((class, instance), (tyco, const)) = + NameSyntaxTable { class = class, instance = instance, tyco = tyco, const = const }; +fun map_name_syntax_table f (NameSyntaxTable { class, instance, tyco, const }) = + mk_name_syntax_table (f ((class, instance), (tyco, const))); +fun merge_name_syntax_table (NameSyntaxTable { class = class1, instance = instance1, tyco = tyco1, const = const1 }, + NameSyntaxTable { class = class2, instance = instance2, tyco = tyco2, const = const2 }) = mk_name_syntax_table ( (Symtab.join (K snd) (class1, class2), - Symtab.join (K snd) (inst1, inst2)), + StringPairTab.join (K snd) (instance1, instance2)), (Symtab.join (K snd) (tyco1, tyco2), Symtab.join (K snd) (const1, const2)) ); @@ -117,12 +114,13 @@ -> (string -> class_syntax option) -> (string -> tyco_syntax option) -> (string -> const_syntax option) + -> Code_Thingol.naming -> Code_Thingol.program -> string list (*selected statements*) -> serialization; datatype serializer_entry = Serializer of serializer * literals - | Extends of string * (Code_Thingol.program -> Code_Thingol.program); + | Extends of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program); datatype target = Target of { serial: serial, @@ -178,19 +176,25 @@ fun put_target (target, seri) thy = let - val defined_target = is_some o Symtab.lookup (fst (CodeTargetData.get thy)); + val lookup_target = Symtab.lookup (fst (CodeTargetData.get thy)); val _ = case seri - of Extends (super, _) => if defined_target super then () + of Extends (super, _) => if is_some (lookup_target super) then () else error ("Unknown code target language: " ^ quote super) | _ => (); - val _ = if defined_target target + val overwriting = case (Option.map the_serializer o lookup_target) target + of NONE => false + | SOME (Extends _) => true + | SOME (Serializer _) => (case seri + of Extends _ => error ("Will not overwrite existing target " ^ quote target) + | _ => true); + val _ = if overwriting then warning ("Overwriting existing target " ^ quote target) - else (); + else (); in thy |> (CodeTargetData.map o apfst oo Symtab.map_default) (target, mk_target ((serial (), seri), (([], Symtab.empty), - (mk_name_syntax_table ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)), + (mk_name_syntax_table ((Symtab.empty, StringPairTab.empty), (Symtab.empty, Symtab.empty)), Symtab.empty)))) ((map_target o apfst o apsnd o K) seri) end; @@ -241,9 +245,8 @@ fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy = let val class = prep_class thy raw_class; - val class' = Code_Name.class thy class; fun mk_classparam c = case AxClass.class_of_param thy c - of SOME class'' => if class = class'' then Code_Name.const thy c + of SOME class' => if class = class' then c else error ("Not a class operation for class " ^ quote class ^ ": " ^ quote c) | NONE => error ("Not a class operation: " ^ quote c); fun mk_syntax_params raw_params = AList.lookup (op =) @@ -252,30 +255,29 @@ of SOME (syntax, raw_params) => thy |> (map_name_syntax target o apfst o apfst) - (Symtab.update (class', (syntax, mk_syntax_params raw_params))) + (Symtab.update (class, (syntax, mk_syntax_params raw_params))) | NONE => thy |> (map_name_syntax target o apfst o apfst) - (Symtab.delete_safe class') + (Symtab.delete_safe class) end; fun gen_add_syntax_inst prep_class prep_tyco target (raw_tyco, raw_class) add_del thy = let - val inst = Code_Name.instance thy (prep_class thy raw_class, prep_tyco thy raw_tyco); + val inst = (prep_class thy raw_class, prep_tyco thy raw_tyco); in if add_del then thy |> (map_name_syntax target o apfst o apsnd) - (Symtab.update (inst, ())) + (StringPairTab.update (inst, ())) else thy |> (map_name_syntax target o apfst o apsnd) - (Symtab.delete_safe inst) + (StringPairTab.delete_safe inst) end; fun gen_add_syntax_tyco prep_tyco target raw_tyco raw_syn thy = let val tyco = prep_tyco thy raw_tyco; - val tyco' = if tyco = "fun" then "fun" else Code_Name.tyco thy tyco; fun check_args (syntax as (n, _)) = if n <> Sign.arity_number thy tyco then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco) else syntax @@ -283,17 +285,16 @@ of SOME syntax => thy |> (map_name_syntax target o apsnd o apfst) - (Symtab.update (tyco', check_args syntax)) + (Symtab.update (tyco, check_args syntax)) | NONE => thy |> (map_name_syntax target o apsnd o apfst) - (Symtab.delete_safe tyco') + (Symtab.delete_safe tyco) end; fun gen_add_syntax_const prep_const target raw_c raw_syn thy = let val c = prep_const thy raw_c; - val c' = Code_Name.const thy c; fun check_args (syntax as (n, _)) = if n > Code_Unit.no_args thy c then error ("Too many arguments in syntax for constant " ^ quote c) else syntax; @@ -301,11 +302,11 @@ of SOME syntax => thy |> (map_name_syntax target o apsnd o apsnd) - (Symtab.update (c', check_args syntax)) + (Symtab.update (c, check_args syntax)) | NONE => thy |> (map_name_syntax target o apsnd o apsnd) - (Symtab.delete_safe c') + (Symtab.delete_safe c) end; fun add_reserved target = @@ -330,11 +331,10 @@ fun add_module_alias target = map_module_alias target o Symtab.update o apsnd Code_Name.check_modulename; -fun gen_allow_abort prep_cs raw_c thy = +fun gen_allow_abort prep_const raw_c thy = let - val c = prep_cs thy raw_c; - val c' = Code_Name.const thy c; - in thy |> (CodeTargetData.map o apsnd) (insert (op =) c') end; + val c = prep_const thy raw_c; + in thy |> (CodeTargetData.map o apsnd) (insert (op =) c) end; fun zip_list (x::xs) f g = f @@ -355,8 +355,6 @@ in -val parse_syntax = parse_syntax; - val add_syntax_class = gen_add_syntax_class cert_class (K I); val add_syntax_inst = gen_add_syntax_inst cert_class cert_tyco; val add_syntax_tyco = gen_add_syntax_tyco cert_tyco; @@ -370,11 +368,6 @@ val add_syntax_const_cmd = gen_add_syntax_const Code_Unit.read_const; val allow_abort_cmd = gen_allow_abort Code_Unit.read_const; -fun add_syntax_tycoP target tyco = parse_syntax I - >> add_syntax_tyco_cmd target tyco; -fun add_syntax_constP target c = parse_syntax fst - >> (add_syntax_const_cmd target c o Code_Printer.simple_const_syntax); - fun the_literals thy = let val (targets, _) = CodeTargetData.get thy; @@ -390,27 +383,63 @@ (* montage *) -fun invoke_serializer thy modify abortable serializer reserved includes - module_alias class inst tyco const module args program1 cs1 = +local + +fun labelled_name thy program name = case Graph.get_node program name + of Code_Thingol.Fun (c, _) => quote (Code_Unit.string_of_const thy c) + | Code_Thingol.Datatype (tyco, _) => "type " ^ quote (Sign.extern_type thy tyco) + | Code_Thingol.Datatypecons (c, _) => quote (Code_Unit.string_of_const thy c) + | Code_Thingol.Class (class, _) => "class " ^ quote (Sign.extern_class thy class) + | Code_Thingol.Classrel (sub, super) => let + val Code_Thingol.Class (sub, _) = Graph.get_node program sub + val Code_Thingol.Class (super, _) = Graph.get_node program super + in quote (Sign.extern_class thy sub ^ " < " ^ Sign.extern_class thy super) end + | Code_Thingol.Classparam (c, _) => quote (Code_Unit.string_of_const thy c) + | Code_Thingol.Classinst ((class, (tyco, _)), _) => let + val Code_Thingol.Class (class, _) = Graph.get_node program class + val Code_Thingol.Datatype (tyco, _) = Graph.get_node program tyco + in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end + +fun invoke_serializer thy abortable serializer reserved includes + module_alias class instance tyco const module args naming program2 names1 = let - val program2 = modify program1; - val hidden = Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const; - val cs2 = subtract (op =) hidden cs1; - val program3 = Graph.subgraph (not o member (op =) hidden) program2; - val all_cs = Graph.all_succs program2 cs2; - val program4 = Graph.subgraph (member (op =) all_cs) program3; + fun distill_names lookup_name src_tab = Symtab.empty + |> fold_map (fn thing_identifier => fn tab => case lookup_name naming thing_identifier + of SOME name => (SOME name, Symtab.update_new (name, the (Symtab.lookup src_tab thing_identifier)) tab) + | NONE => (NONE, tab)) (Symtab.keys src_tab) + |>> map_filter I; + fun lookup_classparam_rev c' = case try (Graph.get_node program2) c' + of SOME (Code_Thingol.Classparam (c, _)) => SOME c + | NONE => NONE; + fun lookup_tyco_fun naming "fun" = SOME "fun" + | lookup_tyco_fun naming tyco = Code_Thingol.lookup_tyco naming tyco; + val (names_class, class') = distill_names Code_Thingol.lookup_class class; + val class'' = class' + |> (Symtab.map o apsnd) (fn class_params => fn c' => + case lookup_classparam_rev c' + of SOME c => class_params c + | NONE => NONE) + val names_inst = map_filter (Code_Thingol.lookup_instance naming) + (StringPairTab.keys instance); + val (names_tyco, tyco') = distill_names lookup_tyco_fun tyco; + val (names_const, const') = distill_names Code_Thingol.lookup_const const; + val names_hidden = names_class @ names_inst @ names_tyco @ names_const; + val names2 = subtract (op =) names_hidden names1; + val program3 = Graph.subgraph (not o member (op =) names_hidden) program2; + val names_all = Graph.all_succs program2 names2; + val program4 = Graph.subgraph (member (op =) names_all) program3; val empty_funs = filter_out (member (op =) abortable) (Code_Thingol.empty_funs program3); val _ = if null empty_funs then () else error ("No defining equations for " - ^ commas (map (Code_Name.labelled_name thy) empty_funs)); + ^ commas (map (Sign.extern_const thy) empty_funs)); in - serializer module args (Code_Name.labelled_name thy) reserved includes - (Symtab.lookup module_alias) (Symtab.lookup class) - (Symtab.lookup tyco) (Symtab.lookup const) - program4 cs2 + serializer module args (labelled_name thy program2) reserved includes + (Symtab.lookup module_alias) (Symtab.lookup class'') + (Symtab.lookup tyco') (Symtab.lookup const') + naming program4 names2 end; -fun mount_serializer thy alt_serializer target = +fun mount_serializer thy alt_serializer target module args naming program = let val (targets, abortable) = CodeTargetData.get thy; fun collapse_hierarchy target = @@ -422,7 +451,7 @@ of Serializer _ => (I, data) | Extends (super, modify) => let val (modify', data') = collapse_hierarchy super - in (modify' #> modify, merge_target false target (data', data)) end + in (modify' #> modify naming, merge_target false target (data', data)) end end; val (modify, data) = collapse_hierarchy target; val (serializer, _) = the_default (case the_serializer data @@ -430,18 +459,22 @@ val reserved = the_reserved data; val includes = Symtab.dest (the_includes data); val module_alias = the_module_alias data; - val { class, inst, tyco, const } = the_name_syntax data; + val { class, instance, tyco, const } = the_name_syntax data; in - invoke_serializer thy modify abortable serializer reserved - includes module_alias class inst tyco const + invoke_serializer thy abortable serializer reserved + includes module_alias class instance tyco const module args naming (modify program) end; +in + fun serialize thy = mount_serializer thy NONE; -fun serialize_custom thy (target_name, seri) program cs = - mount_serializer thy (SOME seri) target_name NONE [] program cs (String []) +fun serialize_custom thy (target_name, seri) naming program cs = + mount_serializer thy (SOME seri) target_name NONE [] naming program cs (String []) |> the; +end; (* local *) + fun parse_args f args = case Scan.read OuterLex.stopper f args of SOME x => x @@ -450,40 +483,47 @@ (* code presentation *) -fun code_of thy target module_name cs stmt_names = +fun code_of thy target module_name cs names_stmt = let - val (cs', program) = Code_Thingol.consts_program thy cs; + val (names_cs, (naming, program)) = Code_Thingol.consts_program thy cs; in - string stmt_names (serialize thy target (SOME module_name) [] program cs') + string names_stmt (serialize thy target (SOME module_name) [] + naming program names_cs) end; (* code generation *) +fun transitivly_non_empty_funs thy naming program = + let + val cs = subtract (op =) (abort_allowed thy) (Code_Thingol.empty_funs program); + val names = map_filter (Code_Thingol.lookup_const naming) cs; + in subtract (op =) (Graph.all_preds program names) (Graph.keys program) end; + fun read_const_exprs thy cs = let val (cs1, cs2) = Code_Name.read_const_exprs thy cs; - val (cs3, program) = Code_Thingol.consts_program thy cs2; - val cs4 = Code_Thingol.transitivly_non_empty_funs program (abort_allowed thy); + val (names3, (naming, program)) = Code_Thingol.consts_program thy cs2; + val names4 = transitivly_non_empty_funs thy naming program; val cs5 = map_filter - (fn (c, c') => if member (op =) cs4 c' then SOME c else NONE) (cs2 ~~ cs3); + (fn (c, name) => if member (op =) names4 name then SOME c else NONE) (cs2 ~~ names3); in fold (insert (op =)) cs5 cs1 end; fun cached_program thy = let - val program = Code_Thingol.cached_program thy; - in (Code_Thingol.transitivly_non_empty_funs program (abort_allowed thy), program) end + val (naming, program) = Code_Thingol.cached_program thy; + in (transitivly_non_empty_funs thy naming program, (naming, program)) end fun export_code thy cs seris = let - val (cs', program) = if null cs then cached_program thy + val (cs', (naming, program)) = if null cs then cached_program thy else Code_Thingol.consts_program thy cs; fun mk_seri_dest dest = case dest of NONE => compile | SOME "-" => export | SOME f => file (Path.explode f) val _ = map (fn (((target, module), dest), args) => - (mk_seri_dest dest (serialize thy target module args program cs'))) seris; + (mk_seri_dest dest (serialize thy target module args naming program cs'))) seris; in () end; fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) seris; @@ -563,13 +603,6 @@ OuterSyntax.command "export_code" "generate executable code for constants" K.diag (P.!!! (code_exprP export_code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of))); -fun shell_command thyname cmd = Toplevel.program (fn _ => - (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! (code_exprP export_code_cmd)) - ((filter OuterLex.is_proper o OuterSyntax.scan Position.none) cmd) - of SOME f => (writeln "Now generating code..."; f (theory thyname)) - | NONE => error ("Bad directive " ^ quote cmd))) - handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure; - end; (*local*) end; (*struct*) diff -r 64ab5bb68d4c -r bd8438543bf2 src/Tools/code/code_thingol.ML --- a/src/Tools/code/code_thingol.ML Wed Oct 22 14:15:44 2008 +0200 +++ b/src/Tools/code/code_thingol.ML Wed Oct 22 14:15:45 2008 +0200 @@ -40,53 +40,59 @@ signature CODE_THINGOL = sig - include BASIC_CODE_THINGOL; - val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list; - 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 split_let: iterm -> (((iterm * itype) * iterm) * iterm) option; - val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm; + include BASIC_CODE_THINGOL + val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list + 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 split_let: iterm -> (((iterm * itype) * iterm) * iterm) option + val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm val unfold_const_app: iterm -> - ((string * (dict list list * itype list)) * iterm list) option; + ((string * (dict list list * itype list)) * iterm list) option val collapse_let: ((vname * itype) * iterm) * iterm - -> (iterm * itype) * (iterm * iterm) list; - val eta_expand: int -> (string * (dict list list * itype list)) * iterm list -> iterm; - val contains_dictvar: iterm -> bool; - val locally_monomorphic: iterm -> bool; - val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a; - val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a; - val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a; + -> (iterm * itype) * (iterm * iterm) list + val eta_expand: int -> (string * (dict list list * itype list)) * iterm list -> iterm + val contains_dictvar: iterm -> bool + val locally_monomorphic: iterm -> bool + val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a + val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a + val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a + + type naming + val lookup_class: naming -> class -> string option + val lookup_classrel: naming -> class * class -> string option + val lookup_tyco: naming -> string -> string option + val lookup_instance: naming -> class * string -> string option + val lookup_const: naming -> string -> string option datatype stmt = NoStmt - | Fun of typscheme * ((iterm list * iterm) * (thm * bool)) list - | Datatype of (vname * sort) list * (string * itype list) list - | Datatypecons of string - | Class of vname * ((class * string) list * (string * itype) list) + | Fun of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list) + | Datatype of string * ((vname * sort) list * (string * itype list) list) + | Datatypecons of string * string + | Class of class * (vname * ((class * string) list * (string * itype) list)) | Classrel of class * class - | Classparam of class + | Classparam of string * class | Classinst of (class * (string * (vname * sort) list)) * ((class * (string * (string * dict list list))) list - * ((string * const) * (thm * bool)) list); - type program = stmt Graph.T; - val empty_funs: program -> string list; - val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm; - val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt; - val transitivly_non_empty_funs: program -> string list -> string list; - val is_cons: program -> string -> bool; - val contr_classparam_typs: program -> string -> itype option list; + * ((string * const) * (thm * bool)) list) + type program = stmt Graph.T + val empty_funs: program -> string list + val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm + val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt + val is_cons: program -> string -> bool + val contr_classparam_typs: program -> string -> itype option list - val consts_program: theory -> string list -> string list * program; - val cached_program: theory -> program; + val consts_program: theory -> string list -> string list * (naming * program) + val cached_program: theory -> naming * program val eval_conv: theory - -> (term -> term * (program -> typscheme * iterm -> string list -> thm)) - -> cterm -> thm; + -> (term -> term * (naming -> program -> typscheme * iterm -> string list -> thm)) + -> cterm -> thm val eval_term: theory - -> (term -> term * (program -> typscheme * iterm -> string list -> 'a)) - -> term -> 'a; + -> (term -> term * (naming -> program -> typscheme * iterm -> string list -> 'a)) + -> term -> 'a end; structure Code_Thingol: CODE_THINGOL = @@ -109,8 +115,6 @@ (** language core - types, patterns, expressions **) -(* language representation *) - type vname = string; datatype dict = @@ -252,18 +256,148 @@ | locally_monomorphic (ICase ((_, ds), _)) = exists (locally_monomorphic o snd) ds; +(** naming policies **) + +(* identifier categories *) + +val suffix_class = "class"; +val suffix_classrel = "classrel" +val suffix_tyco = "tyco"; +val suffix_instance = "inst"; +val suffix_const = "const"; + +fun add_suffix nsp NONE = NONE + | add_suffix nsp (SOME name) = SOME (NameSpace.append name nsp); + + +(* policies *) + +local + fun thyname_of thy f x = the (AList.lookup (op =) (f x) Markup.theory_nameN); + fun thyname_of_class thy = + thyname_of thy (ProofContext.query_class (ProofContext.init thy)); + fun thyname_of_tyco thy = + thyname_of thy (Type.the_tags (Sign.tsig_of thy)); + fun thyname_of_instance thy inst = case AxClass.arity_property thy inst Markup.theory_nameN + of [] => error ("no such instance: " ^ quote (snd inst ^ " :: " ^ fst inst)) + | thyname :: _ => thyname; + fun thyname_of_const thy c = case Code.get_datatype_of_constr thy c + of SOME dtco => thyname_of_tyco thy dtco + | NONE => (case AxClass.class_of_param thy c + of SOME class => thyname_of_class thy class + | NONE => (case AxClass.inst_of_param thy c + of SOME (c, tyco) => thyname_of_instance thy + ((the o AxClass.class_of_param thy) c, tyco) + | NONE => thyname_of thy (Consts.the_tags (Sign.consts_of thy)) c)); + fun namify thy get_basename get_thyname name = + let + val prefix = get_thyname thy name; + val base = (Code_Name.purify_base true o get_basename) name; + in NameSpace.append prefix base end; +in + +fun namify_class thy = namify thy NameSpace.base thyname_of_class; +fun namify_classrel thy = namify thy (fn (class1, class2) => + NameSpace.base class2 ^ "_" ^ NameSpace.base class1) (fn thy => thyname_of_class thy o fst); + (*order fits nicely with composed projections*) +fun namify_tyco thy = namify thy NameSpace.base thyname_of_tyco; +fun namify_instance thy = namify thy (fn (class, tyco) => + NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance; +fun namify_const thy = namify thy NameSpace.base thyname_of_const; + +end; (* local *) + + +(* naming data with lookup and declare *) + +structure StringPairTab = Code_Name.StringPairTab; + +datatype naming = Naming of { + class: class Symtab.table * Name.context, + classrel: string StringPairTab.table * Name.context, + tyco: string Symtab.table * Name.context, + instance: string StringPairTab.table * Name.context, + const: string Symtab.table * Name.context +} + +fun dest_Naming (Naming naming) = naming; + +val empty_naming = Naming { + class = (Symtab.empty, Name.context), + classrel = (StringPairTab.empty, Name.context), + tyco = (Symtab.empty, Name.context), + instance = (StringPairTab.empty, Name.context), + const = (Symtab.empty, Name.context) +}; + +local + fun mk_naming (class, classrel, tyco, instance, const) = + Naming { class = class, classrel = classrel, + tyco = tyco, instance = instance, const = const }; + fun map_naming f (Naming { class, classrel, tyco, instance, const }) = + mk_naming (f (class, classrel, tyco, instance, const)); +in + fun map_class f = map_naming + (fn (class, classrel, tyco, inst, const) => + (f class, classrel, tyco, inst, const)); + fun map_classrel f = map_naming + (fn (class, classrel, tyco, inst, const) => + (class, f classrel, tyco, inst, const)); + fun map_tyco f = map_naming + (fn (class, classrel, tyco, inst, const) => + (class, classrel, f tyco, inst, const)); + fun map_instance f = map_naming + (fn (class, classrel, tyco, inst, const) => + (class, classrel, tyco, f inst, const)); + fun map_const f = map_naming + (fn (class, classrel, tyco, inst, const) => + (class, classrel, tyco, inst, f const)); +end; (*local*) + +fun add_variant update (thing, name) (tab, used) = + let + val (name', used') = yield_singleton Name.variants name used; + val tab' = update (thing, name') tab; + in (tab', used') end; + +fun declare thy mapp lookup update namify thing = + mapp (add_variant update (thing, namify thy thing)) + #> `(fn naming => the (lookup naming thing)); + +val lookup_class = add_suffix suffix_class + oo Symtab.lookup o fst o #class o dest_Naming; +val lookup_classrel = add_suffix suffix_classrel + oo StringPairTab.lookup o fst o #classrel o dest_Naming; +val lookup_tyco = add_suffix suffix_tyco + oo Symtab.lookup o fst o #tyco o dest_Naming; +val lookup_instance = add_suffix suffix_instance + oo StringPairTab.lookup o fst o #instance o dest_Naming; +val lookup_const = add_suffix suffix_const + oo Symtab.lookup o fst o #const o dest_Naming; + +fun declare_class thy = declare thy map_class + lookup_class Symtab.update_new namify_class; +fun declare_classrel thy = declare thy map_classrel + lookup_classrel StringPairTab.update_new namify_classrel; +fun declare_tyco thy = declare thy map_tyco + lookup_tyco Symtab.update_new namify_tyco; +fun declare_instance thy = declare thy map_instance + lookup_instance StringPairTab.update_new namify_instance; +fun declare_const thy = declare thy map_const + lookup_const Symtab.update_new namify_const; + (** statements, abstract programs **) type typscheme = (vname * sort) list * itype; datatype stmt = NoStmt - | Fun of typscheme * ((iterm list * iterm) * (thm * bool)) list - | Datatype of (vname * sort) list * (string * itype list) list - | Datatypecons of string - | Class of vname * ((class * string) list * (string * itype) list) + | Fun of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list) + | Datatype of string * ((vname * sort) list * (string * itype list) list) + | Datatypecons of string * string + | Class of class * (vname * ((class * string) list * (string * itype) list)) | Classrel of class * class - | Classparam of class + | Classparam of string * class | Classinst of (class * (string * (vname * sort) list)) * ((class * (string * (string * dict list list))) list * ((string * const) * (thm * bool)) list); @@ -271,7 +405,7 @@ type program = stmt Graph.T; fun empty_funs program = - Graph.fold (fn (name, (Fun (_, []), _)) => cons name + Graph.fold (fn (name, (Fun (c, (_, [])), _)) => cons c | _ => I) program []; fun map_terms_bottom_up f (t as IConst _) = f t @@ -285,8 +419,8 @@ (map_terms_bottom_up f) ps), map_terms_bottom_up f t0)); fun map_terms_stmt f NoStmt = NoStmt - | map_terms_stmt f (Fun (tysm, eqs)) = Fun (tysm, (map o apfst) - (fn (ts, t) => (map f ts, f t)) eqs) + | map_terms_stmt f (Fun (c, (tysm, eqs))) = Fun (c, (tysm, (map o apfst) + (fn (ts, t) => (map f ts, f t)) eqs)) | map_terms_stmt f (stmt as Datatype _) = stmt | map_terms_stmt f (stmt as Datatypecons _) = stmt | map_terms_stmt f (stmt as Class _) = stmt @@ -296,19 +430,13 @@ Classinst (arity, (superarities, (map o apfst o apsnd) (fn const => case f (IConst const) of IConst const' => const') classparms)); -fun transitivly_non_empty_funs program names_ignored = - let - val names_empty = empty_funs program; - val names_delete = Graph.all_preds program (subtract (op =) names_ignored names_empty) - in subtract (op =) names_delete (Graph.keys program) end; - fun is_cons program name = case Graph.get_node program name of Datatypecons _ => true | _ => false; fun contr_classparam_typs program name = case Graph.get_node program name - of Classparam class => let - val Class (_, (_, params)) = Graph.get_node program class; + of Classparam (_, class) => let + val Class (_, (_, (_, params))) = Graph.get_node program class; val SOME ty = AList.lookup (op =) params name; val (tys, res_ty) = unfold_fun ty; fun no_tyvar (_ `%% tys) = forall no_tyvar tys @@ -322,22 +450,29 @@ (** translation kernel **) -fun ensure_stmt stmtgen name (dep, program) = +fun ensure_stmt lookup declare generate thing (dep, (naming, program)) = let - val add_dep = case dep of NONE => I | SOME dep => Graph.add_edge (dep, name); - fun add_stmt false = - Graph.default_node (name, NoStmt) - #> add_dep - #> curry stmtgen (SOME name) - ##> snd - #-> (fn stmt => Graph.map_node name (K stmt)) - | add_stmt true = - add_dep; - in - program - |> add_stmt (can (Graph.get_node program) name) - |> pair dep - |> pair name + fun add_dep name = case dep + of NONE => I | SOME dep => Graph.add_edge (dep, name); + in case lookup naming thing + of SOME name => program + |> add_dep name + |> pair naming + |> pair dep + |> pair name + | NONE => let + val (name, naming') = declare thing naming; + in + program + |> Graph.default_node (name, NoStmt) + |> add_dep name + |> pair naming' + |> curry generate (SOME name) + ||> snd + |-> (fn stmt => (apsnd o Graph.map_node name) (K stmt)) + |> pair dep + |> pair name + end end; fun not_wellsorted thy thm ty sort e = @@ -353,22 +488,20 @@ let val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class; val cs = #params (AxClass.get_info thy class); - val class' = Code_Name.class thy class; val stmt_class = fold_map (fn superclass => ensure_class thy algbr funcgr superclass ##>> ensure_classrel thy algbr funcgr (class, superclass)) superclasses ##>> fold_map (fn (c, ty) => ensure_const thy algbr funcgr c ##>> exprgen_typ thy algbr funcgr ty) cs - #>> (fn info => Class (unprefix "'" Name.aT, info)) - in ensure_stmt stmt_class class' end + #>> (fn info => Class (class, (unprefix "'" Name.aT, info))) + in ensure_stmt lookup_class (declare_class thy) stmt_class class end and ensure_classrel thy algbr funcgr (subclass, superclass) = let - val classrel' = Code_Name.classrel thy (subclass, superclass); val stmt_classrel = ensure_class thy algbr funcgr subclass ##>> ensure_class thy algbr funcgr superclass #>> Classrel; - in ensure_stmt stmt_classrel classrel' end + in ensure_stmt lookup_classrel (declare_classrel thy) stmt_classrel (subclass, superclass) end and ensure_tyco thy algbr funcgr "fun" = pair "fun" | ensure_tyco thy algbr funcgr tyco = @@ -381,10 +514,9 @@ ##>> fold_map (fn (c, tys) => ensure_const thy algbr funcgr c ##>> fold_map (exprgen_typ thy algbr funcgr) tys) cos - #>> Datatype + #>> (fn info => Datatype (tyco, info)) end; - val tyco' = Code_Name.tyco thy tyco; - in ensure_stmt stmt_datatype tyco' end + in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end and exprgen_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) = fold_map (ensure_class thy algbr funcgr) (proj_sort sort) #>> (fn sort => (unprefix "'" v, sort)) @@ -467,38 +599,33 @@ ##>> fold_map exprgen_classparam_inst classparams #>> (fn ((((class, tyco), arity), superarities), classparams) => Classinst ((class, (tyco, arity)), (superarities, classparams))); - val inst = Code_Name.instance thy (class, tyco); - in ensure_stmt stmt_inst inst end + in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end and ensure_const thy algbr funcgr c = let - val c' = Code_Name.const thy c; fun stmt_datatypecons tyco = ensure_tyco thy algbr funcgr tyco - #>> Datatypecons; + #>> (fn tyco => Datatypecons (c, tyco)); fun stmt_classparam class = ensure_class thy algbr funcgr class - #>> Classparam; - fun stmt_fun trns = + #>> (fn class => Classparam (c, class)); + fun stmt_fun ((vs, raw_ty), raw_thms) = let - val raw_thms = Code_Funcgr.eqns funcgr c; - val (vs, raw_ty) = Code_Funcgr.typ funcgr c; val ty = Logic.unvarifyT raw_ty; val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty then raw_thms else (map o apfst) (Code_Unit.expand_eta thy 1) raw_thms; in - trns - |> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs - ||>> exprgen_typ thy algbr funcgr ty - ||>> fold_map (exprgen_eq thy algbr funcgr) thms - |>> (fn ((vs, ty), eqs) => Fun ((vs, ty), eqs)) + fold_map (exprgen_tyvar_sort thy algbr funcgr) vs + ##>> exprgen_typ thy algbr funcgr ty + ##>> fold_map (exprgen_eq thy algbr funcgr) thms + #>> (fn info => Fun (c, info)) end; - val stmtgen = case Code.get_datatype_of_constr thy c + val stmt_const = case Code.get_datatype_of_constr thy c of SOME tyco => stmt_datatypecons tyco | NONE => (case AxClass.class_of_param thy c of SOME class => stmt_classparam class - | NONE => stmt_fun) - in ensure_stmt stmtgen c' end + | NONE => stmt_fun (Code_Funcgr.typ funcgr c, Code_Funcgr.eqns funcgr c)) + in ensure_stmt lookup_const (declare_const thy) stmt_const c end and exprgen_term thy algbr funcgr thm (Const (c, ty)) = exprgen_app thy algbr funcgr thm ((c, ty), []) | exprgen_term thy algbr funcgr thm (Free (v, _)) = @@ -591,9 +718,9 @@ structure Program = CodeDataFun ( - type T = program; - val empty = Graph.empty; - fun purge thy cs program = + type T = naming * program; + val empty = (empty_naming, Graph.empty); + fun purge thy cs (naming, program) = empty (*FIXME: problem: un-declaration of names let val cs_exisiting = map_filter (Code_Name.const_rev thy) (Graph.keys program); @@ -601,28 +728,25 @@ o map (Code_Name.const thy) o filter (member (op =) cs_exisiting) ) cs; - in Graph.del_nodes dels program end; + in Graph.del_nodes dels program end;*) ); val cached_program = Program.get; -fun transact f program = - (NONE, program) - |> f - |-> (fn x => fn (_, program) => (x, program)); - -fun generate thy funcgr f x = - Program.change_yield thy (transact (f thy (Code.operational_algebra thy) funcgr x)); +fun generate thy funcgr f name = + Program.change_yield thy (fn naming_program => (NONE, naming_program) + |> f thy (Code.operational_algebra thy) funcgr name + |-> (fn name => fn (_, naming_program) => (name, naming_program))); (* program generation *) fun consts_program thy cs = let - fun project_consts cs program = + fun project_consts cs (naming, program) = let val cs_all = Graph.all_succs program cs; - in (cs, Graph.subgraph (member (op =) cs_all) program) end; + in (cs, (naming, Graph.subgraph (member (op =) cs_all) program)) end; fun generate_consts thy algebra funcgr = fold_map (ensure_const thy algebra funcgr); in @@ -642,18 +766,19 @@ fold_map (exprgen_tyvar_sort thy algbr funcgr) vs ##>> exprgen_typ thy algbr funcgr ty ##>> exprgen_term thy algbr funcgr NONE t - #>> (fn ((vs, ty), t) => Fun ((vs, ty), [(([], t), (Drule.dummy_thm, true))])); - fun term_value (dep, program1) = + #>> (fn ((vs, ty), t) => Fun + (Term.dummy_patternN, ((vs, ty), [(([], t), (Drule.dummy_thm, true))]))); + fun term_value (dep, (naming, program1)) = let - val Fun ((vs, ty), [(([], t), _)]) = - Graph.get_node program1 Code_Name.value_name; - val deps = Graph.imm_succs program1 Code_Name.value_name; - val program2 = Graph.del_nodes [Code_Name.value_name] program1; + val Fun (_, ((vs, ty), [(([], t), _)])) = + Graph.get_node program1 Term.dummy_patternN; + val deps = Graph.imm_succs program1 Term.dummy_patternN; + val program2 = Graph.del_nodes [Term.dummy_patternN] program1; val deps_all = Graph.all_succs program2 deps; val program3 = Graph.subgraph (member (op =) deps_all) program2; - in ((program3, (((vs, ty), t), deps)), (dep, program2)) end; + in (((naming, program3), (((vs, ty), t), deps)), (dep, (naming, program2))) end; in - ensure_stmt stmt_value Code_Name.value_name + ensure_stmt ((K o K) NONE) pair stmt_value Term.dummy_patternN #> snd #> term_value end; @@ -662,8 +787,8 @@ let fun evaluator'' evaluator''' funcgr t = let - val ((program, (vs_ty_t, deps)), _) = generate thy funcgr ensure_value t; - in evaluator''' program vs_ty_t deps end; + val (((naming, program), (vs_ty_t, deps)), _) = generate thy funcgr ensure_value t; + in evaluator''' naming program vs_ty_t deps end; fun evaluator' t = let val (t', evaluator''') = evaluator t; diff -r 64ab5bb68d4c -r bd8438543bf2 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Wed Oct 22 14:15:44 2008 +0200 +++ b/src/Tools/nbe.ML Wed Oct 22 14:15:45 2008 +0200 @@ -288,15 +288,15 @@ (* preparing function equations *) -fun eqns_of_stmt (_, Code_Thingol.Fun (_, [])) = +fun eqns_of_stmt (_, Code_Thingol.Fun (_, (_, []))) = [] - | eqns_of_stmt (const, Code_Thingol.Fun ((vs, _), eqns)) = + | eqns_of_stmt (const, Code_Thingol.Fun (_, ((vs, _), eqns))) = [(const, (vs, map fst eqns))] | eqns_of_stmt (_, Code_Thingol.Datatypecons _) = [] | eqns_of_stmt (_, Code_Thingol.Datatype _) = [] - | eqns_of_stmt (class, Code_Thingol.Class (v, (superclasses, classops))) = + | eqns_of_stmt (class, Code_Thingol.Class (_, (v, (superclasses, classops)))) = let val names = map snd superclasses @ map fst classops; val params = Name.invent_list [] "d" (length names); @@ -364,27 +364,28 @@ (* reification *) -fun term_of_univ thy idx_tab t = +fun term_of_univ thy program idx_tab t = let fun take_until f [] = [] | take_until f (x::xs) = if f x then [] else x :: take_until f xs; - fun is_dict (Const (idx, _)) = - let - val c = the (Inttab.lookup idx_tab idx); - in - (is_some o Code_Name.class_rev thy) c - orelse (is_some o Code_Name.classrel_rev thy) c - orelse (is_some o Code_Name.instance_rev thy) c - end + fun is_dict (Const (idx, _)) = (case (Graph.get_node program o the o Inttab.lookup idx_tab) idx + of Code_Thingol.Class _ => true + | Code_Thingol.Classrel _ => true + | Code_Thingol.Classinst _ => true + | _ => false) | is_dict (DFree _) = true | is_dict _ = false; + fun const_of_idx idx = (case (Graph.get_node program o the o Inttab.lookup idx_tab) idx + of Code_Thingol.Fun (c, _) => c + | Code_Thingol.Datatypecons (c, _) => c + | Code_Thingol.Classparam (c, _) => c); fun of_apps bounds (t, ts) = fold_map (of_univ bounds) ts #>> (fn ts' => list_comb (t, rev ts')) and of_univ bounds (Const (idx, ts)) typidx = let val ts' = take_until is_dict ts; - val c = (the o Code_Name.const_rev thy o the o Inttab.lookup idx_tab) idx; + val c = const_of_idx idx; val (_, T) = Code.default_typscheme thy c; val T' = map_type_tvar (fn ((v, i), S) => TypeInfer.param (typidx + i) (v, [])) T; val typidx' = typidx + maxidx_of_typ T' + 1; @@ -405,7 +406,7 @@ ( type T = (Univ option * int) Graph.T * (int * string Inttab.table); val empty = (Graph.empty, (0, Inttab.empty)); - fun purge thy cs (gr, (maxidx, idx_tab)) = + fun purge thy cs (gr, (maxidx, idx_tab)) = empty (*FIXME let val cs_exisiting = map_filter (Code_Name.const_rev thy) (Graph.keys gr); @@ -413,7 +414,7 @@ o map (Code_Name.const thy) o filter (member (op =) cs_exisiting) ) cs; - in (Graph.del_nodes dels gr, (maxidx, idx_tab)) end; + in (Graph.del_nodes dels gr, (maxidx, idx_tab)) end*); ); (* compilation, evaluation and reification *) @@ -425,7 +426,7 @@ in vs_ty_t |> eval_term ctxt gr deps - |> term_of_univ thy idx_tab + |> term_of_univ thy program idx_tab end; (* evaluation with type reconstruction *) @@ -478,13 +479,13 @@ fun norm_conv ct = let val thy = Thm.theory_of_cterm ct; - fun evaluator' t program vs_ty_t deps = norm_oracle (thy, t, program, vs_ty_t, deps); + fun evaluator' t naming program vs_ty_t deps = norm_oracle (thy, t, program, vs_ty_t, deps); fun evaluator t = (add_triv_classes thy t, evaluator' t); in Code_Thingol.eval_conv thy evaluator ct end; fun norm_term thy t = let - fun evaluator' t program vs_ty_t deps = eval thy t program vs_ty_t deps; + fun evaluator' t naming program vs_ty_t deps = eval thy t program vs_ty_t deps; fun evaluator t = (add_triv_classes thy t, evaluator' t); in (Code.postprocess_term thy o Code_Thingol.eval_term thy evaluator) t end;