345 |> Variable.variant_frees ctxt [f] |
345 |> Variable.variant_frees ctxt [f] |
346 |> map Free |
346 |> map Free |
347 |> curry list_comb f *} |
347 |> curry list_comb f *} |
348 |
348 |
349 text {* |
349 text {* |
350 This code extracts the argument types of a given function @{text "f"} and then generates |
350 This function takes a term and a context as argument. If the term is of function |
351 for each argument type a distinct variable; finally it applies the generated |
351 type, then @{ML "apply_fresh_args"} returns the term with distinct variables |
352 variables to the function. For example: |
352 applied to it. For example: |
353 |
353 |
354 @{ML_response_fake [display,gray] |
354 @{ML_response_fake [display,gray] |
355 "apply_fresh_args @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"} @{context} |
355 "let |
356 |> Syntax.string_of_term @{context} |
356 val t = @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"} |
357 |> writeln" |
357 val ctxt = @{context} |
|
358 in |
|
359 apply_fresh_args t ctxt |
|
360 |> Syntax.string_of_term ctxt |
|
361 |> writeln |
|
362 end" |
358 "P z za zb"} |
363 "P z za zb"} |
359 |
364 |
360 You can read off this behaviour from how @{ML apply_fresh_args} is |
365 You can read off this behaviour from how @{ML apply_fresh_args} is |
361 coded: in Line 2, the function @{ML [index] fastype_of} calculates the type of the |
366 coded: in Line 2, the function @{ML [index] fastype_of} calculates the type of the |
362 function; @{ML [index] binder_types} in the next line produces the list of argument |
367 function; @{ML [index] binder_types} in the next line produces the list of argument |
370 function and the variables list as a pair. This kind of functions is often needed when |
375 function and the variables list as a pair. This kind of functions is often needed when |
371 constructing terms and the infrastructure helps tremendously to avoid |
376 constructing terms and the infrastructure helps tremendously to avoid |
372 any name clashes. Consider for example: |
377 any name clashes. Consider for example: |
373 |
378 |
374 @{ML_response_fake [display,gray] |
379 @{ML_response_fake [display,gray] |
375 "apply_fresh_args @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"} @{context} |
380 "let |
376 |> Syntax.string_of_term @{context} |
381 val t = @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"} |
377 |> writeln" |
382 val ctxt = @{context} |
|
383 in |
|
384 apply_fresh_args t ctxt |
|
385 |> Syntax.string_of_term ctxt |
|
386 |> writeln |
|
387 end" |
378 "za z zb"} |
388 "za z zb"} |
379 |
389 |
|
390 where the @{text "za"} is correctly avoided. |
|
391 |
380 The combinator @{ML [index] "#>"} is the reverse function composition. It can be |
392 The combinator @{ML [index] "#>"} is the reverse function composition. It can be |
381 used to define the following function |
393 used to define the following function |
382 *} |
394 *} |
383 |
395 |
384 ML{*val inc_by_six = |
396 ML{*val inc_by_six = |