Skip to content

Commit

Permalink
Run the renamer on parsed cryptol types. Fixes #37.
Browse files Browse the repository at this point in the history
Parsing something like {| Bit |} now properly refers to
type Bit from the Cryptol prelude.
  • Loading branch information
Brian Huffman committed Aug 3, 2015
1 parent b4a2a17 commit d2fd1f2
Showing 1 changed file with 9 additions and 2 deletions.
11 changes: 9 additions & 2 deletions src/SAWScript/CryptolEnv.hs
Original file line number Diff line number Diff line change
Expand Up @@ -372,13 +372,20 @@ parseSchema :: CryptolEnv s -> Located String -> IO T.Schema
parseSchema env input = do
--putStrLn $ "parseSchema: " ++ show input
let modEnv = eModuleEnv env

-- | Parse
pschema <- ioParseSchema input
--putStrLn $ "ioParseSchema: " ++ show pschema

-- | Resolve names
let nameEnv = MR.namingEnv pschema `MR.shadowing` getNamingEnv env
(rschema, _) <- liftModuleM modEnv (MM.interactive (MB.rename nameEnv pschema))

let ifDecls = getAllIfaceDecls modEnv
let range = fromMaybe P.emptyRange (P.getLoc pschema)
let range = fromMaybe P.emptyRange (P.getLoc rschema)
(tcEnv, _) <- liftModuleM modEnv $ MB.genInferInput range ifDecls
let tcEnv' = tcEnv { TM.inpTSyns = Map.union (eExtraTSyns env) (TM.inpTSyns tcEnv) }
out <- TM.runInferM tcEnv' (TK.checkSchema pschema)
out <- TM.runInferM tcEnv' (TK.checkSchema rschema)
((schema, goals), _) <- liftModuleM modEnv (MM.interactive (runInferOutput out))
unless (null goals) (print goals)
return schema
Expand Down

0 comments on commit d2fd1f2

Please sign in to comment.