Re: [isabelle-dev] Code generation: privacy of exported types in signatures

[Florian Haftmann]

Dear Frédéric,

I cannot follow reproduce observation; using the attached theory in
Isabelle2016-1, I get

> structure Foo : sig
>   type 'a b
>   type 'a c
>   val foo : 'a b -> 'a b
> end = struct
> 
> datatype 'a a = A;
> 
> datatype 'a b = B of 'a c a
> and 'a c = C of 'a b;
> 
> fun foo x = x;
> 
> end; (*struct Foo*)

which is almost perfectly fine, apart from the superfluous 'a c export.

How does your theory and export_code statement exactly look like?

Two points to note anyway:

* This question would belong to the user (published release) rather than
the development (ongoing changes to a central code repository) mailing list.

* The implementation of code exports is an over-approximation.  This is
a known issue but not very likely to be addressed in the near future.

Cheers,
Florian


Am 09.04.2017 um 08:04 schrieb Frederic Tuong (Dr):
> Dear all,
> 
> The SML generated code of the following snippet is not well typed
> anymore since Isabelle 2014:
> 
> datatype 'a A = aaa
> datatype 'a B = bbb "'a C A"
>  and 'a C = ccc "'a B"
> 
> This is because when computing types to be marked as not private (during
> the generation of the signature of A, B and C), A has not been assigned
> as an "Opaque" type, where the constructor Opaque is defined in
> ~~/src/Tools/Code/code_namespace.ML .
> 
> One solution is to replace the function deps_of defined in line 94 of
> http://isabelle.in.tum.de/repos/isabelle/file/7dd1971b39c1/src/Tools/Code/code_namespace.ML
> by this function:
> 
> fun deps_of sym =
>   let
> val succs1 = Code_Symbol.Graph.Keys.dest o
> Code_Symbol.Graph.imm_succs gr;
> fun succs2 x = Code_Symbol.Graph.all_succs gr [x];
> val deps1 = succs1 sym;
> val deps2 = [] |> fold (union (op =)) (map succs2 deps1) |>
> subtract (op =) deps1
>   in (deps1, deps2) end;
> 
> In particular, if sym = ccc, instead of having deps1 = [C] and deps2 =
> [B], we now have deps1 = [C] and deps2 = [A, B].
> 
> 
> As remark, this problem does not happen when types are by default set to
> be publicly exported in signatures. For instance:
> - The semantics of @{code ...} has slightly changed since the support of
> @{computation}, so the generation works now correctly in recent versions
> of Isabelle.
> - Whereas code generated by export_code may fail, we can still add the
> option "open" for it to skip privacy in signatures.
> 
> Best,
> Frédéric
> 
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de


Foo.thy
Description: application/extension-thy


signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Irrefutable patterns in Haskell and Quickcheck/Narrowing

[Florian Haftmann]

For the record:

Lukas and me have resolved that issue in 721feefce9c6.

Cheers,
Florian

Am 14.01.2017 um 09:33 schrieb Florian Haftmann:
> Hi Lukas,
> 
> I am currently stuck with a problem in Quickcheck/Narrowing.
> 
> After about 10 years it came to surface that code generation for Haskell
> may produce irrefutable patterns due to pattern bindings in let clauses.
> See ; if I understand
>  correctly that
> particular semantics allows fancy definitions like the following
> fibonacci one-liner: »fib @ (1 : more_fib) = 1 : 1 : [ a + b | (a, b) <-
> zip fib more_fib ]«.
> 
> However the partial correctness approach of the code generator assumes
> that pattern match clauses may silently be dropped, which is made use of
> to translate the HOL-ish »partial« undefined conveniently. This breaks
> down in presence of irrefutable patterns (see the post on isabelle-users
> by Rene Thiemann).
> 
> The correction is obvious: for Haskell, only local variables may be
> bound by let clauses, but never patterns – these are solely bound by
> case clauses, which are strict in Haskell (as in function equations).
> 
> This however breaks Quickcheck/Narrowing where the lazy nature of
> pattern bindings has been exploited, may be unconsciously. A minimal
> example is attached (Quickcheck_Narrowing_Examples.thy) but I also
> distilled the generated Haskell code:
> 
> The same before and after:
>   Typerep.hs
> 
> Then the difference occurs:
>   Generated_Code.hs
>   Before: Generated_Code.A.hs
>   After: Generated_Code.B.hs
> 
> The same before and after:
>   Narrowing_Engine.hs
>   Main.hs
> 
> The diff ist straight-forward to read:
> 
>>  93,102c93,106
>>  <   let {
>>  < (Narrowing_cons (Narrowing_sum_of_products ps) cfs) = f d;
>>  < (Narrowing_cons ta cas) = a (d - (1 :: Prelude.Int));
>>  < shallow = (0 :: Prelude.Int) < d && non_empty ta;
>>  < aa = (if shallow then map (\ cf (x : xs) -> cf xs (conv cas x)) 
>> cfs
>>  >  <   } in Narrowing_cons
>>  <  (Narrowing_sum_of_products
>>  <(if shallow then map (\ ab -> ta : ab) ps else []))
>>  <  aa;
>>  ---
>>  >   (case f d of {
>>  > Narrowing_cons (Narrowing_sum_of_products ps) cfs ->
>>  >   (case a (d - (1 :: Prelude.Int)) of {
>>  > Narrowing_cons ta cas ->
>>  >   let {
>>  > shallow = (0 :: Prelude.Int) < d && non_empty ta;
>>  > aa = (if shallow then map (\ cf (x : xs) -> cf xs (conv 
>> cas x)) cfs
>>  >else []);
>>  >   } in Narrowing_cons
>>  >  (Narrowing_sum_of_products
>>  >(if shallow then map (\ ab -> ta : ab) ps else []))
>>  >  aa;
>>  >   });
>>  >   });
>>  112,115c116,122
>>  <   let {
>>  < (Narrowing_cons (Narrowing_sum_of_products ssa) ca) = a d;
>>  < (Narrowing_cons (Narrowing_sum_of_products ssb) cb) = b d;
>>  <   } in Narrowing_cons (Narrowing_sum_of_products (ssa ++ ssb)) (ca ++ 
>> cb);
>>  ---
>>  >   (case a d of {
>>  > Narrowing_cons (Narrowing_sum_of_products ssa) ca ->
>>  >   (case b d of {
>>  > Narrowing_cons (Narrowing_sum_of_products ssb) cb ->
>>  >   Narrowing_cons (Narrowing_sum_of_products (ssa ++ ssb)) (ca 
>> ++ cb);
>>  >   });
>>  >   });
> 
> Unfortunately my knowledge is too restricted what could be done here to
> restore the intended behaviour economically.
> 
> Hence I ask whether you have an idea what is going wrong here.
> 
> Thanks a lot!
> 
>   Florian
> 
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev