diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 19 | ||||
| -rw-r--r-- | src/rewrites.ml | 28 |
2 files changed, 27 insertions, 20 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 90484598..72d7730e 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -2519,7 +2519,7 @@ let merge_var_patterns map pats = type mutrec_pos = NotMutrec | FirstFn | LaterFn -let doc_funcl mutrec rec_opt (FCL_aux(FCL_Funcl(id, pexp), annot)) = +let doc_funcl mutrec rec_opt ?rec_set (FCL_aux(FCL_Funcl(id, pexp), annot)) = let env = env_of_annot annot in let (tq,typ) = Env.get_val_spec_orig id env in let (arg_typs, ret_typ, eff) = match typ with @@ -2542,9 +2542,8 @@ let doc_funcl mutrec rec_opt (FCL_aux(FCL_Funcl(id, pexp), annot)) = let kid_to_arg_rename, pats = merge_var_patterns kid_to_arg_rename pats in let kids_used = KidSet.diff bound_kids eliminated_kids in let is_measured, recursive_ids = match rec_opt with - (* No mutual recursion in this backend yet; only change recursive - definitions where we have a measure *) - | Rec_aux (Rec_measure _,_) -> true, IdSet.singleton id + | Rec_aux (Rec_measure _,_) -> + true, (match rec_set with None -> IdSet.singleton id | Some s -> s) | _ -> false, IdSet.empty in let kir_rev = @@ -2694,17 +2693,17 @@ let get_id = function (* Coq doesn't support multiple clauses for a single function joined by "and". However, all the funcls should have been merged by the merge_funcls rewrite now. *) -let doc_fundef_rhs ?(mutrec=NotMutrec) (FD_aux(FD_function(r, typa, efa, funcls),(l,_))) = +let doc_fundef_rhs ?(mutrec=NotMutrec) rec_set (FD_aux(FD_function(r, typa, efa, funcls),(l,_))) = match funcls with | [] -> unreachable l __POS__ "function with no clauses" - | [funcl] -> doc_funcl mutrec r funcl + | [funcl] -> doc_funcl mutrec r ~rec_set funcl | (FCL_aux (FCL_Funcl (id,_),_))::_ -> unreachable l __POS__ ("function " ^ string_of_id id ^ " has multiple clauses in backend") -let doc_mutrec = function +let doc_mutrec rec_set = function | [] -> failwith "DEF_internal_mutrec with empty function list" | fundef::fundefs -> - doc_fundef_rhs ~mutrec:FirstFn fundef ^^ hardline ^^ - separate_map hardline (doc_fundef_rhs ~mutrec:LaterFn) fundefs ^^ dot + doc_fundef_rhs ~mutrec:FirstFn rec_set fundef ^^ hardline ^^ + separate_map hardline (doc_fundef_rhs ~mutrec:LaterFn rec_set) fundefs ^^ dot let rec doc_fundef (FD_aux(FD_function(r, typa, efa, fcls),fannot)) = match fcls with @@ -2918,7 +2917,7 @@ let rec doc_def unimplemented generic_eq_types def = | DEF_default df -> empty | DEF_fundef fdef -> group (doc_fundef fdef) ^/^ hardline - | DEF_internal_mutrec fundefs -> doc_mutrec fundefs ^/^ hardline + | DEF_internal_mutrec fundefs -> doc_mutrec (ids_of_def def) fundefs ^/^ hardline | DEF_val (LB_aux (LB_val (pat, exp), _)) -> doc_val pat exp | DEF_scattered sdef -> failwith "doc_def: shoulnd't have DEF_scattered at this point" | DEF_mapdef (MD_aux (_, (l,_))) -> unreachable l __POS__ "Coq doesn't support mappings" diff --git a/src/rewrites.ml b/src/rewrites.ml index 2a5799d3..11b1d469 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -4476,8 +4476,9 @@ let rewrite_explicit_measure env (Defs defs) = Bindings.add id (mpat,mexp) measures | _ -> measures in - let scan_def measures = function + let rec scan_def measures = function | DEF_fundef fd -> scan_function measures fd + | DEF_internal_mutrec fds -> List.fold_left scan_function measures fds | _ -> measures in let measures = List.fold_left scan_def Bindings.empty defs in @@ -4510,7 +4511,7 @@ let rewrite_explicit_measure env (Defs defs) = | exception Not_found -> [vs] in (* Add extra argument and assertion to each funcl, and rewrite recursive calls *) - let rewrite_funcl (FCL_aux (FCL_Funcl (id,pexp),fcl_ann) as fcl) = + let rewrite_funcl recset (FCL_aux (FCL_Funcl (id,pexp),fcl_ann) as fcl) = let loc = Parse_ast.Generated (fst fcl_ann) in let P_aux (pat,pann),guard,body,ann = destruct_pexp pexp in let extra_pat = P_aux (P_id limit,(loc,empty_tannot)) in @@ -4537,15 +4538,15 @@ let rewrite_explicit_measure env (Defs defs) = let body = fold_exp { id_exp_alg with e_app = (fun (f,args) -> - if Id.compare f id == 0 - then E_app (rec_id id, args@[tick]) + if IdSet.mem f recset + then E_app (rec_id f, args@[tick]) else E_app (f, args)) } body in let body = E_aux (E_block [assert_exp; body],(loc,empty_tannot)) in FCL_aux (FCL_Funcl (rec_id id, construct_pexp (P_aux (pat,pann),guard,body,ann)),fcl_ann) in - let rewrite_function (FD_aux (FD_function (r,t,e,fcls),ann) as fd) = + let rewrite_function recset (FD_aux (FD_function (r,t,e,fcls),ann) as fd) = let loc = Parse_ast.Generated (fst ann) in match fcls with | FCL_aux (FCL_Funcl (id,_),fcl_ann)::_ -> begin @@ -4593,15 +4594,22 @@ let rewrite_explicit_measure env (Defs defs) = let new_rec = Rec_aux (Rec_measure (P_aux (P_tup (List.map (fun _ -> P_aux (P_wild,(loc,empty_tannot))) measure_pats @ [P_aux (P_id limit,(loc,empty_tannot))]),(loc,empty_tannot)), E_aux (E_id limit, (loc,empty_tannot))), loc) in - [FD_aux (FD_function (new_rec,t,e,List.map rewrite_funcl fcls),ann); - FD_aux (FD_function (Rec_aux (Rec_nonrec,loc),t,e,[wrapper]),ann)] - | exception Not_found -> [fd] + FD_aux (FD_function (new_rec,t,e,List.map (rewrite_funcl recset) fcls),ann), + [FD_aux (FD_function (Rec_aux (Rec_nonrec,loc),t,e,[wrapper]),ann)] + | exception Not_found -> fd,[] end - | _ -> [fd] + | _ -> fd,[] in let rewrite_def = function | DEF_spec vs -> List.map (fun vs -> DEF_spec vs) (rewrite_spec vs) - | DEF_fundef fd -> List.map (fun f -> DEF_fundef f) (rewrite_function fd) + | DEF_fundef fd -> + let fd,extra = rewrite_function (IdSet.singleton (id_of_fundef fd)) fd in + List.map (fun f -> DEF_fundef f) (fd::extra) + | (DEF_internal_mutrec fds) as d -> + let recset = ids_of_def d in + let fds,extras = List.split (List.map (rewrite_function recset) fds) in + let extras = List.concat extras in + (DEF_internal_mutrec fds)::(List.map (fun f -> DEF_fundef f) extras) | d -> [d] in Defs (List.flatten (List.map rewrite_def defs)) |