I fixed the heterogeneity in parentheses around constructors in
patterns.
This commit is contained in:
parent
4492117589
commit
2f6e17c837
@ -92,7 +92,7 @@ function buy_single(const action : action_buy_single ; const s : storage_type) :
|
||||
function main(const action : action ; const s : storage_type) : (list(operation) * storage_type) is
|
||||
block {skip} with
|
||||
case action of
|
||||
| Buy_single bs -> buy_single (bs , s)
|
||||
| Sell_single as -> sell_single (as , s)
|
||||
| Transfer_single at -> transfer_single (at , s)
|
||||
| Buy_single (bs) -> buy_single (bs , s)
|
||||
| Sell_single (as) -> sell_single (as , s)
|
||||
| Transfer_single (at) -> transfer_single (at , s)
|
||||
end
|
||||
|
@ -11,6 +11,6 @@ function decrement(const i : int ; const n : int) : int is
|
||||
function main (const p : action ; const s : int) : (list(operation) * int) is
|
||||
block {skip} with ((nil : list(operation)),
|
||||
case p of
|
||||
| Increment n -> increment(s , n)
|
||||
| Decrement n -> decrement(s , n)
|
||||
| Increment (n) -> increment (s, n)
|
||||
| Decrement (n) -> decrement (s, n)
|
||||
end)
|
||||
|
@ -12,7 +12,7 @@ function match_option (const o : option(int)) : int is
|
||||
begin
|
||||
case o of
|
||||
| None -> skip
|
||||
| Some(s) -> result := s
|
||||
| Some (s) -> result := s
|
||||
end
|
||||
end with result
|
||||
|
||||
@ -27,5 +27,5 @@ function match_expr_option (const o : option(int)) : int is
|
||||
begin skip end with
|
||||
case o of
|
||||
| None -> 42
|
||||
| Some(s) -> s
|
||||
| Some (s) -> s
|
||||
end
|
||||
|
@ -5,6 +5,6 @@ type action is
|
||||
function main (const p : action ; const s : int) : (list(operation) * int) is
|
||||
block {skip} with ((nil : list(operation)),
|
||||
case p of
|
||||
| Increment n -> s + n
|
||||
| Decrement n -> s - n
|
||||
| Increment (n) -> s + n
|
||||
| Decrement (n) -> s - n
|
||||
end)
|
||||
|
@ -13,6 +13,6 @@ function subtract (const a : int ; const b : int) : int is
|
||||
function main (const p : action ; const s : int) : (list(operation) * int) is
|
||||
block {skip} with ((nil : list(operation)),
|
||||
case p of
|
||||
| Increment n -> add(s, n)
|
||||
| Decrement n -> subtract(s, n)
|
||||
| Increment (n) -> add (s, n)
|
||||
| Decrement (n) -> subtract (s, n)
|
||||
end)
|
||||
|
@ -632,7 +632,7 @@ and arguments = tuple_injection
|
||||
|
||||
and pattern =
|
||||
PCons of (pattern, cons) nsepseq reg
|
||||
| PConstr of (constr * pattern reg) reg
|
||||
| PConstr of (constr * tuple_pattern option) reg
|
||||
| PVar of Lexer.lexeme reg
|
||||
| PWild of wild
|
||||
| PInt of (Lexer.lexeme * Z.t) reg
|
||||
@ -644,7 +644,9 @@ and pattern =
|
||||
| PNone of c_None
|
||||
| PSome of (c_Some * pattern par reg) reg
|
||||
| PList of list_pattern
|
||||
| PTuple of (pattern, comma) nsepseq par reg
|
||||
| PTuple of tuple_pattern
|
||||
|
||||
and tuple_pattern = (pattern, comma) nsepseq par reg
|
||||
|
||||
and list_pattern =
|
||||
Sugar of pattern injection reg
|
||||
|
@ -616,7 +616,7 @@ and arguments = tuple_injection
|
||||
|
||||
and pattern =
|
||||
PCons of (pattern, cons) nsepseq reg
|
||||
| PConstr of (constr * pattern reg) reg
|
||||
| PConstr of (constr * tuple_pattern option) reg
|
||||
| PVar of Lexer.lexeme reg
|
||||
| PWild of wild
|
||||
| PInt of (Lexer.lexeme * Z.t) reg
|
||||
@ -628,7 +628,9 @@ and pattern =
|
||||
| PNone of c_None
|
||||
| PSome of (c_Some * pattern par reg) reg
|
||||
| PList of list_pattern
|
||||
| PTuple of (pattern, comma) nsepseq par reg
|
||||
| PTuple of tuple_pattern
|
||||
|
||||
and tuple_pattern = (pattern, comma) nsepseq par reg
|
||||
|
||||
and list_pattern =
|
||||
Sugar of pattern injection reg
|
||||
|
@ -1060,14 +1060,14 @@ core_pattern:
|
||||
| C_False { PFalse $1 }
|
||||
| C_True { PTrue $1 }
|
||||
| C_None { PNone $1 }
|
||||
| list_patt { PList $1 }
|
||||
| tuple_patt { PTuple $1 }
|
||||
| constr_patt { PConstr $1 }
|
||||
| list_pattern { PList $1 }
|
||||
| tuple_pattern { PTuple $1 }
|
||||
| constr_pattern { PConstr $1 }
|
||||
| C_Some par(core_pattern) {
|
||||
let region = cover $1 $2.region
|
||||
in PSome {region; value = $1,$2}}
|
||||
|
||||
list_patt:
|
||||
list_pattern:
|
||||
injection(List,core_pattern) { Sugar $1 }
|
||||
| Nil { PNil $1 }
|
||||
| par(cons_pattern) { Raw $1 }
|
||||
@ -1075,15 +1075,14 @@ list_patt:
|
||||
cons_pattern:
|
||||
core_pattern CONS pattern { $1,$2,$3 }
|
||||
|
||||
tuple_patt:
|
||||
tuple_pattern:
|
||||
par(nsepseq(core_pattern,COMMA)) { $1 }
|
||||
|
||||
constr_patt:
|
||||
Constr core_pattern {
|
||||
let second =
|
||||
let region = pattern_to_region $2 in
|
||||
{region; value=$2}
|
||||
in
|
||||
let region = cover $1.region second.region in
|
||||
let value = ($1 , second) in
|
||||
{region; value}}
|
||||
constr_pattern:
|
||||
Constr tuple_pattern {
|
||||
let region = cover $1.region $2.region
|
||||
in {region; value = $1, Some $2}
|
||||
}
|
||||
| Constr {
|
||||
{region=$1.region; value = $1, None}
|
||||
}
|
||||
|
@ -681,8 +681,10 @@ and print_pattern = function
|
||||
|
||||
and print_constr_pattern {value; _} =
|
||||
let (constr, args) = value in
|
||||
print_constr constr ;
|
||||
print_pattern args.value ;
|
||||
print_constr constr;
|
||||
match args with
|
||||
None -> ()
|
||||
| Some tuple -> print_ptuple tuple
|
||||
|
||||
and print_psome {value; _} =
|
||||
let c_Some, patterns = value in
|
||||
|
@ -15,6 +15,17 @@ let pseq_to_list = function
|
||||
let get_value : 'a Raw.reg -> 'a = fun x -> x.value
|
||||
|
||||
module Errors = struct
|
||||
let unsupported_cst_constr p =
|
||||
let title () = "constant constructor" in
|
||||
let message () =
|
||||
Format.asprintf "constant constructors are not supported yet" in
|
||||
let pattern_loc = Raw.pattern_to_region p in
|
||||
let data = [
|
||||
("pattern_loc",
|
||||
fun () -> Format.asprintf "%a" Location.pp_lift @@ pattern_loc)
|
||||
] in
|
||||
error ~data title message
|
||||
|
||||
let unsupported_ass_None region =
|
||||
let title () = "assignment of None" in
|
||||
let message () =
|
||||
@ -848,33 +859,37 @@ and simpl_cases : type a . (Raw.pattern * a) list -> a matching result = fun t -
|
||||
let get_var (t:Raw.pattern) =
|
||||
match t with
|
||||
| PVar v -> ok v.value
|
||||
| p -> fail @@ unsupported_non_var_pattern p
|
||||
in
|
||||
let get_tuple (t:Raw.pattern) = match t with
|
||||
| p -> fail @@ unsupported_non_var_pattern p in
|
||||
let get_tuple (t: Raw.pattern) =
|
||||
match t with
|
||||
| PCons v -> npseq_to_list v.value
|
||||
| PTuple v -> npseq_to_list v.value.inside
|
||||
| x -> [ x ]
|
||||
in
|
||||
let get_single (t:Raw.pattern) =
|
||||
| x -> [ x ] in
|
||||
let get_single (t: Raw.pattern) =
|
||||
let t' = get_tuple t in
|
||||
let%bind () =
|
||||
trace_strong (unsupported_tuple_pattern t) @@
|
||||
Assert.assert_list_size t' 1 in
|
||||
ok (List.hd t') in
|
||||
let get_constr (t:Raw.pattern) = match t with
|
||||
| PConstr v ->
|
||||
let%bind var = get_single (snd v.value).value >>? get_var in
|
||||
ok ((fst v.value).value , var)
|
||||
| _ -> fail @@ only_constructors t
|
||||
in
|
||||
let get_constr (t: Raw.pattern) =
|
||||
match t with
|
||||
| PConstr v -> (
|
||||
let (const , pat_opt) = v.value in
|
||||
let%bind pat =
|
||||
trace_option (unsupported_cst_constr t) @@
|
||||
pat_opt in
|
||||
let%bind single_pat = get_single (PTuple pat) in
|
||||
let%bind var = get_var single_pat in
|
||||
ok (const.value , var)
|
||||
)
|
||||
| _ -> fail @@ only_constructors t in
|
||||
let%bind patterns =
|
||||
let aux (x , y) =
|
||||
let xs = get_tuple x in
|
||||
trace_strong (unsupported_tuple_pattern x) @@
|
||||
Assert.assert_list_size xs 1 >>? fun () ->
|
||||
ok (List.hd xs , y)
|
||||
in
|
||||
bind_map_list aux t in
|
||||
in bind_map_list aux t in
|
||||
match patterns with
|
||||
| [(PFalse _ , f) ; (PTrue _ , t)]
|
||||
| [(PTrue _ , t) ; (PFalse _ , f)] ->
|
||||
|
Loading…
Reference in New Issue
Block a user