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

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

This commit is contained in:
Manuel Krucker 2008-04-08 07:42:16 +00:00
parent db445d4f3b
commit 738efcbfc5
3 changed files with 68 additions and 54 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -380,11 +380,11 @@ and generate_variables (Literal (paras)) path meth_name model = Literal (paras)
(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 =
| generate_variables (AttributeCall (src,src_type,["result"],_)) path meth_name model =
let
val _ = trace function_calls ("Preprocessor.generate_variables: AttributeCall\n")
val new_src = generate_variables src path meth_name model
val _ = List.app (print o (fn x => x^"\n") o string_of_path o name_of ) model
(* val classifier = obsolete_obsolete_class_of path model *)
val classifier = class_of path (model,[])
val _ = trace low "classifier found\n"
val meth = get_operation meth_name classifier (model,[])
@ -395,14 +395,26 @@ and generate_variables (Literal (paras)) path meth_name model = Literal (paras)
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 =
| generate_variables (OperationCall (sterm,styp,pa,paras,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))
val _ = trace function_calls ("Preprocessor.generate_variables \n")
val new_para_terms = List.map (fn (a,b) => generate_variables (a) path meth_name model) paras
val new_paras = List.map (fn a => (a, type_of_term a)) new_para_terms
val res =
(OperationCall (generate_variables sterm path meth_name model,styp,pa,new_paras,res_typ))
val _ = trace function_ends ("Preprocessor.generate_variables\n")
in
res
end
| generate_variables (OperationWithType (sterm,stype,para_name,para_type,res_typ)) path meth_name model =
let
val _ = trace function_calls ("Preprocessor.generate_variables \n")
val res =
(OperationWithType (generate_variables sterm path meth_name model,stype,para_name,para_type,res_typ))
val _ = trace function_ends ("Preprocessor.generate_variables\n")
in
res
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 =

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

@ -700,51 +700,53 @@ let
(* RETURN: context option *)
fun check_context (Cond (path,op_name,op_sign,result_type,cond,pre_name,expr)) (model as (cls,assocs)) =
let
val _ = trace high ("Starts typechecking: ")
val _ = trace type_checker ("pre/post/body : " ^ Ocl2String.ocl2string false expr ^ "\n")
val classifier = class_of_type (Classifier (path)) model
val oper = get_operation op_name classifier model
val check1 = (op_sign = (#arguments oper))
val check2 = (result_type = (#result oper))
val _ = trace type_checker ("check1 = " ^ Bool.toString check1 ^ ", check2 = " ^ Bool.toString check2 ^ "\n")
val _ = List.map (fn (a,b) => (trace type_checker (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 as (cls,assocs)) =
let
val _ = trace function_calls ("TypeChecker.check_context STARTS TYPECHECKING ...\n")
val _ = trace type_checker ("init/derive : " ^ Ocl2String.ocl2string false expr ^ "\n")
val classifier = class_of_type (Classifier (real_path path)) model
val _ = trace type_checker ( "classifier found ... " ^ "\n")
val attr_list = attributes_of classifier
val _ = trace type_checker ( "attr_list found ... " ^ "\n")
val attr = valOf (get_attribute (List.last path) attr_list)
val _ = trace type_checker ( "attribute found ... " ^ "\n")
val res =
if (typ = #attr_type attr)
then
let
val _ = trace type_checker (" ... " ^ "\n")
in
(SOME ((Attr (path,(#attr_type attr),attrorassoc,resolve_OclTerm expr model))))
end
else
NONE
val _ = trace function_ends ("TypeChecker.check_context\n\n\n")
in
res
end
| check_context (Inv (path,name,expr)) model =
let
val _ = trace function_calls ("TypeChecker.check_context STARTS TYPECHECKING ...\n")
val _ = trace type_checker ("inv : " ^ Ocl2String.ocl2string false expr ^ "\n")
let
val _ = trace function_calls ("TypeChecker.check_context Cond(...)\n")
val _ = trace type_checker ("pre/post/body : " ^ Ocl2String.ocl2string false expr ^ "\n")
val classifier = class_of_type (Classifier (path)) model
val oper = get_operation op_name classifier model
val check1 = (op_sign = (#arguments oper))
val check2 = (result_type = (#result oper))
val _ = trace type_checker ("check1 = " ^ Bool.toString check1 ^ ", check2 = " ^ Bool.toString check2 ^ "\n")
val _ = List.map (fn (a,b) => (trace type_checker (a ^ ":" ^ (string_of_OclType b) ^ " "))) op_sign
val res =
if check1 andalso check2
then
(SOME((Cond (path,op_name,op_sign,(#result oper),cond,pre_name,resolve_OclTerm expr model))))
else
NONE
val _ = trace function_ends ("TypeChecker.check_context Cond(...)\n\n\n")
in
res
end
| check_context (Attr (path,typ,attrorassoc,expr)) (model as (cls,assocs)) =
let
val _ = trace function_calls ("TypeChecker.check_context Attr(..._)\n")
val _ = trace type_checker ("init/derive : " ^ Ocl2String.ocl2string false expr ^ "\n")
val classifier = class_of_type (Classifier (real_path path)) model
val _ = trace type_checker ( "classifier found ... " ^ "\n")
val attr_list = attributes_of classifier
val _ = trace type_checker ( "attr_list found ... " ^ "\n")
val attr = valOf (get_attribute (List.last path) attr_list)
val _ = trace type_checker ( "attribute found ... " ^ "\n")
val res =
if (typ = #attr_type attr)
then
let
val _ = trace type_checker (" ... " ^ "\n")
in
(SOME ((Attr (path,(#attr_type attr),attrorassoc,resolve_OclTerm expr model))))
end
else
NONE
val _ = trace function_ends ("TypeChecker.check_context\n\n\n")
in
res
end
| check_context (Inv (path,name,expr)) model =
let
val _ = trace function_calls ("TypeChecker.check_context Inv(...)\n")
val _ = trace type_checker ("inv : " ^ Ocl2String.ocl2string false expr ^ "\n")
val res = (SOME (Inv (path,name, resolve_OclTerm expr model)))
val _ = trace function_ends ("TypeChecker.check_context\n\n\n")
in

2
su4sml/src/rep_core.sml
View File

@ -3219,7 +3219,7 @@ fun upcast_op [] source args model =
end
| upcast_op ((class,meth)::class_meth_list) source args model =
let
val _ = trace low ("\nInterfere method : name : '" ^ name_of_op meth ^ "'\n")
val _ = trace low ("Interfere method : name : '" ^ name_of_op meth ^ "'\n")
val check_source = conforms_to (type_of_term source) (type_of class) model
val check_args = upcastable_args (#arguments meth) args model
val _ = trace low ("Upcastable ? : Source conforms : " ^ Bool.toString check_source ^ " Args conforms : " ^ Bool.toString check_args ^ "\n")