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

git-svn-id: https://projects.brucker.ch/su4sml/svn/su4sml/trunk@7462 3260e6d1-4efc-4170-b0a7-36055960796d

This commit is contained in:
Manuel Krucker 2008-03-20 20:05:41 +00:00
parent 6844ccb3f0
commit 2c243044cc
3 changed files with 130 additions and 290 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
su4sml/src/library.sml
View File

@ -175,4 +175,8 @@ fun join s nil = ""
fun uncurry f (x,y) = f x y fun uncurry f (x,y) = f x y
fun curry f x y = f (x,y) fun curry f x y = f (x,y)
fun remove_dup [] = []
| remove_dup (h::tail) = if (member h tail) then (remove_dup tail) else ((h)::(remove_dup tail))
end end

11
su4sml/src/ocl_parser/type_checker.sml
View File

@ -185,7 +185,7 @@ fun FromSet_desugarator rterm path attr_or_meth rargs (model as (cls,assocs):Rep
(* RETURN: OclTerm (OperationCall/AttributeCall) *) (* RETURN: OclTerm (OperationCall/AttributeCall) *)
fun AsSet_desugarator rterm path attr_or_meth rargs (model as (cls,assocs)) = fun AsSet_desugarator rterm path attr_or_meth rargs (model as (cls,assocs)) =
(trace function_calls "AsSet_desugarator\n"; (trace function_calls ("AsSet_desugarator class= " ^ (string_of_OclType (type_of_term rterm)) ^ " , attr\n");
if (attr_or_meth = 0) if (attr_or_meth = 0)
then (* OperationCall *) then (* OperationCall *)
let let
@ -357,7 +357,8 @@ let
val class = class_of_term rterm model val class = class_of_term rterm model
val prfx = package_of class val prfx = package_of class
val _ = trace low ("type of classifier: " ^ string_of_path prfx ^ "\n") val _ = trace low ("type of classifier: " ^ string_of_path prfx ^ "\n")
val ctyp = prefix_type prfx (type_of_path [real_typ] model) (* 20.03.08 val ctyp = prefix_type prfx (type_of_path [real_typ] model) *)
val ctyp = type_of_path (prfx@[real_typ]) model
val _ = trace low ("res OpCall: oclTypeOf 4:" ^ "... " ^ "\n") val _ = trace low ("res OpCall: oclTypeOf 4:" ^ "... " ^ "\n")
in in
OperationWithType (rterm,rtyp,"oclIsTypeOf",ctyp,Boolean) OperationWithType (rterm,rtyp,"oclIsTypeOf",ctyp,Boolean)
@ -375,7 +376,8 @@ let
val class = class_of_term rterm model val class = class_of_term rterm model
val prfx = package_of class val prfx = package_of class
val _ = trace low ("type of classifier: " ^ string_of_path prfx ^ "\n") val _ = trace low ("type of classifier: " ^ string_of_path prfx ^ "\n")
val ctyp = prefix_type prfx (type_of_path [real_typ] model) (* 20.03.08 val ctyp = prefix_type prfx (type_of_path [real_typ] model) *)
val ctyp = type_of_path (prfx@[real_typ]) model
val _ = trace low ("res OpCall: oclIsKindOf 4:" ^ "... " ^ "\n") val _ = trace low ("res OpCall: oclIsKindOf 4:" ^ "... " ^ "\n")
in in
OperationWithType (rterm,rtyp,"oclIsKindOf",ctyp,Boolean) OperationWithType (rterm,rtyp,"oclIsKindOf",ctyp,Boolean)
@ -393,7 +395,8 @@ let
val class = class_of_term rterm model val class = class_of_term rterm model
val prfx = package_of class val prfx = package_of class
val _ = trace low ("type of classifier: " ^ string_of_path prfx ^ "\n") val _ = trace low ("type of classifier: " ^ string_of_path prfx ^ "\n")
val ctyp = prefix_type prfx (type_of_path [real_typ] model) (* 20.03.08 val ctyp = prefix_type (prfx (type_of_path [real_typ] model) *)
val ctyp = type_of_path (prfx@[real_typ]) model
val _ = trace low ("res OpCall: oclAsType 4:" ^ "... " ^ "\n") val _ = trace low ("res OpCall: oclAsType 4:" ^ "... " ^ "\n")
in in
OperationWithType (rterm,rtyp,"oclAsType",ctyp,ctyp) OperationWithType (rterm,rtyp,"oclAsType",ctyp,ctyp)

405
su4sml/src/rep_core.sml
View File

@ -779,6 +779,7 @@ exception NoParentForDatatype of string
exception NoModelReferenced of string exception NoModelReferenced of string
exception NoCollectionTypeError of Rep_OclType.OclType exception NoCollectionTypeError of Rep_OclType.OclType
exception AttributeAssocEndNameClash of string exception AttributeAssocEndNameClash of string
exception ParentsOfError of string
end end
structure Rep_Core : REP_CORE = structure Rep_Core : REP_CORE =
@ -906,6 +907,7 @@ exception NoCollectionTypeError of Rep_OclType.OclType
exception OperationNotFoundError of string exception OperationNotFoundError of string
exception AttributeNotFoundError of string exception AttributeNotFoundError of string
exception AttributeAssocEndNameClash of string exception AttributeAssocEndNameClash of string
exception ParentsOfError of string
val OclLibPackage = "oclLib" val OclLibPackage = "oclLib"
val OclAnyC = Class{name=Rep_OclType.OclAny,parent=NONE,attributes=[], val OclAnyC = Class{name=Rep_OclType.OclAny,parent=NONE,attributes=[],
operations=[], interfaces=[], operations=[], interfaces=[],
@ -1097,34 +1099,41 @@ and class_of_term source (c:Classifier list, a:association list) =
in in
(s,substitute_typ typ t)::(substitute_args typ tail) (s,substitute_typ typ t)::(substitute_args typ tail)
end end
and substitute_parent x = SOME(DummyT) (* (Set (t)) model = and substitute_parent (Set (t)) model =
(case t of (case t of
OclAny => SOME(Set(OclAny)) OclAny => SOME(OclAny)
| x => | x =>
let let
val par = class_of_type x model val _ = trace wgen ("substitute parent SET\n")
val par_type = type_of par val _ = trace wgen ("para type of substitute parent = " ^ (string_of_OclType x) ^ "\n")
in val par = class_of_type x model
SOME(Set(par_type)) val par_type = type_of par
end val _ = trace wgen ("par_type = " ^ (string_of_OclType par_type) ^ "\n")
in
SOME(Set(par_type))
end
) )
| substitute_parent (OrderedSet (t)) model = | substitute_parent (OrderedSet (t)) model =
(case t of (case t of
OclAny => SOME(OrderedSet(OclAny)) OclAny => SOME(OclAny)
| x => | x =>
let let
val par = class_of_type x model val _ = trace wgen ("substitute parent ORDEREDSET\n")
val par_type = type_of par val _ = trace wgen ("para type of substitute parent = " ^ (string_of_OclType x) ^ "\n")
in val par = class_of_type x model
SOME(OrderedSet(par_type)) val par_type = type_of par
in
SOME(OrderedSet(par_type))
end end
) )
| substitute_parent (Sequence (t)) model = | substitute_parent (Sequence (t)) model =
(case t of (case t of
OclAny => SOME(Sequence(OclAny)) OclAny => SOME(OclAny)
| x => | x =>
let let
val _ = trace wgen ("substitute parent SEQUENCE\n")
val _ = trace wgen ("para type of substitute parent = " ^ (string_of_OclType x) ^ "\n")
val par = class_of_type x model val par = class_of_type x model
val par_type = type_of par val par_type = type_of par
in in
@ -1133,9 +1142,11 @@ and class_of_term source (c:Classifier list, a:association list) =
) )
| substitute_parent (Bag (t)) model = | substitute_parent (Bag (t)) model =
(case t of (case t of
OclAny => SOME(Bag(OclAny)) OclAny => SOME(OclAny)
| x => | x =>
let let
val _ = trace wgen ("substitute parent BAG\n")
val _ = trace wgen ("para type of substitute parent = " ^ (string_of_OclType x) ^ "\n")
val par = class_of_type x model val par = class_of_type x model
val par_type = type_of par val par_type = type_of par
in in
@ -1144,17 +1155,24 @@ and class_of_term source (c:Classifier list, a:association list) =
) )
| substitute_parent (Collection (t)) model = | substitute_parent (Collection (t)) model =
(case t of (case t of
OclAny => SOME(Collection(OclAny)) OclAny => SOME(OclAny)
| x => | x =>
let let
val _ = trace wgen ("substitute parent COLLECTION\n")
val _ = trace wgen ("para type of substitute parent = " ^ (string_of_OclType x) ^ "\n")
val par = class_of_type x model val par = class_of_type x model
val par_type = type_of par val par_type = type_of par
in in
SOME(Collection(par_type)) SOME(Collection(par_type))
end end
) )
| substitute_parent t model = raise TemplateInstantiationError ("substitute parent must have set type.\n") | substitute_parent t model =
*) let
val _ = trace wgen ("substitute parent COLLECTION\n")
val _ = trace wgen ("para type of substitute parent = " ^ (string_of_OclType t) ^ "\n")
in
raise TemplateInstantiationError ("substitute parent must have set type.\n")
end
and substitute_operations typ [] = [] and substitute_operations typ [] = []
| substitute_operations typ ((oper:operation)::tail) = | substitute_operations typ ((oper:operation)::tail) =
let let
@ -1211,7 +1229,7 @@ and class_of_term source (c:Classifier list, a:association list) =
val styp = substitute_typ typ (type_of classifier) val styp = substitute_typ typ (type_of classifier)
val ops = substitute_operations typ (local_operations_of classifier) val ops = substitute_operations typ (local_operations_of classifier)
val _ = trace 100 ("substitute parent.\n") val _ = trace 100 ("substitute parent.\n")
val sparent = substitute_parent typ val sparent = substitute_parent styp (c,a)
val _ = trace 100 ("end substitute parent.\n") val _ = trace 100 ("end substitute parent.\n")
in in
(Class (Class
@ -1548,264 +1566,88 @@ fun isColl_Type (Set(x)) = true
| isColl_Type (Collection(x)) = true | isColl_Type (Collection(x)) = true
| isColl_Type _ = false | isColl_Type _ = false
fun parent_of (cl as Class{parent,...}:Classifier) (model:transform_model) =
fun parent_of (cl as Class{parent,...}:Classifier) (model:transform_model) = (case parent of
(
case parent of
NONE => class_of_type OclAny model
| SOME(DummyT) =>
(* Classifier is a template *)
let
val cl_typ = type_of cl
in
case cl_typ of
Collection(OclAny) => class_of_type OclAny model
| Set(OclAny) => class_of_type OclAny model
| OrderedSet(OclAny) => class_of_type OclAny model
| Sequence(OclAny) => class_of_type OclAny model
| Bag(OclAny) => class_of_type OclAny model
| Collection(y) =>
let
val parameter_class = class_of_type y model
val parent_parameter_class = parent_of parameter_class model
val par_type = type_of parent_parameter_class
in
class_of_type (Collection(par_type)) model
end
| Set(y) =>
let
val parameter_class = class_of_type y model
val parent_parameter_class = parent_of parameter_class model
val par_type = type_of parent_parameter_class
in
class_of_type (Set(par_type)) model
end
| OrderedSet(y) =>
let
val parameter_class = class_of_type y model
val parent_parameter_class = parent_of parameter_class model
val par_type = type_of parent_parameter_class
in
class_of_type (OrderedSet(par_type)) model
end
| Sequence(y)=>
let
val parameter_class = class_of_type y model
val parent_parameter_class = parent_of parameter_class model
val par_type = type_of parent_parameter_class
in
class_of_type (Sequence(par_type)) model
end
| Bag(y)=>
let
val parameter_class = class_of_type y model
val parent_parameter_class = parent_of parameter_class model
val par_type = type_of parent_parameter_class
in
class_of_type (Bag(par_type)) model
end
end
| SOME(x) => class_of_type x model
)
| parent_of (asso as AssociationClass{parent,...}) (model:transform_model) =
(
case parent of
NONE => class_of_type OclAny model
| SOME(DummyT) =>
(* Classifier is a template *)
let
val cl_typ = type_of asso
in
case cl_typ of
Collection(OclAny) => class_of_type OclAny model
| Set(OclAny) => class_of_type OclAny model
| OrderedSet(OclAny) => class_of_type OclAny model
| Sequence(OclAny) => class_of_type OclAny model
| Bag(OclAny) => class_of_type OclAny model
| Collection(y) =>
let
val parameter_class = class_of_type y model
val parent_parameter_class = parent_of parameter_class model
val par_type = type_of parent_parameter_class
in
class_of_type (Collection(par_type)) model
end
| Set(y) =>
let
val parameter_class = class_of_type y model
val parent_parameter_class = parent_of parameter_class model
val par_type = type_of parent_parameter_class
in
class_of_type (Set(par_type)) model
end
| OrderedSet(y) =>
let
val parameter_class = class_of_type y model
val parent_parameter_class = parent_of parameter_class model
val par_type = type_of parent_parameter_class
in
class_of_type (OrderedSet(par_type)) model
end
| Sequence(y)=>
let
val parameter_class = class_of_type y model
val parent_parameter_class = parent_of parameter_class model
val par_type = type_of parent_parameter_class
in
class_of_type (Sequence(par_type)) model
end
| Bag(y)=>
let
val parameter_class = class_of_type y model
val parent_parameter_class = parent_of parameter_class model
val par_type = type_of parent_parameter_class
in
class_of_type (Bag(par_type)) model
end
end
| SOME(x) => class_of_type x model
)
| parent_of (Interface{parents,...}) (model:transform_model) =
(case (List.length (parents)) of
0 => class_of_type OclAny model
| x => class_of_type (List.hd (parents)) model
)
| parent_of (enum as Enumeration{parent,...}) (model:transform_model) =
(
case parent of
NONE => class_of_type OclAny model
| SOME(DummyT) =>
(* Classifier is a template *)
let
val cl_typ = type_of enum
in
case cl_typ of
Collection(OclAny) => class_of_type OclAny model
| Set(OclAny) => class_of_type OclAny model
| OrderedSet(OclAny) => class_of_type OclAny model
| Sequence(OclAny) => class_of_type OclAny model
| Bag(OclAny) => class_of_type OclAny model
| Collection(y) =>
let
val parameter_class = class_of_type y model
val parent_parameter_class = parent_of parameter_class model
val par_type = type_of parent_parameter_class
in
class_of_type (Collection(par_type)) model
end
| Set(y) =>
let
val parameter_class = class_of_type y model
val parent_parameter_class = parent_of parameter_class model
val par_type = type_of parent_parameter_class
in
class_of_type (Set(par_type)) model
end
| OrderedSet(y) =>
let
val parameter_class = class_of_type y model
val parent_parameter_class = parent_of parameter_class model
val par_type = type_of parent_parameter_class
in
class_of_type (OrderedSet(par_type)) model
end
| Sequence(y)=>
let
val parameter_class = class_of_type y model
val parent_parameter_class = parent_of parameter_class model
val par_type = type_of parent_parameter_class
in
class_of_type (Sequence(par_type)) model
end
| Bag(y)=>
let
val parameter_class = class_of_type y model
val parent_parameter_class = parent_of parameter_class model
val par_type = type_of parent_parameter_class
in
class_of_type (Bag(par_type)) model
end
end
| SOME(x) => class_of_type x model
)
| parent_of (Primitive{parent,...}) (model:transform_model) =
case (parent) of
NONE => class_of_type OclAny model NONE => class_of_type OclAny model
| SOME(x) => class_of_type x model | SOME(x) => class_of_type x model)
| parent_of (asso as AssociationClass{parent,...}:Classifier) (model:transform_model) =
(case parent of
NONE => class_of_type OclAny model
| SOME(x) => class_of_type x model)
| parent_of (enum as Enumeration{parent,...}:Classifier) (model:transform_model) =
(case parent of
NONE => class_of_type OclAny model
| SOME(x) => class_of_type x model)
| parent_of (primi as Primitive{parent,...}:Classifier) (model:transform_model) =
(case parent of
NONE => class_of_type OclAny model
| SOME(x) => class_of_type x model)
| parent_of (inf as Interface{parents,...}:Classifier) (model:transform_model) =
class_of_type (List.hd(parents)) model
fun parents_of_help C (model:transform_model) = fun parents_of_help (C:Classifier) (model:transform_model) =
let let
val _ = trace wgen ("parents_of_help " ^ (string_of_path (name_of C)) ^ "\n") val _ = trace wgen ("parents_of_help classifier = " ^ (string_of_path (name_of C)) ^ "\n")
val parent = parent_of C model val typ = type_of C
val _ = trace wgen ("parent_of classifer = " ^ (string_of_path (name_of parent)) ^ "\n")
in in
case (isColl_Type (type_of (parent))) of case (isColl_Type typ) of
true => false =>
( let
case (type_of (parent)) of val _ = trace 50 ("no collection type \n")
Collection(y) => [parent]@(parents_of_help parent model) val parent = parent_of C model
| Set(y) => in
let if (type_of parent = OclAny)
val parents_1_prior = [parent]@(parents_of_help parent model) then [parent]
val coll_typ = Collection(y) else [parent]@(parents_of_help parent model)
val coll_class = class_of_type coll_typ model end
val parents_2_prior = [coll_class]@(parents_of_help coll_class model) | true =>
in let
parents_1_prior@parents_2_prior val parent = parent_of C model
end in
| Bag(y) => case (type_of (parent)) of
let OclAny =>
val parents_1_prior = [parent]@(parents_of_help parent model) (* type of classifier is : Collection(OclAny), Set(Any),
val coll_typ = Collection(y) OrderedSet(OclAny), ...
val coll_class = class_of_type coll_typ model *)
val parents_2_prior = [coll_class]@(parents_of_help coll_class model) (
in case typ of
parents_1_prior@parents_2_prior Collection(OclAny) => [class_of_type (OclAny) model]
end | Set(OclAny) => [class_of_type (Collection(OclAny)) model,
| OrderedSet(y) => class_of_type (OclAny) model]
let | Bag(OclAny) => [class_of_type (Collection(OclAny)) model,
val parents_1_prior = [parent]@(parents_of_help parent model) class_of_type (OclAny) model]
val coll_typ = Collection(y) | Sequence(OclAny) => [class_of_type (Collection(OclAny)) model,
val coll_class = class_of_type coll_typ model class_of_type (OclAny) model]
val parents_2_prior = [coll_class]@(parents_of_help coll_class model) | OrderedSet(OclAny) => [class_of_type (Set(OclAny)) model,
in class_of_type (Collection(OclAny)) model,
parents_1_prior@parents_2_prior class_of_type (OclAny) model]
end | x => raise ParentsOfError ("Parent must be Collection(OclAny), Set(OclAny), Bag(OclAny),... \n")
| Sequence(y) => )
let (* for collection only one inheritance direction needs to be done *)
val _ = trace wgen ("1-dim inheritance") | Collection(T) => [parent]@(parents_of_help parent model)
val parents_1_prior = [parent]@(parents_of_help parent model) | Set(T) =>
val _ = trace wgen ("number of parents = " ^ Int.toString (List.length (parents_1_prior)) ^ "\n") let
val coll_typ = Collection(y) val parents_1_prior = [parent]@(parents_of_help parent model)
val coll_class = class_of_type coll_typ model val coll_typ = Collection(T)
val _ = trace wgen ("2-dim inheritance") val coll_class = class_of_type coll_typ model
val parents_2_prior = [coll_class]@(parents_of_help coll_class model) val parents_2_prior = [coll_class]@(parents_of_help coll_class model)
val _ = trace wgen ("number of parents = " ^ Int.toString (List.length (parents_1_prior)) ^ "\n") in
in parents_1_prior@parents_2_prior
parents_1_prior@parents_2_prior end
end end
)
| false => case (type_of parent) of
OclAny => [class_of_type OclAny model]
| x => [parent]@(parents_of_help parent model)
(*
| x => (case isColl_Type x of
false => [parent]@parents_of_help parent model)
| true =>
let
val _ = trace wgen ("parent is colltype : ")
val _ = trace wgen ((string_of_OclType x) ^ "\n")
in
end
)
*)
end end
fun parents_of (C:Classifier) (model:transform_model) =
let
val _ = trace wgen ("parents_of, classifier = " ^ (string_of_path (name_of C)) ^ "\n")
val parents = parents_of_help C model
val _ = trace wgen ("parents_of end manu \n")
in
remove_dup parents
end
fun name_of_association ({name,aends,qualifiers,aclass}:association) = name fun name_of_association ({name,aends,qualifiers,aclass}:association) = name
fun path_of_association assoc = name_of_association assoc fun path_of_association assoc = name_of_association assoc
@ -1881,15 +1723,6 @@ fun local_associationends_of (all_associations:association list) (Class{name,ass
end end
| local_associationends_of _ _ = error ("in local_associationends_of: This classifier has no associationends") (*FIXME: or rather []? *) | local_associationends_of _ _ = error ("in local_associationends_of: This classifier has no associationends") (*FIXME: or rather []? *)
fun associationends_of assocs classes = local_associationends_of assocs classes fun associationends_of assocs classes = local_associationends_of assocs classes
fun parents_of C model =
let
val parents = parents_of_help C model
in
remove_dup parents
end
(* get all inherited operations of a classifier, without the local operations *) (* get all inherited operations of a classifier, without the local operations *)
fun inherited_operations_of class (model as (clist,alist)) = fun inherited_operations_of class (model as (clist,alist)) =