new or-pat compilation + exhaustiveness used in compilation

git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@3274 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
master
Luc Maranget 2000-08-11 19:58:52 +00:00
parent d043fecf18
commit e8ea52a66a
8 changed files with 743 additions and 383 deletions

View File

@ -202,6 +202,9 @@ let add_event ev =
let lbl_staticfail = ref None
and sz_staticfail = ref 0
(* Same information as a stack for Lstaticraise *)
let sz_static_raises = ref []
(* Function bodies that remain to be compiled *)
type function_to_compile =
@ -507,13 +510,25 @@ let rec comp_expr env exp sz cont =
lbl_staticfail := saved_lbl_staticfail;
sz_staticfail := saved_sz_staticfail;
cont3
| Lstaticfail ->
| Lstaticfail -> comp_static_fail sz cont
| Lstaticcatch (body, i, handler) ->
let branch1, cont1 = make_branch cont in
let lbl_handler, cont2 =
label_code (comp_expr env handler sz cont1) in
sz_static_raises := (i, (lbl_handler, sz)) :: !sz_static_raises ;
let cont3 = comp_expr env body sz (branch1 :: cont2) in
sz_static_raises := List.tl !sz_static_raises ;
cont3
| Lstaticraise i ->
let cont = discard_dead_code cont in
begin match !lbl_staticfail with
None -> cont
| Some label ->
add_pop (sz - !sz_staticfail) (Kbranch label :: cont)
end
let label, size =
try
List.assoc i !sz_static_raises
with
| Not_found ->
Misc.fatal_error
("exit("^string_of_int i^") outside appropriated catch") in
add_pop (sz-size) (Kbranch label :: cont)
| Ltrywith(body, id, handler) ->
let (branch1, cont1) = make_branch cont in
let lbl_handler = new_label() in
@ -556,19 +571,27 @@ let rec comp_expr env exp sz cont =
List.iter (fun (n, act) -> act_blocks.(n) <- act) sw.sw_blocks;
let lbl_consts = Array.create sw.sw_numconsts 0 in
let lbl_blocks = Array.create sw.sw_numblocks 0 in
let comp_nofail =
if sw.sw_nofail then
fun l c -> match l with
| Lstaticfail -> label_code c
| _ -> label_code(comp_expr env l sz (branch :: c))
else
fun l c ->
label_code(comp_expr env l sz (branch :: c)) in
for i = sw.sw_numblocks - 1 downto 0 do
let (lbl, c1) =
label_code(comp_expr env act_blocks.(i) sz (branch :: !c)) in
let (lbl, c1) = comp_nofail act_blocks.(i) !c in
lbl_blocks.(i) <- lbl;
c := discard_dead_code c1
done;
for i = sw.sw_numconsts - 1 downto 0 do
let (lbl, c1) =
label_code(comp_expr env act_consts.(i) sz (branch :: !c)) in
let (lbl, c1) = comp_nofail act_consts.(i) !c in
lbl_consts.(i) <- lbl;
c := discard_dead_code c1
done;
if sw.sw_checked then c := comp_expr env Lstaticfail sz !c;
if sw.sw_checked && not sw.sw_nofail then
c := comp_expr env Lstaticfail sz !c;
comp_expr env arg sz (Kswitch(lbl_consts, lbl_blocks) :: !c)
| Lassign(id, expr) ->
begin try
@ -626,6 +649,16 @@ let rec comp_expr env exp sz cont =
| Lifused (_, exp) ->
comp_expr env exp sz cont
(* compile a static failure, fails if not enclosing catch *)
and comp_static_fail sz cont =
let cont = discard_dead_code cont in
begin match !lbl_staticfail with
| None ->
Misc.fatal_error "exit outside appropriated catch"
| Some label ->
add_pop (sz - !sz_staticfail) (Kbranch label :: cont)
end
(* Compile a list of arguments [e1; ...; eN] to a primitive operation.
The values of eN ... e2 are pushed on the stack, e2 at top of stack,
then e3, then ... The value of e1 is left in the accumulator. *)
@ -648,18 +681,18 @@ and comp_binary_test env cond ifso ifnot sz cont =
let (lbl_end, cont1) = label_code cont in
Kstrictbranchifnot lbl_end :: comp_expr env ifso sz cont1
end else
if ifso = Lstaticfail && (sz = !sz_staticfail || !lbl_staticfail = None)
if ifso = Lstaticfail && sz = !sz_staticfail
then
let cont = comp_expr env ifnot sz cont in
match !lbl_staticfail with
None -> cont
| None -> Misc.fatal_error "exit outside appropriated catch"
| Some label -> Kbranchif label :: cont
else
if ifnot = Lstaticfail && (sz = !sz_staticfail || !lbl_staticfail = None)
if ifnot = Lstaticfail && sz = !sz_staticfail
then
let cont = comp_expr env ifso sz cont in
match !lbl_staticfail with
None -> cont
| None -> Misc.fatal_error "exit outside appropriated catch"
| Some label -> Kbranchifnot label :: cont
else begin
let (branch_end, cont1) = make_branch cont in

View File

@ -125,6 +125,8 @@ type lambda =
| Lswitch of lambda * lambda_switch
| Lstaticfail
| Lcatch of lambda * lambda
| Lstaticraise of int
| Lstaticcatch of lambda * int * lambda
| Ltrywith of lambda * Ident.t * lambda
| Lifthenelse of lambda * lambda * lambda
| Lsequence of lambda * lambda
@ -140,7 +142,8 @@ and lambda_switch =
sw_consts: (int * lambda) list;
sw_numblocks: int;
sw_blocks: (int * lambda) list;
sw_checked: bool }
sw_checked: bool ;
sw_nofail: bool }
and lambda_event =
{ lev_loc: int;
@ -201,9 +204,12 @@ let free_variables l =
freevars arg;
List.iter (fun (key, case) -> freevars case) sw.sw_consts;
List.iter (fun (key, case) -> freevars case) sw.sw_blocks
| Lstaticfail -> ()
| Lstaticfail -> ()
| Lcatch(e1, e2) ->
freevars e1; freevars e2
| Lstaticraise _ -> ()
| Lstaticcatch(e1, _, e2) ->
freevars e1; freevars e2
| Ltrywith(e1, exn, e2) ->
freevars e1; freevars e2; fv := IdentSet.remove exn !fv
| Lifthenelse(e1, e2, e3) ->
@ -270,8 +276,10 @@ let subst_lambda s lam =
Lswitch(subst arg,
{sw with sw_consts = List.map subst_case sw.sw_consts;
sw_blocks = List.map subst_case sw.sw_blocks})
| Lstaticfail -> Lstaticfail
| Lstaticfail as l -> l
| Lcatch(e1, e2) -> Lcatch(subst e1, subst e2)
| Lstaticraise i as l -> l
| Lstaticcatch(e1, io, e2) -> Lstaticcatch(subst e1, io, subst e2)
| Ltrywith(e1, exn, e2) -> Ltrywith(subst e1, exn, subst e2)
| Lifthenelse(e1, e2, e3) -> Lifthenelse(subst e1, subst e2, subst e3)
| Lsequence(e1, e2) -> Lsequence(subst e1, subst e2)

View File

@ -134,6 +134,8 @@ type lambda =
| Lswitch of lambda * lambda_switch
| Lstaticfail
| Lcatch of lambda * lambda
| Lstaticraise of int
| Lstaticcatch of lambda * int * lambda
| Ltrywith of lambda * Ident.t * lambda
| Lifthenelse of lambda * lambda * lambda
| Lsequence of lambda * lambda
@ -149,8 +151,8 @@ and lambda_switch =
sw_consts: (int * lambda) list; (* Integer cases *)
sw_numblocks: int; (* Number of tag block cases *)
sw_blocks: (int * lambda) list; (* Tag block cases *)
sw_checked: bool } (* True if bound checks needed *)
sw_checked: bool ; (* True if bound checks needed *)
sw_nofail: bool} (* True if should not fail *)
and lambda_event =
{ lev_loc: int;
lev_kind: lambda_event_kind;

File diff suppressed because it is too large Load Diff

View File

@ -230,13 +230,19 @@ let rec lam ppf = function
fprintf ppf "@[<hv 1>case tag %i:@ %a@]" n lam l)
sw.sw_blocks in
fprintf ppf
"@[<1>(%s%a@ @[<v 0>%a@])@]"
(if sw.sw_checked then "switch-checked " else "switch ")
"@[<1>(%s%s%a@ @[<v 0>%a@])@]"
(if sw.sw_checked then "switch-checked" else "switch")
(if sw.sw_nofail then "* " else " ")
lam larg switch sw
| Lstaticfail ->
fprintf ppf "exit"
| Lstaticraise i ->
fprintf ppf "exit(%d)" i
| Lcatch(lbody, lhandler) ->
fprintf ppf "@[<2>(catch@ %a@;<1 -1>with@ %a)@]" lam lbody lam lhandler
| Lstaticcatch(lbody, i, lhandler) ->
fprintf ppf "@[<2>(catch@ %a@;<1 -1>with(%d)@ %a)@]"
lam lbody i lam lhandler
| Ltrywith(lbody, param, lhandler) ->
fprintf ppf "@[<2>(try@ %a@;<1 -1>with %a@ %a)@]"
lam lbody Ident.print param lam lhandler

View File

@ -53,11 +53,13 @@ let rec eliminate_ref id = function
sw_numblocks = sw.sw_numblocks;
sw_blocks =
List.map (fun (n, e) -> (n, eliminate_ref id e)) sw.sw_blocks;
sw_checked = sw.sw_checked})
| Lstaticfail ->
Lstaticfail
sw_checked = sw.sw_checked; sw_nofail = sw.sw_nofail})
| Lstaticfail as l -> l
| Lstaticraise _ as l -> l
| Lcatch(e1, e2) ->
Lcatch(eliminate_ref id e1, eliminate_ref id e2)
| Lstaticcatch(e1, i, e2) ->
Lstaticcatch(eliminate_ref id e1, i, eliminate_ref id e2)
| Ltrywith(e1, v, e2) ->
Ltrywith(eliminate_ref id e1, v, eliminate_ref id e2)
| Lifthenelse(e1, e2, e3) ->
@ -124,7 +126,9 @@ let simplify_lambda lam =
List.iter (fun (n, l) -> count l) sw.sw_consts;
List.iter (fun (n, l) -> count l) sw.sw_blocks
| Lstaticfail -> ()
| Lstaticraise _ -> ()
| Lcatch(l1, l2) -> count l1; count l2
| Lstaticcatch(l1, _, l2) -> count l1; count l2
| Ltrywith(l1, v, l2) -> count l1; count l2
| Lifthenelse(l1, l2, l3) -> count l1; count l2; count l3
| Lsequence(l1, l2) -> count l1; count l2
@ -182,14 +186,15 @@ let simplify_lambda lam =
Lletrec(List.map (fun (v, l) -> (v, simplif l)) bindings, simplif body)
| Lprim(p, ll) -> Lprim(p, List.map simplif ll)
| Lswitch(l, sw) ->
Lswitch(simplif l,
{sw_numconsts = sw.sw_numconsts;
sw_consts = List.map (fun (n, e) -> (n, simplif e)) sw.sw_consts;
sw_numblocks = sw.sw_numblocks;
sw_blocks = List.map (fun (n, e) -> (n, simplif e)) sw.sw_blocks;
sw_checked = sw.sw_checked})
| Lstaticfail -> Lstaticfail
let new_l = simplif l
and new_consts = List.map (fun (n, e) -> (n, simplif e)) sw.sw_consts
and new_blocks = List.map (fun (n, e) -> (n, simplif e)) sw.sw_blocks in
Lswitch
(new_l,{sw with sw_consts = new_consts ; sw_blocks = new_blocks})
| Lstaticfail as l -> l
| Lstaticraise _ as l -> l
| Lcatch(l1, l2) -> Lcatch(simplif l1, simplif l2)
| Lstaticcatch(l1, i, l2) -> Lstaticcatch(simplif l1, i, simplif l2)
| Ltrywith(l1, v, l2) -> Ltrywith(simplif l1, v, simplif l2)
| Lifthenelse(l1, l2, l3) -> Lifthenelse(simplif l1, simplif l2, simplif l3)
| Lsequence(Lifused(v, l1), l2) ->

View File

@ -92,6 +92,11 @@ let record_arg p = match p.pat_desc with
(* Raise Not_found when pos is not present in arg *)
let sort_fields args =
Sort.list
(fun (lbl1,_) (lbl2,_) -> lbl1.lbl_pos <= lbl2.lbl_pos)
args
let get_field pos arg =
let _,p = List.find (fun (lbl,_) -> pos = lbl.lbl_pos) arg in
p
@ -105,14 +110,27 @@ let extract_fields omegas arg =
with Not_found -> omega)
omegas
let records_args l1 l2 =
let l1 = sort_fields l1
and l2 = sort_fields l2 in
let rec combine r1 r2 l1 l2 = match l1,l2 with
| [],[] -> r1,r2
| [],(_,p2)::rem2 -> combine (omega::r1) (p2::r2) [] rem2
| (_,p1)::rem1,[] -> combine (p1::r1) (omega::r2) rem1 []
| (lbl1,p1)::rem1, (lbl2,p2)::rem2 ->
if lbl1.lbl_pos < lbl2.lbl_pos then
combine (p1::r1) (omega::r2) rem1 l2
else if lbl1.lbl_pos > lbl2.lbl_pos then
combine (omega::r1) (p2::r2) l1 rem2
else (* same label on both sides *)
combine (p1::r1) (p2::r2) rem1 rem2 in
combine [] [] l1 l2
;;
let sort_record p = match p.pat_desc with
| Tpat_record args ->
make_pat
(Tpat_record
(Sort.list
(fun (lbl1,_) (lbl2,_) ->
lbl1.lbl_pos <= lbl2.lbl_pos)
args))
(Tpat_record (sort_fields args))
p.pat_type p.pat_env
| _ -> p
@ -377,21 +395,11 @@ let full_match tdefs force env = match env with
ok && List.mem_assoc tag fields)
true row.row_fields
end else
if row.row_closed then
List.for_all
(fun (tag,f) ->
Btype.row_field_repr f = Rabsent || List.mem_assoc tag fields)
row.row_fields
else begin
List.iter
(fun (tag,f) ->
match Btype.row_field_repr f with
| Reither(true, [], e) -> e := Some (Rpresent None)
| Reither(false, [t], e) -> e := Some (Rpresent (Some t))
| _ -> ())
row.row_fields;
false
end
row.row_closed &&
List.for_all
(fun (tag,f) ->
Btype.row_field_repr f = Rabsent || List.mem_assoc tag fields)
row.row_fields
| ({pat_desc = Tpat_constant(Const_char _)},_) :: _ ->
List.length env = 256
| ({pat_desc = Tpat_constant(_)},_) :: _ -> false
@ -666,11 +674,11 @@ let rec initial_matrix = function
let rec le_pat p q =
match (p.pat_desc, q.pat_desc) with
(Tpat_var _ | Tpat_any), _ -> true
| Tpat_var _,_ -> true | Tpat_any, _ -> true
| Tpat_alias(p,_), _ -> le_pat p q
| _, Tpat_alias(q,_) -> le_pat p q
| Tpat_or(p1,p2), _ -> le_pat p1 q or le_pat p2 q
| _, Tpat_or(q1,q2) -> le_pat p q1 & le_pat p q2
| Tpat_or(p1,p2), _ -> le_pat p1 q || le_pat p2 q
| _, Tpat_or(q1,q2) -> le_pat p q1 && le_pat p q2
| Tpat_constant(c1), Tpat_constant(c2) -> c1 = c2
| Tpat_construct(c1,ps), Tpat_construct(c2,qs) ->
c1.cstr_tag = c2.cstr_tag && le_pats ps qs
@ -700,8 +708,35 @@ let get_mins ps =
else select_rec (p::r) ps in
select_rec [] (select_rec [] ps)
let rec compat p q = match p.pat_desc,q.pat_desc with
| Tpat_alias (p,_),_ -> compat p q
| _,Tpat_alias (q,_) -> compat p q
| (Tpat_any|Tpat_var _),_ -> true
| _,(Tpat_any|Tpat_var _) -> true
| Tpat_or (p1,p2),_ -> compat p1 q || compat p2 q
| _,Tpat_or (q1,q2) -> compat p q1 || compat p q2
| Tpat_constant c1, Tpat_constant c2 -> c1=c2
| Tpat_tuple ps, Tpat_tuple qs -> compats ps qs
| Tpat_construct (c1,ps1), Tpat_construct (c2,ps2) ->
c1.cstr_tag = c2.cstr_tag && compats ps1 ps2
| Tpat_variant(l1,Some p1,_), Tpat_variant(l2,Some p2,_) ->
l1=l2 && compat p1 p2
| Tpat_variant (l1,None,_), Tpat_variant(l2,None,_) -> l1 = l2
| Tpat_variant (_, None, _), Tpat_variant (_,Some _, _) -> false
| Tpat_variant (_, Some _, _), Tpat_variant (_, None, _) -> false
| Tpat_record l1,Tpat_record l2 ->
let ps,qs = records_args l1 l2 in
compats ps qs
| Tpat_array ps, Tpat_array qs ->
List.length ps = List.length qs &&
compats ps qs
| _,_ -> assert false
and compats ps qs = match ps,qs with
| [], [] -> true
| p::ps, q::qs -> compat p q && compats ps qs
| _,_ -> assert false
(*************************************)
(* Values as patterns pretty printer *)
(*************************************)
@ -805,63 +840,75 @@ let top_pretty ppf v =
(******************************)
(* Exported functions *)
(* Entry points *)
(* - Partial match *)
(* - Unused match case *)
(******************************)
let check_partial tdefs loc casel =
let pss = get_mins (initial_matrix casel) in
let r = match pss with
| [] -> begin match casel with
| [] -> Rnone
| (p,_) :: _ -> Rsome [p]
end
| ps::_ -> satisfiable tdefs true pss (omega_list ps) in
match r with
| Rnone -> Total
| Rok ->
Location.prerr_warning loc (Warnings.Partial_match "");
Partial
| Rsome [v] ->
let errmsg =
try
let buf = Buffer.create 16 in
let fmt = formatter_of_buffer buf in
top_pretty fmt v;
Buffer.contents buf
with _ ->
"" in
Location.prerr_warning loc (Warnings.Partial_match errmsg);
Partial
| _ ->
fatal_error "Parmatch.check_partial"
if not (Warnings.is_active (Warnings.Partial_match "")) then
Partial
else
let pss = get_mins (initial_matrix casel) in
match pss with
| [] ->
(*
This can occur
- For empty matches generated by ocamlp4
- when all patterns have guards
Then match should be considered non-exhaustive
(cf. matching.ml) no warning is issued,
users should know what they do
*)
Partial
| ps::_ ->
match satisfiable tdefs true pss (omega_list ps) with
| Rnone -> Total
| Rok ->
Location.prerr_warning loc (Warnings.Partial_match "");
Partial
| Rsome [v] ->
let errmsg =
try
let buf = Buffer.create 16 in
let fmt = formatter_of_buffer buf in
top_pretty fmt v;
Buffer.contents buf
with _ ->
"" in
Location.prerr_warning loc (Warnings.Partial_match errmsg);
Partial
| _ ->
fatal_error "Parmatch.check_partial"
let location_of_clause = function
pat :: _ -> pat.pat_loc
| _ -> fatal_error "Parmatch.location_of_clause"
let check_unused tdefs casel =
let prefs =
List.fold_right
(fun (pat,act as clause) r ->
if has_guard act
then ([], ([pat], act)) :: r
else ([], ([pat], act)) ::
List.map (fun (pss,clause) -> [pat]::pss,clause) r)
casel [] in
List.iter
(fun (pss, ((qs, _) as clause)) ->
try
if
(match satisfiable tdefs false pss qs with
| Rnone -> true
| Rok -> false
| _ -> assert false)
then
Location.prerr_warning (location_of_clause qs) Warnings.Unused_match
with e ->
Location.prerr_warning (location_of_clause qs)
(Warnings.Other "Fatal Error") ;
raise e)
prefs
if Warnings.is_active Warnings.Unused_match then begin
let prefs =
List.fold_right
(fun (pat,act as clause) r ->
if has_guard act
then ([], ([pat], act)) :: r
else ([], ([pat], act)) ::
List.map (fun (pss,clause) -> [pat]::pss,clause) r)
casel [] in
List.iter
(fun (pss, ((qs, _) as clause)) ->
try
if
(match satisfiable tdefs false pss qs with
| Rnone -> true
| Rok -> false
| _ -> assert false)
then
Location.prerr_warning
(location_of_clause qs) Warnings.Unused_match
with e ->
Location.prerr_warning (location_of_clause qs)
(Warnings.Other "Fatal Error") ;
raise e)
prefs
end

View File

@ -16,6 +16,12 @@
open Typedtree
val omega_list : 'a list -> pattern list
val compat : pattern -> pattern -> bool
val compats : pattern list -> pattern list -> bool
val check_partial:
Env.t -> Location.t -> (pattern * expression) list -> partial
val check_unused: Env.t -> (pattern * expression) list -> unit