coq-breakpoints
Mar. 20th, 2013 07:22 pmЗарелизил мелкую библиотечку для отладки редукций выражений в пределах coq: https://bitbucket.org/gds/coq-breakpoints
$ ./main.byte (lcm 6 36/5) = 36
function add(a, b) { return (a + b); };
add : Ta : Type -> a : Ta -> Tb : Type -> b : Tb -> Ta = if Ta = Number then add_number a (cast_to_number Tb b) else if Ta = String then concat a (cast_to_string Tb b) else fail
cast_to_number : T : Type -> x : T -> number cast_to_string : T : Type -> x : T -> string
(Ta : Type, a : Ta)
в виде туплов.[("a", String "str"); ("b", Int 123); ("c", Bool True)]
), кодvalue () = run & (fun f -> f <$> string "a" <*> int "b" <*> bool "c") (Printf.printf "a=%S b=%i c=%b") ;
a="str" b=123 c=true
sql_t = [ `Null | `String of string | `Binary of string | ... ]
.value read : (stringscount:int -> list (iteratee char 'a)) -> iteratee char (list 'a)
value read : (stringscount:int -> 'a -> iteratee char 'a) -> 'a -> iteratee char 'a
(it1 >>= fun v1 -> it2 >>= fun v2 -> return v1 + v2)
, но фишка в том, что it1 и it2 должны не трогать поток за пределами того, что им выделено, то есть, если в терминах итератов, должно было бы быть что-то типа ((join & take len1 it1) >>= fun v1 -> (join & take len2 it2) >>= fun v2 -> return v1 + v2)
, и не представляю, как это сделать.value read : (ntotal -> npart -> nbytes -> iteratee char 'i)
-> iteratee 'i 'a
-> iteratee char 'a