tricu

An interpreted language for exploring Tree Calculus
Log | Files | Refs | README | LICENSE

ContractDesugar.hs (4494B)

      1 {-# LANGUAGE LambdaCase #-}
      2 
      3 module Frontend.ContractDesugar
      4   ( desugarContracts
      5   , viewExprToAst
      6   ) where
      7 
      8 import Research
      9 
     10 -- | Convert source-level contract annotations into runtime boundary checks.
     11 --
     12 -- Named binder annotations (e.g. @x@nat?) wrap each argument as it is
     13 -- received and the result before it is returned.
     14 --
     15 -- Phantom annotations (e.g. @nat? on a point-free definition) are turned
     16 -- into a fresh local raw value plus a wrapper definition that uses named
     17 -- binder annotations.  The raw value is bound with a local 'let' so that
     18 -- fixed points (such as definitions built with 'y') are shared rather than
     19 -- recreated on every call.  The wrapper only needs 'withContract' and
     20 -- 'matchResult' from the contract library.
     21 desugarContracts :: [TricuAST] -> [TricuAST]
     22 desugarContracts asts = concatMap desugarTopItem asts
     23   where
     24     desugarTopItem (SDefAnn name args ret body) = desugarDefAnn name args ret body
     25     desugarTopItem other = [other]
     26 
     27 -- | Fresh internal name for the raw, contract-free helper introduced by
     28 -- phantom annotations.  It is bound locally with 'SLet' so it never escapes
     29 -- into the final environment.
     30 rawNameFor :: String -> String
     31 rawNameFor name = "_" ++ name ++ "_raw"
     32 
     33 desugarDefAnn :: String -> [DefArg] -> Maybe ViewExpr -> TricuAST -> [TricuAST]
     34 desugarDefAnn name args ret body
     35   | all isPhantom args =
     36       let argContracts = map getPhantom args
     37           rawNm = rawNameFor name
     38           rawVar = SVar rawNm Nothing
     39           argNames = take (length args) ["x","y","z"]
     40           newArgs = zipWith DefBinder argNames (map Just argContracts)
     41           wrappedBody = foldl SApp rawVar (map (\n -> SVar n Nothing) argNames)
     42           wrapper = wrapArgs newArgs (wrapReturn ret wrappedBody)
     43       in [ SDef name [] (SLet rawNm body wrapper) ]
     44   | otherwise = [ SDef name [] (wrapArgs args body') ]
     45   where
     46     body' = wrapReturn ret body
     47 
     48     isPhantom (DefPhantom _) = True
     49     isPhantom _              = False
     50 
     51     getPhantom (DefPhantom c) = c
     52     getPhantom _                = error "expected phantom annotation"
     53 
     54     -- | Build:  matchResult onFail (\value _ -> body) result
     55     bindResult result valueName body onFail =
     56       matchResultE
     57         onFail
     58         (SLambda [valueName, "_"] body)
     59         result
     60 
     61     -- | Build:  matchResult (\msg _ -> err msg t) (\r _ -> r) result
     62     returnResult result =
     63       matchResultE
     64         (SLambda ["msg", "_"] errResult)
     65         (SLambda ["r", "_"] (SVar "r" Nothing))
     66         result
     67 
     68     -- | Build:  \msg _ -> \_ -> err msg t
     69     absorbErr =
     70       SLambda ["msg", "_"] (SLambda ["_"] errResult)
     71 
     72     errResult = SApp (SApp (SVar "err" Nothing) (SVar "msg" Nothing)) TLeaf
     73 
     74     wrapReturn Nothing b = b
     75     wrapReturn (Just c) b = returnResult (withContractE (viewExprToAst c) b)
     76 
     77     wrapArgs [] b = b
     78     wrapArgs (DefBinder nm Nothing : rest) b = SLambda [nm] (wrapArgs rest b)
     79     wrapArgs (DefBinder nm (Just c) : rest) b =
     80       let onFail = if null rest then SLambda ["msg", "_"] errResult else absorbErr
     81       in SLambda [nm] $
     82            bindResult
     83              (withContractE (viewExprToAst c) (SVar nm Nothing))
     84              nm
     85              (wrapArgs rest b)
     86              onFail
     87     wrapArgs (DefPhantom _ : _) _ =
     88       error "phantom contract arguments are not yet supported by the frontend"
     89 
     90 -- | Turn a source annotation expression into an ordinary AST expression.
     91 -- Contract annotations are written with the same surface syntax as terms,
     92 -- so the mapping is mostly structural.
     93 viewExprToAst :: ViewExpr -> TricuAST
     94 viewExprToAst = \case
     95   VEName s -> SVar s Nothing
     96   VEVar s  -> SVar s Nothing
     97   VEInt i  -> SInt i
     98   VEString s -> SStr s
     99   VEList es -> SList (map viewExprToAst es)
    100   VEApp f a -> SApp (viewExprToAst f) (viewExprToAst a)
    101   VERaw s -> SStr s
    102   VEVarId _ -> error "view variable ids are not supported by the frontend"
    103   VEForall _ _ -> error "forall annotations are not supported by the frontend"
    104   VEExists _ _ -> error "exists annotations are not supported by the frontend"
    105 
    106 -- | Build an application of 'withContract' from the contract library.
    107 withContractE :: TricuAST -> TricuAST -> TricuAST
    108 withContractE contract value =
    109   SApp (SApp (SVar "withContract" Nothing) contract) value
    110 
    111 -- | Build an application of 'matchResult' from the contract library.
    112 matchResultE :: TricuAST -> TricuAST -> TricuAST -> TricuAST
    113 matchResultE errCase okCase result =
    114   SApp
    115     (SApp
    116       (SApp (SVar "matchResult" Nothing) errCase)
    117       okCase)
    118     result