chore: remove support for quotations in the old frontend
This commit is contained in:
Leonardo de Moura
parent
7a24fe73ca
commit
e4b478ee6a
1 changed files with 0 additions and 135 deletions
|
|
@ -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 "<foo>");
|
||||
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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue