Skip to content

Commit

Permalink
Fix equality
Browse files Browse the repository at this point in the history
  • Loading branch information
@rossberg
rossberg committed Jul 7, 2024
1 parent c909185 commit 0c288f7
Show file tree
Hide file tree
Showing 2 changed files with 49 additions and 34 deletions.
39 changes: 22 additions & 17 deletions spectec/src/frontend/eval.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -116,11 +116,19 @@ and reduce_typ_app env id args at = function

(* Expression Reduction *)

and is_head_normal_exp e =
match e.it with
| AtomE _ | BoolE _ | NatE _ | TextE _ | UnE (MinusOp, {it = NatE _; _})
| SeqE _ | TupE _ | InfixE _ | BrackE _ | StrE _ -> true
| _ -> false

and is_normal_exp e =
match e.it with
| AtomE _ | BoolE _ | NatE _ | TextE _ | SeqE _
| UnE (MinusOp, {it = NatE _; _})
| StrE _ | TupE _ | InfixE _ | BrackE _ -> true
| AtomE _ | BoolE _ | NatE _ | TextE _ | UnE (MinusOp, {it = NatE _; _}) -> true
| SeqE es | TupE es -> List.for_all is_normal_exp es
| BrackE (_, e, _) -> is_normal_exp e
| InfixE (e1, _, e2) -> is_normal_exp e1 && is_normal_exp e2
| StrE efs -> Convert.forall_nl_list (fun (_, e) -> is_normal_exp e) efs
| _ -> false

and reduce_exp env e : exp =
Expand Down Expand Up @@ -187,8 +195,10 @@ 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 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'))
| EqOp, _, _ when Eq.eq_exp e1' e2' -> BoolE true
| EqOp, _, _ when is_normal_exp e1' && is_normal_exp e2' -> BoolE false
| NeOp, _, _ when Eq.eq_exp e1' e2' -> BoolE false
| NeOp, _, _ when is_normal_exp e1' && is_normal_exp e2' -> BoolE true
| LtOp, NatE (_, n1), NatE (_, n2) -> BoolE (n1 < n2)
| LtOp, UnE (MinusOp, {it = NatE (_, n1); _}), UnE (MinusOp, {it = NatE (_, n2); _}) -> BoolE (n2 < n1)
| LtOp, UnE (MinusOp, {it = NatE _; _}), NatE _ -> BoolE true
Expand Down Expand Up @@ -286,16 +296,11 @@ and reduce_exp env e : exp =
let e1' = reduce_exp env e1 in
let e2' = reduce_exp env e2 in
(match e2'.it with
| SeqE [] -> BoolE false $ e.at
| SeqE (e21'::es2') ->
reduce_exp env (BinE (
CmpE (e1', EqOp, e21') $ e.at,
OrOp,
MemE (e1', SeqE es2' $ e2.at) $ e.at
) $ e.at)
| _ when is_normal_exp e2' -> reduce_exp env (CmpE (e1', EqOp, e2') $ e.at)
| _ -> MemE (e1', e2') $ e.at
)
| SeqE [] -> BoolE false
| SeqE es2' when List.exists (Eq.eq_exp e1') es2' -> BoolE true
| SeqE es2' when is_normal_exp e1' && List.for_all is_normal_exp es2' -> BoolE false
| _ -> MemE (e1', e2')
) $ e.at
| LenE e1 ->
let e1' = reduce_exp env e1 in
(match e1'.it with
Expand Down Expand Up @@ -488,7 +493,7 @@ and match_exp env s e1 e2 : subst option =
let e2' = Subst.subst_exp s e2 in
if equiv_exp env e1 e2' then
Some s
else if is_normal_exp e1 && is_normal_exp e2' then
else if is_head_normal_exp e1 && is_head_normal_exp e2' then
None
else
raise Irred
Expand Down Expand Up @@ -585,7 +590,7 @@ and match_exp env s e1 e2 : subst option =
let* s' = match_exp env s e11 e21 in match_iter env s' iter1 iter2
| (HoleE _ | FuseE _ | UnparenE _), _
| _, (HoleE _ | FuseE _ | UnparenE _) -> assert false
| _, _ when is_normal_exp e1 -> None
| _, _ when is_head_normal_exp e1 -> None
| _, _ -> raise Irred

and match_expfield env s (atom1, e1) (atom2, e2) =
Expand Down
44 changes: 27 additions & 17 deletions spectec/src/il/eval.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -102,11 +102,20 @@ and reduce_typ_app' env id args at = function

(* Expression Reduction *)

and is_head_normal_exp e =
match e.it with
| BoolE _ | NatE _ | TextE _ | UnE (MinusOp _, {it = NatE _; _})
| OptE _ | ListE _ | TupE _ | CaseE _ | StrE _ -> true
| SubE (e, _, _) -> is_head_normal_exp e
| _ -> false

and is_normal_exp e =
match e.it with
| BoolE _ | NatE _ | TextE _ | ListE _ | OptE _
| UnE (MinusOp _, {it = NatE _; _})
| StrE _ | TupE _ | CaseE _ -> true
| BoolE _ | NatE _ | TextE _ | UnE (MinusOp _, {it = NatE _; _}) -> true
| ListE es | TupE es -> List.for_all is_normal_exp es
| OptE None -> true
| OptE (Some e) | CaseE (_, e) | SubE (e, _, _) -> is_normal_exp e
| StrE efs -> List.for_all (fun (_, e) -> is_normal_exp e) efs
| _ -> false

and reduce_exp env e : exp =
Expand Down Expand Up @@ -173,8 +182,10 @@ 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 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'))
| EqOp, _, _ when Eq.eq_exp e1' e2' -> BoolE true
| EqOp, _, _ when is_normal_exp e1' && is_normal_exp e2' -> BoolE false
| NeOp, _, _ when Eq.eq_exp e1' e2' -> BoolE false
| NeOp, _, _ when is_normal_exp e1' && is_normal_exp e2' -> BoolE true
| LtOp _, NatE n1, NatE n2 -> BoolE (n1 < n2)
| LtOp _, UnE (MinusOp _, {it = NatE n1; _}), UnE (MinusOp _, {it = NatE n2; _}) -> BoolE (n2 < n1)
| LtOp _, UnE (MinusOp _, {it = NatE _; _}), NatE _ -> BoolE true
Expand Down Expand Up @@ -249,15 +260,14 @@ and reduce_exp env e : exp =
let e1' = reduce_exp env e1 in
let e2' = reduce_exp env e2 in
(match e2'.it with
| OptE None | ListE [] -> BoolE false $> e
| OptE (Some e21') -> reduce_exp env (CmpE (EqOp, e1', e21') $> e)
| ListE (e21'::es2') ->
reduce_exp env (BinE (OrOp,
CmpE (EqOp, e1', e21') $> e,
MemE (e1', ListE es2' $> e2) $> e
) $> e)
| _ -> MemE (e1', e2') $> e
)
| OptE None -> BoolE false
| OptE (Some e2') when Eq.eq_exp e1' e2' -> BoolE true
| OptE (Some e2') when is_normal_exp e1' && is_normal_exp e2' -> BoolE false
| ListE [] -> BoolE false
| ListE es2' when List.exists (Eq.eq_exp e1') es2' -> BoolE true
| ListE es2' when is_normal_exp e1' && List.for_all is_normal_exp es2' -> BoolE false
| _ -> MemE (e1', e2')
) $> e
| LenE e1 ->
let e1' = reduce_exp env e1 in
(match e1'.it with
Expand Down Expand Up @@ -355,7 +365,7 @@ and reduce_exp env e : exp =
)
| _ -> SubE (e1', t1', t2') $> e
)
| _ when is_normal_exp e1' ->
| _ when is_head_normal_exp e1' ->
{e1' with note = e.note}
| _ -> SubE (e1', t1', t2') $> e
)
Expand Down Expand Up @@ -607,7 +617,7 @@ and match_exp' env s e1 e2 : subst option =
| _, SubE (e21, t21, _t22) ->
if sub_typ env e1.note t21 then
match_exp' env s (reduce_exp env (SubE (e1, e1.note, t21) $> e21)) e21
else if is_normal_exp e1 then
else if is_head_normal_exp e1 then
let t21' = reduce_typ env t21 in
if
match e1.it, t21'.it with
Expand All @@ -629,7 +639,7 @@ and match_exp' env s e1 e2 : subst option =
then match_exp' env s {e1 with note = t21} e21
else None
else raise Irred
| _, _ when is_normal_exp e1 -> None
| _, _ when is_head_normal_exp e1 -> None
| _, _ ->
raise Irred

Expand Down

0 comments on commit 0c288f7

Please sign in to comment.