Hi,
I would like to extract the non implicit arguments of an application in ltac. Is it possible?
1 Like
I believe it is not possible. I believe implicit status is very early in the pipeline, and by the time you have constrs (or even uconstrs), it is no longer present.
You can extract non-dependent arguments; or arguments that would not be made implicit by Set Implicit Arguments (both of these by parsing the type).
1 Like
Hi Jason, I am interested in extracting the arguments that would be mage implicit by imlicit arguments. How do you do that please? by checking occurrences of variables in types?
Yeah, you basically need to reimplement the algorithm of Set Implicit Arguments in Ltac
For the record I ended up with a very stupid (but quite efficient) hack to detect the number of head implicit arguments. I will maybe try something smarter but this fits my needs for now:
lazymatch th with
| (?z ?a ?b ?c ?d ?e ?f ?g ?h ?i ?j ?k) =>
match th with
| _ => let foo := constr:(z _ _ _ _ _ _ _ _ _ _ k) in constr:(1%nat)
| _ => let foo := constr:(z _ _ _ _ _ _ _ _ _ j k) in constr:(2%nat)
| _ => let foo := constr:(z _ _ _ _ _ _ _ _ i j k) in constr:(3%nat)
| _ => let foo := constr:(z _ _ _ _ _ _ _ h i j k) in constr:(4%nat)
| _ => let foo := constr:(z _ _ _ _ _ _ g h i j k) in constr:(5%nat)
| _ => let foo := constr:(z _ _ _ _ _ f g h i j k) in constr:(6%nat)
| _ => let foo := constr:(z _ _ _ _ e f g h i j k) in constr:(7%nat)
| _ => let foo := constr:(z _ _ _ d e f g h i j k) in constr:(8%nat)
| _ => let foo := constr:(z _ _ c d e f g h i j k) in constr:(9%nat)
| _ => let foo := constr:(z _ b c d e f g h i j k) in constr:(10%nat)
| _ => let foo := constr:(z a b c d e f g h i j k) in constr:(10%nat)
end
| (?z ?b ?c ?d ?e ?f ?g ?h ?i ?j ?k) =>
match th with
| _ => let foo := constr:(z _ _ _ _ _ _ _ _ _ k) in constr:(1%nat)
| _ => let foo := constr:(z _ _ _ _ _ _ _ _ j k) in constr:(2%nat)
| _ => let foo := constr:(z _ _ _ _ _ _ _ i j k) in constr:(3%nat)
| _ => let foo := constr:(z _ _ _ _ _ _ h i j k) in constr:(4%nat)
| _ => let foo := constr:(z _ _ _ _ _ g h i j k) in constr:(5%nat)
| _ => let foo := constr:(z _ _ _ _ f g h i j k) in constr:(6%nat)
| _ => let foo := constr:(z _ _ _ e f g h i j k) in constr:(7%nat)
| _ => let foo := constr:(z _ _ d e f g h i j k) in constr:(8%nat)
| _ => let foo := constr:(z _ c d e f g h i j k) in constr:(9%nat)
| _ => let foo := constr:(z b c d e f g h i j k) in constr:(10%nat)
end
| (?z ?c ?d ?e ?f ?g ?h ?i ?j ?k) =>
match th with
| _ => let foo := constr:(z _ _ _ _ _ _ _ _ k) in constr:(1%nat)
| _ => let foo := constr:(z _ _ _ _ _ _ _ j k) in constr:(2%nat)
| _ => let foo := constr:(z _ _ _ _ _ _ i j k) in constr:(3%nat)
| _ => let foo := constr:(z _ _ _ _ _ h i j k) in constr:(4%nat)
| _ => let foo := constr:(z _ _ _ _ g h i j k) in constr:(5%nat)
| _ => let foo := constr:(z _ _ _ f g h i j k) in constr:(6%nat)
| _ => let foo := constr:(z _ _ e f g h i j k) in constr:(7%nat)
| _ => let foo := constr:(z _ d e f g h i j k) in constr:(8%nat)
| _ => let foo := constr:(z c d e f g h i j k) in constr:(9%nat)
end
| (?z ?d ?e ?f ?g ?h ?i ?j ?k) =>
match th with
| _ => let foo := constr:(z _ _ _ _ _ _ _ k) in constr:(1%nat)
| _ => let foo := constr:(z _ _ _ _ _ _ j k) in constr:(2%nat)
| _ => let foo := constr:(z _ _ _ _ _ i j k) in constr:(3%nat)
| _ => let foo := constr:(z _ _ _ _ h i j k) in constr:(4%nat)
| _ => let foo := constr:(z _ _ _ g h i j k) in constr:(5%nat)
| _ => let foo := constr:(z _ _ f g h i j k) in constr:(6%nat)
| _ => let foo := constr:(z _ e f g h i j k) in constr:(7%nat)
| _ => let foo := constr:(z d e f g h i j k) in constr:(8%nat)
end
| (?z ?e ?f ?g ?h ?i ?j ?k) =>
match th with
| _ => let foo := constr:(z _ _ _ _ _ _ k) in constr:(1%nat)
| _ => let foo := constr:(z _ _ _ _ _ j k) in constr:(2%nat)
| _ => let foo := constr:(z _ _ _ _ i j k) in constr:(3%nat)
| _ => let foo := constr:(z _ _ _ h i j k) in constr:(4%nat)
| _ => let foo := constr:(z _ _ g h i j k) in constr:(5%nat)
| _ => let foo := constr:(z _ f g h i j k) in constr:(6%nat)
| _ => let foo := constr:(z e f g h i j k) in constr:(7%nat)
end
| (?z ?f ?g ?h ?i ?j ?k) =>
match th with
| _ => let foo := constr:(z _ _ _ _ _ k) in constr:(1%nat)
| _ => let foo := constr:(z _ _ _ _ j k) in constr:(2%nat)
| _ => let foo := constr:(z _ _ _ i j k) in constr:(3%nat)
| _ => let foo := constr:(z _ _ h i j k) in constr:(4%nat)
| _ => let foo := constr:(z _ g h i j k) in constr:(5%nat)
| _ => let foo := constr:(z f g h i j k) in constr:(6%nat)
end
| (?z ?g ?h ?i ?j ?k) =>
match th with
| _ => let foo := constr:(z _ _ _ _ k) in constr:(1%nat)
| _ => let foo := constr:(z _ _ _ j k) in constr:(2%nat)
| _ => let foo := constr:(z _ _ i j k) in constr:(3%nat)
| _ => let foo := constr:(z _ h i j k) in constr:(4%nat)
| _ => let foo := constr:(z g h i j k) in constr:(5%nat)
end
| (?z ?h ?i ?j ?k) =>
match th with
| _ => let foo := constr:(z _ _ _ k) in constr:(1%nat)
| _ => let foo := constr:(z _ _ j k) in constr:(2%nat)
| _ => let foo := constr:(z _ i j k) in constr:(3%nat)
| _ => let foo := constr:(z h i j k) in constr:(4%nat)
end
| (?z ?i ?j ?k) =>
match th with
| _ => let foo := constr:(z _ _ k) in constr:(1%nat)
| _ => let foo := constr:(z _ j k) in constr:(2%nat)
| _ => let foo := constr:(z i j k) in constr:(3%nat)
end
| (?z ?j ?k) =>
match th with
| _ => let foo := constr:(z _ k) in constr:(1%nat)
| _ => let foo := constr:(z j k) in constr:(2%nat)
end
| (?z ?j) => constr:(1%nat)
| _ => constr:(0%nat)
end
Did you really mean constr:(10%nat) and not constr:(11%nat) on the last line of your first match?
You are right it is an 11 there. Thanks!