The Coq mailing list

["Yamamoto, Yosuke" <yoy553 AT mail.usask.ca>]

Hi, 

I am trying to add a tactic (ccred) to Coq 8.6 so that it syntactically executes case-of-case transformation mentioned in the following paper. 

   Title: Compiling without continuation 

   Authors: Luke Maurer, Paul Downen, Zena M. Ariola, and Simon Peyton Jones

   Status: Submitted 2016/11/18

   URL: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/11/join-points.pdf. 

The current implementation 

  https://github.com/yoy553/ccred 

works for simple examples such as the ones used in section 1 and 2 of the above-mentioned paper, but it fails for a slightly complex example: I included both successful (cwc.v) and failure cases (ccred_error.v) in the patch. Testing with variations of this failure case, I observe De Bruijn index off for some variables (in the case of ccred_error.v the index for one of H0 is off).  

I wonder if anyone could point out what is the problem in this implementation, or if someone in the development team can implement case-of-case transformation as a syntactic reduction that even reduces within closures (in the case of ccred_error.v within the match-_expression_ without eliminating b). I plan to use the reduction as a part of some other automation, and want to avoid elimination argument for simplification. 

Following is its main part (a function ccred_reduction which runs for a new brunch in knr to modify the stack when there is a nested match-_expression_) added to kernel/cClosure.ml:  

let rec ccred_reduction info stk m =                            

  match stk with

  | ZcaseT (ci_in,t_in,brs_in,env_in) :: stk -> 

     ( match (compact_stack m stk) with 

       | ZcaseT (ci_out,t_out,brs_out,env_out) :: stk 

           -> let tctxt_in, tb_in   = decompose_lam t_in    in 

              let tctxt_out, tb_out = decompose_lam t_out   in 

              let num_targs_in      = List.length tctxt_in  in

              let num_targs_out     = List.length tctxt_out in

              let t_new = compose_lam tctxt_in (applistc (lift num_targs_in t_out) [tb_in])  in 

              let f brs_in_ith = match kind_of_term brs_in_ith with 

                   | Lambda _ -> let ctxt_in,b_in = decompose_lam brs_in_ith                 in 

                                 let num_args_in  = List.length ctxt_in                      in 

                                 let brs_out_new  = Array.map (lift num_args_in) brs_ou      in

                                   compose_lam ctxt_in (mkCase (ci_out, t_out, b_in, brs_out_new))                       

                   | _ -> mkCase (ci_out, t_out, brs_in_ith, brs_out)                                        

              in                    

              let brs_new = Array.map f brs_in              in 

              let env_new = env_out                         in

               ZcaseT (ci_in, t_new, brs_new, env_new)::stk                                  

       | _ -> assert false )

  | h1::stk -> h1 :: ccred_reduction info (compact_stack m stk) m

  | _ -> assert false (* checked by the branch predicate [is_nested_match_stk] *)​

let rec is_nested_match_stk m stk =

  match stk with

  | [] -> false

  | [a] -> false

  | ZcaseT _ :: stk ->        

     ( match (compact_stack m stk) with 

       | ZcaseT _ :: stk -> true

       | _ -> false)

  | h :: t -> is_nested_match_stk m t 

let rec knr info m stk =

  match m.term with

    .

    .

    .

  | FFlex _ | FRel _ when !Flags.ccred &&

                            (is_nested_match_stk m stk) && 

                              (red_set info.i_flags fCCRED) && !Flags.ccred   -> 

     (m, ccred_reduction info stk m)

    . 

    .

Thanks, 

--

Yosuke Y.​