Unbundle drnim

compiler/ast/ast_types.nim

@@ -389,11 +389,9 @@ const
   nkEffectList* = nkArgList
   # hacks ahead: an nkEffectList is a node with 4 children:
   exceptionEffects* = 0 ## exceptions at position 0
-  requiresEffects* = 1  ## 'requires' annotation
-  ensuresEffects* = 2   ## 'ensures' annotation
-  tagEffects* = 3       ## user defined tag ('gc', 'time' etc.)
-  pragmasEffects* = 4   ## not an effect, but a slot for pragmas in proc type
-  effectListLen* = 5    ## list of effects list
+  tagEffects* = 1       ## user defined tag ('gc', 'time' etc.)
+  pragmasEffects* = 2   ## not an effect, but a slot for pragmas in proc type
+  effectListLen* = 3    ## list of effects list
   nkLastBlockStmts* = {nkRaiseStmt, nkReturnStmt, nkBreakStmt, nkContinueStmt}
                         ## these must be last statements in a block
 
@@ -719,7 +717,6 @@ type
     mCStrToStr,
     mStrToStr, mEnumToStr,
     mAnd, mOr,
-    mImplies, mIff, mExists, mForall, mOld,
     mEqStr, mLeStr, mLtStr,
     mEqSet, mLeSet, mLtSet, mMulSet, mPlusSet, mMinusSet,
     mConStrStr, mSlice,

compiler/ast/reports.nim

@@ -336,6 +336,8 @@ type
     rsemCantComputeOffsetof
     rsemStaticOutOfBounds ## Error generated when semfold or static bound
     ## checking sees and out-of-bounds index error.
+    rsemStaticIndexLeqUnprovable
+    rsemStaticIndexGeProvable
     rsemStaticFieldNotFound # TODO DOC generated in `semfold.nim`, need
     # better documentation, right now I don't know what exactly this error
     # means and how to reproduce it in the example code.
@@ -773,10 +775,6 @@ type
     rsemUnguardedAccess
     rsemInvalidGuardField
 
-    rsemDrNimRequiresUsesMissingResult
-    rsemDrnimCannotProveLeq
-    rsemDrnimCannotPorveGe
-
     rsemErrGcUnsafeListing
     rsemBorrowPragmaNonDot
     rsemInvalidExtern
@@ -1259,8 +1257,9 @@ type
       of rsemWrongIdent:
         expectedIdents*: seq[string]
 
-      of rsemDrnimCannotProveLeq, rsemDrnimCannotPorveGe:
-        drnimExpressions*: tuple[a, b: PNode]
+
+      of rsemStaticIndexLeqUnprovable, rsemStaticIndexGeProvable:
+        rangeExpression*: tuple[a, b: PNode]
 
       of rsemExprHasNoAddress:
         isUnsafeAddr*: bool

compiler/ast/trees.nim

@@ -160,12 +160,6 @@ proc effectSpec*(n: PNode, effectType: TSpecialWord): PNode =
         result.add(it[1])
       return
 
-proc propSpec*(n: PNode, effectType: TSpecialWord): PNode =
-  for i in 0..<n.len:
-    var it = n[i]
-    if it.kind == nkExprColonExpr and whichPragma(it) == effectType:
-      return it[1]
-
 proc unnestStmts(n, result: PNode) =
   if n.kind == nkStmtList:
     for x in items(n): unnestStmts(x, result)

compiler/ast/wordrecg.nim

@@ -70,8 +70,7 @@ type
     wSinkInference = "sinkInference", wWarnings = "warnings",
     wHints = "hints", wOptimization = "optimization", wRaises = "raises",
     wWrites = "writes", wReads = "reads", wSize = "size", wEffects = "effects", wTags = "tags",
-    wRequires = "requires", wEnsures = "ensures", wInvariant = "invariant",
-    wAssume = "assume", wAssert = "assert",
+    wAssert = "assert",
     wDeadCodeElimUnused = "deadCodeElim",  # deprecated, dead code elim always happens
     wSafecode = "safecode", wPackage = "package", wNoForward = "noforward", wReorder = "reorder",
     wNoRewrite = "norewrite", wNoDestroy = "nodestroy", wPragma = "pragma",

compiler/front/cli_reporter.nim

@@ -2163,14 +2163,13 @@ proc reportBody*(conf: ConfigRef, r: SemReport): string =
     of rsemErrGcUnsafe:
       result = r.ast.render & " is not GC safe"
 
-    of rsemDrnimCannotPorveGe:
-      assert false, "TODO"
+    of rsemStaticIndexLeqUnprovable:
+      let (a, b) = r.rangeExpression
+      result = "cannot prove: " & $a & " <= " & $b
 
-    of rsemDrnimCannotProveLeq:
-      assert false, "TODO"
-
-    of rsemDrNimRequiresUsesMissingResult:
-      assert false, "TODO"
+    of rsemStaticIndexGeProvable:
+      let (a, b) = r.rangeExpression
+      result = "can prove: " & $a & " > " & $b
 
     of rsemInvalidGuardField:
       result = "invalid guard field: " & r.symstr

compiler/modules/modulegraphs.nim

@@ -449,9 +449,8 @@ proc registerModule*(g: ModuleGraph; m: PSym) =
 proc registerModuleById*(g: ModuleGraph; m: FileIndex) =
   registerModule(g, g.packed[int m].module)
 
-proc initOperators*(g: ModuleGraph): Operators =
+proc initOperators(g: ModuleGraph): Operators =
   # These are safe for IC.
-  # Public because it's used by DrNim.
   result.opLe = createMagic(g, "<=", mLeI)
   result.opLt = createMagic(g, "<", mLtI)
   result.opAnd = createMagic(g, "and", mAnd)

compiler/sem/guards.nim

@@ -474,30 +474,6 @@ proc hasSubTree(n, x: PNode): bool =
       for i in 0..<n.len:
         if hasSubTree(n[i], x): return true
 
-proc invalidateFacts*(s: var seq[PNode], n: PNode) =
-  # We are able to guard local vars (as opposed to 'let' variables)!
-  # 'while p != nil: f(p); p = p.next'
-  # This is actually quite easy to do:
-  # Re-assignments (incl. pass to a 'var' param) trigger an invalidation
-  # of every fact that contains 'v'.
-  #
-  #   if x < 4:
-  #     if y < 5
-  #       x = unknown()
-  #       # we invalidate 'x' here but it's known that x >= 4
-  #       # for the else anyway
-  #   else:
-  #     echo x
-  #
-  # The same mechanism could be used for more complex data stored on the heap;
-  # procs that 'write: []' cannot invalidate 'n.kind' for instance. In fact, we
-  # could CSE these expressions then and help C's optimizer.
-  for i in 0..high(s):
-    if s[i] != nil and s[i].hasSubTree(n): s[i] = nil
-
-proc invalidateFacts*(m: var TModel, n: PNode) =
-  invalidateFacts(m.s, n)
-
 proc valuesUnequal(a, b: PNode): bool =
   if a.isValue and b.isValue:
     result = not sameValue(a, b)

compiler/sem/pragmas.nim

@@ -67,7 +67,7 @@ const
     wAsmNoStackFrame, wDiscardable, wNoInit, wCodegenDecl,
     wGensym, wInject, wRaises, wEffectsOf, wTags, wLocks, wDelegator, wGcSafe,
     wConstructor, wLiftLocals, wStackTrace, wLineTrace, wNoDestroy,
-    wRequires, wEnsures, wEnforceNoRaises}
+    wEnforceNoRaises}
   converterPragmas* = procPragmas
   methodPragmas* = procPragmas+{wBase}-{wImportCpp}
   templatePragmas* = {wDeprecated, wError, wGensym, wInject, wDirty,
@@ -78,7 +78,7 @@ const
   iteratorPragmas* = declPragmas + {FirstCallConv..LastCallConv, wNoSideEffect, wSideEffect,
     wMagic, wBorrow,
     wDiscardable, wGensym, wInject, wRaises, wEffectsOf,
-    wTags, wLocks, wGcSafe, wRequires, wEnsures}
+    wTags, wLocks, wGcSafe}
   exprPragmas* = {wLine, wLocks, wNoRewrite, wGcSafe, wNoSideEffect}
   stmtPragmas* = {wChecks, wObjChecks, wFieldChecks, wRangeChecks,
     wBoundChecks, wOverflowChecks, wNilChecks, wStaticBoundchecks,
@@ -91,11 +91,11 @@ const
     wDeprecated,
     wFloatChecks, wInfChecks, wNanChecks, wPragma, wEmit, wUnroll,
     wLinearScanEnd, wPatterns, wTrMacros, wEffects, wNoForward, wReorder, wComputedGoto,
-    wExperimental, wThis, wUsed, wInvariant, wAssume, wAssert}
+    wExperimental, wThis, wUsed, wAssert}
   lambdaPragmas* = {FirstCallConv..LastCallConv,
     wNoSideEffect, wSideEffect, wNoreturn, wNosinks, wDynlib, wHeader,
     wThread, wAsmNoStackFrame,
-    wRaises, wLocks, wTags, wRequires, wEnsures, wEffectsOf,
+    wRaises, wLocks, wTags, wEffectsOf,
     wGcSafe, wCodegenDecl, wNoInit, wCompileTime}
   typePragmas* = declPragmas + {wMagic, wAcyclic,
     wPure, wHeader, wCompilerProc, wCore, wFinal, wSize, wShallow,
@@ -115,8 +115,7 @@ const
   paramPragmas* = {wNoalias, wInject, wGensym}
   letPragmas* = varPragmas
   procTypePragmas* = {FirstCallConv..LastCallConv, wVarargs, wNoSideEffect,
-                      wThread, wRaises, wEffectsOf, wLocks, wTags, wGcSafe,
-                      wRequires, wEnsures}
+                      wThread, wRaises, wEffectsOf, wLocks, wTags, wGcSafe}
   forVarPragmas* = {wInject, wGensym}
   allRoutinePragmas* = methodPragmas + iteratorPragmas + lambdaPragmas
   enumFieldPragmas* = {wDeprecated}
@@ -158,45 +157,6 @@ proc newIllegalCustomPragmaNode*(c: PContext; n: PNode, s: PSym): PNode =
     n.info
   )
 
-proc pragmaProposition(c: PContext, n: PNode): PNode =
-  ## drnim - `ensures` pragma,  must be a callable with single arg predicate,
-  ## producing either:
-  ## 1. mutated `n` with the the proposition (2nd child) semantically checked
-  ##    analysed
-  ## 2. nkError node over `n`, when a callable unary proposition isn't provided
-  if n.kind notin nkPragmaCallKinds or n.len != 2:
-    result = c.config.newError(n, SemReport(kind: rsemPropositionExpected))
-  else:
-    n[1] = c.semExpr(c, n[1])
-
-proc pragmaEnsures(c: PContext, n: PNode): PNode =
-  ## drnim - `ensures` pragma, must be a callable with single arg predicate,
-  ## producing either:
-  ## 1. mutated `n` with the the proposition (2nd child) semantically checked
-  ##    analysed, and if the current owner is a routineKind adds a `result`
-  ##    symbol.
-  ## 2. nkError node over `n`, when a callable unary proposition isn't provided
-  ##
-  ## xxx: 1. the implementation is unclear, we create a `result` symbol for
-  ##      routines, adding it to the a sub-scope with the routine as owner, but
-  ##      won't that potentially create a duplicate `result` symbol? or does
-  ##      that get resolved later?
-  ##      2. `routineKinds` includes template, so is that potentially an issue
-  ##      as well?
-  result = n
-  if n.kind notin nkPragmaCallKinds or n.len != 2:
-    result = c.config.newError(n, SemReport(kind: rsemPropositionExpected))
-  else:
-    openScope(c)
-    let o = getCurrOwner(c)
-    if o.kind in routineKinds and o.typ != nil and o.typ.sons[0] != nil:
-      var s = newSym(skResult, getIdent(c.cache, "result"), nextSymId(c.idgen), o, n.info)
-      s.typ = o.typ.sons[0]
-      incl(s.flags, sfUsed)
-      addDecl(c, s)
-    n[1] = c.semExpr(c, n[1])
-    closeScope(c)
-
 proc pragmaAsm*(c: PContext, n: PNode): char =
   result = '\0'
   if n != nil:
@@ -1879,10 +1839,6 @@ proc prepareSinglePragma(
           sym.flags.incl sfUsed
       of wLiftLocals:
         result = it
-      of wRequires, wInvariant, wAssume, wAssert:
-        result = pragmaProposition(c, it)
-      of wEnsures:
-        result = pragmaEnsures(c, it)
       of wEnforceNoRaises:
         sym.flags.incl sfNeverRaises
       else:

compiler/sem/semmagic.nim

@@ -431,45 +431,6 @@ proc turnFinalizerIntoDestructor(c: PContext; orig: PSym; info: TLineInfo): PSym
   result.typ = newProcType(result.info, nextTypeId c.idgen, result)
   result.typ.addParam newParam
 
-proc semQuantifier(c: PContext; n: PNode): PNode =
-  checkSonsLen(n, 2, c.config)
-  openScope(c)
-  result = newNodeIT(n.kind, n.info, n.typ)
-  result.add n[0]
-  let args = n[1]
-  assert args.kind == nkArgList
-  for i in 0..args.len-2:
-    let it = args[i]
-    var valid = false
-    if it.kind == nkInfix:
-      let op = considerQuotedIdent(c, it[0])
-      if op.id == ord(wIn):
-        let v = newSymS(skForVar, it[1], c)
-        styleCheckDef(c.config, v)
-        onDef(it[1].info, v)
-        let domain = semExprWithType(c, it[2], {efWantIterator})
-        v.typ = domain.typ
-        valid = true
-        addDecl(c, v)
-        result.add newTree(nkInfix, it[0], newSymNode(v), domain)
-    if not valid:
-      localReport(c.config, n, reportSem rsemQuantifierInRangeExpected)
-  result.add forceBool(c, semExprWithType(c, args[^1]))
-  closeScope(c)
-
-proc semOld(c: PContext; n: PNode): PNode =
-  if n[1].kind == nkHiddenDeref:
-    n[1] = n[1][0]
-
-  if n[1].kind != nkSym or n[1].sym.kind != skParam:
-    localReport(c.config, n[1], reportSem rsemOldTakesParameterName)
-
-  elif n[1].sym.owner != getCurrOwner(c):
-    localReport(c.config, n[1].info, reportAst(
-      rsemOldDoesNotBelongTo, n[1], sym = getCurrOwner(c)))
-
-  result = n
-
 proc semPrivateAccess(c: PContext, n: PNode): PNode =
   let t = n[1].typ[0].toObjectFromRefPtrGeneric
   c.currentScope.allowPrivateAccess.add t.sym
@@ -574,10 +535,6 @@ proc magicsAfterOverloadResolution(c: PContext, n: PNode,
       result[0] = newSymNode(op)
   of mUnown:
     result = semUnown(c, n)
-  of mExists, mForall:
-    result = semQuantifier(c, n)
-  of mOld:
-    result = semOld(c, n)
   of mSetLengthSeq:
     result = n
     let seqType = result[1].typ.skipTypes({tyPtr, tyRef, # in case we had auto-dereferencing

compiler/sem/semparallel.nim

@@ -373,7 +373,6 @@ proc analyse(c: var AnalysisCtx; n: PNode) =
       # prevent direct assignments to the monotonic variable:
       let slot = c.getSlot(n[0].sym)
       slot.blacklisted = true
-    invalidateFacts(c.guards, n[0])
     let value = n[1]
     if getMagic(value) == mSpawn:
       pushSpawnId(c):