From e4b478ee6a36c8274aeaf4685b9729fd46d4b93f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 26 Oct 2020 07:35:26 -0700 Subject: [PATCH] chore: remove support for quotations in the old frontend --- src/Lean/Elab/Quotation.lean | 135 ----------------------------------- 1 file changed, 135 deletions(-) diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index 8fe6cefac4..6b9b43eefe 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/src/Lean/Elab/Quotation.lean @@ -312,139 +312,4 @@ compileStxMatch [discr] alts.toList @[builtinTermElab «match_syntax»] def elabMatchSyntax : TermElab := adaptExpander match_syntax.expand --- REMOVE with old frontend -private def exprPlaceholder := mkMVar Name.anonymous - -private unsafe def toPreterm : Syntax → TermElabM Expr -| stx => withRef stx $ - match stx.getKind with - | `ident => - match stx with - | Syntax.ident _ _ val preresolved => do - let resolved ← resolveName val preresolved []; - match resolved with - | (pre,projs)::_ => - let pre := match pre with - | Expr.const c _ _ => Lean.mkConst c -- remove universes confusing the old frontend - | _ => pre; - let projs := projs.map mkNameSimple; - pure $ projs.foldl (fun e proj => mkMData (MData.empty.setName `fieldNotation proj) e) pre - | [] => unreachable! - | _ => unreachable! - | `Lean.Parser.Term.fun => do - let params := (stx.getArg 1).getArgs; - let body := stx.getArg 3; - if params.size == 0 then toPreterm body - else - let param := params.get! 0; - let (n, ty) ← - if param.isIdent then - pure (param.getId, exprPlaceholder) - else if param.isOfKind `Lean.Parser.Term.hole then - pure (`_a, exprPlaceholder) - else - let n := ((param.getArg 1).getArg 0).getId; - let ty ← toPreterm $ (((param.getArg 1).getArg 1).getArg 0).getArg 1; - pure (n, ty) - let lctx ← getLCtx; - let lctx := lctx.mkLocalDecl n n ty; - let params := params.eraseIdx 0; - let stx ← `(fun $params* => $body); - withTheReader Meta.Context (fun ctx => { ctx with lctx := lctx }) $ do - let e ← toPreterm stx; - pure $ lctx.mkLambda #[mkFVar n] e - | `Lean.Parser.Term.let => do - let decl := (stx.getArg 1).getArg 0; - let n := decl.getIdAt 0; - let val := decl.getArg 4; - let body := stx.getArg 3; - let val ← toPreterm val; - let lctx ← getLCtx; - let lctx := lctx.mkLetDecl n n exprPlaceholder val; - withTheReader Meta.Context (fun ctx => { ctx with lctx := lctx }) $ do - let e ← toPreterm $ body; - pure $ lctx.mkLambda #[mkFVar n] e - | `Lean.Parser.Term.app => do - let fn ← toPreterm $ stx.getArg 0; - let as ← (stx.getArg 1).getArgs.mapM toPreterm; - pure $ mkAppN fn as - | `Lean.Parser.Term.if => do - let con := stx.getArg 2; - let yes := stx.getArg 4; - let no := stx.getArg 6; - toPreterm $ Unhygienic.run `(ite $con $yes $no) - | `Lean.Parser.Term.paren => - let inner := (stx.getArg 1).getArgs; - if inner.size == 0 then pure $ Lean.mkConst `Unit.unit - else toPreterm $ inner.get! 0 - | `Lean.Parser.Term.band => - let lhs := stx.getArg 0; let rhs := stx.getArg 2; - toPreterm $ Unhygienic.run `(and $lhs $rhs) - | `Lean.Parser.Term.beq => - let lhs := stx.getArg 0; let rhs := stx.getArg 2; - toPreterm $ Unhygienic.run `(HasBeq.beq $lhs $rhs) - | `Lean.Parser.Term.eq => - let lhs := stx.getArg 0; let rhs := stx.getArg 2; - toPreterm $ Unhygienic.run `(Eq $lhs $rhs) - | `strLit => pure $ mkStrLit $ stx.isStrLit?.getD "" - | `numLit => pure $ mkNatLit $ stx.isNatLit?.getD 0 - | `expr => pure $ unsafeCast $ stx.getArg 0 -- HACK: see below - | k => throwError $ "stxQuot: unimplemented kind " ++ toString k - -@[export lean_parse_expr] -def oldParseExpr (env : Environment) (input : String) (pos : String.Pos) : Except String (Syntax × String.Pos) := do -let c := Parser.mkParserContext env (Parser.mkInputContext input ""); -let s := Parser.mkParserState c.input; -let s := s.setPos pos; -let s := (Parser.termParser Parser.maxPrec : Parser.Parser).fn { c with prec := Parser.maxPrec } s; -let stx := s.stxStack.back; -match s.errorMsg with -| some errorMsg => - Except.error $ toString errorMsg -| none => - Except.ok (stx, s.pos) - -structure OldContext := -(env : Environment) -(locals : List Name) -(open_nss : List Name) - -private unsafe def oldRunTermElabMUnsafe {α} (oldCtx : OldContext) (x : TermElabM α) : Except String α := do -let ctxMeta : Meta.Context := { - lctx := oldCtx.locals.foldl (fun lctx l => LocalContext.mkLocalDecl lctx l l exprPlaceholder) $ LocalContext.mkEmpty () -}; -let ctxTerm : Term.Context := { - fileName := "foo", - fileMap := FileMap.ofString "", - currNamespace := Lean.TODELETE.getNamespace oldCtx.env, - openDecls := oldCtx.open_nss.map $ fun n => OpenDecl.simple n [] -}; -match unsafeIO $ x.toIO {} { env := oldCtx.env } ctxMeta {} ctxTerm {} with -| Except.ok (a, _, _, _) => Except.ok a -| Except.error e => Except.error (toString e) - -@[implementedBy oldRunTermElabMUnsafe] -constant oldRunTermElabM {α} (oldCtx : OldContext) (x : TermElabM α) : Except String α := arbitrary _ - -@[export lean_expand_stx_quot] -unsafe def oldExpandStxQuot (ctx : OldContext) (stx : Syntax) : Except String Expr := oldRunTermElabM ctx $ do -let stx ← stxQuot.expand stx; -toPreterm stx - -@[export lean_get_antiquot_vars] -def oldGetPatternVars (ctx : OldContext) (pats : List Syntax) : Except String (List Name) := oldRunTermElabM ctx $ do -let vars := List.join $ pats.map getPatternVars; -pure $ vars.map $ fun var => var.getId - -@[export lean_expand_match_syntax] -unsafe def oldExpandMatchSyntax (ctx : OldContext) (discr : Syntax) (alts : List (List Syntax × Syntax)) : Except String Expr := oldRunTermElabM ctx $ do --- HACK: discr and the RHSs are actually `Expr` -let discr := Syntax.node `expr #[discr]; -let alts := alts.map $ fun alt => - let pats := alt.1.map elimAntiquotChoices; - (pats, Syntax.node `expr #[alt.2]); --- letBindRhss (compileStxMatch Syntax.missing [discr]) alts [] -let stx ← compileStxMatch [discr] alts; -toPreterm stx - end Lean.Elab.Term.Quotation