Commita00dba5

committed

Update LF after removing PGrad

1 parentc065ff4 commita00dba5Copy full SHA for a00dba5

File tree

-7

lines changed

-7

lines changed

Lines changed: 0 additions & 2 deletions

Original file line number	Diff line number	Diff line change
`@@ -290,7 +290,6 @@ buildExprEdges table = Misc.ordNub . go`
`290`	`290`	`go (ETAbs e _)= go e`
`291`	`291`	`go (PKVar _ _)=[]`
`292`	`292`	`go (PExist _ e)= go e`
`293`		`- go (PGrad _ _ _ e)= go e`
`294`	`293`	`go_alias f= [f\|M.member f table ]`
`295`	`294`
`296`	`295`
`@@ -649,7 +648,6 @@ expandExpr rtEnv l = go`
`649`	`648`	`go (PIff e1 e2)=PIff (go e1) (go e2)`
`650`	`649`	`go (PAtom b e1 e2)=PAtom b (go e1) (go e2)`
`651`	`650`	`go (EIte p e1 e2)=EIte (go p)(go e1) (go e2)`
`652`		`- go (PGrad k su i e)=PGrad k su i (go e)`
`653`	`651`	`go e@(PKVar _ _)= e`
`654`	`652`	`go e@(ESym _)= e`
`655`	`653`	`go e@(ECon _)= e`

Lines changed: 0 additions & 1 deletion

Original file line number	Diff line number	Diff line change
`@@ -187,7 +187,6 @@ refTopQuals lEnv ef l tce t0 γ rrt`
`187`	`187`	`= [ mkQ' v so pa\|let (RR so (Reft (v, ra)))= rTypeSortedReft tce rrt`
`188`	`188`	`, pa<- conjuncts ra`
`189`	`189`	`,not$ isHole pa`
`190`		`- ,not$ isGradual pa`
`191`	`190`	`, notracepp ("refTopQuals:"++ showpp pa)`
`192`	`191`	`$ isNothing$ runReader (checkSorted (srcSpan l) (insertSEnv v so γ') pa) ef`
`193`	`192`	`]`

Lines changed: 0 additions & 1 deletion

Original file line number	Diff line number	Diff line change
`@@ -845,7 +845,6 @@ substExprV toSym su0 = go`
`845`	`845`	`go (PIff p1 p2)=PIff (go p1) (go p2)`
`846`	`846`	`go (PAtom r e1 e2)=PAtom r (go e1) (go e2)`
`847`	`847`	go (PKVar k su')=PKVar k$ su'`appendSubst` su0
`848`		- go (PGrad k su' i e)=PGrad k (su'`appendSubst` su0) i (go e)
`849`	`848`	`go (PAll _ _)= panicNothing"substExprV: PAll"`
`850`	`849`	`go (PExist _ _)= panicNothing"substExprV: PExist"`
`851`	`850`	`go p= p`

Lines changed: 0 additions & 2 deletions

Original file line number	Diff line number	Diff line change
`@@ -336,8 +336,6 @@ emapExprVM f = go []`
`336`	`336`	`PKVar k su->PKVar k<$> emapSubstVM (f. (domain su++). (acc++)) su`
`337`	`337`	`PAll bnds e->PAll bnds<$> go (mapfst bnds++ acc) e`
`338`	`338`	`PExist bnds e->PExist bnds<$> go (mapfst bnds++ acc) e`
`339`		`-PGrad k su gi e->`
`340`		`-PGrad k<$> emapSubstVM (f. (acc++)) su<>pure gi<> go (domain su++ acc) e`
`341`	`339`	`ECoerc srt0 srt1 e->ECoerc srt0 srt1<$> go acc e`
`342`	`340`	`ELet x e1 e2->ELet x<$> go acc e1<*> go (x:acc) e2`
`343`	`341`

Comments

(0)