Added support for includes and functions in cat (#736)

Co-authored-by: Hernan Ponce de Leon <[email protected]>

cat/basic.cat

@@ -0,0 +1,12 @@
+let fr = rf^-1;co | ([R] \ [range(rf)]);loc;[W]
+
+let po-loc = po & loc
+
+let rfe = rf & ext
+let coe = co & ext
+let fre = fr & ext
+let rfi = rf & int
+let coi = co & int
+let fri = fr & int
+
+let fencerel(F) = po;[F];po

cat/c11-orig.cat

@@ -9,6 +9,7 @@ Rewritten by Luc Maranget for herd7
 
 *)
 
+include "basic.cat"
 include "c11_cos.cat"
 include "c11_los.cat"
 

cat/c11.cat

@@ -14,6 +14,7 @@ Rewritten by Luc Maranget for herd7
    may be missing. As a consequence, reads may have no rf-edge if they read from initial memory.
 *)
 
+include "basic.cat"
 include "c11_cos.cat"
 include "c11_los.cat"
 

cat/cos.cat

@@ -0,0 +1,5 @@
+// Herd7 uses cos.cat for generating coherence.
+// It usually also defines some derived relations used in many memory models.
+// Dartagnan does not need the former; the later is handled by basic.cat below.
+
+include "basic.cat"

cat/imm.cat

@@ -8,6 +8,8 @@
  * following GenMC's implementation
  *)
 
+include "basic.cat"
+
 (* coherence *)
 let rs = [W];po-loc;[W] | [W];(po-loc?;rf;rmw)*                                                                                     (* release sequence *)
 (* GenMC uses the same sw definition as RC11 *)

cat/linux-kernel.cat

@@ -101,8 +101,9 @@ let to-r = (addr ; [R]) | (dep ; [Marked] ; rfi)
 let ppo = to-r | to-w | (fence & int) | (po-unlock-lock-po & int)
 
 (* Propagation: Ordering from release operations and strong fences. *)
+let A-cumul(r) = (rfe ; [Marked])? ; r
 let rmw-sequence = (rf ; rmw)*
-let cumul-fence = [Marked] ; ((rfe ; [Marked])? ; (strong-fence | po-rel) | wmb |
+let cumul-fence = [Marked] ; (A-cumul(strong-fence | po-rel) | wmb |
 	po-unlock-lock-po) ; [Marked] ; rmw-sequence
 let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ;
 	[Marked] ; rfe? ; [Marked]