浏览代码

consider infinite sets exhaustive only if they are the toplevel match subject (closes #2303)

Simon Krajewski 12 年之前
父节点
当前提交
3ac276da5b
共有 1 个文件被更改,包括 9 次插入9 次删除
  1. 9 9
      matcher.ml

+ 9 - 9
matcher.ml

@@ -827,7 +827,7 @@ let get_cache mctx dt =
 		DynArray.add mctx.dt_lut dt;
 		dt
 
-let rec compile mctx stl pmat =
+let rec compile mctx stl pmat toplevel =
 	let guard e dt1 dt2 = get_cache mctx (Guard(e,dt1,dt2)) in
 	let expr e = get_cache mctx (Expr e) in
 	let bind bl dt = get_cache mctx (Bind(bl,dt)) in
@@ -848,7 +848,7 @@ let rec compile mctx stl pmat =
 		| _ ->
 			assert false)
 	| ([|{p_def = PTuple pt}|],out) :: pl ->
-		compile mctx stl ((pt,out) :: pl)
+		compile mctx stl ((pt,out) :: pl) toplevel
 	| (pv,out) :: pl ->
 		let i = pick_column pmat in
 		if i = -1 then begin
@@ -856,13 +856,13 @@ let rec compile mctx stl pmat =
 			let bl = bind_remaining out pv stl in
 			let dt = match out.o_guard with
 				| None -> expr out.o_expr
-				| Some e -> guard e (expr out.o_expr) (match pl with [] -> None | _ -> Some (compile mctx stl pl))
+				| Some e -> guard e (expr out.o_expr) (match pl with [] -> None | _ -> Some (compile mctx stl pl false))
 			in
 			(if bl = [] then dt else bind bl dt)
 		end else if i > 0 then begin
 			let pmat = swap_pmat_columns i pmat in
 			let stls = swap_columns i stl in
-			compile mctx stls pmat
+			compile mctx stls pmat toplevel
 		end else begin
 			let st_head,st_tail = match stl with st :: stl -> st,stl | _ -> assert false in
 			let sigma,bl = column_sigma mctx st_head pmat in
@@ -872,7 +872,7 @@ let rec compile mctx stl pmat =
 				let spec = spec mctx c pmat in
 				let hsubs = mk_subs st_head c in
 				let subs = hsubs @ st_tail in
-				let dt = compile mctx subs spec in
+				let dt = compile mctx subs spec false in
 				c,dt
 			) sigma in
 			let def = default mctx pmat in
@@ -881,7 +881,7 @@ let rec compile mctx stl pmat =
 				switch st_head cases
 			| _ when not inf && PMap.is_empty !all ->
 				switch st_head cases
-			| [],_ when inf && not mctx.need_val ->
+			| [],_ when inf && not mctx.need_val && toplevel ->
 				switch st_head cases
 			| [],_ when inf ->
 				raise (Not_exhaustive(any,st_head))
@@ -889,10 +889,10 @@ let rec compile mctx stl pmat =
 				let pl = PMap.foldi (fun cd p acc -> (mk_con_pat cd [] t_dynamic p) :: acc) !all [] in
 				raise (Not_exhaustive(collapse_pattern pl,st_head))
 			| def,[] ->
-				compile mctx st_tail def
+				compile mctx st_tail def false
 			| def,_ ->
 				let cdef = mk_con CAny t_dynamic st_head.st_pos in
-				let cases = cases @ [cdef,compile mctx st_tail def] in
+				let cases = cases @ [cdef,compile mctx st_tail def false] in
 				switch st_head cases
 			in
 			if bl = [] then dt else bind bl dt
@@ -1210,7 +1210,7 @@ let match_expr ctx e cases def with_type p =
 	in
 	let dt = try
 		(* compile decision tree *)
-		compile mctx stl pl
+		compile mctx stl pl true
 	with Not_exhaustive(pat,st) ->
  		let rec s_st_r top pre st v = match st.st_def with
  			| SVar v1 ->