-
Notifications
You must be signed in to change notification settings - Fork 4
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
William Sørensen
committed
Jul 25, 2024
1 parent
baed8e3
commit d904907
Showing
4 changed files
with
106 additions
and
90 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,65 @@ | ||
| import Qpf.Macro.Data.Replace | ||
| import Qpf.Macro.Data.View | ||
| import Qpf.Macro.NameUtils | ||
|
|
||
| open Lean Meta Elab.Command | ||
| open PrettyPrinter (delab) | ||
|
|
||
| namespace Data.Command | ||
| open Parser in | ||
| /-- | ||
| Count the number of arguments to a constructor | ||
| -/ | ||
| partial def countConstructorArgs : Syntax → Nat | ||
| | Syntax.node _ ``Term.arrow #[_, _, tail] => 1 + (countConstructorArgs tail) | ||
| | _ => 0 | ||
|
|
||
|
|
||
| open Elab | ||
| /-- | ||
| Add convenient constructor functions to the environment | ||
| -/ | ||
| def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do | ||
| for ctor in view.ctors do | ||
| trace[QPF] "mkConstructors\n{ctor.declName} : {ctor.type?}" | ||
| let n_args := (ctor.type?.map countConstructorArgs).getD 0 | ||
|
|
||
| let args ← (List.range n_args).mapM fun _ => | ||
| do pure <| mkIdent <|← Elab.Term.mkFreshBinderName | ||
| let args := args.toArray | ||
|
|
||
| let mk := mkIdent ((DataCommand.fixOrCofix view.command).getId ++ `mk) | ||
| let shapeCtor := mkIdent <| Name.replacePrefix2 view.declName shape ctor.declName | ||
| trace[QPF] "shapeCtor = {shapeCtor}" | ||
|
|
||
|
|
||
|
|
||
| let body := if n_args = 0 then | ||
| `($mk $shapeCtor) | ||
| else | ||
| `(fun $args:ident* => $mk ($shapeCtor $args:ident*)) | ||
| let body ← body | ||
|
|
||
| let explicit ← view.getExplicitExpectedType | ||
| let type : Term := TSyntax.mk <| | ||
| (ctor.type?.map fun type => | ||
| Replace.replaceAllStx view.getExpectedType explicit type | ||
| ).getD explicit | ||
| let modifiers : Modifiers := { | ||
| isNoncomputable := view.modifiers.isNoncomputable | ||
| attrs := #[{ | ||
| name := `matchPattern | ||
| }] | ||
| } | ||
| let declId := mkIdent <| Name.stripPrefix2 (←getCurrNamespace) ctor.declName | ||
|
|
||
| let cmd ← `( | ||
| $(quote modifiers):declModifiers | ||
| def $declId:ident : $type := $body:term | ||
| ) | ||
|
|
||
| trace[QPF] "mkConstructor.cmd = {cmd}" | ||
| elabCommand cmd | ||
| return () | ||
|
|
||
| end Data.Command |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,17 @@ | ||
| open Lean Meta | ||
|
|
||
| namespace Lean.Name | ||
| -- This function has diffreent behaviour from Name.replacePrefix | ||
| def replacePrefix2 (old_pref new_pref : Name) : Name → Name | ||
| | Name.anonymous => Name.anonymous | ||
| | Name.str p s => let p' := if p == old_pref then new_pref | ||
| else replacePrefix2 old_pref new_pref p | ||
| Name.mkStr p' s | ||
| | Name.num p v => let p' := if p == old_pref then new_pref | ||
| else replacePrefix2 old_pref new_pref p | ||
| Name.mkNum p' v | ||
|
|
||
|
|
||
| def stripPrefix2 (old_pref : Name) : Name → Name | ||
| := Name.replacePrefix2 old_pref .anonymous | ||
| end Lean.Name |