Hi all,
while playing with coq and extraction I did the following:
"
Fixpoint narity (n: nat) : Set :=
match n with
| O => nat
| S n => nat -> (narity n)
end.
Definition sum_aux : nat -> forall n, narity n :=
fix sum acc n :=
match n as n0 return narity n0 with
| O => acc
| S n => fun m => sum (m+acc) n
end.
Definition sum := sum_aux O.
Eval compute in sum 3 14 67 21.
Recursive Extraction sum.
"
I do not want to comment if this is or not meaningfull, but adapting
the code to caml ints (not doing so will do the same thing, but ints
are easier to play with), I got:
Objective Caml version 3.12.0
# type __ = Obj.t
;;
type __ = Obj.t
# let rec sum_aux acc n = if n <= 0
then Obj.magic acc
else Obj.magic (fun m -> sum_aux (m+acc) (n-1));;
val sum_aux : int -> int -> 'a = <fun>
# let sum = sum_aux 0;;
val sum : int -> 'a = <fun>
# print_int (sum 3 14 67 21);;
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
102- : unit = ()
The result is correct, but the warning is quite unexpected!
(Changing the values of the arguments will of course change the result)
It is not important or armfull, but quite funny.
--
Caml-list mailing list. Subscription management and archives:
https://sympa-roc.inria.fr/wws/info/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
