# HG changeset patch # User haftmann # Date 1390690249 -3600 # Node ID bce3dbc11f9508316a6c20848364485d4337b9d1 # Parent 525309c2e4ee8c5fb2f6edd8d4e831f640204c90 prefer explicit code symbol type over ad-hoc name mangling diff -r 525309c2e4ee -r bce3dbc11f95 src/Doc/Codegen/Adaptation.thy --- a/src/Doc/Codegen/Adaptation.thy Sat Jan 25 23:50:49 2014 +0100 +++ b/src/Doc/Codegen/Adaptation.thy Sat Jan 25 23:50:49 2014 +0100 @@ -2,8 +2,8 @@ imports Setup begin -setup %invisible {* Code_Target.extend_target ("\", ("SML", K I)) - #> Code_Target.extend_target ("\", ("Haskell", K I)) *} +setup %invisible {* Code_Target.extend_target ("\", ("SML", I)) + #> Code_Target.extend_target ("\", ("Haskell", I)) *} section {* Adaptation to target languages \label{sec:adaptation} *} diff -r 525309c2e4ee -r bce3dbc11f95 src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Sat Jan 25 23:50:49 2014 +0100 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Sat Jan 25 23:50:49 2014 +0100 @@ -671,25 +671,17 @@ open Code_Thingol; -fun imp_program naming = +val imp_program = let - fun is_const c = case lookup_const naming c - of SOME c' => (fn c'' => c' = c'') - | NONE => K false; - val is_bind = is_const @{const_name bind}; - val is_return = is_const @{const_name return}; + val is_bind = curry (op =) @{const_name bind}; + val is_return = curry (op =) @{const_name return}; val dummy_name = ""; val dummy_case_term = IVar NONE; (*assumption: dummy values are not relevant for serialization*) - val (unitt, unitT) = case lookup_const naming @{const_name Unity} - of SOME unit' => - let - val unitT = the (lookup_tyco naming @{type_name unit}) `%% [] - in - (IConst { name = unit', typargs = [], dicts = [], dom = [], - range = unitT, annotate = false }, unitT) - end - | NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants."); + val unitT = @{type_name unit} `%% []; + val unitt = + IConst { sym = Code_Symbol.Constant @{const_name Unity}, typargs = [], dicts = [], dom = [], + range = unitT, annotate = false }; fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t) | dest_abs (t, ty) = let @@ -697,7 +689,7 @@ val v = singleton (Name.variant_list vs) "x"; val ty' = (hd o fst o unfold_fun) ty; in ((SOME v, ty'), t `$ IVar (SOME v)) end; - fun force (t as IConst { name = c, ... } `$ t') = if is_return c + fun force (t as IConst { sym = Code_Symbol.Constant c, ... } `$ t') = if is_return c then t' else t `$ unitt | force t = t `$ unitt; fun tr_bind'' [(t1, _), (t2, ty2)] = @@ -705,13 +697,13 @@ val ((v, ty), t) = dest_abs (t2, ty2); in ICase { term = force t1, typ = ty, clauses = [(IVar v, tr_bind' t)], primitive = dummy_case_term } end and tr_bind' t = case unfold_app t - of (IConst { name = c, dom = ty1 :: ty2 :: _, ... }, [x1, x2]) => if is_bind c + of (IConst { sym = Code_Symbol.Constant c, dom = ty1 :: ty2 :: _, ... }, [x1, x2]) => if is_bind c then tr_bind'' [(x1, ty1), (x2, ty2)] else force t | _ => force t; fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=> ICase { term = IVar (SOME dummy_name), typ = unitT, clauses = [(unitt, tr_bind'' ts)], primitive = dummy_case_term } - fun imp_monad_bind' (const as { name = c, dom = dom, ... }) ts = if is_bind c then case (ts, dom) + fun imp_monad_bind' (const as { sym = Code_Symbol.Constant c, dom = dom, ... }) ts = if is_bind c then case (ts, dom) 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)) @@ -726,7 +718,7 @@ ICase { term = imp_monad_bind t, typ = ty, clauses = (map o pairself) imp_monad_bind clauses, primitive = imp_monad_bind t0 }; - in (Graph.map o K o map_terms_stmt) imp_monad_bind end; + in (Code_Symbol.Graph.map o K o map_terms_stmt) imp_monad_bind end; in diff -r 525309c2e4ee -r bce3dbc11f95 src/HOL/List.thy --- a/src/HOL/List.thy Sat Jan 25 23:50:49 2014 +0100 +++ b/src/HOL/List.thy Sat Jan 25 23:50:49 2014 +0100 @@ -6318,14 +6318,14 @@ fun implode_list nil' cons' t = let - fun dest_cons (IConst { name = c, ... } `$ t1 `$ t2) = + fun dest_cons (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) = if c = cons' then SOME (t1, t2) else NONE | dest_cons _ = NONE; val (ts, t') = Code_Thingol.unfoldr dest_cons t; in case t' - of IConst { name = c, ... } => if c = nil' then SOME ts else NONE + of IConst { sym = Code_Symbol.Constant c, ... } => if c = nil' then SOME ts else NONE | _ => NONE end; diff -r 525309c2e4ee -r bce3dbc11f95 src/HOL/Quickcheck_Narrowing.thy --- a/src/HOL/Quickcheck_Narrowing.thy Sat Jan 25 23:50:49 2014 +0100 +++ b/src/HOL/Quickcheck_Narrowing.thy Sat Jan 25 23:50:49 2014 +0100 @@ -11,7 +11,7 @@ subsubsection {* Code generation setup *} -setup {* Code_Target.extend_target ("Haskell_Quickcheck", (Code_Haskell.target, K I)) *} +setup {* Code_Target.extend_target ("Haskell_Quickcheck", (Code_Haskell.target, I)) *} code_printing type_constructor typerep \ (Haskell_Quickcheck) "Typerep" diff -r 525309c2e4ee -r bce3dbc11f95 src/HOL/Quickcheck_Random.thy --- a/src/HOL/Quickcheck_Random.thy Sat Jan 25 23:50:49 2014 +0100 +++ b/src/HOL/Quickcheck_Random.thy Sat Jan 25 23:50:49 2014 +0100 @@ -9,7 +9,7 @@ notation fcomp (infixl "\>" 60) notation scomp (infixl "\\" 60) -setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, K I)) *} +setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, I)) *} subsection {* Catching Match exceptions *} diff -r 525309c2e4ee -r bce3dbc11f95 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sat Jan 25 23:50:49 2014 +0100 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sat Jan 25 23:50:49 2014 +0100 @@ -309,9 +309,9 @@ fun dynamic_value_strict opts cookie thy postproc t = let val ctxt = Proof_Context.init_global thy - fun evaluator naming program ((_, vs_ty), t) deps = + fun evaluator program ((_, vs_ty), t) deps = Exn.interruptible_capture (value opts ctxt cookie) - (Code_Target.evaluator thy target naming program deps (vs_ty, t)); + (Code_Target.evaluator thy target program deps (vs_ty, t)); in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end; (** counterexample generator **) diff -r 525309c2e4ee -r bce3dbc11f95 src/HOL/Tools/numeral.ML --- a/src/HOL/Tools/numeral.ML Sat Jan 25 23:50:49 2014 +0100 +++ b/src/HOL/Tools/numeral.ML Sat Jan 25 23:50:49 2014 +0100 @@ -69,11 +69,11 @@ let fun dest_numeral one' bit0' bit1' thm t = let - fun dest_bit (IConst { name = c, ... }) = if c = bit0' then 0 + fun dest_bit (IConst { sym = Code_Symbol.Constant c, ... }) = if c = bit0' then 0 else if c = bit1' then 1 else Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit" | dest_bit _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit"; - fun dest_num (IConst { name = c, ... }) = if c = one' then 1 + fun dest_num (IConst { sym = Code_Symbol.Constant c, ... }) = if c = one' then 1 else Code_Printer.eqn_error thm "Illegal numeral expression: illegal leading digit" | dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_bit t1 | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term"; diff -r 525309c2e4ee -r bce3dbc11f95 src/HOL/Tools/string_code.ML --- a/src/HOL/Tools/string_code.ML Sat Jan 25 23:50:49 2014 +0100 +++ b/src/HOL/Tools/string_code.ML Sat Jan 25 23:50:49 2014 +0100 @@ -23,13 +23,13 @@ | decode _ ~1 = NONE | decode n m = SOME (chr (n * 16 + m)); in case tt - of (IConst { name = c1, ... }, IConst { name = c2, ... }) => decode (idx c1) (idx c2) + of (IConst { sym = Code_Symbol.Constant c1, ... }, IConst { sym = Code_Symbol.Constant c2, ... }) => decode (idx c1) (idx c2) | _ => NONE end; fun implode_string literals char' nibbles' ts = let - fun implode_char (IConst { name = c, ... } `$ t1 `$ t2) = + fun implode_char (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) = if c = char' then decode_char nibbles' (t1, t2) else NONE | implode_char _ = NONE; val ts' = map_filter implode_char ts; diff -r 525309c2e4ee -r bce3dbc11f95 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Sat Jan 25 23:50:49 2014 +0100 +++ b/src/Tools/Code/code_haskell.ML Sat Jan 25 23:50:49 2014 +0100 @@ -37,8 +37,11 @@ fun print_haskell_stmt class_syntax tyco_syntax const_syntax reserved deresolve deriving_show = let + val deresolve_const = deresolve o Code_Symbol.Constant; + val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor; + val deresolve_class = deresolve o Code_Symbol.Type_Class; fun class_name class = case class_syntax class - of NONE => deresolve class + of NONE => deresolve_class class | SOME class => class; fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs of [] => [] @@ -53,7 +56,7 @@ fun print_tyco_expr tyvars fxy (tyco, tys) = brackify fxy (str tyco :: map (print_typ tyvars BR) tys) and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco - of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys) + of NONE => print_tyco_expr tyvars fxy (deresolve_tyco tyco, tys) | SOME (_, print) => print (print_typ tyvars) fxy tys) | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v; fun print_typdecl tyvars (tyco, vs) = @@ -81,18 +84,19 @@ in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end | print_term tyvars some_thm vars fxy (ICase case_expr) = (case Code_Thingol.unfold_const_app (#primitive case_expr) - of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c) + of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) => + if is_none (const_syntax const) then print_case tyvars some_thm vars fxy case_expr else print_app tyvars some_thm vars fxy app | NONE => print_case tyvars some_thm vars fxy case_expr) - and print_app_expr tyvars some_thm vars ({ name = c, dom, range, annotate, ... }, ts) = + and print_app_expr tyvars some_thm vars ({ sym, dom, range, annotate, ... }, ts) = let - val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (dom, range) + val ty = Library.foldr (op `->) (dom, range) val printed_const = if annotate then - brackets [(str o deresolve) c, str "::", print_typ tyvars NOBR ty] + brackets [(str o deresolve) sym, str "::", print_typ tyvars NOBR ty] else - (str o deresolve) c + (str o deresolve) sym in printed_const :: map (print_term tyvars some_thm vars BR) ts end @@ -122,17 +126,16 @@ (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})") (map print_select clauses) end; - fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) = + fun print_stmt (Code_Symbol.Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) = let val tyvars = intro_vars (map fst vs) reserved; fun print_err n = - semicolon ( - (str o deresolve) name - :: map str (replicate n "_") - @ str "=" - :: str "error" - @@ (str o ML_Syntax.print_string - o Long_Name.base_name o Long_Name.qualifier) name + (semicolon o map str) ( + deresolve_const const + :: replicate n "_" + @ "=" + :: "error" + @@ ML_Syntax.print_string const ); fun print_eqn ((ts, t), (some_thm, _)) = let @@ -143,7 +146,7 @@ (insert (op =)) ts []); in semicolon ( - (str o deresolve) name + (str o deresolve_const) const :: map (print_term tyvars some_thm vars BR) ts @ str "=" @@ print_term tyvars some_thm vars NOBR t @@ -152,7 +155,7 @@ in Pretty.chunks ( semicolon [ - (str o suffix " ::" o deresolve) name, + (str o suffix " ::" o deresolve_const) const, print_typscheme tyvars (vs, ty) ] :: (case filter (snd o snd) raw_eqs @@ -160,52 +163,52 @@ | eqs => map print_eqn eqs) ) end - | print_stmt (name, Code_Thingol.Datatype (_, (vs, []))) = + | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, [])) = let val tyvars = intro_vars vs reserved; in semicolon [ str "data", - print_typdecl tyvars (deresolve name, vs) + print_typdecl tyvars (deresolve_tyco tyco, vs) ] end - | print_stmt (name, Code_Thingol.Datatype (_, (vs, [((co, _), [ty])]))) = + | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, [((co, _), [ty])])) = let val tyvars = intro_vars vs reserved; in semicolon ( str "newtype" - :: print_typdecl tyvars (deresolve name, vs) + :: print_typdecl tyvars (deresolve_tyco tyco, vs) :: str "=" - :: (str o deresolve) co + :: (str o deresolve_const) co :: print_typ tyvars BR ty - :: (if deriving_show name then [str "deriving (Read, Show)"] else []) + :: (if deriving_show tyco then [str "deriving (Read, Show)"] else []) ) end - | print_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) = + | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, co :: cos)) = let val tyvars = intro_vars vs reserved; fun print_co ((co, _), tys) = concat ( - (str o deresolve) co + (str o deresolve_const) co :: map (print_typ tyvars BR) tys ) in semicolon ( str "data" - :: print_typdecl tyvars (deresolve name, vs) + :: print_typdecl tyvars (deresolve_tyco tyco, vs) :: str "=" :: print_co co :: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos - @ (if deriving_show name then [str "deriving (Read, Show)"] else []) + @ (if deriving_show tyco then [str "deriving (Read, Show)"] else []) ) end - | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) = + | print_stmt (Code_Symbol.Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) = let val tyvars = intro_vars [v] reserved; fun print_classparam (classparam, ty) = semicolon [ - (str o deresolve) classparam, + (str o deresolve_const) classparam, str "::", print_typ tyvars NOBR ty ] @@ -213,8 +216,8 @@ Pretty.block_enclose ( Pretty.block [ str "class ", - Pretty.block (print_typcontext tyvars [(v, map fst super_classes)]), - str (deresolve name ^ " " ^ lookup_var tyvars v), + Pretty.block (print_typcontext tyvars [(v, map snd classrels)]), + str (deresolve_class class ^ " " ^ lookup_var tyvars v), str " where {" ], str "};" @@ -230,20 +233,20 @@ fun print_classparam_instance ((classparam, (const, _)), (thm, _)) = case requires_args classparam of NONE => semicolon [ - (str o Long_Name.base_name o deresolve) classparam, + (str o Long_Name.base_name o deresolve_const) classparam, str "=", print_app tyvars (SOME thm) reserved NOBR (const, []) ] | SOME k => let - val { name = c, dom, range, ... } = const; + val { sym = Code_Symbol.Constant c, dom, range, ... } = const; val (vs, rhs) = (apfst o map) fst (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, []))); val s = if (is_some o const_syntax) c - then NONE else (SOME o Long_Name.base_name o deresolve) c; + then NONE else (SOME o Long_Name.base_name o deresolve_const) c; val vars = reserved |> intro_vars (map_filter I (s :: vs)); - val lhs = IConst { name = classparam, typargs = [], + val lhs = IConst { sym = Code_Symbol.Constant classparam, typargs = [], dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs; (*dictionaries are not relevant at this late stage, and these consts never need type annotations for disambiguation *) @@ -268,7 +271,7 @@ end; in print_stmt end; -fun haskell_program_of_program ctxt symbol_of module_prefix module_name reserved identifiers = +fun haskell_program_of_program ctxt module_prefix module_name reserved identifiers = let fun namify_fun upper base (nsp_fun, nsp_typ) = let @@ -279,7 +282,7 @@ let val (base', nsp_typ') = Name.variant (first_upper base) nsp_typ; in (base', (nsp_fun, nsp_typ')) end; - fun namify_stmt (Code_Thingol.Fun (_, (_, SOME _))) = pair + fun namify_stmt (Code_Thingol.Fun (_, SOME _)) = pair | namify_stmt (Code_Thingol.Fun _) = namify_fun false | namify_stmt (Code_Thingol.Datatype _) = namify_typ | namify_stmt (Code_Thingol.Datatypecons _) = namify_fun true @@ -287,7 +290,7 @@ | namify_stmt (Code_Thingol.Classrel _) = pair | namify_stmt (Code_Thingol.Classparam _) = namify_fun false | namify_stmt (Code_Thingol.Classinst _) = pair; - fun select_stmt (Code_Thingol.Fun (_, (_, SOME _))) = false + fun select_stmt (Code_Thingol.Fun (_, SOME _)) = false | select_stmt (Code_Thingol.Fun _) = true | select_stmt (Code_Thingol.Datatype _) = true | select_stmt (Code_Thingol.Datatypecons _) = false @@ -296,7 +299,7 @@ | select_stmt (Code_Thingol.Classparam _) = false | select_stmt (Code_Thingol.Classinst _) = true; in - Code_Namespace.flat_program ctxt symbol_of + Code_Namespace.flat_program ctxt { module_prefix = module_prefix, module_name = module_name, reserved = reserved, identifiers = identifiers, empty_nsp = (reserved, reserved), namify_stmt = namify_stmt, modify_stmt = fn stmt => if select_stmt stmt then SOME stmt else NONE } @@ -323,25 +326,24 @@ ("Maybe", ["Nothing", "Just"]) ]; -fun serialize_haskell module_prefix string_classes ctxt { symbol_of, module_name, +fun serialize_haskell module_prefix string_classes ctxt { module_name, reserved_syms, identifiers, includes, class_syntax, tyco_syntax, const_syntax } program = let (* build program *) val reserved = fold (insert (op =) o fst) includes reserved_syms; val { deresolver, flat_program = haskell_program } = haskell_program_of_program - ctxt symbol_of module_prefix module_name (Name.make_context reserved) identifiers program; + ctxt module_prefix module_name (Name.make_context reserved) identifiers program; (* print statements *) fun deriving_show tyco = let fun deriv _ "fun" = false - | deriv tycos tyco = not (tyco = Code_Thingol.fun_tyco) - andalso (member (op =) tycos tyco - orelse case try (Graph.get_node program) tyco - of SOME (Code_Thingol.Datatype (_, (_, cs))) => forall (deriv' (tyco :: tycos)) + | deriv tycos tyco = member (op =) tycos tyco + orelse case try (Code_Symbol.Graph.get_node program) (Code_Symbol.Type_Constructor tyco) + of SOME (Code_Thingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos)) (maps snd cs) - | NONE => true) + | NONE => true and deriv' tycos (tyco `%% tys) = deriv tycos tyco andalso forall (deriv' tycos) tys | deriv' _ (ITyVar _) = true @@ -369,10 +371,10 @@ val deresolve = deresolver module_name; fun print_import module_name = (semicolon o map str) ["import qualified", module_name]; val import_ps = import_common_ps @ map (print_qualified_import o fst) imports; - fun print_stmt' name = case Graph.get_node gr name + fun print_stmt' sym = case Code_Symbol.Graph.get_node gr sym of (_, NONE) => NONE - | (_, SOME stmt) => SOME (markup_stmt name (print_stmt deresolve (name, stmt))); - val body_ps = map_filter print_stmt' ((flat o rev o Graph.strong_conn) gr); + | (_, SOME stmt) => SOME (markup_stmt sym (print_stmt deresolve (sym, stmt))); + val body_ps = map_filter print_stmt' ((flat o rev o Code_Symbol.Graph.strong_conn) gr); in print_module_frame module_name ((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps) @@ -430,7 +432,7 @@ of SOME ((pat, ty), t') => SOME ((SOME ((pat, ty), true), t1), t') | NONE => NONE; - fun dest_monad c_bind_name (IConst { name = c, ... } `$ t1 `$ t2) = + fun dest_monad c_bind_name (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) = if c = c_bind_name then dest_bind t1 t2 else NONE | dest_monad _ t = case Code_Thingol.split_let t diff -r 525309c2e4ee -r bce3dbc11f95 src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Sat Jan 25 23:50:49 2014 +0100 +++ b/src/Tools/Code/code_ml.ML Sat Jan 25 23:50:49 2014 +0100 @@ -28,17 +28,17 @@ datatype ml_binding = ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list) - | ML_Instance of string * { class: string, tyco: string, vs: (vname * sort) list, - superinsts: (class * (string * (string * dict list list))) list, + | ML_Instance of (string * class) * { class: class, tyco: string, vs: (vname * sort) list, + superinsts: (class * dict list list) list, inst_params: ((string * (const * int)) * (thm * bool)) list, superinst_params: ((string * (const * int)) * (thm * bool)) list }; datatype ml_stmt = ML_Exc of string * (typscheme * int) | ML_Val of ml_binding - | ML_Funs of ml_binding list * string list + | ML_Funs of ml_binding list * Code_Symbol.symbol list | ML_Datas of (string * (vname list * ((string * vname list) * itype list) list)) list - | ML_Class of string * (vname * ((class * string) list * (string * itype) list)); + | ML_Class of string * (vname * ((class * class) list * (string * itype) list)); fun print_product _ [] = NONE | print_product print [x] = SOME (print x) @@ -53,30 +53,35 @@ fun print_sml_stmt tyco_syntax const_syntax reserved is_constr deresolve = let - fun print_tyco_expr (tyco, []) = (str o deresolve) tyco - | print_tyco_expr (tyco, [ty]) = - concat [print_typ BR ty, (str o deresolve) tyco] - | print_tyco_expr (tyco, tys) = - concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco] + val deresolve_const = deresolve o Code_Symbol.Constant; + val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor; + val deresolve_class = deresolve o Code_Symbol.Type_Class; + val deresolve_classrel = deresolve o Code_Symbol.Class_Relation; + val deresolve_inst = deresolve o Code_Symbol.Class_Instance; + fun print_tyco_expr (sym, []) = (str o deresolve) sym + | print_tyco_expr (sym, [ty]) = + concat [print_typ BR ty, (str o deresolve) sym] + | print_tyco_expr (sym, tys) = + concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym] and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco - of NONE => print_tyco_expr (tyco, tys) + of NONE => print_tyco_expr (Code_Symbol.Type_Constructor tyco, tys) | SOME (_, print) => print print_typ fxy tys) | print_typ fxy (ITyVar v) = str ("'" ^ v); - fun print_dicttyp (class, ty) = print_tyco_expr (class, [ty]); + fun print_dicttyp (class, ty) = print_tyco_expr (Code_Symbol.Type_Class class, [ty]); fun print_typscheme_prefix (vs, p) = enum " ->" "" "" (map_filter (fn (v, sort) => (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p); fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty); fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty); fun print_classrels fxy [] ps = brackify fxy ps - | print_classrels fxy [classrel] ps = brackify fxy [(str o deresolve) classrel, brackify BR ps] + | print_classrels fxy [classrel] ps = brackify fxy [(str o deresolve_classrel) classrel, brackify BR ps] | print_classrels fxy classrels ps = - brackify fxy [enum " o" "(" ")" (map (str o deresolve) classrels), brackify BR ps] + brackify fxy [enum " o" "(" ")" (map (str o deresolve_classrel) classrels), brackify BR ps] fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) = print_classrels fxy classrels (print_plain_dict is_pseudo_fun fxy x) and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) = - ((str o deresolve) inst :: - (if is_pseudo_fun inst then [str "()"] + ((str o deresolve_inst) inst :: + (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"] else map_filter (print_dicts is_pseudo_fun BR) dss)) | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) = [str (if k = 1 then first_upper v ^ "_" @@ -105,21 +110,22 @@ in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) = (case Code_Thingol.unfold_const_app (#primitive case_expr) - of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c) + of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) => + if is_none (const_syntax const) then print_case is_pseudo_fun some_thm vars fxy case_expr else print_app is_pseudo_fun some_thm vars fxy app | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr) - and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) = - if is_constr c then + and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) = + if is_constr sym then let val k = length dom in if k < 2 orelse length ts = k - then (str o deresolve) c + then (str o deresolve) sym :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts) else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)] end - else if is_pseudo_fun c - then (str o deresolve) c @@ str "()" - else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss + else if is_pseudo_fun sym + then (str o deresolve) sym @@ str "()" + else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dss @ map (print_term is_pseudo_fun some_thm vars BR) ts and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun) (print_term is_pseudo_fun) const_syntax some_thm vars @@ -158,23 +164,23 @@ :: map (print_select "|") clauses ) end; - fun print_val_decl print_typscheme (name, typscheme) = concat - [str "val", str (deresolve name), str ":", print_typscheme typscheme]; + fun print_val_decl print_typscheme (sym, typscheme) = concat + [str "val", str (deresolve sym), str ":", print_typscheme typscheme]; fun print_datatype_decl definer (tyco, (vs, cos)) = let - fun print_co ((co, _), []) = str (deresolve co) - | print_co ((co, _), tys) = concat [str (deresolve co), str "of", + fun print_co ((co, _), []) = str (deresolve_const co) + | print_co ((co, _), tys) = concat [str (deresolve_const co), str "of", enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; in concat ( str definer - :: print_tyco_expr (tyco, map ITyVar vs) + :: print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs) :: str "=" :: separate (str "|") (map print_co cos) ) end; fun print_def is_pseudo_fun needs_typ definer - (ML_Function (name, (vs_ty as (vs, ty), eq :: eqs))) = + (ML_Function (const, (vs_ty as (vs, ty), eq :: eqs))) = let fun print_eqn definer ((ts, t), (some_thm, _)) = let @@ -184,12 +190,12 @@ |> intro_vars ((fold o Code_Thingol.fold_varnames) (insert (op =)) ts []); val prolog = if needs_typ then - concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty] - else (concat o map str) [definer, deresolve name]; + concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty] + else (concat o map str) [definer, deresolve_const const]; in concat ( prolog - :: (if is_pseudo_fun name then [str "()"] + :: (if is_pseudo_fun (Code_Symbol.Constant const) then [str "()"] else print_dict_args vs @ map (print_term is_pseudo_fun some_thm vars BR) ts) @ str "=" @@ -199,53 +205,53 @@ val shift = if null eqs then I else map (Pretty.block o single o Pretty.block o single); in pair - (print_val_decl print_typscheme (name, vs_ty)) + (print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty)) ((Pretty.block o Pretty.fbreaks o shift) ( print_eqn definer eq :: map (print_eqn "|") eqs )) end | print_def is_pseudo_fun _ definer - (ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) = + (ML_Instance (inst as (tyco, class), { vs, superinsts, inst_params, ... })) = let - fun print_super_instance (_, (classrel, x)) = + fun print_super_instance (super_class, x) = concat [ - (str o Long_Name.base_name o deresolve) classrel, + (str o Long_Name.base_name o deresolve_classrel) (class, super_class), str "=", - print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x)) + print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), x))) ]; fun print_classparam_instance ((classparam, (const, _)), (thm, _)) = concat [ - (str o Long_Name.base_name o deresolve) classparam, + (str o Long_Name.base_name o deresolve_const) classparam, str "=", print_app (K false) (SOME thm) reserved NOBR (const, []) ]; in pair (print_val_decl print_dicttypscheme - (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs)))) + (Code_Symbol.Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs)))) (concat ( str definer - :: (str o deresolve) inst - :: (if is_pseudo_fun inst then [str "()"] + :: (str o deresolve_inst) inst + :: (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"] else print_dict_args vs) @ str "=" :: enum "," "{" "}" (map print_super_instance superinsts @ map print_classparam_instance inst_params) :: str ":" - @@ print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs]) + @@ print_dicttyp (class, tyco `%% map (ITyVar o fst) vs) )) end; - fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair - [print_val_decl print_typscheme (name, vs_ty)] + fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair + [print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty)] ((semicolon o map str) ( (if n = 0 then "val" else "fun") - :: deresolve name + :: deresolve_const const :: replicate n "_" @ "=" :: "raise" :: "Fail" - @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name + @@ ML_Syntax.print_string const )) | print_stmt (ML_Val binding) = let @@ -257,11 +263,11 @@ | print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) = let val print_def' = print_def (member (op =) pseudo_funs) false; - fun print_pseudo_fun name = concat [ + fun print_pseudo_fun sym = concat [ str "val", - (str o deresolve) name, + (str o deresolve) sym, str "=", - (str o deresolve) name, + (str o deresolve) sym, str "();" ]; val (sig_ps, (ps, p)) = (apsnd split_last o split_list) @@ -273,7 +279,7 @@ end | print_stmt (ML_Datas [(tyco, (vs, []))]) = let - val ty_p = print_tyco_expr (tyco, map ITyVar vs); + val ty_p = print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs); in pair [concat [str "type", ty_p]] @@ -288,42 +294,42 @@ sig_ps (Pretty.chunks (ps @| semicolon [p])) end - | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) = + | print_stmt (ML_Class (class, (v, (classrels, classparams)))) = let fun print_field s p = concat [str s, str ":", p]; fun print_proj s p = semicolon (map str ["val", s, "=", "#" ^ s, ":"] @| p); - fun print_super_class_decl (super_class, classrel) = + fun print_super_class_decl (classrel as (_, super_class)) = print_val_decl print_dicttypscheme - (classrel, ([(v, [class])], (super_class, ITyVar v))); - fun print_super_class_field (super_class, classrel) = - print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v)); - fun print_super_class_proj (super_class, classrel) = - print_proj (deresolve classrel) + (Code_Symbol.Class_Relation classrel, ([(v, [class])], (super_class, ITyVar v))); + fun print_super_class_field (classrel as (_, super_class)) = + print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v)); + fun print_super_class_proj (classrel as (_, super_class)) = + print_proj (deresolve_classrel classrel) (print_dicttypscheme ([(v, [class])], (super_class, ITyVar v))); fun print_classparam_decl (classparam, ty) = print_val_decl print_typscheme - (classparam, ([(v, [class])], ty)); + (Code_Symbol.Constant classparam, ([(v, [class])], ty)); fun print_classparam_field (classparam, ty) = - print_field (deresolve classparam) (print_typ NOBR ty); + print_field (deresolve_const classparam) (print_typ NOBR ty); fun print_classparam_proj (classparam, ty) = - print_proj (deresolve classparam) + print_proj (deresolve_const classparam) (print_typscheme ([(v, [class])], ty)); in pair (concat [str "type", print_dicttyp (class, ITyVar v)] - :: map print_super_class_decl super_classes + :: map print_super_class_decl classrels @ map print_classparam_decl classparams) (Pretty.chunks ( concat [ str ("type '" ^ v), - (str o deresolve) class, + (str o deresolve_class) class, str "=", enum "," "{" "};" ( - map print_super_class_field super_classes + map print_super_class_field classrels @ map print_classparam_field classparams ) ] - :: map print_super_class_proj super_classes + :: map print_super_class_proj classrels @ map print_classparam_proj classparams )) end; @@ -353,29 +359,34 @@ fun print_ocaml_stmt tyco_syntax const_syntax reserved is_constr deresolve = let - fun print_tyco_expr (tyco, []) = (str o deresolve) tyco - | print_tyco_expr (tyco, [ty]) = - concat [print_typ BR ty, (str o deresolve) tyco] - | print_tyco_expr (tyco, tys) = - concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco] + val deresolve_const = deresolve o Code_Symbol.Constant; + val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor; + val deresolve_class = deresolve o Code_Symbol.Type_Class; + val deresolve_classrel = deresolve o Code_Symbol.Class_Relation; + val deresolve_inst = deresolve o Code_Symbol.Class_Instance; + fun print_tyco_expr (sym, []) = (str o deresolve) sym + | print_tyco_expr (sym, [ty]) = + concat [print_typ BR ty, (str o deresolve) sym] + | print_tyco_expr (sym, tys) = + concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym] and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco - of NONE => print_tyco_expr (tyco, tys) + of NONE => print_tyco_expr (Code_Symbol.Type_Constructor tyco, tys) | SOME (_, print) => print print_typ fxy tys) | print_typ fxy (ITyVar v) = str ("'" ^ v); - fun print_dicttyp (class, ty) = print_tyco_expr (class, [ty]); + fun print_dicttyp (class, ty) = print_tyco_expr (Code_Symbol.Type_Class class, [ty]); fun print_typscheme_prefix (vs, p) = enum " ->" "" "" (map_filter (fn (v, sort) => (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p); fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty); fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty); val print_classrels = - fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve) classrel]) + fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve_classrel) classrel]) fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) = print_plain_dict is_pseudo_fun fxy x |> print_classrels classrels and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) = - brackify BR ((str o deresolve) inst :: - (if is_pseudo_fun inst then [str "()"] + brackify BR ((str o deresolve_inst) inst :: + (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"] else map_filter (print_dicts is_pseudo_fun BR) dss)) | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) = str (if k = 1 then "_" ^ first_upper v @@ -401,21 +412,22 @@ in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) = (case Code_Thingol.unfold_const_app (#primitive case_expr) - of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c) + of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) => + if is_none (const_syntax const) then print_case is_pseudo_fun some_thm vars fxy case_expr else print_app is_pseudo_fun some_thm vars fxy app | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr) - and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) = - if is_constr c then + and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) = + if is_constr sym then let val k = length dom in if length ts = k - then (str o deresolve) c + then (str o deresolve) sym :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts) else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)] end - else if is_pseudo_fun c - then (str o deresolve) c @@ str "()" - else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss + else if is_pseudo_fun sym + then (str o deresolve) sym @@ str "()" + else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dss @ map (print_term is_pseudo_fun some_thm vars BR) ts and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun) (print_term is_pseudo_fun) const_syntax some_thm vars @@ -449,23 +461,23 @@ :: map (print_select "|") clauses ) end; - fun print_val_decl print_typscheme (name, typscheme) = concat - [str "val", str (deresolve name), str ":", print_typscheme typscheme]; + fun print_val_decl print_typscheme (sym, typscheme) = concat + [str "val", str (deresolve sym), str ":", print_typscheme typscheme]; fun print_datatype_decl definer (tyco, (vs, cos)) = let - fun print_co ((co, _), []) = str (deresolve co) - | print_co ((co, _), tys) = concat [str (deresolve co), str "of", + fun print_co ((co, _), []) = str (deresolve_const co) + | print_co ((co, _), tys) = concat [str (deresolve_const co), str "of", enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; in concat ( str definer - :: print_tyco_expr (tyco, map ITyVar vs) + :: print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs) :: str "=" :: separate (str "|") (map print_co cos) ) end; fun print_def is_pseudo_fun needs_typ definer - (ML_Function (name, (vs_ty as (vs, ty), eqs))) = + (ML_Function (const, (vs_ty as (vs, ty), eqs))) = let fun print_eqn ((ts, t), (some_thm, _)) = let @@ -529,57 +541,57 @@ ) end; val prolog = if needs_typ then - concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty] - else (concat o map str) [definer, deresolve name]; + concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty] + else (concat o map str) [definer, deresolve_const const]; in pair - (print_val_decl print_typscheme (name, vs_ty)) + (print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty)) (concat ( prolog :: print_dict_args vs - @| print_eqns (is_pseudo_fun name) eqs + @| print_eqns (is_pseudo_fun (Code_Symbol.Constant const)) eqs )) end | print_def is_pseudo_fun _ definer - (ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) = + (ML_Instance (inst as (tyco, class), { vs, superinsts, inst_params, ... })) = let - fun print_super_instance (_, (classrel, x)) = + fun print_super_instance (super_class, x) = concat [ - (str o deresolve) classrel, + (str o deresolve_classrel) (class, super_class), str "=", - print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x)) + print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), x))) ]; fun print_classparam_instance ((classparam, (const, _)), (thm, _)) = concat [ - (str o deresolve) classparam, + (str o deresolve_const) classparam, str "=", print_app (K false) (SOME thm) reserved NOBR (const, []) ]; in pair (print_val_decl print_dicttypscheme - (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs)))) + (Code_Symbol.Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs)))) (concat ( str definer - :: (str o deresolve) inst - :: (if is_pseudo_fun inst then [str "()"] + :: (str o deresolve_inst) inst + :: (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"] else print_dict_args vs) @ str "=" @@ brackets [ enum_default "()" ";" "{" "}" (map print_super_instance superinsts @ map print_classparam_instance inst_params), str ":", - print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs]) + print_dicttyp (class, tyco `%% map (ITyVar o fst) vs) ] )) end; - fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair - [print_val_decl print_typscheme (name, vs_ty)] + fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair + [print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty)] ((doublesemicolon o map str) ( "let" - :: deresolve name + :: deresolve_const const :: replicate n "_" @ "=" :: "failwith" - @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name + @@ ML_Syntax.print_string const )) | print_stmt (ML_Val binding) = let @@ -591,11 +603,11 @@ | print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) = let val print_def' = print_def (member (op =) pseudo_funs) false; - fun print_pseudo_fun name = concat [ + fun print_pseudo_fun sym = concat [ str "let", - (str o deresolve) name, + (str o deresolve) sym, str "=", - (str o deresolve) name, + (str o deresolve) sym, str "();;" ]; val (sig_ps, (ps, p)) = (apsnd split_last o split_list) @@ -607,7 +619,7 @@ end | print_stmt (ML_Datas [(tyco, (vs, []))]) = let - val ty_p = print_tyco_expr (tyco, map ITyVar vs); + val ty_p = print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs); in pair [concat [str "type", ty_p]] @@ -622,26 +634,26 @@ sig_ps (Pretty.chunks (ps @| doublesemicolon [p])) end - | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) = + | print_stmt (ML_Class (class, (v, (classrels, classparams)))) = let fun print_field s p = concat [str s, str ":", p]; - fun print_super_class_field (super_class, classrel) = - print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v)); + fun print_super_class_field (classrel as (_, super_class)) = + print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v)); fun print_classparam_decl (classparam, ty) = print_val_decl print_typscheme - (classparam, ([(v, [class])], ty)); + (Code_Symbol.Constant classparam, ([(v, [class])], ty)); fun print_classparam_field (classparam, ty) = - print_field (deresolve classparam) (print_typ NOBR ty); + print_field (deresolve_const classparam) (print_typ NOBR ty); val w = "_" ^ first_upper v; fun print_classparam_proj (classparam, _) = - (concat o map str) ["let", deresolve classparam, w, "=", - w ^ "." ^ deresolve classparam ^ ";;"]; + (concat o map str) ["let", deresolve_const classparam, w, "=", + w ^ "." ^ deresolve_const classparam ^ ";;"]; val type_decl_p = concat [ str ("type '" ^ v), - (str o deresolve) class, + (str o deresolve_class) class, str "=", enum_default "unit" ";" "{" "}" ( - map print_super_class_field super_classes + map print_super_class_field classrels @ map print_classparam_field classparams ) ]; @@ -694,7 +706,7 @@ (** SML/OCaml generic part **) -fun ml_program_of_program ctxt symbol_of module_name reserved identifiers program = +fun ml_program_of_program ctxt module_name reserved identifiers program = let fun namify_const upper base (nsp_const, nsp_type) = let @@ -712,76 +724,76 @@ | namify_stmt (Code_Thingol.Classrel _) = namify_const false | namify_stmt (Code_Thingol.Classparam _) = namify_const false | namify_stmt (Code_Thingol.Classinst _) = namify_const false; - fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, ((tysm as (vs, ty), raw_eqs), _))) = + fun ml_binding_of_stmt (sym as Code_Symbol.Constant const, Code_Thingol.Fun ((tysm as (vs, ty), raw_eqs), _)) = let val eqs = filter (snd o snd) raw_eqs; - val (eqs', some_value_name) = if null (filter_out (null o snd) vs) then case eqs + val (eqs', some_sym) = if null (filter_out (null o snd) vs) then case eqs of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE) - else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name)) + else (eqs, SOME (sym, member (op =) (Code_Thingol.add_constsyms t []) sym)) | _ => (eqs, NONE) else (eqs, NONE) - in (ML_Function (name, (tysm, eqs')), some_value_name) end - | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as { vs, ... })) = - (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE) - | ml_binding_of_stmt (name, _) = + in (ML_Function (const, (tysm, eqs')), some_sym) end + | ml_binding_of_stmt (sym as Code_Symbol.Class_Instance inst, Code_Thingol.Classinst (stmt as { vs, ... })) = + (ML_Instance (inst, stmt), if forall (null o snd) vs then SOME (sym, false) else NONE) + | ml_binding_of_stmt (sym, _) = error ("Binding block containing illegal statement: " ^ - (Code_Symbol.quote_symbol ctxt o symbol_of) name) - fun modify_fun (name, stmt) = + Code_Symbol.quote ctxt sym) + fun modify_fun (sym, stmt) = let - val (binding, some_value_name) = ml_binding_of_stmt (name, stmt); + val (binding, some_value_sym) = ml_binding_of_stmt (sym, stmt); val ml_stmt = case binding - of ML_Function (name, ((vs, ty), [])) => - ML_Exc (name, ((vs, ty), + of ML_Function (const, ((vs, ty), [])) => + ML_Exc (const, ((vs, ty), (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty)) - | _ => case some_value_name + | _ => case some_value_sym of NONE => ML_Funs ([binding], []) - | SOME (name, true) => ML_Funs ([binding], [name]) - | SOME (name, false) => ML_Val binding + | SOME (sym, true) => ML_Funs ([binding], [sym]) + | SOME (sym, false) => ML_Val binding in SOME ml_stmt end; fun modify_funs stmts = single (SOME (ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst))) fun modify_datatypes stmts = single (SOME (ML_Datas (map_filter - (fn (name, Code_Thingol.Datatype (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts))) + (fn (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype stmt) => SOME (tyco, stmt) | _ => NONE) stmts))) fun modify_class stmts = single (SOME (ML_Class (the_single (map_filter - (fn (name, Code_Thingol.Class (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts)))) + (fn (Code_Symbol.Type_Class class, Code_Thingol.Class stmt) => SOME (class, stmt) | _ => NONE) stmts)))) fun modify_stmts ([stmt as (_, stmt' as Code_Thingol.Fun _)]) = if Code_Thingol.is_case stmt' then [] else [modify_fun stmt] - | modify_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) = + | modify_stmts ((stmts as (_, Code_Thingol.Fun _) :: _)) = modify_funs (filter_out (Code_Thingol.is_case o snd) stmts) - | modify_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) = + | modify_stmts ((stmts as (_, Code_Thingol.Datatypecons _) :: _)) = modify_datatypes stmts - | modify_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) = + | modify_stmts ((stmts as (_, Code_Thingol.Datatype _) :: _)) = modify_datatypes stmts - | modify_stmts ((stmts as (_, Code_Thingol.Class _)::_)) = + | modify_stmts ((stmts as (_, Code_Thingol.Class _) :: _)) = modify_class stmts - | modify_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) = + | modify_stmts ((stmts as (_, Code_Thingol.Classrel _) :: _)) = modify_class stmts - | modify_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) = + | modify_stmts ((stmts as (_, Code_Thingol.Classparam _) :: _)) = modify_class stmts | modify_stmts ([stmt as (_, Code_Thingol.Classinst _)]) = [modify_fun stmt] - | modify_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) = + | modify_stmts ((stmts as (_, Code_Thingol.Classinst _) :: _)) = modify_funs stmts | modify_stmts stmts = error ("Illegal mutual dependencies: " ^ - (Library.commas o map (Code_Symbol.quote_symbol ctxt o symbol_of o fst)) stmts); + (Library.commas o map (Code_Symbol.quote ctxt o fst)) stmts); in - Code_Namespace.hierarchical_program ctxt symbol_of { + Code_Namespace.hierarchical_program ctxt { module_name = module_name, reserved = reserved, identifiers = identifiers, empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt, cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program end; fun serialize_ml print_ml_module print_ml_stmt with_signatures ctxt - { symbol_of, module_name, reserved_syms, identifiers, includes, + { module_name, reserved_syms, identifiers, includes, class_syntax, tyco_syntax, const_syntax } program = let (* build program *) val { deresolver, hierarchical_program = ml_program } = - ml_program_of_program ctxt symbol_of module_name (Name.make_context reserved_syms) identifiers program; + ml_program_of_program ctxt module_name (Name.make_context reserved_syms) identifiers program; (* print statements *) fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt @@ -803,7 +815,7 @@ lift_markup = apsnd } ml_program)); fun write width NONE = writeln o format [] width | write width (SOME p) = File.write p o format [] width; - fun prepare names width p = ([("", format names width p)], try (deresolver [])); + fun prepare syms width p = ([("", format syms width p)], try (deresolver [])); in Code_Target.serialization write prepare p end; diff -r 525309c2e4ee -r bce3dbc11f95 src/Tools/Code/code_namespace.ML --- a/src/Tools/Code/code_namespace.ML Sat Jan 25 23:50:49 2014 +0100 +++ b/src/Tools/Code/code_namespace.ML Sat Jan 25 23:50:49 2014 +0100 @@ -7,32 +7,32 @@ signature CODE_NAMESPACE = sig type flat_program - val flat_program: Proof.context -> (string -> Code_Symbol.symbol) + val flat_program: Proof.context -> { module_prefix: string, module_name: string, reserved: Name.context, identifiers: Code_Target.identifier_data, empty_nsp: 'a, namify_stmt: Code_Thingol.stmt -> string -> 'a -> string * 'a, modify_stmt: Code_Thingol.stmt -> Code_Thingol.stmt option } -> Code_Thingol.program - -> { deresolver: string -> string -> string, + -> { deresolver: string -> Code_Symbol.symbol -> string, flat_program: flat_program } datatype ('a, 'b) node = Dummy | Stmt of 'a - | Module of ('b * (string * ('a, 'b) node) Graph.T) + | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T) type ('a, 'b) hierarchical_program - val hierarchical_program: Proof.context -> (string -> Code_Symbol.symbol) + val hierarchical_program: Proof.context -> { module_name: string, reserved: Name.context, identifiers: Code_Target.identifier_data, empty_nsp: 'c, namify_module: string -> 'c -> string * 'c, namify_stmt: Code_Thingol.stmt -> string -> 'c -> string * 'c, - cyclic_modules: bool, empty_data: 'b, memorize_data: string -> 'b -> 'b, - modify_stmts: (string * Code_Thingol.stmt) list -> 'a option list } + cyclic_modules: bool, empty_data: 'b, memorize_data: Code_Symbol.symbol -> 'b -> 'b, + modify_stmts: (Code_Symbol.symbol * Code_Thingol.stmt) list -> 'a option list } -> Code_Thingol.program - -> { deresolver: string list -> string -> string, + -> { deresolver: string list -> Code_Symbol.symbol -> string, hierarchical_program: ('a, 'b) hierarchical_program } val print_hierarchical: { print_module: string list -> string -> 'b -> 'c list -> 'c, - print_stmt: string list -> string * 'a -> 'c, + print_stmt: string list -> Code_Symbol.symbol * 'a -> 'c, lift_markup: (Pretty.T -> Pretty.T) -> 'c -> 'c } -> ('a, 'b) hierarchical_program -> 'c list end; @@ -42,24 +42,22 @@ (** fundamental module name hierarchy **) -val split_name = apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode; - -fun lookup_identifier symbol_of identifiers name = - Code_Symbol.lookup identifiers (symbol_of name) +fun lookup_identifier identifiers sym = + Code_Symbol.lookup identifiers sym |> Option.map (split_last o Long_Name.explode); -fun force_identifier symbol_of fragments_tab force_module identifiers name = - case lookup_identifier symbol_of identifiers name of - NONE => (apfst (the o Symtab.lookup fragments_tab) o split_name) name +fun force_identifier ctxt fragments_tab force_module identifiers sym = + case lookup_identifier identifiers sym of + NONE => ((the o Symtab.lookup fragments_tab o Code_Symbol.namespace_prefix ctxt) sym, Code_Symbol.base_name sym) | SOME prefix_name => if null force_module then prefix_name else (force_module, snd prefix_name); -fun build_module_namespace { module_prefix, module_identifiers, reserved } program = +fun build_module_namespace ctxt { module_prefix, module_identifiers, reserved } program = let fun alias_fragments name = case module_identifiers name of SOME name' => Long_Name.explode name' | NONE => map (fn name => fst (Name.variant name reserved)) (Long_Name.explode name); - val module_names = Graph.fold (insert (op =) o fst o split_name o fst) program []; + val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.namespace_prefix ctxt o fst) program []; in fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ alias_fragments name)) module_names Symtab.empty @@ -68,9 +66,9 @@ (** flat program structure **) -type flat_program = ((string * Code_Thingol.stmt option) Graph.T * (string * string list) list) Graph.T; +type flat_program = ((string * Code_Thingol.stmt option) Code_Symbol.Graph.T * (string * Code_Symbol.symbol list) list) Graph.T; -fun flat_program ctxt symbol_of { module_prefix, module_name, reserved, +fun flat_program ctxt { module_prefix, module_name, reserved, identifiers, empty_nsp, namify_stmt, modify_stmt } program = let @@ -78,70 +76,70 @@ val module_identifiers = if module_name = "" then Code_Symbol.lookup_module_data identifiers else K (SOME module_name); - val fragments_tab = build_module_namespace { module_prefix = module_prefix, + val fragments_tab = build_module_namespace ctxt { module_prefix = module_prefix, module_identifiers = module_identifiers, reserved = reserved } program; - val prep_name = force_identifier symbol_of fragments_tab (Long_Name.explode module_name) identifiers + val prep_sym = force_identifier ctxt fragments_tab (Long_Name.explode module_name) identifiers #>> Long_Name.implode; (* distribute statements over hierarchy *) - fun add_stmt name stmt = + fun add_stmt sym stmt = let - val (module_name, base) = prep_name name; + val (module_name, base) = prep_sym sym; in - Graph.default_node (module_name, (Graph.empty, [])) - #> (Graph.map_node module_name o apfst) (Graph.new_node (name, (base, stmt))) + Graph.default_node (module_name, (Code_Symbol.Graph.empty, [])) + #> (Graph.map_node module_name o apfst) (Code_Symbol.Graph.new_node (sym, (base, stmt))) end; - fun add_dependency name name' = + fun add_dependency sym sym' = let - val (module_name, _) = prep_name name; - val (module_name', _) = prep_name name'; + val (module_name, _) = prep_sym sym; + val (module_name', _) = prep_sym sym'; in if module_name = module_name' - then (Graph.map_node module_name o apfst) (Graph.add_edge (name, name')) - else (Graph.map_node module_name o apsnd) (AList.map_default (op =) (module_name', []) (insert (op =) name')) + then (Graph.map_node module_name o apfst) (Code_Symbol.Graph.add_edge (sym, sym')) + else (Graph.map_node module_name o apsnd) (AList.map_default (op =) (module_name', []) (insert (op =) sym')) end; val proto_program = Graph.empty - |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program - |> Graph.fold (fn (name, (_, (_, names))) => - Graph.Keys.fold (add_dependency name) names) program; + |> Code_Symbol.Graph.fold (fn (sym, (stmt, _)) => add_stmt sym stmt) program + |> Code_Symbol.Graph.fold (fn (sym, (_, (_, syms))) => + Code_Symbol.Graph.Keys.fold (add_dependency sym) syms) program; (* name declarations and statement modifications *) - fun declare name (base, stmt) (gr, nsp) = + fun declare sym (base, stmt) (gr, nsp) = let val (base', nsp') = namify_stmt stmt base nsp; - val gr' = (Graph.map_node name o apfst) (K base') gr; + val gr' = (Code_Symbol.Graph.map_node sym o apfst) (K base') gr; in (gr', nsp') end; fun declarations gr = (gr, empty_nsp) - |> fold (fn name => declare name (Graph.get_node gr name)) (Graph.keys gr) + |> fold (fn sym => declare sym (Code_Symbol.Graph.get_node gr sym)) (Code_Symbol.Graph.keys gr) |> fst - |> (Graph.map o K o apsnd) modify_stmt; + |> (Code_Symbol.Graph.map o K o apsnd) modify_stmt; val flat_program = proto_program |> (Graph.map o K o apfst) declarations; (* qualified and unqualified imports, deresolving *) - fun base_deresolver name = fst (Graph.get_node - (fst (Graph.get_node flat_program (fst (prep_name name)))) name); + fun base_deresolver sym = fst (Code_Symbol.Graph.get_node + (fst (Graph.get_node flat_program (fst (prep_sym sym)))) sym); fun classify_names gr imports = let val import_tab = maps - (fn (module_name, names) => map (rpair module_name) names) imports; - val imported_names = map fst import_tab; - val here_names = Graph.keys gr; + (fn (module_name, syms) => map (rpair module_name) syms) imports; + val imported_syms = map fst import_tab; + val here_syms = Code_Symbol.Graph.keys gr; in - Symtab.empty - |> fold (fn name => Symtab.update (name, base_deresolver name)) here_names - |> fold (fn name => Symtab.update (name, - Long_Name.append (the (AList.lookup (op =) import_tab name)) - (base_deresolver name))) imported_names + Code_Symbol.Table.empty + |> fold (fn sym => Code_Symbol.Table.update (sym, base_deresolver sym)) here_syms + |> fold (fn sym => Code_Symbol.Table.update (sym, + Long_Name.append (the (AList.lookup (op =) import_tab sym)) + (base_deresolver sym))) imported_syms end; val deresolver_tab = Symtab.make (AList.make (uncurry classify_names o Graph.get_node flat_program) (Graph.keys flat_program)); - fun deresolver "" name = - Long_Name.append (fst (prep_name name)) (base_deresolver name) - | deresolver module_name name = - the (Symtab.lookup (the (Symtab.lookup deresolver_tab module_name)) name) + fun deresolver "" sym = + Long_Name.append (fst (prep_sym sym)) (base_deresolver sym) + | deresolver module_name sym = + the (Code_Symbol.Table.lookup (the (Symtab.lookup deresolver_tab module_name)) sym) handle Option.Option => error ("Unknown statement name: " - ^ (Code_Symbol.quote_symbol ctxt o symbol_of) name); + ^ Code_Symbol.quote ctxt sym); in { deresolver = deresolver, flat_program = flat_program } end; @@ -151,18 +149,18 @@ datatype ('a, 'b) node = Dummy | Stmt of 'a - | Module of ('b * (string * ('a, 'b) node) Graph.T); + | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T); -type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Graph.T; +type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Code_Symbol.Graph.T; fun map_module_content f (Module content) = Module (f content); fun map_module [] = I | map_module (name_fragment :: name_fragments) = - apsnd o Graph.map_node name_fragment o apsnd o map_module_content + apsnd o Code_Symbol.Graph.map_node (Code_Symbol.Module name_fragment) o apsnd o map_module_content o map_module name_fragments; -fun hierarchical_program ctxt symbol_of { module_name, reserved, identifiers, empty_nsp, +fun hierarchical_program ctxt { module_name, reserved, identifiers, empty_nsp, namify_module, namify_stmt, cyclic_modules, empty_data, memorize_data, modify_stmts } program = let @@ -170,95 +168,95 @@ val module_identifiers = if module_name = "" then Code_Symbol.lookup_module_data identifiers else K (SOME module_name); - val fragments_tab = build_module_namespace { module_prefix = "", + val fragments_tab = build_module_namespace ctxt { module_prefix = "", module_identifiers = module_identifiers, reserved = reserved } program; - val prep_name = force_identifier symbol_of fragments_tab (Long_Name.explode module_name) identifiers; + val prep_sym = force_identifier ctxt fragments_tab (Long_Name.explode module_name) identifiers; (* building empty module hierarchy *) - val empty_module = (empty_data, Graph.empty); + val empty_module = (empty_data, Code_Symbol.Graph.empty); fun ensure_module name_fragment (data, nodes) = - if can (Graph.get_node nodes) name_fragment then (data, nodes) + if can (Code_Symbol.Graph.get_node nodes) (Code_Symbol.Module name_fragment) then (data, nodes) else (data, - nodes |> Graph.new_node (name_fragment, (name_fragment, Module empty_module))); + nodes |> Code_Symbol.Graph.new_node (Code_Symbol.Module name_fragment, (name_fragment, Module empty_module))); fun allocate_module [] = I | allocate_module (name_fragment :: name_fragments) = ensure_module name_fragment - #> (apsnd o Graph.map_node name_fragment o apsnd o map_module_content o allocate_module) name_fragments; + #> (apsnd o Code_Symbol.Graph.map_node (Code_Symbol.Module name_fragment) o apsnd o map_module_content o allocate_module) name_fragments; val empty_program = empty_module |> Symtab.fold (fn (_, fragments) => allocate_module fragments) fragments_tab - |> Graph.fold (allocate_module o these o Option.map fst - o lookup_identifier symbol_of identifiers o fst) program; + |> Code_Symbol.Graph.fold (allocate_module o these o Option.map fst + o lookup_identifier identifiers o fst) program; (* distribute statements over hierarchy *) - fun add_stmt name stmt = + fun add_stmt sym stmt = let - val (name_fragments, base) = prep_name name; + val (name_fragments, base) = prep_sym sym; in - (map_module name_fragments o apsnd) (Graph.new_node (name, (base, Stmt stmt))) + (map_module name_fragments o apsnd) (Code_Symbol.Graph.new_node (sym, (base, Stmt stmt))) end; - fun add_dependency name name' = + fun add_dependency sym sym' = let - val (name_fragments, _) = prep_name name; - val (name_fragments', _) = prep_name name'; + val (name_fragments, _) = prep_sym sym; + val (name_fragments', _) = prep_sym sym'; val (name_fragments_common, (diff, diff')) = chop_prefix (op =) (name_fragments, name_fragments'); val is_module = not (null diff andalso null diff'); - val dep = pairself hd (diff @ [name], diff' @ [name']); + val dep = pairself hd (map Code_Symbol.Module diff @ [sym], map Code_Symbol.Module diff' @ [sym']); val add_edge = if is_module andalso not cyclic_modules - then (fn node => Graph.add_edge_acyclic dep node + then (fn node => Code_Symbol.Graph.add_edge_acyclic dep node handle Graph.CYCLES _ => error ("Dependency " - ^ (Code_Symbol.quote_symbol ctxt o symbol_of) name ^ " -> " - ^ (Code_Symbol.quote_symbol ctxt o symbol_of) name' + ^ Code_Symbol.quote ctxt sym ^ " -> " + ^ Code_Symbol.quote ctxt sym' ^ " would result in module dependency cycle")) - else Graph.add_edge dep + else Code_Symbol.Graph.add_edge dep in (map_module name_fragments_common o apsnd) add_edge end; val proto_program = empty_program - |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program - |> Graph.fold (fn (name, (_, (_, names))) => - Graph.Keys.fold (add_dependency name) names) program; + |> Code_Symbol.Graph.fold (fn (sym, (stmt, _)) => add_stmt sym stmt) program + |> Code_Symbol.Graph.fold (fn (sym, (_, (_, syms))) => + Code_Symbol.Graph.Keys.fold (add_dependency sym) syms) program; (* name declarations, data and statement modifications *) fun make_declarations nsps (data, nodes) = let - val (module_fragments, stmt_names) = List.partition - (fn name_fragment => case Graph.get_node nodes name_fragment - of (_, Module _) => true | _ => false) (Graph.keys nodes); - fun declare namify name (nsps, nodes) = + val (module_fragments, stmt_syms) = List.partition + (fn sym => case Code_Symbol.Graph.get_node nodes sym + of (_, Module _) => true | _ => false) (Code_Symbol.Graph.keys nodes); + fun declare namify sym (nsps, nodes) = let - val (base, node) = Graph.get_node nodes name; + val (base, node) = Code_Symbol.Graph.get_node nodes sym; val (base', nsps') = namify node base nsps; - val nodes' = Graph.map_node name (K (base', node)) nodes; + val nodes' = Code_Symbol.Graph.map_node sym (K (base', node)) nodes; in (nsps', nodes') end; val (nsps', nodes') = (nsps, nodes) |> fold (declare (K namify_module)) module_fragments - |> fold (declare (namify_stmt o (fn Stmt stmt => stmt))) stmt_names; + |> fold (declare (namify_stmt o (fn Stmt stmt => stmt))) stmt_syms; fun zip_fillup xs ys = xs ~~ ys @ replicate (length xs - length ys) NONE; - fun select_names names = case filter (member (op =) stmt_names) names + fun select_syms syms = case filter (member (op =) stmt_syms) syms of [] => NONE - | xs => SOME xs; - val modify_stmts' = AList.make (snd o Graph.get_node nodes) + | syms => SOME syms; + val modify_stmts' = AList.make (snd o Code_Symbol.Graph.get_node nodes) #> split_list ##> map (fn Stmt stmt => stmt) - #> (fn (names, stmts) => zip_fillup names (modify_stmts (names ~~ stmts))); - val stmtss' = (maps modify_stmts' o map_filter select_names o Graph.strong_conn) nodes; - val nodes'' = Graph.map (fn name => apsnd (fn Module content => Module (make_declarations nsps' content) - | _ => case AList.lookup (op =) stmtss' name of SOME (SOME stmt) => Stmt stmt | _ => Dummy)) nodes'; - val data' = fold memorize_data stmt_names data; + #> (fn (syms, stmts) => zip_fillup syms (modify_stmts (syms ~~ stmts))); + val stmtss' = (maps modify_stmts' o map_filter select_syms o Code_Symbol.Graph.strong_conn) nodes; + val nodes'' = Code_Symbol.Graph.map (fn sym => apsnd (fn Module content => Module (make_declarations nsps' content) + | _ => case AList.lookup (op =) stmtss' sym of SOME (SOME stmt) => Stmt stmt | _ => Dummy)) nodes'; + val data' = fold memorize_data stmt_syms data; in (data', nodes'') end; val (_, hierarchical_program) = make_declarations empty_nsp proto_program; (* deresolving *) - fun deresolver prefix_fragments name = + fun deresolver prefix_fragments sym = let - val (name_fragments, _) = prep_name name; + val (name_fragments, _) = prep_sym sym; val (_, (_, remainder)) = chop_prefix (op =) (prefix_fragments, name_fragments); - val nodes = fold (fn name_fragment => fn nodes => case Graph.get_node nodes name_fragment + val nodes = fold (fn name_fragment => fn nodes => case Code_Symbol.Graph.get_node nodes (Code_Symbol.Module name_fragment) of (_, Module (_, nodes)) => nodes) name_fragments hierarchical_program; - val (base', _) = Graph.get_node nodes name; + val (base', _) = Code_Symbol.Graph.get_node nodes sym; in Long_Name.implode (remainder @ [base']) end - handle Graph.UNDEF _ => error ("Unknown statement name: " - ^ (Code_Symbol.quote_symbol ctxt o symbol_of) name); + handle Code_Symbol.Graph.UNDEF _ => error ("Unknown statement name: " + ^ Code_Symbol.quote ctxt sym); in { deresolver = deresolver, hierarchical_program = hierarchical_program } end; @@ -266,10 +264,10 @@ let fun print_node _ (_, Dummy) = NONE - | print_node prefix_fragments (name, Stmt stmt) = - SOME (lift_markup (Code_Printer.markup_stmt name) - (print_stmt prefix_fragments (name, stmt))) - | print_node prefix_fragments (name_fragment, Module (data, nodes)) = + | print_node prefix_fragments (sym, Stmt stmt) = + SOME (lift_markup (Code_Printer.markup_stmt sym) + (print_stmt prefix_fragments (sym, stmt))) + | print_node prefix_fragments (Code_Symbol.Module name_fragment, Module (data, nodes)) = let val prefix_fragments' = prefix_fragments @ [name_fragment] in @@ -278,9 +276,9 @@ end and print_nodes prefix_fragments nodes = let - val xs = (map_filter (fn name => print_node prefix_fragments - (name, snd (Graph.get_node nodes name))) o rev o flat o Graph.strong_conn) nodes + val xs = (map_filter (fn sym => print_node prefix_fragments + (sym, snd (Code_Symbol.Graph.get_node nodes sym))) o rev o flat o Code_Symbol.Graph.strong_conn) nodes in if null xs then NONE else SOME xs end; in these o print_nodes [] end; -end; \ No newline at end of file +end; diff -r 525309c2e4ee -r bce3dbc11f95 src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Sat Jan 25 23:50:49 2014 +0100 +++ b/src/Tools/Code/code_printer.ML Sat Jan 25 23:50:49 2014 +0100 @@ -25,8 +25,8 @@ val semicolon: Pretty.T list -> Pretty.T val doublesemicolon: Pretty.T list -> Pretty.T val indent: int -> Pretty.T -> Pretty.T - val markup_stmt: string -> Pretty.T -> Pretty.T - val format: string list -> int -> Pretty.T -> string + val markup_stmt: Code_Symbol.symbol -> Pretty.T -> Pretty.T + val format: Code_Symbol.symbol list -> int -> Pretty.T -> string val first_upper: string -> string val first_lower: string -> string @@ -36,7 +36,7 @@ val lookup_var: var_ctxt -> string -> string val intro_base_names: (string -> bool) -> (string -> string) -> string list -> var_ctxt -> var_ctxt - val intro_base_names_for: (string -> bool) -> (string -> string) + val intro_base_names_for: (string -> bool) -> (Code_Symbol.symbol -> string) -> iterm list -> var_ctxt -> var_ctxt val aux_params: var_ctxt -> iterm list list -> string list @@ -81,7 +81,7 @@ val simple_const_syntax: simple_const_syntax -> const_syntax val complex_const_syntax: complex_const_syntax -> const_syntax val activate_const_syntax: theory -> literals - -> string -> const_syntax -> Code_Thingol.naming -> activated_const_syntax * Code_Thingol.naming + -> string -> const_syntax -> activated_const_syntax val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list) -> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T) -> (string -> activated_const_syntax option) @@ -125,17 +125,18 @@ fun doublesemicolon ps = Pretty.block [concat ps, str ";;"]; fun indent i = Print_Mode.setmp [] (Pretty.indent i); -fun markup_stmt name = Print_Mode.setmp [code_presentationN] - (Pretty.mark (code_presentationN, [(stmt_nameN, name)])); +fun markup_stmt sym = Print_Mode.setmp [code_presentationN] + (Pretty.mark (code_presentationN, [(stmt_nameN, Code_Symbol.marker sym)])); fun filter_presentation [] tree = Buffer.empty |> fold XML.add_content tree - | filter_presentation presentation_names tree = + | filter_presentation presentation_syms tree = let + val presentation_idents = map Code_Symbol.marker presentation_syms fun is_selected (name, attrs) = name = code_presentationN - andalso member (op =) presentation_names (the (Properties.get attrs stmt_nameN)); + andalso member (op =) presentation_idents (the (Properties.get attrs stmt_nameN)); fun add_content_with_space tree (is_first, buf) = buf |> not is_first ? Buffer.add "\n\n" @@ -198,8 +199,8 @@ fun intro_base_names_for no_syntax deresolve ts = [] - |> fold Code_Thingol.add_constnames ts - |> intro_base_names no_syntax deresolve; + |> fold Code_Thingol.add_constsyms ts + |> intro_base_names (fn Code_Symbol.Constant const => no_syntax const | _ => true) deresolve; (** pretty literals **) @@ -304,30 +305,31 @@ datatype activated_const_syntax = Plain_const_syntax of int * string | Complex_const_syntax of activated_complex_const_syntax; -fun activate_const_syntax thy literals c (plain_const_syntax s) naming = - (Plain_const_syntax (Code.args_number thy c, s), naming) - | activate_const_syntax thy literals c (complex_const_syntax (n, (cs, f))) naming = - fold_map (Code_Thingol.ensure_declared_const thy) cs naming - |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs'))); +fun activate_const_syntax thy literals c (plain_const_syntax s) = + Plain_const_syntax (Code.args_number thy c, s) + | activate_const_syntax thy literals c (complex_const_syntax (n, (cs, f)))= + Complex_const_syntax (n, f literals cs); fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy - (app as ({ name = c, dom, ... }, ts)) = - case const_syntax c of - NONE => brackify fxy (print_app_expr some_thm vars app) - | SOME (Plain_const_syntax (_, s)) => - brackify fxy (str s :: map (print_term some_thm vars BR) ts) - | SOME (Complex_const_syntax (k, print)) => - let - fun print' fxy ts = - print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom); - in - if k = length ts - then print' fxy ts - else if k < length ts - then case chop k ts of (ts1, ts2) => - brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2) - else print_term some_thm vars fxy (Code_Thingol.eta_expand k app) - end; + (app as ({ sym, dom, ... }, ts)) = + case sym of + Code_Symbol.Constant const => (case const_syntax const of + NONE => brackify fxy (print_app_expr some_thm vars app) + | SOME (Plain_const_syntax (_, s)) => + brackify fxy (str s :: map (print_term some_thm vars BR) ts) + | SOME (Complex_const_syntax (k, print)) => + let + fun print' fxy ts = + print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom); + in + if k = length ts + then print' fxy ts + else if k < length ts + then case chop k ts of (ts1, ts2) => + brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2) + else print_term some_thm vars fxy (Code_Thingol.eta_expand k app) + end) + | _ => brackify fxy (print_app_expr some_thm vars app); fun gen_print_bind print_term thm (fxy : fixity) pat vars = let diff -r 525309c2e4ee -r bce3dbc11f95 src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Sat Jan 25 23:50:49 2014 +0100 +++ b/src/Tools/Code/code_runtime.ML Sat Jan 25 23:50:49 2014 +0100 @@ -52,7 +52,7 @@ datatype truth = Holds; val _ = Theory.setup - (Code_Target.extend_target (target, (Code_ML.target_SML, K I)) + (Code_Target.extend_target (target, (Code_ML.target_SML, I)) #> Code_Target.set_printings (Code_Symbol.Type_Constructor (@{type_name prop}, [(target, SOME (0, (K o K o K) (Code_Printer.str s_truth)))])) #> Code_Target.set_printings (Code_Symbol.Constant (@{const_name Code_Generator.holds}, @@ -87,10 +87,13 @@ val ctxt = Proof_Context.init_global thy; in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end; -fun obtain_evaluator thy some_target naming program consts expr = - Code_Target.evaluator thy (the_default target some_target) naming program consts expr +fun obtain_evaluator thy some_target program consts expr = + Code_Target.evaluator thy (the_default target some_target) program consts expr |> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules)); +fun obtain_evaluator' thy some_target program = + obtain_evaluator thy some_target program o map Code_Symbol.Constant; + fun evaluation cookie thy evaluator vs_t args = let val ctxt = Proof_Context.init_global thy; @@ -110,8 +113,8 @@ val _ = if ! trace then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term_global thy t)) else () - fun evaluator naming program ((_, vs_ty), t) deps = - evaluation cookie thy (obtain_evaluator thy some_target naming program deps) (vs_ty, t) args; + fun evaluator program ((_, vs_ty), t) deps = + evaluation cookie thy (obtain_evaluator thy some_target program deps) (vs_ty, t) args; in Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t end; fun dynamic_value_strict cookie thy some_target postproc t args = @@ -120,9 +123,9 @@ fun dynamic_value cookie thy some_target postproc t args = partiality_as_none (dynamic_value_exn cookie thy some_target postproc t args); -fun static_evaluator cookie thy some_target naming program consts' = +fun static_evaluator cookie thy some_target program consts' = let - val evaluator = obtain_evaluator thy some_target naming program consts' + val evaluator = obtain_evaluator' thy some_target program consts' in fn ((_, vs_ty), t) => fn _ => evaluation cookie thy evaluator (vs_ty, t) [] end; fun static_value_exn cookie thy some_target postproc consts = @@ -175,13 +178,13 @@ in fun dynamic_holds_conv thy = Code_Thingol.dynamic_conv thy - (fn naming => fn program => fn vs_t => fn deps => - check_holds_oracle thy (obtain_evaluator thy NONE naming program deps) vs_t deps) + (fn program => fn vs_t => fn deps => + check_holds_oracle thy (obtain_evaluator thy NONE program deps) vs_t deps) o reject_vars thy; fun static_holds_conv thy consts = Code_Thingol.static_conv thy consts - (fn naming => fn program => fn consts' => - check_holds_oracle thy (obtain_evaluator thy NONE naming program consts')) + (fn program => fn consts' => + check_holds_oracle thy (obtain_evaluator' thy NONE program consts')) o reject_vars thy; end; (*local*) @@ -192,23 +195,22 @@ fun evaluation_code thy module_name tycos consts = let val ctxt = Proof_Context.init_global thy; - val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts; - val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos; + val program = Code_Thingol.consts_program thy false consts; val (ml_modules, target_names) = Code_Target.produce_code_for thy - target NONE module_name [] naming program (consts' @ tycos'); + target NONE module_name [] program (map Code_Symbol.Constant consts @ map Code_Symbol.Type_Constructor tycos); val ml_code = space_implode "\n\n" (map snd ml_modules); - val (consts'', tycos'') = chop (length consts') target_names; + val (consts', tycos') = chop (length consts) target_names; val consts_map = map2 (fn const => fn NONE => error ("Constant " ^ (quote o Code.string_of_const thy) const ^ "\nhas a user-defined serialization") - | SOME const'' => (const, const'')) consts consts'' + | SOME const' => (const, const')) consts consts' val tycos_map = map2 (fn tyco => fn NONE => error ("Type " ^ quote (Proof_Context.extern_type ctxt tyco) ^ "\nhas a user-defined serialization") - | SOME tyco'' => (tyco, tyco'')) tycos tycos''; + | SOME tyco' => (tyco, tyco')) tycos tycos'; in (ml_code, (tycos_map, consts_map)) end; diff -r 525309c2e4ee -r bce3dbc11f95 src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Sat Jan 25 23:50:49 2014 +0100 +++ b/src/Tools/Code/code_scala.ML Sat Jan 25 23:50:49 2014 +0100 @@ -27,15 +27,18 @@ fun print_scala_stmt tyco_syntax const_syntax reserved args_num is_constr (deresolve, deresolve_full) = let + val deresolve_const = deresolve o Code_Symbol.Constant; + val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor; + val deresolve_class = deresolve o Code_Symbol.Type_Class; fun lookup_tyvar tyvars = lookup_var tyvars o first_upper; fun intro_tyvars vs = intro_vars (map (first_upper o fst) vs); - fun print_tyco_expr tyvars fxy (tyco, tys) = applify "[" "]" - (print_typ tyvars NOBR) fxy ((str o deresolve) tyco) tys + fun print_tyco_expr tyvars fxy (sym, tys) = applify "[" "]" + (print_typ tyvars NOBR) fxy ((str o deresolve) sym) tys and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco - of NONE => print_tyco_expr tyvars fxy (tyco, tys) + of NONE => print_tyco_expr tyvars fxy (Code_Symbol.Type_Constructor tyco, tys) | SOME (_, print) => print (print_typ tyvars) fxy tys) | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v; - fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (class, [ty]); + fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (Code_Symbol.Type_Class class, [ty]); fun print_tupled_typ tyvars ([], ty) = print_typ tyvars NOBR ty | print_tupled_typ tyvars ([ty1], ty2) = @@ -67,20 +70,24 @@ end | print_term tyvars is_pat some_thm vars fxy (ICase case_expr) = (case Code_Thingol.unfold_const_app (#primitive case_expr) - of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c) + of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) => + if is_none (const_syntax const) then print_case tyvars some_thm vars fxy case_expr else print_app tyvars is_pat some_thm vars fxy app | NONE => print_case tyvars some_thm vars fxy case_expr) and print_app tyvars is_pat some_thm vars fxy - (app as ({ name = c, typargs, dom, ... }, ts)) = + (app as ({ sym, typargs, dom, ... }, ts)) = let val k = length ts; val typargs' = if is_pat then [] else typargs; - val (l, print') = case const_syntax c - of NONE => (args_num c, fn fxy => fn ts => gen_applify (is_constr c ) "(" ")" + val syntax = case sym of + Code_Symbol.Constant const => const_syntax const + | _ => NONE; + val (l, print') = case syntax of + NONE => (args_num sym, fn fxy => fn ts => gen_applify (is_constr sym) "(" ")" (print_term tyvars is_pat some_thm vars NOBR) fxy (applify "[" "]" (print_typ tyvars NOBR) - NOBR ((str o deresolve) c) typargs') ts) + NOBR ((str o deresolve) sym) typargs') ts) | SOME (Plain_const_syntax (k, s)) => (k, fn fxy => fn ts => applify "(" ")" (print_term tyvars is_pat some_thm vars NOBR) fxy (applify "[" "]" (print_typ tyvars NOBR) @@ -137,32 +144,32 @@ |> single |> enclose "(" ")" end; - fun print_context tyvars vs name = applify "[" "]" + fun print_context tyvars vs sym = applify "[" "]" (fn (v, sort) => (Pretty.block o map str) - (lookup_tyvar tyvars v :: maps (fn sort => [" : ", deresolve sort]) sort)) - NOBR ((str o deresolve) name) vs; - fun print_defhead tyvars vars name vs params tys ty = + (lookup_tyvar tyvars v :: maps (fn class => [" : ", deresolve_class class]) sort)) + NOBR ((str o deresolve) sym) vs; + fun print_defhead tyvars vars const vs params tys ty = Pretty.block [str "def ", constraint (applify "(" ")" (fn (param, ty) => constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty)) - NOBR (print_context tyvars vs name) (params ~~ tys)) (print_typ tyvars NOBR ty), + NOBR (print_context tyvars vs (Code_Symbol.Constant const)) (params ~~ tys)) (print_typ tyvars NOBR ty), str " ="]; - fun print_def name (vs, ty) [] = + fun print_def const (vs, ty) [] = let val (tys, ty') = Code_Thingol.unfold_fun ty; val params = Name.invent (snd reserved) "a" (length tys); val tyvars = intro_tyvars vs reserved; val vars = intro_vars params reserved; in - concat [print_defhead tyvars vars name vs params tys ty', - str ("sys.error(\"" ^ name ^ "\")")] + concat [print_defhead tyvars vars const vs params tys ty', + str ("sys.error(\"" ^ const ^ "\")")] end - | print_def name (vs, ty) eqs = + | print_def const (vs, ty) eqs = let val tycos = fold (fn ((ts, t), _) => fold Code_Thingol.add_tyconames (t :: ts)) eqs []; val tyvars = reserved |> intro_base_names - (is_none o tyco_syntax) deresolve tycos + (is_none o tyco_syntax) deresolve_tyco tycos |> intro_tyvars vs; val simple = case eqs of [((ts, _), _)] => forall Code_Thingol.is_IVar ts @@ -188,7 +195,7 @@ tuplify (map (print_term tyvars true some_thm vars' NOBR) ts), str "=>", print_rhs vars' eq] end; - val head = print_defhead tyvars vars2 name vs params tys' ty'; + val head = print_defhead tyvars vars2 const vs params tys' ty'; in if simple then concat [head, print_rhs vars2 (hd eqs)] else @@ -197,34 +204,34 @@ str "match", str "{"], str "}") (map print_clause eqs) end; - val print_method = str o Library.enclose "`" "`" o deresolve_full; - fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) = - print_def name (vs, ty) (filter (snd o snd) raw_eqs) - | print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) = + val print_method = str o Library.enclose "`" "`" o deresolve_full o Code_Symbol.Constant; + fun print_stmt (Code_Symbol.Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) = + print_def const (vs, ty) (filter (snd o snd) raw_eqs) + | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, cos)) = let val tyvars = intro_tyvars (map (rpair []) vs) reserved; fun print_co ((co, vs_args), tys) = concat [Pretty.block ((applify "[" "]" (str o lookup_tyvar tyvars) NOBR - ((concat o map str) ["final", "case", "class", deresolve co]) vs_args) + ((concat o map str) ["final", "case", "class", deresolve_const co]) vs_args) @@ enum "," "(" ")" (map (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg)) (Name.invent_names (snd reserved) "a" tys))), str "extends", applify "[" "]" (str o lookup_tyvar tyvars) NOBR - ((str o deresolve) name) vs + ((str o deresolve_tyco) tyco) vs ]; in Pretty.chunks (applify "[" "]" (str o lookup_tyvar tyvars) - NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve name]) vs + NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs :: map print_co cos) end - | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) = + | print_stmt (Code_Symbol.Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) = let - val tyvars = intro_tyvars [(v, [name])] reserved; + val tyvars = intro_tyvars [(v, [class])] reserved; fun add_typarg s = Pretty.block [str s, str "[", (str o lookup_tyvar tyvars) v, str "]"]; fun print_super_classes [] = NONE - | print_super_classes classes = SOME (concat (str "extends" - :: separate (str "with") (map (add_typarg o deresolve o fst) classes))); + | print_super_classes classrels = SOME (concat (str "extends" + :: separate (str "with") (map (add_typarg o deresolve_class o snd) classrels))); fun print_classparam_val (classparam, ty) = concat [str "val", constraint (print_method classparam) ((print_tupled_typ tyvars o Code_Thingol.unfold_fun) ty)]; @@ -238,22 +245,22 @@ in concat [str "def", constraint (Pretty.block [applify "(" ")" (fn (aux, ty) => constraint ((str o lookup_var vars) aux) - (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve classparam)) + (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_const classparam)) (auxs ~~ tys), str "(implicit ", str implicit_name, str ": ", - add_typarg (deresolve name), str ")"]) (print_typ tyvars NOBR ty), str "=", + add_typarg (deresolve_class class), str ")"]) (print_typ tyvars NOBR ty), str "=", applify "(" ")" (str o lookup_var vars) NOBR (Pretty.block [str implicit_name, str ".", print_method classparam]) auxs] end; in Pretty.chunks ( (Pretty.block_enclose - (concat ([str "trait", (add_typarg o deresolve) name] - @ the_list (print_super_classes super_classes) @ [str "{"]), str "}") + (concat ([str "trait", (add_typarg o deresolve_class) class] + @ the_list (print_super_classes classrels) @ [str "{"]), str "}") (map print_classparam_val classparams)) :: map print_classparam_def classparams ) end - | print_stmt (name, Code_Thingol.Classinst + | print_stmt (sym, Code_Thingol.Classinst { class, tyco, vs, inst_params, superinst_params, ... }) = let val tyvars = intro_tyvars vs reserved; @@ -277,13 +284,13 @@ end; in Pretty.block_enclose (concat [str "implicit def", - constraint (print_context tyvars vs name) (print_dicttyp tyvars classtyp), + constraint (print_context tyvars vs sym) (print_dicttyp tyvars classtyp), str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}") (map print_classparam_instance (inst_params @ superinst_params)) end; in print_stmt end; -fun scala_program_of_program ctxt symbol_of module_name reserved identifiers program = +fun scala_program_of_program ctxt module_name reserved identifiers program = let fun namify_module name_fragment ((nsp_class, nsp_object), nsp_common) = let @@ -312,49 +319,49 @@ | namify_stmt (Code_Thingol.Classrel _) = namify_object | namify_stmt (Code_Thingol.Classparam _) = namify_object | namify_stmt (Code_Thingol.Classinst _) = namify_common false; - fun memorize_implicits name = + fun memorize_implicits sym = let fun is_classinst stmt = case stmt of Code_Thingol.Classinst _ => true | _ => false; - val implicits = filter (is_classinst o Graph.get_node program) - (Graph.immediate_succs program name); + val implicits = filter (is_classinst o Code_Symbol.Graph.get_node program) + (Code_Symbol.Graph.immediate_succs program sym); in union (op =) implicits end; - fun modify_stmt (_, Code_Thingol.Fun (_, (_, SOME _))) = NONE + fun modify_stmt (_, Code_Thingol.Fun (_, SOME _)) = NONE | modify_stmt (_, Code_Thingol.Datatypecons _) = NONE | modify_stmt (_, Code_Thingol.Classrel _) = NONE | modify_stmt (_, Code_Thingol.Classparam _) = NONE | modify_stmt (_, stmt) = SOME stmt; in - Code_Namespace.hierarchical_program ctxt symbol_of + Code_Namespace.hierarchical_program ctxt { module_name = module_name, reserved = reserved, identifiers = identifiers, empty_nsp = ((reserved, reserved), reserved), namify_module = namify_module, namify_stmt = namify_stmt, cyclic_modules = true, empty_data = [], memorize_data = memorize_implicits, modify_stmts = map modify_stmt } program end; -fun serialize_scala ctxt { symbol_of, module_name, reserved_syms, identifiers, +fun serialize_scala ctxt { module_name, reserved_syms, identifiers, includes, class_syntax, tyco_syntax, const_syntax } program = let (* build program *) val { deresolver, hierarchical_program = scala_program } = - scala_program_of_program ctxt symbol_of module_name (Name.make_context reserved_syms) identifiers program; + scala_program_of_program ctxt module_name (Name.make_context reserved_syms) identifiers program; (* print statements *) - fun lookup_constr tyco constr = case Graph.get_node program tyco - of Code_Thingol.Datatype (_, (_, constrs)) => + fun lookup_constr tyco constr = case Code_Symbol.Graph.get_node program (Code_Symbol.Type_Constructor tyco) + of Code_Thingol.Datatype (_, constrs) => the (AList.lookup (op = o apsnd fst) constrs constr); - fun classparams_of_class class = case Graph.get_node program class - of Code_Thingol.Class (_, (_, (_, classparams))) => classparams; - fun args_num c = case Graph.get_node program c - of Code_Thingol.Fun (_, (((_, ty), []), _)) => + fun classparams_of_class class = case Code_Symbol.Graph.get_node program (Code_Symbol.Type_Class class) + of Code_Thingol.Class (_, (_, classparams)) => classparams; + fun args_num (sym as Code_Symbol.Constant const) = case Code_Symbol.Graph.get_node program sym + of Code_Thingol.Fun (((_, ty), []), _) => (length o fst o Code_Thingol.unfold_fun) ty - | Code_Thingol.Fun (_, ((_, ((ts, _), _) :: _), _)) => length ts - | Code_Thingol.Datatypecons (_, tyco) => length (lookup_constr tyco c) - | Code_Thingol.Classparam (_, class) => + | Code_Thingol.Fun ((_, ((ts, _), _) :: _), _) => length ts + | Code_Thingol.Datatypecons tyco => length (lookup_constr tyco const) + | Code_Thingol.Classparam class => (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =) - (classparams_of_class class)) c; + (classparams_of_class class)) const; fun print_stmt prefix_fragments = print_scala_stmt tyco_syntax const_syntax (make_vars reserved_syms) args_num (Code_Thingol.is_constr program) (deresolver prefix_fragments, deresolver []); @@ -378,7 +385,7 @@ lift_markup = I } scala_program); fun write width NONE = writeln o format [] width | write width (SOME p) = File.write p o format [] width; - fun prepare names width p = ([("", format names width p)], try (deresolver [])); + fun prepare syms width p = ([("", format syms width p)], try (deresolver [])); in Code_Target.serialization write prepare p end; diff -r 525309c2e4ee -r bce3dbc11f95 src/Tools/Code/code_simp.ML --- a/src/Tools/Code/code_simp.ML Sat Jan 25 23:50:49 2014 +0100 +++ b/src/Tools/Code/code_simp.ML Sat Jan 25 23:50:49 2014 +0100 @@ -52,7 +52,7 @@ (* build simpset and conversion from program *) -fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss = +fun add_stmt (Code_Thingol.Fun ((_, eqs), some_cong)) ss = ss |> fold Simplifier.add_simp ((map_filter (fst o snd)) eqs) |> fold Simplifier.add_cong (the_list some_cong) @@ -61,7 +61,7 @@ |> fold Simplifier.add_simp (map (fst o snd) inst_params) | add_stmt _ ss = ss; -val add_program = Graph.fold (add_stmt o fst o snd); +val add_program = Code_Symbol.Graph.fold (add_stmt o fst o snd); fun simp_ctxt_program thy some_ss program = simp_ctxt_default thy some_ss @@ -77,7 +77,7 @@ (* evaluation with dynamic code context *) fun dynamic_conv thy = Code_Thingol.dynamic_conv thy - (fn _ => fn program => fn _ => fn _ => rewrite_modulo thy NONE program); + (fn program => fn _ => fn _ => rewrite_modulo thy NONE program); fun dynamic_tac thy = CONVERSION (dynamic_conv thy) THEN' conclude_tac thy NONE (Proof_Context.init_global thy); diff -r 525309c2e4ee -r bce3dbc11f95 src/Tools/Code/code_symbol.ML --- a/src/Tools/Code/code_symbol.ML Sat Jan 25 23:50:49 2014 +0100 +++ b/src/Tools/Code/code_symbol.ML Sat Jan 25 23:50:49 2014 +0100 @@ -13,9 +13,12 @@ type symbol = (string, string, class, class * class, string * class, string) attr structure Table: TABLE; structure Graph: GRAPH; - val default_name: Proof.context -> symbol -> string * string - val quote_symbol: Proof.context -> symbol -> string - val tyco_fun: string + val namespace_prefix: Proof.context -> symbol -> string + val base_name: symbol -> string + val quote: Proof.context -> symbol -> string + val marker: symbol -> string + val value: symbol + val is_value: symbol -> bool val map_attr: ('a -> 'g) -> ('b -> 'h) -> ('c -> 'i) -> ('d -> 'j) -> ('e -> 'k) -> ('f -> 'l) -> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('g, 'h, 'i, 'j, 'k, 'l) attr val maps_attr: ('a -> 'g list) -> ('b -> 'h list) @@ -38,6 +41,8 @@ val lookup_class_instance_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string * class -> 'e option val lookup_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'f option val lookup: ('a, 'a, 'a, 'a, 'a, 'a) data -> symbol -> 'a option + val symbols_of: ('a, 'b, 'c, 'd, 'e, 'f) data -> symbol list + val mapped_const_data: (string -> 'a -> 'g) -> ('a, 'b, 'c, 'd, 'e, 'f) data -> 'g Symtab.table val dest_constant_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'a) list val dest_type_constructor_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'b) list val dest_type_class_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (class * 'c) list @@ -89,40 +94,48 @@ | NONE => (case Code.get_type_of_constr_or_abstr thy c of SOME (tyco, _) => thyname_of_type thy tyco | NONE => #theory_name (Name_Space.the_entry (Sign.const_space thy) c)); - fun base_rel (x, y) = Long_Name.base_name y ^ "_" ^ Long_Name.base_name x; - fun plainify ctxt get_prefix get_basename thing = - (get_prefix (Proof_Context.theory_of ctxt) thing, - Name.desymbolize false (get_basename thing)); + fun prefix thy (Constant "") = "Code" + | prefix thy (Constant c) = thyname_of_const thy c + | prefix thy (Type_Constructor tyco) = thyname_of_type thy tyco + | prefix thy (Type_Class class) = thyname_of_class thy class + | prefix thy (Class_Relation (class, _)) = thyname_of_class thy class + | prefix thy (Class_Instance inst) = thyname_of_instance thy inst; + val base = Name.desymbolize false o Long_Name.base_name; + fun base_rel (x, y) = base y ^ "_" ^ base x; in -fun default_name ctxt (Constant "==>") = - plainify ctxt thyname_of_const (K "follows") "==>" - | default_name ctxt (Constant "==") = - plainify ctxt thyname_of_const (K "meta_eq") "==" - | default_name ctxt (Constant c) = - plainify ctxt thyname_of_const Long_Name.base_name c - | default_name ctxt (Type_Constructor "fun") = - plainify ctxt thyname_of_type (K "fun") "fun" - | default_name ctxt (Type_Constructor tyco) = - plainify ctxt thyname_of_type Long_Name.base_name tyco - | default_name ctxt (Type_Class class) = - plainify ctxt thyname_of_class Long_Name.base_name class - | default_name ctxt (Class_Relation classrel) = - plainify ctxt (fn thy => fn (class, _) => thyname_of_class thy class) base_rel classrel - | default_name ctxt (Class_Instance inst) = - plainify ctxt thyname_of_instance base_rel inst; +fun base_name (Constant "") = "value" + | base_name (Constant "==>") = "follows" + | base_name (Constant "==") = "meta_eq" + | base_name (Constant c) = base c + | base_name (Type_Constructor tyco) = base tyco + | base_name (Type_Class class) = base class + | base_name (Class_Relation classrel) = base_rel classrel + | base_name (Class_Instance inst) = base_rel inst; -val tyco_fun = (uncurry Long_Name.append o default_name @{context}) (Type_Constructor "fun"); +fun namespace_prefix ctxt = prefix (Proof_Context.theory_of ctxt); + +fun default_name ctxt sym = (namespace_prefix ctxt sym, base_name sym); + +val value = Constant ""; +fun is_value (Constant "") = true + | is_value _ = false; end; -fun quote_symbol ctxt (Constant c) = quote (Code.string_of_const (Proof_Context.theory_of ctxt) c) - | quote_symbol ctxt (Type_Constructor tyco) = "type " ^ quote (Proof_Context.extern_type ctxt tyco) - | quote_symbol ctxt (Type_Class class) = "class " ^ quote (Proof_Context.extern_class ctxt class) - | quote_symbol ctxt (Class_Relation (sub, super)) = - quote (Proof_Context.extern_class ctxt sub) ^ " < " ^ quote (Proof_Context.extern_class ctxt super) - | quote_symbol ctxt (Class_Instance (tyco, class)) = - quote (Proof_Context.extern_type ctxt tyco) ^ " :: " ^ quote (Proof_Context.extern_class ctxt class); +fun quote ctxt (Constant c) = Library.quote (Code.string_of_const (Proof_Context.theory_of ctxt) c) + | quote ctxt (Type_Constructor tyco) = "type " ^ Library.quote (Proof_Context.extern_type ctxt tyco) + | quote ctxt (Type_Class class) = "class " ^ Library.quote (Proof_Context.extern_class ctxt class) + | quote ctxt (Class_Relation (sub, super)) = + Library.quote (Proof_Context.extern_class ctxt sub) ^ " < " ^ Library.quote (Proof_Context.extern_class ctxt super) + | quote ctxt (Class_Instance (tyco, class)) = + Library.quote (Proof_Context.extern_type ctxt tyco) ^ " :: " ^ Library.quote (Proof_Context.extern_class ctxt class); + +fun marker (Constant c) = "CONST " ^ c + | marker (Type_Constructor tyco) = "TYPE " ^ tyco + | marker (Type_Class class) = "CLASS " ^ class + | marker (Class_Relation (sub, super)) = "CLASSREL " ^ sub ^ " < " ^ super + | marker (Class_Instance (tyco, class)) = "INSTANCE " ^ tyco ^ " :: " ^ class; fun map_attr const tyco class classrel inst module (Constant x) = Constant (const x) | map_attr const tyco class classrel inst module (Type_Constructor x) = Type_Constructor (tyco x) @@ -199,6 +212,15 @@ | lookup data (Class_Instance x) = lookup_class_instance_data data x | lookup data (Module x) = lookup_module_data data x; +fun symbols_of x = (map Constant o Symtab.keys o #constant o dest_data) x + @ (map Type_Constructor o Symtab.keys o #type_constructor o dest_data) x + @ (map Type_Class o Symtab.keys o #type_class o dest_data) x + @ (map Class_Relation o Symreltab.keys o #class_relation o dest_data) x + @ (map Class_Instance o Symreltab.keys o #class_instance o dest_data) x + @ (map Module o Symtab.keys o #module o dest_data) x; + +fun mapped_const_data f x = Symtab.map f ((#constant o dest_data) x); + fun dest_constant_data x = (Symtab.dest o #constant o dest_data) x; fun dest_type_constructor_data x = (Symtab.dest o #type_constructor o dest_data) x; fun dest_type_class_data x = (Symtab.dest o #type_class o dest_data) x; diff -r 525309c2e4ee -r bce3dbc11f95 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Sat Jan 25 23:50:49 2014 +0100 +++ b/src/Tools/Code/code_target.ML Sat Jan 25 23:50:49 2014 +0100 @@ -11,26 +11,26 @@ val read_const_exprs: theory -> string list -> string list val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list - -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit + -> Code_Thingol.program -> Code_Symbol.symbol list -> unit val produce_code_for: theory -> string -> int option -> string -> Token.T list - -> Code_Thingol.naming -> Code_Thingol.program -> string list -> (string * string) list * string option list + -> Code_Thingol.program -> Code_Symbol.symbol list -> (string * string) list * string option list val present_code_for: theory -> string -> int option -> string -> Token.T list - -> Code_Thingol.naming -> Code_Thingol.program -> string list * string list -> string + -> Code_Thingol.program -> Code_Symbol.symbol list * Code_Symbol.symbol list -> string val check_code_for: theory -> string -> bool -> Token.T list - -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit + -> Code_Thingol.program -> Code_Symbol.symbol list -> unit val export_code: theory -> string list -> (((string * string) * Path.T option) * Token.T list) list -> unit val produce_code: theory -> string list -> string -> int option -> string -> Token.T list -> (string * string) list * string option list - val present_code: theory -> string list -> (Code_Thingol.naming -> string list) + val present_code: theory -> string list -> Code_Symbol.symbol list -> string -> int option -> string -> Token.T list -> string val check_code: theory -> string list -> ((string * bool) * Token.T list) list -> unit val generatedN: string - val evaluator: theory -> string -> Code_Thingol.naming -> Code_Thingol.program - -> string list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm + val evaluator: theory -> string -> Code_Thingol.program + -> Code_Symbol.symbol list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm -> (string * string) list * string type serializer @@ -39,14 +39,14 @@ check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } } -> theory -> theory val extend_target: string * - (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program)) + (string * (Code_Thingol.program -> Code_Thingol.program)) -> theory -> theory val assert_target: theory -> string -> string val the_literals: theory -> string -> literals type serialization val parse_args: 'a parser -> Token.T list -> 'a val serialization: (int -> Path.T option -> 'a -> unit) - -> (string list -> int -> 'a -> (string * string) list * (string -> string option)) + -> (Code_Symbol.symbol list -> int -> 'a -> (string * string) list * (Code_Symbol.symbol -> string option)) -> 'a -> serialization val set_default_code_width: int -> theory -> theory @@ -117,7 +117,7 @@ (cert_class thy class, cert_tyco thy tyco); fun read_inst thy (raw_tyco, raw_class) = - (read_class thy raw_class, read_tyco thy raw_tyco); + (read_tyco thy raw_tyco, read_class thy raw_class); val parse_inst_ident = Parse.xname --| @{keyword "::"} -- Parse.class; @@ -154,21 +154,21 @@ (* serialization: abstract nonsense to cover different destinies for generated code *) -datatype destination = Export of Path.T option | Produce | Present of string list; -type serialization = int -> destination -> ((string * string) list * (string -> string option)) option; +datatype destination = Export of Path.T option | Produce | Present of Code_Symbol.symbol list; +type serialization = int -> destination -> ((string * string) list * (Code_Symbol.symbol -> string option)) option; fun serialization output _ content width (Export some_path) = (output width some_path content; NONE) | serialization _ string content width Produce = string [] width content |> SOME - | serialization _ string content width (Present stmt_names) = - string stmt_names width content + | serialization _ string content width (Present syms) = + string syms width content |> (apfst o map o apsnd) (Pretty.output (SOME width) o Pretty.str) |> SOME; fun export some_path f = (f (Export some_path); ()); fun produce f = the (f Produce); -fun present stmt_names f = space_implode "\n\n" (map snd (fst (the (f (Present stmt_names))))); +fun present syms f = space_implode "\n\n" (map snd (fst (the (f (Present syms))))); (* serializers: functions producing serializations *) @@ -176,7 +176,6 @@ type serializer = Token.T list -> Proof.context -> { - symbol_of: string -> Code_Symbol.symbol, module_name: string, reserved_syms: string list, identifiers: identifier_data, @@ -193,7 +192,7 @@ check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } } | Extension of string * - (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program); + (Code_Thingol.program -> Code_Thingol.program); (** theory data **) @@ -311,10 +310,10 @@ of SOME data => data | NONE => error ("Unknown code target language: " ^ quote target); in case the_description data - of Fundamental _ => (K I, data) + of Fundamental _ => (I, data) | Extension (super, modify) => let val (modify', data') = collapse super - in (fn naming => modify' naming #> modify naming, merge_target false target (data', data)) end + in (modify' #> modify, merge_target false target (data', data)) end end; in collapse end; @@ -326,68 +325,37 @@ val (modify, data) = collapse_hierarchy thy target; in (default_width, data, modify) end; -fun activate_const_syntax thy literals cs_data naming = - (Symtab.empty, naming) - |> fold_map (fn (c, data) => fn (tab, naming) => - case Code_Thingol.lookup_const naming c - of SOME name => let - val (syn, naming') = - Code_Printer.activate_const_syntax thy literals c data naming - in (SOME name, (Symtab.update_new (name, syn) tab, naming')) end - | NONE => (NONE, (tab, naming))) cs_data - |>> map_filter I; +fun activate_symbol_syntax thy literals printings = + (Code_Symbol.symbols_of printings, + (Symtab.lookup (Code_Symbol.mapped_const_data (Code_Printer.activate_const_syntax thy literals) printings), + Code_Symbol.lookup_type_constructor_data printings, Code_Symbol.lookup_type_class_data printings)) -fun activate_syntax lookup_name things = - Symtab.empty - |> fold_map (fn (thing_identifier, data) => fn tab => case lookup_name thing_identifier - of SOME name => (SOME name, Symtab.update_new (name, data) tab) - | NONE => (NONE, tab)) things - |>> map_filter I; - -fun activate_symbol_syntax thy literals naming printings = - let - val (names_const, (const_syntax, _)) = - activate_const_syntax thy literals (Code_Symbol.dest_constant_data printings) naming; - val (names_tyco, tyco_syntax) = - activate_syntax (Code_Thingol.lookup_tyco naming) (Code_Symbol.dest_type_constructor_data printings); - val (names_class, class_syntax) = - activate_syntax (Code_Thingol.lookup_class naming) (Code_Symbol.dest_type_class_data printings); - val names_inst = map_filter (Code_Thingol.lookup_instance naming o fst) - (Code_Symbol.dest_class_instance_data printings); - in - (names_const @ names_tyco @ names_class @ names_inst, - (Symtab.lookup const_syntax, Symtab.lookup tyco_syntax, Symtab.lookup class_syntax)) - end; - -fun project_program thy names_hidden names1 program2 = +fun project_program thy syms_hidden syms1 program2 = let val ctxt = Proof_Context.init_global thy; - val names2 = subtract (op =) names_hidden names1; - val program3 = Graph.restrict (not o member (op =) names_hidden) program2; - val names4 = Graph.all_succs program3 names2; + val syms2 = subtract (op =) syms_hidden syms1; + val program3 = Code_Symbol.Graph.restrict (not o member (op =) syms_hidden) program2; + val syms4 = Code_Symbol.Graph.all_succs program3 syms2; val unimplemented = Code_Thingol.unimplemented program3; val _ = if null unimplemented then () else error ("No code equations for " ^ commas (map (Proof_Context.extern_const ctxt) unimplemented)); - val program4 = Graph.restrict (member (op =) names4) program3; - in (names4, program4) end; + val program4 = Code_Symbol.Graph.restrict (member (op =) syms4) program3; + in (syms4, program4) end; fun prepare_serializer thy (serializer : serializer) literals reserved identifiers - printings module_name args naming proto_program names = + printings module_name args proto_program syms = let - val (names_hidden, (const_syntax, tyco_syntax, class_syntax)) = - activate_symbol_syntax thy literals naming printings; - val (names_all, program) = project_program thy names_hidden names proto_program; + val (syms_hidden, (const_syntax, tyco_syntax, class_syntax)) = + activate_symbol_syntax thy literals printings; + val (syms_all, program) = project_program thy syms_hidden syms proto_program; fun select_include (name, (content, cs)) = - if null cs orelse exists (fn c => case Code_Thingol.lookup_const naming c - of SOME name => member (op =) names_all name - | NONE => false) cs + if null cs orelse exists (fn c => member (op =) syms_all (Code_Symbol.Constant c)) cs then SOME (name, content) else NONE; val includes = map_filter select_include (Code_Symbol.dest_module_data printings); in (serializer args (Proof_Context.init_global thy) { - symbol_of = Code_Thingol.symbol_of proto_program, module_name = module_name, reserved_syms = reserved, identifiers = identifiers, @@ -398,7 +366,7 @@ program) end; -fun mount_serializer thy target some_width module_name args naming program names = +fun mount_serializer thy target some_width module_name args program syms = let val (default_width, data, modify) = activate_target thy target; val serializer = case the_description data @@ -406,15 +374,15 @@ val (prepared_serializer, prepared_program) = prepare_serializer thy serializer (the_literals thy target) (the_reserved data) (the_identifiers data) (the_printings data) - module_name args naming (modify naming program) names + module_name args (modify program) syms val width = the_default default_width some_width; in (fn program => prepared_serializer program width, prepared_program) end; -fun invoke_serializer thy target some_width module_name args naming program names = +fun invoke_serializer thy target some_width module_name args program syms = let val check = if module_name = "" then I else check_name true; val (mounted_serializer, prepared_program) = mount_serializer thy - target some_width (check module_name) args naming program names; + target some_width (check module_name) args program syms; in mounted_serializer prepared_program end; fun assert_module_name "" = error "Empty module name not allowed here" @@ -429,23 +397,23 @@ fun export_code_for thy some_path target some_width module_name args = export (using_master_directory thy some_path) - ooo invoke_serializer thy target some_width module_name args; + oo invoke_serializer thy target some_width module_name args; fun produce_code_for thy target some_width module_name args = let val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args; - in fn naming => fn program => fn names => - produce (serializer naming program names) |> apsnd (fn deresolve => map deresolve names) + in fn program => fn syms => + produce (serializer program syms) |> apsnd (fn deresolve => map deresolve syms) end; fun present_code_for thy target some_width module_name args = let val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args; - in fn naming => fn program => fn (names, selects) => - present selects (serializer naming program names) + in fn program => fn (syms, selects) => + present selects (serializer program syms) end; -fun check_code_for thy target strict args naming program names_cs = +fun check_code_for thy target strict args program syms = let val { env_var, make_destination, make_command } = (#check o the_fundamental thy) target; @@ -453,7 +421,7 @@ let val destination = make_destination p; val _ = export (SOME destination) (invoke_serializer thy target (SOME 80) - generatedN args naming program names_cs); + generatedN args program syms); val cmd = make_command generatedN; in if Isabelle_System.bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0 @@ -468,46 +436,38 @@ else Isabelle_System.with_tmp_dir "Code_Test" ext_check end; -fun evaluation mounted_serializer prepared_program consts ((vs, ty), t) = +fun evaluation mounted_serializer prepared_program syms ((vs, ty), t) = let val _ = if Code_Thingol.contains_dict_var t then error "Term to be evaluated contains free dictionaries" else (); val v' = singleton (Name.variant_list (map fst vs)) "a"; val vs' = (v', []) :: vs; - val ty' = Code_Thingol.fun_tyco `%% [ITyVar v', ty]; - val value_name = "Value.value.value" + val ty' = ITyVar v' `-> ty; val program = prepared_program - |> Graph.new_node (value_name, - Code_Thingol.Fun (@{const_name dummy_pattern}, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE))) - |> fold (curry (perhaps o try o Graph.add_edge) value_name) consts; + |> Code_Symbol.Graph.new_node (Code_Symbol.value, + Code_Thingol.Fun (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)) + |> fold (curry (perhaps o try o + Code_Symbol.Graph.add_edge) Code_Symbol.value) syms; val (program_code, deresolve) = produce (mounted_serializer program); - val value_name' = the (deresolve value_name); - in (program_code, value_name') end; + val value_name = the (deresolve Code_Symbol.value); + in (program_code, value_name) end; -fun evaluator thy target naming program consts = +fun evaluator thy target program syms = let - val (mounted_serializer, prepared_program) = mount_serializer thy - target NONE generatedN [] naming program consts; - in evaluation mounted_serializer prepared_program consts end; + val (mounted_serializer, prepared_program) = + mount_serializer thy target NONE generatedN [] program syms; + in evaluation mounted_serializer prepared_program syms end; end; (* local *) (* code generation *) -fun implemented_functions thy naming program = +fun read_const_exprs thy const_exprs = let - val cs = Code_Thingol.unimplemented 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_Thingol.read_const_exprs thy cs; - val (names2, (naming, program)) = Code_Thingol.consts_program thy true cs2; - val names3 = implemented_functions thy naming program; - val cs3 = map_filter (fn (c, name) => - if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2); + val (cs1, cs2) = Code_Thingol.read_const_exprs thy const_exprs; + val program = Code_Thingol.consts_program thy true cs2; + val cs3 = Code_Thingol.implemented_deps program; in union (op =) cs3 cs1 end; fun prep_destination "" = NONE @@ -515,9 +475,9 @@ fun export_code thy cs seris = let - val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs; + val program = Code_Thingol.consts_program thy false cs; val _ = map (fn (((target, module_name), some_path), args) => - export_code_for thy some_path target NONE module_name args naming program names_cs) seris; + export_code_for thy some_path target NONE module_name args program (map Code_Symbol.Constant cs)) seris; in () end; fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) @@ -525,19 +485,19 @@ fun produce_code thy cs target some_width some_module_name args = let - val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs; - in produce_code_for thy target some_width some_module_name args naming program names_cs end; + val program = Code_Thingol.consts_program thy false cs; + in produce_code_for thy target some_width some_module_name args program (map Code_Symbol.Constant cs) end; -fun present_code thy cs names_stmt target some_width some_module_name args = +fun present_code thy cs syms target some_width some_module_name args = let - val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs; - in present_code_for thy target some_width some_module_name args naming program (names_cs, names_stmt naming) end; + val program = Code_Thingol.consts_program thy false cs; + in present_code_for thy target some_width some_module_name args program (map Code_Symbol.Constant cs, syms) end; fun check_code thy cs seris = let - val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs; + val program = Code_Thingol.consts_program thy false cs; val _ = map (fn ((target, strict), args) => - check_code_for thy target strict args naming program names_cs) seris; + check_code_for thy target strict args program (map Code_Symbol.Constant cs)) seris; in () end; fun check_code_cmd raw_cs seris thy = check_code thy (read_const_exprs thy raw_cs) seris; @@ -547,22 +507,22 @@ val parse_const_terms = Scan.repeat1 Args.term >> (fn ts => fn thy => map (Code.check_const thy) ts); -fun parse_names category parse internalize lookup = +fun parse_names category parse internalize mark_symbol = Scan.lift (Args.parens (Args.$$$ category)) |-- Scan.repeat1 parse - >> (fn xs => fn thy => fn naming => map_filter (lookup naming o internalize thy) xs); + >> (fn xs => fn thy => map (mark_symbol o internalize thy) xs); val parse_consts = parse_names "consts" Args.term - Code.check_const Code_Thingol.lookup_const; + Code.check_const Code_Symbol.Constant; val parse_types = parse_names "types" (Scan.lift Args.name) - Sign.intern_type Code_Thingol.lookup_tyco; + Sign.intern_type Code_Symbol.Type_Constructor; val parse_classes = parse_names "classes" (Scan.lift Args.name) - Sign.intern_class Code_Thingol.lookup_class; + Sign.intern_class Code_Symbol.Type_Class; val parse_instances = parse_names "instances" (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name)) - (fn thy => fn (raw_tyco, raw_class) => (Sign.intern_class thy raw_class, Sign.intern_type thy raw_tyco)) - Code_Thingol.lookup_instance; + (fn thy => fn (raw_tyco, raw_class) => (Sign.intern_class thy raw_tyco, Sign.intern_type thy raw_class)) + Code_Symbol.Class_Instance; in @@ -574,7 +534,7 @@ (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target, some_width)) => let val thy = Proof_Context.theory_of ctxt in present_code thy (mk_cs thy) - (fn naming => maps (fn f => f thy naming) mk_stmtss) + (maps (fn f => f thy) mk_stmtss) target some_width "Example" [] end); diff -r 525309c2e4ee -r bce3dbc11f95 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Sat Jan 25 23:50:49 2014 +0100 +++ b/src/Tools/Code/code_thingol.ML Sat Jan 25 23:50:49 2014 +0100 @@ -8,6 +8,7 @@ infix 8 `%%; infix 4 `$; infix 4 `$$; +infixr 3 `->; infixr 3 `|=>; infixr 3 `|==>; @@ -15,14 +16,14 @@ sig type vname = string; datatype dict = - Dict of string list * plain_dict + Dict of (class * class) list * plain_dict and plain_dict = - Dict_Const of string * dict list list + Dict_Const of (string * class) * dict list list | Dict_Var of vname * (int * int); datatype itype = `%% of string * itype list | ITyVar of vname; - type const = { name: string, typargs: itype list, dicts: dict list list, + type const = { sym: Code_Symbol.symbol, typargs: itype list, dicts: dict list list, dom: itype list, range: itype, annotate: bool }; datatype iterm = IConst of const @@ -30,6 +31,7 @@ | `$ of iterm * iterm | `|=> of (vname option * itype) * iterm | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm }; + val `-> : itype * itype -> itype; val `$$ : iterm * iterm list -> iterm; val `|==> : (vname option * itype) list * iterm -> iterm; type typscheme = (vname * sort) list * itype; @@ -38,7 +40,6 @@ signature CODE_THINGOL = sig include BASIC_CODE_THINGOL - val fun_tyco: string 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 @@ -54,59 +55,50 @@ val is_IAbs: iterm -> bool val eta_expand: int -> const * iterm list -> iterm val contains_dict_var: iterm -> bool - val add_constnames: iterm -> string list -> string list + val add_constsyms: iterm -> Code_Symbol.symbol list -> Code_Symbol.symbol list val add_tyconames: iterm -> string list -> string list val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a - type naming - val empty_naming: 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 - val ensure_declared_const: theory -> string -> naming -> string * naming - datatype stmt = - NoStmt of string - | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option) - | Datatype of string * (vname list * - ((string * vname list (*type argument wrt. canonical order*)) * itype list) list) - | Datatypecons of string * string - | Class of class * (vname * ((class * string) list * (string * itype) list)) + NoStmt + | Fun of (typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option + | Datatype of vname list * + ((string * vname list (*type argument wrt. canonical order*)) * itype list) list + | Datatypecons of string + | Class of vname * ((class * class) list * (string * itype) list) | Classrel of class * class - | Classparam of string * class + | Classparam of class | Classinst of { class: string, tyco: string, vs: (vname * sort) list, - superinsts: (class * (string * (string * dict list list))) list, + superinsts: (class * dict list list) list, inst_params: ((string * (const * int)) * (thm * bool)) list, superinst_params: ((string * (const * int)) * (thm * bool)) list }; - type program = stmt Graph.T + type program = stmt Code_Symbol.Graph.T val unimplemented: program -> string list + val implemented_deps: program -> string list val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt - val is_constr: program -> string -> bool + val is_constr: program -> Code_Symbol.symbol -> bool val is_case: stmt -> bool - val symbol_of: program -> string -> Code_Symbol.symbol; val group_stmts: theory -> program - -> ((string * stmt) list * (string * stmt) list - * ((string * stmt) list * (string * stmt) list)) list + -> ((Code_Symbol.symbol * stmt) list * (Code_Symbol.symbol * stmt) list + * ((Code_Symbol.symbol * stmt) list * (Code_Symbol.symbol * stmt) list)) list val read_const_exprs: theory -> string list -> string list * string list - val consts_program: theory -> bool -> string list -> string list * (naming * program) - val dynamic_conv: theory -> (naming -> program - -> ((string * sort) list * typscheme) * iterm -> string list -> conv) + val consts_program: theory -> bool -> string list -> program + val dynamic_conv: theory -> (program + -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.symbol list -> conv) -> conv - val dynamic_value: theory -> ((term -> term) -> 'a -> 'a) -> (naming -> program - -> ((string * sort) list * typscheme) * iterm -> string list -> 'a) + val dynamic_value: theory -> ((term -> term) -> 'a -> 'a) -> (program + -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.symbol list -> 'a) -> term -> 'a - val static_conv: theory -> string list -> (naming -> program -> string list - -> ((string * sort) list * typscheme) * iterm -> string list -> conv) + val static_conv: theory -> string list -> (program -> string list + -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.symbol list -> conv) -> conv val static_conv_simple: theory -> string list -> (program -> (string * sort) list -> term -> conv) -> conv val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list -> - (naming -> program -> string list - -> ((string * sort) list * typscheme) * iterm -> string list -> 'a) + (program -> string list + -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.symbol list -> 'a) -> term -> 'a end; @@ -133,16 +125,29 @@ type vname = string; datatype dict = - Dict of string list * plain_dict + Dict of (class * class) list * plain_dict and plain_dict = - Dict_Const of string * dict list list + Dict_Const of (string * class) * dict list list | Dict_Var of vname * (int * int); datatype itype = `%% of string * itype list | ITyVar of vname; -type const = { name: string, typargs: itype list, dicts: dict list list, +fun ty1 `-> ty2 = "fun" `%% [ty1, ty2]; + +val unfold_fun = unfoldr + (fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2) + | _ => NONE); + +fun unfold_fun_n n ty = + let + val (tys1, ty1) = unfold_fun ty; + val (tys3, tys2) = chop n tys1; + val ty3 = Library.foldr (op `->) (tys2, ty1); + in (tys3, ty3) end; + +type const = { sym: Code_Symbol.symbol, typargs: itype list, dicts: dict list list, dom: itype list, range: itype, annotate: bool }; datatype iterm = @@ -191,7 +196,7 @@ #> fold (fn (p, body) => fold' p #> fold' body) clauses in fold' end; -val add_constnames = fold_constexprs (fn { name = c, ... } => insert (op =) c); +val add_constsyms = fold_constexprs (fn { sym, ... } => insert (op =) sym); fun add_tycos (tyco `%% tys) = insert (op =) tyco #> fold add_tycos tys | add_tycos (ITyVar _) = I; @@ -238,15 +243,15 @@ val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys); in (vs_tys, t `$$ map (IVar o fst) vs_tys) end; -fun eta_expand k (const as { name = c, dom = tys, ... }, ts) = +fun eta_expand k (const as { dom = tys, ... }, ts) = let val j = length ts; val l = k - j; val _ = if l > length tys - then error ("Impossible eta-expansion for constant " ^ quote c) else (); - val ctxt = (fold o fold_varnames) Name.declare ts Name.context; + then error "Impossible eta-expansion" else (); + val vars = (fold o fold_varnames) Name.declare ts Name.context; val vs_tys = (map o apfst) SOME - (Name.invent_names ctxt "a" ((take l o drop j) tys)); + (Name.invent_names vars "a" ((take l o drop j) tys)); in vs_tys `|==> IConst const `$$ ts @ map (IVar o fst) vs_tys end; fun contains_dict_var t = @@ -262,178 +267,31 @@ in cont_term t end; -(** namings **) - -(* policies *) - -local - fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy); - fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy); - fun thyname_of_instance thy inst = case Axclass.thynames_of_arity thy (swap inst) - of [] => error ("No such instance: " ^ quote (snd inst ^ " :: " ^ fst inst)) - | thyname :: _ => thyname; - fun thyname_of_const thy c = case Axclass.class_of_param thy c - of SOME class => thyname_of_class thy class - | NONE => (case Code.get_type_of_constr_or_abstr thy c - of SOME (tyco, _) => thyname_of_type thy tyco - | NONE => #theory_name (Name_Space.the_entry (Sign.const_space thy) c)); - fun namify thy get_basename get_thyname name = - let - val prefix = get_thyname thy name; - val base = (Name.desymbolize false o get_basename) name; - in Long_Name.append prefix base end; -in - -fun namify_class thy = namify thy Long_Name.base_name thyname_of_class; -fun namify_classrel thy = namify thy (fn (sub_class, super_class) => - Long_Name.base_name super_class ^ "_" ^ Long_Name.base_name sub_class) - (fn thy => thyname_of_class thy o fst); - (*order fits nicely with composed projections*) -fun namify_tyco thy "fun" = "Pure.fun" - | namify_tyco thy tyco = namify thy Long_Name.base_name thyname_of_type tyco; -fun namify_instance thy = namify thy (fn (class, tyco) => - Long_Name.base_name class ^ "_" ^ Long_Name.base_name tyco) thyname_of_instance; -fun namify_const thy "==>" = "Pure.follows" - | namify_const thy "==" = "Pure.meta_eq" - | namify_const thy c = namify thy Long_Name.base_name thyname_of_const c; - -end; (* local *) - - -(* data *) - -datatype naming = Naming of { - class: class Symtab.table * Name.context, - classrel: string Symreltab.table * Name.context, - tyco: string Symtab.table * Name.context, - instance: string Symreltab.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 = (Symreltab.empty, Name.context), - tyco = (Symtab.empty, Name.context), - instance = (Symreltab.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') = Name.variant 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)); - - -(* lookup and declare *) - -local - -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 (Long_Name.append name nsp); - -in - -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 Symreltab.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 Symreltab.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 Symreltab.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 Symreltab.update_new namify_instance; -fun declare_const thy = declare thy map_const - lookup_const Symtab.update_new namify_const; - -fun ensure_declared_const thy const naming = - case lookup_const naming const - of SOME const' => (const', naming) - | NONE => declare_const thy const naming; - -val fun_tyco = Long_Name.append (namify_tyco Pure.thy "fun") suffix_tyco - (*depends on add_suffix*); - -val unfold_fun = unfoldr - (fn tyco `%% [ty1, ty2] => if tyco = fun_tyco then SOME (ty1, ty2) else NONE - | _ => NONE); - -fun unfold_fun_n n ty = - let - val (tys1, ty1) = unfold_fun ty; - val (tys3, tys2) = chop n tys1; - val ty3 = Library.foldr (fn (ty1, ty2) => fun_tyco `%% [ty1, ty2]) (tys2, ty1); - in (tys3, ty3) end; - -end; (* local *) - - (** statements, abstract programs **) type typscheme = (vname * sort) list * itype; datatype stmt = - NoStmt of string - | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option) - | Datatype of string * (vname list * ((string * vname list) * itype list) list) - | Datatypecons of string * string - | Class of class * (vname * ((class * string) list * (string * itype) list)) + NoStmt + | Fun of (typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option + | Datatype of vname list * ((string * vname list) * itype list) list + | Datatypecons of string + | Class of vname * ((class * class) list * (string * itype) list) | Classrel of class * class - | Classparam of string * class + | Classparam of class | Classinst of { class: string, tyco: string, vs: (vname * sort) list, - superinsts: (class * (string * (string * dict list list))) list, + superinsts: (class * dict list list) list, inst_params: ((string * (const * int)) * (thm * bool)) list, superinst_params: ((string * (const * int)) * (thm * bool)) list }; -type program = stmt Graph.T; +type program = stmt Code_Symbol.Graph.T; fun unimplemented program = - Graph.fold (fn (_, (NoStmt c, _)) => cons c | _ => I) program []; + Code_Symbol.Graph.fold (fn (Code_Symbol.Constant c, (NoStmt, _)) => cons c | _ => I) program []; + +fun implemented_deps program = + Code_Symbol.Graph.keys program + |> subtract (op =) (Code_Symbol.Graph.all_preds program (map Code_Symbol.Constant (unimplemented program))) + |> map_filter (fn Code_Symbol.Constant c => SOME c | _ => NONE); fun map_terms_bottom_up f (t as IConst _) = f t | map_terms_bottom_up f (t as IVar _) = f t @@ -449,9 +307,9 @@ fun map_classparam_instances_as_term f = (map o apfst o apsnd o apfst) (fn const => case f (IConst const) of IConst const' => const') -fun map_terms_stmt f (NoStmt c) = (NoStmt c) - | map_terms_stmt f (Fun (c, ((tysm, eqs), case_cong))) = Fun (c, ((tysm, (map o apfst) - (fn (ts, t) => (map f ts, f t)) eqs), case_cong)) +fun map_terms_stmt f NoStmt = NoStmt + | map_terms_stmt f (Fun ((tysm, eqs), case_cong)) = Fun ((tysm, (map o apfst) + (fn (ts, t) => (map f ts, f t)) eqs), case_cong) | map_terms_stmt f (stmt as Datatype _) = stmt | map_terms_stmt f (stmt as Datatypecons _) = stmt | map_terms_stmt f (stmt as Class _) = stmt @@ -463,41 +321,16 @@ inst_params = map_classparam_instances_as_term f inst_params, superinst_params = map_classparam_instances_as_term f superinst_params }; -fun is_constr program name = case Graph.get_node program name +fun is_constr program sym = case Code_Symbol.Graph.get_node program sym of Datatypecons _ => true | _ => false; -fun is_case (Fun (_, (_, SOME _))) = true +fun is_case (Fun (_, SOME _)) = true | is_case _ = false; -fun symbol_of program name = - case try (Graph.get_node program) name of - NONE => Code_Symbol.Module "(unknown)" - (*FIXME: need to be liberal due to ad-hoc introduction of value for evaluation*) - | SOME stmt => case stmt of - Fun (c, _) => Code_Symbol.Constant c - | Datatype (tyco, _) => Code_Symbol.Type_Constructor tyco - | Datatypecons (c, _) => Code_Symbol.Constant c - | Class (class, _) => Code_Symbol.Type_Class class - | Classrel (sub, super) => - let - val Class (sub, _) = Graph.get_node program sub; - val Class (super, _) = Graph.get_node program super; - in - Code_Symbol.Class_Relation (sub, super) - end - | Classparam (c, _) => Code_Symbol.Constant c - | Classinst { class, tyco, ... } => - let - val Class (class, _) = Graph.get_node program class; - val Datatype (tyco, _) = Graph.get_node program tyco; - in - Code_Symbol.Class_Instance (tyco, class) - end; - fun linear_stmts program = - rev (Graph.strong_conn program) - |> map (AList.make (Graph.get_node program)); + rev (Code_Symbol.Graph.strong_conn program) + |> map (AList.make (Code_Symbol.Graph.get_node program)); fun group_stmts thy program = let @@ -516,8 +349,8 @@ else if forall (is_fun orf is_classinst) stmts then ([], [], List.partition is_fun stmts) else error ("Illegal mutual dependencies: " ^ (commas - o map (Code_Symbol.quote_symbol (Proof_Context.init_global thy) - o symbol_of program o fst)) stmts); + o map (Code_Symbol.quote (Proof_Context.init_global thy) + o fst)) stmts); in linear_stmts program |> map group @@ -528,31 +361,27 @@ (* generic mechanisms *) -fun ensure_stmt lookup declare generate thing (dep, (naming, program)) = +fun ensure_stmt symbolize generate x (dep, program) = let - fun add_dep name = case dep of NONE => I - | SOME dep => Graph.add_edge (dep, name); - val (name, naming') = case lookup naming thing - of SOME name => (name, naming) - | NONE => declare thing naming; + val sym = symbolize x; + val add_dep = case dep of NONE => I + | SOME dep => Code_Symbol.Graph.add_edge (dep, sym); in - if can (Graph.get_node program) name + if can (Code_Symbol.Graph.get_node program) sym then program - |> add_dep name - |> pair naming' + |> add_dep |> pair dep - |> pair name + |> pair x else program - |> Graph.default_node (name, NoStmt "") - |> add_dep name - |> pair naming' - |> curry generate (SOME name) + |> Code_Symbol.Graph.default_node (sym, NoStmt) + |> add_dep + |> curry generate (SOME sym) ||> snd - |-> (fn stmt => (apsnd o Graph.map_node name) (K stmt)) + |-> (fn stmt => (Code_Symbol.Graph.map_node sym) (K stmt)) |> pair dep - |> pair name + |> pair x end; exception PERMISSIVE of unit; @@ -582,10 +411,6 @@ (err_typ ^ "\n" ^ err_class) end; -fun undefineds thy (dep, (naming, program)) = - (map_filter (lookup_const naming) (Code.undefineds thy), - (dep, (naming, program))); - (* inference of type annotations for disambiguation with type classes *) @@ -640,18 +465,18 @@ ensure_const thy algbr eqngr permissive c ##>> pair (map (unprefix "'" o fst) vs) ##>> fold_map (translate_typ thy algbr eqngr permissive) tys) cos - #>> (fn info => Datatype (tyco, info)); - in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end + #>> Datatype; + in ensure_stmt Code_Symbol.Type_Constructor stmt_datatype tyco end and ensure_const thy algbr eqngr permissive c = let fun stmt_datatypecons tyco = ensure_tyco thy algbr eqngr permissive tyco - #>> (fn tyco => Datatypecons (c, tyco)); + #>> Datatypecons; fun stmt_classparam class = ensure_class thy algbr eqngr permissive class - #>> (fn class => Classparam (c, class)); + #>> Classparam; fun stmt_fun cert = case Code.equations_of_cert thy cert - of (_, NONE) => pair (NoStmt c) + of (_, NONE) => pair NoStmt | ((vs, ty), SOME eqns) => let val eqns' = annotate_eqns thy algbr eqngr (c, ty) eqns @@ -661,34 +486,34 @@ ##>> translate_typ thy algbr eqngr permissive ty ##>> translate_eqns thy algbr eqngr permissive eqns' #>> - (fn (_, NONE) => NoStmt c - | (tyscm, SOME eqns) => Fun (c, ((tyscm, eqns), some_case_cong))) + (fn (_, NONE) => NoStmt + | (tyscm, SOME eqns) => Fun ((tyscm, eqns), some_case_cong)) end; val stmt_const = case Code.get_type_of_constr_or_abstr 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 (Code_Preproc.cert eqngr c)) - in ensure_stmt lookup_const (declare_const thy) stmt_const c end + in ensure_stmt Code_Symbol.Constant stmt_const c end and ensure_class thy (algbr as (_, algebra)) eqngr permissive class = let val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class; val cs = #params (Axclass.get_info thy class); val stmt_class = - fold_map (fn super_class => ensure_class thy algbr eqngr permissive super_class - ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)) super_classes + fold_map (fn super_class => + ensure_classrel thy algbr eqngr permissive (class, super_class)) super_classes ##>> fold_map (fn (c, ty) => ensure_const thy algbr eqngr permissive c ##>> translate_typ thy algbr eqngr permissive ty) cs - #>> (fn info => Class (class, (unprefix "'" Name.aT, info))) - in ensure_stmt lookup_class (declare_class thy) stmt_class class end + #>> (fn info => Class (unprefix "'" Name.aT, info)) + in ensure_stmt Code_Symbol.Type_Class stmt_class class end and ensure_classrel thy algbr eqngr permissive (sub_class, super_class) = let val stmt_classrel = ensure_class thy algbr eqngr permissive sub_class ##>> ensure_class thy algbr eqngr permissive super_class #>> Classrel; - in ensure_stmt lookup_classrel (declare_classrel thy) stmt_classrel (sub_class, super_class) end -and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (class, tyco) = + in ensure_stmt Code_Symbol.Class_Relation stmt_classrel (sub_class, super_class) end +and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (tyco, class) = let val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class; val these_class_params = these o try (#params o Axclass.get_info thy); @@ -703,10 +528,8 @@ val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs'); fun translate_super_instance super_class = ensure_class thy algbr eqngr permissive super_class - ##>> ensure_classrel thy algbr eqngr permissive (class, super_class) ##>> translate_dicts thy algbr eqngr permissive NONE (arity_typ, [super_class]) - #>> (fn ((super_class, classrel), [Dict ([], Dict_Const (inst, dss))]) => - (super_class, (classrel, (inst, dss)))); + #>> (fn (super_class, [Dict ([], Dict_Const (_, dss))]) => (super_class, dss)); fun translate_classparam_instance (c, ty) = let val raw_const = Const (c, map_type_tfree (K arity_typ') ty); @@ -729,7 +552,7 @@ #>> (fn (((((class, tyco), vs), superinsts), inst_params), superinst_params) => Classinst { class = class, tyco = tyco, vs = vs, superinsts = superinsts, inst_params = inst_params, superinst_params = superinst_params }); - in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end + in ensure_stmt Code_Symbol.Class_Instance stmt_inst (tyco, class) end and translate_typ thy algbr eqngr permissive (TFree (v, _)) = pair (ITyVar (unprefix "'" v)) | translate_typ thy algbr eqngr permissive (Type (tyco, tys)) = @@ -781,7 +604,7 @@ ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (typargs ~~ sorts) ##>> fold_map (translate_typ thy algbr eqngr permissive) (range :: dom) #>> (fn (((c, typargs), dss), range :: dom) => - IConst { name = c, typargs = typargs, dicts = dss, + IConst { sym = Code_Symbol.Constant c, typargs = typargs, dicts = dss, dom = dom, range = range, annotate = annotate }) end and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) = @@ -790,6 +613,7 @@ #>> (fn (t, ts) => t `$$ ts) and translate_case thy algbr eqngr permissive some_thm (num_args, (t_pos, case_pats)) (c_ty, ts) = let + val undefineds = Code.undefineds thy; fun arg_types num_args ty = fst (chop num_args (binder_types ty)); val tys = arg_types num_args (snd c_ty); val ty = nth tys t_pos; @@ -801,11 +625,11 @@ val constrs = if null case_pats then [] else map_filter I (map2 mk_constr case_pats (nth_drop t_pos ts)); - fun casify undefineds constrs ty t_app ts = + fun casify constrs ty t_app ts = let fun collapse_clause vs_map ts body = case body - of IConst { name = c, ... } => if member (op =) undefineds c + of IConst { sym = Code_Symbol.Constant c, ... } => if member (op =) undefineds c then [] else [(ts, body)] | ICase { term = IVar (SOME v), clauses = clauses, ... } => @@ -839,9 +663,8 @@ #>> rpair n) constrs ##>> translate_typ thy algbr eqngr permissive ty ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts - ##>> undefineds thy - #>> (fn ((((t, constrs), ty), ts), undefineds) => - casify undefineds constrs ty t ts) + #>> (fn (((t, constrs), ty), ts) => + casify constrs ty t ts) end and translate_app_case thy algbr eqngr permissive some_thm (case_scheme as (num_args, _)) ((c, ty), ts) = if length ts < num_args then @@ -873,12 +696,12 @@ datatype typarg_witness = Weakening of (class * class) list * plain_typarg_witness and plain_typarg_witness = - Global of (class * string) * typarg_witness list list + Global of (string * class) * typarg_witness list list | Local of string * (int * sort); fun class_relation ((Weakening (classrels, x)), sub_class) super_class = Weakening ((sub_class, super_class) :: classrels, x); fun type_constructor (tyco, _) dss class = - Weakening ([], Global ((class, tyco), (map o map) fst dss)); + Weakening ([], Global ((tyco, class), (map o map) fst dss)); fun type_variable (TFree (v, sort)) = let val sort' = proj_sort sort; @@ -905,31 +728,33 @@ structure Program = Code_Data ( - type T = naming * program; - val empty = (empty_naming, Graph.empty); + type T = program; + val empty = Code_Symbol.Graph.empty; ); fun invoke_generation ignore_cache thy (algebra, eqngr) generate thing = Program.change_yield (if ignore_cache then NONE else SOME thy) - (fn naming_program => (NONE, naming_program) + (fn program => (NONE, program) |> generate thy algebra eqngr thing - |-> (fn thing => fn (_, naming_program) => (thing, naming_program))); + |-> (fn thing => fn (_, program) => (thing, program))); (* program generation *) fun consts_program thy permissive consts = let - fun project_consts consts (naming, program) = - if permissive then (consts, (naming, program)) - else (consts, (naming, Graph.restrict - (member (op =) (Graph.all_succs program consts)) program)); + fun project program = + if permissive then program + else Code_Symbol.Graph.restrict + (member (op =) (Code_Symbol.Graph.all_succs program + (map Code_Symbol.Constant consts))) program; fun generate_consts thy algebra eqngr = fold_map (ensure_const thy algebra eqngr permissive); in invoke_generation permissive thy (Code_Preproc.obtain false thy consts []) generate_consts consts - |-> project_consts + |> snd + |> project end; @@ -941,23 +766,24 @@ val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =) o dest_TFree))) t []; val t' = annotate thy algbr eqngr (@{const_name dummy_pattern}, ty) [] t; + val dummy_constant = Code_Symbol.Constant @{const_name dummy_pattern}; val stmt_value = fold_map (translate_tyvar_sort thy algbr eqngr false) vs ##>> translate_typ thy algbr eqngr false ty ##>> translate_term thy algbr eqngr false NONE (t', NONE) #>> (fn ((vs, ty), t) => Fun - (@{const_name dummy_pattern}, (((vs, ty), [(([], t), (NONE, true))]), NONE))); - fun term_value (dep, (naming, program1)) = + (((vs, ty), [(([], t), (NONE, true))]), NONE)); + fun term_value (dep, program1) = let - val Fun (_, ((vs_ty, [(([], t), _)]), _)) = - Graph.get_node program1 @{const_name dummy_pattern}; - val deps = Graph.immediate_succs program1 @{const_name dummy_pattern}; - val program2 = Graph.del_node @{const_name dummy_pattern} program1; - val deps_all = Graph.all_succs program2 deps; - val program3 = Graph.restrict (member (op =) deps_all) program2; - in (((naming, program3), ((vs_ty, t), deps)), (dep, (naming, program2))) end; + val Fun ((vs_ty, [(([], t), _)]), _) = + Code_Symbol.Graph.get_node program1 dummy_constant; + val deps = Code_Symbol.Graph.immediate_succs program1 dummy_constant; + val program2 = Code_Symbol.Graph.del_node dummy_constant program1; + val deps_all = Code_Symbol.Graph.all_succs program2 deps; + val program3 = Code_Symbol.Graph.restrict (member (op =) deps_all) program2; + in ((program3, ((vs_ty, t), deps)), (dep, program2)) end; in - ensure_stmt ((K o K) NONE) pair stmt_value @{const_name dummy_pattern} + ensure_stmt Code_Symbol.Constant stmt_value @{const_name dummy_pattern} #> snd #> term_value end; @@ -967,9 +793,9 @@ fun dynamic_evaluator thy evaluator algebra eqngr vs t = let - val (((naming, program), (((vs', ty'), t'), deps)), _) = + val ((program, (((vs', ty'), t'), deps)), _) = invoke_generation false thy (algebra, eqngr) ensure_value t; - in evaluator naming program ((original_sorts vs vs', (vs', ty')), t') deps end; + in evaluator program ((original_sorts vs vs', (vs', ty')), t') deps end; fun dynamic_conv thy evaluator = Code_Preproc.dynamic_conv thy (dynamic_evaluator thy evaluator); @@ -977,26 +803,26 @@ fun dynamic_value thy postproc evaluator = Code_Preproc.dynamic_value thy postproc (dynamic_evaluator thy evaluator); -fun lift_evaluation thy evaluation' algebra eqngr naming program vs t = +fun lift_evaluation thy evaluation' algebra eqngr program vs t = let - val (((_, _), (((vs', ty'), t'), deps)), _) = - ensure_value thy algebra eqngr t (NONE, (naming, program)); + val ((_, (((vs', ty'), t'), deps)), _) = + ensure_value thy algebra eqngr t (NONE, program); in evaluation' ((original_sorts vs vs', (vs', ty')), t') deps end; fun lift_evaluator thy evaluator' consts algebra eqngr = let fun generate_consts thy algebra eqngr = fold_map (ensure_const thy algebra eqngr false); - val (consts', (naming, program)) = + val (consts', program) = invoke_generation true thy (algebra, eqngr) generate_consts consts; - val evaluation' = evaluator' naming program consts'; - in lift_evaluation thy evaluation' algebra eqngr naming program end; + val evaluation' = evaluator' program consts'; + in lift_evaluation thy evaluation' algebra eqngr program end; fun lift_evaluator_simple thy evaluator' consts algebra eqngr = let fun generate_consts thy algebra eqngr = fold_map (ensure_const thy algebra eqngr false); - val (_, (_, program)) = + val (_, program) = invoke_generation true thy (algebra, eqngr) generate_consts consts; in evaluator' program end; diff -r 525309c2e4ee -r bce3dbc11f95 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Sat Jan 25 23:50:49 2014 +0100 +++ b/src/Tools/nbe.ML Sat Jan 25 23:50:49 2014 +0100 @@ -249,11 +249,11 @@ val univs_cookie = (Univs.get, put_result, name_put); -val sloppy_name = Long_Name.base_name o Long_Name.qualifier +val sloppy_name = Code_Symbol.base_name; -fun nbe_fun idx_of 0 "" = "nbe_value" - | nbe_fun idx_of i c = "c_" ^ string_of_int (idx_of c) - ^ "_" ^ sloppy_name c ^ "_" ^ string_of_int i; +fun nbe_fun idx_of 0 (Code_Symbol.Constant "") = "nbe_value" + | nbe_fun idx_of i sym = "c_" ^ string_of_int (idx_of sym) + ^ "_" ^ sloppy_name sym ^ "_" ^ string_of_int i; fun nbe_dict v n = "d_" ^ v ^ "_" ^ string_of_int n; fun nbe_bound v = "v_" ^ v; fun nbe_bound_optional NONE = "_" @@ -291,24 +291,24 @@ in (c, (num_args, (dicts, eqns))) end; val eqnss' = map prep_eqns eqnss; - fun assemble_constapp c dss ts = + fun assemble_constapp sym dss ts = let val ts' = (maps o map) assemble_dict dss @ ts; - in case AList.lookup (op =) eqnss' c + in case AList.lookup (op =) eqnss' sym of SOME (num_args, _) => if num_args <= length ts' then let val (ts1, ts2) = chop num_args ts' - in nbe_apps (nbe_apps_local idx_of 0 c ts1) ts2 - end else nbe_apps (nbe_abss num_args (nbe_fun idx_of 0 c)) ts' - | NONE => if member (op =) deps c - then nbe_apps (nbe_fun idx_of 0 c) ts' - else nbe_apps_constr idx_of c ts' + in nbe_apps (nbe_apps_local idx_of 0 sym ts1) ts2 + end else nbe_apps (nbe_abss num_args (nbe_fun idx_of 0 sym)) ts' + | NONE => if member (op =) deps sym + then nbe_apps (nbe_fun idx_of 0 sym) ts' + else nbe_apps_constr idx_of sym ts' end and assemble_classrels classrels = - fold_rev (fn classrel => assemble_constapp classrel [] o single) classrels + fold_rev (fn classrel => assemble_constapp (Code_Symbol.Class_Relation classrel) [] o single) classrels and assemble_dict (Dict (classrels, x)) = assemble_classrels classrels (assemble_plain_dict x) and assemble_plain_dict (Dict_Const (inst, dss)) = - assemble_constapp inst dss [] + assemble_constapp (Code_Symbol.Class_Instance inst) dss [] | assemble_plain_dict (Dict_Var (v, (n, _))) = nbe_dict v n @@ -318,7 +318,7 @@ let val (t', ts) = Code_Thingol.unfold_app t in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end - and of_iapp match_cont (IConst { name = c, dicts = dss, ... }) ts = constapp c dss ts + and of_iapp match_cont (IConst { sym, dicts = dss, ... }) ts = constapp sym dss ts | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts | of_iapp match_cont ((v, _) `|=> t) ts = nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts @@ -353,12 +353,12 @@ val (args', _) = fold_map subst_vars args samepairs; in (samepairs, args') end; - fun assemble_eqn c dicts default_args (i, (args, rhs)) = + fun assemble_eqn sym dicts default_args (i, (args, rhs)) = let - val match_cont = if c = "" then NONE - else SOME (nbe_apps_local idx_of (i + 1) c (dicts @ default_args)); + val match_cont = if Code_Symbol.is_value sym then NONE + else SOME (nbe_apps_local idx_of (i + 1) sym (dicts @ default_args)); val assemble_arg = assemble_iterm - (fn c => fn dss => fn ts => nbe_apps_constr idx_of c ((maps o map) (K "_") dss @ ts)) NONE; + (fn sym' => fn dss => fn ts => nbe_apps_constr idx_of sym' ((maps o map) (K "_") dss @ ts)) NONE; val assemble_rhs = assemble_iterm assemble_constapp match_cont; val (samepairs, args') = subst_nonlin_vars args; val s_args = map assemble_arg args'; @@ -370,17 +370,17 @@ | SOME default_rhs => [([ml_list (rev (dicts @ map2 ml_as default_args s_args))], s_rhs), ([ml_list (rev (dicts @ default_args))], default_rhs)] - in (nbe_fun idx_of i c, eqns) end; + in (nbe_fun idx_of i sym, eqns) end; - fun assemble_eqns (c, (num_args, (dicts, eqns))) = + fun assemble_eqns (sym, (num_args, (dicts, eqns))) = let val default_args = map nbe_default (Name.invent Name.context "a" (num_args - length dicts)); - val eqns' = map_index (assemble_eqn c dicts default_args) eqns - @ (if c = "" then [] else [(nbe_fun idx_of (length eqns) c, + val eqns' = map_index (assemble_eqn sym dicts default_args) eqns + @ (if Code_Symbol.is_value sym then [] else [(nbe_fun idx_of (length eqns) sym, [([ml_list (rev (dicts @ default_args))], - nbe_apps_constr idx_of c (dicts @ default_args))])]); - in (eqns', nbe_abss num_args (nbe_fun idx_of 0 c)) end; + nbe_apps_constr idx_of sym (dicts @ default_args))])]); + in (eqns', nbe_abss num_args (nbe_fun idx_of 0 sym)) end; val (fun_vars, fun_vals) = map_split assemble_eqns eqnss'; val deps_vars = ml_list (map (nbe_fun idx_of 0) deps); @@ -394,9 +394,9 @@ let val ctxt = Proof_Context.init_global thy; val (deps, deps_vals) = split_list (map_filter - (fn dep => Option.map (fn univ => (dep, univ)) (fst ((Graph.get_node nbe_program dep)))) raw_deps); + (fn dep => Option.map (fn univ => (dep, univ)) (fst ((Code_Symbol.Graph.get_node nbe_program dep)))) raw_deps); val idx_of = raw_deps - |> map (fn dep => (dep, snd (Graph.get_node nbe_program dep))) + |> map (fn dep => (dep, snd (Code_Symbol.Graph.get_node nbe_program dep))) |> AList.lookup (op =) |> (fn f => the o f); val s = assemble_eqnss idx_of deps eqnss; @@ -413,45 +413,45 @@ (* extract equations from statements *) -fun dummy_const c dss = - IConst { name = c, typargs = [], dicts = dss, +fun dummy_const sym dss = + IConst { sym = sym, typargs = [], dicts = dss, dom = [], range = ITyVar "", annotate = false }; -fun eqns_of_stmt (_, Code_Thingol.NoStmt _) = +fun eqns_of_stmt (_, Code_Thingol.NoStmt) = [] - | eqns_of_stmt (_, Code_Thingol.Fun (_, ((_, []), _))) = + | eqns_of_stmt (_, Code_Thingol.Fun ((_, []), _)) = [] - | eqns_of_stmt (const, Code_Thingol.Fun (_, (((vs, _), eqns), _))) = - [(const, (vs, map fst eqns))] + | eqns_of_stmt (sym_const, Code_Thingol.Fun (((vs, _), eqns), _)) = + [(sym_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, (super_classes, classparams)))) = + | eqns_of_stmt (sym_class, Code_Thingol.Class (v, (classrels, classparams))) = let - val names = map snd super_classes @ map fst classparams; - val params = Name.invent Name.context "d" (length names); - fun mk (k, name) = - (name, ([(v, [])], - [([dummy_const class [] `$$ map (IVar o SOME) params], + val syms = map Code_Symbol.Class_Relation classrels @ map (Code_Symbol.Constant o fst) classparams; + val params = Name.invent Name.context "d" (length syms); + fun mk (k, sym) = + (sym, ([(v, [])], + [([dummy_const sym_class [] `$$ map (IVar o SOME) params], IVar (SOME (nth params k)))])); - in map_index mk names end + in map_index mk syms end | eqns_of_stmt (_, Code_Thingol.Classrel _) = [] | eqns_of_stmt (_, Code_Thingol.Classparam _) = [] - | eqns_of_stmt (inst, Code_Thingol.Classinst { class, vs, superinsts, inst_params, ... }) = - [(inst, (vs, [([], dummy_const class [] `$$ - map (fn (_, (_, (inst, dss))) => dummy_const inst dss) superinsts + | eqns_of_stmt (sym_inst, Code_Thingol.Classinst { class, tyco, vs, superinsts, inst_params, ... }) = + [(sym_inst, (vs, [([], dummy_const (Code_Symbol.Type_Class class) [] `$$ + map (fn (class, dss) => dummy_const (Code_Symbol.Class_Instance (tyco, class)) dss) superinsts @ map (IConst o fst o snd o fst) inst_params)]))]; (* compile whole programs *) fun ensure_const_idx name (nbe_program, (maxidx, idx_tab)) = - if can (Graph.get_node nbe_program) name + if can (Code_Symbol.Graph.get_node nbe_program) name then (nbe_program, (maxidx, idx_tab)) - else (Graph.new_node (name, (NONE, maxidx)) nbe_program, + else (Code_Symbol.Graph.new_node (name, (NONE, maxidx)) nbe_program, (maxidx + 1, Inttab.update_new (maxidx, name) idx_tab)); fun compile_stmts thy stmts_deps = @@ -468,20 +468,20 @@ |> rpair nbe_program; in fold ensure_const_idx refl_deps - #> apfst (fold (fn (name, deps) => fold (curry Graph.add_edge name) deps) names_deps + #> apfst (fold (fn (name, deps) => fold (curry Code_Symbol.Graph.add_edge name) deps) names_deps #> compile - #-> fold (fn (name, univ) => (Graph.map_node name o apfst) (K (SOME univ)))) + #-> fold (fn (name, univ) => (Code_Symbol.Graph.map_node name o apfst) (K (SOME univ)))) end; fun compile_program thy program = let - fun add_stmts names (nbe_program, (maxidx, idx_tab)) = if exists ((can o Graph.get_node) nbe_program) names + fun add_stmts names (nbe_program, (maxidx, idx_tab)) = if exists ((can o Code_Symbol.Graph.get_node) nbe_program) names then (nbe_program, (maxidx, idx_tab)) else (nbe_program, (maxidx, idx_tab)) - |> compile_stmts thy (map (fn name => ((name, Graph.get_node program name), - Graph.immediate_succs program name)) names); + |> compile_stmts thy (map (fn name => ((name, Code_Symbol.Graph.get_node program name), + Code_Symbol.Graph.immediate_succs program name)) names); in - fold_rev add_stmts (Graph.strong_conn program) + fold_rev add_stmts (Code_Symbol.Graph.strong_conn program) end; @@ -493,7 +493,7 @@ let val dict_frees = maps (fn (v, sort) => map_index (curry DFree v o fst) sort) vs; in - ("", (vs, [([], t)])) + (Code_Symbol.value, (vs, [([], t)])) |> singleton (compile_eqnss thy nbe_program deps) |> snd |> (fn t => apps t (rev dict_frees)) @@ -502,43 +502,35 @@ (* reconstruction *) -fun typ_of_itype program vs (ityco `%% itys) = - let - val Code_Thingol.Datatype (tyco, _) = Graph.get_node program ityco; - in Type (tyco, map (typ_of_itype program vs) itys) end - | typ_of_itype program vs (ITyVar v) = - let - val sort = (the o AList.lookup (op =) vs) v; - in TFree ("'" ^ v, sort) end; +fun typ_of_itype vs (tyco `%% itys) = + Type (tyco, map (typ_of_itype vs) itys) + | typ_of_itype vs (ITyVar v) = + TFree ("'" ^ v, (the o AList.lookup (op =) vs) v); -fun term_of_univ thy program idx_tab t = +fun term_of_univ thy 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, _)) = (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) + | take_until f (x :: xs) = if f x then [] else x :: take_until f xs; + fun is_dict (Const (idx, _)) = + (case Inttab.lookup idx_tab idx of + SOME (Code_Symbol.Constant _) => false + | _ => true) | 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.NoStmt c => c - | Code_Thingol.Fun (c, _) => c - | Code_Thingol.Datatypecons (c, _) => c - | Code_Thingol.Classparam (c, _) => c); + fun const_of_idx idx = + case Inttab.lookup idx_tab idx of SOME (Code_Symbol.Constant const) => const; 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 = const_of_idx idx; + val const = const_of_idx idx; val T = map_type_tvar (fn ((v, i), _) => Type_Infer.param typidx (v ^ string_of_int i, [])) - (Sign.the_const_type thy c); + (Sign.the_const_type thy const); val typidx' = typidx + 1; - in of_apps bounds (Term.Const (c, T), ts') typidx' end + in of_apps bounds (Term.Const (const, T), ts') typidx' end | of_univ bounds (BVar (n, ts)) typidx = of_apps bounds (Bound (bounds - n - 1), ts) typidx | of_univ bounds (t as Abs _) typidx = @@ -550,11 +542,11 @@ (* evaluation with type reconstruction *) -fun eval_term thy program (nbe_program, idx_tab) ((vs0, (vs, ty)), t) deps = +fun eval_term thy (nbe_program, idx_tab) ((vs0, (vs, ty)), t) deps = let val ctxt = Syntax.init_pretty_global thy; val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt); - val ty' = typ_of_itype program vs0 ty; + val ty' = typ_of_itype vs0 ty; fun type_infer t = Syntax.check_term (Config.put Type_Infer_Context.const_sorts false ctxt) (Type.constraint ty' t); @@ -563,7 +555,7 @@ else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t); in compile_term thy nbe_program deps (vs, t) - |> term_of_univ thy program idx_tab + |> term_of_univ thy idx_tab |> traced (fn t => "Normalized:\n" ^ string_of_term t) |> type_infer |> traced (fn t => "Types inferred:\n" ^ string_of_term t) @@ -576,8 +568,8 @@ structure Nbe_Functions = Code_Data ( - type T = (Univ option * int) Graph.T * (int * string Inttab.table); - val empty = (Graph.empty, (0, Inttab.empty)); + type T = (Univ option * int) Code_Symbol.Graph.T * (int * Code_Symbol.symbol Inttab.table); + val empty = (Code_Symbol.Graph.empty, (0, Inttab.empty)); ); fun compile ignore_cache thy program = @@ -599,26 +591,23 @@ val (_, raw_oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (@{binding normalization_by_evaluation}, - fn (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct) => - mk_equals thy ct (eval_term thy program nbe_program_idx_tab vsp_ty_t deps)))); + fn (thy, nbe_program_idx_tab, vsp_ty_t, deps, ct) => + mk_equals thy ct (eval_term thy nbe_program_idx_tab vsp_ty_t deps)))); -fun oracle thy program nbe_program_idx_tab vsp_ty_t deps ct = - raw_oracle (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct); +fun oracle thy nbe_program_idx_tab vsp_ty_t deps ct = + raw_oracle (thy, nbe_program_idx_tab, vsp_ty_t, deps, ct); -fun dynamic_conv thy = lift_triv_classes_conv thy (Code_Thingol.dynamic_conv thy - (K (fn program => oracle thy program (compile false thy program)))); +fun dynamic_conv thy = lift_triv_classes_conv thy + (Code_Thingol.dynamic_conv thy (oracle thy o compile false thy)); fun dynamic_value thy = lift_triv_classes_rew thy - (Code_Thingol.dynamic_value thy I - (K (fn program => eval_term thy program (compile false thy program)))); + (Code_Thingol.dynamic_value thy I (eval_term thy o compile false thy)); -fun static_conv thy consts = - lift_triv_classes_conv thy (Code_Thingol.static_conv thy consts - (K (fn program => fn _ => oracle thy program (compile true thy program)))); +fun static_conv thy consts = lift_triv_classes_conv thy + (Code_Thingol.static_conv thy consts (K o oracle thy o compile true thy)); fun static_value thy consts = lift_triv_classes_rew thy - (Code_Thingol.static_value thy I consts - (K (fn program => fn _ => eval_term thy program (compile true thy program)))); + (Code_Thingol.static_value thy I consts (K o eval_term thy o compile true thy)); (** setup **)