From de5c581fdfc57c50226e4d7cceb47268193a3cc4 Mon Sep 17 00:00:00 2001 From: Manuel Krucker Date: Mon, 19 May 2008 10:59:51 +0000 Subject: [PATCH] git-svn-id: https://projects.brucker.ch/su4sml/svn/su4sml/trunk@7990 3260e6d1-4efc-4170-b0a7-36055960796d --- su4sml/src/wfcpog/refine_constraint.sml | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/su4sml/src/wfcpog/refine_constraint.sml b/su4sml/src/wfcpog/refine_constraint.sml index 32cc196..8ca2ed3 100644 --- a/su4sml/src/wfcpog/refine_constraint.sml +++ b/su4sml/src/wfcpog/refine_constraint.sml @@ -350,20 +350,24 @@ fun get_holocl_operation var_name oper class model = (** use Rep_Encoder to get operation as HOL-OCL-Term **) (* val term = Rep_Encoder. .... *) val hol_name = (name_of class)@[(name_of_op oper)] - val args = List.map (fn (a,b) => (Variable(a,b),b)) (arguments_of_op oper) val typ = type_of class - val predicate = Predicate(Variable(var_name,typ),typ,hol_name,args) + val predicate = Predicate(Variable(var_name,typ),typ,hol_name,args2varargs (arguments_of_op oper)) val _ = trace function_ends ("WFCPOG_Refine_Constraint.get_holocl_operation\n") in predicate end -fun get_holocl_abstraction_relation abs_path conc_path class_name = +fun get_holocl_abstraction_relation abs_path conc_path class_name model = let val _ = trace function_calls ("WFCPOG_Refine_Constraint.get_holocl_abstraction_relation\n") val predicate_name = "R_"^(string_of_path abs_path)^"_"^(string_of_path conc_path)^"_"^class_name - val dummy_term = Variable("R",DummyT) - val predicate = Predicate(dummy_term,DummyT,[predicate_name],[]) + val abs_state = Variable(varcounter.nextStr(),OclState) + val conc_state = Variable(varcounter.nextStr(),OclState) + val abs_type = type_of (class_of abs_path model) + val conc_type = type_of (class_of conc_path model) + val abs_term = Variable(varcounter.nextStr(),abs_type) + val conc_term = Variable(varcounter.nextStr(),conc_type) + val predicate = Predicate(abs_state,OclState,[predicate_name],[(conc_state,OclState),(abs_term,abs_type),(conc_term,conc_type)]) val _ = trace function_ends ("WFCPOG_Refine_Constraint.get_holocl_abstraction_relation\n") in predicate @@ -373,7 +377,7 @@ fun get_holocl_abstraction_relation abs_path conc_path class_name = fun refine_operation abs_oper conc_oper abs_class conc_class model = let val _ = trace function_calls ("WFCPOG_Refine_Constraint.refine_classifier\n") - val R = get_holocl_abstraction_relation (package_of abs_class) (package_of conc_class) (List.last(name_of abs_class)) + val R = get_holocl_abstraction_relation (package_of abs_class) (package_of conc_class) (List.last(name_of abs_class)) model val S = get_holocl_operation (name_of_op abs_oper) abs_oper abs_class model val T = get_holocl_operation (name_of_op conc_oper) conc_oper conc_class model val refine = OperationCall(S,DummyT,["holOclLib","methodology","refinement","OclForwardRefinement"],[(T,DummyT),(R,DummyT)],Boolean)