Maude-help mailing list

[Francisco Durán <fdm AT uma.es>]

Hu Raghu,

The show advisories command may be useful for that. 

https://urldefense.com/v3/__https://maude.lcc.uma.es/maude-manual/maude-manualap1.html*x119-316000A.11__;Iw!!DZ3fjg!_IvJF6tKEtV6h7YIj3dUdIXLuGYp-iNwkIQ7BLU7gV2lSdnW82ZoF5aY0MQprgAcrlV7mKtGfsbsd6sCgNB8YQ$
 

Cheers,

Francisco

> On 7 Dec 2023, at 00:33, Raghu Ranganathan <rraghu.11502 AT gmail.com> wrote:
> 
> Thanks, this works well for  the problem. Is there a way to disable the 
> warning messages  specifically from the importations? Is there a 
> possibility that the module loading mechanism can be patched to avoid this?
> 
> On Mon, Dec 4, 2023 at 8:47 PM Francisco Durán <fdm AT uma.es> wrote:
> Hi Raghu,
> 
> The advisories come from the double importation of LIST{NAT}. The problem 
> is that META-LEVEL imports NAT-LIST
> 
> fmod NAT-LIST is
> protecting LIST{Nat} * (sort NeList{Nat} to NeNatList, sort List{Nat} to 
> NatList) .
> endfm
> 
> which leads to the importation of both LIST{Nat} and LIST{Nat} * (sort 
> NeList{Nat} to NeNatList, sort List{Nat} to NatList). This is possibly 
> harmless and you don't need to worry about the advisories, but you get two 
> different copies of nat lists, those of type NatList and those of type 
> List{Nat}. The solution to this would be just to apply the same renaming in 
> the importation in NAT-MAP
> 
> fmod NAT-MAP is
> pr MAPinc{Nat} * (sort NeList{Nat} to NeNatList, sort List{Nat} to NatList) 
> .
> endfm
> 
> However, by the way in which importations work you'll still get the 
> advisory messages. In this case, you can ignore them safely. 
> 
> Best,
> 
> Francisco
> 
> > On 4 Dec 2023, at 05:29, Raghu Ranganathan <rraghu.11502 AT gmail.com> wrote:
> > 
> > hi, thank you for the response.
> > 
> > I decided that i would go with the metaprogramming approach today, and I 
> > came up with the following:
> > 
> > fmod MAPinc{X :: TRIV} is
> >   pr META-LEVEL .
> >   ex LIST{X} .
> > 
> >   var F M : Qid .
> >   var Y D : X$Elt .
> >   var L : List{X} .
> > 
> >   op map : Qid Qid X$Elt List{X} -> List{X} .
> >   eq map(F, M, D, Y L) = downTerm(getTerm(metaReduce(upModule(M, false), 
> > F[upTerm(Y)])), D) map(F, M, D, L) .
> >   eq map(F, M, D, nil) = nil .
> > endfm
> > 
> > fmod NAT-MAP is
> >   pr MAPinc{Nat} .
> > endfm
> > 
> > M is a Qid that specifies the module, and D is a default value of sort X.
> > I am doing this extra modification because I want a generalizable form of 
> > map, and I want some more similar convenient ways to work with 
> > programming problems in maude (current Advent of Code 2023).
> > 
> > MAPinc loads fine as is, but when i added NAT-MAP I got the following 
> > Advisories:
> > 
> > Advisory: <automatic>: operator nil has been imported from both 
> > "prelude.maude", line 1011 (fmod LIST) and "prelude.maude", line 1011 
> > (fmod LIST) with no common ancestor.
> > Advisory: <automatic>: operator __ has been imported from both 
> > "prelude.maude", line 1012 (fmod LIST) and "prelude.maude", line 1012 
> > (fmod LIST) with no common ancestor.
> > Advisory: <automatic>: operator append has been imported from both 
> > "prelude.maude", line 1020 (fmod LIST) and "prelude.maude", line 1020 
> > (fmod LIST) with no common ancestor.
> > Advisory: <automatic>: operator head has been imported from both 
> > "prelude.maude", line 1025 (fmod LIST) and "prelude.maude", line 1025 
> > (fmod LIST) with no common ancestor.
> > Advisory: <automatic>: operator tail has been imported from both 
> > "prelude.maude", line 1028 (fmod LIST) and "prelude.maude", line 1028 
> > (fmod LIST) with no common ancestor.
> > Advisory: <automatic>: operator last has been imported from both 
> > "prelude.maude", line 1031 (fmod LIST) and "prelude.maude", line 1031 
> > (fmod LIST) with no common ancestor.
> > Advisory: <automatic>: operator front has been imported from both 
> > "prelude.maude", line 1034 (fmod LIST) and "prelude.maude", line 1034 
> > (fmod LIST) with no common ancestor.
> > Advisory: <automatic>: operator occurs has been imported from both 
> > "prelude.maude", line 1037 (fmod LIST) and "prelude.maude", line 1037 
> > (fmod LIST) with no common ancestor.
> > Advisory: <automatic>: operator reverse has been imported from both 
> > "prelude.maude", line 1041 (fmod LIST) and "prelude.maude", line 1041 
> > (fmod LIST) with no common ancestor.
> > Advisory: <automatic>: operator $reverse has been imported from both 
> > "prelude.maude", line 1045 (fmod LIST) and "prelude.maude", line 1045 
> > (fmod LIST) with no common ancestor.
> > Advisory: <automatic>: operator size has been imported from both 
> > "prelude.maude", line 1049 (fmod LIST) and "prelude.maude", line 1049 
> > (fmod LIST) with no common ancestor.
> > Advisory: <automatic>: operator $size has been imported from both 
> > "prelude.maude", line 1053 (fmod LIST) and "prelude.maude", line 1053 
> > (fmod LIST) with no common ancestor.
> > Advisory: "lib.maude", line 69 (fmod NAT-MAP): operator nil has been 
> > imported from both "prelude.maude", line 1011 (fmod LIST) and 
> > "prelude.maude", line 1011 (fmod LIST) with no common ancestor.
> > Advisory: "lib.maude", line 69 (fmod NAT-MAP): operator __ has been 
> > imported from both "prelude.maude", line 1012 (fmod LIST) and 
> > "prelude.maude", line 1012 (fmod LIST) with no common ancestor.
> > Advisory: "lib.maude", line 69 (fmod NAT-MAP): operator append has been 
> > imported from both "prelude.maude", line 1020 (fmod LIST) and 
> > "prelude.maude", line 1020 (fmod LIST) with no common ancestor.
> > Advisory: "lib.maude", line 69 (fmod NAT-MAP): operator head has been 
> > imported from both "prelude.maude", line 1025 (fmod LIST) and 
> > "prelude.maude", line 1025 (fmod LIST) with no common ancestor.
> > Advisory: "lib.maude", line 69 (fmod NAT-MAP): operator tail has been 
> > imported from both "prelude.maude", line 1028 (fmod LIST) and 
> > "prelude.maude", line 1028 (fmod LIST) with no common ancestor.
> > Advisory: "lib.maude", line 69 (fmod NAT-MAP): operator last has been 
> > imported from both "prelude.maude", line 1031 (fmod LIST) and 
> > "prelude.maude", line 1031 (fmod LIST) with no common ancestor.
> > Advisory: "lib.maude", line 69 (fmod NAT-MAP): operator front has been 
> > imported from both "prelude.maude", line 1034 (fmod LIST) and 
> > "prelude.maude", line 1034 (fmod LIST) with no common ancestor.
> > Advisory: "lib.maude", line 69 (fmod NAT-MAP): operator occurs has been 
> > imported from both "prelude.maude", line 1037 (fmod LIST) and 
> > "prelude.maude", line 1037 (fmod LIST) with no common ancestor.
> > Advisory: "lib.maude", line 69 (fmod NAT-MAP): operator reverse has been 
> > imported from both "prelude.maude", line 1041 (fmod LIST) and 
> > "prelude.maude", line 1041 (fmod LIST) with no common ancestor.
> > Advisory: "lib.maude", line 69 (fmod NAT-MAP): operator $reverse has been 
> > imported from both "prelude.maude", line 1045 (fmod LIST) and 
> > "prelude.maude", line 1045 (fmod LIST) with no common ancestor.
> > Advisory: "lib.maude", line 69 (fmod NAT-MAP): operator size has been 
> > imported from both "prelude.maude", line 1049 (fmod LIST) and 
> > "prelude.maude", line 1049 (fmod LIST) with no common ancestor.
> > Advisory: "lib.maude", line 69 (fmod NAT-MAP): operator $size has been 
> > imported from both "prelude.maude", line 1053 (fmod LIST) and 
> > "prelude.maude", line 1053 (fmod LIST) with no common ancestor.
> > 
> > how do i make this work correctly? I am assuming i am loading List 
> > incorrectly, but I am not sure how.
> > 
> > On Mon, Dec 4, 2023 at 3:17 AM Francisco Durán <narudocap AT gmail.com> 
> > wrote:
> > Hi Raghu,
> > 
> > Many years ago we proposed a generic solution, as an extension of Full 
> > Maude. However, after so many years it has got completely outdated, and 
> > it would require a complete re-implementation.
> > 
> > Manuel Clavel, Francisco Durán, Narciso Martí-Oliet:
> > Polytypic Programming in Maude. WRLA 2000: 339-360
> > https://urldefense.com/v3/__https://doi.org/10.1016/S1571-0661(05)80135-5__;!!DZ3fjg!_IvJF6tKEtV6h7YIj3dUdIXLuGYp-iNwkIQ7BLU7gV2lSdnW82ZoF5aY0MQprgAcrlV7mKtGfsbsd6sEmAnpGA$
> >  
> > 
> > I can see two ways to handle this kind of things: parameterization and 
> > metalevel. 
> > 
> > The simplest solution is using parameterization. E.g., 
> > 
> > fth FUN is
> > inc TRIV .
> > op f : Elt -> Elt .
> > endfth
> > 
> > view FUN from TRIV to FUN is
> > sort Elt to Elt .
> > endv 
> > 
> > fmod MAPF{X :: FUN} is
> > pr LIST{FUN}{X} .
> > op map : List{FUN}{X} -> List{FUN}{X} .
> > var X : X$Elt .
> > var L : List{FUN}{X} .
> > eq map(X L) = f(X) map(L) .
> > eq map(nil) = nil .
> > endfm
> > 
> > view inc from FUN to NAT is 
> > sort Elt to Nat .
> > var N : Elt .
> > op f(N) to term N + 1 .
> > endv
> > 
> > fmod MAPinc is
> > pr MAPF{inc} .
> > endfm
> > 
> > red map(2 3 4) .
> > 
> > In this solution the function is not a parameter of the map, it's 
> > provided in the view. 
> > 
> > Metaprogramming provides a simpler solution
> > 
> > fmod MAPinc is
> > pr META-LEVEL .
> > op map : Qid NatList -> NatList .
> > var F : Qid .
> > var X : Nat .
> > var L : NatList .
> > eq map(F, X L) = downTerm(getTerm(metaReduce(upModule('NAT, false), 
> > F[upTerm(X)])), 0) map(F, L) .
> > eq map(F, nil) = nil .
> > endfm
> > 
> > red map('s_, 2 3 4) .
> > 
> > Best regards, 
> > 
> > Francisco
> > 
> > 
> > > On 2 Dec 2023, at 07:30, Raghu Ranganathan <rraghu.11502 AT gmail.com> 
> > > wrote:
> > > 
> > > I would like to create an operator that can take in a different 
> > > operator and add that operator to its expansion. I want to implement 
> > > things like map and filter in haskell or find useful alternatives to 
> > > those.
> > > 
> > > For example:
> > > 
> > > mod FUNC{X :: TRIV} is
> > >   ex LIST*{X} .
> > >   pr META-TERM . 
> > >   var F : Term .
> > >   var Y : List{X} .
> > >   var N : Nat .
> > >   op map : X List{X} -> List{X} .
> > >   op inc : Nat -> Nat .
> > >   
> > >   eq map(F, Y) = append( [F(head(Y))], map(F, tail(Y)) ) .
> > >   eq inc(X) = X + 1 .
> > > endm 
> > > 
> > > then red map(inc, [1 2 3])  should reduce to [2 3 4].
> > > 
> > > I'm not sure how to make this parse and work correctly. Thank you for 
> > > your help in advance.
> > 
>