Commit 010b02f0 authored by MARCHE Claude's avatar MARCHE Claude

Print match in smtv2 in progress

parent 9c60096e
......@@ -337,6 +337,7 @@ let sprint_decl (fn : 'a -> Format.formatter -> decl -> 'a * string list) =
exception UnsupportedType of ty * string
exception UnsupportedTerm of term * string
exception UnsupportedPattern of pattern * string
exception UnsupportedDecl of decl * string
exception NotImplemented of string
exception Unsupported of string
......@@ -345,6 +346,7 @@ exception Unsupported of string
let unsupportedType e s = raise (UnsupportedType (e,s))
let unsupportedTerm e s = raise (UnsupportedTerm (e,s))
let unsupportedPattern p s = raise (UnsupportedPattern (p,s))
let unsupportedDecl e s = raise (UnsupportedDecl (e,s))
let notImplemented s = raise (NotImplemented s)
let unsupported s = raise (Unsupported s)
......@@ -384,6 +386,9 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
| UnsupportedTerm (e,s) ->
fprintf fmt "@[@[<hov 3> This expression isn't supported:@\n%a@]@\n %s@]"
Pretty.print_term e s
| UnsupportedPattern (p,s) ->
fprintf fmt "@[@[<hov 3> This pattern isn't supported:@\n%a@]@\n %s@]"
Pretty.print_pat p s
| UnsupportedDecl (d,s) ->
fprintf fmt "@[@[<hov 3> This declaration isn't supported:@\n%a@]@\n %s@]"
Pretty.print_decl d s
......
......@@ -109,6 +109,7 @@ exception NotImplemented of string
val unsupportedType : ty -> string -> 'a
val unsupportedTerm : term -> string -> 'a
val unsupportedPattern : pattern -> string -> 'a
val unsupportedDecl : decl -> string -> 'a
val notImplemented : string -> 'a
......
......@@ -156,12 +156,41 @@ let rec print_term info fmt t = match t.t_node with
| Tif (f1,t1,t2) ->
fprintf fmt "@[(ite %a@ %a@ %a)@]"
(print_fmla info) f1 (print_term info) t1 (print_term info) t2
(*
| Tcase _ -> unsupportedTerm t
"smtv2 : you must eliminate match"
"smtv2: you must eliminate match"
*)
| Tcase(t,bl) ->
let subject = create_vsymbol (id_fresh "subject") (t_type t) in
fprintf fmt "@[(let ((%a @[%a@]))@ %a)@]"
print_var subject (print_term info) t
(print_branches info subject) bl;
forget_var subject
| Teps _ -> unsupportedTerm t
"smtv2 : you must eliminate epsilon"
"smtv2: you must eliminate epsilon"
| Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
and print_branches info subject fmt bl =
match bl with
| [] -> assert false
| br::bl ->
let (p,t) = t_open_branch br in
let constr,args =
match p.pat_node with
| Papp(cs,args) -> cs,args
| _ -> unsupportedPattern p
"smtv2: you must compile nested pattern-matching"
in
match bl with
| [] -> print_branch info fmt (args,t)
| _ ->
fprintf fmt "@[(ite (is-%a %a) %a %a)@]"
print_ident constr.ls_name print_var subject
(print_branch info) (args,t) (print_branches info subject) bl
and print_branch info fmt (vars,t) =
fprintf fmt "<branch>"
and print_fmla info fmt f = match f.t_node with
| Tapp ({ ls_name = id }, []) ->
print_ident fmt id
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment