[spectec] Restrict reduction of equality to values

Author: rossberg

spectec/doc/semantics/il/5-reduction.spectec

@@ -155,21 +155,21 @@ rule Step_exp/CMP-ctx2:
   -- Step_exp: S |- e_2 ~> e_2'
 
 rule Step_exp/CMP-EQ-true:
-  S |- CMP EQ e_1 e_2 ~> BOOL true
-  -- if e_1 = e_2
+  S |- CMP EQ val_1 val_2 ~> BOOL true
+  -- if val_1 = val_2
 
 rule Step_exp/CMP-EQ-false:
   S |- CMP EQ val_1 val_2 ~> BOOL false
   -- if val_1 =/= val_2
 
-rule Step_exp/CMP-NE-false:
-  S |- CMP NE e_1 e_2 ~> BOOL false
-  -- if e_1 = e_2
-
 rule Step_exp/CMP-NE-true:
   S |- CMP NE val_1 val_2 ~> BOOL true
   -- if val_1 =/= val_2
 
+rule Step_exp/CMP-NE-false:
+  S |- CMP NE val_1 val_2 ~> BOOL false
+  -- if val_1 = val_2
+
 rule Step_exp/CMP-NUM:
   S |- CMP numcmpop num_1 num_2 ~> BOOL $numcmp(numcmpop, num_1, num_2)
 
@@ -557,6 +557,8 @@ rule Step_argmatch/EXP-fail:
   S |- `{q*} (EXP e / EXP e')  ~>_s  `{} FAIL
   -- Step_expmatch: S |- `{q*} (e / e')  ~>_s  `{} FAIL
 
+;; TODO: EXP disjointness?
+
 
 rule Step_argmatch_plain/ctx1:
   S |- a / a'  ~>  a'' / a'
@@ -566,14 +568,6 @@ rule Step_argmatch_plain/ctx2:
   S |- a / a'  ~>  a / a''
   -- Step_arg: S |- a' ~> a''
 
-rule Step_argmatch_plain/eq:
-  S |- a / a  ~>  eps
-
-;; TODO: disjointness
-;;rule Step_argmatch_plain/neq:
-;;  S |- a / a' ~> FAIL
-;;  -- Disj_arg: S |- a =/= a'
-
 
 rule Step_expmatch/plain:
   S |- `{q*} (e / e')*  ~>_{}  `{q*} (e'' / e''')*
@@ -616,7 +610,7 @@ rule Step_expmatch_plain/ctx2:
   -- Step_exp: S |- e' ~> e''
 
 rule Step_expmatch_plain/eq:
-  S |- e / e  ~>  eps
+  S |- val / val  ~>  eps
 
 rule Step_expmatch_plain/UN-PLUS:
   S |- num / UN PLUS e ~> num / e
@@ -721,7 +715,7 @@ rule Step_expmatch_plain/SUB-SUB:
     SUB e t_1 t'_1 / e'
   -- Sub_typ: $storeenv(S) |- t_1 <: t'_1
 
-;; TODO: disjointness
+;; TODO: disjointness?
 
 rule Step_expmatch_plain/SUB-TUP:
   S |- TUP e^n / SUB e' (TUP (x_1 `: t'_1)^n) (TUP (x_2 `: t'_2)^n) ~>

spectec/src/il/eval.ml

@@ -179,10 +179,8 @@ and reduce_exp env e : exp =
     let e1' = reduce_exp env e1 in
     let e2' = reduce_exp env e2 in
     (match op, e1'.it, e2'.it with
-    | `EqOp, _, _ when Eq.eq_exp e1' e2' -> BoolE true
-    | `NeOp, _, _ when Eq.eq_exp e1' e2' -> BoolE false
-    | `EqOp, _, _ when is_normal_exp e1' && is_normal_exp e2' -> BoolE false
-    | `NeOp, _, _ when is_normal_exp e1' && is_normal_exp e2' -> BoolE true
+    | `EqOp, _, _ when is_normal_exp e1' && is_normal_exp e2' -> BoolE (Eq.eq_exp e1' e2')
+    | `NeOp, _, _ when is_normal_exp e1' && is_normal_exp e2' -> BoolE (not (Eq.eq_exp e1' e2'))
     | #Num.cmpop as op', NumE n1, NumE n2 ->
       (match Num.cmp op' n1 n2 with
       | Some b -> BoolE b
@@ -686,7 +684,8 @@ and match_exp' env s e1 e2 : subst option =
     (fun r -> fmt "%s" (opt il_subst r))
   ) @@ fun _ ->
   assert (Eq.eq_exp e1 (reduce_exp env e1));
-  if Eq.eq_exp e1 e2 then Some s else  (* HACK around subtype elim pass introducing calls on LHS's *)
+  (* HACK around subtype elim pass introducing calls on LHS's *)
+  if Eq.eq_exp e1 e2 && is_normal_exp e1 && is_normal_exp e2 then Some s else
   match e1.it, (reduce_exp env (Subst.subst_exp s e2)).it with
   | _, VarE id when Subst.mem_varid s id ->
     (* A pattern variable already in the substitution is non-linear *)