From 61b4659b7bcbf2c61b09db8370487b6f78403701 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Tue, 1 Feb 2022 13:25:06 -0800 Subject: [PATCH] fix: look at resolutions when translating names (closes #97) --- Mathport/Bridge/Rename.lean | 22 ++- Mathport/Syntax/AST3.lean | 4 +- Mathport/Syntax/Parse.lean | 148 +++++++++++--------- Mathport/Syntax/Translate/Basic.lean | 14 +- Mathport/Syntax/Translate/Tactic/Lean3.lean | 4 +- 5 files changed, 113 insertions(+), 79 deletions(-) diff --git a/Mathport/Bridge/Rename.lean b/Mathport/Bridge/Rename.lean index 33a72b862..ee52688b2 100644 --- a/Mathport/Bridge/Rename.lean +++ b/Mathport/Bridge/Rename.lean @@ -46,12 +46,26 @@ namespace Rename variable (env : Environment) -- For both binport and synport -def resolveIdent? (n3 : Name) : Option Name := - getRenameMap env |>.find? n3 +def resolveIdent? (n3 : Name) (choices : Array Name := #[]) : Option Name := + if choices.isEmpty then + getRenameMap env |>.find? n3 + else + match getRenameMap env |>.find? choices[0] with + | none => none + | some target => clipLike target n3 +where + clipLike target n3 := + some <| componentsToName <| target.components.drop (target.getNumParts - n3.getNumParts) + + componentsToName + | [] => Name.anonymous + | (c::cs) => c ++ componentsToName cs + +#check resolveIdent? -- For both binport and synport -def resolveIdent! (n3 : Name) : Name := - resolveIdent? env n3 |>.getD n3 +def resolveIdent! (n3 : Name) (choices : Array Name := #[]) : Name := + resolveIdent? env n3 choices |>.getD n3 -- For synport only -- TODO: better heuristic/binport index? diff --git a/Mathport/Syntax/AST3.lean b/Mathport/Syntax/AST3.lean index 1d3c1695a..17662eb94 100644 --- a/Mathport/Syntax/AST3.lean +++ b/Mathport/Syntax/AST3.lean @@ -320,7 +320,7 @@ mutual | «()» : Expr | «{}» : Expr | ident : Name → Expr - | const (ambiguous : Bool) : #Name → Levels → Expr + | const : #Name → Levels → Array Name → Expr | nat : Nat → Expr | decimal : Nat → Nat → Expr | string : String → Expr @@ -690,7 +690,7 @@ mutual | Expr.«()», _ => "()" | Expr.«{}», _ => "{}" | Expr.ident n, _ => n.toString - | Expr.const _ n l, _ => n.kind.toString ++ repr l + | Expr.const n l _, _ => n.kind.toString ++ repr l | Expr.nat n, _ => repr n | Expr.decimal n d, _ => repr n ++ "/" ++ repr d | Expr.string s, _ => repr s diff --git a/Mathport/Syntax/Parse.lean b/Mathport/Syntax/Parse.lean index 8a847f9ba..99b464620 100644 --- a/Mathport/Syntax/Parse.lean +++ b/Mathport/Syntax/Parse.lean @@ -106,6 +106,10 @@ def withNode (f : String → Name → Array AstId → M α) (i : AstId) : M (Spa let r ← getRaw i pure { meta := ⟨i, r.start, r.end'⟩, kind := ← f r.kind r.value r.children' } +def withNodeP (f : String → Name → Array AstId → Option ExprId → M α) (i : AstId) : M (Spanned α) := do + let r ← getRaw i + pure { meta := ⟨i, r.start, r.end'⟩, kind := ← f r.kind r.value r.children' r.pexpr } + def withNodeR (f : RawNode3 → M α) (i : AstId) : M (Spanned α) := do let r ← getRaw i pure { meta := ⟨i, r.start, r.end'⟩, kind := ← f r } @@ -295,79 +299,95 @@ mutual | "binders", _, args => Arg.binders <$> args.mapM getBinder | k, v, args => if k.startsWith "binder" then Arg.binder <$> getBinder_aux k v args - else Arg.expr <$> getExpr_aux k v args + else Arg.expr <$> getExpr_aux k v args none - partial def getExpr_aux : String → Name → Array AstId → M Expr - | "notation", v, args => match v with + partial def getExpr_aux : String → Name → Array AstId → Option ExprId → M Expr + | "notation", v, args, _ => match v with | `«->» => do Expr.«→» (← getExpr args[0]) (← getExpr args[1]) | `Pi => do Expr.«Pi» (← getBinders args[0]) (← getExpr args[1]) | _ => if wrapperNotations.contains v then Spanned.kind <$> getExpr args[0] else Expr.notation (Choice.one v) <$> args.mapM getArg - | "sorry", _, _ => Expr.«sorry» - | "_", _, _ => Expr.«_» - | "()", _, _ => Expr.«()» - | "{}", _, _ => Expr.«{}» - | "ident", v, _ => Expr.ident v - | "const", _, #[n, us] => do Expr.const false (← getName n) (← opt (arr getLevel) us) - | "choice_const", _, #[n, us] => do Expr.const true (← getName n) (← opt (arr getLevel) us) - | "nat", v, _ => Expr.nat $ decodeNat! v - | "decimal", v, _ => let (n, d) := decodeDecimal! v; Expr.decimal n d - | "string", v, _ => Expr.string v.getString! - | "char", v, _ => Expr.char v.getString!.front - | "(", _, #[e] => Expr.paren <$> getExpr e - | "Sort*", _, _ => Expr.sort false true none - | "Type*", _, _ => Expr.sort true true none - | "Sort", _, #[l] => Expr.sort false false <$> opt getLevel l - | "Type", _, #[l] => Expr.sort true false <$> opt getLevel l - | "app", _, #[f, x] => do Expr.app (← getExpr f) (← getExpr x) - | "fun", _, #[bis, e] => do Expr.fun false (← arr getLambdaBinder bis) (← getExpr e) - | "assume", _, #[bis, e] => do Expr.fun true (← arr getLambdaBinder bis) (← getExpr e) - | "show", _, #[ty, e] => do Expr.show (← getExpr ty) (← getProof e) - | "have", _, args => getHave false args - | "suffices", _, args => getHave true args - | "field", _, #[e, pr] => do Expr.«.» true (← getExpr e) (← getProj pr) - | "^.", _, #[e, pr] => do Expr.«.» false (← getExpr e) (← getProj pr) - | "if", _, #[h, c, t, e] => do + | "sorry", _, _, _ => Expr.«sorry» + | "_", _, _, _ => Expr.«_» + | "()", _, _, _ => Expr.«()» + | "{}", _, _, _ => Expr.«{}» + | "ident", v, _, _ => Expr.ident v + | "const", _, #[n, us], none => do Expr.const (← getName n) (← opt (arr getLevel) us) #[] + | "const", _, #[n, us], some pexprId => do + match (← read).expr[pexprId] with + | Lean3.Expr.const resolved _ => Expr.const (← getName n) (← opt (arr getLevel) us) #[resolved] + | pexpr => throw s!"[const.pexpr] not a const: {repr pexpr}" + + | "choice_const", _, #[n, us], none => do + dbg_trace "[getExpr_aux.warn] choice_const {(← getName n).kind} has no choices" + Expr.const (← getName n) (← opt (arr getLevel) us) #[] + | "choice_const", _, #[n, us], some pexprId => do + match (← read).expr[pexprId] with + | Lean3.Expr.choice args => + let choices ← args.mapM fun + | Lean3.Expr.const n _ => n + | choice => do throw s!"[getExpr_aux.error] choice_const {(← getName n).kind} expecting constants, found {repr choice}" + Expr.const (← getName n) (← opt (arr getLevel) us) choices + | _ => throw s!"choice_const: expecting choice" + + | "nat", v, _, _ => Expr.nat $ decodeNat! v + | "decimal", v, _, _ => let (n, d) := decodeDecimal! v; Expr.decimal n d + | "string", v, _, _ => Expr.string v.getString! + | "char", v, _, _ => Expr.char v.getString!.front + | "(", _, #[e], _ => Expr.paren <$> getExpr e + | "Sort*", _, _, _ => Expr.sort false true none + | "Type*", _, _, _ => Expr.sort true true none + | "Sort", _, #[l], _ => Expr.sort false false <$> opt getLevel l + | "Type", _, #[l], _ => Expr.sort true false <$> opt getLevel l + | "app", _, #[f, x], _ => do Expr.app (← getExpr f) (← getExpr x) + | "fun", _, #[bis, e], _ => do Expr.fun false (← arr getLambdaBinder bis) (← getExpr e) + | "assume", _, #[bis, e], _ => do Expr.fun true (← arr getLambdaBinder bis) (← getExpr e) + | "show", _, #[ty, e], _ => do Expr.show (← getExpr ty) (← getProof e) + | "have", _, args, _ => getHave false args + | "suffices", _, args, _ => getHave true args + | "field", _, #[e, pr], _ => do Expr.«.» true (← getExpr e) (← getProj pr) + | "^.", _, #[e, pr], _ => do Expr.«.» false (← getExpr e) (← getProj pr) + | "if", _, #[h, c, t, e], _ => do Expr.if (← opt getName h) (← getExpr c) (← getExpr t) (← getExpr e) - | "calc", _, args => Expr.calc <$> args.mapM getStep - | "@", _, #[e] => Expr.«@» false <$> getExpr e - | "@@", _, #[e] => Expr.«@» true <$> getExpr e - | "(:", _, #[e] => Expr.pattern <$> getExpr e - | "```()", _, #[e] => Expr.«`()» true false <$> getExpr e - | "``()", _, #[e] => Expr.«`()» false false <$> getExpr e - | "`()", _, #[e] => Expr.«`()» false true <$> getExpr e - | "%%", _, #[e] => Expr.«%%» <$> getExpr e - | "`[", _, args => Expr.«`[]» <$> args.mapM getTactic - | "`", v, _ => Expr.«`» false v - | "``", v, _ => Expr.«`» true v - | "⟨", _, args => Expr.«⟨⟩» <$> args.mapM getExpr - | "infix_fn", _, #[f, e] => do Expr.infix_fn (← getChoice f) (← opt getExpr e) - | "tuple", _, args => Expr.«(,)» <$> args.mapM getExpr - | ":", _, #[e, ty] => do Expr.«:» (← getExpr e) (← getExpr ty) - | "{!", _, args => Expr.hole <$> args.mapM getExpr - | "#[", _, args => Expr.«#[]» <$> args.mapM getExpr - | "by", _, #[tac] => Expr.by <$> getTactic tac - | "begin", _, args => Expr.begin <$> getBlock false args - | "let", _, #[decls, e] => do Expr.let (← arr getLetDecl decls) (← getExpr e) - | "match", _, #[e, ty, arms] => do + | "calc", _, args, _ => Expr.calc <$> args.mapM getStep + | "@", _, #[e], _ => Expr.«@» false <$> getExpr e + | "@@", _, #[e], _ => Expr.«@» true <$> getExpr e + | "(:", _, #[e], _ => Expr.pattern <$> getExpr e + | "```()", _, #[e], _ => Expr.«`()» true false <$> getExpr e + | "``()", _, #[e], _ => Expr.«`()» false false <$> getExpr e + | "`()", _, #[e], _ => Expr.«`()» false true <$> getExpr e + | "%%", _, #[e], _ => Expr.«%%» <$> getExpr e + | "`[", _, args, _ => Expr.«`[]» <$> args.mapM getTactic + | "`", v, _, _ => Expr.«`» false v + | "``", v, _, _ => Expr.«`» true v + | "⟨", _, args, _ => Expr.«⟨⟩» <$> args.mapM getExpr + | "infix_fn", _, #[f, e], _ => do Expr.infix_fn (← getChoice f) (← opt getExpr e) + | "tuple", _, args, _ => Expr.«(,)» <$> args.mapM getExpr + | ":", _, #[e, ty], _ => do Expr.«:» (← getExpr e) (← getExpr ty) + | "{!", _, args, _ => Expr.hole <$> args.mapM getExpr + | "#[", _, args, _ => Expr.«#[]» <$> args.mapM getExpr + | "by", _, #[tac], _ => Expr.by <$> getTactic tac + | "begin", _, args, _ => Expr.begin <$> getBlock false args + | "let", _, #[decls, e], _ => do Expr.let (← arr getLetDecl decls) (← getExpr e) + | "match", _, #[e, ty, arms], _ => do Expr.match (← arr getExpr e) (← opt getExpr ty) (← arr getArm arms) - | "do", v, args => Expr.do (!v.isAnonymous) <$> args.mapM getDoElem - | "fin_set", _, args => Expr.«{,}» <$> args.mapM getExpr - | "subtype", _, args => getSubtype false args - | "set_of", _, args => getSubtype true args - | "sep", _, #[x, S, p] => do Expr.sep (← getName x) (← getExpr S) (← getExpr p) - | "set_replacement", _, #[e, bis] => do Expr.setReplacement (← getExpr e) (← getBinders bis) - | "structinst", _, #[S, src, flds, srcs, catchall] => do + | "do", v, args, _ => Expr.do (!v.isAnonymous) <$> args.mapM getDoElem + | "fin_set", _, args, _ => Expr.«{,}» <$> args.mapM getExpr + | "subtype", _, args, _ => getSubtype false args + | "set_of", _, args, _ => getSubtype true args + | "sep", _, #[x, S, p], _ => do Expr.sep (← getName x) (← getExpr S) (← getExpr p) + | "set_replacement", _, #[e, bis], _ => do Expr.setReplacement (← getExpr e) (← getBinders bis) + | "structinst", _, #[S, src, flds, srcs, catchall], _ => do Expr.structInst (← opt getName S) (← opt getExpr src) (← arr getField flds) (← arr getExpr srcs) (catchall ≠ 0) - | "at_pat", _, #[n, pat] => do Expr.atPat (← getName n) (← getExpr pat) - | ".(", _, #[e] => Expr.«.()» <$> getExpr e - | "...", _, _ => Expr.«...» - | "choice", _, args => do + | "at_pat", _, #[n, pat], _ => do Expr.atPat (← getName n) (← getExpr pat) + | ".(", _, #[e], _ => Expr.«.()» <$> getExpr e + | "...", _, _, _ => Expr.«...» + | "choice", _, args, _ => do Expr.notation (Choice.many (← arr getNameK args[0])) (← args[1:].toArray.mapM getArg) - | "user_notation", v, args => Expr.userNotation v <$> args.mapM getParam - | k, v, args => do + | "user_notation", v, args, _ => Expr.userNotation v <$> args.mapM getParam + | k, v, args, _ => do throw s!"getExpr parse error, unknown kind {k}" -- at\n {repr (← Expr.other <$> mkNodeK k v args)}" where getHave (suff : Bool) (args) : M _ := do @@ -378,7 +398,7 @@ mutual getSubtype (setOf : Bool) (args) : M _ := do Expr.subtype setOf (← getName args[0]) (← opt getExpr args[1]) (← getExpr args[2]) - partial def getExpr : AstId → M (Spanned Expr) := withNode getExpr_aux + partial def getExpr : AstId → M (Spanned Expr) := withNodeP getExpr_aux partial def getArm : AstId → M Arm := withNodeK fun _ _ args => do pure ⟨← arr getExpr args[0], ← getExpr args[1]⟩ @@ -528,7 +548,7 @@ open DeclVal in def getDeclVal : AstId → M (Spanned DeclVal) := withNode fun | "eqns", _, args => eqns <$> args.mapM getArm - | k, v, args => expr <$> getExpr_aux k v args + | k, v, args => expr <$> getExpr_aux k v args none open Modifier in def getModifier : AstId → M (Spanned Modifier) := withNode fun diff --git a/Mathport/Syntax/Translate/Basic.lean b/Mathport/Syntax/Translate/Basic.lean index 83439115f..ddaf65a12 100644 --- a/Mathport/Syntax/Translate/Basic.lean +++ b/Mathport/Syntax/Translate/Basic.lean @@ -160,7 +160,7 @@ elab:max "warn!" interpStr:interpolatedStr(term) or:(checkColGt "|" term)? : ter def trExpr (e : Expr) : M Syntax := do (← read).trExpr e def trCommand (e : Command) : M Unit := do (← read).trCommand e -def renameIdent (n : Name) : M Name := do Rename.resolveIdent! (← getEnv) n +def renameIdent (n : Name) (choices : Array Name := #[]) : M Name := do Rename.resolveIdent! (← getEnv) n choices def renameNamespace (n : Name) : M Name := do Rename.renameNamespace (← getEnv) n def renameAttr (n : Name) : M Name := do Rename.renameAttr n def renameModule (n : Name) : M Name := do Rename.renameModule (← read).pcfg n @@ -168,7 +168,7 @@ def renameField (n : Name) : M Name := do Rename.renameField? (← getEnv) n |>. def renameOption : Name → M Name | n => warn! "warning: unsupported option {n}" | n -def mkIdentI (n : Name) : M Syntax := do mkIdent (← renameIdent n) +def mkIdentI (n : Name) (choices : Array Name := #[]) : M Syntax := do mkIdent (← renameIdent n choices) def mkIdentA (n : Name) : M Syntax := do mkIdent (← renameAttr n) def mkIdentN (n : Name) : M Syntax := do mkIdent (← renameNamespace n) def mkIdentF (n : Name) : M Syntax := do mkIdent (← renameField n) @@ -727,10 +727,10 @@ def trExpr' : Expr → M Syntax | Expr.«()» => `(()) | Expr.«{}» => `({}) | Expr.ident n => mkIdentI n - | Expr.const _ n none => mkIdentI n.kind - | Expr.const _ n (some #[]) => mkIdentI n.kind - | Expr.const _ n (some l) => do - mkNode ``Parser.Term.explicitUniv #[← mkIdentI n.kind, + | Expr.const n none choices => mkIdentI n.kind choices + | Expr.const n (some #[]) choices => mkIdentI n.kind choices + | Expr.const n (some l) choices => do + mkNode ``Parser.Term.explicitUniv #[← mkIdentI n.kind choices, mkAtom ".{", (mkAtom ",").mkSep $ ← l.mapM fun e => trLevel e.kind, mkAtom "}"] | Expr.nat n => Quote.quote n | Expr.decimal n d => (scientificLitOfDecimal n d).get! @@ -853,7 +853,7 @@ def mkSimpleAttr (n : Name) (args : Array Syntax := #[]) := def trDerive (e : AST3.Expr) : M Name := match e.unparen with | Expr.ident n => renameIdent n - | Expr.const _ ⟨_, n⟩ _ => renameIdent n + | Expr.const ⟨_, n⟩ _ choices => renameIdent n choices | e => warn! "unsupported derive handler {repr e}" inductive TrAttr diff --git a/Mathport/Syntax/Translate/Tactic/Lean3.lean b/Mathport/Syntax/Translate/Tactic/Lean3.lean index 7c11b8af0..3691329b1 100644 --- a/Mathport/Syntax/Translate/Tactic/Lean3.lean +++ b/Mathport/Syntax/Translate/Tactic/Lean3.lean @@ -313,8 +313,8 @@ def parseSimpConfig : Option AST3.Expr → M (Option Meta.Simp.Config × Syntax) | some _ => warn! "warning: unsupported simp config syntax" | (none, mkNullNode) where asBool {α} : AST3.Expr → α → (α → Bool → α) → α - | AST3.Expr.const _ ⟨_, `tt⟩ _, a, f => f a true - | AST3.Expr.const _ ⟨_, `ff⟩ _, a, f => f a false + | AST3.Expr.const ⟨_, `tt⟩ _ _, a, f => f a true + | AST3.Expr.const ⟨_, `ff⟩ _ _, a, f => f a false | _, a, _ => a def quoteSimpConfig (cfg : Meta.Simp.Config) : Option Syntax := Id.run do