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

fixing endloss loop while type-checking 

git-svn-id: https://projects.brucker.ch/su4sml/svn/su4sml/trunk@8367 3260e6d1-4efc-4170-b0a7-36055960796d
This commit is contained in:
Achim D. Brucker 2008-12-30 09:00:24 +00:00
parent 3f18a611c8
commit 4318d446e0
7 changed files with 119 additions and 39 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
su4sml/src/ocl2string.sml
View File

@ -115,10 +115,13 @@ fun ocl2string show_types oclterm =
| Literal (lit, typ) => if show_types
then "("^lit^":"^(string_of_OclType typ)^")"
else lit
| CollectionLiteral (parts, typ as Bag x) => "Bag{"^(collection_part_list show_types parts)^"}"
| CollectionLiteral (parts, typ as Set x) => "Set{"^(collection_part_list show_types parts)^"}"
| CollectionLiteral (parts, typ as OrderedSet x) => "OrderedSet{"^(collection_part_list show_types parts)^"}"
| CollectionLiteral (parts, typ as Sequence x) => "Sequence{"^(collection_part_list show_types parts)^"}"
| CollectionLiteral (parts, typ as Collection x) => "Collection{"^(collection_part_list show_types parts)^"}"
| If (cterm,ctyp, tterm,ttyp,eterm,etyp,iftyp) => if show_types
then "(if ("^(ocl2string show_types cterm)^":"^(string_of_OclType ctyp)
@ -317,7 +320,8 @@ fun ocl2string show_types oclterm =
in
"Tuple{"^(String.substring(x,0,size-1))^"}\n"
end
| _ => error "error: unknown OCL-term in in ocl2string"
| _ => error "error: unknown OCL-term in in ocl2string"
end
end

5
su4sml/src/ocl_parser/context_declarations.sml
View File

@ -5,7 +5,8 @@
* context_declarations.sml ---
* This file is part of su4sml.
*
* Copyright (c) 2005-2007, ETH Zurich, Switzerland
* Copyright (c) 2005-2007 ETH Zurich, Switzerland
* (c) 2008 Achim D. Brucker, Germany
*
* All rights reserved.
*
@ -43,7 +44,7 @@ signature CONTEXT =
sig
(* datatypes *)
datatype ConditionType = pre | post | body
datatype ConditionType = pre | post | body (* | def *)
datatype AttrOrAssoc = derive | init | def
datatype context =
Empty_context of string *

3
su4sml/src/ocl_parser/model_import.sml
View File

@ -46,9 +46,6 @@ sig
val parseOCL : string -> Context.context list
val parseModel : string -> Rep_Core.Classifier list
val import : string -> string -> string list -> Rep_Core.transform_model
(* val removePackages : (Rep_Core.transform_model * Context.context list)
-> string list
-> (Rep_Core.transform_model * Context.context list) *)
val removePackages : string list -> Rep_Core.transform_model
-> Rep_Core.transform_model
val removeOclLibrary : Rep_Core.Classifier list -> Rep_Core.Classifier list

47
su4sml/src/ocl_parser/preprocessor.sml
View File

@ -6,6 +6,7 @@
* This file is part of su4sml.
*
* Copyright (c) 2005-2007, ETH Zurich, Switzerland
* 2008 Achim D. Brucker, Germany
*
* All rights reserved.
*
@ -368,16 +369,25 @@ fun embed_iterator_variables arg_list term = embed_method_arguments arg_list ter
It can be easily extended 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)
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)
| generate_variables_coll_list [] 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 ([],dummyT)) path meth_name model =
(CollectionLiteral ([],Set OclAny)) (* HACK/ DefaultType for Empty List: OclAny *)
| 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 (src,src_type,["result"],_)) path meth_name model =
@ -438,6 +448,24 @@ fun check_for_self_paras arg_list typ [] model = []
res
end
and check_for_self_collpart arg_list typ model (CollectionItem (term,ctyp)) =
let
val _ = trace function_calls ("Preprocessor.check_for_self_collpart CollectionItem(...)\n")
val res = (CollectionItem (check_for_self arg_list typ term model,ctyp))
val _ = trace function_ends ("Preprocessor.check_for_self_collpart\n")
in
res
end
| check_for_self_collpart arg_list typ model (CollectionRange (term1,term2,ctyp)) =
let
val _ = trace function_calls ("Preprocessor.check_for_self_collpart CollectionRange(...)\n")
val res = (CollectionRange (check_for_self arg_list typ term1 model,
check_for_self arg_list typ term2 model, ctyp))
val _ = trace function_ends ("Preprocessor.check_for_self_collpart\n")
in
res
end
(* RETURN: OclTerm *)
and check_for_self arg_list typ (AttributeCall (Variable("dummy_source",_),_,path,_)) model=
let
@ -454,6 +482,17 @@ and check_for_self arg_list typ (AttributeCall (Variable("dummy_source",_),_,pat
in
res
end
| check_for_self arg_list typ (CollectionLiteral (collpart,ctyp)) model =
let
val _ = trace function_calls ("Preprocessor.check_for_self: dummy_source CollectionLiteral\n")
val res = (CollectionLiteral (List.map (check_for_self_collpart arg_list typ model) collpart,ctyp))
val _ = trace function_ends ("Preprocessor.check_for_self\n")
in
res
end
| check_for_self arg_list typ (AttributeCall (source_term,source_typ,path,ret_typ)) model =
let
val _ = trace function_calls ("Preprocessor.check_for_self: complex AttributeCall\n")

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

@ -5,7 +5,8 @@
* type_checker.sml ---
* This file is part of su4sml.
*
* Copyright (c) 2005-2007, ETH Zurich, Switzerland
* Copyright (c) 2005-2007 ETH Zurich, Switzerland
* 2008 Achim D. Brucker, Germany
*
* All rights reserved.
*
@ -187,10 +188,11 @@ fun FromSet_desugarator rterm path attr_or_meth rargs (model as (cls,assocs):Rep
end
end
end
exception unkown
(* RETURN: OclTerm (OperationCall/AttributeCall) *)
fun AsSet_desugarator rterm path attr_or_meth rargs (model as (cls,assocs)) =
let
val _ = if isColl_Type (type_of_term rterm) then print "\n error in AsSet_Desugarotr\n" else ()
val _ = (trace function_calls ("TypeChecker.AsSet_desugarator class= " ^ (string_of_OclType (type_of_term rterm)) ^ " , attr\n"))
val res = if (attr_or_meth = 0)
then (* OperationCall *)
@ -204,8 +206,11 @@ fun AsSet_desugarator rterm path attr_or_meth rargs (model as (cls,assocs)) =
in
if (List.length ops = 0)
then
let val _ = print ("RAise: "^(Ocl2String.ocl2string false rterm))
in
raise TC_NoSuchOperationError ("interefere_methods: No operation signature matches given types (source: "^(Ocl2String.ocl2string false rterm)^").")
else
end
else
upcast_op ops new_rterm rargs model
end
else (* AttributeCall *)
@ -366,14 +371,12 @@ and resolve_OclTerm (Literal (s,typ)) model =
(
(
let
val _ = trace type_checker ("==> 2-dim Inheritance check: ma attribute/assocend\n")
val _ = trace type_checker ("==> 2-dim Inheritance check: attribute/assocend\n")
val rtyp = type_of_term rterm
val _ = trace type_checker (string_of_OclType rtyp ^ "manu \n")
val _ = trace type_checker (string_of_OclType rtyp ^"\n")
val templ_type = type_of_template_parameter rtyp
val pclass = class_of_term (Variable ("x",templ_type)) model
val _ = trace type_checker ("manu 2")
val ntempl_type = type_of_parent pclass
val _ = trace type_checker ("manu 3")
val new_type = substitute_templ_para rtyp ntempl_type
val new_class = class_of_term (Variable ("x",new_type)) model
val attrs = get_overloaded_attrs_or_assocends new_class (List.last attr_path) model
@ -385,7 +388,7 @@ and resolve_OclTerm (Literal (s,typ)) model =
end
)
handle TC_DesugaratorCall arg => desugarator (#1 arg) (#2 arg) (#3 arg) (#4 arg) (#5 arg)
| NoCollectionTypeError t => AsSet_desugarator rterm attr_path 1 [] model
| NoCollectionTypeError t => AsSet_desugarator rterm attr_path 1 [] model
| Empty => AsSet_desugarator rterm attr_path 1 [] model
)
end
@ -499,7 +502,7 @@ let
(
(
let
val _ = trace type_checker ("==> 2-dim Inheritance check: attribute/assocend\n")
val _ = trace type_checker ("==> no 2-dim Inheritance check: attribute/assocend\n")
val rtyp = type_of_term rterm
val _ = trace type_checker (string_of_OclType rtyp ^ "\n")
val templ_type = type_of_template_parameter rtyp
@ -826,14 +829,38 @@ fun check_context_list [] model = []
raise TC_OperationWithTypeError mes
end
)::(check_context_list context_list_tail model))
handle TC_WrongContextChecked h =>
handle(* TC_WrongContextChecked h => *)
(* let *)
(* val s1 = ("\n\n#################################################\n") *)
(* val s2 = ("WrongContextChecked:\n") *)
(* val s3 = ("In Context: " ^ (cxt_list2string [h]) ^ "\n") *)
(* val _ = trace exce (s1^s2^s3) *)
(* in *)
(* raise TC_RootError ("Something went wrong!\n") *)
(* end *)
(* | *) TC_NoSuchAttributeError s =>
let
val s1 = ("\n\n#################################################\n")
val s2 = ("WrongContextChecked:\n")
val s3 = ("In Context: " ^ (cxt_list2string [h]) ^ "\n")
val _ = trace exce (s1^s2^s3)
in
raise TC_RootError ("Something went wrong!\n")
val s1 = ("\n\n#################################################\n")
val s2 = ("Attribute not found: "^s^ "\n")
val _ = print s2
in (* ADB TODO *)
raise TC_RootError ("Something went wrong!\n")
end
end
| GetClassifierError s =>
let
val s1 = ("\n\n#################################################\n")
val s2 = ("Classifier not found: "^s^ "\n")
val _ = print s2
in (* ADB TODO *)
raise TC_RootError ("Something went wrong!\n")
end
| TC_NoSuchOperationError s =>
let
val s1 = ("\n\n#################################################\n")
val s2 = ("Operation not found: "^s^ "\n")
val _ = print s2
in (* ADB TODO *)
raise TC_RootError ("Something went wrong!\n")
end
end

34
su4sml/src/rep_core.sml
View File

@ -1691,6 +1691,7 @@ fun parent_of_template (cl as Class{parent,...}:Classifier) (model:transform_mod
raise TemplateError ("parent_of_template should never be used during Instantiation of a template.\n")
(* never ending *)
fun parents_of_help (C:Classifier) (model:transform_model) =
let
val this_type = type_of C
@ -1703,6 +1704,14 @@ fun parents_of_help (C:Classifier) (model:transform_model) =
| Bag(OclAny) => []
| Sequence(OclAny) => []
| OrderedSet(OclAny) => []
| Collection(Collection _) => []
| Set(Set _) => []
| Bag(Bag _) => []
| Sequence(Sequence _) => []
| OrderedSet(OrderedSet _) => []
| Collection(T) =>
let
val class_T = class_of_type (T) model
@ -1720,7 +1729,7 @@ fun parents_of_help (C:Classifier) (model:transform_model) =
val T' = type_of class_T'
val set_T' = class_of_type (Set(T')) model
in
[col_T]@(parents_of_help col_T model)@[set_T']@(parents_of_help set_T' model)
[col_T]@(parents_of_help col_T model)@[set_T']@(parents_of_help set_T' model)
end
| OrderedSet(T) =>
let
@ -1772,8 +1781,9 @@ fun parent_of (C:Classifier) model = parent_of_template C model
fun parents_of (C:Classifier) model =
let
val _ = trace rep_core ("parents_of ... \n")
val helper = (parents_of_help C model)
in
(if (parents_of_help C model = [])
(if (helper = [])
then
(
if (isColl_Type (type_of C))
@ -2109,14 +2119,13 @@ fun substitute_templ_para (Collection(tt)) t = Collection (t)
| substitute_templ_para (Bag (tt)) t = Bag (t)
| substitute_templ_para t1 t2 = raise TemplateError ("Not possible to replace template parameter of a basic type. Type is: " ^ string_of_OclType t1 ^ " \n")
fun type_of_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
fun type_of_template_parameter (Set t) = t
| type_of_template_parameter (Sequence t) = t
| type_of_template_parameter (Bag t) = t
| type_of_template_parameter (Collection t) = t
| type_of_template_parameter (OrderedSet t) = t
| type_of_template_parameter t = raise NoCollectionTypeError t
fun consistency_constraint cls_name (aend,revAend) =
let
@ -3505,7 +3514,10 @@ fun get_overloaded_methods class op_name ([],_) = raise NoModelReferenced ("in '
fun get_overloaded_attrs_or_assocends class attr_name (model as (clist,alist)) =
let
val _ = trace function_calls ("Rep_Core.get_overloaded_attrs_or_assocends, look for attr_or_assoc = " ^ attr_name ^ "\n")
val _ = trace function_calls
("Rep_Core.get_overloaded_attrs_or_assocends, look for attr_or_assoc = "
^ attr_name
^ "\n")
val parents = parents_of class model
(* Attributes *)
val loc_atts = List.map (fn a => (class,a)) (local_attributes_of class)

2
su4sml/src/su4sml.sml
View File

@ -76,7 +76,7 @@ fun print_usage() = let
val _ = print("typecheck: typecheck a UML/OCL specification\n")
val _ = print("usage: typeckeck UML [OCL]\n")
val _ = print("\n")
val _ = print("UML can be either a ArgoUML file (*.zargo), a compatible XMI file \n")
val _ = print("UML can be either a ArgoUML file (i.e, *.zargo), a compatible XMI file \n")
val _ = print("or the output of the Dresden OCL Toolkit, version 2.0. In the latter \n")
val _ = print("case, the OCL specification contained in the XMI from Dresden OCL \n")
val _ = print("is merged with the specification given in the OCL file.\n")