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

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

This commit is contained in:
Manuel Krucker 2008-04-30 10:14:26 +00:00
parent 876fc95e44
commit eb57a59228
1 changed files with 27 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
su4sml/src/wfcpog/holocl_namespace.sml
View File

@ -231,4 +231,31 @@ end
fun name_of_pre C Op = hc_path l2 (pre_1_of ((Rep_Core.name_of C)@[Rep_Core.mangled_name_of_op Op]))
fun name_of_post C Op = hc_path l2 (post_1_of ((Rep_Core.name_of C)@[Rep_Core.mangled_name_of_op Op]))
end
structure HolOcl_Helper =
struct
open Rep_OclType
open Rep_OclTerm
exception HolOcl_Helper_InvalidArguments of string
fun ocl_opcall source f args t = OperationCalil (source, type_of source, f,
map (fn x => (x,type_of x)) args,
t)
fun holocl_and a b = ocl_opcall a ["holOclLib","Boolean","and"] [b] Boolean
fun holocl_and_all [] = raise (HolOcl_Helper_InvalidArguments ("holocl.holocl_and_all: empty argument list")
| holocl_and_all [a] = a
| holocl_and_all (h::t) = holocl_and a (holocl_and_all t)
fun holocl_or a b = ocl_opcall a ["holOclLib","Boolean","or"] [b] Boolean
| holocl_or_all [] = raise (HolOcl_Helper_InvalidArguments ("holocl.holocl_or_all: empty argument list")
| holocl_or_all [a] = a
| holocl_or_all (h::t) = holocl_or a (holocl_or_all t)
fun holocl_implies a b = ocl_opcall a ["holOclLib","Boolean","implies"] [b] Boolean
fun holocl_xor a b = ocl_opcall a ["holOclLib","Boolean","xor"] [b] Boolean
fun holocl_not a = ocl_opcall a ["holOclLib","Boolean","not"] [] Boolean
end