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.overturetool.vdmj.expressions;
25
26 import org.overturetool.vdmj.definitions.Definition;
27 import org.overturetool.vdmj.definitions.DefinitionList;
28 import org.overturetool.vdmj.lex.LexLocation;
29 import org.overturetool.vdmj.pog.PODefContext;
30 import org.overturetool.vdmj.pog.POContextStack;
31 import org.overturetool.vdmj.pog.ProofObligationList;
32 import org.overturetool.vdmj.runtime.Context;
33 import org.overturetool.vdmj.util.Utils;
34 import org.overturetool.vdmj.values.Value;
35
36 public class DefExpression extends LetDefExpression
37 {
38 private static final long serialVersionUID = 1L;
39
40 public DefExpression(LexLocation location,
41 DefinitionList equalsDefs, Expression expression)
42 {
43 super(location, equalsDefs, expression);
44 }
45
46 @Override
47 public String toString()
48 {
49 return "def " + Utils.listToString(localDefs) + " in\n" + expression;
50 }
51
52 @Override
53 public Value eval(Context ctxt)
54 {
55 breakpoint.check(location, ctxt);
56
57 Context evalContext = new Context(location, "def expression", ctxt);
58
59 for (Definition d: localDefs)
60 {
61 evalContext.put(d.getNamedValues(evalContext));
62 }
63
64 return expression.eval(evalContext);
65 }
66
67 @Override
68 public ProofObligationList getProofObligations(POContextStack ctxt)
69 {
70 ProofObligationList obligations = localDefs.getProofObligations(ctxt);
71
72 ctxt.push(new PODefContext(this));
73 obligations.addAll(expression.getProofObligations(ctxt));
74 ctxt.pop();
75
76 return obligations;
77 }
78
79 @Override
80 public String kind()
81 {
82 return "def";
83 }
84 }