# HG changeset patch # User haftmann # Date 1399616017 -7200 # Node ID 4044a7d1720f64fa101baf107766f14da2f65689 # Parent aaea99edc040faef335c0fef58f20b634f2cd8c5 hardcoded nbe and sml into value command diff -r aaea99edc040 -r 4044a7d1720f NEWS --- a/NEWS Fri May 09 08:13:36 2014 +0200 +++ b/NEWS Fri May 09 08:13:37 2014 +0200 @@ -204,8 +204,11 @@ *** HOL *** +* Command and antiquotation ''value'' are hardcoded against nbe and +ML now. Minor INCOMPATIBILITY. + * Separate command ''approximate'' for approximative computation -in Decision_Procs/Approximation. Minor INCOMPATBILITY. +in Decision_Procs/Approximation. Minor INCOMPATIBILITY. * Adjustion of INF and SUP operations: * Elongated constants INFI and SUPR to INFIMUM and SUPREMUM. diff -r aaea99edc040 -r 4044a7d1720f src/Doc/Codegen/Evaluation.thy --- a/src/Doc/Codegen/Evaluation.thy Fri May 09 08:13:36 2014 +0200 +++ b/src/Doc/Codegen/Evaluation.thy Fri May 09 08:13:37 2014 +0200 @@ -90,18 +90,12 @@ value %quote "42 / (12 :: rat)" text {* - \noindent By default @{command value} tries all available evaluation - techniques and prints the result of the first succeeding one. A particular - technique may be specified in square brackets, e.g. -*} + \noindent @{command value} tries first to evaluate using ML, falling + back to normalization by evaluation if this fails. -value %quote [nbe] "42 / (12 :: rat)" - -text {* To employ dynamic evaluation in the document generation, there is also - a @{text value} antiquotation. By default, it also tries all available evaluation - techniques and prints the result of the first succeeding one, unless a particular - technique is specified in square brackets. + a @{text value} antiquotation with the same evaluation techniques + as @{command value}. Static evaluation freezes the code generator configuration at a certain point and uses this context whenever evaluation is issued @@ -172,10 +166,7 @@ \fontsize{9pt}{12pt}\selectfont \begin{tabular}{ll||c|c|c} & & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline - \multirow{5}{1ex}{\rotatebox{90}{dynamic}} - & interactive evaluation - & @{command value} @{text "[simp]"} & @{command value} @{text "[nbe]"} & @{command value} @{text "[code]"} - \tabularnewline + \multirow{4}{1ex}{\rotatebox{90}{dynamic}} & plain evaluation & & & \ttsize@{ML "Code_Evaluation.dynamic_value"} \tabularnewline \cline{2-5} & evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline & property conversion & & & \ttsize@{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \cline{2-5} diff -r aaea99edc040 -r 4044a7d1720f src/Doc/Isar_Ref/HOL_Specific.thy --- a/src/Doc/Isar_Ref/HOL_Specific.thy Fri May 09 08:13:36 2014 +0200 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Fri May 09 08:13:37 2014 +0200 @@ -2114,7 +2114,7 @@ \end{matharray} @{rail \ - @@{command (HOL) value} ( '[' @{syntax name} ']' )? modes? @{syntax term} + @@{command (HOL) value} modes? @{syntax term} ; @@{command (HOL) values} modes? @{syntax nat}? @{syntax term} @@ -2144,13 +2144,8 @@ \item @{command (HOL) "value"}~@{text t} evaluates and prints a term; optionally @{text modes} can be specified, which are appended to the current print mode; see \secref{sec:print-modes}. - Internally, the evaluation is performed by registered evaluators, - which are invoked sequentially until a result is returned. - Alternatively a specific evaluator can be selected using square - brackets; typical evaluators use the current set of code equations - to normalize and include @{text simp} for fully symbolic evaluation - using the simplifier, @{text nbe} for \emph{normalization by - evaluation} and \emph{code} for code generation in SML. + Evaluation is tried first using ML, falling + back to normalization by evaluation if this fails. \item @{command (HOL) "values"}~@{text t} enumerates a set comprehension by evaluation and prints its values up to the given diff -r aaea99edc040 -r 4044a7d1720f src/HOL/Code_Evaluation.thy --- a/src/HOL/Code_Evaluation.thy Fri May 09 08:13:36 2014 +0200 +++ b/src/HOL/Code_Evaluation.thy Fri May 09 08:13:37 2014 +0200 @@ -158,11 +158,6 @@ ML_file "~~/src/HOL/Tools/value.ML" -setup {* - Value.add_evaluator ("nbe", Nbe.dynamic_value) - #> Value.add_evaluator ("code", Code_Evaluation.dynamic_value_strict) -*} - subsection {* Generic reification *} diff -r aaea99edc040 -r 4044a7d1720f src/HOL/IMP/Abs_Int1_parity.thy --- a/src/HOL/IMP/Abs_Int1_parity.thy Fri May 09 08:13:36 2014 +0200 +++ b/src/HOL/IMP/Abs_Int1_parity.thy Fri May 09 08:13:37 2014 +0200 @@ -134,7 +134,7 @@ definition "test1_parity = ''x'' ::= N 1;; WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)" -value [code] "show_acom (the(AI_parity test1_parity))" +value "show_acom (the(AI_parity test1_parity))" definition "test2_parity = ''x'' ::= N 1;; diff -r aaea99edc040 -r 4044a7d1720f src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Fri May 09 08:13:36 2014 +0200 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Fri May 09 08:13:37 2014 +0200 @@ -100,12 +100,12 @@ WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y'';; ''y'' ::= V ''z'';; ''z'' ::= V ''u'')" -value [code] "list (AI_const test1_const Top)" -value [code] "list (AI_const test2_const Top)" -value [code] "list (AI_const test3_const Top)" -value [code] "list (AI_const test4_const Top)" -value [code] "list (AI_const test5_const Top)" -value [code] "list (AI_const test6_const Top)" -value [code] "list (AI_const test7_const Top)" +value "list (AI_const test1_const Top)" +value "list (AI_const test2_const Top)" +value "list (AI_const test3_const Top)" +value "list (AI_const test4_const Top)" +value "list (AI_const test5_const Top)" +value "list (AI_const test6_const Top)" +value "list (AI_const test7_const Top)" end diff -r aaea99edc040 -r 4044a7d1720f src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Fri May 09 08:13:36 2014 +0200 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Fri May 09 08:13:37 2014 +0200 @@ -213,22 +213,22 @@ "list_up bot = bot" | "list_up (Up x) = Up(list x)" -value [code] "list_up(afilter_ivl (N 5) (I (Some 4) (Some 5)) Top)" -value [code] "list_up(afilter_ivl (N 5) (I (Some 4) (Some 4)) Top)" -value [code] "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 4)) +value "list_up(afilter_ivl (N 5) (I (Some 4) (Some 5)) Top)" +value "list_up(afilter_ivl (N 5) (I (Some 4) (Some 4)) Top)" +value "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 4)) (Up(FunDom(Top(''x'':=I (Some 5) (Some 6))) [''x''])))" -value [code] "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 5)) +value "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 5)) (Up(FunDom(Top(''x'':=I (Some 5) (Some 6))) [''x''])))" -value [code] "list_up(afilter_ivl (Plus (V ''x'') (V ''x'')) (I (Some 0) (Some 10)) +value "list_up(afilter_ivl (Plus (V ''x'') (V ''x'')) (I (Some 0) (Some 10)) (Up(FunDom(Top(''x'':= I (Some 0) (Some 100)))[''x''])))" -value [code] "list_up(afilter_ivl (Plus (V ''x'') (N 7)) (I (Some 0) (Some 10)) +value "list_up(afilter_ivl (Plus (V ''x'') (N 7)) (I (Some 0) (Some 10)) (Up(FunDom(Top(''x'':= I (Some 0) (Some 100)))[''x''])))" -value [code] "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True +value "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True (Up(FunDom(Top(''x'':= I (Some 0) (Some 0)))[''x''])))" -value [code] "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True +value "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True (Up(FunDom(Top(''x'':= I (Some 0) (Some 2)))[''x''])))" -value [code] "list_up(bfilter_ivl (Less (V ''x'') (Plus (N 10) (V ''y''))) True +value "list_up(bfilter_ivl (Less (V ''x'') (Plus (N 10) (V ''y''))) True (Up(FunDom(Top(''x'':= I (Some 15) (Some 20),''y'':= I (Some 5) (Some 7)))[''x'', ''y''])))" definition "test_ivl1 = @@ -236,7 +236,7 @@ IF Less (V ''x'') (V ''y'') THEN ''y'' ::= Plus (V ''y'') (V ''x'') ELSE ''x'' ::= Plus (V ''x'') (V ''y'')" -value [code] "list_up(AI_ivl test_ivl1 Top)" +value "list_up(AI_ivl test_ivl1 Top)" value "list_up (AI_ivl test3_const Top)" @@ -247,24 +247,24 @@ definition "test2_ivl = ''y'' ::= N 7;; WHILE Less (V ''x'') (N 100) DO ''y'' ::= Plus (V ''y'') (N 1)" -value [code] "list_up(AI_ivl test2_ivl Top)" +value "list_up(AI_ivl test2_ivl Top)" definition "test3_ivl = ''x'' ::= N 0;; ''y'' ::= N 100;; ''z'' ::= Plus (V ''x'') (V ''y'');; WHILE Less (V ''x'') (N 11) DO (''x'' ::= Plus (V ''x'') (N 1);; ''y'' ::= Plus (V ''y'') (N -1))" -value [code] "list_up(AI_ivl test3_ivl Top)" +value "list_up(AI_ivl test3_ivl Top)" definition "test4_ivl = ''x'' ::= N 0;; ''y'' ::= N 0;; WHILE Less (V ''x'') (N 1001) DO (''y'' ::= V ''x'';; ''x'' ::= Plus (V ''x'') (N 1))" -value [code] "list_up(AI_ivl test4_ivl Top)" +value "list_up(AI_ivl test4_ivl Top)" text{* Nontermination not detected: *} definition "test5_ivl = ''x'' ::= N 0;; WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)" -value [code] "list_up(AI_ivl test5_ivl Top)" +value "list_up(AI_ivl test5_ivl Top)" end diff -r aaea99edc040 -r 4044a7d1720f src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Fri May 09 08:13:36 2014 +0200 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Fri May 09 08:13:37 2014 +0200 @@ -200,8 +200,8 @@ and aval_ivl' = aval' proof qed (auto simp: iter'_pfp_above) -value [code] "list_up(AI_ivl' test3_ivl Top)" -value [code] "list_up(AI_ivl' test4_ivl Top)" -value [code] "list_up(AI_ivl' test5_ivl Top)" +value "list_up(AI_ivl' test3_ivl Top)" +value "list_up(AI_ivl' test4_ivl Top)" +value "list_up(AI_ivl' test5_ivl Top)" end diff -r aaea99edc040 -r 4044a7d1720f src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Fri May 09 08:13:36 2014 +0200 +++ b/src/HOL/Library/Extended_Real.thy Fri May 09 08:13:37 2014 +0200 @@ -2444,10 +2444,10 @@ (* A small list of simple arithmetic expressions *) -value [code] "- \ :: ereal" -value [code] "\-\\ :: ereal" -value [code] "4 + 5 / 4 - ereal 2 :: ereal" -value [code] "ereal 3 < \" -value [code] "real (\::ereal) = 0" +value "- \ :: ereal" +value "\-\\ :: ereal" +value "4 + 5 / 4 - ereal 2 :: ereal" +value "ereal 3 < \" +value "real (\::ereal) = 0" end diff -r aaea99edc040 -r 4044a7d1720f src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Fri May 09 08:13:36 2014 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Fri May 09 08:13:37 2014 +0200 @@ -452,8 +452,8 @@ values [random_dseq 1, 3, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}" values [random_dseq 1, 1, 4] 10 "{(xs, ys, zs::int list). append xs ys zs}" -value [code] "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])" -value [code] "Predicate.the (slice ([]::int list))" +value "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])" +value "Predicate.the (slice ([]::int list))" text {* tricky case with alternative rules *} @@ -830,7 +830,7 @@ code_pred divmod_rel . thm divmod_rel.equation -value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)" +value "Predicate.the (divmod_rel_i_i_o_o 1705 42)" subsection {* Transforming predicate logic into logic programs *} diff -r aaea99edc040 -r 4044a7d1720f src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy --- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Fri May 09 08:13:36 2014 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Fri May 09 08:13:37 2014 +0200 @@ -183,7 +183,7 @@ quickcheck[tester = smart_exhaustive] oops -value [code] "prop_regex a_sol" +value "prop_regex a_sol" end diff -r aaea99edc040 -r 4044a7d1720f src/HOL/Tools/value.ML --- a/src/HOL/Tools/value.ML Fri May 09 08:13:36 2014 +0200 +++ b/src/HOL/Tools/value.ML Fri May 09 08:13:37 2014 +0200 @@ -1,53 +1,30 @@ -(* Title: Tools/value.ML +(* Title: HOL/Tools/value.ML Author: Florian Haftmann, TU Muenchen -Generic value command for arbitrary evaluators. +Evaluation using nbe or SML. *) signature VALUE = sig val value: Proof.context -> term -> term - val value_select: string -> Proof.context -> term -> term - val value_cmd: string option -> string list -> string -> Toplevel.state -> unit - val add_evaluator: string * (Proof.context -> term -> term) -> theory -> theory + val value_cmd: string list -> string -> Toplevel.state -> unit end; structure Value : VALUE = struct -structure Evaluator = Theory_Data -( - type T = (string * (Proof.context -> term -> term)) list; - val empty = []; - val extend = I; - fun merge data : T = AList.merge (op =) (K true) data; -) - -val add_evaluator = Evaluator.map o AList.update (op =); - -fun value_select name ctxt = - case AList.lookup (op =) (Evaluator.get (Proof_Context.theory_of ctxt)) name - of NONE => error ("No such evaluator: " ^ name) - | SOME f => f ctxt; +fun value ctxt t = + if null (Term.add_frees t []) + then case try (Code_Evaluation.dynamic_value_strict ctxt) t of + SOME t' => t' + | NONE => Nbe.dynamic_value ctxt t + else Nbe.dynamic_value ctxt t; -fun value ctxt t = let val evaluators = Evaluator.get (Proof_Context.theory_of ctxt) - in if null evaluators then error "No evaluators" - else let val (evaluators, (_, evaluator)) = split_last evaluators - in case get_first (fn (_, f) => try (f ctxt) t) evaluators - of SOME t' => t' - | NONE => evaluator ctxt t - end end; - -fun value_maybe_select some_name = - case some_name - of NONE => value - | SOME name => value_select name; - -fun value_cmd some_name modes raw_t state = +fun value_cmd modes raw_t state = let val ctxt = Toplevel.context_of state; val t = Syntax.read_term ctxt raw_t; - val t' = value_maybe_select some_name ctxt t; + val t' = value ctxt t; val ty' = Term.type_of t'; val ctxt' = Variable.auto_fixes t' ctxt; val p = Print_Mode.with_modes modes (fn () => @@ -63,14 +40,14 @@ val _ = Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term" - (opt_evaluator -- opt_modes -- Parse.term - >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t))); + (opt_modes -- Parse.term + >> (fn (modes, t) => Toplevel.keep (value_cmd modes t))); val _ = Context.>> (Context.map_theory (Thy_Output.antiquotation @{binding value} - (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term) - (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context + (Term_Style.parse -- Args.term) + (fn {source, context, ...} => fn (style, t) => Thy_Output.output context (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source - [style (value_maybe_select some_name context t)])))); + [style (value context t)])))); end; diff -r aaea99edc040 -r 4044a7d1720f src/HOL/ex/Eval_Examples.thy --- a/src/HOL/ex/Eval_Examples.thy Fri May 09 08:13:36 2014 +0200 +++ b/src/HOL/ex/Eval_Examples.thy Fri May 09 08:13:37 2014 +0200 @@ -25,36 +25,20 @@ text {* term evaluation *} value "(Suc 2 + 1) * 4" -value [code] "(Suc 2 + 1) * 4" -value [nbe] "(Suc 2 + 1) * 4" value "(Suc 2 + Suc 0) * Suc 3" -value [code] "(Suc 2 + Suc 0) * Suc 3" -value [nbe] "(Suc 2 + Suc 0) * Suc 3" value "nat 100" -value [code] "nat 100" -value [nbe] "nat 100" value "(10::int) \ 12" -value [code] "(10::int) \ 12" -value [nbe] "(10::int) \ 12" value "max (2::int) 4" -value [code] "max (2::int) 4" -value [nbe] "max (2::int) 4" value "of_int 2 / of_int 4 * (1::rat)" -value [code] "of_int 2 / of_int 4 * (1::rat)" -value [nbe] "of_int 2 / of_int 4 * (1::rat)" value "[] :: nat list" -value [code] "[] :: nat list" -value [nbe] "[] :: nat list" value "[(nat 100, ())]" -value [code] "[(nat 100, ())]" -value [nbe] "[(nat 100, ())]" text {* a fancy datatype *} @@ -67,7 +51,5 @@ | Blubb "('a, 'b) foo" value "Bla (Bar (4::nat) [Suc 0])" -value [code] "Bla (Bar (4::nat) [Suc 0])" -value [nbe] "Bla (Bar (4::nat) [Suc 0])" end diff -r aaea99edc040 -r 4044a7d1720f src/HOL/ex/Normalization_by_Evaluation.thy --- a/src/HOL/ex/Normalization_by_Evaluation.thy Fri May 09 08:13:36 2014 +0200 +++ b/src/HOL/ex/Normalization_by_Evaluation.thy Fri May 09 08:13:37 2014 +0200 @@ -68,20 +68,20 @@ lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs" by normalization rule lemma "rev [a, b, c] = [c, b, a]" by normalization -value [nbe] "rev (a#b#cs) = rev cs @ [b, a]" -value [nbe] "map (%F. F [a,b,c::'x]) (map map [f,g,h])" -value [nbe] "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))" -value [nbe] "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])" +value "rev (a#b#cs) = rev cs @ [b, a]" +value "map (%F. F [a,b,c::'x]) (map map [f,g,h])" +value "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))" +value "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])" lemma "map (%x. case x of None \ False | Some y \ True) [None, Some ()] = [False, True]" by normalization -value [nbe] "case xs of [] \ True | x#xs \ False" -value [nbe] "map (%x. case x of None \ False | Some y \ True) xs = P" +value "case xs of [] \ True | x#xs \ False" +value "map (%x. case x of None \ False | Some y \ True) xs = P" lemma "let x = y in [x, x] = [y, y]" by normalization lemma "Let y (%x. [x,x]) = [y, y]" by normalization -value [nbe] "case n of Z \ True | S x \ False" +value "case n of Z \ True | S x \ False" lemma "(%(x,y). add x y) (S z,S z) = S (add z (S z))" by normalization -value [nbe] "filter (%x. x) ([True,False,x]@xs)" -value [nbe] "filter Not ([True,False,x]@xs)" +value "filter (%x. x) ([True,False,x]@xs)" +value "filter Not ([True,False,x]@xs)" lemma "[x,y,z] @ [a,b,c] = [x, y, z, a, b, c]" by normalization lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]" by normalization @@ -106,7 +106,7 @@ lemma "[Suc 0, 0] = [Suc 0, 0]" by normalization lemma "max (Suc 0) 0 = Suc 0" by normalization lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization -value [nbe] "Suc 0 \ set ms" +value "Suc 0 \ set ms" (* non-left-linear patterns, equality by extensionality *) @@ -115,13 +115,13 @@ lemma "(f o g) x = f (g x)" by normalization lemma "(f o id) x = f x" by normalization lemma "(id :: bool \ bool) = id" by normalization -value [nbe] "(\x. x)" +value "(\x. x)" (* Church numerals: *) -value [nbe] "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))" -value [nbe] "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))" -value [nbe] "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))" +value "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))" +value "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))" +value "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))" (* handling of type classes in connection with equality *) diff -r aaea99edc040 -r 4044a7d1720f src/HOL/ex/Parallel_Example.thy --- a/src/HOL/ex/Parallel_Example.thy Fri May 09 08:13:36 2014 +0200 +++ b/src/HOL/ex/Parallel_Example.thy Fri May 09 08:13:37 2014 +0200 @@ -93,7 +93,7 @@ (\() \ let c = Parallel.fork computation_harmonic in (computation_primes (), Parallel.join c))" -value [code] "computation_future ()" +value "computation_future ()" definition computation_factorise :: "nat \ nat list" where "computation_factorise = Debug.timing (STR ''factorise'') factorise" @@ -102,7 +102,7 @@ "computation_parallel _ = Debug.timing (STR ''overall computation'') (Parallel.map computation_factorise) [20000..<20100]" -value [code] "computation_parallel ()" +value "computation_parallel ()" end