Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Unquote Definition will normalize the term #1091

Open
WeituoDAI opened this issue Jun 24, 2024 · 0 comments
Open

Unquote Definition will normalize the term #1091

WeituoDAI opened this issue Jun 24, 2024 · 0 comments

Comments

@WeituoDAI
Copy link

WeituoDAI commented Jun 24, 2024

Unquote Definition will normalize the term automatically,
An example:

MetaCoq Quote Definition mytp := (fun (x:nat) => x) 1.
MetaCoq Unquote Definition mytp' := mytp.
Print mytp'.

The output is mytp' = 1 : nat. Not the same as originally defined.
I wonder if this is the expected behavior. I hope that I can get the original definition but not the term after normalization.

The problem possibly comes from tmEval.
When use tmUnquote to the term mytp, I get {| my_projT1 := nat; my_projT2 := (fun x:nat => x) 1 |}.
Then use tmEval cbv/cbn/unfold ... on the term my_projT2 {| my_projT1 := nat; my_projT2 := (fun x:nat => x) 1 |}, we will always beta-reduce the term.

I define my own plugin to get the (non normalized) unquoted term:

Notation "'$let' x ':=' c1 'in' c2" := (@bind _ _ _ _ c1 (fun x => c2))
  (at level 100, c1 at next level, right associativity, x pattern) : monad_scope.
Definition MyDef (a : term) (out : option ident): TemplateMonad unit :=
  $let b := tmUnquote a in
  let ty := my_projT1 b in
  $let r := tmUnquoteTyped ty a in
  match out with
  | Some name => tmDefinitionRed name (Some all) r ;; tmPrint r ;; ret tt
  | None => tmPrint r
  end.

However, this function does unquotation twice.. It will help if there is any better approach to do this. Anyway, I do not think that MetaCoq Unquote Definition should normalize the term.

@WeituoDAI WeituoDAI changed the title tmUnquote will normalize the term (get rid of all tLetIn) tmUnquote will normalize the term Sep 20, 2024
@WeituoDAI WeituoDAI changed the title tmUnquote will normalize the term Unquote Definition will normalize the term Sep 20, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant