Skip to content

Make it so that RM get optimized to take in 3 args in PolyML #1776

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
ordinarymath wants to merge 1 commit into
base: develop
Choose a base branch
from
Open

Make it so that RM get optimized to take in 3 args in PolyML #1776

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 7 additions & 7 deletions src/0/Term.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -891,7 +891,7 @@ local
val tymatch = Type.raw_match_type
open KernelSig
in
fun RM [] theta = theta
fun RM [] (tmS,tyS) = (tmS,tyS)
| RM (((v as Fv(n,Ty)),tm,scoped)::rst) ((S1 as (tmS,Id)),tyS)
= if bound_by_scope scoped tm
then MERR "Attempt to capture bound variable"
Expand Down Expand Up @@ -920,12 +920,12 @@ fun RM [] theta = theta
| (POLY pat,POLY obj) => (tmS, tymatch pat obj tyS))
| RM ((Abs(Fv(_,ty1),M),Abs(Fv(_,ty2),N),_)::rst) (tmS,tyS)
= RM ((M,N,true)::rst) (tmS, tymatch ty1 ty2 tyS)
| RM ((Comb(M,N),Comb(P,Q),s)::rst) S = RM ((M,P,s)::(N,Q,s)::rst) S
| RM ((Bv i,Bv j,_)::rst) S = if i=j then RM rst S
else MERR "Bound var doesn't match"
| RM (((pat as Clos _),ob,s)::t) S = RM ((push_clos pat,ob,s)::t) S
| RM ((pat,(ob as Clos _),s)::t) S = RM ((pat,push_clos ob,s)::t) S
| RM all others = MERR "different constructors"
| RM ((Comb(M,N),Comb(P,Q),s)::rst) (tmS,tyS) = RM ((M,P,s)::(N,Q,s)::rst) (tmS,tyS)
| RM ((Bv i,Bv j,_)::rst) (tmS,tyS) = if i=j then RM rst (tmS,tyS)
else MERR "Bound var doesn't match"
| RM (((pat as Clos _),ob,s)::t) (tmS,tyS) = RM ((push_clos pat,ob,s)::t) (tmS,tyS)
| RM ((pat,(ob as Clos _),s)::t) (tmS,tyS) = RM ((pat,push_clos ob,s)::t) (tmS,tyS)
| RM all (tmS,tyS) = MERR "different constructors"
end

fun raw_match tyfixed tmfixed pat ob (tmS,tyS)
Expand Down