diff --git a/src/ocl_parser/ROOT.ML b/src/ocl_parser/ROOT.ML new file mode 100644 index 0000000..f938dfe --- /dev/null +++ b/src/ocl_parser/ROOT.ML @@ -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 + * Burkhart Wolff + * + * 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"; diff --git a/src/ocl_parser/STATUS b/src/ocl_parser/STATUS new file mode 100644 index 0000000..634357b --- /dev/null +++ b/src/ocl_parser/STATUS @@ -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 + diff --git a/src/ocl_parser/context_declarations.sml b/src/ocl_parser/context_declarations.sml new file mode 100644 index 0000000..2abfb54 --- /dev/null +++ b/src/ocl_parser/context_declarations.sml @@ -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 + * + * 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; diff --git a/src/ocl_parser/examples/encoding_example/encoding_example.xmi b/src/ocl_parser/examples/encoding_example/encoding_example.xmi new file mode 100644 index 0000000..bcff551 --- /dev/null +++ b/src/ocl_parser/examples/encoding_example/encoding_example.xmi @@ -0,0 +1,104 @@ + + + + + ArgoUML (using Netbeans XMI Writer version 1.0) + 0.20.x + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/ocl_parser/examples/encoding_example/encoding_example3.ocl b/src/ocl_parser/examples/encoding_example/encoding_example3.ocl new file mode 100644 index 0000000..032dc9e --- /dev/null +++ b/src/ocl_parser/examples/encoding_example/encoding_example3.ocl @@ -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 diff --git a/src/ocl_parser/examples/simple/classifier_list.sml b/src/ocl_parser/examples/simple/classifier_list.sml new file mode 100644 index 0000000..7e0a07b --- /dev/null +++ b/src/ocl_parser/examples/simple/classifier_list.sml @@ -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 diff --git a/src/ocl_parser/examples/simple/simple.argo b/src/ocl_parser/examples/simple/simple.argo new file mode 100644 index 0000000..7a5dc56 --- /dev/null +++ b/src/ocl_parser/examples/simple/simple.argo @@ -0,0 +1,35 @@ + + + + + + 0.19.7 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/ocl_parser/examples/simple/simple.ocl b/src/ocl_parser/examples/simple/simple.ocl new file mode 100644 index 0000000..93f8970 --- /dev/null +++ b/src/ocl_parser/examples/simple/simple.ocl @@ -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 + + diff --git a/src/ocl_parser/examples/simple/simple.todo b/src/ocl_parser/examples/simple/simple.todo new file mode 100644 index 0000000..274c81a --- /dev/null +++ b/src/ocl_parser/examples/simple/simple.todo @@ -0,0 +1,8 @@ + + + + + + + + diff --git a/src/ocl_parser/examples/simple/simple.xmi b/src/ocl_parser/examples/simple/simple.xmi new file mode 100644 index 0000000..cd32e01 --- /dev/null +++ b/src/ocl_parser/examples/simple/simple.xmi @@ -0,0 +1,264 @@ + + + + + Netbeans XMI Writer + 1.0 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/ocl_parser/examples/simple/simple1.ocl b/src/ocl_parser/examples/simple/simple1.ocl new file mode 100644 index 0000000..b96d78f --- /dev/null +++ b/src/ocl_parser/examples/simple/simple1.ocl @@ -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 \ No newline at end of file diff --git a/src/ocl_parser/examples/simple/simple_ClassDiagram.pgml b/src/ocl_parser/examples/simple/simple_ClassDiagram.pgml new file mode 100644 index 0000000..600da85 --- /dev/null +++ b/src/ocl_parser/examples/simple/simple_ClassDiagram.pgml @@ -0,0 +1,674 @@ + + + + + + + + + + E + + + + + + + + + + + + r : Integer + + + + + + + + + + D + + + + + + + + + + + + r : Real + + + + + + + + + + C + + + + + + + + + + + + s : String + + + + + + + + + + B + + + + + + + + + + + + j : Integer + attribA : A + + + + + + + + + + A + + + + + + m(p : Integer) : Integer + + + + + + + i : Integer + r : Real + attribB : B + + + + + + sourcePortFig="Fig4" + destPortFig="Fig3" + sourceFigNode="Fig4" + destFigNode="Fig3" + + + + + + + + + sourcePortFig="Fig2" + destPortFig="Fig4" + sourceFigNode="Fig2" + destFigNode="Fig4" + + + + + + + + + + + sourcePortFig="Fig1" + destPortFig="Fig4" + sourceFigNode="Fig1" + destFigNode="Fig4" + + + + + + + + + + + sourcePortFig="Fig0" + destPortFig="Fig3" + sourceFigNode="Fig0" + destFigNode="Fig3" + + + + + + + diff --git a/src/ocl_parser/fix_types.sml b/src/ocl_parser/fix_types.sml new file mode 100644 index 0000000..96060a6 --- /dev/null +++ b/src/ocl_parser/fix_types.sml @@ -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" [] + +*) diff --git a/src/ocl_parser/isar/isar_setup.sml b/src/ocl_parser/isar/isar_setup.sml new file mode 100644 index 0000000..62e55e1 --- /dev/null +++ b/src/ocl_parser/isar/isar_setup.sml @@ -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 + * + * 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 + diff --git a/src/ocl_parser/isar/test.thy b/src/ocl_parser/isar/test.thy new file mode 100644 index 0000000..428ca95 --- /dev/null +++ b/src/ocl_parser/isar/test.thy @@ -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 diff --git a/src/ocl_parser/library.sml b/src/ocl_parser/library.sml new file mode 100644 index 0000000..d1a212c --- /dev/null +++ b/src/ocl_parser/library.sml @@ -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 + * + * 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 diff --git a/src/ocl_parser/make_classifier_list.sml b/src/ocl_parser/make_classifier_list.sml new file mode 100644 index 0000000..92d11c2 --- /dev/null +++ b/src/ocl_parser/make_classifier_list.sml @@ -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 + * + * 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 diff --git a/src/ocl_parser/ml-yacc-lib/base.sig b/src/ocl_parser/ml-yacc-lib/base.sig new file mode 100644 index 0000000..5528865 --- /dev/null +++ b/src/ocl_parser/ml-yacc-lib/base.sig @@ -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 + diff --git a/src/ocl_parser/ml-yacc-lib/join.sml b/src/ocl_parser/ml-yacc-lib/join.sml new file mode 100644 index 0000000..5cf9df1 --- /dev/null +++ b/src/ocl_parser/ml-yacc-lib/join.sml @@ -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; diff --git a/src/ocl_parser/ml-yacc-lib/lrtable.sml b/src/ocl_parser/ml-yacc-lib/lrtable.sml new file mode 100644 index 0000000..67cc1f4 --- /dev/null +++ b/src/ocl_parser/ml-yacc-lib/lrtable.sml @@ -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; diff --git a/src/ocl_parser/ml-yacc-lib/parser2.sml b/src/ocl_parser/ml-yacc-lib/parser2.sml new file mode 100644 index 0000000..618340e --- /dev/null +++ b/src/ocl_parser/ml-yacc-lib/parser2.sml @@ -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; + diff --git a/src/ocl_parser/ml-yacc-lib/root.sml b/src/ocl_parser/ml-yacc-lib/root.sml new file mode 100644 index 0000000..84ee7a3 --- /dev/null +++ b/src/ocl_parser/ml-yacc-lib/root.sml @@ -0,0 +1,5 @@ +use "base.sig"; +use "join.sml"; +use "lrtable.sml"; +use "stream.sml"; +use "parser2.sml"; diff --git a/src/ocl_parser/ml-yacc-lib/stream.sml b/src/ocl_parser/ml-yacc-lib/stream.sml new file mode 100644 index 0000000..ea90960 --- /dev/null +++ b/src/ocl_parser/ml-yacc-lib/stream.sml @@ -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; diff --git a/src/ocl_parser/model_import.sml b/src/ocl_parser/model_import.sml new file mode 100644 index 0000000..7fdab9d --- /dev/null +++ b/src/ocl_parser/model_import.sml @@ -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 + * + * 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 diff --git a/src/ocl_parser/ocl.grm b/src/ocl_parser/ocl.grm new file mode 100644 index 0000000..3db57bc --- /dev/null +++ b/src/ocl_parser/ocl.grm @@ -0,0 +1,690 @@ +(************************************************************************** + * SML OCL 2.0 Parser - A Parser writen in SML for OCL 2.0 + * + * Copyright (C) 2007 Manuel P. Krucker + * + **************************************************************************) + +(* + +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) diff --git a/src/ocl_parser/ocl.lex b/src/ocl_parser/ocl.lex new file mode 100644 index 0000000..65383ad --- /dev/null +++ b/src/ocl_parser/ocl.lex @@ -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()); diff --git a/src/ocl_parser/parser.110.62.cm b/src/ocl_parser/parser.110.62.cm new file mode 100644 index 0000000..cf0c709 --- /dev/null +++ b/src/ocl_parser/parser.110.62.cm @@ -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 diff --git a/src/ocl_parser/parser.cm b/src/ocl_parser/parser.cm new file mode 100644 index 0000000..14dbacd --- /dev/null +++ b/src/ocl_parser/parser.cm @@ -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 diff --git a/src/ocl_parser/parser.sml b/src/ocl_parser/parser.sml new file mode 100644 index 0000000..8c853d1 --- /dev/null +++ b/src/ocl_parser/parser.sml @@ -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 diff --git a/src/ocl_parser/preprocessor.sml b/src/ocl_parser/preprocessor.sml new file mode 100644 index 0000000..0d4ac93 --- /dev/null +++ b/src/ocl_parser/preprocessor.sml @@ -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 + * + * 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 diff --git a/src/ocl_parser/script.sml b/src/ocl_parser/script.sml new file mode 100644 index 0000000..5f24de3 --- /dev/null +++ b/src/ocl_parser/script.sml @@ -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" []; + diff --git a/src/ocl_parser/test-suite.sml b/src/ocl_parser/test-suite.sml new file mode 100644 index 0000000..638f386 --- /dev/null +++ b/src/ocl_parser/test-suite.sml @@ -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 + diff --git a/src/ocl_parser/todo.txt b/src/ocl_parser/todo.txt new file mode 100644 index 0000000..0ec64db --- /dev/null +++ b/src/ocl_parser/todo.txt @@ -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) diff --git a/src/ocl_parser/type_checker.sml b/src/ocl_parser/type_checker.sml new file mode 100644 index 0000000..7268ba2 --- /dev/null +++ b/src/ocl_parser/type_checker.sml @@ -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 + * + * 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 + diff --git a/src/ocl_parser/values.sml b/src/ocl_parser/values.sml new file mode 100644 index 0000000..8d5f686 --- /dev/null +++ b/src/ocl_parser/values.sml @@ -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; +