type eq first

1 files changed, 49 insertions, 1 deletions

diff --git a/src/type_internal.ml b/src/type_internal.ml
index bfed90ee..2bd0f659 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -1,3 +1,4 @@
+open Ast
 module Envmap = Finite_map.Fmap_map(String)
 module Nameset' = Set.Make(String)
 module Nameset = struct
@@ -39,7 +40,7 @@ and n_uvar = { nindex : int; mutable nsubst : t option }
 and effect = { mutable effect : effect_aux }
 and effect_aux =
   | Evar of string
-  | Eset of Ast.base_effect list
+  | Eset of base_effect list
   | Euvar of e_uvar
 and e_uvar = { eindex : int; mutable esubst : t option }
 and order = { mutable order : order_aux }
@@ -82,5 +83,52 @@ let initial_kind_env =
     ("vector", {k = K_Lam( [ {k = K_Nat}; {k = K_Nat}; {k= K_Ord} ; {k=K_Typ}], {k=K_Typ}) } )
   ]
 
+let eq_error l msg = raise (Reporting_basic.err_typ l msg)
+
+let compare_effect (BE_aux(e1,_)) (BE_aux(e2,_)) =
+  match e1,e2 with 
+  | (BE_rreg,BE_rreg) -> 0
+  | (BE_rreg,_) -> -1
+  | (_,BE_rreg) -> 1
+  | (BE_wreg,BE_wreg) -> 0
+  | (BE_wreg,_) -> -1
+  | (_,BE_wreg) -> 1
+  | (BE_rmem,BE_rmem) -> 0
+  | (BE_rmem,_) -> -1
+  | (_,BE_rmem) -> 1
+  | (BE_wmem,BE_wmem) -> 0
+  | (BE_wmem,_) -> -1
+  | (_,BE_wmem) -> 1
+  | (BE_undef,BE_undef) -> 0
+  | (BE_undef,_) -> -1
+  | (_,BE_undef) -> 1
+  | (BE_unspec,BE_unspec) -> 0
+  | (BE_unspec,_) -> -1
+  | (_,BE_unspec) -> 1
+  | (BE_nondet,BE_nondet) -> 0
+
+let effect_sort = List.sort compare_effect
+
+(* Check that o1 is or can be eqaul to o2. In the event that one is polymorphic, inc or dec can be used polymorphically but 'a cannot be used as inc or dec *)
+let order_eq l o1 o2 = 
+  match (o1.order,o2.order) with 
+  | (Oinc,Oinc) | (Odec,Odec) | (Oinc,Ovar _) | (Odec,Ovar _) -> o2
+  | (_,Ouvar i) -> o2.order <- o1.order; o2
+  | (Ouvar i,_) -> o1.order <- o2.order; o2
+  | (Ovar v1,Ovar v2) -> if v1=v2 then o2 else eq_error l ("Order variables " ^ v1 ^ " and " ^ v2 ^ " do not match and cannot be unified")
+  | (Oinc,Odec) | (Odec,Oinc) -> eq_error l "Order mismatch of inc and dec"
+  | (Ovar v1,Oinc) -> eq_error l ("Polymorphic order " ^ v1 ^ " cannot be used where inc is expected")
+  | (Ovar v1,Odec) -> eq_error l ("Polymorhpic order " ^ v1 ^ " cannot be used where dec is expected")
+
+(*Similarly to above.*)
+let effects_eq l e1 e2 =
+  match e1.effect,e2.effect with
+  | Eset _ , Evar _ -> e2
+  | Euvar i,_ -> e1.effect <- e2.effect; e2
+  | _,Euvar i -> e2.effect <- e1.effect; e2
+  | Eset es1,Eset es2 -> if ( effect_sort es1 = effect_sort es2 ) then e2 else eq_error l ("Effects must be the same") (*Print out both effect lists?*)
+  | Evar v1, Evar v2 -> if v1 = v2 then e2 else eq_error l ("Effect variables " ^ v1 ^ " and " ^ v2 ^ " do not match and cannot be unified")
+  | Evar v1, Eset _ -> eq_error l ("Effect variable " ^ v1 ^ " cannot be used where a concrete set of effects is specified")
+
 let rec type_eq l t1 t2 = (t2,[])
 let rec type_coerce l t1 t2 = (t2,[])