1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
open Lang
module Make (M : sig
val get_old_name : string -> string
module Error : sig
exception Const_rebind of string
exception Sugar_lack_args of string * string list
exception Useless_if_cond of expr
exception Useless_match_cond of expr
exception Apply_anon_const
exception Useless_if_expr of expr
exception Useless_match_expr of expr
exception Useless_match_onecase of expr
end
module Pp : sig
val get_args_nosugar : expr -> string list
end
end) =
struct
let rec expr = function
| Const _ ->
()
| Bind (id, e1, e2) ->
( match e1 with
| Const _ ->
raise @@ M.Error.Const_rebind (M.get_old_name id)
| _ ->
() ) ;
let args = M.Pp.get_args_nosugar e1 in
if not (args = []) then
raise
@@ M.Error.Sugar_lack_args
(M.get_old_name id, List.map M.get_old_name args) ;
expr e1 ;
expr e2
| Abstract (_, _, e) ->
expr e
| Apply (e1, e2) ->
( match e1 with
| Abstract _ ->
raise @@ M.Error.Apply_anon_const
| _ ->
() ) ;
expr e1 ; expr e2
| Match (origin, match_expr, cases) as e ->
( match match_expr with
| Const (Literal _) ->
raise
@@
if origin = Generated then M.Error.Useless_if_cond e
else M.Error.Useless_match_cond e
| _ ->
() ) ;
let cases_res = List.map snd cases in
List.iter expr (match_expr :: cases_res) ;
let diff = ref false in
( match cases_res with
| [] ->
failwith "internal error"
| [_] ->
raise @@ M.Error.Useless_match_onecase e
| x :: s ->
(* TODO: compare them in a better way... *)
List.iter (fun el -> if el <> x then diff := true) s ) ;
if not !diff then
raise
@@
if origin = Generated then M.Error.Useless_if_expr e
else M.Error.Useless_match_expr e
| Type (_id, _cons, e) ->
expr e
end