reduce expression_eq to equal variable
This commit is contained in:
Pierre-Emmanuel Wulfman
Tom Jack
parent
1cbadbc7cf
commit
2a8edb53da
@ -528,104 +528,7 @@ let program_environment (program : program) : full_environment =
|
|||||||
match last_declaration with
|
match last_declaration with
|
||||||
| Declaration_constant { binder=_ ; expr=_ ; inline=_ ; post_env } -> post_env
|
| Declaration_constant { binder=_ ; expr=_ ; inline=_ ; post_env } -> post_env
|
||||||
|
|
||||||
let rec expression_eq a b : bool =
|
let expression_eq a b : bool =
|
||||||
match a.expression_content, b.expression_content with
|
match a.expression_content, b.expression_content with
|
||||||
| E_literal a, E_literal b -> literal_eq a b
|
|
||||||
| E_literal _, _ -> false
|
|
||||||
| E_constant {cons_name=ca;arguments=lsta}, E_constant {cons_name=cb;arguments=lstb} when ca == cb ->
|
|
||||||
let lst = List.combine lsta lstb in
|
|
||||||
let aux res (a,b) = res && expression_eq a b in
|
|
||||||
List.fold_left aux true lst
|
|
||||||
| E_constant _, _ -> false
|
|
||||||
| E_constructor {constructor=ca;element=ea}, E_constructor {constructor=cb;element=eb} when ca = cb ->
|
|
||||||
expression_eq ea eb
|
|
||||||
| E_constructor _, _ -> false
|
|
||||||
| E_variable a, E_variable b -> Var.equal a b
|
| E_variable a, E_variable b -> Var.equal a b
|
||||||
| E_variable _, _ -> false
|
| _, _ -> false
|
||||||
| E_application {lamb=a;args=la}, E_application {lamb=b;args=lb} ->
|
|
||||||
expression_eq a b && expression_eq la lb
|
|
||||||
| E_application _, _ -> false
|
|
||||||
| E_lambda {binder=ba;result=ra}, E_lambda {binder=bb;result=rb} ->
|
|
||||||
Var.equal ba bb && expression_eq ra rb
|
|
||||||
| E_lambda _, _ -> false
|
|
||||||
| E_recursive {fun_name=na;fun_type=_;lambda={binder=ba;result=ra}},
|
|
||||||
E_recursive {fun_name=nb;fun_type=_;lambda={binder=bb;result=rb}} ->
|
|
||||||
Var.equal na nb && Var.equal ba bb && expression_eq ra rb
|
|
||||||
| E_recursive _,_ -> false
|
|
||||||
| E_let_in {let_binder=na;rhs=ra;let_result=la;_}, E_let_in {let_binder=nb;rhs=rb;let_result=lb;_} ->
|
|
||||||
Var.equal na nb && expression_eq ra rb && expression_eq la lb
|
|
||||||
| E_let_in _,_ -> false
|
|
||||||
| E_record ra, E_record rb ->
|
|
||||||
let la = LMap.to_kv_list ra in
|
|
||||||
let lb = LMap.to_kv_list rb in
|
|
||||||
let lst = List.combine la lb in
|
|
||||||
let aux res ((Label ka,va),(Label kb,vb)) =
|
|
||||||
res && String.equal ka kb && expression_eq va vb
|
|
||||||
in
|
|
||||||
List.fold_left aux true lst
|
|
||||||
| E_record _,_ -> false
|
|
||||||
| E_record_accessor {record=ra;path=Label la}, E_record_accessor {record=rb;path=Label lb} ->
|
|
||||||
expression_eq ra rb && String.equal la lb
|
|
||||||
| E_record_accessor _, _ -> false
|
|
||||||
| E_record_update {record=ra;path=Label la;update=ua}, E_record_update {record=rb;path=Label lb; update=ub} ->
|
|
||||||
expression_eq ra rb && String.equal la lb && expression_eq ua ub
|
|
||||||
| E_record_update _, _ -> false
|
|
||||||
| E_matching {matchee=ma;cases=ca}, E_matching {matchee=mb;cases=cb} ->
|
|
||||||
expression_eq ma mb && matching_eq ca cb
|
|
||||||
| E_matching _, _ -> false
|
|
||||||
|
|
||||||
and literal_eq la lb :bool =
|
|
||||||
match (la,lb) with
|
|
||||||
| Literal_bool a, Literal_bool b -> a = b
|
|
||||||
| Literal_bool _, _ -> false
|
|
||||||
| Literal_int a, Literal_int b -> a = b
|
|
||||||
| Literal_int _, _ -> false
|
|
||||||
| Literal_nat a, Literal_nat b -> a = b
|
|
||||||
| Literal_nat _, _ -> false
|
|
||||||
| Literal_timestamp a, Literal_timestamp b -> a = b
|
|
||||||
| Literal_timestamp _, _ -> false
|
|
||||||
| Literal_mutez a, Literal_mutez b -> a = b
|
|
||||||
| Literal_mutez _, _ -> false
|
|
||||||
| Literal_string a, Literal_string b -> a = b
|
|
||||||
| Literal_string _, _ -> false
|
|
||||||
| Literal_bytes a, Literal_bytes b -> a = b
|
|
||||||
| Literal_bytes _, _ -> false
|
|
||||||
| Literal_void, Literal_void -> true
|
|
||||||
| Literal_void, _ -> false
|
|
||||||
| Literal_unit, Literal_unit -> true
|
|
||||||
| Literal_unit, _ -> false
|
|
||||||
| Literal_address a, Literal_address b -> a = b
|
|
||||||
| Literal_address _, _ -> false
|
|
||||||
| Literal_signature a, Literal_signature b -> a = b
|
|
||||||
| Literal_signature _, _ -> false
|
|
||||||
| Literal_key a, Literal_key b -> a = b
|
|
||||||
| Literal_key _, _ -> false
|
|
||||||
| Literal_key_hash a, Literal_key_hash b -> a = b
|
|
||||||
| Literal_key_hash _, _ -> false
|
|
||||||
| Literal_chain_id a, Literal_chain_id b -> a = b
|
|
||||||
| Literal_chain_id _, _ -> false
|
|
||||||
| Literal_operation _, _ -> false
|
|
||||||
|
|
||||||
and matching_eq ma mb : bool =
|
|
||||||
match (ma,mb) with
|
|
||||||
| Match_bool {match_true=ta;match_false=fa}, Match_bool {match_true=tb;match_false=fb} ->
|
|
||||||
expression_eq ta tb && expression_eq fa fb
|
|
||||||
| Match_bool _, _ -> false
|
|
||||||
| Match_option {match_some={opt=a;body=sa;_};match_none=na}, Match_option {match_some={opt=b;body=sb;_};match_none=nb} ->
|
|
||||||
Var.equal a b && expression_eq sa sb && expression_eq na nb
|
|
||||||
| Match_option _, _ -> false
|
|
||||||
| Match_list {match_nil=na;match_cons={hd=a;tl=aa;body=ca;_}}, Match_list {match_nil=nb;match_cons={hd=b;tl=bb;body=cb;_}} ->
|
|
||||||
expression_eq na nb && Var.equal a b && Var.equal aa bb && expression_eq ca cb
|
|
||||||
| Match_list _, _ -> false
|
|
||||||
| Match_tuple {vars=la;body=a;_}, Match_tuple {vars=lb;body=b;_} ->
|
|
||||||
let lst = List.combine la lb in
|
|
||||||
let aux res (a,b) = res && Var.equal a b in
|
|
||||||
List.fold_left aux (expression_eq a b) lst
|
|
||||||
| Match_tuple _, _ -> false
|
|
||||||
| Match_variant {cases=la;_}, Match_variant {cases=lb;_} ->
|
|
||||||
let lst = List.combine la lb in
|
|
||||||
let aux res ({constructor=Constructor ca;pattern=va;body=a}, {constructor=Constructor cb;pattern=vb;body=b}) =
|
|
||||||
res && String.equal ca cb && Var.equal va vb && expression_eq a b
|
|
||||||
in
|
|
||||||
List.fold_left aux true lst
|
|
||||||
| Match_variant _, _ -> false
|
|
||||||
|
|||||||
Loading…
Reference in New Issue
Block a user