Commit 80b5b265 authored by MARCHE Claude's avatar MARCHE Claude

printing of match expressions in smtv2

parent a07e74f4
......@@ -164,32 +164,50 @@ let rec print_term info fmt t = match t.t_node with
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;
(print_branches info subject print_term) bl;
forget_var subject
| Teps _ -> unsupportedTerm t
"smtv2: you must eliminate epsilon"
| Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
and print_branches info subject fmt bl =
and print_branches info subject pr 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"
try
match p.pat_node with
| Papp(cs,args) ->
let vars = List.map
(function { pat_node = Pvar v} -> v
| _ -> raise Exit) args
in cs,vars
| _ -> raise Exit
with Exit ->
unsupportedPattern p
"smtv2: you must compile nested pattern-matching"
in
match bl with
| [] -> print_branch info fmt (args,t)
| [] -> print_branch info subject pr fmt (constr,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>"
(print_branch info subject pr) (constr,args,t)
(print_branches info subject pr) bl
and print_branch info subject pr fmt (cs,vars,t) =
let i = ref 0 in
let print_proj fmt v =
incr i;
fprintf fmt "(%a (%a_proj_%d %a))" print_var v print_ident cs.ls_name
!i print_var subject
in
match vars with
| [] -> pr info fmt t
| _ -> fprintf fmt "@[(let (%a) %a)@]"
(print_list space print_proj) vars
(pr info) t
and print_fmla info fmt f = match f.t_node with
| Tapp ({ ls_name = id }, []) ->
......@@ -242,8 +260,16 @@ and print_fmla info fmt f = match f.t_node with
fprintf fmt "@[(let ((%a %a))@ %a)@]" print_var v
(print_term info) t1 (print_fmla info) f2;
forget_var v
(*
| Tcase _ -> unsupportedTerm f
"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 print_fmla) bl;
forget_var subject
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
and print_expr info fmt =
......
......@@ -179,7 +179,7 @@ let eliminate_definition_if_poly =
Trans.on_meta Detect_polymorphism.meta_monomorphic_types_only
(function
| [] -> eliminate_definition
| _ -> Trans.identity)
| _ -> eliminate_recursion)
let () =
Trans.register_transform "eliminate_definition_if_poly"
......
......@@ -6,24 +6,23 @@ theory T
type list = Nil | Cons int list
function tl list : list
function length (l:list) : int
(* =
function tl (l:list) : list =
match l with
| Nil -> Nil
| Cons _ r -> r
end
goal g0: tl (Cons 42 (Cons 37 Nil)) = Cons 37 Nil
function length (l:list) : int =
match l with
| Nil -> 0
| Cons _ r -> 1 + length r
end
*)
axiom a : forall l:list. let h = tl l in length l = 1 + length h
goal g0: length (Cons 1 Nil) = 1
goal g1 : forall l:list. l <> Nil -> let h = tl l in length l = 1 + length h
goal g2: length (Cons 1 Nil) = 1
(*
goal g1 : forall x.
match x with A -> x=x | B A -> false | B (B _) -> false end
*)
end
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