Method: FunctionApplyObligation(PExp, List, ILexNameToken, IPOContextStack, IPogAssistantFactory)

1: /*******************************************************************************
2: *
3: *        Copyright (C) 2008 Fujitsu Services Ltd.
4: *
5: *        Author: Nick Battle
6: *
7: *        This file is part of VDMJ.
8: *
9: *        VDMJ is free software: you can redistribute it and/or modify
10: *        it under the terms of the GNU General Public License as published by
11: *        the Free Software Foundation, either version 3 of the License, or
12: *        (at your option) any later version.
13: *
14: *        VDMJ is distributed in the hope that it will be useful,
15: *        but WITHOUT ANY WARRANTY; without even the implied warranty of
16: *        MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
17: *        GNU General Public License for more details.
18: *
19: *        You should have received a copy of the GNU General Public License
20: *        along with VDMJ. If not, see <http://www.gnu.org/licenses/>.
21: *
22: ******************************************************************************/
23:
24: package org.overture.pog.obligation;
25:
26: import java.util.List;
27:
28: import org.overture.ast.analysis.AnalysisException;
29: import org.overture.ast.expressions.APreExp;
30: import org.overture.ast.expressions.AVariableExp;
31: import org.overture.ast.expressions.PExp;
32: import org.overture.ast.intf.lex.ILexNameToken;
33: import org.overture.ast.types.ABooleanBasicType;
34: import org.overture.pog.pub.IPOContextStack;
35: import org.overture.pog.pub.IPogAssistantFactory;
36: import org.overture.pog.pub.POType;
37:
38: public class FunctionApplyObligation extends ProofObligation
39: {
40:         private static final long serialVersionUID = -7146271970744572457L;
41:
42:         public FunctionApplyObligation(PExp root, List<PExp> args,
43:                         ILexNameToken prename, IPOContextStack ctxt, IPogAssistantFactory af)
44:                         throws AnalysisException
45:         {
46:                 super(root, POType.FUNC_APPLY, ctxt, root.getLocation(), af);
47:
48:                 /**
49:                  * If the root is an expression that evaluates to a function, we do not know which pre_f to call and prename is
50:                  * null. So we use the "pre_(root, args)" form. If the prename is defined, like "pre_f" then we can use
51:                  * "pre_f(args)". We should not attempt to create an obligation if there is no precondition - ie. we should not
52:                  * be here if prename is "".
53:                  */
54:
55:•                if (prename == null) // Root is an expression, so use pre_(root, args)
56:                 {
57:                         // pre_(root, args)
58:                         APreExp preExp = new APreExp();
59:                         preExp.setType(new ABooleanBasicType());
60:                         preExp.setFunction(root.clone());
61:                         preExp.setArgs(cloneListPExp(args));
62:                         stitch = preExp.clone();
63:                         valuetree.setPredicate(ctxt.getPredWithContext(preExp));
64:                 } else
65:                 {
66:                         // pre_f(args)
67:                         AVariableExp varExp = getVarExp(prename);
68:                         varExp.setType(root.getType().clone());
69:                         PExp pred = getApplyExp(varExp, cloneListPExp(args));
70:                         pred.setType(new ABooleanBasicType());
71:                         stitch = pred.clone();
72:                         valuetree.setPredicate(ctxt.getPredWithContext(pred));
73:                 }
74:         }
75:
76: }