From 765c62866a2f0b13d86e9143d08bc8256d5d9c98 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Mon, 13 Mar 2023 19:33:09 +0100 Subject: [PATCH] more FromParser --- lib/Quox/Definition.idr | 5 ++ lib/Quox/Parser/FromParser.idr | 109 +++++++++++++++++++++++---------- lib/Quox/Parser/Parser.idr | 4 +- lib/Quox/Syntax/Qty.idr | 4 ++ tests/Tests/FromPTerm.idr | 12 ++-- tests/TypingImpls.idr | 16 +++++ 6 files changed, 110 insertions(+), 40 deletions(-) diff --git a/lib/Quox/Definition.idr b/lib/Quox/Definition.idr index 41e426c..844f806 100644 --- a/lib/Quox/Definition.idr +++ b/lib/Quox/Definition.idr @@ -40,6 +40,11 @@ mkPostulate : IsQty q => (qty : q) -> (0 _ : IsGlobal qty) => (type : forall d, n. Term q d n) -> Definition q mkPostulate qty type = MkDef {qty, type = T type, body = Postulate} +public export %inline +mkDef0 : IsQty q => (qty : q) -> (0 _ : IsGlobal qty) => + (type, term : Term q 0 0) -> Definition q +mkDef0 qty type term = mkDef qty (inject type) (inject term) + public export %inline (.get0) : AnyTerm q -> Term q 0 0 diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr index 136c0ca..ab8b00a 100644 --- a/lib/Quox/Parser/FromParser.idr +++ b/lib/Quox/Parser/FromParser.idr @@ -2,6 +2,7 @@ module Quox.Parser.FromParser import Quox.Parser.Syntax +import Quox.Parser.Parser import Quox.Typechecker import Data.List @@ -9,6 +10,13 @@ import public Control.Monad.Either import public Control.Monad.State import public Control.Monad.Reader +import System.File +import System.Path + + +public export +0 Defs : Type +Defs = Definitions Three public export data FromParserError = @@ -17,26 +25,34 @@ data FromParserError = | DimNotInScope PBaseName | QtyNotGlobal PQty | DimNameInTerm PBaseName - -public export -interface LoadFile m where - loadFile : (file : String) -> m PTopLevel + | TypeError (Typing.Error Three) + | LoadError String FileError + | ParseError Parser.Error public export 0 CanError : (Type -> Type) -> Type CanError = MonadError FromParserError +public export +0 HasDefsRW : (Type -> Type) -> Type +HasDefsRW = MonadState Defs + public export 0 HasNamespace : (Type -> Type) -> Type HasNamespace = MonadReader Mods + public export -0 HasSeenFiles : (Type -> Type) -> Type -HasSeenFiles = MonadState (SortedSet String) +0 LoadFile : (Type -> Type) -> Type +LoadFile m = + (HasIO m, MonadReader (List String) m, MonadState (SortedSet String) m) + -- reader for include paths, state for seen files + public export 0 FromParser : (Type -> Type) -> Type -FromParser m = (CanError m, HasNamespace m, HasSeenFiles m) +FromParser m = + (CanError m, HasDefsRW m, HasNamespace m, LoadFile m) @@ -179,34 +195,61 @@ globalPQty pi = case isGlobal pi of No n => throwError $ QtyNotGlobal pi +export +fromPNameNS : HasNamespace m => PName -> m Name +fromPNameNS name = asks $ \ns => addMods ns $ fromPName name --- -- [todo] extend substitutions so they can do this injection. that's the sort of --- -- thing they are for. --- export --- fromPDefinition : FromParser m => PDefinition -> m (Name, Definition Three) --- fromPDefinition (MkPDef {name, qty, type, term}) = --- pure (addMods !ask $ fromPName name, MkDef' { --- qty, qtyGlobal = !(globalPQty qty), --- type = T $ inject !(fromPTerm type), --- term = Just $ T $ inject !(fromPTerm term) --- }) +private +injTC : (CanError m, HasDefsRW m) => (forall m'. CanTC Three m' => m' a) -> m a +injTC act = + either (throwError . TypeError) pure $ + runReaderT {m = Either _} !get act + +export +fromPDef : (CanError m, HasDefsRW m, HasNamespace m) => PDefinition -> m () +fromPDef (MkPDef qty pname ptype pterm) = do + name <- fromPNameNS pname + qtyGlobal <- globalPQty qty + let sqty = globalToSubj $ Element qty qtyGlobal + type <- traverse fromPTerm ptype + term <- fromPTerm pterm + case type of + Just type => do + injTC $ checkTypeC empty type Nothing + injTC $ ignore $ checkC empty sqty term type + modify $ insert name $ mkDef0 qty type term + Nothing => do + let E elim = term | _ => throwError $ AnnotationNeeded pterm + res <- injTC $ inferC empty sqty elim + modify $ insert name $ mkDef0 qty res.type term + +export +fromPDecl : FromParser m => PDecl -> m () +fromPDecl (PDef def) = fromPDef def +fromPDecl (PNs ns) = + local (<+> ns.name) $ concat <$> traverse fromPDecl ns.decls --- export --- fromPDecl : FromParser m => PDecl -> m (List (Name, Definition Three)) --- fromPDecl (PDef def) = singleton <$> fromPDefinition def --- fromPDecl (PNs ns) = local (<+> ns.name) $ --- concat <$> assert_total traverse fromPDecl ns.decls +export +loadFile : (LoadFile m, CanError m) => String -> m (Maybe String) +loadFile file = + if contains file !get then + pure Nothing + else do + Just file <- firstExists (map ( file) !ask) + | Nothing => throwError $ LoadError file FileNotFound + case !(readFile file) of + Right res => pure $ Just res + Left err => throwError $ LoadError file err --- export covering --- fromPTopLevel : (FromParser m, LoadFile m) => --- PTopLevel -> m (List (Name, Definition Three)) --- fromPTopLevel (PD decl) = fromPDecl decl --- fromPTopLevel (PLoad file) = --- if contains file !get then --- pure [] --- else do --- modify $ insert file --- t <- loadFile file --- fromPTopLevel t +||| populates the `defs` field of the state +export +fromPTopLevel : FromParser m => PTopLevel -> m () +fromPTopLevel (PD decl) = fromPDecl decl +fromPTopLevel (PLoad file) = + case !(loadFile file) of + Just inp => do + tl <- either (throwError . ParseError) pure $ lexParseInput inp + traverse_ fromPTopLevel tl + Nothing => pure () diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr index cc61f64..b731f74 100644 --- a/lib/Quox/Parser/Parser.idr +++ b/lib/Quox/Parser/Parser.idr @@ -277,9 +277,7 @@ defIntro = Zero <$ resC "def0" export covering definition : Grammar True PDefinition definition = - [|MkPDef defIntro name - (optional (resC ":" *> term)) - (resC "≔" *> term)|] + [|MkPDef defIntro name (optional (resC ":" *> term)) (resC "≔" *> term)|] export load : Grammar True String diff --git a/lib/Quox/Syntax/Qty.idr b/lib/Quox/Syntax/Qty.idr index 2318649..a4fb890 100644 --- a/lib/Quox/Syntax/Qty.idr +++ b/lib/Quox/Syntax/Qty.idr @@ -88,3 +88,7 @@ GQty q = Subset q IsGlobal public export %inline gzero : IsQty q => GQty q gzero = Element zero $ zeroIsGlobal zeroIsZero + +export %inline +globalToSubj : IsQty q => GQty q -> SQty q +globalToSubj q = if isYes $ isZero q.fst then szero else sone diff --git a/tests/Tests/FromPTerm.idr b/tests/Tests/FromPTerm.idr index 3991f7c..1faa0ee 100644 --- a/tests/Tests/FromPTerm.idr +++ b/tests/Tests/FromPTerm.idr @@ -3,9 +3,11 @@ module Tests.FromPTerm import Quox.Parser.Syntax import Quox.Parser import TermImpls +import TypingImpls import Tests.Parser as TParser import TAP +import System.File import Derive.Prelude %language ElabReflection @@ -15,16 +17,18 @@ import Derive.Prelude public export data Failure = ParseError (Parser.Error) - | FromParserError FromParserError + | FromParser FromParserError | WrongResult String | ExpectedFail String -%runElab derive "FromParser.FromParserError" [Show] +%runElab derive "FileError" [Show] +%runElab derive "Parser.Error" [Show] +%runElab derive "FromParserError" [Show] export ToInfo Failure where toInfo (ParseError err) = toInfo err - toInfo (FromParserError err) = + toInfo (FromParser err) = [("type", "FromParserError"), ("got", show err)] toInfo (WrongResult got) = @@ -40,7 +44,7 @@ parameters {c : Bool} {auto _ : Show b} parsesWith : (b -> Bool) -> Test parsesWith p = test label $ do pres <- mapFst ParseError $ lexParseWith grm inp - res <- mapFst FromParserError $ fromP pres + res <- mapFst FromParser $ fromP pres unless (p res) $ Left $ WrongResult $ show res parses : Test diff --git a/tests/TypingImpls.idr b/tests/TypingImpls.idr index 26c4e3b..584bd82 100644 --- a/tests/TypingImpls.idr +++ b/tests/TypingImpls.idr @@ -3,7 +3,23 @@ module TypingImpls import TAP import public Quox.Typing import public Quox.Pretty +import public TermImpls +import Derive.Prelude +%language ElabReflection + + +%runElab derive "WhnfErr" [Show] + +%runElab deriveIndexed "DimEq" [Show] + +export %hint +showTyContext : (PrettyHL q, Show q) => Show (TyContext q d n) +showTyContext = deriveShow + +export %hint +showTypingError : (PrettyHL q, Show q) => Show (Error q) +showTypingError = deriveShow export ToInfo WhnfErr where