I'm reading the module prepost, and there are a few issues I would like to raise. Disclaimer: I have never programmed in Stratego, the code is most certainly wrong. 1. The complete file ==================== For reference. imports liblib ContractC strategies SearchFunDecl = alltd({ ?|InitDeclarator[ ~Declarator: <id>~ ]| ; debug ; oncetd(?|DirectDeclarator[ ~ID: fun_name~ ]|) ; oncetd( ?|DirectDeclarator[ DirectDeclarator(ParameterTypeList) PreCondition-opt PostCondition-opt ]| ; !PreCondition-opt ; if ?|PreCondition?[ ]| then !|Statement[ ; ]| => pre else ?|PreCondition?[ precondition { ~Assertion+: pre~ } ]| end ; !PostCondition-opt ; if ?|PostCondition?[ ]| then !|Statement[ ; ]| => post ; !|ReturnValueDeclaration?[ ]| => ret else ?|PostCondition?[ postcondition ~ReturnValueDeclaration?: ret~ { ~Assertion+: post~ } ]| end ; !|DirectDeclarator[ DirectDeclarator(ParameterTypeList) ]|) ; rules (PrePost : fun_name -> (pre, ret, post)) }) SearchFunDef = alltd({ ?|ExternalDeclaration[ ~FunctionDefinition: <id> ~ ]| ; oncetd(?|DirectDeclarator[ ~ID: fun_name ~ ]| ; where(<PrePost> fun_name => (pre, ret, post)) ; oncetd(?|BlockItemList[ BlockItem-iter ]| ; !|BlockItemList[ ~BlockItem+: <concat> [ [|BlockItem[ ~CompoundStatement: pre ~ ]|, |BlockItem[ ~CompoundStatement: post ~ ]|], BlockItem-iter ]~]| )) }) prepost = io-wrap(SearchFunDecl ; SearchFunDef) 2. The strategies ================= First of all, why the heck should the alltd be in the rules? And BTW, why the rules are strategies here? As a first improvement, I propose to move the alltd down to the prepost strategy. prepost = io-wrap(alltd (FunDecl) ; alltd (FunDef)) Then you see that there are two alltd. Although this allows to have declarations after the implementation (which is indeed a feature) it goes against the spirit of C. Therefore it should read prepost = io-wrap(alltd (FunDecl ; FunDef)) Also, *save the space*! What is this fashion of starting to implement immediately after `='? FunDecl = { ?|InitDeclarator[ ~Declarator: <id>~ ]| ; debug ; oncetd(?|DirectDeclarator[ ~ID: fun_name~ ]|) ; oncetd( ?|DirectDeclarator[ DirectDeclarator(ParameterTypeList) PreCondition-opt PostCondition-opt ]| ; !PreCondition-opt ; if ?|PreCondition?[ ]| then !|Statement[ ; ]| => pre else ?|PreCondition?[ precondition { ~Assertion+: pre~ } ]| end ; !PostCondition-opt ; if ?|PostCondition?[ ]| then !|Statement[ ; ]| => post ; !|ReturnValueDeclaration?[ ]| => ret else ?|PostCondition?[ postcondition ~ReturnValueDeclaration?: ret~ { ~Assertion+: post~ } ]| end ; !|DirectDeclarator[ DirectDeclarator(ParameterTypeList) ]|) ; rules (PrePost : fun_name -> (pre, ret, post)) } FunDef = { ?|ExternalDeclaration[ ~FunctionDefinition: <id> ~ ]| ; oncetd(?|DirectDeclarator[ ~ID: fun_name ~ ]| ; where(<PrePost> fun_name => (pre, ret, post)) ; oncetd(?|BlockItemList[ BlockItem-iter ]| ; !|BlockItemList[ ~BlockItem+: <concat> [ [|BlockItem[ ~CompoundStatement: pre ~ ]|, |BlockItem[ ~CompoundStatement: post ~ ]|], BlockItem-iter ]~]| )) } 3. The rules ============ The rules exist, and that's because they make sense. Why just making strategies? I know, they are equivalent, but so are for and while loops, and you do use both. What is the InitDeclarator that we start by matching? Apparently it is only for debugging, but that's cluttering the code. What are all these oncetd doing here? This is *so wrong*: the code is trying to match various piece instead of just matching what it's looking for. IMNSHO it should look like: FunDecl = ? |Declarator[fn (arg*) pre post]| ; rules (PrePost : fn -> (cs1*, i, cs2*)) where <?|[precondition { cs1* }]|> (pre); <?|[postcondition (i) { cs2* }]|> (post) Is there a nicer way to match pre*, ret and post*? And we'll see for the function with either a pre- xor a postcondition later... The other rule/strategy is also quite not understandable! What is to be done is to create a dynamic rule *that performs the replacement*!!! Not some pseudo table, which completely defeats the whole point of dynamic rules. We want to write something like: where When you put the two together, you have: FunDecl = ? |Declarator[fn (arg*) pre post]| ; rules (InstallContract : |FunctionDefinition[fn (arg*) { stm* }] => !|[fn (arg*) { stm'* }] where <?|[precondition { cs1* }]|> (pre); <?|[postcondition (i) { cs2* }]|> (post); <install-contract (cs1*, i, cs2*)> (stm) => stm'*) And for an experimental start, I propose install-contract (|cs1*, i, cs2*) = !|[ { cs1* } ~id { cs2*} ]| We will see the complications later. I would like to have detailed answers, and particularly from Jesus. I'm quite sure my code is wrong, but it is probably close to correct, my Stratego is far from fluent.
On Thu, 22 Sep 2005 11:13:50 +0200 Akim Demaille <akim@lrde.epita.fr> wrote:
2. The strategies =================
First of all, why the heck should the alltd be in the rules? And BTW, why the rules are strategies here? As a first improvement, I propose to move the alltd down to the prepost strategy.
Then you see that there are two alltd. Although this allows to have declarations after the implementation (which is indeed a feature) it goes against the spirit of C.
I think you are right.
Also, *save the space*! What is this fashion of starting to implement immediately after `='?
I don't know but some code I wrote shows the same phenomenon. It maybe comes from code that I read in papers about Stratego/XT (so, code not indented in the same way that real source code) or from the Stratego/XT, Tiger Compiler and particularly Transformers source code... Yes, I *think* that Transformers code inspired me more than others.
3. The rules ============ The rules exist, and that's because they make sense. Why just making strategies? I know, they are equivalent, but so are for and while loops, and you do use both.
What is the InitDeclarator that we start by matching? Apparently it is only for debugging, but that's cluttering the code. What are all these oncetd doing here? This is *so wrong*: the code is trying to match various piece instead of just matching what it's looking for. IMNSHO it should look like:
InitDeclarator is not only used for debugging. The term projection is important for the rest of the code to work. It enables us to know that a function declaration is found (where the pre- and postconditions are).
What is to be done is to create a dynamic rule *that performs the replacement*!!! Not some pseudo table, which completely defeats the whole point of dynamic rules.
Yes, I understood when you told me that. It was only for commiting an understandable file. Thus Jesus modified the code to show me how to use concrete syntax with our grammars and tools with a simple example.
We want to write something like: where
I didn't understand, or something is missing here... -- Alexandre Borghi "Freedom is the right of all sentient beings." Optimus Prime alexandre.borghi@lrde.org
"Alexandre" == Alexandre BORGHI <alexandre.borghi@lrde.epita.fr> writes:
InitDeclarator is not only used for debugging. The term projection is important for the rest of the code to work. It enables us to know that a function declaration is found (where the pre- and postconditions are).
OK.
We want to write something like: where
I didn't understand, or something is missing here...
Dead sentence, forget about it. Still the current code is much more hairy than (IMHO) it needs to be. Or something is rotten elsewhere in the project.
participants (2)
-
Akim Demaille -
Alexandre BORGHI