summaryrefslogtreecommitdiff
path: root/src/nexp_functions
diff options
context:
space:
mode:
authorAlasdair Armstrong2018-04-04 15:14:39 +0100
committerAlasdair Armstrong2018-04-05 18:40:36 +0100
commit09fca718c6e850a3a94db399fd1744dc537bbe41 (patch)
tree0d679d573f87236ee02e1ffe623d2e031a940ccb /src/nexp_functions
parent3604e9e94b766147b482c4c653c4d09bb4ee7a7c (diff)
Cleanup repository by removing old and generated files
Rename l2.ott to sail.ott
Diffstat (limited to 'src/nexp_functions')
-rw-r--r--src/nexp_functions67
1 files changed, 0 insertions, 67 deletions
diff --git a/src/nexp_functions b/src/nexp_functions
deleted file mode 100644
index e6ab14ba..00000000
--- a/src/nexp_functions
+++ /dev/null
@@ -1,67 +0,0 @@
-val compare_nexps : nexp -> nexp -> int
-(*usefull for sorting nexps*)
-
-val contains_const : nexp -> bool
-(*Does the given nexp recursively conain a constant*)
-
-val get_var : nexp -> nexp option
-(*extracts variable in a normalized nexp*)
-
-val get_all_nvar : nexp -> string list
-(*Gets a list (with duplicates) of all variables used in an nexp*)
-
-val get_factor : nexp -> nexp
-(*extracts a variables factor in a normalized nexp*)
-
-val increment_factor : nexp -> nexp -> nexp
-(*first nexp is multiplied by second, increased by one, expects normalized nexps*)
-
-val negate : nexp -> nexp
-(*negate normalized nexp into normalized form*)
-
-val normalize_nexp : nexp -> nexp
-(*convert nexp into a normal form*)
-
-val nexp_eq_check : nexp -> nexp -> bool
-(*structural equality*)
-
-val nexp_gt : nexp -> nexp -> triple
-(*greater than check, normalizes first, might not know*)
-
-val nexp_ge : nexp -> nexp -> triple
-(*greather than eq check, normalizes first, might not know*)
-
-
-val nexp_eq : nexp -> nexp -> bool
-(*wrapper on above that normalizes first*)
-
-val nexp_one_more_then : nexp -> nexp -> bool
-(*nexp_one_more_then n1 n2 checks if n1 is n2 + -1, n2 - 1*)
-
-val contains_nuvar_nexp : nexp -> nexp -> bool
-(*contains_nuvar n1 n2: n1 expected to be a nuvar (otherwise always false) otherwise says if n1 occurs in n2*)
-
-val contains_nuvar : nexp -> constraints -> constraints
-(*produces a list of all constraints that contain nexp, assumed to be a nuvar*)
-
-val n_subst : s_env -> nexp -> nexp
-(*replaces nvars*)
-
-val contains_var : nexp -> nexp -> bool
-(*expects nexp1 to be nvar or nuvar otherwise like contains_nuvar_nexp*)
-
-val subst_nuvar : nexp -> nexp ->nexp
-(*replace occurence of n1 (an nuvar) with n2 in n3*)
-
-val subst_nuvars : (nexp * nexp) list -> nexp -> nexp
-(*replace all occurences of the first nuvars in the list with the second nexp in the list in nexp*)
-
-val get_nuvars : nexp -> nexp list
-(*pull out all nuvars in an nexp*)
-
-val get_all_nuvars_cs : constraints -> Set.Make(NexpM).t
-(*pull out all the nuvars in a constraint set*)
-
-val equate_nuvars : 'a -> constraints -> contraints
-(*Set equal nuvars to each other in the constraint list... first parameter presently unused and has forgotten intent*)
-