diff options
| author | Brian Campbell | 2019-10-02 16:44:56 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-10-02 16:44:56 +0100 |
| commit | 2374aea33aa332f3927dd4dc4d6d9a15f5620ac9 (patch) | |
| tree | e84accdd464868a9ece9971ca17a2bae45aa62d6 /src/pretty_print_coq.ml | |
| parent | 2d1051cc4a1dfdd1a55e2df6ba331d7f1954bb61 (diff) | |
Coq: generate decidable equality instances for variant types
It only produces them when necessary (because some types do not have
decidable equality due to embedded proofs).
Also add trivial instance for the unit type.
Diffstat (limited to 'src/pretty_print_coq.ml')
| -rw-r--r-- | src/pretty_print_coq.ml | 23 |
1 files changed, 22 insertions, 1 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index dfef59a1..b0a0aee8 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -2611,7 +2611,28 @@ let doc_typdef generic_eq_types (TD_aux(td, (l, annot))) = (concat [string "Inductive"; space; typ_nm]) ((*doc_typquant typq*) ar_doc) in let reset_implicits_pp = doc_reset_implicits id_pp typq in - typ_pp ^^ dot ^^ hardline ^^ reset_implicits_pp ^^ twice hardline) + let doc_dec_eq_req = function + | QI_aux (QI_id (KOpt_aux (KOpt_kind (K_aux (K_type,_),kid),_)),_) -> + (* TODO: collision avoidance for x y *) + Some (string "`{forall x y : " ^^ doc_var empty_ctxt kid ^^ string ", Decidable (x = y)}") + | _ -> None + in + let eq_pp = + if IdSet.mem id generic_eq_types then + let typ_use_pp = + separate space (id_pp::Util.map_filter (quant_item_id_name empty_ctxt) (quant_items typq)) + in + let eq_reqs_pp = + separate (break 1) (Util.map_filter doc_dec_eq_req (quant_items typq)) + in + string "Instance Decidable_eq_" ^^ typ_nm ^^ space ^^ eq_reqs_pp ^^ colon ^/^ + string "forall (x y : " ^^ typ_use_pp ^^ string "), Decidable (x = y)." ^^ hardline ^^ + string "refine (Decidable_eq_from_dec (fun x y => _))." ^^ hardline ^^ + string "decide equality; refine (generic_dec _ _)." ^^ hardline ^^ + string "Defined." ^^ hardline + else empty + in + typ_pp ^^ dot ^^ hardline ^^ reset_implicits_pp ^^ hardline ^^ eq_pp ^^ hardline) | TD_enum(id,enums,_) -> (match id with | Id_aux ((Id "read_kind"),_) -> empty |