The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Oops - I just re-read this email and realized I wrote "Extraction 
Inline" when I meant "Extraction Implicit" :-[

All the same, I still need help....

-- Jonathan

On 06/21/2016 10:54 AM, Jonathan Leivent wrote:
> Does anyone have experience debugging Extraction Inline failures with 
> Unset Extraction SafeImplicits?  I just tried this for the first time, 
> and am not understanding what went wrong based on the comment placed 
> in the output by Unset Extraction SafeImplicits. The warning is:
>
> Warning:
>  At least an implicit occurs after extraction : 3rd argument (a) of 
> wfi_lt.
>  Extraction SafeImplicits is unset, extracting nonetheless,
>  but this code is potentially unsafe, please review it manually.
>
> The Coq script is attached.  The key extracted function is:
>
>   let merge_sort d ls =
>     let rec f _ =
>       let iH = fun y -> f y in
>       (fun d0 ls0 _ ->
>       let (ls1, ls2) = split ls0 in
>       (match ls2 with
>        | [] -> ls1
>        | _ :: _ -> merge_acc d0 (iH (length ls1) (not d0) ls1 __) (iH 
> (length ls2) (not d0) ls2 __) []))
>     in f __ (* 3rd argument (a) of wfi_lt *) d ls __
>  end
>
> It looks to me like the first arg of f is understood as not used by 
> extraction.   So, what is the comment saying about that arg?
>
> The function wfi_lt (well-founded induction using lt) was defined with:
>
>
> Definition wfi_lt := well_founded_induction_type Wf_nat.lt_wf.
>
> Extraction Implicit wfi_lt [1 3].
>
> Extraction Inline wfi_lt.
>
>
> Interestingly, merge_acc also uses wfi_lt, but extraction had no 
> difficulty with it:
>
>
>   let rec merge_acc d ls1 ls2 acc =
>     match ls1 with
>     | [] ->
>       (match ls2 with
>        | [] -> acc
>        | b :: ls4 -> merge_acc d [] ls4 (b :: acc))
>     | a :: ls3 ->
>       (match ls2 with
>        | [] -> merge_acc d [] ls3 (a :: acc)
>        | b :: ls4 -> if le_or_ge_dec d a b then merge_acc d ls1 ls4 (b 
> :: acc) else merge_acc d ls3 ls2 (a :: acc))
>
>
> This is using 8.5pl1
>
> Thanks,
>
> -- Jonathan