Re: [isabelle] Composing BNFs



Hi Dimitriy,

this is really cool! I haven't looked into the BNF_.. code yet, so I have two questions out of ignorance, that I hope are quick to answer for you:

- is there something similar for fold / traverse?

- in the below example, for the type "('a option + 'b ) list + 'c", a function "sum1.sum1.sum1.list.map_list_lift1_permute_201_01" is created. Can this be avoided / why is this needed, and why is a function created that ignores its last argument?

local_setup â fn lthy =>
 let
   val live_As = [ at {typ 'a}, @{typ 'b}, @{typ 'c}]
   val dead_As = []

   fun flatten_tyargs Ass =
     map dest_TFree live_As
     |> filter (fn T => exists (fn Ts => member (op =) Ts T) Ass);

   val ((bnf, _), (_, lthy)) =
     BNF_Comp.bnf_of_typ false BNF_Def.Do_Inline I
       flatten_tyargs (map dest_TFree live_As) (map dest_TFree dead_As)
       @{typ "('a option + 'b ) list + 'c"}
       ((BNF_Comp.empty_comp_cache, BNF_Comp.empty_unfolds), lthy)
   val _ = BNF_Def.map_of_bnf bnf |> Syntax.string_of_term lthy |> warning
   val _ = BNF_Def.map_of_bnf bnf |> fastype_of |> Syntax.string_of_typ lthy |> warning
 in
   lthy
 end
â

(* Note that I could simply use the following term, indicating that no extra functions are required: *)
term "op o (map_sum o map_option) o op o map o map_sum"



> On 10 Apr 2017, at 16:49, Dmitriy Traytel <traytel at inf.ethz.ch> wrote:
> 
> Hi Lars,
> 
> sure, BNFs can figure this out by themselves indeed. But then very often the variables will not be in the order in which you expect them. (Same for the dead ones.) Therefore it is better to fix the order on the callerâs side.
> 
> Cheers,
> Dmitriy
> 
>> On 10 Apr 2017, at 16:38, Lars Hupel <hupel at in.tum.de> wrote:
>> 
>> Hi Dmitriy,
>> 
>> thanks for that.
>> 
>>>   val live_As = [ at {typ 'a}, @{typ 'b}]
>>>   val dead_As = []
>> 
>> Is there a reason why I need to specify the live variables? Surely the
>> internal bookkeeping of BNF already knows which variables are live and
>> which are dead.
>> 
>> Cheers
>> Lars
> 
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.