Resource Aware ML, Version 1.4.2, July 2018 Typechecking module ... Typecheck successful. Stack-based typecheck successful. Analyzing function add ... Trying degree: 1 == add : [nat; nat] -> nat Non-zero annotations of the argument: 10.00 <-- ([Succ(*)], []) 5.00 <-- ([], []) Non-zero annotations of result: Simplified bound: 5.00 + 10.00*M where M is the number of Succ-nodes of the 1st component of the argument -- Mode: upper Metric: steps Degree: 1 Run time: 0.01 seconds #Constraints: 34 ==== Analyzing function sub ... Trying degree: 1 == sub : [nat; nat] -> nat Non-zero annotations of the argument: 8.00 <-- ([Succ(*)], []) 2.00 <-- ([], [Succ(*)]) 5.00 <-- ([], []) Non-zero annotations of result: Simplified bound: 5.00 + 2.00*L + 8.00*M where L is the number of Succ-nodes of the 2nd component of the argument M is the number of Succ-nodes of the 1st component of the argument -- Mode: upper Metric: steps Degree: 1 Run time: 0.02 seconds #Constraints: 43 ==== Analyzing function mult ... Trying degree: 1, 2 == mult : [nat; 'a] -> nat Non-zero annotations of the argument: 10.00 <-- ([Succ(*); Succ(*)], *) 14.00 <-- ([Succ(*)], *) 3.00 <-- ([], *) Non-zero annotations of result: Simplified bound: 3.00 + 9.00*M + 5.00*M^2 where M is the number of Succ-nodes of the 1st component of the argument -- Mode: upper Metric: steps Degree: 2 Run time: 0.06 seconds #Constraints: 204 ==== Analyzing function eval ... Trying degree: 1, 2, 3 == eval : expr -> nat Non-zero annotations of the argument: 20.00 <-- [Add(*); Nat([Succ(*)])] 14.00 <-- [Nat([Succ(*)])] 14.00 <-- [Add(*)] 14.00 <-- [Sub(*)] 3.00 <-- [] Non-zero annotations of result: 14.00 <-- [Succ(*)] Simplified bound: 3.00 + 20.00*K*L*N + 14.00*K*N + 14.00*L + 14.00*X where X is the number of Sub-nodes of the argument L is the number of Add-nodes of the argument N is the number of Nat-nodes of the argument K is the maximal number of Succ-nodes in the Nat-nodes of the argument -- Mode: upper Metric: steps Degree: 3 Run time: 1.36 seconds #Constraints: 10695 ==== Analyzing function nat_to_int ... Trying degree: 1 == nat_to_int : nat -> int Non-zero annotations of the argument: 11.00 <-- [Succ(*)] 3.00 <-- [] Non-zero annotations of result: Simplified bound: 3.00 + 11.00*M where M is the number of Succ-nodes of the argument -- Mode: upper Metric: steps Degree: 1 Run time: 0.01 seconds #Constraints: 29 ====