Skip to content

Printer for terms #14

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 14 commits into from
Closed

Printer for terms #14

Changes from 1 commit
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
a982ea9
Typo in doc comment
Gbury Oct 25, 2018
2459ccc
Add escaping module
Gbury Oct 25, 2018
c8d5491
Started tptp pretty-printer
Gbury Oct 31, 2018
82a1104
Commited skeleton
Gbury Nov 9, 2018
e1ab3ca
Remove `.merlin`.
anmaped Dec 3, 2018
4a9a66b
Merge remote-tracking branch 'remotes/origin/master' into printer
anmaped Dec 3, 2018
883a16c
Add dune build to export folder.
anmaped Dec 3, 2018
ada95d1
Add package dolmen-export.
anmaped Dec 3, 2018
2671d93
Fix Makefile.
anmaped Dec 3, 2018
7eba3e8
Update on smtlib print functions.
anmaped Dec 5, 2018
f5ee3fb
Updated smtlib exporter.
anmaped Jan 29, 2019
309c830
small update on smtlib exporter.
anmaped Jan 29, 2019
b4adc60
Fix double parenthesis.
anmaped Apr 15, 2019
e81b130
Merge branch 'master' into printer
anmaped Jul 17, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
119 changes: 68 additions & 51 deletions src/export/smtlib.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,71 +1,86 @@
(* This module contains the pretty-printer functions for smtlib *)

open Dolmen_std

open Pretty
open Term
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm really, really, really not a fan of using a lot of opens. Dolmen_std is fine to open, but Pretty and Term should not be opened.


(* auxiliar functions *)
let pp_builtins = function
| Wildcard -> Pretty.mk "$_" Pretty.Prefix
| Ttype -> Pretty.mk "Type" Pretty.Prefix
| Prop -> Pretty.mk "$o" Pretty.Prefix
let print_builtins = function
| Wildcard -> assert false
| Ttype -> assert false
| Prop -> assert false
| True -> Pretty.mk "true" Pretty.Prefix
| False -> Pretty.mk "false" Pretty.Prefix
| Eq -> Pretty.mk "=" Pretty.Infix
| Distinct -> Pretty.mk "$distinct" Pretty.Prefix
| Ite -> Pretty.mk "$ite" Pretty.Prefix
| Sequent -> Pretty.mk "-->" Pretty.Infix
| Int -> Pretty.mk "$int" Pretty.Prefix
| Minus -> Pretty.mk "$uminus" Pretty.Prefix
| Add -> Pretty.mk "$sum" Pretty.Prefix
| Sub -> Pretty.mk "$difference" Pretty.Prefix
| Mult -> Pretty.mk "$product" Pretty.Prefix
| Lt -> Pretty.mk "$less" Pretty.Prefix
| Leq -> Pretty.mk "$lesseq" Pretty.Prefix
| Gt -> Pretty.mk "$greater" Pretty.Prefix
| Geq -> Pretty.mk "$greatereq" Pretty.Prefix
| Subtype -> Pretty.mk "<<" Pretty.Infix
| Product -> Pretty.mk "*" Pretty.Infix
| Union -> Pretty.mk "+" Pretty.Infix
| Not -> Pretty.mk "~" Pretty.Prefix
| And -> Pretty.mk "&" Pretty.Infix ~assoc:Pretty.Left
| Or -> Pretty.mk "|" Pretty.Infix ~assoc:Pretty.Left
| Nand -> Pretty.mk "~&" Pretty.Infix
| Xor -> Pretty.mk "<~>" Pretty.Infix
| Nor -> Pretty.mk "~|" Pretty.Infix
| Imply -> Pretty.mk "=>" Pretty.Infix ~assoc:Pretty.Right
| Implied -> Pretty.mk "<=" Pretty.Infix
| Equiv -> Pretty.mk "<=>" Pretty.Infix
| Eq -> Pretty.mk "=" Pretty.Prefix
| Distinct -> assert false
| Ite -> Pretty.mk "ite" Pretty.Prefix
| Sequent -> assert false
| Int -> assert false
| Minus -> Pretty.mk "-" Pretty.Prefix
| Add -> Pretty.mk "+" Pretty.Prefix
| Sub -> Pretty.mk "-" Pretty.Prefix
| Mult -> Pretty.mk "*" Pretty.Prefix
| Lt -> Pretty.mk "<" Pretty.Prefix
| Leq -> Pretty.mk "<=" Pretty.Prefix
| Gt -> Pretty.mk ">" Pretty.Prefix
| Geq -> Pretty.mk ">=" Pretty.Prefix
| Subtype -> assert false
| Product -> assert false
| Union -> assert false
| Not -> Pretty.mk "not" Pretty.Prefix
| And -> Pretty.mk "and" Pretty.Prefix
| Or -> Pretty.mk "or" Pretty.Prefix
| Nand -> assert false
| Xor -> assert false
| Nor -> assert false
| Imply -> Pretty.mk "=>" Pretty.Prefix
| Implied -> assert false
| Equiv -> assert false
;;

let pp_binder = function
let print_binder = function
| All -> Pretty.mk "forall" Pretty.Prefix
| Ex -> Pretty.mk "exists" Pretty.Prefix
| Pi -> assert false
| Arrow -> assert false
| Let -> assert false
| Fun -> assert false
| Fun -> Pretty.mk "fun" Pretty.Prefix
| Choice -> assert false
| Description -> assert false
;;

let pp_descr = function
| Symbol id -> Pretty.mk "%symb%" Pretty.Prefix
let rec print_descr = function
| Symbol id -> Pretty.mk (Dolmen_std.Id.full_name id) Pretty.Prefix
| Builtin builtin -> assert false
| Colon (term1, term2) -> assert false
| Colon (term1, term2) ->
Pretty.mk ((print_terms_ term1).name ^ " " ^ (print_terms_ term2).name) Pretty.Prefix
| App (term1, term2) -> assert false
| Binder (binder, term_list1, term_list2) -> assert false
| Binder (binder, term_list, term) ->
Pretty.mk
((print_fold_terms term_list).name ^ " " ^ (print_terms_ term).name)
Pretty.Infix
| Match (term, term_pair_list) -> assert false

and print_fold_terms t =
List.fold_left
(fun a b -> {a with name = a.name ^ (print_terms_ b).name})
(Pretty.mk "" Pretty.Prefix)
t

and print_variables v = assert false

(* terms *)
and print_terms_ = function
| {term = Symbol _ as d; _} | {term = Builtin _ as d; _} -> print_descr d
| e -> Pretty.mk ("(" ^ (print_descr e.term).name ^ ")") Pretty.Prefix
;;

let pp = function
| { term = (Symbol _) as d; _ }
| { term = (Builtin _) as d; _ } -> pp_descr d
| e -> ( match (pp_descr e.term) with { name=n; _} -> Pretty.mk ("("^n^")") Pretty.Prefix )
let print_terms fmt t = Format.fprintf fmt "%s" (print_terms_ t).name

open Statement

let pp_descr = function
(* statements *)
let print_statements fmt = function
| Pack term_list -> assert false
| Pop n -> assert false
| Push n -> assert false
Expand All @@ -76,12 +91,20 @@ let pp_descr = function
| Antecedent term -> assert false
| Consequent term -> assert false
| Include str -> assert false
| Set_logic str -> assert false
| Set_logic str -> Format.fprintf fmt "(set-logic %s)" str
| Get_info str -> assert false
| Set_info term -> assert false
| Set_info term -> Format.fprintf fmt "(set-info %a)" print_terms term
| Get_option str -> assert false
| Set_option term -> assert false
| Def (id, term) -> assert false
| Def (id, ({term = Binder (binder, _, _)} as term)) ->
Format.fprintf
fmt
"(define-%s %s %a)"
(print_binder binder).name
(Dolmen_std.Id.full_name id)
print_terms
term
| Def (id, _) -> assert false
| Decl (id, term) -> assert false
| Inductive inductive -> assert false
| Get_proof -> assert false
Expand All @@ -96,10 +119,4 @@ let pp_descr = function
| Exit -> assert false
;;

let pp_variables = assert false

(* terms *)
let pp_terms = assert false

(* statements *)
let pp_statements = assert false
let print fmt = function {descr; _} -> Format.fprintf fmt "%a" print_statements descr