From b7ba1a93012b283112475dff125cd56ddc6e18f3 Mon Sep 17 00:00:00 2001 From: Ohad Kammar Date: Sun, 23 Feb 2020 15:18:10 +0000 Subject: [PATCH] Decouple totality annotations from `IFnOpt` using the existing `TotalReq` value This requires moving `TotalReq` into `src/Core/TT.idr`. --- src/Core/Context.idr | 10 ---------- src/Core/Options.idr | 1 + src/Core/TT.idr | 10 ++++++++++ src/Idris/Parser.idr | 22 +++++++++++++--------- src/TTImp/Parser.idr | 10 +++++++--- src/TTImp/ProcessType.idr | 6 +++--- src/TTImp/TTImp.idr | 26 +++++++++++--------------- 7 files changed, 45 insertions(+), 40 deletions(-) diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 5a6b460..9a27d6d 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -122,9 +122,6 @@ data Clause : Type where MkClause : (env : Env Term vars) -> (lhs : Term vars) -> (rhs : Term vars) -> Clause -public export -data TotalReq = Total | CoveringOnly | PartialOK - public export data DefFlag = Inline @@ -142,13 +139,6 @@ data DefFlag | BlockedHint -- a hint, but blocked for the moment (so don't use) | Macro -export -Eq TotalReq where - (==) Total Total = True - (==) CoveringOnly CoveringOnly = True - (==) PartialOK PartialOK = True - (==) _ _ = False - export Eq DefFlag where (==) Inline Inline = True diff --git a/src/Core/Options.idr b/src/Core/Options.idr index 1ace4cd..9b87861 100644 --- a/src/Core/Options.idr +++ b/src/Core/Options.idr @@ -2,6 +2,7 @@ module Core.Options import Core.Core import Core.Name +import Core.TT import Utils.Binary import System.Info diff --git a/src/Core/TT.idr b/src/Core/TT.idr index fd3ea5a..2ac466c 100644 --- a/src/Core/TT.idr +++ b/src/Core/TT.idr @@ -508,6 +508,16 @@ Ord Visibility where compare Public Private = GT compare Public Export = GT +public export +data TotalReq = Total | CoveringOnly | PartialOK + +export +Eq TotalReq where + (==) Total Total = True + (==) CoveringOnly CoveringOnly = True + (==) PartialOK PartialOK = True + (==) _ _ = False + public export data PartialReason = NotStrictlyPositive diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index af8949e..666f3af 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -921,6 +921,15 @@ extension = do exactIdent "Borrowing" pure Borrowing +totalityOpt : Rule TotalReq +totalityOpt + = do keyword "partial" + pure PartialOK + <|> do keyword "total" + pure Total + <|> do keyword "covering" + pure CoveringOnly + directive : FileName -> IndentInfo -> Rule Directive directive fname indents = do exactIdent "hide" @@ -1048,16 +1057,11 @@ usingDecls fname indents ds <- assert_total (nonEmptyBlock (topDecl fname)) end <- location pure (PUsing (MkFC fname start end) us (collectDefs (concat ds))) - + fnOpt : Rule PFnOpt -fnOpt - = do keyword "partial" - pure $ IFnOpt PartialOK - <|> do keyword "total" - pure $ IFnOpt Total - <|> do keyword "covering" - pure $ IFnOpt Covering - +fnOpt = do x <- totalityOpt + pure $ IFnOpt (Totality x) + fnDirectOpt : FileName -> Rule PFnOpt fnDirectOpt fname = do exactIdent "hint" diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr index 28c3dd0..1041925 100644 --- a/src/TTImp/Parser.idr +++ b/src/TTImp/Parser.idr @@ -65,14 +65,18 @@ visibility = visOption <|> pure Private -fnOpt : Rule FnOpt -fnOpt +totalityOpt : Rule TotalReq +totalityOpt = do keyword "partial" pure PartialOK <|> do keyword "total" pure Total <|> do keyword "covering" - pure Covering + pure CoveringOnly + +fnOpt : Rule FnOpt +fnOpt = do x <- totalityOpt + pure $ Totality x fnDirectOpt : Rule FnOpt fnDirectOpt diff --git a/src/TTImp/ProcessType.idr b/src/TTImp/ProcessType.idr index cfacd81..86f3d61 100644 --- a/src/TTImp/ProcessType.idr +++ b/src/TTImp/ProcessType.idr @@ -46,11 +46,11 @@ processFnOpt fc ndef (ForeignFn _) = setFlag fc ndef Inline -- if externally defined, inline when compiling processFnOpt fc ndef Invertible = setFlag fc ndef Invertible -processFnOpt fc ndef Total +processFnOpt fc ndef (Totality Total) = setFlag fc ndef (SetTotal Total) -processFnOpt fc ndef Covering +processFnOpt fc ndef (Totality Covering) = setFlag fc ndef (SetTotal CoveringOnly) -processFnOpt fc ndef PartialOK +processFnOpt fc ndef (Totality PartialOK) = setFlag fc ndef (SetTotal PartialOK) processFnOpt fc ndef Macro = setFlag fc ndef Macro diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index 825573e..8f0def3 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -187,9 +187,7 @@ mutual ForeignFn : List RawImp -> FnOpt -- assume safe to cancel arguments in unification Invertible : FnOpt - Total : FnOpt - Covering : FnOpt - PartialOK : FnOpt + Totality : TotalReq -> FnOpt Macro : FnOpt export @@ -200,9 +198,9 @@ mutual show ExternFn = "%extern" show (ForeignFn cs) = "%foreign " ++ showSep " " (map show cs) show Invertible = "%invertible" - show Total = "total" - show Covering = "covering" - show PartialOK = "partial" + show (Totality Total) = "total" + show (Totality CoveringOnly) = "covering" + show (Totality PartialOK) = "partial" show Macro = "%macro" export @@ -213,9 +211,7 @@ mutual ExternFn == ExternFn = True (ForeignFn xs) == (ForeignFn ys) = True -- xs == ys Invertible == Invertible = True - Total == Total = True - Covering == Covering = True - PartialOK == PartialOK = True + (Totality tot_lhs) == (Totality tot_rhs) = tot_lhs == tot_rhs Macro == Macro = True _ == _ = False @@ -858,9 +854,9 @@ mutual toBuf b ExternFn = tag 3 toBuf b (ForeignFn cs) = do tag 4; toBuf b cs toBuf b Invertible = tag 5 - toBuf b Total = tag 6 - toBuf b Covering = tag 7 - toBuf b PartialOK = tag 8 + toBuf b (Totality Total) = tag 6 + toBuf b (Totality CoveringOnly) = tag 7 + toBuf b (Totality PartialOK) = tag 8 toBuf b Macro = tag 9 fromBuf b @@ -871,9 +867,9 @@ mutual 3 => pure ExternFn 4 => do cs <- fromBuf b; pure (ForeignFn cs) 5 => pure Invertible - 6 => pure Total - 7 => pure Covering - 8 => pure PartialOK + 6 => pure (Totality Total) + 7 => pure (Totality CoveringOnly) + 8 => pure (Totality PartialOK) 9 => pure Macro _ => corrupt "FnOpt"