Skip to content

Commit

Permalink
Relax rules for variable binding
Browse files Browse the repository at this point in the history
Summary:
The existing behaviour was too strict and ruled out some useful
predicates, e.g.

```
predicate P : { a : hack.Name, b : string }
  { hack.Name S, S }
```

we would have to use a workaround like

```
predicate P : { a : hack.Name, b : string }
  { hack.Name S, S } where S : string
```

but that should be unnecessary.

Reviewed By: josefs

Differential Revision: D65269922

fbshipit-source-id: eb01c5d61b4da154645d376515241a0535bec5ea
  • Loading branch information
Simon Marlow authored and facebook-github-bot committed Nov 1, 2024
1 parent 68aef3b commit 069ffd0
Show file tree
Hide file tree
Showing 3 changed files with 12 additions and 13 deletions.
13 changes: 6 additions & 7 deletions glean/db/Glean/Query/Typecheck.hs
Original file line number Diff line number Diff line change
Expand Up @@ -90,7 +90,7 @@ typecheck dbSchema opts rtsType query = do
let state = initialTypecheckState tcEnv opts rtsType TcModeQuery in
withExceptT (Text.pack . show) $ flip runStateT state $ do
modify $ \s -> s { tcVisible = varsQuery query mempty }
q@(TcQuery retTy _ _ _ _) <- inferQuery ContextExpr query
q@(TcQuery retTy _ _ _ _) <- inferQuery ContextPat query
<* freeVariablesAreErrors <* unboundVariablesAreErrors
subst <- gets tcSubst
whenDebug $ liftIO $ hPutStrLn stderr $ show $
Expand Down Expand Up @@ -152,7 +152,7 @@ typecheckDeriving tcEnv opts rtsType PredicateDetails{..} derivingInfo = do
in
(key, Just (App span val xs))
_other -> (head, Nothing)
key' <- typecheckPattern ContextExpr predicateKeyType key
key' <- typecheckPattern ContextPat predicateKeyType key
maybeVal' <- case maybeVal of
Nothing
| eqType (tcOptAngleVersion opts) unit predicateValueType ->
Expand All @@ -161,7 +161,7 @@ typecheckDeriving tcEnv opts rtsType PredicateDetails{..} derivingInfo = do
[ "a functional predicate must return a value,"
, "i.e. the query should have the form 'X -> Y where .." ]
Just val -> Just <$>
typecheckPattern ContextExpr predicateValueType val
typecheckPattern ContextPat predicateValueType val
stmts' <- mapM typecheckStatement stmts
freeVariablesAreErrors
unboundVariablesAreErrors
Expand Down Expand Up @@ -228,7 +228,7 @@ typecheckQuery
-> T TcQuery
typecheckQuery ctx ty q = do
(head,stmts,ord) <- needsResult q
head' <- typecheckPattern ctx ty head
head' <- typecheckPattern ctx ty head
stmts' <- mapM typecheckStatement stmts
return (TcQuery ty head' Nothing stmts' ord)

Expand Down Expand Up @@ -309,7 +309,7 @@ inferExpr ctx pat = case pat of
Prim span primOp args -> do
(primArgTys, retTy) <- primOpType primOp
checkPrimOpArgs span args primArgTys
args' <- zipWithM (typecheckPattern ctx) primArgTys args
args' <- zipWithM (typecheckPattern ContextExpr) primArgTys args
return (RTS.Ref (MatchExt (Typed retTy (TcPrimCall primOp args'))),
retTy)
Clause _ pred pat range -> tcFactGenerator pred pat range
Expand Down Expand Up @@ -545,7 +545,7 @@ typecheckPattern ctx typ pat = case (typ, pat) of
(ty, Prim span primOp args) -> do
(primArgTys, retTy) <- primOpType primOp
checkPrimOpArgs span args primArgTys
args' <- zipWithM (typecheckPattern ctx) primArgTys args
args' <- zipWithM (typecheckPattern ContextExpr) primArgTys args
inPat pat $ unify ty retTy
return (RTS.Ref (MatchExt (Typed retTy (TcPrimCall primOp args'))))
(PredicateTy (PidRef _ ref), Clause _ ref' arg range) ->
Expand Down Expand Up @@ -808,7 +808,6 @@ unboundVariablesAreErrors_ uses binds = do
hsep (punctuate "," (map pretty badGuys))
, "All variables must occur at least once in a context that will bind"
, "the variable to a value; i.e., *not*"
, " * the head of a derived predicate"
, " * the argument of a primitive"
, " * the array in an array generator Arr[..]"
, "A variable that is bound in just one side of '|'"
Expand Down
10 changes: 5 additions & 5 deletions glean/test/tests/Angle/AngleTest.hs
Original file line number Diff line number Diff line change
Expand Up @@ -724,7 +724,7 @@ angleIfThenElse modify = dbTestCase $ \env repo -> do
[Nat 1] r

r <- try $ runQuery_ env repo $ angleData @Nat
"if (A = 1) then A else A"
"if (A = 1) then A else A+1"
print r
assertBool
"if statement - variables bound in condition are not available in 'else' branch" $
Expand All @@ -734,7 +734,7 @@ angleIfThenElse modify = dbTestCase $ \env repo -> do

r <- try $ runQuery_ env repo $ angleData @Nat
[s|
A where if (A = 1) then A else 2;
A+1 where if (A = 1) then A else 2;
|]
print r
assertBool
Expand All @@ -745,7 +745,7 @@ angleIfThenElse modify = dbTestCase $ \env repo -> do

r <- try $ runQuery_ env repo $ angleData @Nat
[s|
A where if 1 then (A = 1) else 2;
A+1 where if 1 then (A = 1) else 2;
|]
print r
assertBool
Expand All @@ -756,7 +756,7 @@ angleIfThenElse modify = dbTestCase $ \env repo -> do

r <- try $ runQuery_ env repo $ angleData @Nat
[s|
A where if never : {} then 1 else (A = 1) ;
A+1 where if never : {} then 1 else (A = 1) ;
|]
print r
assertBool
Expand Down Expand Up @@ -813,7 +813,7 @@ angleNegationTest modify = dbTestCase $ \env repo -> do
-- negated queries do not bind variables to the parent scope
r <- try $ runQuery_ env repo $ modify $ angleData @()
[s|
A where !(A = glean.test.IsGlean "not-glean");
A+1 where !(A = 0);
|]
print r
assertBool "negation - scope" $
Expand Down
2 changes: 1 addition & 1 deletion glean/test/tests/Angle/MiscTest.hs
Original file line number Diff line number Diff line change
Expand Up @@ -90,7 +90,7 @@ scopingTest = dbTestCase $ \env repo -> do
|]
print r
assertBool "angle - scoping 2" $ case r of
Left e@BadQuery{} -> "not bound anywhere: N" `isInfixOf` show e
Left e@BadQuery{} -> "cannot resolve" `isInfixOf` show e
_ -> False

-- it's OK to not bind the variable in every branch of | if it is
Expand Down

0 comments on commit 069ffd0

Please sign in to comment.