From 421d664a18cea3abe729dd7becd7edadec1afaf1 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Sat, 17 Dec 2022 17:38:35 +0000 Subject: Add type checking and inference. --- src/Obs/Main.idr | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'src/Obs/Main.idr') diff --git a/src/Obs/Main.idr b/src/Obs/Main.idr index 639094f..2cf10e6 100644 --- a/src/Obs/Main.idr +++ b/src/Obs/Main.idr @@ -1,9 +1,11 @@ module Obs.Main import Obs.Abstract +import Obs.NormalForm import Obs.Parser import Obs.Syntax import Obs.Term +import Obs.Typing import System @@ -20,5 +22,6 @@ main = do [_, file] <- getArgs | _ => usage defs <- parseFile file - blk <- printErr $ abstractBlock defs - putDoc $ pretty blk + blk <- Abstract.printErr $ abstractBlock defs + ctx <- Typing.printErr $ checkBlock blk + putDoc $ pretty ctx -- cgit v1.2.3