HOL-OCL
/
su4sml
1
0
Fork 0
Code Issues Pull Requests Releases Activity

imported OCL parser/type-checker (semester thesis of Manuel Krucker) 

git-svn-id: https://projects.brucker.ch/su4sml/svn/infsec-import/trunk/src/su4sml@6594 3260e6d1-4efc-4170-b0a7-36055960796d
This commit is contained in:
Achim D. Brucker 2007-06-12 18:51:39 +00:00
parent 6e656ff3b1
commit 378034413f
35 changed files with 6856 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

41
src/ocl_parser/ROOT.ML Normal file
View File

@ -0,0 +1,41 @@
(*****************************************************************************
* HOL-OCL - a shallow embedding of OCL into Isabelle/HOL
*
* ROOT.ML - main "ROOT.ML" file for HOL-OCL
* Copyright (C) 2006,2007 Achim D. Brucker <achim@brucker.ch>
* Burkhart Wolff <bwolff@inf.ethz.ch>
*
* This file is part of HOL-OCL.
*
* HOL-OCL is free software; you can redistribute it and/or modify it under
* the terms of the GNU General Public License as published by the Free
* Software Foundation; either version 2 of the License, or (at your option)
* any later version.
*
* HOL-OCL is distributed in the hope that it will be useful, but WITHOUT ANY
* WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
* FOR A PARTICULAR PURPOSE. See the GNU General Public License for more
* details.
*
* You should have received a copy of the GNU General Public License along
* with this program; if not, write to the Free Software Foundation, Inc.,
* 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
******************************************************************************)
OS.FileSys.chDir "ml-yacc-lib";
use "root.sml";
OS.FileSys.chDir "..";
use "library.sml";
use "context_declarations.sml";
use "preprocessor.sml";
use "type_checker.sml";
use "make_classifier_list.sml";
use "ocl.grm.sig";
use "ocl.lex.sml";
nonfix THEN;
use "ocl.grm.sml";
use "parser.sml";
use "fix_types.sml";
use "model_import.sml";

81
src/ocl_parser/STATUS Normal file
View File

@ -0,0 +1,81 @@
*** Company ***
parsing: passed
preprocess: passed
typecheck: passed
update: passed
encode: passed
==> overall: passed
*** ebank ***
parsing: passed
preprocess: passed
typecheck: passed
update: passed
encode: passed
==> overall: passed
*** encoding_example ***
parsing: passed
preprocess: passed
typecheck: passed
update: passed
encoding: passed
==> overall: passed
*** isp ***
parsing: passed
preprocess: passed
typecheck: passed
update: passed
encode: passed
==> overall: passed
*** Royals and Loyals ***
parsing: passed
preprocess: passed
typecheck: passed
update: passed
encode: passed
==> overall: passed
*** simple ***
parsing: passed
preprocess: passed
typecheck: passed
update: passed
encode: passed
==> overall: passed
*** stack ***
parsing: passed
preprocess: passed
typecheck: passed
update: passed
encode: passed
==> overall: passed
*** digraph ***
parsing: passed
preprocess: passed
typecheck: passed
update: passed
encode: passed
==> overall: passed
*** vehicles ***
parsing: passed
preprocess: passed
typecheck: passed
update: passed
encode: passed
==> overall: passed

307
src/ocl_parser/context_declarations.sml Normal file
View File

@ -0,0 +1,307 @@
(*****************************************************************************
* SML OCL 2.0 Parser - Parser/TypeChecker for OCL 2.0 written in SML(NJ)
*
* context_declaration.sml - main "ROOT.ML" file for HOL-OCL
* Copyright (C) 2007 Manuel P. Krucker <mkrucker@ethz.ch>
*
* This file is part of HOL-OCL.
*
* HOL-OCL is free software; you can redistribute it and/or modify it under
* the terms of the GNU General Public License as published by the Free
* Software Foundation; either version 2 of the License, or (at your option)
* any later version.
*
* HOL-OCL is distributed in the hope that it will be useful, but WITHOUT ANY
* WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
* FOR A PARTICULAR PURPOSE. See the GNU General Public License for more
* details.
*
* You should have received a copy of the GNU General Public License along
* with this program; if not, write to the Free Software Foundation, Inc.,
* 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
*****************************************************************************)
signature CONTEXT =
sig
(* datatypes *)
datatype ConditionType = pre | post | body
datatype AttrOrAssoc = derive | init | def
datatype context =
Empty_context of string *
Rep_OclTerm.OclTerm (* expression *)
| Inv of string list * (* context *)
string option * (* name of invariant *)
Rep_OclTerm.OclTerm (* invariant expression *)
| Attr of string list * (* context *)
Rep_OclType.OclType * (* type *)
AttrOrAssoc * (* {Init|Derive} *)
Rep_OclTerm.OclTerm (* init_or_der_value *)
| Cond of string list * (* context *)
string * (* name of operation *)
(string * Rep_OclType.OclType) list * (* signature of operation *)
Rep_OclType.OclType * (* result *)
ConditionType * (* {Pre | Post | Body} *)
string option * (* name of precondition *)
Rep_OclTerm.OclTerm (* preondition expression *)
| Guard of string list * (* context *) (* not yet supported *)
string option * (* name *)
Rep_OclTerm.OclTerm (* expression *)
(* exceptions *)
exception Error of string
exception wrongOperation of string
(* operations *)
val add_source : Rep_OclTerm.OclTerm * Rep_OclTerm.OclTerm -> Rep_OclTerm.OclTerm
val nest_source : Rep_OclTerm.OclTerm list -> Rep_OclTerm.OclTerm
val cond_type_to_string : ConditionType -> string
val package_of_context : context -> string list
val real_path : string list -> string list
val gen_let_term : (string * Rep_OclType.OclType * Rep_OclTerm.OclTerm) list -> Rep_OclTerm.OclTerm -> Rep_OclTerm.OclTerm
val gen_literal_term : string * Rep_OclType.OclType -> Rep_OclTerm.OclTerm * Rep_OclType.OclType
val extend_path : context -> string list -> context
val list_extend_path : string list -> context list -> context list
val real_signature : ('a * 'b) list -> ('a * 'b) list
val cxt_list2string : context list -> string
val guard_list : string list * (string option * Rep_OclTerm.OclTerm) list -> context list
val inv_list : string list * (string option * Rep_OclTerm.OclTerm) list -> context list
val cond_list : string list * (string * Rep_OclType.OclType) list * (ConditionType * string option * Rep_OclTerm.OclTerm) list -> context list
val attr_list : string list * Rep_OclType.OclType * (AttrOrAssoc * Rep_OclTerm.OclTerm) list -> context list
(* values *)
val OclLibPackage : string
end
structure Context:CONTEXT =
struct
open Rep_Core
open Rep_OclType
open Rep_OclTerm
open OclLibrary
open Ext_Library
type operation = Rep_Core.operation
datatype ConditionType = pre | post | body
datatype AttrOrAssoc = derive | init | def
datatype context =
Empty_context of string *
Rep_OclTerm.OclTerm (* expression *)
| Inv of string list * (* context *)
string option * (* name of invariant *)
Rep_OclTerm.OclTerm (* invariant expression *)
| Attr of string list * (* context *)
Rep_OclType.OclType * (* type *)
AttrOrAssoc * (* {Init|Derive} *)
Rep_OclTerm.OclTerm (* init_or_der_value *)
| Cond of string list * (* context *)
string * (* name of operation *)
(string * Rep_OclType.OclType) list * (* signature of operation *)
Rep_OclType.OclType * (* result *)
ConditionType * (* {Pre | Post | Body} *)
string option * (* name of precondition *)
Rep_OclTerm.OclTerm (* preondition expression *)
| Guard of string list * (* context *) (* not yet supported *)
string option * (* name *)
Rep_OclTerm.OclTerm (* expression *)
exception Error of string
exception wrongOperation of string
exception NestSourceError of string
val OclLibPackage = OclLibrary.OclLibPackage
(* RETURN: string *)
fun cond_type_to_string pre = "pre"
| cond_type_to_string post = "post"
| cond_type_to_string body = "body"
(* RETURN: string list *)
fun package_of_context (Empty_context (_,_)) = raise Error "Empty Context in Context.package_of"
| package_of_context (Inv (p,_,_)) = rev (tl (rev p))
| package_of_context (Attr (p,_,_,_)) = rev ((tl o tl) (rev p))
| package_of_context (Cond (p,_,_,_,_,_,_)) = rev ((tl o tl) (rev p))
| package_of_context (Guard (_,_,_)) = raise Error "Guard not supported in in Context.package_of"
(* switch arguments *)
fun switch f (a,b) = f (b,a)
(* RETURN: Path *)
fun real_path ([]) = []
| real_path ([x]) = []
| real_path (x::tail) = x::real_path tail
(* RETURN: OclTerm /* a let term */ *)
fun gen_let_term [] expr = expr
| gen_let_term ((str,typ,exp)::init_var_list_tail) expr =
(Let (str,typ,exp,DummyT,gen_let_term init_var_list_tail expr,DummyT))
(* RETURN: OclTerm *)
fun gen_literal_term (name,typ) = (Literal (name,typ),typ)
(* prefix the path of an OclTerm with 'ext_path' *)
fun extend_path (Attr (path,typ,selector,expr)) ext_path = Attr (ext_path@path,prefix_type ext_path typ,selector,prefix_expression ext_path expr)
| extend_path (Cond (path,name,sign,res,selector,name_sel,expr)) ext_path =
Cond (ext_path@path,name,sign,res,selector,name_sel,prefix_expression ext_path expr)
| extend_path (Inv (path, name, expr)) ext_path = Inv (ext_path@path,name,prefix_expression ext_path expr)
| extend_path (Guard (path, name, expr)) ext_path = Guard (ext_path@path, name, prefix_expression ext_path expr)
(* RETURN: context list *)
(* prefixes the path of every list member with 'ext_path' *)
fun list_extend_path s [] = []
| list_extend_path ext_path ((Empty_context (s,t))::(context_list_tail)) =
[(Empty_context(s,t))]@(list_extend_path ext_path context_list_tail)
| list_extend_path ext_path ((Inv(path,st,t))::(context_list_tail)) =
[(extend_path (Inv(path,st,t)) ext_path)]@(list_extend_path ext_path context_list_tail)
| list_extend_path ext_path ((Attr(path,ty,aoa,t))::(context_list_tail)) =
[(extend_path (Attr(path,ty,aoa,t)) ext_path)]@(list_extend_path ext_path context_list_tail)
| list_extend_path ext_path ((Cond(path,s,sig_list,res,con,so,t))::(context_list_tail)) =
[(extend_path (Cond(path,s,sig_list,res,con,so,t)) ext_path)]@(list_extend_path ext_path context_list_tail)
| list_extend_path ext_path ((Guard(path,so,t))::(context_list_tail)) =
[(extend_path (Guard(path,so,t)) ext_path)]@(list_extend_path ext_path context_list_tail)
(* deletes last element of signature which is return type of operation *)
fun real_signature ([]) = []
| real_signature [(name,typ)] = []
| real_signature ((name,typ)::tail) =
(name,typ)::real_signature tail
(* RETURN: OclTerm *)
(* Add to an OclTerm the correct source term 'source' *)
fun add_source (source,(AttributeCall (_, _, path, res_typ ))) =
let
val test = (AttributeCall (source,DummyT,path,res_typ))
val _ = trace low ("source added for AttributeCall..." ^ Ocl2String.ocl2string true test ^ "\n");
in
(AttributeCall (source, DummyT, path, res_typ))
end
| add_source (source,(OperationCall (_,_,path,paras,res_typ))) =
let
val _ = trace low ("source added for OperationCall..." ^ "\n");
in
(OperationCall (source,DummyT,path,paras,res_typ))
end
| add_source (source, Literal(s,t)) = Literal (s,t)
| add_source (source, CollectionLiteral (part_list,typ)) =
let
val _ = trace low ("source added for AttributeCall..." ^ "\n");
in
(CollectionLiteral (part_list,typ))
end
| add_source (source, Iterator(name,iter_vars_list,_,_,body_term,body_typ,res_typ)) =
let
val _ = trace low ("source added for Iterator..." ^ "\n");
in
(Iterator (name,iter_vars_list,source,DummyT,body_term,body_typ,res_typ))
end
| add_source (source, Let(paras)) =
(* let has no source *)
Let(paras)
| add_source (source, If (paras)) =
(* If has no source *)
If (paras)
(* RETURN: OclTerm list *)
fun add_source_to_list source (h::tail) = (add_source (source,h))::tail
(* RETURN: OclTerm *)
(* add sources of a list, when every list element is the
source of the following element.
The last element is initalized with "self", because its
always so in an object oriented language if its no an argument
of an operation, which is checked later.
*)
(* RETURN: OclTerm *)
fun nest_source (OperationCall (sterm,styp,[OclLibPackage,rtyp,"-"],[],res_typ)::tail) =
let
val _ = trace low ("unary_exp_cs Call: '-' ... \n")
in
foldl (switch add_source) (OperationCall (sterm,styp,[OclLibPackage,rtyp,"-"],[],res_typ)) tail
end
| nest_source (OperationCall (sterm,styp,[OclLibPackage,rtyp,"not"],[],res_typ)::tail) =
let
val _ = trace low ("unary_exp_cs Call: 'not' ... \n")
in
foldl (switch add_source) (OperationCall (sterm,styp,[OclLibPackage,rtyp,"not"],[],res_typ)) tail
end
| nest_source term_list =
let
val _ = trace low ("source nested for AttributeCall..." ^ "\n");
val _ = trace low ((Ocl2String.ocl2string true (List.last term_list)) ^ "bla\n");
in
foldl (switch add_source) (Variable ("dummy_source",DummyT)) term_list
end
(* RETURN: context list *)
fun attr_list (context,Typ,[]) =
let
val _ = trace low ("Contextes created form list of Attributes ..." ^ "\n")
in
[]
end
| attr_list (context,Typ,((asser,expr)::tail)) =
let
val _ = trace low ("Contextes created form list of Attributes ..." ^ "\n")
in
(Attr (context,Typ,asser,expr))::(attr_list (context,Typ,tail))
end
(* RETURN: context list *)
fun inv_list (context,[]) =
let
val _ = trace low ("Contextes created form list of invs ..." ^ "\n")
in
[]
end
| inv_list (context,((name,expr)::tail)) =
let
val _ = trace low ("Contextes created form list of invs ..." ^ "\n")
in
(Inv(context,name,expr))::(inv_list (context,tail))
end
(* RETURN: context list *)
fun cond_list (path,sign,[]) =
let
val _ = trace low ("Contextes created form list of conds ..." ^ "\n")
in
[]
end
| cond_list (path,sign,((asser,name_cond,expr)::tail)) =
let
val _ = trace low ("Contextes created form list of conds ..." ^ "\n")
in
Cond(real_path path,List.last path,real_signature sign, #2(List.last sign),asser,name_cond,expr)::cond_list (path,sign,tail)
end
(* RETURN: context list *)
fun guard_list (context,[]) = []
| guard_list (context,(name,expr)::tail) = Guard (context,name,expr)::guard_list (context,tail)
(* RETURN: string *)
fun cxt_list2string ([]) = ""
| cxt_list2string ((Empty_context(s,t))::tail) =
"empty: "^(Ocl2String.ocl2string false t)^"\n"^(cxt_list2string tail)
| cxt_list2string ((Inv(p,s,t))::tail) =
"inv: "^(Ocl2String.ocl2string false t)^"\n"^(cxt_list2string tail)
| cxt_list2string ((Attr(p,ty,a,t))::tail) =
"attr_or_assoc "^(Ocl2String.ocl2string false t)^"\n"^(cxt_list2string tail)
| cxt_list2string ((Cond(p,s,l,ty,c,so,t))::tail) =
"condition: "^(Ocl2String.ocl2string false t)^"\n"^(cxt_list2string tail)
| cxt_list2string ((Guard(p,so,t))::tail) =
"guard: "^(Ocl2String.ocl2string false t)^"\n"^(cxt_list2string tail)
end;

104
src/ocl_parser/examples/encoding_example/encoding_example.xmi Normal file
View File

@ -0,0 +1,104 @@
<?xml version = '1.0' encoding = 'UTF-8' ?>
<XMI xmi.version = '1.2' xmlns:UML = 'org.omg.xmi.namespace.UML' timestamp = 'Wed Feb 01 17:42:30 CET 2006'>
<XMI.header> <XMI.header>
<XMI.documentation>
<XMI.exporter>ArgoUML (using Netbeans XMI Writer version 1.0)</XMI.exporter>
<XMI.exporterVersion>0.20.x</XMI.exporterVersion>
</XMI.documentation>
<XMI.metamodel xmi.name="UML" xmi.version="1.4"/> </XMI.header>
</XMI.header>
<XMI.content>
<UML:Model xmi.id = '.:0000000000000833' name = 'Simple Encoding Example'
isSpecification = 'false' isRoot = 'false' isLeaf = 'false' isAbstract = 'false'>
<UML:Namespace.ownedElement>
<UML:Package xmi.id = '.:0000000000000824' name = 'UML_OCL' isSpecification = 'false'
isRoot = 'false' isLeaf = 'false' isAbstract = 'false'>
<UML:Namespace.ownedElement>
<UML:Class xmi.id = '.:0000000000000821' name = 'String' isSpecification = 'false'
isRoot = 'false' isLeaf = 'false' isAbstract = 'false' isActive = 'false'/>
<UML:DataType xmi.id = '.:0000000000000822' name = 'Real' isSpecification = 'false'
isRoot = 'false' isLeaf = 'false' isAbstract = 'false'/>
<UML:DataType xmi.id = '.:0000000000000823' name = 'Integer' isSpecification = 'false'
isRoot = 'false' isLeaf = 'false' isAbstract = 'false'/>
</UML:Namespace.ownedElement>
</UML:Package>
<UML:Package xmi.id = '.:0000000000000832' name = 'encoding' isSpecification = 'false'
isRoot = 'false' isLeaf = 'false' isAbstract = 'false'>
<UML:Namespace.ownedElement>
<UML:Generalization xmi.id = '.:0000000000000829' isSpecification = 'false'>
<UML:Generalization.child>
<UML:Class xmi.idref = '.:0000000000000828'/>
</UML:Generalization.child>
<UML:Generalization.parent>
<UML:Class xmi.idref = '.:0000000000000831'/>
</UML:Generalization.parent>
</UML:Generalization>
<UML:Class xmi.id = '.:0000000000000831' name = 'A' visibility = 'public'
isSpecification = 'false' isRoot = 'false' isLeaf = 'false' isAbstract = 'false'
isActive = 'false'>
<UML:Classifier.feature>
<UML:Attribute xmi.id = '.:000000000000082C' name = 'i' visibility = 'public'
isSpecification = 'false' ownerScope = 'instance' changeability = 'changeable'
targetScope = 'instance'>
<UML:StructuralFeature.multiplicity>
<UML:Multiplicity xmi.id = '.:000000000000082B'>
<UML:Multiplicity.range>
<UML:MultiplicityRange xmi.id = '.:000000000000082A' lower = '1' upper = '1'/>
</UML:Multiplicity.range>
</UML:Multiplicity>
</UML:StructuralFeature.multiplicity>
<UML:StructuralFeature.type>
<UML:DataType xmi.idref = '.:0000000000000823'/>
</UML:StructuralFeature.type>
</UML:Attribute>
<UML:Operation xmi.id = '.:0000000000000830' name = 'f' visibility = 'public'
isSpecification = 'false' ownerScope = 'instance' isQuery = 'false' concurrency = 'sequential'
isRoot = 'false' isLeaf = 'false' isAbstract = 'false'>
<UML:BehavioralFeature.parameter>
<UML:Parameter xmi.id = '.:000000000000082D' name = 'return' isSpecification = 'false'
kind = 'return'>
<UML:Parameter.type>
<UML:DataType xmi.idref = '.:0000000000000823'/>
</UML:Parameter.type>
</UML:Parameter>
<UML:Parameter xmi.id = '.:000000000000082F' name = 'x' isSpecification = 'false'
kind = 'in'>
<UML:Parameter.defaultValue>
<UML:Expression xmi.id = '.:000000000000082E' language = 'Java' body = ''/>
</UML:Parameter.defaultValue>
<UML:Parameter.type>
<UML:DataType xmi.idref = '.:0000000000000823'/>
</UML:Parameter.type>
</UML:Parameter>
</UML:BehavioralFeature.parameter>
</UML:Operation>
</UML:Classifier.feature>
</UML:Class>
<UML:Class xmi.id = '.:0000000000000828' name = 'B' isSpecification = 'false'
isRoot = 'false' isLeaf = 'false' isAbstract = 'false' isActive = 'false'>
<UML:GeneralizableElement.generalization>
<UML:Generalization xmi.idref = '.:0000000000000829'/>
</UML:GeneralizableElement.generalization>
<UML:Classifier.feature>
<UML:Attribute xmi.id = '.:0000000000000827' name = 'j' visibility = 'public'
isSpecification = 'false' ownerScope = 'instance' changeability = 'changeable'
targetScope = 'instance'>
<UML:StructuralFeature.multiplicity>
<UML:Multiplicity xmi.id = '.:0000000000000826'>
<UML:Multiplicity.range>
<UML:MultiplicityRange xmi.id = '.:0000000000000825' lower = '1' upper = '1'/>
</UML:Multiplicity.range>
</UML:Multiplicity>
</UML:StructuralFeature.multiplicity>
<UML:StructuralFeature.type>
<UML:Class xmi.idref = '.:0000000000000828'/>
</UML:StructuralFeature.type>
</UML:Attribute>
</UML:Classifier.feature>
</UML:Class>
</UML:Namespace.ownedElement>
</UML:Package>
</UML:Namespace.ownedElement>
</UML:Model>
</XMI.content>
</XMI>

11
src/ocl_parser/examples/encoding_example/encoding_example3.ocl Normal file
View File

@ -0,0 +1,11 @@
package encoding
context A::i:Integer
init: 42
context A
inv: i >= 0
context A::f(x:Integer):Integer
pre: x > 0
post: 45 >= x
endpackage

76
src/ocl_parser/examples/simple/classifier_list.sml Normal file
View File

@ -0,0 +1,76 @@
val it =
[Class
{activity_graphs=[],associationends=[],
attributes=[{attr_type=Integer,init=NONE,name="r",scope=InstanceScope,
stereotypes=[],visibility=public}],interfaces=[],
invariant=[],name=["simple","E"],operations=[],
parent=SOME ["simple","B"],stereotypes=[],thyname=NONE},
Class
{activity_graphs=[],associationends=[],
attributes=[{attr_type=Real,init=NONE,name="r",scope=InstanceScope,
stereotypes=[],visibility=public}],interfaces=[],
invariant=[],name=["simple","D"],operations=[],
parent=SOME ["simple","A"],stereotypes=[],thyname=NONE},
Class
{activity_graphs=[],associationends=[],
attributes=[{attr_type=String,init=NONE,name="s",scope=InstanceScope,
stereotypes=[],visibility=public}],interfaces=[],
invariant=[],name=["simple","C"],operations=[],
parent=SOME ["simple","A"],stereotypes=[],thyname=NONE},
Class
{activity_graphs=[],associationends=[],
attributes=[{attr_type=Set (Classifier ["simple","A"]),init=NONE,
name="a",scope=InstanceScope,stereotypes=[],
visibility=public},
{attr_type=Integer,init=NONE,name="j",scope=InstanceScope,
stereotypes=[],visibility=public},
{attr_type=Classifier ["simple","A"],init=NONE,
name="attribA",scope=InstanceScope,stereotypes=[],
visibility=public}],interfaces=[],
invariant=[(SOME "multconstraint_for_aend_a",
OperationCall
(OperationCall
(OperationCall
(AttributeCall
(Variable ("self",Classifier ["simple","B"]),
Classifier ["simple","B"],["simple","B","a"],
Set (Classifier ["simple","A"])),
Set (Classifier ["simple","A"]),
["oclLib","Collection","size"],[],Integer),Integer,
["oclLib","Real",">="],
[(Literal ("1",Integer),Integer)],Boolean),Boolean,
["oclLib","Boolean","and"],
[(OperationCall
(OperationCall
(AttributeCall
(Variable ("self",Classifier ["simple","B"]),
Classifier ["simple","B"],["simple","B","a"],
Set (Classifier ["simple","A"])),
Set (Classifier ["simple","A"]),
["oclLib","Collection","size"],[],Integer),
Integer,["oclLib","Real","<="],
[(Literal ("5",Integer),Integer)],Boolean),Boolean)],
Boolean))],name=["simple","B"],operations=[],parent=NONE,
stereotypes=[],thyname=NONE},
Class
{activity_graphs=[],associationends=[],
attributes=[{attr_type=Classifier ["simple","B"],init=NONE,name="b",
scope=InstanceScope,stereotypes=[],visibility=public},
{attr_type=Integer,init=NONE,name="i",scope=InstanceScope,
stereotypes=[],visibility=public},
{attr_type=Real,init=NONE,name="r",scope=InstanceScope,
stereotypes=[],visibility=public},
{attr_type=Classifier ["simple","B"],init=NONE,
name="attribB",scope=InstanceScope,stereotypes=[],
visibility=public}],interfaces=[],
invariant=[(SOME "multconstraint_for_aend_b",
OperationCall
(AttributeCall
(Variable ("self",Classifier ["simple","A"]),
Classifier ["simple","A"],["simple","A","b"],
Classifier ["simple","B"]),Classifier ["simple","B"],
["oclIsDefined"],[],Boolean))],name=["simple","A"],
operations=[{arguments=[("p",Integer)],isQuery=true,name="m",
postcondition=[],precondition=[],result=Integer,
scope=InstanceScope,visibility=public}],parent=NONE,
stereotypes=[],thyname=NONE}] : Classifier list

35
src/ocl_parser/examples/simple/simple.argo Normal file
View File

@ -0,0 +1,35 @@
<?xml version = "1.0" encoding = "UTF-8" ?>
<!DOCTYPE argo SYSTEM "argo.dtd" >
<argo version="4">
<documentation>
<authorname></authorname>
<version>0.19.7</version>
<description>
</description>
</documentation>
<searchpath href="PROJECT_DIR" />
<searchpath href="PROJECT_DIR" />
<searchpath href="PROJECT_DIR" />
<searchpath href="PROJECT_DIR" />
<searchpath href="PROJECT_DIR" />
<searchpath href="PROJECT_DIR" />
<searchpath href="PROJECT_DIR" />
<searchpath href="PROJECT_DIR" />
<searchpath href="PROJECT_DIR" />
<searchpath href="PROJECT_DIR" />
<searchpath href="PROJECT_DIR" />
<searchpath href="PROJECT_DIR" />
<searchpath href="PROJECT_DIR" />
<searchpath href="PROJECT_DIR" />
<searchpath href="PROJECT_DIR" />
<searchpath href="PROJECT_DIR" />
<searchpath href="PROJECT_DIR" />
<searchpath href="PROJECT_DIR" />
<searchpath href="PROJECT_DIR" />
<member type="xmi" />
<member type="pgml" />
<member type="todo" />
<historyfile name="" />
</argo>

166
src/ocl_parser/examples/simple/simple.ocl Normal file
View File

@ -0,0 +1,166 @@
--
-- Testing OCL syntax variations
--
package simple
-- testing implicit self
-- =====================
context A
inv self_short: i = 5
inv self_long: self.i = 5
inv: self.i=self.attribB.attribA.i
inv: i = attribB.attribA.i
inv iskind: self.oclIsKindOf(A)
inv meth: self.m(1) > 5
inv meth2: self.m(self.i) > 5
inv real: r = 2.45
inv: not Set{1,2,3,4,5} ->isEmpty()
inv: Set{} ->isEmpty()
context B
inv constant: self.j = 42
inv iskind: not self.oclIsKindOf(A)
inv istype: self.oclIsTypeOf(B)
context C
inv cast: self.oclAsType(A).oclIsTypeOf(A)
-- testing named self
-- ==================
-- not supported by dresden-ocl (parser-bug?)
-- ( Cannot parse OCL constraint: expecting: 'derive', 'init')
-- context foo:A
-- inv named_self_short: i=5 -- Dresden
-- inv named_self_foo: foo.i=5 -- Dresden
-- ->size() on non-collection types
-- ================================
-- [Dresden] context A
-- [Dresden] inv: self.i->size() > 0
-- implicit ->asSet()
-- ==================
-- [Dresden] context A
-- [Dresden] inv setshort: self.i->size() > 0
-- [Dresden] inv set_long: self.i->asSet()->size() > 0
-- [Dresden] inv intAsSet: 1->asSet()->includes(1)
-- [Dresden] inv intInclude: 1->includes(1)
-- [Dresden] inv intSizew: 1->size() > 0
-- [Dresden] inv inc: self.i ->includes(4)
-- Operations: pre/post
-- ==============================
context A::m(p:Integer):Integer
pre: p > 0
post: (result = 0 - p) and p > (0-5)
-- Operations: @per
-- ==============================
context A::m(p:Integer):Integer
post pre1: self = self@pre
post pre2: p = i@pre - 5
post pre3: self.i=self.attribB.attribA.i@pre
post pre4: self.i=self.attribB.attribA@pre.i
post pre5: self.i=self.attribB@pre.attribA.i
post pre6: self.i=self@pre.attribB.attribA.i
-- syntactical variants of iterate/forall
-- ======================================
context B
inv forall: self.a->forAll(a:A | a.i = 5)
inv twoforall: self.a->forAll(a:A, b:A | a.i = b.i)
inv existential: self.a->exists(a:A | a.i = 5)
-- shorthand for collect [omg:ocl:2003, p27]
-- =========================================
-- context B
-- inv collect_short: self.a.i = Set{5} -- Dresden
-- inv collect_long: self.a ->collect(i) = Set{5} -- Dresden
-- inv collect_test: self.a.i = 5 -- Dresden
-- inv collect_test2: self.a->collect(i) = 5 -- Dresden
-- inv strange_collect: self.a->size() = 1 implies self.a.i=5 -- Dresden
-- access to top-level path-expressions
-- ====================================
-- context B -- Dresden
-- inv: simple::A.i = 5 -- Dresden
-- types of overloaded infix operations
-- ====================================
context A
inv: r = 1.0
inv: i + r = 10
inv: i + r = 10.0
inv: r = 10.0
inv: r = 10
-- @pre for method calls
-- =====================
context A::m(p:Integer):Integer
post: self.m(4)=5 -- Dresden
post: self@pre.m(4)=5 -- Dresden
post: self.m@pre(4)=5 -- Dresden
-- body vs. post
-- =============
context A::m(p:Integer):Integer
body testbody: p
-- body (recursive)
-- ================
-- context A::m(p:Integer):Integer -- Dresden/HOL-OCL
-- body: p * m(p-1) -- Dresden/HOL-OCL
-- init:
-- =====
context A::i : Integer
init: 0
-- def (attributes):
-- =================
-- should be transformed into the UML model
-- context A
-- def: s:String='' -- Dresden (HOL-OCL)
-- def (method):
-- =================
-- should be transformed into the UML model
-- context A
-- def: fac(n:Integer):Integer = n fac(n-1) -- Dresden (HOL-OCL)
-- derive:
-- =======
-- (transformation into UML model)
-- (derive (attributes) ~~> invariants (class))?
-- context A.r
-- derive: i -- Dresden (HOL-OCL)
-- oclAsType (explicit overriding):
-- ================================
-- context D
-- inv: self.oclAsType(A).r = 0 -- Dresden (HOL-OCL)
-- let expressions
-- ===============
context A::m(p:Integer):Integer -- HOL-OCL
pre: let m:Integer = p+5 in m > 0 -- HOL-OCL
-- operations on sets
-- ==================
context B
inv mt: self.a->isEmpty()
inv full: self.a->notEmpty()
inv un: self.a->union(self.a) = self.a
inv inter: self.a->intersection(self.a) = self.a
endpackage

8
src/ocl_parser/examples/simple/simple.todo Normal file
View File

@ -0,0 +1,8 @@
<?xml version = "1.0" encoding = "UTF-8" ?>
<!DOCTYPE todo SYSTEM "todo.dtd" >
<todo>
<todolist>
</todolist>
<resolvedcritics>
</resolvedcritics>
</todo>

264
src/ocl_parser/examples/simple/simple.xmi Normal file
View File

@ -0,0 +1,264 @@
<?xml version = '1.0' encoding = 'UTF-8' ?>
<XMI xmi.version = '1.2' xmlns:UML = 'org.omg.xmi.namespace.UML' timestamp = 'Tue Nov 08 21:32:56 CET 2005'>
<XMI.header>
<XMI.documentation>
<XMI.exporter>Netbeans XMI Writer</XMI.exporter>
<XMI.exporterVersion>1.0</XMI.exporterVersion>
</XMI.documentation>
</XMI.header>
<XMI.content>
<UML:Model xmi.id = '.:000000000000085C' name = 'Simple Example' isSpecification = 'false'
isRoot = 'false' isLeaf = 'false' isAbstract = 'false'>
<UML:Namespace.ownedElement>
<UML:Package xmi.id = '.:000000000000082F' name = 'UML_OCL' isSpecification = 'false'
isRoot = 'false' isLeaf = 'false' isAbstract = 'false'>
<UML:Namespace.ownedElement>
<UML:Class xmi.id = '.:000000000000082C' name = 'String' isSpecification = 'false'
isRoot = 'false' isLeaf = 'false' isAbstract = 'false' isActive = 'false'/>
<UML:DataType xmi.id = '.:000000000000082D' name = 'Real' isSpecification = 'false'
isRoot = 'false' isLeaf = 'false' isAbstract = 'false'/>
<UML:DataType xmi.id = '.:000000000000082E' name = 'Integer' isSpecification = 'false'
isRoot = 'false' isLeaf = 'false' isAbstract = 'false'/>
</UML:Namespace.ownedElement>
</UML:Package>
<UML:Package xmi.id = '.:000000000000085B' name = 'simple' isSpecification = 'false'
isRoot = 'false' isLeaf = 'false' isAbstract = 'false'>
<UML:Namespace.ownedElement>
<UML:Class xmi.id = '.:0000000000000833' name = 'E' isSpecification = 'false'
isRoot = 'false' isLeaf = 'false' isAbstract = 'false' isActive = 'false'>
<UML:GeneralizableElement.generalization>
<UML:Generalization xmi.idref = '.:0000000000000859'/>
<UML:Generalization xmi.idref = '.:000000000000085A'/>
</UML:GeneralizableElement.generalization>
<UML:Classifier.feature>
<UML:Attribute xmi.id = '.:0000000000000832' name = 'r' visibility = 'public'
isSpecification = 'false' ownerScope = 'instance' changeability = 'changeable'
targetScope = 'instance'>
<UML:StructuralFeature.multiplicity>
<UML:Multiplicity xmi.id = '.:0000000000000831'>
<UML:Multiplicity.range>
<UML:MultiplicityRange xmi.id = '.:0000000000000830' lower = '1' upper = '1'/>
</UML:Multiplicity.range>
</UML:Multiplicity>
</UML:StructuralFeature.multiplicity>
<UML:StructuralFeature.type>
<UML:DataType xmi.idref = '.:000000000000082E'/>
</UML:StructuralFeature.type>
</UML:Attribute>
</UML:Classifier.feature>
</UML:Class>
<UML:Class xmi.id = '.:0000000000000837' name = 'D' isSpecification = 'false'
isRoot = 'false' isLeaf = 'false' isAbstract = 'false' isActive = 'false'>
<UML:GeneralizableElement.generalization>
<UML:Generalization xmi.idref = '.:0000000000000858'/>
</UML:GeneralizableElement.generalization>
<UML:Classifier.feature>
<UML:Attribute xmi.id = '.:0000000000000836' name = 'r' visibility = 'public'
isSpecification = 'false' ownerScope = 'instance' changeability = 'changeable'
targetScope = 'instance'>
<UML:StructuralFeature.multiplicity>
<UML:Multiplicity xmi.id = '.:0000000000000835'>
<UML:Multiplicity.range>
<UML:MultiplicityRange xmi.id = '.:0000000000000834' lower = '1' upper = '1'/>
</UML:Multiplicity.range>
</UML:Multiplicity>
</UML:StructuralFeature.multiplicity>
<UML:StructuralFeature.type>
<UML:DataType xmi.idref = '.:000000000000082D'/>
</UML:StructuralFeature.type>
</UML:Attribute>
</UML:Classifier.feature>
</UML:Class>
<UML:Class xmi.id = '.:000000000000083B' name = 'C' isSpecification = 'false'
isRoot = 'false' isLeaf = 'false' isAbstract = 'false' isActive = 'false'>
<UML:GeneralizableElement.generalization>
<UML:Generalization xmi.idref = '.:0000000000000857'/>
</UML:GeneralizableElement.generalization>
<UML:Classifier.feature>
<UML:Attribute xmi.id = '.:000000000000083A' name = 's' visibility = 'public'
isSpecification = 'false' ownerScope = 'instance' changeability = 'changeable'
targetScope = 'instance'>
<UML:StructuralFeature.multiplicity>
<UML:Multiplicity xmi.id = '.:0000000000000839'>
<UML:Multiplicity.range>
<UML:MultiplicityRange xmi.id = '.:0000000000000838' lower = '1' upper = '1'/>
</UML:Multiplicity.range>
</UML:Multiplicity>
</UML:StructuralFeature.multiplicity>
<UML:StructuralFeature.type>
<UML:Class xmi.idref = '.:000000000000082C'/>
</UML:StructuralFeature.type>
</UML:Attribute>
</UML:Classifier.feature>
</UML:Class>
<UML:Class xmi.id = '.:0000000000000842' name = 'B' visibility = 'public'
isSpecification = 'false' isRoot = 'false' isLeaf = 'false' isAbstract = 'false'
isActive = 'false'>
<UML:Classifier.feature>
<UML:Attribute xmi.id = '.:000000000000083E' name = 'j' visibility = 'public'
isSpecification = 'false' ownerScope = 'instance' changeability = 'changeable'
targetScope = 'instance'>
<UML:StructuralFeature.multiplicity>
<UML:Multiplicity xmi.id = '.:000000000000083D'>
<UML:Multiplicity.range>
<UML:MultiplicityRange xmi.id = '.:000000000000083C' lower = '1' upper = '1'/>
</UML:Multiplicity.range>
</UML:Multiplicity>
</UML:StructuralFeature.multiplicity>
<UML:StructuralFeature.type>
<UML:DataType xmi.idref = '.:000000000000082E'/>
</UML:StructuralFeature.type>
</UML:Attribute>
<UML:Attribute xmi.id = '.:0000000000000841' name = 'attribA' visibility = 'public'
isSpecification = 'false' ownerScope = 'instance' changeability = 'changeable'
targetScope = 'instance'>
<UML:StructuralFeature.multiplicity>
<UML:Multiplicity xmi.id = '.:0000000000000840'>
<UML:Multiplicity.range>
<UML:MultiplicityRange xmi.id = '.:000000000000083F' lower = '1' upper = '1'/>
</UML:Multiplicity.range>
</UML:Multiplicity>
</UML:StructuralFeature.multiplicity>
<UML:StructuralFeature.type>
<UML:Class xmi.idref = '.:000000000000084F'/>
</UML:StructuralFeature.type>
</UML:Attribute>
</UML:Classifier.feature>
</UML:Class>
<UML:Class xmi.id = '.:000000000000084F' name = 'A' visibility = 'public'
isSpecification = 'false' isRoot = 'false' isLeaf = 'false' isAbstract = 'false'
isActive = 'false'>
<UML:Classifier.feature>
<UML:Attribute xmi.id = '.:0000000000000845' name = 'i' visibility = 'public'
isSpecification = 'false' ownerScope = 'instance' changeability = 'changeable'
targetScope = 'instance'>
<UML:StructuralFeature.multiplicity>
<UML:Multiplicity xmi.id = '.:0000000000000844'>
<UML:Multiplicity.range>
<UML:MultiplicityRange xmi.id = '.:0000000000000843' lower = '1' upper = '1'/>
</UML:Multiplicity.range>
</UML:Multiplicity>
</UML:StructuralFeature.multiplicity>
<UML:StructuralFeature.type>
<UML:DataType xmi.idref = '.:000000000000082E'/>
</UML:StructuralFeature.type>
</UML:Attribute>
<UML:Attribute xmi.id = '.:0000000000000848' name = 'r' visibility = 'public'
isSpecification = 'false' ownerScope = 'instance' changeability = 'changeable'
targetScope = 'instance'>
<UML:StructuralFeature.multiplicity>
<UML:Multiplicity xmi.id = '.:0000000000000847'>
<UML:Multiplicity.range>
<UML:MultiplicityRange xmi.id = '.:0000000000000846' lower = '1' upper = '1'/>
</UML:Multiplicity.range>
</UML:Multiplicity>
</UML:StructuralFeature.multiplicity>
<UML:StructuralFeature.type>
<UML:DataType xmi.idref = '.:000000000000082D'/>
</UML:StructuralFeature.type>
</UML:Attribute>
<UML:Operation xmi.id = '.:000000000000084B' name = 'm' visibility = 'public'
isSpecification = 'false' ownerScope = 'instance' isQuery = 'true' concurrency = 'sequential'
isRoot = 'false' isLeaf = 'false' isAbstract = 'false'>
<UML:BehavioralFeature.parameter>
<UML:Parameter xmi.id = '.:0000000000000849' name = 'return' isSpecification = 'false'
kind = 'return'>
<UML:Parameter.type>
<UML:DataType xmi.idref = '.:000000000000082E'/>
</UML:Parameter.type>
</UML:Parameter>
<UML:Parameter xmi.id = '.:000000000000084A' name = 'p' isSpecification = 'false'
kind = 'in'>
<UML:Parameter.type>
<UML:DataType xmi.idref = '.:000000000000082E'/>
</UML:Parameter.type>
</UML:Parameter>
</UML:BehavioralFeature.parameter>
</UML:Operation>
<UML:Attribute xmi.id = '.:000000000000084E' name = 'attribB' visibility = 'public'
isSpecification = 'false' ownerScope = 'instance' changeability = 'changeable'
targetScope = 'instance'>
<UML:StructuralFeature.multiplicity>
<UML:Multiplicity xmi.id = '.:000000000000084D'>
<UML:Multiplicity.range>
<UML:MultiplicityRange xmi.id = '.:000000000000084C' lower = '1' upper = '1'/>
</UML:Multiplicity.range>
</UML:Multiplicity>
</UML:StructuralFeature.multiplicity>
<UML:StructuralFeature.type>
<UML:Class xmi.idref = '.:0000000000000842'/>
</UML:StructuralFeature.type>
</UML:Attribute>
</UML:Classifier.feature>
</UML:Class>
<UML:Association xmi.id = '.:0000000000000856' name = 'foo' isSpecification = 'false'
isRoot = 'false' isLeaf = 'false' isAbstract = 'false'>
<UML:Association.connection>
<UML:AssociationEnd xmi.id = '.:0000000000000852' name = 'a' visibility = 'public'
isSpecification = 'false' isNavigable = 'true' ordering = 'unordered' aggregation = 'none'
targetScope = 'instance' changeability = 'changeable'>
<UML:AssociationEnd.multiplicity>
<UML:Multiplicity xmi.id = '.:0000000000000851'>
<UML:Multiplicity.range>
<UML:MultiplicityRange xmi.id = '.:0000000000000850' lower = '1' upper = '5'/>
</UML:Multiplicity.range>
</UML:Multiplicity>
</UML:AssociationEnd.multiplicity>
<UML:AssociationEnd.participant>
<UML:Class xmi.idref = '.:000000000000084F'/>
</UML:AssociationEnd.participant>
</UML:AssociationEnd>
<UML:AssociationEnd xmi.id = '.:0000000000000855' name = 'b' visibility = 'public'
isSpecification = 'false' isNavigable = 'true' ordering = 'unordered' aggregation = 'none'
targetScope = 'instance' changeability = 'changeable'>
<UML:AssociationEnd.multiplicity>
<UML:Multiplicity xmi.id = '.:0000000000000854'>
<UML:Multiplicity.range>
<UML:MultiplicityRange xmi.id = '.:0000000000000853' lower = '1' upper = '1'/>
</UML:Multiplicity.range>
</UML:Multiplicity>
</UML:AssociationEnd.multiplicity>
<UML:AssociationEnd.participant>
<UML:Class xmi.idref = '.:0000000000000842'/>
</UML:AssociationEnd.participant>
</UML:AssociationEnd>
</UML:Association.connection>
</UML:Association>
<UML:Generalization xmi.id = '.:0000000000000857' isSpecification = 'false'>
<UML:Generalization.child>
<UML:Class xmi.idref = '.:000000000000083B'/>
</UML:Generalization.child>
<UML:Generalization.parent>
<UML:Class xmi.idref = '.:000000000000084F'/>
</UML:Generalization.parent>
</UML:Generalization>
<UML:Generalization xmi.id = '.:0000000000000858' isSpecification = 'false'>
<UML:Generalization.child>
<UML:Class xmi.idref = '.:0000000000000837'/>
</UML:Generalization.child>
<UML:Generalization.parent>
<UML:Class xmi.idref = '.:000000000000084F'/>
</UML:Generalization.parent>
</UML:Generalization>
<UML:Generalization xmi.id = '.:0000000000000859' isSpecification = 'false'>
<UML:Generalization.child>
<UML:Class xmi.idref = '.:0000000000000833'/>
</UML:Generalization.child>
<UML:Generalization.parent>
<UML:Class xmi.idref = '.:0000000000000842'/>
</UML:Generalization.parent>
</UML:Generalization>
<UML:Generalization xmi.id = '.:000000000000085A' isSpecification = 'false'>
<UML:Generalization.child>
<UML:Class xmi.idref = '.:0000000000000833'/>
</UML:Generalization.child>
<UML:Generalization.parent>
<UML:Class xmi.idref = '.:0000000000000842'/>
</UML:Generalization.parent>
</UML:Generalization>
</UML:Namespace.ownedElement>
</UML:Package>
</UML:Namespace.ownedElement>
</UML:Model>
</XMI.content>
</XMI>

16
src/ocl_parser/examples/simple/simple1.ocl Normal file
View File

@ -0,0 +1,16 @@
--
-- Testing OCL syntax variations
--
package simple
-- testing implicit self
-- =====================
context A
inv self_short: i = 5
inv self_long: self.i = 5
-- inv: self.i=self.attribB.attribA.i
-- inv: i = attribB.attribA.i
-- inv iskind: self.oclIsKindOf(A)
-- inv meth: self.m(1) > 5
-- inv meth2: self.m(self.i) > 5
inv real: r = 2.45
endpackage

674
src/ocl_parser/examples/simple/simple_ClassDiagram.pgml Normal file
View File

@ -0,0 +1,674 @@
<?xml version="1.0" encoding="UTF-8" ?>
<!DOCTYPE pgml SYSTEM "pgml.dtd">
<pgml description="org.argouml.uml.diagram.static_structure.ui.UMLClassDiagram|.:000000000000085B"
name="Class Diagram"
>
<group name="Fig0"
description="org.argouml.uml.diagram.static_structure.ui.FigClass[299, 232, 61, 57]pathVisible=false;operationsVisible=true;attributesVisible=true"
href=".:0000000000000833"
fill="1"
fillcolor="white"
stroke="1"
strokecolor="black"
>
<private>
</private>
<rectangle name="Fig0.0"
x="299"
y="232"
width="61"
height="57"
fill="1"
fillcolor="white"
stroke="0"
strokecolor="black"
/>
<text name="Fig0.1"
x="299"
y="232"
fill="1"
fillcolor="white"
stroke="0"
strokecolor="black"
font="Dialog"
textsize="10"
></text>
<text name="Fig0.2"
x="299"
y="232"
fill="1"
fillcolor="white"
stroke="0"
strokecolor="red"
font="Dialog"
textsize="10"
>E</text>
<group name="Fig0.3"
description="org.argouml.uml.diagram.ui.FigOperationsCompartment[299, 270, 61, 19]"
fill="1"
fillcolor="white"
stroke="1"
strokecolor="black"
>
<private>
</private>
<rectangle name="Fig0.3.0"
x="299"
y="270"
width="61"
height="19"
fill="1"
fillcolor="white"
stroke="1"
strokecolor="black"
/>
</group>
<group name="Fig0.4"
description="org.argouml.uml.diagram.ui.FigAttributesCompartment[299, 252, 61, 19]"
fill="1"
fillcolor="white"
stroke="1"
strokecolor="black"
>
<private>
</private>
<rectangle name="Fig0.4.0"
x="299"
y="252"
width="61"
height="19"
fill="1"
fillcolor="white"
stroke="1"
strokecolor="black"
/>
<text name="Fig0.4.1"
x="300"
y="253"
fill="0"
fillcolor="white"
stroke="0"
strokecolor="black"
font="Dialog"
textsize="10"
>r : Integer</text>
</group>
<rectangle name="Fig0.5"
x="299"
y="232"
width="61"
height="57"
fill="0"
fillcolor="white"
stroke="1"
strokecolor="black"
/>
</group>
<group name="Fig1"
description="org.argouml.uml.diagram.static_structure.ui.FigClass[176, 224, 61, 57]pathVisible=false;operationsVisible=true;attributesVisible=true"
href=".:0000000000000837"
fill="1"
fillcolor="white"
stroke="1"
strokecolor="black"
>
<private>
</private>
<rectangle name="Fig1.0"
x="176"
y="224"
width="61"
height="57"
fill="1"
fillcolor="white"
stroke="0"
strokecolor="black"
/>
<text name="Fig1.1"
x="176"
y="224"
fill="1"
fillcolor="white"
stroke="0"
strokecolor="black"
font="Dialog"
textsize="10"
></text>
<text name="Fig1.2"
x="176"
y="224"
fill="1"
fillcolor="white"
stroke="0"
strokecolor="red"
font="Dialog"
textsize="10"
>D</text>
<group name="Fig1.3"
description="org.argouml.uml.diagram.ui.FigOperationsCompartment[176, 262, 61, 19]"
fill="1"
fillcolor="white"
stroke="1"
strokecolor="black"
>
<private>
</private>
<rectangle name="Fig1.3.0"
x="176"
y="262"
width="61"
height="19"
fill="1"
fillcolor="white"
stroke="1"
strokecolor="black"
/>
</group>
<group name="Fig1.4"
description="org.argouml.uml.diagram.ui.FigAttributesCompartment[176, 244, 61, 19]"
fill="1"
fillcolor="white"
stroke="1"
strokecolor="black"
>
<private>
</private>
<rectangle name="Fig1.4.0"
x="176"
y="244"
width="61"
height="19"
fill="1"
fillcolor="white"
stroke="1"
strokecolor="black"
/>
<text name="Fig1.4.1"
x="177"
y="245"
fill="0"
fillcolor="white"
stroke="0"
strokecolor="black"
font="Dialog"
textsize="10"
>r : Real</text>
</group>
<rectangle name="Fig1.5"
x="176"
y="224"
width="61"
height="57"
fill="0"
fillcolor="white"
stroke="1"
strokecolor="black"
/>
</group>
<group name="Fig2"
description="org.argouml.uml.diagram.static_structure.ui.FigClass[32, 224, 61, 57]pathVisible=false;operationsVisible=true;attributesVisible=true"
href=".:000000000000083B"
fill="1"
fillcolor="white"
stroke="1"
strokecolor="black"
>
<private>
</private>
<rectangle name="Fig2.0"
x="32"
y="224"
width="61"
height="57"
fill="1"
fillcolor="white"
stroke="0"
strokecolor="black"
/>
<text name="Fig2.1"
x="32"
y="224"
fill="1"
fillcolor="white"
stroke="0"
strokecolor="black"
font="Dialog"
textsize="10"
></text>
<text name="Fig2.2"
x="32"
y="224"
fill="1"
fillcolor="white"
stroke="0"
strokecolor="red"
font="Dialog"
textsize="10"
>C</text>
<group name="Fig2.3"
description="org.argouml.uml.diagram.ui.FigOperationsCompartment[32, 262, 61, 19]"
fill="1"
fillcolor="white"
stroke="1"
strokecolor="black"
>
<private>
</private>
<rectangle name="Fig2.3.0"
x="32"
y="262"
width="61"
height="19"
fill="1"
fillcolor="white"
stroke="1"
strokecolor="black"
/>
</group>
<group name="Fig2.4"
description="org.argouml.uml.diagram.ui.FigAttributesCompartment[32, 244, 61, 19]"
fill="1"
fillcolor="white"
stroke="1"
strokecolor="black"
>
<private>
</private>
<rectangle name="Fig2.4.0"
x="32"
y="244"
width="61"
height="19"
fill="1"
fillcolor="white"
stroke="1"
strokecolor="black"
/>
<text name="Fig2.4.1"
x="33"
y="245"
fill="0"
fillcolor="white"
stroke="0"
strokecolor="black"
font="Dialog"
textsize="10"
>s : String</text>
</group>
<rectangle name="Fig2.5"
x="32"
y="224"
width="61"
height="57"
fill="0"
fillcolor="white"
stroke="1"
strokecolor="black"
/>
</group>
<group name="Fig3"
description="org.argouml.uml.diagram.static_structure.ui.FigClass[297, 58, 63, 74]pathVisible=false;operationsVisible=true;attributesVisible=true"
href=".:0000000000000842"
fill="1"
fillcolor="white"
stroke="1"
strokecolor="black"
>
<private>
</private>
<rectangle name="Fig3.0"
x="297"
y="58"
width="63"
height="74"
fill="1"
fillcolor="white"
stroke="0"
strokecolor="black"
/>
<text name="Fig3.1"
x="297"
y="58"
fill="1"
fillcolor="white"
stroke="0"
strokecolor="black"
font="Dialog"
textsize="10"
></text>
<text name="Fig3.2"
x="297"
y="58"
fill="1"
fillcolor="white"
stroke="0"
strokecolor="red"
font="Dialog"
textsize="10"
>B</text>
<group name="Fig3.3"
description="org.argouml.uml.diagram.ui.FigOperationsCompartment[297, 114, 63, 18]"
fill="1"
fillcolor="white"
stroke="1"
strokecolor="black"
>
<private>
</private>
<rectangle name="Fig3.3.0"
x="297"
y="114"
width="63"
height="18"
fill="1"
fillcolor="white"
stroke="1"
strokecolor="black"
/>
</group>
<group name="Fig3.4"
description="org.argouml.uml.diagram.ui.FigAttributesCompartment[297, 78, 63, 37]"
fill="1"
fillcolor="white"
stroke="1"
strokecolor="black"
>
<private>
</private>
<rectangle name="Fig3.4.0"
x="297"
y="78"
width="63"
height="37"
fill="1"
fillcolor="white"
stroke="1"
strokecolor="black"
/>
<text name="Fig3.4.1"
x="298"
y="79"
fill="0"
fillcolor="white"
stroke="0"
strokecolor="black"
font="Dialog"
textsize="10"
>j : Integer</text>
<text name="Fig3.4.2"
x="298"
y="97"
fill="0"
fillcolor="white"
stroke="0"
strokecolor="black"
font="Dialog"
textsize="10"
>attribA : A</text>
</group>
<rectangle name="Fig3.5"
x="297"
y="58"
width="63"
height="74"
fill="0"
fillcolor="white"
stroke="1"
strokecolor="black"
/>
</group>
<group name="Fig4"
description="org.argouml.uml.diagram.static_structure.ui.FigClass[40, 40, 126, 91]pathVisible=false;operationsVisible=true;attributesVisible=true"
href=".:000000000000084F"
fill="1"
fillcolor="white"
stroke="1"
strokecolor="black"
>
<private>
</private>
<rectangle name="Fig4.0"
x="40"
y="40"
width="126"
height="91"
fill="1"
fillcolor="white"
stroke="0"
strokecolor="black"
/>
<text name="Fig4.1"
x="40"
y="40"
fill="1"
fillcolor="white"
stroke="0"
strokecolor="black"
font="Dialog"
textsize="10"
></text>
<text name="Fig4.2"
x="40"
y="40"
fill="1"
fillcolor="white"
stroke="0"
strokecolor="red"
font="Dialog"
textsize="10"
>A</text>
<group name="Fig4.3"
description="org.argouml.uml.diagram.ui.FigOperationsCompartment[40, 113, 126, 18]"
fill="1"
fillcolor="white"
stroke="1"
strokecolor="black"
>
<private>
</private>
<rectangle name="Fig4.3.0"
x="40"
y="113"
width="126"
height="18"
fill="1"
fillcolor="white"
stroke="1"
strokecolor="black"
/>
<text name="Fig4.3.1"
x="41"
y="114"
fill="0"
fillcolor="white"
stroke="0"
strokecolor="black"
font="Dialog"
textsize="10"
>m(p : Integer) : Integer</text>
</group>
<group name="Fig4.4"
description="org.argouml.uml.diagram.ui.FigAttributesCompartment[40, 60, 126, 54]"
fill="1"
fillcolor="white"
stroke="1"
strokecolor="black"
>
<private>
</private>
<rectangle name="Fig4.4.0"
x="40"
y="60"
width="126"
height="54"
fill="1"
fillcolor="white"
stroke="1"
strokecolor="black"
/>
<text name="Fig4.4.1"
x="41"
y="61"
fill="0"
fillcolor="white"
stroke="0"
strokecolor="black"
font="Dialog"
textsize="10"
>i : Integer</text>
<text name="Fig4.4.2"
x="41"
y="78"
fill="0"
fillcolor="white"
stroke="0"
strokecolor="black"
font="Dialog"
textsize="10"
>r : Real</text>
<text name="Fig4.4.3"
x="41"
y="95"
fill="0"
fillcolor="white"
stroke="0"
strokecolor="black"
font="Dialog"
textsize="10"
>attribB : B</text>
</group>
<rectangle name="Fig4.5"
x="40"
y="40"
width="126"
height="91"
fill="0"
fillcolor="white"
stroke="1"
strokecolor="black"
/>
</group>
<group name="Fig5"
description="org.argouml.uml.diagram.ui.FigAssociation"
href=".:0000000000000856"
stroke="1"
strokecolor="black"
>
<private>
sourcePortFig="Fig4"
destPortFig="Fig3"
sourceFigNode="Fig4"
destFigNode="Fig3"
</private>
<path name="Fig5.0"
description="org.tigris.gef.presentation.FigPoly"
fill="0"
fillcolor="white"
stroke="1"
strokecolor="black"
>
<moveto x="166"
y="58" />
<lineto x="297"
y="58" />
</path>
</group>
<group name="Fig6"
description="org.argouml.uml.diagram.ui.FigGeneralization"
href=".:0000000000000857"
stroke="1"
strokecolor="black"
>
<private>
sourcePortFig="Fig2"
destPortFig="Fig4"
sourceFigNode="Fig2"
destFigNode="Fig4"
</private>
<path name="Fig6.0"
description="org.tigris.gef.presentation.FigPoly"
fill="0"
fillcolor="white"
stroke="1"
strokecolor="black"
>
<moveto x="65"
y="224" />
<lineto x="65"
y="187" />
<lineto x="98"
y="187" />
<lineto x="98"
y="131" />
</path>
</group>
<group name="Fig7"
description="org.argouml.uml.diagram.ui.FigGeneralization"
href=".:0000000000000858"
stroke="1"
strokecolor="black"
>
<private>
sourcePortFig="Fig1"
destPortFig="Fig4"
sourceFigNode="Fig1"
destFigNode="Fig4"
</private>
<path name="Fig7.0"
description="org.tigris.gef.presentation.FigPoly"
fill="0"
fillcolor="white"
stroke="1"
strokecolor="black"
>
<moveto x="206"
y="224" />
<lineto x="206"
y="187" />
<lineto x="98"
y="187" />
<lineto x="98"
y="131" />
</path>
</group>
<group name="Fig8"
description="org.argouml.uml.diagram.ui.FigGeneralization"
href=".:000000000000085A"
stroke="1"
strokecolor="black"
>
<private>
sourcePortFig="Fig0"
destPortFig="Fig3"
sourceFigNode="Fig0"
destFigNode="Fig3"
</private>
<path name="Fig8.0"
description="org.tigris.gef.presentation.FigPoly"
fill="0"
fillcolor="white"
stroke="1"
strokecolor="black"
>
<moveto x="328"
y="232" />
<lineto x="328"
y="132" />
</path>
</group>
</pgml>

239
src/ocl_parser/fix_types.sml Normal file
View File

@ -0,0 +1,239 @@
signature FixTypes = sig
val type_of : Rep_OclTerm.OclTerm -> Rep_OclTerm.OclType
val src_type_of : Rep_OclTerm.OclTerm -> Rep_OclTerm.OclType
val IntegerLiteralToReal : Rep_OclTerm.OclTerm -> Rep_OclTerm.OclTerm
val downcastCollection : Rep_OclTerm.OclTerm -> Rep_OclTerm.OclTerm
val transformForHolOcl : Rep_OclTerm.OclTerm -> Rep_OclTerm.OclTerm
val upCastClassifier : Rep_OclTerm.OclTerm -> Rep_OclTerm.OclTerm
val transform_invariant: (Rep_OclTerm.OclTerm -> Rep_OclTerm.OclTerm) -> Rep_Core.Classifier -> Rep_Core.Classifier
val transform_invariants: (Rep_OclTerm.OclTerm -> Rep_OclTerm.OclTerm) -> Rep_Core.Classifier list -> Rep_Core.Classifier list
exception FixTyping of string
end
structure FixTyping = struct
open Rep_OclTerm
exception FixTyping of string
fun error t = let val _ = print (t^"\n") in raise FixTyping t end
fun type_of (Literal (_,t )) = t
| type_of (CollectionLiteral (_,t)) = t
| type_of (If (_,_,_,_,_,_,t)) = t
| type_of (AssociationEndCall (_,_,_,t)) = t
| type_of (AttributeCall(_,_,_,t)) = t
| type_of (OperationCall (_,_,_,_,t)) = t
| type_of (OperationWithType (_,_,_,_,t)) = t
| type_of (Variable (_,t)) = t
| type_of (Iterate (_,_,_,_,_,_,_,_,t)) = t
| type_of (Iterator (_,_,_,_,_,_,t)) = t
fun src_type_of (Literal (_,_)) = error "Literal: src_type_of"
| src_type_of (CollectionLiteral (_,_)) = error "CollectionLitearal: src_type_of"
| src_type_of (If (_,_,_,_,_,_,_)) = error "if: src_type_of"
| src_type_of (AssociationEndCall (_,t,_,_)) = t
| src_type_of (AttributeCall(_,t,_,_)) = t
| src_type_of (OperationCall (_,t,_,_,_)) = t
| src_type_of (OperationWithType (_,t,_,_,_)) = t
| src_type_of (Variable (_,_)) = error "Variable: src_type_of"
| src_type_of (Iterate (_,_,_,_,_,_,_,_,_)) = error "Iterate: src_type_of"
| src_type_of (Iterator (_,_,_,_,_,_,_)) = error "Iterator: src_type_of"
fun downcastCollection (exp as Literal (_,_)) = exp
| downcastCollection (exp as (CollectionLiteral (_,_)))
= exp
| downcastCollection (If (c,ct,t,tt,e,et,typ))
= (If (downcastCollection c,ct,downcastCollection t,tt,downcastCollection e,et,typ))
| downcastCollection (AssociationEndCall (src,srcT,a,t))
=(AssociationEndCall(downcastCollection src,srcT,a,t))
| downcastCollection (AttributeCall(src,srcT,a,t))
= (AttributeCall(downcastCollection src,srcT,a,t))
| downcastCollection (OperationCall (src,st,p,params,typ))
= (let
fun dca (a, at) = (downcastCollection a, at)
in
(case st of
Collection _ => (let
val dc_src = downcastCollection src
in
(OperationCall (dc_src,type_of (dc_src),p ,map dca params,typ))
end)
| _ => (OperationCall (downcastCollection src, st,p ,map dca params,typ))
)
end
)
| downcastCollection (OperationWithType (src,srcT,n,argTyp,typ))
= (OperationWithType (downcastCollection src,srcT,n,argTyp,typ))
| downcastCollection (exp as (Variable (_,_)))
= exp
| downcastCollection (Let (var, varT, rhs, rhsT, term, typ))
= (Let (var, varT, downcastCollection rhs, rhsT, downcastCollection term, typ))
| downcastCollection (Iterate (vars, result, resultT, resultTerm, src,srct,body,bodyT,typ))
= (Iterate (vars, result, resultT,resultTerm, downcastCollection src,srct,downcastCollection body,bodyT,typ))
| downcastCollection (Iterator (name, vars, src,srct,body,bodyT,typ))
= (Iterator (name, vars, downcastCollection src,srct,downcastCollection body,bodyT,typ))
fun setTypeToReal (Literal(v,Real)) = Literal(v,Real)
| setTypeToReal (Literal(v,Integer)) = Literal(v,Real)
| setTypeToReal exp = let
val src = IntegerLiteralToReal exp
in
if (type_of src = Integer)
then OperationWithType (exp,Integer,"oclAsType",Real,Real)
else exp
end
and IntegerLiteralToReal (exp as Literal (_,_)) = exp
| IntegerLiteralToReal (exp as (CollectionLiteral (_,_)))
= exp
| IntegerLiteralToReal (If (c,ct,t,tt,e,et,typ))
= (If (IntegerLiteralToReal c,ct,IntegerLiteralToReal t,tt,IntegerLiteralToReal e,et,typ))
| IntegerLiteralToReal (AssociationEndCall (src,srcT,a,t))
=(AssociationEndCall(IntegerLiteralToReal src,srcT,a,t))
| IntegerLiteralToReal (AttributeCall(src,srcT,a,t))
= (AttributeCall(IntegerLiteralToReal src,srcT,a,t))
| IntegerLiteralToReal (OperationCall (src,Real,p,[(arg, Real)],typ))
= let
val srcT = type_of src
val argT = type_of arg
in
case (srcT, argT) of
(Real, Real) => (OperationCall (IntegerLiteralToReal src,Real,p,
[(IntegerLiteralToReal arg, Real)],typ))
| (Integer, Real) => (OperationCall (IntegerLiteralToReal(setTypeToReal src),Real,p,
[(arg, Real)],typ))
| (Real, Integer) => (OperationCall (IntegerLiteralToReal src,Real,p,
[(setTypeToReal arg, Real)],typ))
| (Integer, Integer) => (OperationCall (IntegerLiteralToReal src,Integer,p,
[(arg, Integer)],typ))
end
| IntegerLiteralToReal (OperationCall (src,srcT',["oclLib","OclAny","="],[(arg, argT')],typ))
= let
val src = IntegerLiteralToReal src
val arg = IntegerLiteralToReal arg
val srcT = type_of (src )
val argT = type_of arg
in
(case (srcT, argT) of
(Real, Real) => (OperationCall (src,srcT,["oclLib","OclAny","="],[(arg, argT)],typ))
| (Integer, Real) => (OperationCall ((setTypeToReal src),Real,["oclLib","OclAny","="],
[(arg, Real)],typ))
| (Real, Integer) => (OperationCall (src,Real,["oclLib","OclAny","="],
[(setTypeToReal arg, Real)],typ))
| (Integer, Integer) => (OperationCall (src,srcT,["oclLib","OclAny","="],[(arg, argT)],typ))
| (_, _) => (OperationCall (src,srcT,["oclLib","OclAny","="],[(arg, argT)],typ)))
end
| IntegerLiteralToReal (OperationCall (src,srcT,p,args,typ))
= (OperationCall (IntegerLiteralToReal src,srcT, p,
map (fn (a, aT) => (IntegerLiteralToReal a, aT)) args ,typ))
| IntegerLiteralToReal (OperationWithType (src,srcT,n,argTyp,typ))
= (OperationWithType (IntegerLiteralToReal src,srcT,n,argTyp,typ))
| IntegerLiteralToReal (exp as (Variable (_,_)))
= exp
| IntegerLiteralToReal (Let (var, varT, rhs, rhsT, term, typ))
= (Let (var, varT, IntegerLiteralToReal rhs, rhsT, IntegerLiteralToReal term, typ))
| IntegerLiteralToReal (Iterate (vars, result, resultT, resultTerm, src,srct,body,bodyT,typ))
= (Iterate (vars, result, resultT,resultTerm, IntegerLiteralToReal src,srct,IntegerLiteralToReal body,bodyT,typ))
| IntegerLiteralToReal (Iterator (name, vars, src,srct,body,bodyT,typ))
= (Iterator (name, vars, IntegerLiteralToReal src,srct,IntegerLiteralToReal body,bodyT,typ))
fun transform_body_in_post Op =
let
fun transform_body_in_postconstraint body =
let
val result_type = type_of body
val result = Rep_OclTerm.Variable ("result",result_type)
val equal = ["oclLib","OclAny","="]
val body_type = result_type
in
Rep_OclTerm.OperationCall (result, result_type,
equal,[(body,body_type)],
Rep_OclType.Boolean)
end
val post_representation = map (fn (n,c) => (n,transform_body_in_postconstraint c)) (Rep_Core.body_of_op Op)
val post = Rep_Core.postcondition_of_op Op
in
Rep_Core.update_postcondition (post@post_representation) Op
end
fun transform_body_in_post_of_c c =
let
val Ops = map (transform_body_in_post) (Rep_Core.operations_of c)
in
Rep_Core.update_operations Ops c
end
fun transformForHolOcl t = (IntegerLiteralToReal o downcastCollection) t
fun transform_pre f Op =
let
val pre = map (fn (n,i) => (n, f i)) (Rep_Core.precondition_of_op Op)
in
Rep_Core.update_precondition pre Op
end
fun transform_post f Op =
let
val post = map (fn (n,i) => (n, f i)) (Rep_Core.postcondition_of_op Op)
in
Rep_Core.update_postcondition post Op
end
fun transform_pre_of_c f c =
let
val Ops = map (transform_pre f) (Rep_Core.operations_of c)
in
Rep_Core.update_operations Ops c
end
fun transform_post_of_c f c =
let
val Ops = map (transform_post f) (Rep_Core.operations_of c)
in
Rep_Core.update_operations Ops c
end
fun transform_invariant f c =
let
val invariant = map (fn (n,i) => (n, f i)) (Rep_Core.invariant_of c)
in
Rep_Core.update_invariant invariant c
end
fun transform_invariants f cl = map (transform_invariant f) cl
fun transform_pres f cl = map (transform_pre_of_c f) cl
fun transform_posts f cl = map (transform_post_of_c f) cl
fun transform_bodys_in_posts cl = map (transform_body_in_post_of_c) cl
fun transform_ocl_spec f =
(transform_pres f) o (transform_posts f) o (transform_invariants f) o transform_bodys_in_posts
end
(*
fun print_depth n =
(Control.Print.printDepth := n div 2;
Control.Print.printLength := n);
val cl = ModelImport.import
"/home/brucker/infsec/teaching/theses/semesterarbeiten/2006_mkrucker_ocl/examples/company/company.zargo"
"/home/brucker/infsec/teaching/theses/semesterarbeiten/2006_mkrucker_ocl/examples/company/company.ocl" []
*)

64
src/ocl_parser/isar/isar_setup.sml Normal file
View File

@ -0,0 +1,64 @@
(*****************************************************************************
* HOL-OCL - a shallow embedding of OCL into Isabelle/HOL
*
* model_import. - main "ROOT.ML" file for HOL-OCL
* Copyright (C) 2006,2007 Achim D. Brucker <achim@brucker.ch>
*
* This file is part of HOL-OCL.
*
* HOL-OCL is free software; you can redistribute it and/or modify it under
* the terms of the GNU General Public License as published by the Free
* Software Foundation; either version 2 of the License, or (at your option)
* any later version.
*
* HOL-OCL is distributed in the hope that it will be useful, but WITHOUT ANY
* WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
* FOR A PARTICULAR PURPOSE. See the GNU General Public License for more
* details.
*
* You should have received a copy of the GNU General Public License along
* with this program; if not, write to the Free Software Foundation, Inc.,
* 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
*****************************************************************************)
OS.FileSys.chDir "..";
use "ROOT.ML";
OS.FileSys.chDir "isar";
structure isar_import_setup =
struct
structure P = OuterParse and K = OuterKeyword;
fun load_xmiOclT ((xmiFile,oclFile),excludedPackages) thy =
let
fun load_mds xmiFile oclFile thy =
let
val model = map Rep.normalize (ModelImport.import xmiFile oclFile excludedPackages)
val thy = rep_encoder.add_classifiers model thy;
in
thy
end
val thy = load_mds xmiFile oclFile thy
in
thy
end
val load_xmiOclP =
OuterSyntax.command "import_model" "import UML/OCL specification"
OuterKeyword.thy_script
((P.name -- (Scan.optional P.name "")
-- (Scan.optional (P.$$$ "[" |-- P.list1 P.name --| P.$$$ "]") [] ))
>> (fn((xmi,ocl),exPackages) =>
(Toplevel.theory ( fn thy => load_xmiOclT ((xmi,ocl),exPackages) thy))))
val _ = OuterSyntax.add_parsers [load_xmiOclP];
end

70
src/ocl_parser/isar/test.thy Normal file
View File

@ -0,0 +1,70 @@
theory test
imports
OCL
begin
welcome
ML{*
use "isar_setup.sml";
*}
welcome
(*
import_model "/home/brucker/infsec/teaching/theses/semesterarbeiten/2006_mkrucker_ocl/examples/company/company.zargo"
"/home/brucker/infsec/teaching/theses/semesterarbeiten/2006_mkrucker_ocl/examples/company/company.ocl"
*)
welcome
(*
import_model "/home/brucker/infsec/teaching/theses/semesterarbeiten/2006_mkrucker_ocl/examples/ebank/ebank.zargo"
"/home/brucker/infsec/teaching/theses/semesterarbeiten/2006_mkrucker_ocl/examples/ebank/ebank.ocl"
*)
welcome
(*
import_model "/home/brucker/infsec/teaching/theses/semesterarbeiten/2006_mkrucker_ocl/examples/encoding_example/encoding_example.zargo"
"/home/brucker/infsec/teaching/theses/semesterarbeiten/2006_mkrucker_ocl/examples/encoding_example/encoding_example.ocl"
*)
welcome
(*
import_model "/home/brucker/infsec/teaching/theses/semesterarbeiten/2006_mkrucker_ocl/examples/isp/isp.zargo"
"/home/brucker/infsec/teaching/theses/semesterarbeiten/2006_mkrucker_ocl/examples/isp/isp.ocl"
*)
welcome
(*
import_model "/home/brucker/infsec/teaching/theses/semesterarbeiten/2006_mkrucker_ocl/examples/royals_and_loyals/royals_and_loyals.zargo"
"/home/brucker/infsec/teaching/theses/semesterarbeiten/2006_mkrucker_ocl/examples/royals_and_loyals/royals_and_loyals.ocl"
*)
welcome
(*
holocl_params [op_semantics=invoke]
import_model "/home/brucker/infsec/teaching/theses/semesterarbeiten/2006_mkrucker_ocl/examples/simple/simple.zargo"
"/home/brucker/infsec/teaching/theses/semesterarbeiten/2006_mkrucker_ocl/examples/simple/simple.ocl"
*)
welcome
(*
import_model "/home/brucker/infsec/teaching/theses/semesterarbeiten/2006_mkrucker_ocl/examples/stack/stack.zargo"
"/home/brucker/infsec/teaching/theses/semesterarbeiten/2006_mkrucker_ocl/examples/stack/stack.ocl"
*)
welcome
(*
import_model "/home/brucker/infsec/teaching/theses/semesterarbeiten/2006_mkrucker_ocl/examples/digraph/digraph.zargo"
"/home/brucker/infsec/teaching/theses/semesterarbeiten/2006_mkrucker_ocl/examples/digraph/digraph.ocl"
*)
welcome
(*
import_model "/home/brucker/infsec/teaching/theses/semesterarbeiten/2006_mkrucker_ocl/examples/vehicles/vehicles.zargo"
"/home/brucker/infsec/teaching/theses/semesterarbeiten/2006_mkrucker_ocl/examples/vehicles/vehicles.ocl"
*)
welcome
end

945
src/ocl_parser/library.sml Normal file
View File

@ -0,0 +1,945 @@
(*****************************************************************************
* SML OCL 2.0 Parser - Parser/TypeChecker for OCL 2.0 written in SML(NJ)
*
* library.sml - main "ROOT.ML" file for HOL-OCL
* Copyright (C) 2007 Manuel P. Krucker <mkrucker@ethz.ch>
*
* This file is part of HOL-OCL.
*
* HOL-OCL is free software; you can redistribute it and/or modify it under
* the terms of the GNU General Public License as published by the Free
* Software Foundation; either version 2 of the License, or (at your option)
* any later version.
*
* HOL-OCL is distributed in the hope that it will be useful, but WITHOUT ANY
* WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
* FOR A PARTICULAR PURPOSE. See the GNU General Public License for more
* details.
*
* You should have received a copy of the GNU General Public License along
* with this program; if not, write to the Free Software Foundation, Inc.,
* 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
*****************************************************************************)
signature EXT_LIBRARY =
sig
(* operations with parents *)
val class_of_parent : Rep_Core.Classifier -> Rep_Core.Classifier list -> Rep_Core.Classifier
val type_of_parent : Rep_Core.Classifier -> Rep_OclType.OclType
(* classifiers and packages *)
val class_of_type : Rep_OclType.OclType -> Rep_Core.Classifier list -> Rep_Core.Classifier
val get_classifier : Rep_OclTerm.OclTerm -> Rep_Core.Classifier list -> Rep_Core.Classifier
val package_of_template_parameter : Rep_OclType.OclType -> string list
(* operations for types *)
val type_equals : Rep_OclType.OclType -> Rep_OclType.OclType -> bool
val prefix_type : string list -> Rep_OclType.OclType -> Rep_OclType.OclType
val flatten_type : Rep_OclType.OclType -> Rep_OclType.OclType
val template_parameter : Rep_OclType.OclType -> Rep_OclType.OclType
val isColl_Type : Rep_OclType.OclType -> bool
val replace_templ_para : Rep_OclType.OclType -> Rep_OclType.OclType -> Rep_OclType.OclType
val string_to_type : string list -> Rep_OclType.OclType
val correct_type_for_CollLiteral : Rep_OclType.OclType -> Rep_OclTerm.CollectionPart -> bool
val type_of_CollPart : Rep_OclTerm.CollectionPart -> Rep_OclType.OclType
val dispatch_collection : (string * Rep_OclType.OclType) -> Rep_OclType.OclType
(* operations for terms *)
val prefix_expression : string list -> Rep_OclTerm.OclTerm -> Rep_OclTerm.OclTerm
val type_of_term : Rep_OclTerm.OclTerm -> Rep_OclType.OclType
val find_operation : string -> Rep_Core.operation list -> Rep_Core.operation
val find_attribute : string -> Rep_Core.attribute list -> Rep_Core.attribute
(* operations for inheritance *)
val conforms_to : Rep_OclType.OclType -> Rep_OclType.OclType -> Rep_Core.Classifier list -> bool
val upcast : (Rep_OclTerm.OclTerm * Rep_OclType.OclType) -> Rep_OclTerm.OclTerm
val args_interfereable : (string * Rep_OclType.OclType) list -> (Rep_OclTerm.OclTerm * Rep_OclType.OclType) list -> Rep_Core.Classifier list -> bool
val interfere_args : (string * Rep_OclType.OclType) list -> (Rep_OclTerm.OclTerm * Rep_OclType.OclType) list -> Rep_Core.Classifier list -> (Rep_OclTerm.OclTerm * Rep_OclType.OclType) list
val interfere_methods : (Rep_Core.Classifier * Rep_Core.operation) list -> Rep_OclTerm.OclTerm -> (Rep_OclTerm.OclTerm * Rep_OclType.OclType) list -> Rep_Core.Classifier list -> Rep_OclTerm.OclTerm
val interfere_attrs_or_assocends: (Rep_Core.Classifier * Rep_Core.attribute option * Rep_Core.associationend option) list -> Rep_OclTerm.OclTerm -> Rep_Core.Classifier list -> Rep_OclTerm.OclTerm
val get_overloaded_methods : Rep_Core.Classifier -> string -> Rep_Core.Classifier list -> (Rep_Core.Classifier * Rep_Core.operation) list
val get_overloaded_attrs_or_assocends : Rep_Core.Classifier -> string -> Rep_Core.Classifier list -> (Rep_Core.Classifier * Rep_Core.attribute option * Rep_Core.associationend option) list
val get_meth : Rep_OclTerm.OclTerm -> string -> (Rep_OclTerm.OclTerm * Rep_OclType.OclType) list -> Rep_Core.Classifier list -> Rep_OclTerm.OclTerm
val get_attr_or_assoc : Rep_OclTerm.OclTerm -> string -> Rep_Core.Classifier list -> Rep_OclTerm.OclTerm
(* operations/values for debugging/logging *)
val trace : int -> string -> unit
val log_level : int ref
val zero : int
val high : int
val medium : int
val low : int
val development : int
(* exceptions *)
exception InterferenceError of string
exception TemplateInstantiationError of string
exception NoModelReferenced of string
exception GetClassifierError of string
exception TemplateError of string
exception NoCollectionTypeError of Rep_OclType.OclType
exception NoSuchAttributeError of string
exception NoSuchAssociationEndError of string
exception NoSuchOperationError of string
end
structure Ext_Library:EXT_LIBRARY =
struct
open Rep_Core
open Rep_OclType
open Rep_OclTerm
open OclLibrary
exception InterferenceError of string
exception TemplateInstantiationError of string
exception NoModelReferenced of string
exception GetClassifierError of string
exception TemplateError of string
exception NoCollectionTypeError of OclType
exception NoSuchAttributeError of string
exception NoSuchAssociationEndError of string
exception NoSuchOperationError of string
(* Error logging *)
(* default value *)
val log_level = ref 5
(* debugging-levels *)
val zero = 0
val high = 5
val medium = 20
val low = 100
val development = 200
(* RETURN: unit *)
fun trace lev s = if (lev <= !log_level ) then print(s) else ()
(* RETURN: OclType *)
fun dispatch_collection (selector,typ) =
case selector of
"Set" => Set (typ)
| "Sequence" => Sequence (typ)
| "Collection" => Collection (typ)
| "OrderedSet" => OrderedSet (typ)
| "Bag" => Bag (typ)
| _ => DummyT
(* RETURN: Boolean *)
fun correct_type_for_CollLiteral coll_typ (CollectionItem (term,typ)) =
if (typ = coll_typ) then
true
else
false
| correct_type_for_CollLiteral coll_typ (CollectionRange (term1,term2,typ)) =
if (typ = coll_typ) then
true
else
false
(* RETURN: operation *)
fun find_operation op_name [] = raise NoSuchOperationError ("no such operation")
| find_operation op_name ((oper:operation)::tail) =
if (op_name = #name oper)
then
let
val _ = trace low ("Operation found ... " ^ "\n");
in
oper
end
else
let
val _ = trace low ("no match: next op ..." ^ (#name oper) ^ "\n")
in
find_operation op_name tail
end
(* RETURN: attribute *)
fun find_attribute attr_name [] =
let
val _ = trace low ("Error ... " ^ "\n")
in
raise (NoSuchAttributeError ("Error: no attribute '"^attr_name^" found"))
end
| find_attribute attr_name ((a:attribute)::attribute_list) =
if (attr_name = #name a) then
let
val _ = trace low ("Attribute found ... " ^ "\n")
in
(a)
end
else
let
val _ = trace low ("Attribute not found ... " ^ "\n")
in
(find_attribute attr_name attribute_list)
end
(* RETURN: OclType *)
fun flatten_type (Set(Set(t))) = Set(t)
| flatten_type (Set(Collection(t))) = Set(t)
| flatten_type (Set(Bag(t))) = Set(t)
| flatten_type (Set(OrderedSet(t))) = Set(t)
| flatten_type (Set(Sequence(t))) = Set(t)
| flatten_type (Collection(Set(t))) = Collection(t)
| flatten_type (Collection(Bag(t))) = Collection(t)
| flatten_type (Collection(OrderedSet(t))) = Collection(t)
| flatten_type (Collection(Sequence(t))) = Collection(t)
| flatten_type (Collection(Collection(t))) = Collection(t)
| flatten_type (OrderedSet(Collection(t))) = OrderedSet(t)
| flatten_type (OrderedSet(Bag(t))) = OrderedSet(t)
| flatten_type (OrderedSet(OrderedSet(t))) = OrderedSet(t)
| flatten_type (OrderedSet(Sequence(t))) = OrderedSet(t)
| flatten_type (OrderedSet(Set(t))) = OrderedSet(t)
| flatten_type (Bag(Collection(t))) = Bag(t)
| flatten_type (Bag(Bag(t))) = Bag(t)
| flatten_type (Bag(OrderedSet(t))) = Bag(t)
| flatten_type (Bag(Sequence(t))) = Bag(t)
| flatten_type (Bag(Set(t))) = Bag(t)
| flatten_type (Sequence(Collection(t))) = Sequence(t)
| flatten_type (Sequence(Bag(t))) = Sequence(t)
| flatten_type (Sequence(OrderedSet(t))) = Sequence(t)
| flatten_type (Sequence(Sequence(t))) = Sequence(t)
| flatten_type (Sequence(Set(t))) = Sequence(t)
| flatten_type typ = typ
(* RETURN: bool *)
fun member x [] = false
| member x (h::tail) =
if (x = h) then
true
else
member x tail
(* RETURN: Path *)
fun real_path ([]) = []
| real_path ([x]) = []
| real_path (x::tail) = x::real_path tail
(* RETURN: Boolean *)
fun isColl_Type (Set(x)) = true
| isColl_Type (Sequence(x)) = true
| isColl_Type (OrderedSet(x)) = true
| isColl_Type (Bag(x)) = true
| isColl_Type (Collection(x)) = true
| isColl_Type _ = false
(* RETURN: OclTerm *)
fun type_of_term (Literal (s,typ)) = typ
| type_of_term (AttributeCall (t,typ,p,res_typ)) = res_typ
| type_of_term (AssociationEndCall (t,typ,p,res_typ)) = res_typ
| type_of_term (OperationCall (t,typ,p,l,res_typ)) = res_typ
| type_of_term (Variable (s,typ)) = typ
| type_of_term (CollectionLiteral (set,typ)) = typ
| type_of_term (Iterator (_,_,_,_,_,_,res_typ)) = res_typ
| type_of_term (If(_,_,_,_,_,_,res_typ)) = res_typ
| type_of_term (OperationWithType (_,_,_,_,res_typ)) = res_typ
| type_of_term (Let (_,_,_,_,_,res_typ)) = res_typ
| type_of_term (Iterate (_,_,_,_,_,_,_,_,res_typ)) = res_typ
fun type_of_CollPart (CollectionItem (term,typ)) = typ
| type_of_CollPart (CollectionRange (term1,term2,typ)) = typ
(* RETURN: OclType *)
fun type_of_parent (Class {parent,...}) =
let
val _ = trace development ("type_of_parent : Class{parent,...} \n")
in
( case parent of
NONE => OclAny
| SOME (t) => t
)
end
| type_of_parent (Primitive {parent, ...}) =
( case parent of
NONE => OclAny
| SOME (t) => t
)
| type_of_parent (Interface {parents, ...}) = List.hd parents
| type_of_parent (Template{classifier,...}) =
let
val _ = trace development ("type_of_parent: Template {classifier,...} \n")
in
type_of_parent classifier
end
(* RETURN: string list *)
fun adjust_path [] [] = []
| adjust_path [] list = list
| adjust_path (h1::tail1) (h2::tail2) =
if (h1 = h2)
then (h1::(adjust_path tail1 tail2))
else (h1::tail1)@(h2::tail2)
(* RETURN: OclType *)
fun prefix_type [] typ = typ
| prefix_type h (Classifier (path)) = Classifier (h@[List.last path])
| prefix_type h (Set (t)) = Set (prefix_type h t)
| prefix_type h (Collection (t)) = Collection (prefix_type h t)
| prefix_type h (OrderedSet (t)) = OrderedSet (prefix_type h t)
| prefix_type h (Sequence (t)) = Sequence (prefix_type h t)
| prefix_type h (Bag (t)) = Bag (prefix_type h t)
| prefix_type h basic_type = basic_type
(* RETURN: (string * OclType) list *)
fun prefix_signature ext_path [] = []
| prefix_signature ext_path ((s,typ)::tail) =
(s,prefix_type ext_path typ)::(prefix_signature ext_path tail)
(* RETURN: CollectionPart *)
fun prefix_collectionpart ext_path (CollectionItem (term,typ)) =
(CollectionItem (prefix_expression ext_path term,typ))
| prefix_collectionpart ext_path (CollectionRange (first_term,last_term,typ)) =
(CollectionRange (prefix_expression ext_path first_term,prefix_expression ext_path last_term,typ))
(* RETURN: OclTerm *)
and prefix_expression ext_path (Variable (s,t)) = (Variable (s,t))
| prefix_expression ext_path (Literal(s,t)) = Literal (s,t)
| prefix_expression ext_path (AttributeCall (sterm,stype,path,res_typ)) =
(AttributeCall (prefix_expression ext_path sterm,stype,path,res_typ))
| prefix_expression ext_path (OperationCall (sterm,stype,path,args,res_typ)) =
(OperationCall (prefix_expression ext_path sterm,stype,path,args,res_typ))
| prefix_expression ext_path (Iterator (name,iter_vars,sterm,styp,expr,expr_typ,res_typ)) =
let
val prefixed_vars = List.map (fn a => (#1 a,prefix_type ext_path (#2 a))) iter_vars
in
Iterator (name,prefixed_vars,prefix_expression ext_path sterm,styp,prefix_expression ext_path expr,expr_typ,res_typ)
end
| prefix_expression ext_path (Let (var_name,var_type,rhs_term,rhs_type,expr,expr_type)) =
(Let (var_name,prefix_type ext_path var_type,rhs_term,rhs_type,prefix_expression ext_path expr,expr_type))
| prefix_expression ext_path (If (cond,cond_type,then_e,then_type,else_e,else_type,res_type)) =
(If (prefix_expression ext_path cond,cond_type,prefix_expression ext_path then_e,then_type,prefix_expression ext_path else_e,else_type,res_type))
| prefix_expression ext_path (OperationWithType (sterm,stype,para_name,para_type,res_type)) =
(OperationWithType (prefix_expression ext_path sterm,stype,para_name,para_type,res_type))
| prefix_expression ext_path (CollectionLiteral (coll_part_list,typ)) =
(CollectionLiteral (List.map (prefix_collectionpart ext_path) coll_part_list,typ))
(* RETURN: OclType *)
fun template_parameter typ =
case typ of
Set(t) => t
| Sequence(t) => t
| Bag(t) => t
| Collection(t) => t
| OrderedSet(t) => t
| t => raise NoCollectionTypeError t
(* RETURN: OclType *)
fun replace_templ_para (Collection(tt)) t = Collection (t)
| replace_templ_para (Set (tt)) t = Set (t)
| replace_templ_para (OrderedSet (tt)) t = OrderedSet (t)
| replace_templ_para (Sequence (tt)) t = Sequence (t)
| replace_templ_para (Bag (tt)) t = Bag (t)
| replace_templ_para t1 t2 = raise TemplateError ("Not possible to replace template parameter of a basic type. Type is: " ^ string_of_OclType t1 ^ " \n")
(* RETURN: String list *)
fun package_of_template_parameter typ =
case (typ) of
Set (t) => (package_of_template_parameter (template_parameter t)
handle NoCollectionTypeError t => package_of_template_parameter t)
| OrderedSet (t) => (package_of_template_parameter (template_parameter t)
handle NoCollectionTypeError t => package_of_template_parameter t)
| Collection (t) => (package_of_template_parameter (template_parameter t)
handle NoCollectionTypeError t => package_of_template_parameter t)
| Sequence (t) => (package_of_template_parameter (template_parameter t)
handle NoCollectionTypeError t => package_of_template_parameter t)
| Bag (t) => (package_of_template_parameter (template_parameter t)
handle NoCollectionTypeError t => package_of_template_parameter t)
| Integer => [OclLibPackage]
| String => [OclLibPackage]
| Boolean => [OclLibPackage]
| Real => [OclLibPackage]
| DummyT => []
| OclVoid => []
| OclAny => []
| Classifier (p) =>
if (length p > 1) then
List.take (p,(length p) -1)
else
[]
(* RETURN: IDENDITAET *)
fun swap1 f a b c = f c b a
(* RETURN: (a' list * a' list ) *)
fun parse_string c ([]) = ([],[])
fun parse_string c (h::tail) =
if (c = h) then
([],h::tail)
else
(h::(#1 (parse_string c tail)),(#2 (parse_string c tail)))
(* RETURN: OclType *)
fun string_to_cons "Set" typ = Set(typ)
| string_to_cons "Bag" typ = Bag(typ)
| string_to_cons "Collection" typ = Collection (typ)
| string_to_cons "OrderedSet" typ = OrderedSet (typ)
| string_to_cons "Sequence" typ = Sequence (typ)
(* RETURN: OclType *)
fun string_to_type ["Integer"] = Integer
| string_to_type ["Boolean"] = Boolean
| string_to_type ["Real"] = Real
| string_to_type ["OclAny"] = OclAny
| string_to_type ["DummyT"] = DummyT
| string_to_type ["String"] = String
| string_to_type ["OclVoid"] = OclVoid
| string_to_type [set] =
if (List.exists (fn a => if (a = (#"(")) then true else false) (String.explode set)) then
(* set *)
let
val tokens = parse_string (#"(") (String.explode set)
val cons = (#1 tokens)
(* delete first "(" and last ")" element *)
val tail = List.tl (real_path (#2 tokens))
val _ = TextIO.output(TextIO.stdOut,"tail "^ (String.implode tail) ^ "\n")
in
string_to_cons (String.implode cons) (string_to_type ([String.implode tail]))
end
else
Classifier ([set])
| string_to_type list = Classifier (list)
(* RETURN: OclType *)
fun type_of_template (T as Template{classifier,parameter}) =
case (name_of classifier) of
["Collection(T)"] => Collection (parameter)
| ["Set(T)"] => Set (parameter)
| ["OrderedSet(T)"] => OrderedSet (parameter)
| ["Bag(T)"] => Bag (parameter)
| ["Sequence(T)"] => Sequence (parameter)
(*** TYPE INFERENCE ***)
(* RETURN: Boolean *)
fun type_equals Integer (Classifier ([OclLibPackage,"Real"])) = true
| type_equals (Classifier ([OclLibPackage,"Integer"])) Real = true
| type_equals _ OclAny = true
| type_equals _ (Classifier ([OclLibPackage,"OclAny"])) = true
| type_equals x y =
if (x = y) then
true
else
false
(* INHERITANCE *)
(* RETURN: OclTyp *)
fun substitute_typ typ templ_type =
let
val _ = trace low ("substitute type : " ^ (string_of_OclType typ) ^ " instead of " ^ (string_of_OclType templ_type) ^ " \n")
in
case templ_type of
(* innerst type *)
Sequence(TemplateParameter "T") => Sequence (typ)
| Set(TemplateParameter "T") => Set(typ)
| OrderedSet(TemplateParameter "T") => OrderedSet (typ)
| Collection(TemplateParameter "T") => Collection(typ)
| Bag(TemplateParameter "T") => Bag(typ)
(* nested types *)
| Sequence (t) => Sequence (substitute_typ typ t)
| Set (t) => Set (substitute_typ typ t)
| OrderedSet (t) => OrderedSet (substitute_typ typ t)
| Collection (t) => Collection (substitute_typ typ t)
| Bag (t) => Bag (substitute_typ typ t)
(* only parameter *)
| TemplateParameter "T" => typ
(* basic types *)
| OclAny => OclAny
| OclVoid => OclVoid
| Integer => Integer
| Real => Real
| String => String
| Boolean => Boolean
| DummyT => DummyT
| Classifier (path) => Classifier (path)
(* else error *)
| _ => raise TemplateInstantiationError ("Template type not of type: Sequence, Set, OrderedSet, Collection or Bag")
end
(* RETURN: (string * OclType ) list *)
fun substitute_args typ [] = []
| substitute_args typ ((s,t)::tail) =
let
val _ = trace low ("substitute argument : " ^ (string_of_OclType typ) ^ " template parameter of " ^ (string_of_OclType t) ^ " \n")
in
(s,substitute_typ typ t)::(substitute_args typ tail)
end
(* RETURN: operation list*)
fun substitute_operations typ [] = []
| substitute_operations typ ((oper:operation)::tail) =
let
val _ = trace low ("\n\nsubstitute operation : " ^ (#name oper) ^ " ... \n")
val args = substitute_args typ (#arguments oper)
val res = substitute_typ typ (#result oper)
in
({
name = #name oper,
postcondition = #postcondition oper,
precondition = #precondition oper,
body = #body oper,
arguments = args,
result = res,
visibility = #visibility oper,
isQuery = #isQuery oper,
scope = #scope oper
}:operation)::(substitute_operations typ tail)
end
(* RETURN: OclType option *)
fun substitute_parent (Set (t)) = SOME (Collection t)
| substitute_parent (OrderedSet (t)) = SOME (Set (t))
| substitute_parent (Sequence (t)) = SOME (Collection (t))
| substitute_parent (Bag (t)) = SOME (Collection t)
| substitute_parent (Collection (t)) = SOME (Collection (t))
| substitute_parent t = SOME (Collection t)
(* RETURN: Classifier *)
fun substitute_classifier typ classifier =
let
val _ = trace low ("substitute classifier: parameter type: " ^ string_of_OclType typ ^ " template type: " ^ string_of_OclType (type_of classifier) ^ "\n")
val styp = substitute_typ typ (type_of classifier)
val ops = substitute_operations typ (operations_of classifier)
val sparent = substitute_parent typ
in
(Class
{
name = styp,
(* take the parent of the template parameter *)
parent = sparent,
(* a template has no attributes *)
attributes = [],
operations = ops,
(* a template has no associationends *)
associationends = [],
(* a template has no invariants *)
invariant = [],
(* a template has no stereotypes *)
stereotypes = [],
(* a template has no interfaces *)
interfaces = [],
(* a template's thyname is NONE *)
thyname = NONE,
(* a template has no activity_graphs *)
activity_graphs = []
})
end
(* RETURN: classifier *)
(* RETURN: Classifer *)
and get_classifier source model =
let
val typ = type_of_term (source)
fun class_of_t typ cl = hd (List.filter (fn a => if ((type_of a) = typ) then true else false) cl)
in
case typ of
(* Primitive types of lib *)
Boolean => class_of_t Boolean model
| Integer => class_of_t Integer model
| Real => class_of_t Real model
| String => class_of_t String model
(* Template types of lib *)
| Sequence (T) => templ_of (Sequence(TemplateParameter "T")) T model
| Set (T) => templ_of (Set(TemplateParameter "T")) T model
| OrderedSet (T) => templ_of (OrderedSet(TemplateParameter "T")) T model
| Bag (T) => templ_of (Bag(TemplateParameter "T")) T model
| Collection (T) => templ_of (Collection(TemplateParameter "T")) T model
(* Class types of lib *)
| OclVoid => class_of_t OclVoid model
| OclAny => class_of_t OclAny model
(* Model types *)
| Classifier (path) => class_of_t (Classifier (path)) model
| DummyT =>
let
val _ = trace development ("GetClassifierError: DummyT \n")
in
raise GetClassifierError ("No classifier of type: 'DummyT' \n")
end
| TemplateParameter (string) =>
let
val _ = trace development ("GetClassifierError: TemplateParameter ("^ string ^") \n")
in
raise GetClassifierError ("No classifier of type: 'TemplateParameter (string)' \n")
end
end
(* RETURN: Classifier /* one-time classifier */ *)
(* Return the "one-time" classifier.
The classifier is instanciated form the corresponding
template form the library. Its only instanciate for one
use and not stored later in the library.
*)
and templ_of temp_typ para_typ [] = raise TemplateInstantiationError ("Error during instantiating a template" ^ "\n")
| templ_of temp_typ para_typ (Template{parameter,classifier}::tail) =
let
val _ = trace low ("Instantiate Template for classifier: " ^ (string_of_OclType (type_of classifier)) ^ "\n")
in
if ((type_of classifier) = temp_typ) then
substitute_classifier para_typ classifier
else
templ_of temp_typ para_typ tail
end
(* element in lib not a template *)
| templ_of temp_typ para_typ (h::tail) =
let
val _ = trace development ("shit")
in
templ_of temp_typ para_typ tail
end
and class_of_type typ model =
get_classifier (Variable ("x",typ)) model
(* RETURN: Boolean *)
fun conforms_to_up _ OclAny _ = true
| conforms_to_up (Set(T1)) (Collection(T2)) model =
let
val _ = trace low ("conforms_to_up: set -> collection \n")
in
if (conforms_to T1 T2 model) then
true
else
false
end
| conforms_to_up (Bag(T1)) (Collection(T2)) model =
let
val _ = trace low ("conforms_to_up: bag -> collection \n")
in
if (conforms_to T1 T2 model) then
true
else
false
end
| conforms_to_up (Sequence(T1)) (Collection(T2)) model =
let
val _ = trace low ("conforms_to_up: sequence -> collection \n")
in
if (conforms_to T1 T2 model) then
true
else
false
end
| conforms_to_up (OrderedSet(T1)) (Collection(T2)) model =
let
val _ = trace low ("conforms_to_up: orderedset -> collection \n")
in
if (conforms_to T1 T2 model) then
true
else
false
end
| conforms_to_up typ1 typ2 model =
let
val class = class_of_type typ1 model
val parents_types = type_of_parents (class) model
val _ = trace low ("conforms_to_up: ... \n")
in
member (typ2) (parents_types)
end
and
(* RETRUN: Boolean *)
conforms_to x y model =
let
val _ = trace low ("conforms_to: " ^ string_of_OclType x ^ " -> " ^ string_of_OclType y ^ " ? \n")
in
if (x = y) then
true
else
if (type_equals x y) then
true
else
conforms_to_up x y model
end
(* RETURN: OclTerm *)
and upcast (term,typ) =
if (type_equals (type_of_term term) typ) then
term
else
OperationWithType (term,type_of_term term,"oclIsTypeOf",typ,typ)
(* RETURN: OclType list *)
and type_of_parents (Primitive {parent,...}) model =
(
case parent of
NONE => [OclAny]
| SOME (OclAny) => [OclAny]
| SOME (t) => (t)::(type_of_parents (class_of_type t model) model)
)
| type_of_parents (Class {parent,...}) model =
(
case parent of
NONE => [OclAny]
| SOME (OclAny) => [OclAny]
| SOME (t) => (t)::(type_of_parents (class_of_type t model) model)
)
| type_of_parents (Interface {parents,...}) model = parents
| type_of_parents (Template {classifier,...}) model =
raise TemplateInstantiationError ("During Instantiation of template parent needn't to be accessed")
(* RETURN: Classifier *)
fun class_of_parent (Class {parent,...}) clist =
(case parent of
NONE => get_classifier (Variable ("x",OclAny)) clist
| SOME (others) => get_classifier (Variable ("x",others)) clist
)
| class_of_parent (Primitive {parent,...}) clist =
(case parent of
NONE => class_of_type OclAny clist
| SOME (others) => class_of_type others clist
)
| class_of_parent (Interface {parents,...}) clist =
(* TODO: change API *)
(*
(case (List.last (parents)) of
NONE => class_of_type OclAny clist
| SOME (others) => class_of_type others clist
)
*)
class_of_type (List.hd parents) clist
| class_of_parent c (h::tail) = class_of_parent c tail
(* RETURN: Boolean *)
fun args_interfereable [] [] model = true
| args_interfereable ((str,typ)::tail) ((term,ttyp)::args) model =
let
val _ = trace low ("term type: " ^ (Ocl2String.ocl2string true term) ^ "\n")
val _ = trace low ("must conform to: " ^ (string_of_OclType typ) ^ "\n")
in
if (conforms_to (type_of_term term) typ model) then
true
else
false
end
(* not same nuber of arguments *)
| args_interfereable [x] list model = false
| args_interfereable list [x] model = false
(* RETURN: (OclTerm * OclType) list *)
fun interfere_args [] [] model = []
| interfere_args ((str,typ)::tail) ((term,_)::args) model =
let
val _ = trace low ("interfere args" ^ "\n")
in
if (type_equals typ (type_of_term term)) then
(term,type_of_term term)::(interfere_args tail args model)
else
if (conforms_to (type_of_term term) typ model) then
(term,typ)::(interfere_args tail args model)
else
raise InterferenceError ("Arguments are not interferebable \n")
end
(* RETURN: OclType *)
fun interfere_res_type t1 t2 model =
if (conforms_to t1 t2 model)
then t2
else raise InterferenceError ("Result type does not conform \n")
(* RETURN: OclTerm *)
fun interfere_methods [] source args model =
let
val _ = trace development ("InterferenceError ... \n")
in
raise InterferenceError ("interefere_methods: No operation signature matches given types (source: "^(Ocl2String.ocl2string false source)^").")
end
| interfere_methods ((class,meth)::class_meth_list) source args model =
let
val _ = trace low ("\nInterfere method : name : '" ^ name_of_op meth ^ "'\n")
val check_source = conforms_to (type_of_term source) (type_of class) model
val check_args = args_interfereable (#arguments meth) args model
val _ = trace low ("Interfereable ? : Source conforms : " ^ Bool.toString check_source ^ " Args conforms : " ^ Bool.toString check_args ^ "\n")
val _ = trace low ("Return type of method : " ^ string_of_OclType (result_of_op meth) ^ "\n\n")
in
if (check_source andalso check_args) then
(* signature matches given types *)
(OperationCall(source,type_of class,(name_of class)@[name_of_op meth],interfere_args (#arguments meth) args model,result_of_op meth))
else
(interfere_methods class_meth_list source args model)
end
(* RETURN: (OclTerm) *)
fun interfere_attrs (class,attr:attribute) source model =
let
val check_source = conforms_to (type_of_term source) (type_of class) model
val _ = trace low ("interfere attribute: check_source "^ Bool.toString check_source ^ "\n\n")
in
if check_source then
(* signature matches given types *)
SOME ((AttributeCall (source,type_of class,(name_of class)@[(#name attr)],(#attr_type attr))))
else
NONE
end
(* RETURN: OclTerm option*)
fun interfere_assocends (class,assocend:associationend) source model =
let
val check_source = conforms_to (type_of_term source) (type_of class) model
val _ = trace low ("Interfere assocend: check_source " ^ Bool.toString check_source ^ "\n")
val _ = trace low ("type of assoc " ^ string_of_OclType (assoc_to_attr_type assocend) ^ "\n")
in
if check_source then
SOME ((AssociationEndCall (source,type_of class,(name_of class)@[(#name assocend)],assoc_to_attr_type assocend)))
else
NONE
end
(* RETURN: OclTerm *)
fun interfere_attrs_or_assocends [] source model = raise InterferenceError ("interference_attr_or_assoc: No operation signature matches given types (source: " ^ (Ocl2String.ocl2string false source) ^ ").")
| interfere_attrs_or_assocends ((class,SOME(attr:attribute),NONE)::class_attr_or_assoc_list) source model =
(
case (interfere_attrs (class,attr) source model) of
NONE => (interfere_attrs_or_assocends class_attr_or_assoc_list source model)
| SOME (term) => term
)
| interfere_attrs_or_assocends ((class,NONE,SOME(assocend:associationend))::class_attr_or_assoc_list) source model =
(
case (interfere_assocends (class,assocend) source model) of
NONE => (interfere_attrs_or_assocends class_attr_or_assoc_list source model)
| SOME (term) => term
)
(* RETURN: Boolean *)
fun collection_type classifier =
case (type_of classifier) of
Collection(T) => true
| Set (T) => true
| OrderedSet (T) => true
| Sequence (T) => true
| Bag (T) => true
| x => false
(* RETURN: Boolean *)
fun end_of_recursion classifier =
case (type_of classifier) of
Collection (T) => true
| others => false
(* RETURN: (Classifier * operation ) list *)
fun get_overloaded_methods class op_name [] = raise NoModelReferenced ("in 'get_overloaded_methods' ...\n")
| get_overloaded_methods class op_name model =
let
val _ = trace low("\n")
val ops = operations_of class
val _ = trace low("Look for methods for classifier: " ^ string_of_OclType (type_of class) ^ "\n")
val ops2 = List.filter (fn a => (if ((#name a) = op_name) then true else false)) ops
val _ = trace low("operation name : " ^ op_name ^ " Found " ^ Int.toString (List.length ops2) ^ " method(s) \n")
val parent = class_of_parent class model
val _ = trace low("Parent class : " ^ string_of_OclType (type_of parent) ^ "\n\n")
val cl_op = List.map (fn a => (class,a)) ops2
in
if (class = class_of_type OclAny model)
then (* end of hierarchie *)
if (List.length ops2 = 0)
then[]
else[(class,List.hd(ops2))]
else
(
if (end_of_recursion class)
then (* end of collection hierarchie *)
if (List.length ops2 = 0)
then []
else [(class,List.hd(ops2))]
else (* go up the hierarchie tree *)
(
if (List.length ops2 = 0)
then (get_overloaded_methods parent op_name model)
else (cl_op)@(get_overloaded_methods parent op_name model)
)
)
end
(* RETURN: (Classifier * attribute option * association option) list *)
fun get_overloaded_attrs_or_assocends class attr_name [] = raise NoModelReferenced ("in 'get_overloaded_attrs' ... \n")
| get_overloaded_attrs_or_assocends class attr_name model =
let
val _ = trace low ("\n")
val attrs = attributes_of class
val assocends = associationends_of class
val _ = trace low ("Look for attributes/assocends : Class: " ^ string_of_OclType (type_of class) ^ " \n")
val attrs2 = List.filter (fn a => (if ((#name a) = attr_name) then true else false)) attrs
val assocends2 = List.filter (fn a => (if ((#name a) = attr_name) then true else false)) assocends
val _ = trace low ("Name of attr/assocend : " ^ attr_name ^ " Found " ^ Int.toString (List.length attrs2) ^ " attribute(s), " ^ Int.toString (List.length assocends2) ^ " assocend(s) \n")
val parent = class_of_parent class model
val _ = trace low ("Parent class : " ^ string_of_OclType(type_of parent) ^ "\n\n")
val cl_at = List.map (fn a => (class,SOME(a),NONE)) attrs2
val cl_as = List.map (fn a => (class,NONE,SOME(a))) assocends2
in
if (class = class_of_type OclAny model) then
(* end of hierarchie *)
if (List.length attrs2 = 0)
then if (List.length assocends2 = 0)
then []
else
[(class,NONE,SOME(List.hd(assocends2)))]
else [(class,SOME(List.hd(attrs2)),NONE)]
else
(
if (end_of_recursion class)
then (* end of collection hierarchie *)
if (List.length attrs2 = 0)
then if (List.length assocends2 = 0)
then []
else [(class,NONE,SOME(List.hd(assocends2)))]
else [(class,SOME(List.hd(attrs2)),NONE)]
else (* go up the hierarchie tree *)
(
if (List.length attrs2 = 0)
then if (List.length assocends2 = 0)
then (get_overloaded_attrs_or_assocends parent attr_name model)
else (cl_as)@(get_overloaded_attrs_or_assocends parent attr_name model)
else
(cl_at)@(get_overloaded_attrs_or_assocends parent attr_name model)
)
)
end
(* RETURN: OclTerm *)
fun get_meth source op_name args model=
(* object type *)
let
val _ = trace low ("Type of Classifier : " ^ string_of_OclType (type_of_term source ) ^ "\n")
val class = get_classifier source model
val meth_list = get_overloaded_methods class op_name model
val _ = trace low ("overloaded methods found: " ^ Int.toString (List.length meth_list) ^ "\n")
in
interfere_methods meth_list source args model
end
(* RETURN: OclTerm *)
fun get_attr_or_assoc source attr_name model =
let
val _ = trace low ("GET ATTRIBUTES OR ASSOCENDS: source term = " ^ Ocl2String.ocl2string false source ^ "\n")
val class = get_classifier source model
val attr_or_assocend_list = get_overloaded_attrs_or_assocends class attr_name model
val _ = trace low ("overloaded attributes/associationends found: " ^ Int.toString (List.length attr_or_assocend_list) ^ "\n")
in
let
val x = interfere_attrs_or_assocends attr_or_assocend_list source model
val _ = trace low ("\nReturn type of attribute: " ^ string_of_OclType (type_of_term x) ^ "\n\n")
in
x
end
end
end

313
src/ocl_parser/make_classifier_list.sml Normal file
View File

@ -0,0 +1,313 @@
(*****************************************************************************
* SML OCL 2.0 Parser - Parser/TypeChecker for OCL 2.0 written in SML(NJ)
*
* make_classifier_list.sml - main "ROOT.ML" file for HOL-OCL
* Copyright (C) 2007 Manuel P. Krucker <mkrucker@ethz.ch>
*
* This file is part of HOL-OCL.
*
* HOL-OCL is free software; you can redistribute it and/or modify it under
* the terms of the GNU General Public License as published by the Free
* Software Foundation; either version 2 of the License, or (at your option)
* any later version.
*
* HOL-OCL is distributed in the hope that it will be useful, but WITHOUT ANY
* WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
* FOR A PARTICULAR PURPOSE. See the GNU General Public License for more
* details.
*
* You should have received a copy of the GNU General Public License along
* with this program; if not, write to the Free Software Foundation, Inc.,
* 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
*****************************************************************************)
signature UPDATE_MODEL =
sig
(* exceptions *)
exception AlreadyInitValueError of string * Rep_OclTerm.OclTerm * string
exception NotYetSupportedError of string
exception ContextToClassifierError of Rep_OclTerm.OclTerm * string
exception OperationUpdateError of string * Context.ConditionType * Rep_OclTerm.OclTerm * string
(* operations *)
val add_precondition : string * string option * Rep_OclTerm.OclTerm -> Rep_Core.operation list -> Rep_Core.operation list
val add_postcondition : string * string option * Rep_OclTerm.OclTerm -> Rep_Core.operation list -> Rep_Core.operation list
val add_body : string * string option * Rep_OclTerm.OclTerm -> Rep_Core.operation list -> Rep_Core.operation list
val add_attribute : string * Rep_OclTerm.OclTerm -> Rep_Core.attribute list -> Rep_Core.attribute list
val context_to_classifier : Context.context -> Rep_Core.Classifier list -> Rep_Core.Classifier
val merge_classifier : Rep_Core.Classifier -> Rep_Core.Classifier list -> Rep_Core.Classifier list
val gen_updated_classifier_list: (Context.context option) list -> Rep_Core.Classifier list -> Rep_Core.Classifier list
end
structure Update_Model:UPDATE_MODEL =
struct
open Rep_Core;
open Ext_Library;
open Context;
exception AlreadyInitValueError of string * Rep_OclTerm.OclTerm * string
exception NotYetSupportedError of string
exception ContextToClassifierError of Rep_OclTerm.OclTerm * string
exception OperationUpdateError of string * Context.ConditionType * Rep_OclTerm.OclTerm * string
(* Error logging *)
val high = 5
val medium = 20
val low = 100
(* RETURN: operation list *)
fun add_precondition (op_name,cond_name,term) ((oper: operation)::operations_tail) =
if (#name oper = op_name) then
({name = #name oper,
precondition = (#precondition oper)@[(cond_name,term)],
postcondition = #postcondition oper,
body = #body oper,
arguments = #arguments oper,
result = #result oper,
isQuery = #isQuery oper,
visibility = #visibility oper,
scope = #scope oper})
::(operations_tail)
else
oper::(add_precondition (op_name,cond_name,term) operations_tail)
(* RETURN: operation list *)
fun add_postcondition (op_name,cond_name,term) ((oper: operation)::operations_tail) =
if (#name oper = op_name) then
({name = #name oper,
precondition = #precondition oper,
postcondition = (#postcondition oper)@[(cond_name,term)],
body = #body oper,
arguments = #arguments oper,
result = #result oper,
isQuery = #isQuery oper,
visibility = #visibility oper,
scope = #scope oper})
::(operations_tail)
else
oper::(add_postcondition (op_name,cond_name,term) operations_tail)
(* RETURN: operation list *)
fun add_body (op_name,cond_name,term) ((oper: operation)::operations_tail) =
if (#name oper = op_name) then
({name = #name oper,
precondition = #precondition oper,
postcondition = #postcondition oper,
body = (#body oper)@[(cond_name,term)],
arguments = #arguments oper,
result = #result oper,
isQuery = #isQuery oper,
visibility = #visibility oper,
scope = #scope oper})
::(operations_tail)
else
oper::(add_body (op_name,cond_name,term) operations_tail)
(* RETURN: operation list *)
fun add_operations cond_type (op_name,cond_name,term) [] = raise OperationUpdateError (op_name,cond_type,term,"Class has no operations\n")
| add_operations cond_type (op_name,cond_name,term) op_list =
case cond_type of
pre =>
let
val _ = trace low ("pre\n")
in
add_precondition (op_name,cond_name,term) op_list
end
| post =>
let
val _ = trace low ("post\n")
in
add_postcondition (op_name,cond_name,term) op_list
end
| body =>
let
val _ = trace low ("body\n")
in
add_body (op_name,cond_name,term) op_list
end
(* RETURN: attribute list *)
fun add_attribute (attr_name,term) ((attr: attribute)::attribute_tail) =
if (#name attr = attr_name) then
if (#init attr = NONE) then
({name = #name attr,
attr_type = #attr_type attr,
visibility = #visibility attr,
scope = #scope attr,
stereotypes = #stereotypes attr,
init = SOME (term)})
::(attribute_tail)
else
raise (AlreadyInitValueError (attr_name,term, "Classifier already defined an init value ..." ^ "\n"))
else
attr::(add_attribute (attr_name,term) attribute_tail)
(* RETURN: Classifier *)
(* INVARIANTS *)
fun context_to_classifier (Inv (path,string_opt,term)) model =
let
val _ = trace low ("Invariant to Classifier ... " ^ "\n")
val c = class_of_type (Rep_OclType.Classifier (path)) model
in
(
case c of
(Class {name,parent,attributes,operations,associationends,interfaces,stereotypes,invariant,thyname,activity_graphs}) =>
Class
{
name = name,
parent = parent,
attributes = attributes,
operations = operations,
associationends = associationends,
interfaces = interfaces,
stereotypes = stereotypes,
invariant = invariant@[(string_opt,term)],
thyname = thyname,
activity_graphs = activity_graphs
}
| (Interface {name,parents,operations,stereotypes,invariant,thyname}) =>
Interface
{
name = name,
parents = parents,
operations = operations,
stereotypes = stereotypes,
invariant = invariant,
thyname = thyname
}
| (Primitive {...}) => raise ContextToClassifierError (term,"Not possible to have an invariant on a 'Primitve' Type\n")
| (Enumeration {...}) => raise ContextToClassifierError (term,"Not possible to have an invariant on an 'Enumeration'Type\n")
)
end
(* Attribute constraints *)
| context_to_classifier (Attr (path,typ,attrorassoc,term)) model =
let
val _ = trace low ("Attribute to Classifier ... " ^ "\n")
val c = class_of_type (Rep_OclType.Classifier (real_path path)) model
in
(
case c of
(Class {name,parent,attributes,operations,associationends,interfaces,stereotypes,invariant,thyname,activity_graphs}) =>
(
case attrorassoc of
init =>
Class
{
name = name,
parent = parent,
attributes = add_attribute (List.last path,term) (attributes),
operations = operations,
associationends = associationends,
interfaces = interfaces,
stereotypes = stereotypes,
invariant = invariant,
thyname = thyname,
activity_graphs = activity_graphs
}
| derive => raise NotYetSupportedError ("derive not yet supported ... sorry" ^ "\n")
| def => raise NotYetSupportedError ("def not yet supported ... sorry" ^ "\n")
)
| (Interface {...}) => raise ContextToClassifierError (term,"Not possible to have an attribute constraint on an 'Interface' ... \n")
| (Primitive {...}) => raise ContextToClassifierError (term,"Not possible to have an attribute constraint on a 'Primitive' ... \n")
| (Enumeration {...}) => raise ContextToClassifierError (term,"Not possible to have an attribute constraint on a 'Enumeration' ...\n")
)
end
(* Operation constraints *)
| context_to_classifier (Cond (path,op_name,args,ret_typ,cond_type,cond_name,term)) model=
let
val _ = trace low ("Cond to Classifier ... " ^ "\n")
val c = class_of_type (Rep_OclType.Classifier (path)) model
in
(
case c of
(Class {name,parent,attributes,operations,associationends,interfaces,stereotypes,invariant,thyname,activity_graphs}) =>
Class
{
name = name,
parent = parent,
attributes = attributes,
operations = add_operations cond_type (op_name,cond_name,term) operations,
associationends = associationends,
interfaces = interfaces,
stereotypes = stereotypes,
invariant = invariant,
thyname = thyname,
activity_graphs = activity_graphs
}
| (Interface {name,parents,operations,stereotypes,invariant,thyname}) =>
Interface
{
name = name,
parents = parents,
operations = add_operations cond_type (op_name,cond_name,term) operations,
stereotypes = stereotypes,
invariant = invariant,
thyname = thyname
}
| (Primitive {...}) => raise ContextToClassifierError (term,"Not possible to have pre/post-conditions on a 'Primitve' ... \n")
| (Enumeration {...}) => raise ContextToClassifierError (term,"Not possible to have pre/post-conditions on an 'Enumeration' ... \n")
)
end
(* RETURN: Classifier list *)
fun merge_classifier classifier (h::classifier_list_tail) =
if (type_of classifier = type_of h) then
(* update classifier *)
(classifier)::(classifier_list_tail)
else
(* take next classifier *)
h::(merge_classifier classifier classifier_list_tail)
(* RETURN: Classifier list *)
fun gen_updated_classifier_list [] model = model
| gen_updated_classifier_list (SOME(h)::context_list_tail) model =
let
val updated_classifier = context_to_classifier h model
in
gen_updated_classifier_list context_list_tail (merge_classifier updated_classifier model)
handle AlreadyInitValueError (attr_path,term,mes) =>
let
val _ = trace zero ("\n\n#################################################\n")
val _ = trace zero ("AlreadyInitValueError:\n")
val _ = trace zero ("Error Message: " ^ mes ^ "\n")
val _ = trace zero ("In attribute or association: " ^ (attr_path) ^ "\n")
val _ = trace zero ("In Term: " ^ Ocl2String.ocl2string false term ^ "\n")
in
[]
end
| NotYetSupportedError mes =>
let
val _ = trace zero ("\n\n#################################################\n")
val _ = trace zero ("NotYetSupportedError:\n")
val _ = trace zero ("Error Message: " ^ mes ^ "\n")
in
[]
end
| ContextToClassifierError (term,mes) =>
let
val _ = trace zero ("\n\n#################################################\n")
val _ = trace zero ("ContextToClassifierError:\n")
val _ = trace zero ("Error Message: " ^ mes ^ "\n")
val _ = trace zero ("In Term: " ^ Ocl2String.ocl2string false term ^ "\n")
in
[]
end
| OperationUpdateError (meth_path,cond_type,term,mes) =>
let
val _ = trace zero ("\n\n#################################################\n")
val _ = trace zero ("AlreadyInitValueError:\n")
val _ = trace zero ("Error Message: " ^ mes ^ "\n")
val _ = trace zero ("In condition: " ^ (cond_type_to_string cond_type) ^ "\n")
val _ = trace zero ("In operation: " ^ (meth_path) ^ "\n")
val _ = trace zero ("In Term: " ^ Ocl2String.ocl2string false term ^ "\n")
in
[]
end
end
| gen_updated_classifier_list (NONE::context_list_tail) model = gen_updated_classifier_list context_list_tail model
(* end struct *)
end

299
src/ocl_parser/ml-yacc-lib/base.sig Normal file
View File

@ -0,0 +1,299 @@
(* ML-Yacc Parser Generator (c) 1989 Andrew W. Appel, David R. Tarditi *)
(* base.sig: Base signature file for SML-Yacc. This file contains signatures
that must be loaded before any of the files produced by ML-Yacc are loaded
*)
(* STREAM: signature for a lazy stream.*)
signature STREAM =
sig type 'xa stream
val streamify : (unit -> '_a) -> '_a stream
val cons : '_a * '_a stream -> '_a stream
val get : '_a stream -> '_a * '_a stream
end
(* LR_TABLE: signature for an LR Table.
The list of actions and gotos passed to mkLrTable must be ordered by state
number. The values for state 0 are the first in the list, the values for
state 1 are next, etc.
*)
signature LR_TABLE =
sig
datatype ('a,'b) pairlist = EMPTY | PAIR of 'a * 'b * ('a,'b) pairlist
datatype state = STATE of int
datatype term = T of int
datatype nonterm = NT of int
datatype action = SHIFT of state
| REDUCE of int
| ACCEPT
| ERROR
type table
val numStates : table -> int
val numRules : table -> int
val describeActions : table -> state ->
(term,action) pairlist * action
val describeGoto : table -> state -> (nonterm,state) pairlist
val action : table -> state * term -> action
val goto : table -> state * nonterm -> state
val initialState : table -> state
exception Goto of state * nonterm
val mkLrTable : {actions : ((term,action) pairlist * action) array,
gotos : (nonterm,state) pairlist array,
numStates : int, numRules : int,
initialState : state} -> table
end
(* TOKEN: signature revealing the internal structure of a token. This signature
TOKEN distinct from the signature {parser name}_TOKENS produced by ML-Yacc.
The {parser name}_TOKENS structures contain some types and functions to
construct tokens from values and positions.
The representation of token was very carefully chosen here to allow the
polymorphic parser to work without knowing the types of semantic values
or line numbers.
This has had an impact on the TOKENS structure produced by SML-Yacc, which
is a structure parameter to lexer functors. We would like to have some
type 'a token which functions to construct tokens would create. A
constructor function for a integer token might be
INT: int * 'a * 'a -> 'a token.
This is not possible because we need to have tokens with the representation
given below for the polymorphic parser.
Thus our constructur functions for tokens have the form:
INT: int * 'a * 'a -> (svalue,'a) token
This in turn has had an impact on the signature that lexers for SML-Yacc
must match and the types that a user must declare in the user declarations
section of lexers.
*)
signature TOKEN =
sig
structure LrTable : LR_TABLE
datatype ('a,'b) token = TOKEN of LrTable.term * ('a * 'b * 'b)
val sameToken : ('a,'b) token * ('a,'b) token -> bool
end
(* LR_PARSER: signature for a polymorphic LR parser *)
signature LR_PARSER =
sig
structure Stream: STREAM
structure LrTable : LR_TABLE
structure Token : TOKEN
sharing LrTable = Token.LrTable
exception ParseError
val parse : {table : LrTable.table,
lexer : ('_b,'_c) Token.token Stream.stream,
arg: 'arg,
saction : int *
'_c *
(LrTable.state * ('_b * '_c * '_c)) list *
'arg ->
LrTable.nonterm *
('_b * '_c * '_c) *
((LrTable.state *('_b * '_c * '_c)) list),
void : '_b,
ec : { is_keyword : LrTable.term -> bool,
noShift : LrTable.term -> bool,
preferred_change : (LrTable.term list * LrTable.term list) list,
errtermvalue : LrTable.term -> '_b,
showTerminal : LrTable.term -> string,
terms: LrTable.term list,
error : string * '_c * '_c -> unit
},
lookahead : int (* max amount of lookahead used in *)
(* error correction *)
} -> '_b *
(('_b,'_c) Token.token Stream.stream)
end
(* LEXER: a signature that most lexers produced for use with SML-Yacc's
output will match. The user is responsible for declaring type token,
type pos, and type svalue in the UserDeclarations section of a lexer.
Note that type token is abstract in the lexer. This allows SML-Yacc to
create a TOKENS signature for use with lexers produced by ML-Lex that
treats the type token abstractly. Lexers that are functors parametrized by
a Tokens structure matching a TOKENS signature cannot examine the structure
of tokens.
*)
signature LEXER =
sig
structure UserDeclarations :
sig
type ('a,'b) token
type pos
type svalue
end
val makeLexer : (int -> string) -> unit ->
(UserDeclarations.svalue,UserDeclarations.pos) UserDeclarations.token
end
(* ARG_LEXER: the %arg option of ML-Lex allows users to produce lexers which
also take an argument before yielding a function from unit to a token
*)
signature ARG_LEXER =
sig
structure UserDeclarations :
sig
type ('a,'b) token
type pos
type svalue
type arg
end
val makeLexer : (int -> string) -> UserDeclarations.arg -> unit ->
(UserDeclarations.svalue,UserDeclarations.pos) UserDeclarations.token
end
(* PARSER_DATA: the signature of ParserData structures in {parser name}LrValsFun
produced by SML-Yacc. All such structures match this signature.
The {parser name}LrValsFun produces a structure which contains all the values
except for the lexer needed to call the polymorphic parser mentioned
before.
*)
signature PARSER_DATA =
sig
(* the type of line numbers *)
type pos
(* the type of semantic values *)
type svalue
(* the type of the user-supplied argument to the parser *)
type arg
(* the intended type of the result of the parser. This value is
produced by applying extract from the structure Actions to the
final semantic value resultiing from a parse.
*)
type result
structure LrTable : LR_TABLE
structure Token : TOKEN
sharing Token.LrTable = LrTable
(* structure Actions contains the functions which mantain the
semantic values stack in the parser. Void is used to provide
a default value for the semantic stack.
*)
structure Actions :
sig
val actions : int * pos *
(LrTable.state * (svalue * pos * pos)) list * arg->
LrTable.nonterm * (svalue * pos * pos) *
((LrTable.state *(svalue * pos * pos)) list)
val void : svalue
val extract : svalue -> result
end
(* structure EC contains information used to improve error
recovery in an error-correcting parser *)
structure EC :
sig
val is_keyword : LrTable.term -> bool
val noShift : LrTable.term -> bool
val preferred_change : (LrTable.term list * LrTable.term list) list
val errtermvalue : LrTable.term -> svalue
val showTerminal : LrTable.term -> string
val terms: LrTable.term list
end
(* table is the LR table for the parser *)
val table : LrTable.table
end
(* signature PARSER is the signature that most user parsers created by
SML-Yacc will match.
*)
signature PARSER =
sig
structure Token : TOKEN
structure Stream : STREAM
exception ParseError
(* type pos is the type of line numbers *)
type pos
(* type result is the type of the result from the parser *)
type result
(* the type of the user-supplied argument to the parser *)
type arg
(* type svalue is the type of semantic values for the semantic value
stack
*)
type svalue
(* val makeLexer is used to create a stream of tokens for the parser *)
val makeLexer : (int -> string) ->
(svalue,pos) Token.token Stream.stream
(* val parse takes a stream of tokens and a function to print
errors and returns a value of type result and a stream containing
the unused tokens
*)
val parse : int * ((svalue,pos) Token.token Stream.stream) *
(string * pos * pos -> unit) * arg ->
result * (svalue,pos) Token.token Stream.stream
val sameToken : (svalue,pos) Token.token * (svalue,pos) Token.token ->
bool
end
(* signature ARG_PARSER is the signature that will be matched by parsers whose
lexer takes an additional argument.
*)
signature ARG_PARSER =
sig
structure Token : TOKEN
structure Stream : STREAM
exception ParseError
type arg
type lexarg
type pos
type result
type svalue
val makeLexer : (int -> string) -> lexarg ->
(svalue,pos) Token.token Stream.stream
val parse : int * ((svalue,pos) Token.token Stream.stream) *
(string * pos * pos -> unit) * arg ->
result * (svalue,pos) Token.token Stream.stream
val sameToken : (svalue,pos) Token.token * (svalue,pos) Token.token ->
bool
end

94
src/ocl_parser/ml-yacc-lib/join.sml Normal file
View File

@ -0,0 +1,94 @@
(* ML-Yacc Parser Generator (c) 1989 Andrew W. Appel, David R. Tarditi *)
(* functor Join creates a user parser by putting together a Lexer structure,
an LrValues structure, and a polymorphic parser structure. Note that
the Lexer and LrValues structure must share the type pos (i.e. the type
of line numbers), the type svalues for semantic values, and the type
of tokens.
*)
functor Join(structure Lex : LEXER
structure ParserData: PARSER_DATA
structure LrParser : LR_PARSER
sharing ParserData.LrTable = LrParser.LrTable
sharing ParserData.Token = LrParser.Token
sharing type Lex.UserDeclarations.svalue = ParserData.svalue
sharing type Lex.UserDeclarations.pos = ParserData.pos
sharing type Lex.UserDeclarations.token = ParserData.Token.token)
: PARSER =
struct
structure Token = ParserData.Token
structure Stream = LrParser.Stream
exception ParseError = LrParser.ParseError
type arg = ParserData.arg
type pos = ParserData.pos
type result = ParserData.result
type svalue = ParserData.svalue
val makeLexer = LrParser.Stream.streamify o Lex.makeLexer
val parse = fn (lookahead,lexer,error,arg) =>
(fn (a,b) => (ParserData.Actions.extract a,b))
(LrParser.parse {table = ParserData.table,
lexer=lexer,
lookahead=lookahead,
saction = ParserData.Actions.actions,
arg=arg,
void= ParserData.Actions.void,
ec = {is_keyword = ParserData.EC.is_keyword,
noShift = ParserData.EC.noShift,
preferred_change = ParserData.EC.preferred_change,
errtermvalue = ParserData.EC.errtermvalue,
error=error,
showTerminal = ParserData.EC.showTerminal,
terms = ParserData.EC.terms}}
)
val sameToken = Token.sameToken
end
(* functor JoinWithArg creates a variant of the parser structure produced
above. In this case, the makeLexer take an additional argument before
yielding a value of type unit -> (svalue,pos) token
*)
functor JoinWithArg(structure Lex : ARG_LEXER
structure ParserData: PARSER_DATA
structure LrParser : LR_PARSER
sharing ParserData.LrTable = LrParser.LrTable
sharing ParserData.Token = LrParser.Token
sharing type Lex.UserDeclarations.svalue = ParserData.svalue
sharing type Lex.UserDeclarations.pos = ParserData.pos
sharing type Lex.UserDeclarations.token = ParserData.Token.token)
: ARG_PARSER =
struct
structure Token = ParserData.Token
structure Stream = LrParser.Stream
exception ParseError = LrParser.ParseError
type arg = ParserData.arg
type lexarg = Lex.UserDeclarations.arg
type pos = ParserData.pos
type result = ParserData.result
type svalue = ParserData.svalue
val makeLexer = fn s => fn arg =>
LrParser.Stream.streamify (Lex.makeLexer s arg)
val parse = fn (lookahead,lexer,error,arg) =>
(fn (a,b) => (ParserData.Actions.extract a,b))
(LrParser.parse {table = ParserData.table,
lexer=lexer,
lookahead=lookahead,
saction = ParserData.Actions.actions,
arg=arg,
void= ParserData.Actions.void,
ec = {is_keyword = ParserData.EC.is_keyword,
noShift = ParserData.EC.noShift,
preferred_change = ParserData.EC.preferred_change,
errtermvalue = ParserData.EC.errtermvalue,
error=error,
showTerminal = ParserData.EC.showTerminal,
terms = ParserData.EC.terms}}
)
val sameToken = Token.sameToken
end;

59
src/ocl_parser/ml-yacc-lib/lrtable.sml Normal file
View File

@ -0,0 +1,59 @@
(* ML-Yacc Parser Generator (c) 1989 Andrew W. Appel, David R. Tarditi *)
structure LrTable : LR_TABLE =
struct
open Array List
infix 9 sub
datatype ('a,'b) pairlist = EMPTY
| PAIR of 'a * 'b * ('a,'b) pairlist
datatype term = T of int
datatype nonterm = NT of int
datatype state = STATE of int
datatype action = SHIFT of state
| REDUCE of int (* rulenum from grammar *)
| ACCEPT
| ERROR
exception Goto of state * nonterm
type table = {states: int, rules : int,initialState: state,
action: ((term,action) pairlist * action) array,
goto : (nonterm,state) pairlist array}
val numStates = fn ({states,...} : table) => states
val numRules = fn ({rules,...} : table) => rules
val describeActions =
fn ({action,...} : table) =>
fn (STATE s) => action sub s
val describeGoto =
fn ({goto,...} : table) =>
fn (STATE s) => goto sub s
fun findTerm (T term,row,default) =
let fun find (PAIR (T key,data,r)) =
if key < term then find r
else if key=term then data
else default
| find EMPTY = default
in find row
end
fun findNonterm (NT nt,row) =
let fun find (PAIR (NT key,data,r)) =
if key < nt then find r
else if key=nt then SOME data
else NONE
| find EMPTY = NONE
in find row
end
val action = fn ({action,...} : table) =>
fn (STATE state,term) =>
let val (row,default) = action sub state
in findTerm(term,row,default)
end
val goto = fn ({goto,...} : table) =>
fn (a as (STATE state,nonterm)) =>
case findNonterm(nonterm,goto sub state)
of SOME state => state
| NONE => raise (Goto a)
val initialState = fn ({initialState,...} : table) => initialState
val mkLrTable = fn {actions,gotos,initialState,numStates,numRules} =>
({action=actions,goto=gotos,
states=numStates,
rules=numRules,
initialState=initialState} : table)
end;

542
src/ocl_parser/ml-yacc-lib/parser2.sml Normal file
View File

@ -0,0 +1,542 @@
(* ML-Yacc Parser Generator (c) 1989 Andrew W. Appel, David R. Tarditi *)
(* parser.sml: This is a parser driver for LR tables with an error-recovery
routine added to it. The routine used is described in detail in this
article:
'A Practical Method for LR and LL Syntactic Error Diagnosis and
Recovery', by M. Burke and G. Fisher, ACM Transactions on
Programming Langauges and Systems, Vol. 9, No. 2, April 1987,
pp. 164-197.
This program is an implementation is the partial, deferred method discussed
in the article. The algorithm and data structures used in the program
are described below.
This program assumes that all semantic actions are delayed. A semantic
action should produce a function from unit -> value instead of producing the
normal value. The parser returns the semantic value on the top of the
stack when accept is encountered. The user can deconstruct this value
and apply the unit -> value function in it to get the answer.
It also assumes that the lexer is a lazy stream.
Data Structures:
----------------
* The parser:
The state stack has the type
(state * (semantic value * line # * line #)) list
The parser keeps a queue of (state stack * lexer pair). A lexer pair
consists of a terminal * value pair and a lexer. This allows the
parser to reconstruct the states for terminals to the left of a
syntax error, and attempt to make error corrections there.
The queue consists of a pair of lists (x,y). New additions to
the queue are cons'ed onto y. The first element of x is the top
of the queue. If x is nil, then y is reversed and used
in place of x.
Algorithm:
----------
* The steady-state parser:
This parser keeps the length of the queue of state stacks at
a steady state by always removing an element from the front when
another element is placed on the end.
It has these arguments:
stack: current stack
queue: value of the queue
lexPair ((terminal,value),lex stream)
When SHIFT is encountered, the state to shift to and the value are
are pushed onto the state stack. The state stack and lexPair are
placed on the queue. The front element of the queue is removed.
When REDUCTION is encountered, the rule is applied to the current
stack to yield a triple (nonterm,value,new stack). A new
stack is formed by adding (goto(top state of stack,nonterm),value)
to the stack.
When ACCEPT is encountered, the top value from the stack and the
lexer are returned.
When an ERROR is encountered, fixError is called. FixError
takes the arguments to the parser, fixes the error if possible and
returns a new set of arguments.
* The distance-parser:
This parser includes an additional argument distance. It pushes
elements on the queue until it has parsed distance tokens, or an
ACCEPT or ERROR occurs. It returns a stack, lexer, the number of
tokens left unparsed, a queue, and an action option.
*)
signature FIFO =
sig type 'a queue
val empty : 'a queue
exception Empty
val get : 'a queue -> 'a * 'a queue
val put : 'a * 'a queue -> 'a queue
end
(* drt (12/15/89) -- the functor should be used in development work, but
it wastes space in the release version.
functor ParserGen(structure LrTable : LR_TABLE
structure Stream : STREAM) : LR_PARSER =
*)
structure LrParser :> LR_PARSER =
struct
structure LrTable = LrTable
structure Stream = Stream
fun eqT (LrTable.T i, LrTable.T i') = i = i'
structure Token : TOKEN =
struct
structure LrTable = LrTable
datatype ('a,'b) token = TOKEN of LrTable.term * ('a * 'b * 'b)
val sameToken = fn (TOKEN(t,_),TOKEN(t',_)) => eqT (t,t')
end
open LrTable
open Token
val DEBUG1 = false
val DEBUG2 = false
exception ParseError
exception ParseImpossible of int
structure Fifo :> FIFO =
struct
type 'a queue = ('a list * 'a list)
val empty = (nil,nil)
exception Empty
fun get(a::x, y) = (a, (x,y))
| get(nil, nil) = raise Empty
| get(nil, y) = get(rev y, nil)
fun put(a,(x,y)) = (x,a::y)
end
type ('a,'b) elem = (state * ('a * 'b * 'b))
type ('a,'b) stack = ('a,'b) elem list
type ('a,'b) lexv = ('a,'b) token
type ('a,'b) lexpair = ('a,'b) lexv * (('a,'b) lexv Stream.stream)
type ('a,'b) distanceParse =
('a,'b) lexpair *
('a,'b) stack *
(('a,'b) stack * ('a,'b) lexpair) Fifo.queue *
int ->
('a,'b) lexpair *
('a,'b) stack *
(('a,'b) stack * ('a,'b) lexpair) Fifo.queue *
int *
action option
type ('a,'b) ecRecord =
{is_keyword : term -> bool,
preferred_change : (term list * term list) list,
error : string * 'b * 'b -> unit,
errtermvalue : term -> 'a,
terms : term list,
showTerminal : term -> string,
noShift : term -> bool}
local
val print = fn s => TextIO.output(TextIO.stdOut,s)
val println = fn s => (print s; print "\n")
val showState = fn (STATE s) => "STATE " ^ (Int.toString s)
in
fun printStack(stack: ('a,'b) stack, n: int) =
case stack
of (state,_) :: rest =>
(print("\t" ^ Int.toString n ^ ": ");
println(showState state);
printStack(rest, n+1))
| nil => ()
fun prAction showTerminal
(stack as (state,_) :: _, next as (TOKEN (term,_),_), action) =
(println "Parse: state stack:";
printStack(stack, 0);
print(" state="
^ showState state
^ " next="
^ showTerminal term
^ " action="
);
case action
of SHIFT state => println ("SHIFT " ^ (showState state))
| REDUCE i => println ("REDUCE " ^ (Int.toString i))
| ERROR => println "ERROR"
| ACCEPT => println "ACCEPT")
| prAction _ (_,_,action) = ()
end
(* ssParse: parser which maintains the queue of (state * lexvalues) in a
steady-state. It takes a table, showTerminal function, saction
function, and fixError function. It parses until an ACCEPT is
encountered, or an exception is raised. When an error is encountered,
fixError is called with the arguments of parseStep (lexv,stack,and
queue). It returns the lexv, and a new stack and queue adjusted so
that the lexv can be parsed *)
val ssParse =
fn (table,showTerminal,saction,fixError,arg) =>
let val prAction = prAction showTerminal
val action = LrTable.action table
val goto = LrTable.goto table
fun parseStep(args as
(lexPair as (TOKEN (terminal, value as (_,leftPos,_)),
lexer
),
stack as (state,_) :: _,
queue)) =
let val nextAction = action (state,terminal)
val _ = if DEBUG1 then prAction(stack,lexPair,nextAction)
else ()
in case nextAction
of SHIFT s =>
let val newStack = (s,value) :: stack
val newLexPair = Stream.get lexer
val (_,newQueue) =Fifo.get(Fifo.put((newStack,newLexPair),
queue))
in parseStep(newLexPair,(s,value)::stack,newQueue)
end
| REDUCE i =>
(case saction(i,leftPos,stack,arg)
of (nonterm,value,stack as (state,_) :: _) =>
parseStep(lexPair,(goto(state,nonterm),value)::stack,
queue)
| _ => raise (ParseImpossible 197))
| ERROR => parseStep(fixError args)
| ACCEPT =>
(case stack
of (_,(topvalue,_,_)) :: _ =>
let val (token,restLexer) = lexPair
in (topvalue,Stream.cons(token,restLexer))
end
| _ => raise (ParseImpossible 202))
end
| parseStep _ = raise (ParseImpossible 204)
in parseStep
end
(* distanceParse: parse until n tokens are shifted, or accept or
error are encountered. Takes a table, showTerminal function, and
semantic action function. Returns a parser which takes a lexPair
(lex result * lexer), a state stack, a queue, and a distance
(must be > 0) to parse. The parser returns a new lex-value, a stack
with the nth token shifted on top, a queue, a distance, and action
option. *)
val distanceParse =
fn (table,showTerminal,saction,arg) =>
let val prAction = prAction showTerminal
val action = LrTable.action table
val goto = LrTable.goto table
fun parseStep(lexPair,stack,queue,0) = (lexPair,stack,queue,0,NONE)
| parseStep(lexPair as (TOKEN (terminal, value as (_,leftPos,_)),
lexer
),
stack as (state,_) :: _,
queue,distance) =
let val nextAction = action(state,terminal)
val _ = if DEBUG1 then prAction(stack,lexPair,nextAction)
else ()
in case nextAction
of SHIFT s =>
let val newStack = (s,value) :: stack
val newLexPair = Stream.get lexer
in parseStep(newLexPair,(s,value)::stack,
Fifo.put((newStack,newLexPair),queue),distance-1)
end
| REDUCE i =>
(case saction(i,leftPos,stack,arg)
of (nonterm,value,stack as (state,_) :: _) =>
parseStep(lexPair,(goto(state,nonterm),value)::stack,
queue,distance)
| _ => raise (ParseImpossible 240))
| ERROR => (lexPair,stack,queue,distance,SOME nextAction)
| ACCEPT => (lexPair,stack,queue,distance,SOME nextAction)
end
| parseStep _ = raise (ParseImpossible 242)
in parseStep : ('_a,'_b) distanceParse
end
(* mkFixError: function to create fixError function which adjusts parser state
so that parse may continue in the presence of an error *)
fun mkFixError({is_keyword,terms,errtermvalue,
preferred_change,noShift,
showTerminal,error,...} : ('_a,'_b) ecRecord,
distanceParse : ('_a,'_b) distanceParse,
minAdvance,maxAdvance)
(lexv as (TOKEN (term,value as (_,leftPos,_)),_),stack,queue) =
let val _ = if DEBUG2 then
error("syntax error found at " ^ (showTerminal term),
leftPos,leftPos)
else ()
fun tokAt(t,p) = TOKEN(t,(errtermvalue t,p,p))
val minDelta = 3
(* pull all the state * lexv elements from the queue *)
val stateList =
let fun f q = let val (elem,newQueue) = Fifo.get q
in elem :: (f newQueue)
end handle Fifo.Empty => nil
in f queue
end
(* now number elements of stateList, giving distance from
error token *)
val (_, numStateList) =
List.foldr (fn (a,(num,r)) => (num+1,(a,num)::r)) (0, []) stateList
(* Represent the set of potential changes as a linked list.
Values of datatype Change hold information about a potential change.
oper = oper to be applied
pos = the # of the element in stateList that would be altered.
distance = the number of tokens beyond the error token which the
change allows us to parse.
new = new terminal * value pair at that point
orig = original terminal * value pair at the point being changed.
*)
datatype ('a,'b) change = CHANGE of
{pos : int, distance : int, leftPos: 'b, rightPos: 'b,
new : ('a,'b) lexv list, orig : ('a,'b) lexv list}
val showTerms = concat o map (fn TOKEN(t,_) => " " ^ showTerminal t)
val printChange = fn c =>
let val CHANGE {distance,new,orig,pos,...} = c
in (print ("{distance= " ^ (Int.toString distance));
print (",orig ="); print(showTerms orig);
print (",new ="); print(showTerms new);
print (",pos= " ^ (Int.toString pos));
print "}\n")
end
val printChangeList = app printChange
(* parse: given a lexPair, a stack, and the distance from the error
token, return the distance past the error token that we are able to parse.*)
fun parse (lexPair,stack,queuePos : int) =
case distanceParse(lexPair,stack,Fifo.empty,queuePos+maxAdvance+1)
of (_,_,_,distance,SOME ACCEPT) =>
if maxAdvance-distance-1 >= 0
then maxAdvance
else maxAdvance-distance-1
| (_,_,_,distance,_) => maxAdvance - distance - 1
(* catList: concatenate results of scanning list *)
fun catList l f = List.foldr (fn(a,r)=> f a @ r) [] l
fun keywordsDelta new = if List.exists (fn(TOKEN(t,_))=>is_keyword t) new
then minDelta else 0
fun tryChange{lex,stack,pos,leftPos,rightPos,orig,new} =
let val lex' = List.foldr (fn (t',p)=>(t',Stream.cons p)) lex new
val distance = parse(lex',stack,pos+length new-length orig)
in if distance >= minAdvance + keywordsDelta new
then [CHANGE{pos=pos,leftPos=leftPos,rightPos=rightPos,
distance=distance,orig=orig,new=new}]
else []
end
(* tryDelete: Try to delete n terminals.
Return single-element [success] or nil.
Do not delete unshiftable terminals. *)
fun tryDelete n ((stack,lexPair as (TOKEN(term,(_,l,r)),_)),qPos) =
let fun del(0,accum,left,right,lexPair) =
tryChange{lex=lexPair,stack=stack,
pos=qPos,leftPos=left,rightPos=right,
orig=rev accum, new=[]}
| del(n,accum,left,right,(tok as TOKEN(term,(_,_,r)),lexer)) =
if noShift term then []
else del(n-1,tok::accum,left,r,Stream.get lexer)
in del(n,[],l,r,lexPair)
end
(* tryInsert: try to insert tokens before the current terminal;
return a list of the successes *)
fun tryInsert((stack,lexPair as (TOKEN(_,(_,l,_)),_)),queuePos) =
catList terms (fn t =>
tryChange{lex=lexPair,stack=stack,
pos=queuePos,orig=[],new=[tokAt(t,l)],
leftPos=l,rightPos=l})
(* trySubst: try to substitute tokens for the current terminal;
return a list of the successes *)
fun trySubst ((stack,lexPair as (orig as TOKEN (term,(_,l,r)),lexer)),
queuePos) =
if noShift term then []
else
catList terms (fn t =>
tryChange{lex=Stream.get lexer,stack=stack,
pos=queuePos,
leftPos=l,rightPos=r,orig=[orig],
new=[tokAt(t,r)]})
(* do_delete(toks,lexPair) tries to delete tokens "toks" from "lexPair".
If it succeeds, returns SOME(toks',l,r,lp), where
toks' is the actual tokens (with positions and values) deleted,
(l,r) are the (leftmost,rightmost) position of toks',
lp is what remains of the stream after deletion
*)
fun do_delete(nil,lp as (TOKEN(_,(_,l,_)),_)) = SOME(nil,l,l,lp)
| do_delete([t],(tok as TOKEN(t',(_,l,r)),lp')) =
if eqT (t, t')
then SOME([tok],l,r,Stream.get lp')
else NONE
| do_delete(t::rest,(tok as TOKEN(t',(_,l,r)),lp')) =
if eqT (t,t')
then case do_delete(rest,Stream.get lp')
of SOME(deleted,l',r',lp'') =>
SOME(tok::deleted,l,r',lp'')
| NONE => NONE
else NONE
fun tryPreferred((stack,lexPair),queuePos) =
catList preferred_change (fn (delete,insert) =>
if List.exists noShift delete then [] (* should give warning at
parser-generation time *)
else case do_delete(delete,lexPair)
of SOME(deleted,l,r,lp) =>
tryChange{lex=lp,stack=stack,pos=queuePos,
leftPos=l,rightPos=r,orig=deleted,
new=map (fn t=>(tokAt(t,r))) insert}
| NONE => [])
val changes = catList numStateList tryPreferred @
catList numStateList tryInsert @
catList numStateList trySubst @
catList numStateList (tryDelete 1) @
catList numStateList (tryDelete 2) @
catList numStateList (tryDelete 3)
val findMaxDist = fn l =>
foldr (fn (CHANGE {distance,...},high) => Int.max(distance,high)) 0 l
(* maxDist: max distance past error taken that we could parse *)
val maxDist = findMaxDist changes
(* remove changes which did not parse maxDist tokens past the error token *)
val changes = catList changes
(fn(c as CHANGE{distance,...}) =>
if distance=maxDist then [c] else [])
in case changes
of (l as change :: _) =>
let fun print_msg (CHANGE {new,orig,leftPos,rightPos,...}) =
let val s =
case (orig,new)
of (_::_,[]) => "deleting " ^ (showTerms orig)
| ([],_::_) => "inserting " ^ (showTerms new)
| _ => "replacing " ^ (showTerms orig) ^
" with " ^ (showTerms new)
in error ("syntax error: " ^ s,leftPos,rightPos)
end
val _ =
(if length l > 1 andalso DEBUG2 then
(print "multiple fixes possible; could fix it by:\n";
app print_msg l;
print "chosen correction:\n")
else ();
print_msg change)
(* findNth: find nth queue entry from the error
entry. Returns the Nth queue entry and the portion of
the queue from the beginning to the nth-1 entry. The
error entry is at the end of the queue.
Examples:
queue = a b c d e
findNth 0 = (e,a b c d)
findNth 1 = (d,a b c)
*)
val findNth = fn n =>
let fun f (h::t,0) = (h,rev t)
| f (h::t,n) = f(t,n-1)
| f (nil,_) = let exception FindNth
in raise FindNth
end
in f (rev stateList,n)
end
val CHANGE {pos,orig,new,...} = change
val (last,queueFront) = findNth pos
val (stack,lexPair) = last
val lp1 = foldl(fn (_,(_,r)) => Stream.get r) lexPair orig
val lp2 = foldr(fn(t,r)=>(t,Stream.cons r)) lp1 new
val restQueue =
Fifo.put((stack,lp2),
foldl Fifo.put Fifo.empty queueFront)
val (lexPair,stack,queue,_,_) =
distanceParse(lp2,stack,restQueue,pos)
in (lexPair,stack,queue)
end
| nil => (error("syntax error found at " ^ (showTerminal term),
leftPos,leftPos); raise ParseError)
end
val parse = fn {arg,table,lexer,saction,void,lookahead,
ec=ec as {showTerminal,...} : ('_a,'_b) ecRecord} =>
let val distance = 15 (* defer distance tokens *)
val minAdvance = 1 (* must parse at least 1 token past error *)
val maxAdvance = Int.max(lookahead,0)(* max distance for parse check *)
val lexPair = Stream.get lexer
val (TOKEN (_,(_,leftPos,_)),_) = lexPair
val startStack = [(initialState table,(void,leftPos,leftPos))]
val startQueue = Fifo.put((startStack,lexPair),Fifo.empty)
val distanceParse = distanceParse(table,showTerminal,saction,arg)
val fixError = mkFixError(ec,distanceParse,minAdvance,maxAdvance)
val ssParse = ssParse(table,showTerminal,saction,fixError,arg)
fun loop (lexPair,stack,queue,_,SOME ACCEPT) =
ssParse(lexPair,stack,queue)
| loop (lexPair,stack,queue,0,_) = ssParse(lexPair,stack,queue)
| loop (lexPair,stack,queue,distance,SOME ERROR) =
let val (lexPair,stack,queue) = fixError(lexPair,stack,queue)
in loop (distanceParse(lexPair,stack,queue,distance))
end
| loop _ = let exception ParseInternal
in raise ParseInternal
end
in loop (distanceParse(lexPair,startStack,startQueue,distance))
end
end;

5
src/ocl_parser/ml-yacc-lib/root.sml Normal file
View File

@ -0,0 +1,5 @@
use "base.sig";
use "join.sml";
use "lrtable.sml";
use "stream.sml";
use "parser2.sml";

19
src/ocl_parser/ml-yacc-lib/stream.sml Normal file
View File

@ -0,0 +1,19 @@
(* ML-Yacc Parser Generator (c) 1989 Andrew W. Appel, David R. Tarditi *)
(* Stream: a structure implementing a lazy stream. The signature STREAM
is found in base.sig *)
structure Stream :> STREAM =
struct
datatype 'a str = EVAL of 'a * 'a str ref | UNEVAL of (unit->'a)
type 'a stream = 'a str ref
fun get(ref(EVAL t)) = t
| get(s as ref(UNEVAL f)) =
let val t = (f(), ref(UNEVAL f)) in s := EVAL t; t end
fun streamify f = ref(UNEVAL f)
fun cons(a,s) = ref(EVAL(a,s))
end;

185
src/ocl_parser/model_import.sml Normal file
View File

@ -0,0 +1,185 @@
(*****************************************************************************
* HOL-OCL - a shallow embedding of OCL into Isabelle/HOL
*
* model_import.sml - main "ROOT.ML" file for HOL-OCL
* Copyright (C) 2006 Achim D. Brucker <achim@brucker.ch>
*
* This file is part of HOL-OCL.
*
* HOL-OCL is free software; you can redistribute it and/or modify it under
* the terms of the GNU General Public License as published by the Free
* Software Foundation; either version 2 of the License, or (at your option)
* any later version.
*
* HOL-OCL is distributed in the hope that it will be useful, but WITHOUT ANY
* WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
* FOR A PARTICULAR PURPOSE. See the GNU General Public License for more
* details.
*
* You should have received a copy of the GNU General Public License along
* with this program; if not, write to the Free Software Foundation, Inc.,
* 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
*****************************************************************************)
signature MODEL_IMPORT =
sig
val parseUML : string -> Rep_Core.Classifier list
val parseOCL : string -> Context.context list
val import : string -> string -> string list -> Rep_Core.Classifier list
val removePackages : (Rep_Core.Classifier list * Context.context list)
-> string list
-> (Rep_Core.Classifier list * Context.context list)
val removeOclLibrary : Rep_Core.Classifier list -> Rep_Core.Classifier list
end
structure ModelImport : MODEL_IMPORT =
struct
(* basic library *)
open List
open Posix.Error
(* OclParser *)
open Ext_Library
open Context
open TypeChecker
open Update_Model
(* Error logging *)
val high = 5
val medium = 20
val low = 100
fun readFileUnNormalized f =
(RepParser.transformXMI o XmiParser.readFile) f
fun importArgoUMLUnNormalized file =
let
fun basename f = ((hd o rev) o (String.fields (fn x => x = #"/"))) f
val tmpFile = OS.FileSys.tmpName ()
val base = if String.isSuffix ".zargo" file
then String.substring(file,0, (String.size file) -6)
else file
val _ = print ("*** Syscall: unzip -ca "^base^".zargo "^(basename base)^".xmi > "^tmpFile^"\n")
val _ = OS.Process.system ("unzip -ca "^base^".zargo "^(basename base)^".xmi > "^tmpFile)
val model = readFileUnNormalized tmpFile
val _ = OS.FileSys.remove tmpFile
in
model
end
fun parseUML umlFile =
let
val _ = trace high "### Parsing UML Model ###\n"
val umlModel = if String.isSuffix ".zargo" umlFile
then importArgoUMLUnNormalized umlFile
else readFileUnNormalized umlFile
val _ = trace high ("### Finished Parsing UML Model ("
^(Int.toString(length umlModel))
^" Classifiers found)###\n\n")
in
umlModel
end
fun parseOCL oclFile =
let
val _ = trace high "### Parsing OCL File ###\n"
val ocl = case oclFile of
"" => []
| filename => OclParser.parse_contextlist oclFile;
val _ = trace high ("### Finished Parsing OCL File ("
^(Int.toString(length ocl))
^" Constraints Found) ###\n\n")
in
ocl
end
fun removePackages (uml,ocl) packageList =
let
fun filter_package model p = filter (fn cl => not (Rep_Core.package_of cl = p)) model
fun filter_cl_package cl p = filter (fn cl => not (package_of_context cl = p)) cl
val _ = trace high "### Excluding Packages ###\n"
val uml =
let
fun stringToPath s = (String.tokens (fn s => (s = (#":"))) s)
in
foldr (fn (p,m) => filter_package m (stringToPath p)) uml packageList
end
val ocl =
let
fun stringToPath s = (String.tokens (fn s => (s = (#":"))) s)
in
foldr (fn (p,m) => filter_cl_package m (stringToPath p)) ocl packageList
end
val _ = trace high ("### Finished excluding Packages ("
^(Int.toString(length uml))
^ " Classifiers found and "
^(Int.toString(length ocl))
^" Constraints Found) ###\n\n")
in
(uml,ocl)
end
fun removeOclLibrary model =
let
fun filter_template model =
let
fun is_template (Rep_Core.Template _) = true
| is_template _ = false
in
filter (not o is_template) model
end
fun filter_oclLib model = filter (not o OclLibrary.is_oclLib) model
in
(filter_oclLib o filter_template) model
end
fun import xmifile oclfile excludePackages =
let
val xmi = parseUML xmifile
val ocl = parseOCL oclfile
val (xmi,ocl) = removePackages (xmi,ocl) excludePackages
val model = case ocl of
[] => xmi
| ocl => let
val _ = trace high "### Preprocess Context List ###\n"
val fixed_ocl = Preprocessor.preprocess_context_list ocl ((OclLibrary.oclLib)@xmi)
val _ = trace high "### Finished Preprocess Context List ###\n\n"
val _ = trace high "### Type Checking ###\n"
val typed_cl = TypeChecker.check_context_list fixed_ocl ((OclLibrary.oclLib)@xmi);
val _ = trace high "### Finished Type Checking ###\n\n"
val _ = print"### Updating Classifier List ###\n"
val model = Update_Model.gen_updated_classifier_list typed_cl ((OclLibrary.oclLib)@xmi);
val _ = trace high ("### Finished Updating Classifier List "
^(Int.toString(length model))
^ " Classifiers found (11 from 'oclLib') ###\n")
val _ = trace high "### Fixing Types ###\n"
val model = removeOclLibrary model
val model = FixTyping.transform_ocl_spec FixTyping.transformForHolOcl model
val _ = trace high "### Finished Fixing Types ###\n\n"
in
model
end
in
model
end
end

690
src/ocl_parser/ocl.grm Normal file
View File

@ -0,0 +1,690 @@
(**************************************************************************
* SML OCL 2.0 Parser - A Parser writen in SML for OCL 2.0
*
* Copyright (C) 2007 Manuel P. Krucker <mkrucker@ethz.ch>
*
**************************************************************************)
(*
THIS POINTS HAVE TO BE NOTICED TO UNDERSTAND THE SEMANTICS OF:
- context_declarations.sml
- type_checker.sml
i.) 'AttributeCall' needs a path for the name of the attriubte.
But it is not possible to extract the hole name when 'AttributeCall' is constructed.
So, we only have a 'Path' with one element, the name of the attribute.
But the type still is 'Path' because of the types.
ii.) We cannot know if a 'propertycall_exp_cs' is a member of a Class or a Variable of the signature.
Therefore, all calls to Variables from signature are parsed as 'AttributeCall's
*)
open Rep_OclTerm
open Rep_OclType
open Context
open Ext_Library
exception NotYetSupported of string
%%
%eop EOF
%left
%left LOG_AND LOG_OR LOG_XOR
%left LOG_IMPL
(* the operators precedencies *)
%name OclParser
%term EOF
| TICK of string
| COMMA of string
| ARROW_RIGHT of string
| DOT of string
| DBL_DOT of string
| COLON of string
| DBL_COLON of string
| SEMI_COLON of string
| EQUALS of string
| QUESTION_MARK of string
| HASH of string
| AT_PRE of string
| BAG of string
| COLLECTION of string
| SEQUENCE of string
| ORDERED_SET of string
| SET of string
| TUPLE of string
| TUPLE_TYPE of string
| BRACKET_OPEN of string
| BRACKET_CLOSE of string
| CARAT of string
| DBL_CARAT of string
| BODY of Context.ConditionType
| CONTEXT of string
| DEF of string
| DERIVE of Context.AttrOrAssoc
| ELSE of string
| ENDIF of string
| ENDPACKAGE of string
| FALSE of string
| FORALL of string
| TRUE of string
| IF of string
| IN of string
| INIT of Context.AttrOrAssoc
| INV of string
| LET of string
| PACKAGE of string
| PRE of Context.ConditionType
| POST of Context.ConditionType
| THEN of string
| PAREN_OPEN of string
| PAREN_CLOSE of string
| BRACE_OPEN of string
| BRACE_CLOSE of string
| VERTICAL_BAR of string
| GUARD of string
| ITERATE of string
| SELECT of string
| REJECT of string
| COLLECT of string
| ANY of string
| EXISTS of string
| ONE of string
| ISUNIQUE of string
| OCLISTYPEOF of string
| OCLISKINDOF of string
| OCLASTYPE of string
| MINUS of string
| STAR of string
| SLASH of string
| PLUS of string
| REL_NOTEQUAL of string
| REL_GT of string
| REL_LT of string
| REL_GTE of string
| REL_LTE of string
| LOG_AND of string
| LOG_OR of string
| LOG_XOR of string
| LOG_IMPL of string
| NOT of string
| INTEGER_LITERAL of string
| REAL_LITERAL of string
| STRING_LITERAL of string
| SIMPLE_NAME of string
%nonterm START of context list
| OclExpression of Rep_OclTerm.OclTerm
| LiteralExp of OclTerm
| PrimitiveLiteralExp of Rep_OclTerm.OclTerm
| IntegerLiteralExp of Rep_OclTerm.OclTerm
| BooleanLiteralExp of Rep_OclTerm.OclTerm
| StringLiteralExp of Rep_OclTerm.OclTerm
| RealLiteralExp of Rep_OclTerm.OclTerm
| ocl_file of context list
| package_constraint_list_cs_p of context list
| package_constraint_list_cs of context list
| path_name_cs of Path
| path_name_head_cs of Path
| context_declaration_list_cs of context list
| context_declaration_cs of context list
| attr_or_assoc_cs of context list
| classifier_context_declaration_cs of context list
| operation_context_declaration_cs of context list
| guard_context_declaration_cs of context list
| type_specifier of OclType
| init_or_der_value_cs_p of (AttrOrAssoc*OclTerm) list
| init_or_der_value_cs of (AttrOrAssoc*OclTerm)
| classifier_constraint_cs_p of (string option*OclTerm) list
| classifier_constraint_cs of (string option*OclTerm)
| operation_signature_cs of (string * OclType) list
| operation_constraint_cs_p of (Context.ConditionType*string option*OclTerm) list
| operation_constraint_cs of (Context.ConditionType*string option*OclTerm)
| guard_constraint_cs_p of (string option*OclTerm) list
| guard_constraint_cs of (string option*OclTerm)
| invariant_cs of OclTerm
| definition_cs of OclTerm
| op_constraint_stereotype_cs of Context.ConditionType
| simple_name of string
| definition_constraint_cs of OclTerm
| defined_entity_decl_cs of OclTerm
| ocl_attribute_defined_entity_decl_cs of (string * OclType)
| ocl_operation_defined_entity_decl_cs of string * ((string * OclType) list)
| formal_parameter_cs of (string * OclType)
| formal_parameter_list_cs of (string * OclType) list
| formal_parameter_list_tail_cs of (string * OclType) list
| operation_return_type_specifier_cs of OclType
| collection_literal_exp of OclTerm
| collection_type_identifier_cs of string
| collection_literal_parts_cs of CollectionPart list
| collection_literal_part_cs of CollectionPart
| collection_literal_parts_tail_cs of CollectionPart list
| collection_range_cs of CollectionPart
| expression of OclTerm
| collection_type_specifier_cs of OclType
| time_exp_cs of string
| is_marked_pre_cs of string
| if_exp_cs of OclTerm
| simple_type_specifier_cs of OclType
| tuple_type_specifier_cs of OclType
| ocl_expression_cs of OclTerm
| let_exp_cs of OclTerm
| message_arg_cs
| message_argument_list_cs
| message_argument_list_tail_cs
| identifier_cs of string
| iterator_name_cs of string
| ocl_op_name of string
| literal_exp_cs of OclTerm
| collection_literal_exp_cs of OclTerm
| tuple_literal_exp_cs of OclTerm
| primitive_literal_exp_cs of OclTerm
| numeric_literal_exp_cs of OclTerm
| string_literal_exp_cs of OclTerm
| boolean_literal_exp_cs of OclTerm
| integer_literal of OclTerm
| real_literal of OclTerm
| string_literal of OclTerm
| initialized_variable_list_cs of (string * OclType * OclTerm)list
| logical_exp_cs of OclTerm
| logical_exp_tail_cs of (string*OclTerm)
| relational_exp_cs of OclTerm
| relational_exp_tail_cs_p of (string*OclTerm)
| relational_exp_tail_cs of (string*OclTerm)
| logic_op of string
| additive_exp_cs of OclTerm
| additive_exp_tail_cs of (string*OclTerm)
| additive_exp_tail_cs_p of (string*OclTerm)
| rel_op of string
| multiplicative_exp_cs of OclTerm
| multiplicative_exp_tail_cs_p of (string*OclTerm)
| multiplicative_exp_tail_cs of (string*OclTerm)
| add_op of string
| unary_exp_cs of OclTerm
| mult_op of string
| unary_op of string
| postfix_exp_cs of OclTerm
| postfix_exp_tail_cs_p of OclTerm list
| postfix_exp_tail_cs of OclTerm
| primary_exp_cs of OclTerm
| property_call_exp_cs of OclTerm
| arrow_property_call_exp_cs of OclTerm
| signal_spec_exp_cs of OclTerm
| msg_operator_cs of OclTerm
| property_call_parameters_cs of (OclTerm * OclType) list
| qualifiers of CollectionPart list
| iterate_vars_cs
| initialized_variable_cs of (string * OclType * OclTerm)
| actual_parameter_list_cs of (OclTerm * OclType) list
| actual_parameter_list_tail_cs of (OclTerm * OclType) list
| actual_parameter_list_tail_cs_p of (OclTerm * OclType) list
| actual_parameter_list_element_cs of (OclTerm * OclType)
| formal_parameter_type_specifier of OclType
| iterator_vars_cs of (string*OclType)list
| initialized_variable_list_tail_cs_p of (string * OclType * OclTerm)list
| initialized_variable_list_tail_cs of (string * OclType * OclTerm)
| variable_initializer of OclTerm
| variable_declaration_cs of (string*OclType)
| variable_declaration_list_cs of (string*OclType)list
| variable_declaration_list_tail_cs of (string*OclType)list
| logical_exp_tail_cs_p of (string*OclTerm)
| type_argument
| classifier_context_declarations_cs
%pos (int * int * int)
%noshift EOF
%%
(* RETURN: context list *)
START : ocl_file (ocl_file)
(* RETURN: context list *)
ocl_file : package_constraint_list_cs_p (package_constraint_list_cs_p)
(* RETURN: context list *)
package_constraint_list_cs_p : package_constraint_list_cs (package_constraint_list_cs)
| package_constraint_list_cs package_constraint_list_cs_p (package_constraint_list_cs@package_constraint_list_cs_p)
(* RETURN: context list *)
package_constraint_list_cs : PACKAGE path_name_cs ENDPACKAGE (trace low ("Starts creatind empty package ... " ^ "\n"); ([Empty_context ("this is an empty context", Literal ("empty",OclVoid))]))
| PACKAGE path_name_cs context_declaration_list_cs ENDPACKAGE (trace low ("Starts creating contextes ..." ^ "\n"); (list_extend_path path_name_cs context_declaration_list_cs))
(* RETURN: context list *)
context_declaration_list_cs : context_declaration_cs (context_declaration_cs)
| context_declaration_cs context_declaration_list_cs (context_declaration_cs@context_declaration_list_cs)
(* RETURN: context list *)
context_declaration_cs : attr_or_assoc_cs (attr_or_assoc_cs)
| classifier_context_declaration_cs (classifier_context_declaration_cs)
| operation_context_declaration_cs (operation_context_declaration_cs)
| guard_context_declaration_cs (guard_context_declaration_cs)
(* RETURN: context list *)
attr_or_assoc_cs : CONTEXT path_name_cs COLON type_specifier init_or_der_value_cs_p (attr_list (path_name_cs, type_specifier, init_or_der_value_cs_p))
(* RETURN: string *)
simple_name : SIMPLE_NAME (trace low ("simple_name..." ^ "\n");SIMPLE_NAME)
(* RETURN: context list *)
classifier_context_declaration_cs : CONTEXT path_name_cs classifier_constraint_cs_p (inv_list (path_name_cs, classifier_constraint_cs_p))
(* RETURN: context list *)
operation_context_declaration_cs : CONTEXT path_name_cs operation_signature_cs operation_constraint_cs_p (cond_list (path_name_cs, operation_signature_cs, operation_constraint_cs_p))
(* RETURN: context list *)
guard_context_declaration_cs : CONTEXT path_name_cs guard_constraint_cs_p (guard_list (real_path (path_name_cs), guard_constraint_cs_p))
(* RETURN: (AttrOrAssoc,OclTerm) list 1.{INIT|DERIVE} 2.expression *)
init_or_der_value_cs_p: init_or_der_value_cs ([init_or_der_value_cs])
| init_or_der_value_cs init_or_der_value_cs_p ([init_or_der_value_cs]@init_or_der_value_cs_p)
(* RETURN: (string option, OclTerm) list 1.name 2.expression *)
classifier_constraint_cs_p : classifier_constraint_cs ([classifier_constraint_cs])
| classifier_constraint_cs classifier_constraint_cs_p ([classifier_constraint_cs]@classifier_constraint_cs_p)
(* RETURN: (ConditionType, string option, OclTerm) list 1.{Pre|Post|Body} 2. name 3.expression *)
operation_constraint_cs_p : operation_constraint_cs ([operation_constraint_cs])
| operation_constraint_cs operation_constraint_cs_p ([operation_constraint_cs]@operation_constraint_cs_p)
(* RETURN: (string option,OclTerm) list *)
guard_constraint_cs_p : guard_constraint_cs ([guard_constraint_cs])
| guard_constraint_cs guard_constraint_cs_p ([guard_constraint_cs]@guard_constraint_cs_p)
(* RETURN: (AttrOrAssoc, OclTerm) *)
init_or_der_value_cs : INIT COLON ocl_expression_cs (INIT, ocl_expression_cs)
| DERIVE COLON ocl_expression_cs (DERIVE, ocl_expression_cs)
(* RETURN: (string option, OclTerm) 1.name 2.expression *)
classifier_constraint_cs : INV COLON ocl_expression_cs (trace low ("INV COLON ocl_expression_cs ..." ^ "\n"); (NONE,ocl_expression_cs))
| INV simple_name COLON ocl_expression_cs (trace low ("INV simple_name COLON ocl_expression_cs ..." ^ "\n");(SOME(simple_name),ocl_expression_cs))
| DEF COLON definition_constraint_cs (NONE,definition_constraint_cs)
| DEF simple_name COLON definition_constraint_cs (SOME(simple_name),definition_constraint_cs)
(* RETURN: (ConditionType, string option, OclTerm) 1.{Pre|Post|Body} 2. name 3.expression*)
operation_constraint_cs : op_constraint_stereotype_cs COLON ocl_expression_cs (trace low ("operation_constraint_cs 1..." ^ "\n"); (op_constraint_stereotype_cs,NONE,ocl_expression_cs))
| op_constraint_stereotype_cs simple_name COLON ocl_expression_cs (trace low ("operation_constraint_cs 23454..." ^ "\n"); (op_constraint_stereotype_cs,SOME(simple_name),ocl_expression_cs))
(* RETURN: (string option, OclTerm) 1.name 2.expression *)
guard_constraint_cs : GUARD COLON ocl_expression_cs (NONE,ocl_expression_cs)
| GUARD simple_name COLON ocl_expression_cs (SOME(simple_name),ocl_expression_cs)
(* RETURN: OclTerm *)
definition_constraint_cs : defined_entity_decl_cs EQUALS ocl_expression_cs (OperationCall (defined_entity_decl_cs,DummyT,[OclLibPackage,"DummyT",EQUALS],[(ocl_expression_cs,DummyT)],DummyT))
(* RETURN: OclTerm *)
defined_entity_decl_cs : ocl_attribute_defined_entity_decl_cs (trace low ("AttributeCall 1 ..." ^ "\n");AttributeCall (Literal ("self2",DummyT),DummyT,[#1(ocl_attribute_defined_entity_decl_cs)],#2(ocl_attribute_defined_entity_decl_cs)))
| ocl_operation_defined_entity_decl_cs (OperationCall (Literal ("self2",DummyT),DummyT,[#1(ocl_operation_defined_entity_decl_cs)],List.map gen_literal_term (real_signature (#2(ocl_operation_defined_entity_decl_cs))),#2(List.last (#2(ocl_operation_defined_entity_decl_cs)))))
(* RETURN: (string * OclType) *)
ocl_attribute_defined_entity_decl_cs : formal_parameter_cs (formal_parameter_cs)
(* RETURN: (string * (string * OclType)) list *)
(* OclType is the return type *)
ocl_operation_defined_entity_decl_cs : simple_name operation_signature_cs (simple_name,operation_signature_cs)
(* RETURN: (string * OclType) list *)
(* last element of list is the return type. Only second part of tuple then used *)
operation_signature_cs : PAREN_OPEN PAREN_CLOSE (trace low ("operation_signature_cs ..." ^ "\n");[("",OclVoid)])
| PAREN_OPEN PAREN_CLOSE operation_return_type_specifier_cs (trace low ("operation_signature_cs ..." ^ "\n");[("",operation_return_type_specifier_cs)])
| PAREN_OPEN formal_parameter_list_cs PAREN_CLOSE (trace low ("operation_signature_cs ..." ^ "\n");formal_parameter_list_cs@[("",OclVoid)])
| PAREN_OPEN formal_parameter_list_cs PAREN_CLOSE operation_return_type_specifier_cs (trace low ("operation_signature_cs ..." ^ "\n");formal_parameter_list_cs@[("",operation_return_type_specifier_cs)])
(* RETURN: OclType *)
operation_return_type_specifier_cs : COLON type_specifier (trace low ("Contextes created form list of Attributes ..." ^ "\n");type_specifier)
(* RETURN: (ConditionType) *)
op_constraint_stereotype_cs : PRE (PRE)
| POST (POST)
| BODY (BODY)
(* Taken from OCL1.6 and merged with older OCL1.4 rules *)
(* RETURN: OclTerm *)
collection_literal_exp_cs : collection_type_identifier_cs BRACE_OPEN BRACE_CLOSE (CollectionLiteral ([],dispatch_collection (collection_type_identifier_cs,DummyT)))
| collection_type_identifier_cs BRACE_OPEN collection_literal_parts_cs BRACE_CLOSE (CollectionLiteral (collection_literal_parts_cs,dispatch_collection(collection_type_identifier_cs,DummyT)))
(* RETURN: CollectionPart list *)
collection_literal_parts_cs : collection_literal_part_cs ([collection_literal_part_cs])
| collection_literal_part_cs collection_literal_parts_tail_cs ([collection_literal_part_cs]@collection_literal_parts_tail_cs)
(* RETURN: CollectionPart list *)
collection_literal_parts_tail_cs : COMMA collection_literal_parts_cs (collection_literal_parts_cs)
(* RETURN: CollectionPart *)
collection_literal_part_cs : collection_range_cs (collection_range_cs)
| expression (CollectionItem (expression,DummyT))
(* RETURN: CollectionPart *)
collection_range_cs : expression DBL_DOT expression (CollectionRange (expression1,expression2,DummyT))
(* renamed to collection_type_specifier_cs from collection_type_cs *)
(* RETURN: OclType *)
collection_type_specifier_cs : collection_type_identifier_cs PAREN_OPEN type_specifier PAREN_CLOSE (dispatch_collection (collection_type_identifier_cs,type_specifier))
(* RETURN: string *)
collection_type_identifier_cs: SET (SET)
| BAG (BAG)
| SEQUENCE (SEQUENCE)
| COLLECTION (COLLECTION)
| ORDERED_SET (ORDERED_SET)
(* Part of OCL2.0 concrete syntax, but unused by now *)
(* expression_in_ocl_cs = ocl_expression_cs *)
(* RETURN: string *)
time_exp_cs : is_marked_pre_cs (is_marked_pre_cs)
(* RETURN: string *)
is_marked_pre_cs: AT_PRE (AT_PRE)
(* RETURN: OclType *)
(* NOT YET SUPPORTED
??? QUESTION: How can i implement this ???
tuple_type_specifier_cs : TUPLE_TYPE PAREN_OPEN PAREN_CLOSE (let _ = raise (NotYetSupported "not yet supported") in DummyT end)
| TUPLE_TYPE PAREN_OPEN formal_parameter_list_cs PAREN_CLOSE (let _ = raise (NotYetSupported "not yet supported") in DummyT end)
*)
(* RETURN: OclTerm *)
ocl_expression_cs : logical_exp_cs (trace low ("ocl_expression_cs..." ^ "\n");logical_exp_cs)
| let_exp_cs (trace low ("ocl_expression_cs..." ^ "\n");let_exp_cs)
(* RETURN: OclTerm *)
let_exp_cs : LET initialized_variable_list_cs IN expression (gen_let_term initialized_variable_list_cs expression)
(* RETURN: OclTerm *)
expression : ocl_expression_cs (ocl_expression_cs)
(* NOT YET SUPPORTED
??? QUESTION: this is used for what ???
message_arg_cs : QUESTION_MARK
| QUESTION_MARK formal_parameter_type_specifier
| expression
message_argument_list_cs : message_arg_cs
| message_arg_cs message_argument_list_tail_cs
message_argument_list_tail_cs : COMMA message_argument_list_cs
*)
(* RETURN: string *)
iterator_name_cs : SELECT (SELECT)
| REJECT (REJECT)
| COLLECT (COLLECT)
| FORALL (FORALL)
| EXISTS (EXISTS)
| ANY (ANY)
| ONE (ONE)
| ISUNIQUE (ISUNIQUE)
(* RETURN: String *)
ocl_op_name : OCLISKINDOF (OCLISKINDOF)
| OCLISTYPEOF (OCLISTYPEOF)
| OCLASTYPE (OCLASTYPE)
(* RETURN: Path *)
path_name_cs : identifier_cs (trace low ("path_name finished..." ^ "\n");[identifier_cs])
| path_name_head_cs identifier_cs (trace low ("path_name generation ..." ^ "\n");path_name_head_cs@[identifier_cs])
(* RETURN : string *)
identifier_cs : simple_name (trace low ("path_name generation..." ^ "\n");simple_name)
| ITERATE (ITERATE)
| iterator_name_cs (iterator_name_cs)
| ocl_op_name (ocl_op_name)
(* RETURN: Path *)
path_name_head_cs : identifier_cs DBL_COLON (trace low ("path_name generation..." ^ "\n");[identifier_cs])
| path_name_head_cs identifier_cs DBL_COLON (trace low ("path_name generation..." ^ "\n");path_name_head_cs@[identifier_cs])
(* RETURN: OclTerm *)
literal_exp_cs : primitive_literal_exp_cs (trace low ("primitive_literal_exp_cs..." ^ "\n");primitive_literal_exp_cs)
| collection_literal_exp_cs (collection_literal_exp_cs)
(* NOT YET SUPPORTED ...
| tuple_literal_exp_cs (tuple_literal_exp_cs)
*)
primitive_literal_exp_cs : numeric_literal_exp_cs (trace low ("numeric_literal_exp_cs..." ^ "\n");numeric_literal_exp_cs)
| string_literal_exp_cs (trace low ("string_literal_exp_cs..." ^ "\n");string_literal_exp_cs)
| boolean_literal_exp_cs (boolean_literal_exp_cs)
numeric_literal_exp_cs : INTEGER_LITERAL (trace low ("INTEGER_LITERAL..." ^ "\n");Literal (INTEGER_LITERAL,Integer))
| REAL_LITERAL (Literal (REAL_LITERAL,Real))
string_literal_exp_cs : STRING_LITERAL (Literal (STRING_LITERAL,String))
boolean_literal_exp_cs : TRUE (Literal ("true",Boolean))
| FALSE (Literal ("false",Boolean))
(* NOT SUPPORTED YET
tuple_literal_exp_cs : TUPLE BRACE_OPEN initialized_variable_list_cs BRACE_CLOSE
*)
(* RETURN: OclTerm *)
logical_exp_cs : relational_exp_cs (trace low ("logical_exp_cs..." ^ "\n");relational_exp_cs)
| relational_exp_cs logical_exp_tail_cs_p (trace low ("logical_exp_cs..." ^ "\n");OperationCall(relational_exp_cs,Boolean,[OclLibPackage,"Boolean",#1(logical_exp_tail_cs_p)],[(#2(logical_exp_tail_cs_p),Boolean)],Boolean))
(* RETURN: (logic_op, OclTerm) *)
logical_exp_tail_cs_p : logical_exp_tail_cs (logical_exp_tail_cs)
| logical_exp_tail_cs logical_exp_tail_cs_p ((#1(logical_exp_tail_cs),OperationCall(#2(logical_exp_tail_cs),Boolean,[OclLibPackage,"Boolean",#1(logical_exp_tail_cs_p)],[(#2(logical_exp_tail_cs_p),Boolean)],Boolean)))
(* RETURN: (logic_op, Ocl_Term) *)
logical_exp_tail_cs : logic_op relational_exp_cs (logic_op,relational_exp_cs)
(* RETURN: string *)
logic_op : LOG_AND (LOG_AND)
| LOG_OR (LOG_OR)
| LOG_XOR (LOG_XOR)
| LOG_IMPL (LOG_IMPL)
(* RETURN: OclTerm *)
relational_exp_cs : additive_exp_cs (trace low ("additive_exp_cs..." ^ "\n");additive_exp_cs)
| additive_exp_cs relational_exp_tail_cs (trace low ("additive_exp_cs relational_exp_tail_cs ..." ^ "\n");OperationCall(additive_exp_cs,DummyT,[OclLibPackage,"DummyT",#1(relational_exp_tail_cs)],[(#2(relational_exp_tail_cs),DummyT)],Boolean))
(* RETURN: (rel_op, Ocl_Term) *)
relational_exp_tail_cs : rel_op additive_exp_cs (trace low ("relational_exp_tail_cs..." ^ "\n");(rel_op, additive_exp_cs))
(* RETURN: string *)
rel_op : EQUALS (EQUALS)
| REL_GT (trace low (">..." ^ "\n");REL_GT)
| REL_LT (trace low ("<..." ^ "\n");REL_LT)
| REL_GTE (REL_GTE)
| REL_LTE (REL_LTE)
| REL_NOTEQUAL (REL_NOTEQUAL)
(* RETURN: OclTerm *)
additive_exp_cs : multiplicative_exp_cs (trace low ("multiplicative_exp_cs..." ^ "\n");multiplicative_exp_cs)
| multiplicative_exp_cs additive_exp_tail_cs_p (trace low ("multiplicative_exp_cs additive_exp_tail_cs_p..." ^ "\n");OperationCall (multiplicative_exp_cs,DummyT,[OclLibPackage,"DummyT",#1(additive_exp_tail_cs_p)],[(#2(additive_exp_tail_cs_p),DummyT)],DummyT))
(* RETURN: (add_op, Ocl_Term) *)
additive_exp_tail_cs_p : additive_exp_tail_cs (additive_exp_tail_cs)
| additive_exp_tail_cs additive_exp_tail_cs_p (#1(additive_exp_tail_cs),OperationCall (#2(additive_exp_tail_cs),DummyT,[OclLibPackage,"DummyT",#1(additive_exp_tail_cs_p)],[(#2(additive_exp_tail_cs_p),DummyT)],DummyT))
(* RETURN: (add_op,Ocl_Term) *)
additive_exp_tail_cs : add_op multiplicative_exp_cs (add_op, multiplicative_exp_cs)
(* RETURN: string *)
add_op: PLUS (PLUS)
| MINUS (MINUS)
(* RETURN: OclTerm *)
multiplicative_exp_cs: unary_exp_cs (trace low ("unary_exp_cs ..." ^ "\n");unary_exp_cs)
| unary_exp_cs multiplicative_exp_tail_cs_p (OperationCall (unary_exp_cs,DummyT,[OclLibPackage,"DummyT",#1(multiplicative_exp_tail_cs_p)],[(#2(multiplicative_exp_tail_cs_p),DummyT)],DummyT))
(* RETURN: (mult_op, Ocl_Term ) *)
multiplicative_exp_tail_cs_p : multiplicative_exp_tail_cs (multiplicative_exp_tail_cs)
| multiplicative_exp_tail_cs multiplicative_exp_tail_cs_p (#1(multiplicative_exp_tail_cs),OperationCall (#2(multiplicative_exp_tail_cs),DummyT,[OclLibPackage,"DummyT",#1(multiplicative_exp_tail_cs_p)],[(#2(multiplicative_exp_tail_cs_p),DummyT)],DummyT))
(* RETURN: (mult_op, Ocl_Term) *)
multiplicative_exp_tail_cs : mult_op unary_exp_cs (mult_op, unary_exp_cs)
(* RETURN: string *)
mult_op : STAR (STAR)
| SLASH (SLASH)
(* RETURN: OclTerm *)
unary_exp_cs : unary_op postfix_exp_cs (OperationCall (postfix_exp_cs,DummyT,[OclLibPackage,"DummyT",unary_op],[],DummyT))
| postfix_exp_cs (postfix_exp_cs)
(* RETURN: String *)
unary_op : MINUS (MINUS)
| NOT (NOT)
(* RETURN: OclTerm *)
postfix_exp_cs : primary_exp_cs (primary_exp_cs)
| primary_exp_cs postfix_exp_tail_cs_p (trace low ("literal_call_exp_cs..." ^ "\n");nest_source ([primary_exp_cs]@postfix_exp_tail_cs_p))
(* NOT YET IMPLEMENTED
| msg_operator_cs signal_spec_exp_cs
*)
(* RETURN: OclTerm *)
primary_exp_cs : literal_exp_cs (trace low ("literal_call_exp_cs..." ^ "\n");literal_exp_cs)
| PAREN_OPEN expression PAREN_CLOSE (expression)
| property_call_exp_cs (trace low ("property_call_exp_cs..." ^ "\n");property_call_exp_cs)
| if_exp_cs (if_exp_cs)
(* RETURN: OclTerm *)
if_exp_cs: IF logical_exp_cs THEN ocl_expression_cs ELSE ocl_expression_cs ENDIF (If (logical_exp_cs,DummyT,ocl_expression_cs1,DummyT,ocl_expression_cs2,DummyT,DummyT))
(* RETURN: OclTerm list *)
postfix_exp_tail_cs_p : postfix_exp_tail_cs (trace low ("end of recursion..." ^ Ocl2String.ocl2string false postfix_exp_tail_cs ^ "\n");[postfix_exp_tail_cs])
| postfix_exp_tail_cs postfix_exp_tail_cs_p (trace low ("add_source ..." ^ "\n" ^ "done");([postfix_exp_tail_cs]@postfix_exp_tail_cs_p))
(* RETURN: OclTerm *)
postfix_exp_tail_cs : DOT property_call_exp_cs (property_call_exp_cs)
| ARROW_RIGHT arrow_property_call_exp_cs (arrow_property_call_exp_cs)
(* NOT YET SUPPORTED
| msg_operator_cs signal_spec_exp_cs
*)
(* RETURN: OclTerm *)
(* time_exp_cs ('atPre') gets handled separately in the preprocessor *)
property_call_exp_cs : path_name_cs (AttributeCall (Variable ("dummy_source",DummyT),DummyT,path_name_cs, DummyT))
(* '@pre'-expressions for 'AttributeCalls' *)
| path_name_cs time_exp_cs (AttributeCall (Variable ("dummy_source",DummyT),DummyT,path_name_cs@["atPre"],DummyT))
| path_name_cs property_call_parameters_cs (OperationCall (Variable ("dummy_source",DummyT),DummyT,path_name_cs , property_call_parameters_cs,DummyT))
(* '@pre'-expressions for 'OperationCalls' *)
| path_name_cs time_exp_cs property_call_parameters_cs (OperationCall (Variable ("dummy_source",DummyT),DummyT,path_name_cs@["atPre"],property_call_parameters_cs,DummyT))
(* NOT YET SUPPORTED
| path_name_cs qualifiers (CollectionLiteral (qualifiers, dispatch_collection (List.last path_name_cs,qualifiers)))
| path_name_cs qualifiers time_exp_cs
*)
(* RETURN: OclTerm *)
arrow_property_call_exp_cs: iterator_name_cs PAREN_OPEN expression PAREN_CLOSE (Iterator (iterator_name_cs,[],Variable("dummy_source",DummyT),DummyT,expression,DummyT,DummyT))
| iterator_name_cs PAREN_OPEN iterator_vars_cs expression PAREN_CLOSE (trace low ("arrow_property_call_cs: iterator with vars..." ^ "\n");Iterator (iterator_name_cs,iterator_vars_cs,Variable("dummy_source",DummyT),DummyT,expression,DummyT,DummyT))
| simple_name PAREN_OPEN PAREN_CLOSE (trace low ("arrow_property_call_exp_cs..." ^ "\n");OperationCall (Variable ("dummy_source",DummyT),DummyT,(["arrow"]@[simple_name]),[],DummyT))
| simple_name PAREN_OPEN actual_parameter_list_cs PAREN_CLOSE (OperationCall (Variable ("dummy_source",DummyT),DummyT,(["arrow"]@[simple_name]),actual_parameter_list_cs,DummyT))
(*
| ITERATE PAREN_OPEN initialized_variable_cs VERTICAL_BAR expression PAREN_CLOSE ()
| ITERATE PAREN_OPEN iterate_vars_cs initialize_variable_cs VERTICAL_BAR expression PAREN_CLOSE ()
*)
(*
(* RETURN: (string * OclType) list *)
iterate_vars_cs : actual_parameter_list_cs SEMI_COLON ()
*)
(* RETURN: (string * OclType) list *)
iterator_vars_cs : formal_parameter_list_cs VERTICAL_BAR (formal_parameter_list_cs)
(*
(* RETURN: ... *)
msg_operator_cs : CARAT ()
| DBL_CARAT ()
*)
(* NOT YET SUPPORTED
qualifiers : BRACKET_OPEN actual_parameter_list_cs BRACKET_CLOSE (actual_parameter_list_cs)
*)
type_argument : PAREN_OPEN type_specifier PAREN_CLOSE (type_specifier)
(* RETURN: (OclTerm * OclType) list *)
property_call_parameters_cs : PAREN_OPEN actual_parameter_list_cs PAREN_CLOSE (actual_parameter_list_cs)
| PAREN_OPEN PAREN_CLOSE ([])
(* NOT SUPPORTED YET
signal_spec_exp_cs : simple_name PAREN_OPEN PAREN_CLOSE
| simple_name PAREN_OPEN message_argument_list_cs PAREN_CLOSE
*)
(* RETURN: (OclTerm * OclType) list *)
actual_parameter_list_cs : actual_parameter_list_element_cs ([actual_parameter_list_element_cs])
| actual_parameter_list_element_cs actual_parameter_list_tail_cs_p ([actual_parameter_list_element_cs]@actual_parameter_list_tail_cs_p)
(* RETURN: (OclTerm * OclType) list *)
actual_parameter_list_tail_cs_p : actual_parameter_list_tail_cs (actual_parameter_list_tail_cs)
| actual_parameter_list_tail_cs actual_parameter_list_tail_cs_p (actual_parameter_list_tail_cs@actual_parameter_list_tail_cs_p)
(* RETURN: (OclTerm * OclType) list *)
actual_parameter_list_tail_cs : COMMA actual_parameter_list_cs (actual_parameter_list_cs)
(* RETURN: (OclTerm * OclType) *)
actual_parameter_list_element_cs : expression (expression,DummyT)
| formal_parameter_cs (Variable (#1(formal_parameter_cs),#2(formal_parameter_cs)),#2(formal_parameter_cs))
(* RETURN: (string * OclType) list *)
formal_parameter_list_cs : formal_parameter_cs ([formal_parameter_cs])
| formal_parameter_cs formal_parameter_list_tail_cs ([formal_parameter_cs]@formal_parameter_list_tail_cs)
(* RETURN: (string, OclType) list *)
formal_parameter_list_tail_cs : COMMA formal_parameter_list_cs (formal_parameter_list_cs)
(* RETURN: (string, OclType) *)
formal_parameter_cs : simple_name formal_parameter_type_specifier (simple_name,formal_parameter_type_specifier)
(* RETURN: OclType *)
formal_parameter_type_specifier : COLON type_specifier (type_specifier)
(* RETURN: OclType *)
type_specifier: simple_type_specifier_cs (trace low ("type_specifier ..." ^ "\n");simple_type_specifier_cs)
| collection_type_specifier_cs (collection_type_specifier_cs)
(*
| typle_type_specifier_cs
*)
(* RETURN: OclType *)
simple_type_specifier_cs : simple_name (string_to_type [simple_name])
(* RETURN: (string * OclType * OclTerm) list *)
initialized_variable_list_cs : initialized_variable_cs ([initialized_variable_cs])
| initialized_variable_list_tail_cs_p (initialized_variable_list_tail_cs_p)
(* RETURN: (string * OclType * OclTerm) list *)
initialized_variable_list_tail_cs_p : initialized_variable_list_tail_cs ([initialized_variable_list_tail_cs])
| initialized_variable_list_tail_cs initialized_variable_list_tail_cs_p ([initialized_variable_list_tail_cs]@(initialized_variable_list_tail_cs_p))
(* RETURN: (string * OclType * OclTerm) *)
initialized_variable_list_tail_cs : COMMA initialized_variable_cs (initialized_variable_cs)
(* RETURN: (string * OclType * OclTerm*)
initialized_variable_cs : formal_parameter_cs variable_initializer ((#1 formal_parameter_cs),(#2 formal_parameter_cs),variable_initializer)
(* RETURN: (string * OclType) *)
variable_declaration_cs : formal_parameter_cs (formal_parameter_cs)
(* RETRUN: (OclTerm) *)
variable_initializer : EQUALS ocl_expression_cs (ocl_expression_cs)
(* RETURN: (string * OclType) list *)
variable_declaration_list_cs : variable_declaration_cs ([variable_declaration_cs])
| variable_declaration_cs variable_declaration_list_tail_cs ([variable_declaration_cs]@variable_declaration_list_tail_cs)
(* RETURN: (string * OclType) list *)
variable_declaration_list_tail_cs : COMMA variable_declaration_list_cs (variable_declaration_list_cs)

134
src/ocl_parser/ocl.lex Normal file
View File

@ -0,0 +1,134 @@
open Rep_OclTerm
open Rep_OclType
open Context
structure Tokens = Tokens
type pos = int * int * int
type svalue = Tokens.svalue
type ('a,'b) token = ('a,'b) Tokens.token
type lexresult= (svalue,pos) token
val pos = ref (0,0,0)
fun eof () = Tokens.EOF((!pos,!pos))
fun error (e,p : (int * int * int),_) = TextIO.output (TextIO.stdOut,
String.concat[
"line ", (Int.toString (#1 p)), "/",
(Int.toString (#2 p - #3 p)),": ", e, "\n"
])
fun inputPos yypos = ((#1 (!pos), yypos - (#3(!pos)), (#3 (!pos))),
(#1 (!pos), yypos - (#3(!pos)), (#3 (!pos))))
fun inputPos_half yypos = (#1 (!pos), yypos - (#3(!pos)), (#3 (!pos)))
%%
%header (functor OclParserLexFun(structure Tokens: OclParser_TOKENS));
alpha=[A-Za-z_];
digit=[0-9];
ws = [\ \t];
%%
\n => (pos := ((#1 (!pos)) + 1, yypos - (#3(!pos)),yypos ); lex());
{ws}+ => (pos := (#1 (!pos), yypos - (#3(!pos)), (#3 (!pos))); lex());
(--)[^\n]*\n => (pos := ((#1 (!pos)) + 1, yypos - (#3(!pos)),yypos ); lex());
"/*""/"*([^*/]|[^*]"/"|"*"[^/])*"*"*"*/" => (lex());
"," => (Tokens.COMMA(yytext,inputPos_half yypos,inputPos_half yypos));
"->" => (Tokens.ARROW_RIGHT(yytext,inputPos_half yypos,inputPos_half yypos));
"." => (Tokens.DOT(yytext,inputPos_half yypos,inputPos_half yypos));
".." => (Tokens.DBL_DOT(yytext,inputPos_half yypos,inputPos_half yypos));
":" => (Tokens.COLON(yytext,inputPos_half yypos,inputPos_half yypos));
"::" => (Tokens.DBL_COLON(yytext,inputPos_half yypos,inputPos_half yypos));
";" => (Tokens.SEMI_COLON(yytext,inputPos_half yypos,inputPos_half yypos));
"=" => (Tokens.EQUALS(yytext,inputPos_half yypos,inputPos_half yypos));
"?" => (Tokens.QUESTION_MARK(yytext,inputPos_half yypos,inputPos_half yypos));
"#" => (Tokens.HASH(yytext,inputPos_half yypos,inputPos_half yypos));
"@pre" => (Tokens.AT_PRE(yytext,inputPos_half yypos,inputPos_half yypos));
"Bag" => (Tokens.BAG(yytext,inputPos_half yypos,inputPos_half yypos));
"Collection" => (Tokens.COLLECTION(yytext,inputPos_half yypos,inputPos_half yypos));
"OrderedSet" => (Tokens.ORDERED_SET(yytext,inputPos_half yypos,inputPos_half yypos));
"Sequence" => (Tokens.SEQUENCE(yytext,inputPos_half yypos,inputPos_half yypos));
"Set" => (Tokens.SET(yytext,inputPos_half yypos,inputPos_half yypos));
"Tuple" => (Tokens.TUPLE(yytext,inputPos_half yypos,inputPos_half yypos));
"TupleType" => (Tokens.TUPLE_TYPE(yytext,inputPos_half yypos,inputPos_half yypos));
"[" => (Tokens.BRACKET_OPEN(yytext,inputPos_half yypos,inputPos_half yypos));
"]" => (Tokens.BRACKET_CLOSE(yytext,inputPos_half yypos,inputPos_half yypos));
"^" => (Tokens.CARAT(yytext,inputPos_half yypos,inputPos_half yypos));
"^^" => (Tokens.DBL_CARAT(yytext,inputPos_half yypos,inputPos_half yypos));
"body" => (Tokens.BODY(body,inputPos_half yypos,inputPos_half yypos));
"context" => (Tokens.CONTEXT(yytext,inputPos_half yypos,inputPos_half yypos));
"def" => (Tokens.DEF(yytext,inputPos_half yypos,inputPos_half yypos));
"derive" => (Tokens.DERIVE(derive,inputPos_half yypos,inputPos_half yypos));
"else" => (Tokens.ELSE(yytext,inputPos_half yypos,inputPos_half yypos));
"endif" => (Tokens.ENDIF(yytext,inputPos_half yypos,inputPos_half yypos));
"endpackage" => (Tokens.ENDPACKAGE(yytext,inputPos_half yypos,inputPos_half yypos));
"false" => (Tokens.FALSE(yytext,inputPos_half yypos,inputPos_half yypos));
"if" => (Tokens.IF(yytext,inputPos_half yypos,inputPos_half yypos));
"in" => (Tokens.IN(yytext,inputPos_half yypos,inputPos_half yypos));
"init" => (Tokens.INIT(init,inputPos_half yypos,inputPos_half yypos));
"inv" => (Tokens.INV(yytext,inputPos_half yypos,inputPos_half yypos));
"let" => (Tokens.LET(yytext,inputPos_half yypos,inputPos_half yypos));
"package" => (Tokens.PACKAGE(yytext,inputPos_half yypos,inputPos_half yypos));
"pre" => (Tokens.PRE(pre,inputPos_half yypos,inputPos_half yypos));
"post" => (Tokens.POST(post,inputPos_half yypos,inputPos_half yypos));
"then" => (Tokens.THEN(yytext,inputPos_half yypos,inputPos_half yypos));
"true" => (Tokens.TRUE(yytext,inputPos_half yypos,inputPos_half yypos));
"(" => (Tokens.PAREN_OPEN(yytext,inputPos_half yypos,inputPos_half yypos));
")" => (Tokens.PAREN_CLOSE(yytext,inputPos_half yypos,inputPos_half yypos));
"{" => (Tokens.BRACE_OPEN(yytext,inputPos_half yypos,inputPos_half yypos));
"}" => (Tokens.BRACE_CLOSE(yytext,inputPos_half yypos,inputPos_half yypos));
"|" => (Tokens.VERTICAL_BAR(yytext,inputPos_half yypos,inputPos_half yypos));
"guard" => (Tokens.GUARD(yytext,inputPos_half yypos,inputPos_half yypos));
"iterate" => (Tokens.ITERATE(yytext,inputPos_half yypos,inputPos_half yypos));
"select" => (Tokens.SELECT(yytext,inputPos_half yypos,inputPos_half yypos));
"reject" => (Tokens.REJECT(yytext,inputPos_half yypos,inputPos_half yypos));
"collect" => (Tokens.COLLECT(yytext,inputPos_half yypos,inputPos_half yypos));
"forAll" => (Tokens.FORALL(yytext,inputPos_half yypos,inputPos_half yypos));
"any" => (Tokens.ANY(yytext,inputPos_half yypos,inputPos_half yypos));
"exists" => (Tokens.EXISTS(yytext,inputPos_half yypos,inputPos_half yypos));
"one" => (Tokens.ONE(yytext,inputPos_half yypos,inputPos_half yypos));
"isUnique" => (Tokens.ISUNIQUE(yytext,inputPos_half yypos,inputPos_half yypos));
"oclIsTypeOf" => (Tokens.OCLISTYPEOF(yytext,inputPos_half yypos,inputPos_half yypos));
"oclIsKindOf" => (Tokens.OCLISKINDOF(yytext,inputPos_half yypos,inputPos_half yypos));
"oclAsType" => (Tokens.OCLASTYPE(yytext,inputPos_half yypos,inputPos_half yypos));
"-" => (Tokens.MINUS(yytext,inputPos_half yypos,inputPos_half yypos));
"*" => (Tokens.STAR(yytext,inputPos_half yypos,inputPos_half yypos));
"/" => (Tokens.SLASH(yytext,inputPos_half yypos,inputPos_half yypos));
"+" => (Tokens.PLUS(yytext,inputPos_half yypos,inputPos_half yypos));
">" => (Tokens.REL_GT(yytext,inputPos_half yypos,inputPos_half yypos));
"<" => (Tokens.REL_LT(yytext,inputPos_half yypos,inputPos_half yypos));
">=" => (Tokens.REL_GTE(yytext,inputPos_half yypos,inputPos_half yypos));
"<=" => (Tokens.REL_LTE(yytext,inputPos_half yypos,inputPos_half yypos));
"<>" => (Tokens.REL_NOTEQUAL(yytext,inputPos_half yypos,inputPos_half yypos));
"and" => (Tokens.LOG_AND(yytext,inputPos_half yypos,inputPos_half yypos));
"or" => (Tokens.LOG_OR(yytext,inputPos_half yypos,inputPos_half yypos));
"xor" => (Tokens.LOG_XOR(yytext,inputPos_half yypos,inputPos_half yypos));
"implies" => (Tokens.LOG_IMPL(yytext,inputPos_half yypos,inputPos_half yypos));
"not" => (Tokens.NOT(yytext,inputPos_half yypos,inputPos_half yypos));
{digit}+"."{digit}+(E|e)?({digit})* => (Tokens.REAL_LITERAL(yytext,inputPos_half yypos,inputPos_half yypos));
{digit}+ => (Tokens.INTEGER_LITERAL(yytext,inputPos_half yypos,inputPos_half yypos));
"'"({alpha}|{ws}|{digit})*(("."|"_"|"/"|"-")*({alpha}|{ws}|{digit})*)*"'" => (Tokens.STRING_LITERAL(yytext,inputPos_half yypos,inputPos_half yypos));
{alpha}+(_)?({alpha}|{digit})* => (Tokens.SIMPLE_NAME(yytext,inputPos_half yypos,inputPos_half yypos));
. => (error ("ignoring bad character "^yytext,
((#1 (!pos), yypos - (#3(!pos)), (#3 (!pos)))),
((#1 (!pos), yypos - (#3(!pos)), (#3 (!pos)))));
lex());

26
src/ocl_parser/parser.110.62.cm Normal file
View File

@ -0,0 +1,26 @@
Group is
#if(defined(SMLNJ_VERSION))
$smlnj/basis/basis.cm
$smlnj/compiler/compiler.cm
$smlnj/smlnj-lib/smlnj-lib.cm
#else
#endif
../su4sml/src/su4sml.110.62.cm
#if defined (NEW_CM)
$smlnj/basis/basis.cm
$smlnj/ml-yacc/ml-yacc-lib.cm
#else
ml-yacc-lib.cm
#endif
ocl.grm
ocl.lex
parser.sml
context_declarations.sml
library.sml
preprocessor.sml
type_checker.sml
make_classifier_list.sml
fix_types.sml
model_import.sml

26
src/ocl_parser/parser.cm Normal file
View File

@ -0,0 +1,26 @@
Group is
#if(defined(SMLNJ_VERSION))
$/basis.cm
$smlnj/compiler/compiler.cm
$/smlnj-lib.cm
#else
#endif
../su4sml/src/su4sml.cm
#if defined (NEW_CM)
$/basis.cm
$/ml-yacc-lib.cm
#else
ml-yacc-lib.cm
#endif
ocl.grm
ocl.lex
parser.sml
library.sml
context_declarations.sml
preprocessor.sml
type_checker.sml
make_classifier_list.sml
fix_types.sml
model_import.sml

89
src/ocl_parser/parser.sml Normal file
View File

@ -0,0 +1,89 @@
structure OclParser : sig
val parse : string -> unit
val parse_contextlist: string -> Context.context list
end =
struct
open Context
structure OclParserLrVals =
OclParserLrValsFun(structure Token = LrParser.Token)
structure OclParserLex =
OclParserLexFun(structure Tokens = OclParserLrVals.Tokens)
structure OclParserParser =
Join(structure LrParser = LrParser
structure ParserData = OclParserLrVals.ParserData
structure Lex = OclParserLex)
(*
* We need a function which given a lexer invokes the parser. The
* function invoke does this.
*)
(* Error logging *)
val high = 5
val medium = 20
val low = 100
fun invoke lexstream =
let fun print_error (s,i:(int * int * int),_) =
TextIO.output(TextIO.stdOut,
"Error, line .... " ^ (Int.toString (#1 i)) ^"."^(Int.toString (#2 i ))^ ", " ^ s ^ "\n")
in OclParserParser.parse(0,lexstream,print_error,())
end
(*
* Finally, we need a driver function that reads one or more expressions
* from the standard input. The function parse, shown below, does
* this. It runs the calculator on the standard input and terminates when
* an end-of-file is encountered.
*)
fun parse oclFile =
let
val infile = TextIO.openIn oclFile
val lexer = OclParserParser.makeLexer (fn _ => case ((TextIO.inputLine) infile) of
SOME s => s
| NONE => "")
val ocl = ""
val dummyEOF = OclParserLrVals.Tokens.EOF((0,0,0),(0,0,0))
fun loop lexer =
let
val _ = (OclParserLex.UserDeclarations.pos := (0,0,0);())
val (res,lexer) = invoke lexer
val (nextToken,lexer) = OclParserParser.Stream.get lexer
val _ = TextIO.output(TextIO.stdOut,(cxt_list2string res) ^ "\n")
in if OclParserParser.sameToken(nextToken,dummyEOF) then ()
else loop lexer
end
in loop lexer
end
fun parse_contextlist oclFile =
let
val infile = TextIO.openIn oclFile
val lexer = OclParserParser.makeLexer (fn _ => case ((TextIO.inputLine) infile) of
SOME s => s
| NONE => "")
val ocl = ""
val dummyEOF = OclParserLrVals.Tokens.EOF((0,0,0),(0,0,0))
fun loop lexer =
let
val _ = (OclParserLex.UserDeclarations.pos := (0,0,0);())
val (res,lexer) = invoke lexer
val (nextToken,lexer) = OclParserParser.Stream.get lexer
(*
val _ = TextIO.output(TextIO.stdOut,(cxt_list2string res) ^ "\n")
*)
in if OclParserParser.sameToken(nextToken,dummyEOF) then ((),res)
else loop lexer
end
in (#2(loop lexer))
end
end

407
src/ocl_parser/preprocessor.sml Normal file
View File

@ -0,0 +1,407 @@
(*****************************************************************************
* SML OCL 2.0 Parser - Parser/TypeChecker for OCL 2.0 written in SML(NJ)
*
* library.sml - main "ROOT.ML" file for HOL-OCL
* Copyright (C) 2007 Manuel P. Krucker <mkrucker@ethz.ch>
*
* This file is part of HOL-OCL.
*
* HOL-OCL is free software; you can redistribute it and/or modify it under
* the terms of the GNU General Public License as published by the Free
* Software Foundation; either version 2 of the License, or (at your option)
* any later version.
*
* HOL-OCL is distributed in the hope that it will be useful, but WITHOUT ANY
* WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
* FOR A PARTICULAR PURPOSE. See the GNU General Public License for more
* details.
*
* You should have received a copy of the GNU General Public License along
* with this program; if not, write to the Free Software Foundation, Inc.,
* 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
*****************************************************************************)
signature PREPROCESSOR =
sig
val preprocess_context_list : Context.context list -> Rep_Core.Classifier list -> Context.context list
val embed_bound_variables : (string * Rep_OclType.OclType) list -> Rep_OclTerm.OclTerm -> Rep_OclTerm.OclTerm
end
structure Preprocessor:PREPROCESSOR =
struct
open Context
open Rep_OclTerm
open Rep_OclType
open Rep_Core
open RepParser
open XMI_DataTypes
open OclLibrary
open Ext_Library
type operation = Rep_Core.operation
type attribute = Rep_Core.attribute
(* The problem here is, that when parsing the ocl file, there is something the parser cannot
know. Therefore we have to solve the problem before to type check.
PROBLEM 1:
The parser can never know if it is an absolute call for an operation or an attribute, or
a relative call.
Example: x.hallo >= 0
Possiblity 1:
context A::f(x:Object):Integer
pre: x > 0
to get classifier x look up in the signature for Object x
Possiblity 2:
context A::f(y:Object):Integer
pre: x > 0
to get classifier x look up in the classifer list at self.x
This problem is solve by going through all the contexts, looking whether the attribute calls
refer to self or signature arguemnts.
Used methods:
- member
- fetch
- check_for_self
PROBLEM 2:
The parser parses a call to result following:
******************************************************
post: result = 0
AttributeCall (Variable("self",_),...,["result"], ...)
******************************************************
So we have to substitute this by: Variable ("result",typ_of_operation_return_typ)
PROBLEM 3:
The parser parses the OperationWithType calls wrong.
PROBLEM 4:
package simple
context A
inv : self.i->forAll(a:B | ...)
endpackage
but the type is not (Classifier (["B"]) but (Classifier (["simple","B"])
PROBLEM 5:
'@pre'-expressions needs to be treated separately
*)
(*
TEMPLATE FOR TERM:
fun embed_atPre_expressions (Varible (str,type)) =
| embed_atPre_expressions (Literal (str,type)) =
| embed_atPre_expressions (CollectionLiteral (collpart,typ)) =
| embed_atPre_expressions (If (cond,cond_type,then_e,then_type,else_e,else_type,res_type)) path meth_name model=
| embed_atPre_expressions (AttributeCall (sterm,styp,p,res_typ)) path meth_name model =
| embed_atPre_expressions (OperationCall (sterm,styp,pa,para,res_typ)) path meth_name model =
| embed_atPre_expressions (OperationWithType (sterm,stype,para_name,para_type,res_type)) path meth_name model =
| embed_atPre_expressions (Let (var_name,var_type,rhs,rhs_type,in_e,in_type)) path meth_name model =
| embed_atPre_expressions (Iterator (name,iter_vars,sterm,stype,body_e,body_type,res_type)) path meth_name model =
*)
(* RETURN: bool *)
fun member x [] = false
| member x (h::tail) =
if (x = h) then
true
else
member x tail
(* RETURN: OclTerm *)
fun embed_atPre_expressions_collpart (CollectionItem (term,typ)) =
(CollectionItem (embed_atPre_expressions term,typ))
| embed_atPre_expressions_collpart (CollectionRange (term1,term2,typ)) =
(CollectionRange (embed_atPre_expressions term1, embed_atPre_expressions term2, typ))
and embed_atPre_expressions (Variable (str,typ)) = (Variable (str,typ))
| embed_atPre_expressions (Literal (str,typ)) = (Literal (str,typ))
| embed_atPre_expressions (CollectionLiteral (collpart,typ)) =
(CollectionLiteral (List.map (embed_atPre_expressions_collpart) collpart,typ))
| embed_atPre_expressions (If (cond,cond_type,then_e,then_type,else_e,else_type,res_type)) =
(If (embed_atPre_expressions cond,cond_type,embed_atPre_expressions then_e,then_type,embed_atPre_expressions else_e,else_type,res_type))
| embed_atPre_expressions (AttributeCall (sterm,styp,p,res_typ)) =
if (List.last (p) = "atPre")
then (* atPre Call *)
(
if (List.length p = 1)
then (* self *)
(OperationCall (sterm,styp,[OclLibPackage,"OclAny","atPre"],[],DummyT))
else (* contains at least one 'normal' attribute *)
(AttributeCall (OperationCall (embed_atPre_expressions sterm,styp,[OclLibPackage,"OclAny","atPre"],[],DummyT),styp,real_path p,res_typ))
)
else (* normal Call *)
(AttributeCall (embed_atPre_expressions sterm,styp,p,res_typ))
| embed_atPre_expressions (OperationCall (sterm,styp,pa,para,res_typ)) =
let
val atpre_para = List.map (fn (a,b) => (embed_atPre_expressions a,b)) para
in
if (List.last (pa) = "atPre")
then (OperationCall (OperationCall (embed_atPre_expressions sterm,styp,real_path pa,atpre_para,res_typ),DummyT,[OclLibPackage,"OclAny","atPre"],[],DummyT))
else (OperationCall (embed_atPre_expressions sterm,styp,pa,atpre_para,res_typ))
end
| embed_atPre_expressions (OperationWithType (sterm,stype,para_name,para_type,res_type)) =
(OperationWithType (embed_atPre_expressions sterm,stype,para_name,para_type,res_type))
| embed_atPre_expressions (Let (var_name,var_type,rhs,rhs_type,in_e,in_type)) =
(Let (var_name,var_type,embed_atPre_expressions rhs,rhs_type,embed_atPre_expressions in_e,in_type))
| embed_atPre_expressions (Iterator (name,iter_vars,sterm,stype,body_e,body_type,res_type)) =
(Iterator (name,iter_vars,embed_atPre_expressions sterm,stype,embed_atPre_expressions body_e,body_type,res_type))
(* RETURN: OclTerm *)
fun embed_bound_variable (str,typ) (Variable(s,t)) =
let
val _ = trace zero ("1 Bound variable '" ^ s ^ "' in 'AttributeCall': " ^ Ocl2String.ocl2string false (Variable(s,t)) ^ "\n")
in
if (str = s ) then
Variable(s,typ)
else
Variable(s,t)
end
| embed_bound_variable (s,typ) (AttributeCall (sterm,styp,path,rtyp)) =
let
val _ = trace zero ("2 Bound variable '" ^ s ^ "' in 'AttributeCall': " ^ Ocl2String.ocl2string false (AttributeCall (sterm,styp,path,rtyp)) ^ "\n")
in
if (List.last path = s) then
(* embed variable *)
(Variable (s,typ))
else
(AttributeCall (embed_bound_variable (s,typ) sterm,styp,path,rtyp))
end
| embed_bound_variable (s,typ) (OperationCall (sterm,styp,path,args,rtyp)) =
let
val _ = trace zero ("Bound variable '" ^ s ^ "' in 'OperationCall': " ^ Ocl2String.ocl2string false (OperationCall (sterm,styp,path,args,rtyp)) ^ "\n")
in
(OperationCall (embed_bound_variable (s,typ) sterm,styp,path,embed_bound_args (s,typ) args ,rtyp))
end
| embed_bound_variable (s,typ) (Iterator (name,iter_list,sterm,styp,expr,expr_typ,rtyp)) =
let
val _ = trace zero ("Bound variable '" ^ s ^ "' in 'Iterator': " ^ Ocl2String.ocl2string false (Iterator (name,iter_list,sterm,styp,expr,expr_typ,rtyp)) ^ "\n")
in
(Iterator (name,iter_list,embed_bound_variable (s,typ) sterm,styp,embed_bound_variables iter_list (embed_bound_variable (s,typ) expr),expr_typ,rtyp))
end
| embed_bound_variable (s,typ) (Let (var_name,var_type,rhs,rhs_type,in_e,in_type)) =
let
val _ = trace zero ("Bound variable '" ^ s ^ "' in 'Let': " ^ Ocl2String.ocl2string false (Let (var_name,var_type,rhs,rhs_type,in_e,in_type)) ^ "\n")
val embed_in_e = embed_bound_variable (var_name,var_type) in_e
in
(Let (var_name,var_type,embed_bound_variable (s,typ) rhs,rhs_type,embed_bound_variable (s,typ) embed_in_e,in_type))
end
| embed_bound_variable (s,typ) (If (cond,cond_type,then_e,then_type,else_e,else_type,res_type)) =
let
val _ = trace zero ("Bound variable '" ^ s ^ "' in 'If' ..." ^ "\n")
in
(If (embed_bound_variable (s,typ) cond,cond_type,embed_bound_variable (s,typ) then_e,then_type,embed_bound_variable (s,typ) else_e,else_type,res_type))
end
| embed_bound_variable (s,typ) term = term
(* RETURN: IDENDITAET *)
and swap f a b = f b a
(* RETURN: OclTerm *)
and embed_bound_variables [] term = term
| embed_bound_variables (h::tail) term =
(embed_bound_variables tail (embed_bound_variable h term))
(* RETURN: (OclTerm * OclType) list *)
and embed_bound_args (str,typ) [] = []
| embed_bound_args (str,typ) (h::arg_list) =
(embed_bound_variable (str,typ) (#1 h),#2 h)::(embed_bound_args (str,typ) arg_list)
(* RETURN: OclTerm *)
(* Better readable source code *)
fun embed_method_arguments [] term = term
| embed_method_arguments ((str,typ)::tail) term =
embed_method_arguments tail (embed_bound_variable (str,typ) term)
(* RETURN: OclTerm *)
fun embed_iterator_variables arg_list term = embed_method_arguments arg_list term
(* For the existing variables in Ocl.
There is only one (I know, maybe some more).
It can be easily extende here
*)
(* RETURN: CollectionPart list *)
fun generate_variables_coll_list ((CollectionItem (term,typ))::tail) path meth_name model =
(CollectionItem(generate_variables term path meth_name model,typ))::(generate_variables_coll_list tail path meth_name model)
| generate_variables_coll_list ((CollectionRange (first_term,last_term,typ))::tail) path meth_name model =
(CollectionRange(generate_variables first_term path meth_name model,generate_variables last_term path meth_name model,typ))::(generate_variables_coll_list tail path meth_name model)
(* RETURN: OclTerm *)
and generate_variables (Literal (paras)) path meth_name model = Literal (paras)
| generate_variables (Variable (paras)) path meth_name model = Variable (paras)
| generate_variables (CollectionLiteral (collpart_list,typ)) path meth_name model =
(CollectionLiteral (generate_variables_coll_list collpart_list path meth_name model,typ))
| generate_variables (If (cond,cond_type,then_e,then_type,else_e,else_type,res_type)) path meth_name model=
(If (generate_variables cond path meth_name model,cond_type,generate_variables then_e path meth_name model,then_type,generate_variables else_e path meth_name model,else_type,res_type))
| generate_variables (AttributeCall (_,_,["result"],_)) path meth_name model =
let
val classifier = class_of path model
val meth_list = operations_of classifier
val meth = find_operation meth_name meth_list
val _ = trace zero ("a result call resolved ..." ^ "\n")
in
(Variable ("result",(#result meth)))
end
| generate_variables (AttributeCall (sterm,styp,p,res_typ)) path meth_name model =
(AttributeCall (generate_variables sterm path meth_name model,styp,p,res_typ))
| generate_variables (OperationCall (sterm,styp,pa,para,res_typ)) path meth_name model =
let
val _ = print ("recursive embed 'result' ... \n")
in
(OperationCall (generate_variables sterm path meth_name model,styp,pa,para,res_typ))
end
| generate_variables (OperationWithType (sterm,stype,para_name,para_term,res_type)) path meth_name model =
(OperationWithType (generate_variables sterm path meth_name model,stype,para_name,para_term,res_type))
| generate_variables (Let (var_name,var_type,rhs,rhs_type,in_e,in_type)) path meth_name model =
(Let (var_name,var_type,generate_variables rhs path meth_name model,rhs_type,generate_variables in_e path meth_name model,in_type))
| generate_variables (Iterator (name,iter_vars,sterm,stype,body_e,body_type,res_type)) path meth_name model =
(Iterator (name,iter_vars,generate_variables sterm path meth_name model,stype,generate_variables body_e path meth_name model,body_type,res_type))
(* RETURN: (string*OclType) *)
fun fetch (x,((y1,y2)::tail)) =
if (x=y1) then
(y1,y2)
else
fetch (x,tail)
(* RETURN: OclTerm list *)
fun check_for_self_paras arg_list typ [] model = []
| check_for_self_paras arg_list typ ((term,t)::tail) model = ((check_for_self arg_list typ term model),t)::(check_for_self_paras arg_list typ tail model)
and
(* RETURN: OclTerm *)
check_for_self arg_list typ (AttributeCall (Variable("dummy_source",_),_,path,_)) model=
let
val test = (member (List.last path) (List.map (#1) arg_list))
val _ = trace zero ("member? "^ Bool.toString (test) ^ "\n")
in
if (List.last path = "self") then
(* 'self' is writen in the ocl file *)
(Variable ("self",typ))
else
(AttributeCall (Variable ("self",typ),DummyT,path,DummyT))
end
| check_for_self arg_list typ (AttributeCall (source_term,source_typ,path,ret_typ)) model =
let
val _ = trace zero ("check_for_self: complex AttributeCall "^ "\n")
in
(AttributeCall (check_for_self arg_list typ source_term model,source_typ,path,ret_typ))
end
(* OperationCall *)
| check_for_self arg_list typ (OperationCall (Variable ("dummy_source",_),source_type,path,paras,ret_typ)) model =
let
val test = (member (List.last path) (List.map (#1) arg_list))
val _ = trace zero ("member2? "^ Bool.toString (test) ^ "\n")
in
if (member (List.last path) (List.map (#1) arg_list))
then
(* Call of a method parameter *)
(Variable ((#1 (fetch ((List.last path), arg_list))), (#2 (fetch ((List.last path),arg_list)))))
else
(* Call of a member of the class *)
(OperationCall (Variable ("self",typ),source_type,path,check_for_self_paras arg_list typ paras model,ret_typ))
end
| check_for_self arg_list typ (OperationCall (source_term,source_typ,path,paras,ret_typ)) model =
let
val _ = trace zero ("check_for_self: complex OperationCall "^ "\n")
in
(OperationCall (check_for_self arg_list typ source_term model ,source_typ,path,check_for_self_paras arg_list typ paras model,ret_typ))
end
| check_for_self arg_list typ (Iterator (name,iter_var,sterm,styp,expr,expr_typ,res_typ)) model =
let
val _ = trace zero ("check_for_self: complex OperationCall "^ "\n")
in
(Iterator (name,iter_var,(check_for_self arg_list typ sterm model),styp,(check_for_self arg_list typ expr model),expr_typ,res_typ))
end
| check_for_self arg_list typ (Let (str,ttyp,rhs_term,rhs_typ,in_term,in_typ)) model =
let
val self_rhs_term = check_for_self arg_list typ rhs_term model
val self_in_term = check_for_self arg_list typ in_term model
in
(Let (str,ttyp,self_rhs_term,rhs_typ,self_in_term,in_typ))
end
| check_for_self arg_list typ (If (cond,cond_typ,expr1,typ1,expr2,typ2,res_typ)) model =
let
val self_cond = check_for_self arg_list typ cond model
val self_expr1 = check_for_self arg_list typ expr1 model
val self_expr2 = check_for_self arg_list typ expr2 model
in
(If (self_cond,cond_typ,self_expr1,typ1,self_expr2,typ2,res_typ))
end
| check_for_self arg_list typ term model = term
(* RETURN: Context *)
fun preprocess_context (Cond (path,op_name,op_sign,result_type,cond,pre_name,expr)) model =
let
(* embed 'result' variable *)
val _ = trace zero ("Embed result variable \n")
val vexpr = generate_variables expr path op_name model
val _ = trace zero ("Variable 'result' embeded ... \n")
(* embed method arguments *)
val class = class_of_type (Classifier (path)) model
val prfx = package_of class
val prefixed_op_sign = List.map (fn (a,b) => (a,prefix_type prfx b)) op_sign
val prefixed_result_type = prefix_type prfx result_type
val eexpr = embed_method_arguments prefixed_op_sign vexpr
(* embed '@pre'-expressions *)
val pexpr = embed_atPre_expressions eexpr
in
(Cond (path,op_name,prefixed_op_sign,prefixed_result_type,cond,pre_name,(check_for_self prefixed_op_sign (Classifier (path)) pexpr model)))
end
| preprocess_context (Inv (path,string,term)) model =
let
val _ = trace zero ("Preprocess context: Inv (...)" ^ "\n")
(* embed '@pre'-expressions *)
val pexpr = embed_atPre_expressions term
in
(Inv (path,string,(check_for_self [] (Classifier (path)) pexpr model)))
end
| preprocess_context (Attr (path,typ,aoa,expr)) model =
let
val _ = trace zero ("Preprocess context: Attr"^ "\n")
(* embed '@pre'-expressions *)
val pexpr = embed_atPre_expressions expr
in
(Attr (path,typ,aoa,check_for_self [] (Classifier (path)) pexpr model))
end
| preprocess_context c model =
let
val _ = trace zero ("Preprocess context: others" ^ "\n")
in
c
end
(* RETURN: Context list *)
fun preprocess_context_list [] model = []
| preprocess_context_list (h::context_list_tail) model = (preprocess_context h model)::(preprocess_context_list context_list_tail model)
end

19
src/ocl_parser/script.sml Normal file
View File

@ -0,0 +1,19 @@
(* simple script for debugging and testing *)
(* this script requires that the environment variable
SU4SML_HOME
points to the su4sml top-level directory (i.e., `pwd`/../su4sml")
*)
(* display settings: printDepth = 1000 *)
Control.Print.printDepth := 5000;
fun print_depth n =
(Control.Print.printDepth := n div 2;
Control.Print.printLength := n);
val model = ModelImport.import "../examples/ebank/ebank.xmi"
"../examples/ebank/ebank.manuel.ocl" [];

157
src/ocl_parser/test-suite.sml Normal file
View File

@ -0,0 +1,157 @@
type result = {
parse : bool,
preprocess : bool,
typecheck : bool,
update : bool,
msg : string
}
type testcase = {
name : string,
uml : string,
ocl : string,
result : result
}
val initResult = {
parse = false,
preprocess = false,
typecheck = false,
update = false,
msg = ""
}:result
val prefix = "../examples/"
val testcases = [
{
name = "Company",
uml = prefix^"company/company.zargo",
ocl = prefix^"company/company.ocl",
result = initResult
}:testcase,
{
name = "ebank (Manuel)",
uml = prefix^"ebank/ebank.zargo",
ocl = prefix^"ebank/ebank.ocl",
result = initResult
}:testcase,
{
name = "encoding_example",
uml = prefix^"encoding_example/encoding_example.zargo",
ocl = prefix^"encoding_example/encoding_example.ocl",
result = initResult
}:testcase,
{
name = "isp",
uml = prefix^"isp/isp.zargo",
ocl = prefix^"isp/isp.ocl",
result = initResult
}:testcase,
{
name = "Royals and Loyals",
uml = prefix^"royals_and_loyals/royals_and_loyals.zargo",
ocl = prefix^"royals_and_loyals/royals_and_loyals.ocl",
result = initResult
}:testcase,
{
name = "simple",
uml = prefix^"simple/simple.zargo",
ocl = prefix^"simple/simple.ocl",
result = initResult
}:testcase,
{
name = "stack",
uml = prefix^"stack/stack.zargo",
ocl = prefix^"stack/stack.ocl",
result = initResult
}:testcase,
{
name = "digraph",
uml = prefix^"digraph/digraph.zargo",
ocl = prefix^"digraph/digraph.ocl",
result = initResult
}:testcase,
{
name = "vehicles",
uml = prefix^"vehicles/vehicles.zargo",
ocl = prefix^"vehicles/vehicles.ocl",
result = initResult
}:testcase
]
fun test (tc:testcase) =
let
val xmi = ModelImport.parseUML (#uml tc)
handle _ => []
val ocl = ModelImport.parseOCL (#ocl tc)
handle _ => []
val OclParse = if ocl = [] then false else true
val (xmi,ocl) = ModelImport.removePackages (xmi,ocl) []
handle _ => ([],[])
val _ = print "### Preprocess Context List ###\n"
val fixed_ocl = Preprocessor.preprocess_context_list ocl ((OclLibrary.oclLib)@xmi)
handle _ => []
val OclPreprocess = if fixed_ocl = [] then false else true
val _ = print "### Finished Preprocess Context List ###\n\n"
val _ = print "### Type Checking ###\n"
val typed_cl = TypeChecker.check_context_list fixed_ocl ((OclLibrary.oclLib)@xmi)
handle _ => []
val OclTC = if typed_cl = [] then false else true
val _ = print "### Finished Type Checking ###\n\n"
val _ = print"### Updating Classifier List ###\n"
val model = Update_Model.gen_updated_classifier_list typed_cl ((OclLibrary.oclLib)@xmi)
handle _ => []
val modelUpdate = if model = [] then false else true
val _ = print "### Finished Updating Classifier List ###\n"
val model = ModelImport.removeOclLibrary model
in
{
name = #name tc,
uml = #uml tc,
ocl = #ocl tc,
result =
{
parse = OclParse,
preprocess = OclParse andalso OclPreprocess,
typecheck = OclParse andalso OclPreprocess andalso OclTC,
update = OclParse andalso OclPreprocess andalso OclTC andalso modelUpdate,
msg = ""
}:result
}:testcase
end
fun printResult (tc:testcase) =
let
fun printBool b = if b then "passed" else "FAILED"
val _ = print ("\n *** "^(#name tc)^" ***\n")
val res = (#result tc)
val _ = print (" parsing: "^(printBool (#parse res))^"\n")
val _ = print (" preprocess: "^(printBool (#preprocess res))^"\n")
val _ = print (" typecheck: "^(printBool (#typecheck res))^"\n")
val _ = print (" update: "^(printBool (#update res))^"\n\n")
val _ = print (" ==> overall: "^(printBool ((#parse res)
andalso (#preprocess res)
andalso (#typecheck res)
andalso (#update res)))^"\n")
in
()
end
val _ = (Ext_Library.log_level := 10);();
val testcases = map test testcases
val _ = map printResult testcases

9
src/ocl_parser/todo.txt Normal file
View File

@ -0,0 +1,9 @@
what needs to be done:
- new copy of AssociationEndCall in typechecker.sml
(now written as comment and it is not actuall)

651
src/ocl_parser/type_checker.sml Normal file
View File

@ -0,0 +1,651 @@
(*****************************************************************************
* SML OCL 2.0 Parser - Parser/TypeChecker for OCL 2.0 written in SML(NJ)
*
* type_checker.sml - main "ROOT.ML" file for HOL-OCL
* Copyright (C) 2007 Manuel P. Krucker <mkrucker@ethz.ch>
*
* This file is part of HOL-OCL.
*
* HOL-OCL is free software; you can redistribute it and/or modify it under
* the terms of the GNU General Public License as published by the Free
* Software Foundation; either version 2 of the License, or (at your option)
* any later version.
*
* HOL-OCL is distributed in the hope that it will be useful, but WITHOUT ANY
* WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
* FOR A PARTICULAR PURPOSE. See the GNU General Public License for more
* details.
*
* You should have received a copy of the GNU General Public License along
* with this program; if not, write to the Free Software Foundation, Inc.,
* 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
*****************************************************************************)
signature TYPECHECKER =
sig
exception wrongCollectionLiteral of Rep_OclTerm.OclTerm * string
exception CollectionRangeError of Rep_OclTerm.CollectionPart * string
exception IteratorTypeMissMatch of Rep_OclTerm.OclTerm * string
exception NoSuchIteratorNameError of Rep_OclTerm.OclTerm * string
exception TypeCheckerResolveIfError of Rep_OclTerm.OclTerm * string
exception NotYetSupportedError of string
exception WrongContextChecked of Context.context
val check_context_list : Context.context list -> Rep_Core.Classifier list -> Context.context option list
val check_context : Context.context -> Rep_Core.Classifier list -> Context.context option
val resolve_OclTerm : Rep_OclTerm.OclTerm -> Rep_Core.Classifier list -> Rep_OclTerm.OclTerm
val resolve_CollectionPart : Rep_Core.Classifier list -> Rep_OclTerm.CollectionPart -> Rep_OclTerm.CollectionPart
val resolve_arguments : (Rep_OclTerm.OclTerm * Rep_OclType.OclType) list -> Rep_Core.Classifier list -> (Rep_OclTerm.OclTerm * Rep_OclType.OclType) list
end
structure TypeChecker:TYPECHECKER =
struct
open Context
open Rep_OclTerm
open Rep_OclType
open Rep_Core
open RepParser
open XMI_DataTypes
open Preprocessor
open OclLibrary
open Ext_Library
type operation = Rep_Core.operation
type attribute = Rep_Core.attribute
exception wrongCollectionLiteral of Rep_OclTerm.OclTerm * string
exception CollectionRangeError of Rep_OclTerm.CollectionPart * string
exception IteratorTypeMissMatch of Rep_OclTerm.OclTerm * string
exception NoSuchIteratorNameError of Rep_OclTerm.OclTerm * string
exception TypeCheckerResolveIfError of Rep_OclTerm.OclTerm * string
exception NotYetSupportedError of string
exception WrongContextChecked of context
exception AsSetError of (OclTerm * string list * int * (OclTerm * OclType) list * Classifier list)
exception DesugaratorCall of (OclTerm * string list * int * (OclTerm * OclType) list * Classifier list)
(* RETURN: bool *)
fun check_argument_type [] [] = true
| check_argument_type [x] [] = false
| check_argument_type [] [x] = false
| check_argument_type list [] = false
| check_argument_type [] list = false
| check_argument_type [(term,typ1:OclType)] [(string,typ2:OclType)] =
if (typ1 = typ2) then
true
else
false
| check_argument_type ((term,typ1)::sig_tail1) ((string,typ2)::sig_tail2) =
if (typ1 = typ2) then
(check_argument_type sig_tail1 sig_tail2)
else false
(* RETURN: OclTerm (OperationCall/AttributeCall) *)
fun FromSet_desugarator rterm path attr_or_meth rargs model =
if (attr_or_meth = 0)
then (* OperationCall *)
let
(* check 'fromSet' *)
val _ = trace low ("\n==> FromSet-desugarator: operation ... \n")
val new_type = template_parameter (type_of_term rterm)
val iterVar = (("anonIterVar_" ^ (varcounter.nextStr())),new_type)
val class = get_classifier (Variable (iterVar)) model
val ops = get_overloaded_methods class (List.last path) model
in
if (List.length ops = 0)
then raise InterferenceError ("FromSet no operation/attribute found. \n")
else
let
val insert_term = interfere_methods ops (Variable iterVar) rargs model
val it_type = type_of_term insert_term
in
Iterator ("collect",[iterVar],rterm,type_of_term rterm,insert_term,it_type,it_type)
end
end
else (* AttributeCall *)
let
(* check 'fromSet' *)
val _ = trace low ("\n==> FromSet-desugarator: attribute/assocend ... \n")
val new_type = template_parameter (type_of_term rterm)
val iterVar = (("anonIterVar_" ^ (varcounter.nextStr())),new_type)
val class = get_classifier (Variable (iterVar)) model
val attrs_or_assocs = get_overloaded_attrs_or_assocends class (List.last path) model
in
if (List.length attrs_or_assocs = 0)
then raise InterferenceError ("Attriubte '" ^ (List.last path) ^ "' does not exist ... \n")
else
let
val insert_term = interfere_attrs_or_assocends attrs_or_assocs (Variable iterVar) model
val it_type = type_of_term insert_term
val _ = trace development ("association type " ^ string_of_OclType it_type ^ "\n")
(* special case *)
(* if it is an attribute, there needs to be added a collection type constructor *)
in
case (List.hd attrs_or_assocs) of
(* AttributeCall *)
(x,SOME(shit),NONE) =>
let
val ret_type = replace_templ_para (type_of_term rterm) it_type
in
Iterator ("collect",[iterVar],rterm,type_of_term rterm,insert_term,it_type,ret_type)
end
(* AssociatonCall *)
| (x,NONE,SOME(shit)) =>
if (isColl_Type it_type)
then
let
val ret_type = replace_templ_para (type_of_term rterm) (template_parameter it_type)
in
Iterator("collect",[iterVar],rterm,type_of_term rterm,insert_term,it_type,ret_type)
end
else
let
val ret_type = replace_templ_para (type_of_term rterm) it_type
in
Iterator("collect",[iterVar],rterm,type_of_term rterm,insert_term,it_type,ret_type)
end
end
end
(* RETURN: OclTerm (OperationCall/AttributeCall) *)
fun AsSet_desugarator rterm path attr_or_meth rargs model =
if (attr_or_meth = 0)
then (* OperationCall *)
let
val _ = trace low ("\n==> AsSet-desugarator: operation ... \n")
val rtyp = Set(type_of_term rterm)
val _ = trace low ("Type of source term " ^ string_of_OclType rtyp ^ " ---> try Set(" ^ string_of_OclType rtyp ^ ")\n")
val class = get_classifier (Variable ("anonIterVar_" ^ (varcounter.nextStr()),rtyp)) model
val ops = get_overloaded_methods class (List.last path) model
val new_rterm = CollectionLiteral([CollectionItem(rterm,type_of_term rterm)],rtyp)
in
if (List.length ops = 0)
then
raise NoSuchOperationError ("interefere_methods: No operation signature matches given types (source: "^(Ocl2String.ocl2string false rterm)^").")
else
interfere_methods ops new_rterm rargs model
end
else (* AttributeCall *)
let
val _ = trace low ("\n==> AsSet-desugarator: attribute/assocend\n")
val rtyp = Set(type_of_term rterm)
val _ = trace low (string_of_OclType rtyp ^ "\n")
val class = get_classifier (Variable ("anonIterVar_" ^ (varcounter.nextStr()),Set(rtyp))) model
val attrs = get_overloaded_attrs_or_assocends class (List.last path) model
(* source term is a dummy-Term *)
val new_rterm = CollectionLiteral([CollectionItem(rterm,type_of_term rterm)],rtyp)
val _ = trace low ("'AsSetError' ... \n")
in
if (List.length attrs = 0)
then
raise NoSuchAttributeError ("Attriubte '" ^ (List.last path) ^ "' does not exist ... \n")
else
interfere_attrs_or_assocends attrs new_rterm model
end
(* RETURN: OclTerm (OperationCall/AttributeCall) *)
fun desugarator rterm path attr_or_meth rargs model =
FromSet_desugarator rterm path attr_or_meth rargs model
handle InterferenceError s => AsSet_desugarator rterm path attr_or_meth rargs model
(* RETURN: CollectionPart *)
fun resolve_CollectionPart model (CollectionItem (term,typ)) =
let
val rterm = resolve_OclTerm term model
val rtyp = type_of_term rterm
in
(CollectionItem (rterm,rtyp))
end
| resolve_CollectionPart model (CollectionRange (term1,term2,typ)) =
let
val rterm1 = resolve_OclTerm term1 model
val rtyp1 = type_of_term rterm1
val rterm2 = resolve_OclTerm term2 model
val rtyp2 = type_of_term rterm2
in
if (rtyp2 = rtyp1) then
(CollectionRange (rterm1,rterm2,rtyp1))
else
raise (CollectionRangeError ((CollectionRange (term1,term2,typ)),("Begin and end of Range not of same type.\n")))
end
and resolve_CollectionLiteral (CollectionLiteral (part_list,typ)) model =
let
val rpart_list = List.map (resolve_CollectionPart model) part_list
val tlist = List.map (type_of_CollPart) rpart_list
in
if (List.all (type_equals (List.hd (tlist))) tlist)
then
rpart_list
else
raise wrongCollectionLiteral ((CollectionLiteral (part_list,typ)),"Not all Literals have the same type.\n")
end
(* RETURN: OclTerm * OclType *)
and resolve_arguments [] model = []
| resolve_arguments ((term,typ)::list_tail) model =
let
val rterm = resolve_OclTerm term model
val rtyp = type_of_term rterm
in
(rterm,rtyp)::(resolve_arguments list_tail model)
end
(* RETURN: OclTerm *)
and resolve_OclTerm (Literal (s,typ)) model =
let
val _ = trace medium ("RESOLVE Literal: " ^ s ^ "\n")
in
(Literal (s,typ))
end
(* Variable *)
| resolve_OclTerm (Variable ("self",typ)) model = (Variable ("self",typ))
| resolve_OclTerm (Variable (name,typ)) model =
let
val _ = trace medium ("RESOLVE Variable: " ^ name ^ "\n")
in
Variable (name,typ)
end
(* AssociationEndCall *)
| resolve_OclTerm (AssociationEndCall (term,_,["self"],_)) model = (resolve_OclTerm (AttributeCall (term,OclAny,["self"],OclAny)) model)
| resolve_OclTerm (AssociationEndCall (term,_,attr_path,_)) model = (resolve_OclTerm (AttributeCall (term,OclAny,attr_path,OclAny)) model)
(* AttributeCall *)
(* self.self -> self *)
| resolve_OclTerm (AttributeCall (term,_,["self"],_)) model =
let
val _ = trace medium ("RESOLVE AttributeCall: a self call ... " ^ "\n")
in
(resolve_OclTerm term model)
end
| resolve_OclTerm (AttributeCall (term,_,attr_path,_)) model =
let
val _ = trace medium ("RESOLVE AttributeCall: attribute name: " ^ (List.last attr_path) ^ "\n")
(* resolve source term *)
val rterm = resolve_OclTerm term model
val _ = trace low ("res AttCall (" ^ (List.last attr_path) ^ ") : rterm = " ^ Ocl2String.ocl2string false rterm ^ "\n")
val _ = trace low ("res AttCall (" ^ (List.last attr_path) ^ ") : rtype = " ^ string_of_OclType (type_of_term rterm) ^ "\n")
in
let
in
if (List.hd attr_path = "arrow")
then get_attr_or_assoc rterm (List.last attr_path) model
handle InterferenceError s => AsSet_desugarator rterm (List.tl attr_path) 1 [] model
else
get_attr_or_assoc rterm (List.last attr_path) model
(* 2-dimensional inheritance of Collection types *)
handle InterferenceError s =>
(
(
let
val _ = trace low ("\n==> 2-dim Inheritance check: attribute/assocend\n")
val rtyp = type_of_term rterm
val _ = trace low (string_of_OclType rtyp ^ "\n")
val templ_type = template_parameter rtyp
val pclass = get_classifier (Variable ("x",templ_type)) model
val ntempl_type = type_of_parent pclass
val new_type = replace_templ_para rtyp ntempl_type
val new_class = get_classifier (Variable ("x",new_type)) model
val attrs = get_overloaded_attrs_or_assocends new_class (List.last attr_path) model
val _ = trace low ("parent type of term:" ^ string_of_OclType new_type ^ "\n")
in
if (List.length attrs = 0)
then raise DesugaratorCall (rterm,attr_path,1,[],model)
else interfere_attrs_or_assocends attrs rterm model
end
)
handle DesugaratorCall arg => desugarator (#1 arg) (#2 arg) (#3 arg) (#4 arg) (#5 arg)
| NoCollectionTypeError t => AsSet_desugarator rterm attr_path 1 [] model
)
end
end
(* built in Operations not include in Library: oclIsKindOf, oclIsTypOf, oclAsType *)
(* OperationWithType Calls *)
(* OCLISTYPEOF *)
| resolve_OclTerm (OperationCall (term,_,["oclIsTypeOf"],[(AttributeCall (Variable ("self",vtyp),_,[real_typ], _),argt)],_)) model =
let
(* prefix type of iterator variable *)
val _ = trace medium ("\n\nRESOLVE OperationCallWithType: oclIsTypeOf\n")
val rterm = resolve_OclTerm term model
val _ = trace low ("res OpCall: oclIsTypeOf 2: " ^ "\n")
(* prefix types *)
val rtyp = type_of_term rterm
val _ = trace low ("res OpCall: oclIsTypeOf 3: " ^ "\n")
(* need to prefix the package *)
(* because parameter is written relativly *)
val class = get_classifier rterm model
val prfx = package_of class
val _ = trace low ("type of classifier: " ^ string_of_path prfx ^ "\n")
val ctyp = prefix_type prfx (string_to_type [real_typ])
val _ = trace low ("res OpCall: oclTypeOf 4:" ^ "... " ^ "\n")
in
OperationWithType (rterm,rtyp,"oclIsTypeOf",ctyp,Boolean)
end
(* OCLISKINDOF *)
| resolve_OclTerm (OperationCall (term,_,["oclIsKindOf"],[(AttributeCall (Variable ("self",_),_,[real_typ], _),argt)],_)) model =
let
val _ = trace medium ("RESOLVE OperationCallWithType: oclIsKindOf\n")
val rterm = resolve_OclTerm term model
val _ = trace low ("res OpCall: oclIsKindOf 2:" ^ "... " ^ "\n")
val rtyp = type_of_term rterm
val _ = trace low ("res OpCall: oclIsKindOf 3:" ^ "... " ^ "\n")
(* need to prefix the package *)
(* because parameter is written relativly *)
val class = get_classifier rterm model
val prfx = package_of class
val _ = trace low ("type of classifier: " ^ string_of_path prfx ^ "\n")
val ctyp = prefix_type prfx (string_to_type [real_typ])
val _ = trace low ("res OpCall: oclIsKindOf 4:" ^ "... " ^ "\n")
in
OperationWithType (rterm,rtyp,"oclIsKindOf",ctyp,Boolean)
end
(* OCLASTYPE *)
| resolve_OclTerm (OperationCall (term,_,["oclAsType"],[(AttributeCall (Variable ("self",_),_,[real_typ], _),argt)],_)) model =
let
val _ = trace medium ("RESOLVE OperationCallWithType: oclIsKindOf\n")
val rterm = resolve_OclTerm term model
val _ = trace low ("res OpCall: oclAsType 2:" ^ "... " ^ "\n")
val rtyp = type_of_term rterm
val _ = trace low ("res OpCall: oclAsType 3:" ^ "... " ^ "\n")
(* need to prefix the package *)
(* because parameter is written relativly *)
val class = get_classifier rterm model
val prfx = package_of class
val _ = trace low ("type of classifier: " ^ string_of_path prfx ^ "\n")
val ctyp = prefix_type prfx (string_to_type [real_typ])
val _ = trace low ("res OpCall: oclAsType 4:" ^ "... " ^ "\n")
in
OperationWithType (rterm,rtyp,"oclAsType",ctyp,ctyp)
end
(* HARD CODED STUFF *)
| resolve_OclTerm (OperationCall (term,typ,[OclLibPackage,"OclAny","atPre"],[],_)) model =
let
val _ = trace medium ("RESOLVE OperationCall: atPre \n")
(* resolve source term *)
val rterm = resolve_OclTerm term model
val rtyp = type_of_term rterm
val _ = trace low ("res OpCall: Type of source : " ^ string_of_OclType rtyp ^ "\n")
in
OperationCall (rterm,rtyp,[OclLibPackage,"OclAny","atPre"],[],rtyp)
end
| resolve_OclTerm (OperationCall (term,typ,meth_path,args,res_typ)) model =
let
val _ = trace medium ("RESOLVE OperatioCall: name = " ^ (List.last (meth_path)) ^ "\n")
(* resolve source term *)
val rterm = resolve_OclTerm term model
val _ = trace low ("res OpCall: Type of source : " ^ string_of_OclType (type_of_term rterm) ^ "\n")
(* resolve arguments *)
val rargs = resolve_arguments args model
val _ = trace low ("res OpCall: args resolved ...\n")
in
let
in
if (List.hd meth_path = "arrow")
then get_meth rterm (List.last meth_path) rargs model
handle InterferenceError s => AsSet_desugarator rterm (List.tl meth_path) 0 rargs model
else
get_meth rterm (List.last meth_path) rargs model
(* 2-dimensional inheritance of Collection types *)
handle InterferenceError s =>
(
(
let
val _ = trace low ("\n==> 2-dim Inheritance check: attribute/assocend\n")
val rtyp = type_of_term rterm
val _ = trace low (string_of_OclType rtyp ^ "\n")
val templ_type = template_parameter rtyp
val pclass = get_classifier (Variable ("x",templ_type)) model
val ntempl_type = type_of_parent pclass
val _ = trace low (string_of_OclType ntempl_type ^ "\n")
val new_type = replace_templ_para rtyp ntempl_type
val new_class = get_classifier (Variable ("x",new_type)) model
val ops = get_overloaded_methods new_class (List.last meth_path) model
val _ = trace low ("parent type of term: " ^ string_of_OclType new_type ^ "\n")
in
if (List.length ops = 0)
then raise DesugaratorCall (rterm, meth_path, 0, rargs, model)
else interfere_methods ops rterm rargs model
end
)
handle DesugaratorCall arg => desugarator (#1 arg) (#2 arg) (#3 arg) (#4 arg) (#5 arg)
| NoCollectionTypeError typ => AsSet_desugarator rterm meth_path 0 rargs model
)
end
end
(* Iterator *)
| resolve_OclTerm (Iterator (name,iter_vars,source_term,_,expr,expr_typ,res_typ)) model =
let
(* resolve source term, type *)
val _ = trace low ("RESOLVE Itertor: name = " ^ name ^ "\n")
val rterm = resolve_OclTerm source_term model
val rtyp = type_of_term rterm
val _ = trace low ("res Iter (" ^ name ^ "): source type " ^ string_of_OclType (type_of_term rterm) ^ "\n\n")
(* get source classifier *)
val source_class = get_classifier rterm model
val _ = trace low ("res Iter (" ^ name ^ "): type of classifier: " ^ string_of_OclType (type_of source_class) ^ "\n")
(* prefix types *)
val prfx = (package_of_template_parameter (type_of source_class))
val _ = trace low ("res Iter (" ^ name ^ "): Type prefixed ... \n")
val piter_vars = List.map (fn (a,b) => (a,prefix_type prfx b)) iter_vars
val piter_types = List.map (fn (a,b) => b) piter_vars
val _ = trace low ("res Iter (" ^ name ^ "): first iter types: " ^ string_of_OclType (List.hd piter_types) ^ "\n")
(* check if iterator types correspond to source type *)
val static_iter_type = template_parameter (type_of (source_class))
val _ = trace low ("Length of iter_types: " ^ Int.toString (List.length piter_types) ^ "\n")
val _ = trace low ("parent of classifier: " ^ string_of_OclType (type_of_parent source_class) ^ "\n")
val _ = trace low ("\nstatic iter type : " ^ string_of_OclType static_iter_type ^ " \n")
val _ = trace low ("iter types: " ^ string_of_OclType (List.hd piter_types) ^ "\n")
val h2 = List.map (fn a => conforms_to a static_iter_type model) (piter_types)
val check = List.all (fn a => a=true) h2
in
if (check) then
let
val _ = trace low ("res Iter: types conforms \n")
val bound_expr = embed_bound_variables piter_vars expr
val _ = trace low ("res Iter: term : " ^ Ocl2String.ocl2string false bound_expr ^ "\n")
val rexpr = resolve_OclTerm bound_expr model
val _ = trace low (" manuel " ^ string_of_OclType (type_of_term rexpr) ^ "\n")
val _ = trace low (" ma " ^ string_of_OclType (Set(static_iter_type)) ^ "\n")
val _ = trace low ("res Iter: Iterator name = " ^ name ^ " \n\n\n")
in
(
case name of
"select" =>
Iterator (name,piter_vars,rterm,rtyp,rexpr,type_of_term rexpr,rtyp)
| "reject" =>
Iterator (name,piter_vars,rterm,rtyp,rexpr,type_of_term rexpr,rtyp)
| "forAll" =>
Iterator (name,piter_vars,rterm,rtyp,rexpr,type_of_term rexpr,Boolean)
| "one" =>
Iterator (name,piter_vars,rterm,rtyp,rexpr,type_of_term rexpr,Boolean)
| "any" =>
Iterator (name,piter_vars,rterm,rtyp,rexpr,type_of_term rexpr,Boolean)
| "exists" =>
Iterator (name,piter_vars,rterm,rtyp,rexpr,type_of_term rexpr,Boolean)
| "collect" =>
Iterator (name,piter_vars,rterm,rtyp,rexpr,type_of_term rexpr,flatten_type (replace_templ_para (rtyp) (type_of_term rexpr)))
| _ => raise NoSuchIteratorNameError (Iterator (name,iter_vars,source_term,DummyT,expr,expr_typ,res_typ),("No such Iterator ..."))
)
end
else
raise IteratorTypeMissMatch (Iterator (name,iter_vars,source_term,DummyT,expr,expr_typ,res_typ),("Iterator variable doesn't conform to choosen set \n"))
end
| resolve_OclTerm (CollectionLiteral ([],typ)) model =
let
val _ = trace medium ("RESOLVE CollectionLiteral\n")
in
CollectionLiteral ([],typ)
end
| resolve_OclTerm (CollectionLiteral (coll_parts,temp_typ)) model =
let
val _ = trace medium ("RESOLVE CollectionLiteral\n")
val r_coll_parts = List.map (resolve_CollectionPart model) coll_parts
val typ = type_of_CollPart (List.hd r_coll_parts)
in
if (List.all (correct_type_for_CollLiteral typ) r_coll_parts) then
(CollectionLiteral (r_coll_parts,replace_templ_para temp_typ typ))
else
raise (wrongCollectionLiteral ((CollectionLiteral (coll_parts,temp_typ)), ("not all Literals have type of Collection")))
end
| resolve_OclTerm (Let (str,typ,rhs_term,_,in_term,_)) model =
let
val _ = trace medium ("RESOLVE a Let-Expression \n")
val rrhs_term = resolve_OclTerm rhs_term model
val rrhs_typ = type_of_term rrhs_term
val rin_term = resolve_OclTerm in_term model
val rin_typ = type_of_term rin_term
in
(Let (str,typ,rrhs_term,rrhs_typ,rin_term,rin_typ))
end
| resolve_OclTerm (If (cond_term,cond_typ,if_expr,if_typ,else_expr,else_typ,ret_typ)) model =
let
val _ = trace medium ("RESOLVE a If-Expression \n")
val rterm = resolve_OclTerm cond_term model
val rtyp = type_of_term rterm
val rif_expr = resolve_OclTerm if_expr model
val rif_typ = type_of_term rif_expr
val relse_expr = resolve_OclTerm else_expr model
val relse_typ = type_of_term relse_expr
in
if (rtyp = Boolean) then
if (conforms_to rif_typ relse_typ model) then
If(rterm,rtyp,rif_expr,rif_typ,relse_expr,relse_typ,relse_typ)
else if (conforms_to relse_typ rif_typ model) then
If(rterm,rtyp,rif_expr,rif_typ,relse_expr,relse_typ,rif_typ)
else
raise TypeCheckerResolveIfError (If (cond_term,cond_typ,if_expr,if_typ,else_expr,else_typ,ret_typ),("Types of if-expression and else-expression don't conform each other \n"))
else
raise TypeCheckerResolveIfError (If (cond_term,cond_typ,if_expr,if_typ,else_expr,else_typ,ret_typ),("Type of condition is not Boolean. \n"))
end
(* RETURN: context option *)
fun check_context (Cond (path,op_name,op_sign,result_type,cond,pre_name,expr)) model =
let
val _ = trace high ("Starts typechecking: ")
val _ = trace high ("pre/post/body : " ^ Ocl2String.ocl2string false expr ^ "\n")
val classifier = class_of_type (Classifier (path)) model
val oper_list = operations_of classifier
val oper = find_operation op_name oper_list
val check1 = (op_sign = (#arguments oper))
val check2 = (result_type = (#result oper))
val _ = trace low ("check1 = " ^ Bool.toString check1 ^ ", check2 = " ^ Bool.toString check2 ^ "\n")
val _ = List.map (fn (a,b) => (trace low (a ^ ":" ^ (string_of_OclType b) ^ " "))) op_sign
in
if check1 andalso check2
then
(SOME((Cond (path,op_name,op_sign,(#result oper),cond,pre_name,resolve_OclTerm expr model))))
else
NONE
end
| check_context (Attr (path,typ,attrorassoc,expr)) model =
let
val _ = trace high ("Starts typechecking: ")
val _ = trace high ("init/derive : " ^ Ocl2String.ocl2string false expr ^ "\n")
val classifier = class_of_type (Classifier (real_path path)) model
val _ = trace low ( "classifier found ... " ^ "\n")
val attr_list = attributes_of classifier
val _ = trace low ( "attr_list found ... " ^ "\n")
val attr = find_attribute (List.last path) attr_list
val _ = trace low ( "attribute found ... " ^ "\n")
in
if (typ = #attr_type attr)
then
let
val _ = trace low (" ... " ^ "\n")
in
(SOME ((Attr (path,(#attr_type attr),attrorassoc,resolve_OclTerm expr model))))
end
else
NONE
end
| check_context (Inv (path,name,expr)) model =
let
val _ = trace high ("Starts typechecking: ")
val _ = trace high ("inv : " ^ Ocl2String.ocl2string false expr ^ "\n")
in
(SOME (Inv (path,name, resolve_OclTerm expr model)))
end
| check_context (Empty_context (s,t)) _ = raise NotYetSupportedError ("Empty_context not supported.\n")
(* SOME (Empty_context (s,t)) *)
| check_context (Guard (path,name,expr)) _ = raise NotYetSupportedError ("Guard not supported.\n")
(* SOME (Guard (path,name,expr)) *)
(* RETURN: (context option) list *)
fun check_context_list [] model = []
| check_context_list (h::context_list_tail) model =
((check_context h model
handle wrongCollectionLiteral (term,mes) =>
let
val _ = trace high ("\n\n#################################################\n")
val _ = trace high ("wrongCollectionLiteral:\n")
val _ = trace high ("Error Message: " ^ mes ^ "\n")
val _ = trace high ("In Term: " ^ Ocl2String.ocl2string false term ^ "\n")
in
raise WrongContextChecked h
end
| CollectionRangeError (part,mes) =>
let
val _ = trace high ("\n\n#################################################\n")
val _ = trace high ("CollectionRangeError:\n")
val _ = trace high ("Error Message: " ^ mes ^ "\n")
in
raise WrongContextChecked h
end
| IteratorTypeMissMatch (term,mes) =>
let
val _ = trace high ("\n\n#################################################\n")
val _ = trace high ("IteratorTypeMissMatch:\n")
val _ = trace high ("Error Message: " ^ mes ^ "\n")
val _ = trace high ("In Term: " ^ Ocl2String.ocl2string false term ^ "\n")
in
raise WrongContextChecked h
end
| NoSuchIteratorNameError (term,mes) =>
let
val _ = trace high ("\n\n#################################################\n")
val _ = trace high ("NoSuchIteratorNameError:\n")
val _ = trace high ("Error Message: " ^ mes ^ "\n")
val _ = trace high ("In Term: " ^ Ocl2String.ocl2string false term ^ "\n")
in
raise WrongContextChecked h
end
| TypeCheckerResolveIfError (term,mes) =>
let
val _ = trace high ("\n\n#################################################\n")
val _ = trace high ("TypeCheckerResolveIfError:\n")
val _ = trace high ("Error Message: " ^ mes ^ "\n")
val _ = trace high ("In Term: " ^ Ocl2String.ocl2string false term ^ "\n")
in
raise WrongContextChecked h
end
| NotYetSupportedError mes =>
let
val _ = trace high mes
in
raise WrongContextChecked h
end
)::(check_context_list context_list_tail model))
handle WrongContextChecked h =>
let
val _ = trace high ("\n\n#################################################\n")
val _ = trace high ("WrongContextChecked:\n")
val _ = trace high ("In Context: " ^ (cxt_list2string [h]) ^ "\n")
in
[]
end
end

31
src/ocl_parser/values.sml Normal file
View File

@ -0,0 +1,31 @@
open Rep_OclTerm;
open Rep_Core;
open OclLibrary;
open Context;
open OclLibrary;
val xmi = RepParser.readFile "../examples/company/company.xmi";
val untyped_model = (oclLib@xmi);
val ocl = OclParser.parse_contextlist "../examples/company/company.manuel.ocl";
val pp = Preprocessor.preprocess_context_list ocl xmi;
val c = Literal ("a",Classifier (["Company","Company"]));
val p = Literal ("b",Classifier (["Company","Person"]));
val j = Literal ("c",Classifier (["Company","Job"]));
val b = Literal ("d",Classifier (["Company","Bank"]));
val s = Literal ("s",String);
val i = Literal ("i",Integer);
val r = Literal ("r",Real);
val set = Literal ("set",Set(Integer));
val collection = Literal("collection",Collection(String));
val bag = Literal ("bag",Bag(Real));
val model = (oclLib@xmi);
val cc = get_classifier c model;
val cp = get_classifier p model;
val cj = get_classifier j model;
val cb = get_classifier b model;