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

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

This commit is contained in:
Manuel Krucker 2008-05-19 10:59:51 +00:00
parent 3d38ea1f0e
commit de5c581fdf
1 changed files with 10 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
su4sml/src/wfcpog/refine_constraint.sml
View File

@ -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)