diff options
| author | Brian Campbell | 2019-03-13 09:28:10 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-03-13 09:28:10 +0000 |
| commit | 874bb01f0e2c201474e0a07602a38037bb2495f9 (patch) | |
| tree | 30c5e3ac630cec58690f7a6e6684e5bcb4f32f66 /src/pretty_print_lem.ml | |
| parent | 8c56dcf65016c3669b24e2c5828b5588436e078d (diff) | |
Tell Lem that records parametrised over Ints need the len typeclass annotations
Diffstat (limited to 'src/pretty_print_lem.ml')
| -rw-r--r-- | src/pretty_print_lem.ml | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 50ce1e5a..759c7637 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1024,6 +1024,22 @@ let rec doc_range_lem (BF_aux(r,_)) = match r with | BF_concat(ir1,ir2) -> (doc_range ir1) ^^ comma ^^ (doc_range ir2) *) +let doc_typquant_sorts idpp (TypQ_aux (typq,_)) = + match typq with + | TypQ_tq qs -> + let q (QI_aux (qi,_)) = + match qi with + | QI_id (KOpt_aux (KOpt_kind (K_aux (K_int,_),kid),_)) -> Some (string "`len`") + | QI_id (KOpt_aux (KOpt_kind (K_aux (K_type,_),kid),_)) -> Some underscore + | QI_id (KOpt_aux (KOpt_kind (K_aux ((K_order|K_bool),_),kid),_)) -> None + | QI_const _ -> None + in + if List.exists (function (QI_aux (QI_id (KOpt_aux (KOpt_kind (K_aux (K_int,_),_),_)),_)) -> true | _ -> false) qs then + let qs_pp = Util.map_filter q qs in + string "declare isabelle target_sorts " ^^ idpp ^^ space ^^ separate space (equals::qs_pp) ^^ hardline + else empty + | TypQ_no_forall -> empty + let doc_typdef_lem env (TD_aux(td, (l, annot))) = match td with | TD_abbrev(id,typq,A_aux (A_typ typ, _)) -> let typschm = TypSchm_aux (TypSchm_ts (typq, typ), l) in @@ -1078,9 +1094,10 @@ let doc_typdef_lem env (TD_aux(td, (l, annot))) = match td with doc_op equals (string "field_is_inc") (string (if is_inc then "true" else "false")); semi_sp; doc_op equals (string "get_field") (parens (doc_op arrow (string "fun rec_val") get)); semi_sp; doc_op equals (string "set_field") (parens (doc_op arrow (string "fun rec_val v") set)); space])) in *) + let sorts_pp = doc_typquant_sorts (doc_id_lem_type id) typq in doc_op equals (separate space [string "type"; doc_id_lem_type id; doc_typquant_items_lem None typq]) - ((*doc_typquant_lem typq*) (anglebars (space ^^ align fs_doc ^^ space))) ^^ hardline + ((*doc_typquant_lem typq*) (anglebars (space ^^ align fs_doc ^^ space))) ^^ hardline ^^ sorts_pp (* if !opt_sequential && string_of_id id = "regstate" then empty else separate_map hardline doc_field fs *) | TD_variant(id,typq,ar,_) -> |