diff options
| author | Brian Campbell | 2018-05-03 13:57:38 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-05-04 10:26:33 +0100 |
| commit | bdeaec366f85128a43e302b3e5831f9e2bace33c (patch) | |
| tree | a66979326369b3a75016e81ca1087b7677157266 /src | |
| parent | 5c6f3cf7822a7d4086031a4cf009af4b85c8949f (diff) | |
Basic Coq constraints
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 347b691d..5af4f417 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -397,6 +397,22 @@ let doc_lit (L_aux(lit,l)) = parens (separate space (List.map string [ "realFromFrac"; Big_int.to_string num; Big_int.to_string denom])) +(* TODO: parens *) +let rec doc_nc (NC_aux (nc,_)) = + match nc with + | NC_equal (ne1, ne2) -> doc_op equals (doc_nexp ne1) (doc_nexp ne2) + | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=") (doc_nexp ne1) (doc_nexp ne2) + | NC_bounded_le (ne1, ne2) -> doc_op (string "<=") (doc_nexp ne1) (doc_nexp ne2) + | NC_not_equal (ne1, ne2) -> doc_op (string "<>") (doc_nexp ne1) (doc_nexp ne2) + | NC_set (kid, is) -> (* TODO: is this a good translation? *) + separate space [string "In"; doc_var_lem kid; + brackets (separate (string "; ") + (List.map (fun i -> string (Nat_big_num.to_string i)) is))] + | NC_or (nc1, nc2) -> doc_op (string "\\/") (doc_nc nc1) (doc_nc nc2) + | NC_and (nc1, nc2) -> doc_op (string "/\\") (doc_nc nc1) (doc_nc nc2) + | NC_true -> string "True" + | NC_false -> string "False" + let doc_quant_item delimit (QI_aux (qi,_)) = match qi with | QI_id (KOpt_aux (KOpt_none kid,_)) -> @@ -408,7 +424,7 @@ let doc_quant_item delimit (QI_aux (qi,_)) = | BK_order -> None end | QI_id _ -> failwith "Quantifier with multiple kinds" - | QI_const nc -> None (* TODO *) + | QI_const nc -> Some (bquote ^^ braces (string "ArithFact" ^^ parens (doc_nc nc))) let doc_typquant_items delimit (TypQ_aux (tq,_)) = match tq with |