diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 21 | ||||
| -rw-r--r-- | src/rewriter.mli | 2 | ||||
| -rw-r--r-- | src/rewrites.ml | 36 |
3 files changed, 53 insertions, 6 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 90276cb3..d5aa7151 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -105,6 +105,11 @@ let is_number_char c = c = '0' || c = '1' || c = '2' || c = '3' || c = '4' || c = '5' || c = '6' || c = '7' || c = '8' || c = '9' +let is_enum env id = + match Env.lookup_id id env with + | Enum _ -> true + | _ -> false + let rec fix_id remove_tick name = match name with | "assert" | "lsl" @@ -1316,10 +1321,12 @@ let doc_exp_lem, doc_let_lem = | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> string ">>" | P_aux (P_id id,_) - when Util.is_none (is_auto_decomposed_exist (env_of e1) (typ_of e1)) -> + when Util.is_none (is_auto_decomposed_exist (env_of e1) (typ_of e1)) && + not (is_enum (env_of e1) id) -> separate space [string ">>= fun"; doc_id id; bigarrow] | P_aux (P_typ (typ, P_aux (P_id id,_)),_) - when Util.is_none (is_auto_decomposed_exist (env_of e1) typ) -> + when Util.is_none (is_auto_decomposed_exist (env_of e1) typ) && + not (is_enum (env_of e1) id) -> separate space [string ">>= fun"; doc_id id; colon; doc_typ ctxt typ; bigarrow] | _ -> separate space [string ">>= fun"; squote ^^ doc_pat ctxt true (pat, typ_of e1); bigarrow] @@ -1373,12 +1380,14 @@ let doc_exp_lem, doc_let_lem = (* Prefer simple lets over patterns, because I've found Coq can struggle to work out return types otherwise *) | LB_val(P_aux (P_id id,_),e) - when Util.is_none (is_auto_decomposed_exist (env_of e) (typ_of e)) -> + when Util.is_none (is_auto_decomposed_exist (env_of e) (typ_of e)) && + not (is_enum (env_of e) id) -> prefix 2 1 (separate space [string "let"; doc_id id; coloneq]) (top_exp ctxt false e) | LB_val(P_aux (P_typ (typ,P_aux (P_id id,_)),_),e) - when Util.is_none (is_auto_decomposed_exist (env_of e) typ) -> + when Util.is_none (is_auto_decomposed_exist (env_of e) typ) && + not (is_enum (env_of e) id) -> prefix 2 1 (separate space [string "let"; doc_id id; colon; doc_typ ctxt typ; coloneq]) (top_exp ctxt false e) @@ -1730,7 +1739,9 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = let exp_typ = Env.expand_synonyms env typ in match p with | P_id id - | P_typ (_,P_aux (P_id id,_)) when Util.is_none (is_auto_decomposed_exist env exp_typ) -> + | P_typ (_,P_aux (P_id id,_)) + when Util.is_none (is_auto_decomposed_exist env exp_typ) && + not (is_enum env id) -> parens (separate space [doc_id id; colon; doc_typ ctxt typ]) | _ -> (used_a_pattern := true; diff --git a/src/rewriter.mli b/src/rewriter.mli index 3e582071..da4702b5 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -74,6 +74,8 @@ val rewrite_lexp : tannot rewriters -> tannot lexp -> tannot lexp val rewrite_pat : tannot rewriters -> tannot pat -> tannot pat +val rewrite_pexp : tannot rewriters -> tannot pexp -> tannot pexp + val rewrite_let : tannot rewriters -> tannot letbind -> tannot letbind val rewrite_def : tannot rewriters -> tannot def -> tannot def diff --git a/src/rewrites.ml b/src/rewrites.ml index 0a8c8156..825073b4 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -4043,7 +4043,10 @@ let rewrite_defs_realise_mappings (Defs defs) = (* Rewrite to make all pattern matches in Coq output exhaustive. - Assumes that guards, vector patterns, etc have been rewritten already. *) + Assumes that guards, vector patterns, etc have been rewritten already, + and the scattered functions have been merged. + Will add escape effect where a default is needed, so effects will + need recalculated afterwards. *) let opt_coq_warn_nonexhaustive = ref false @@ -4285,6 +4288,37 @@ let rewrite_case (e,ann) = end | _ -> E_aux (e,ann) +let rewrite_fun rewriters (FD_aux (FD_function (r,t,e,fcls),f_ann)) = + let id,fcl_ann = + match fcls with + | FCL_aux (FCL_Funcl (id,_),ann) :: _ -> id,ann + | [] -> raise (Reporting_basic.err_unreachable (fst f_ann) + "Empty function") + in + let env = env_of_annot fcl_ann in + let process_funcl rps (FCL_aux (FCL_Funcl (_,pexp),_)) = process_pexp env rps pexp in + let rps = List.fold_left process_funcl [RP_any] fcls in + let fcls' = List.map (function FCL_aux (FCL_Funcl (id,pexp),ann) -> + FCL_aux (FCL_Funcl (id, rewrite_pexp rewriters pexp),ann)) + fcls in + match rps with + | [] -> FD_aux (FD_function (r,t,e,fcls'),f_ann) + | (example::_) -> + let _ = + if !opt_coq_warn_nonexhaustive + then Reporting_basic.print_err false false + (fst f_ann) "Non-exhaustive matching" ("Example: " ^ string_of_rp example) in + + let l = Parse_ast.Generated Parse_ast.Unknown in + let p = P_aux (P_wild, (l, empty_tannot)) in + let ann' = mk_tannot env (typ_of_annot fcl_ann) (mk_effect [BE_escape]) in + (* TODO: use an expression that specifically indicates a failed pattern match *) + let b = E_aux (E_exit (E_aux (E_lit (L_aux (L_unit, l)),(l,empty_tannot))),(l,ann')) in + let default = FCL_aux (FCL_Funcl (id,Pat_aux (Pat_exp (p,b),(l,empty_tannot))),fcl_ann) in + + FD_aux (FD_function (r,t,e,fcls'@[default]),f_ann) + + let rewrite = let alg = { id_exp_alg with e_aux = rewrite_case } in rewrite_defs_base |