add expression pattern-matching

This commit is contained in:
Galfour 2019-03-31 11:55:52 +00:00
parent c7a7f0065a
commit f8dcca8a12
11 changed files with 287 additions and 106 deletions

View File

@ -66,6 +66,8 @@ and expression =
(* Data Structures *) (* Data Structures *)
| Map of (ae * ae) list | Map of (ae * ae) list
| LookUp of (ae * ae) | LookUp of (ae * ae)
(* Matching *)
| Matching_expr of (ae * matching_expr)
and access = and access =
| Tuple_access of int | Tuple_access of int
@ -85,26 +87,30 @@ and b = block
and instruction = and instruction =
| Assignment of named_expression | Assignment of named_expression
| Matching of ae * matching | Matching_instr of ae * matching_instr
| Loop of ae * b | Loop of ae * b
| Skip | Skip
| Fail of ae | Fail of ae
| Record_patch of name * access_path * (string * ae) list | Record_patch of name * access_path * (string * ae) list
and matching = and 'a matching =
| Match_bool of { | Match_bool of {
match_true : b ; match_true : 'a ;
match_false : b ; match_false : 'a ;
} }
| Match_list of { | Match_list of {
match_nil : b ; match_nil : 'a ;
match_cons : name * name * b ; match_cons : name * name * 'a ;
} }
| Match_option of { | Match_option of {
match_none : b ; match_none : 'a ;
match_some : name * b ; match_some : name * 'a ;
} }
| Match_tuple of name list * b | Match_tuple of name list * 'a
and matching_instr = b matching
and matching_expr = annotated_expression matching
let ae expression = {expression ; type_annotation = None} let ae expression = {expression ; type_annotation = None}
@ -146,6 +152,8 @@ module PP = struct
fprintf ppf "lambda (%s:%a) : %a {%a} return %a" fprintf ppf "lambda (%s:%a) : %a {%a} return %a"
binder type_expression input_type type_expression output_type binder type_expression input_type type_expression output_type
block body annotated_expression result block body annotated_expression result
| Matching_expr (ae, m) ->
fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m
and assoc_annotated_expression ppf : (ae * ae) -> unit = fun (a, b) -> and assoc_annotated_expression ppf : (ae * ae) -> unit = fun (a, b) ->
fprintf ppf "%a -> %a" annotated_expression a annotated_expression b fprintf ppf "%a -> %a" annotated_expression a annotated_expression b
@ -171,15 +179,16 @@ module PP = struct
and single_record_patch ppf ((p, ae) : string * ae) = and single_record_patch ppf ((p, ae) : string * ae) =
fprintf ppf "%s <- %a" p annotated_expression ae fprintf ppf "%s <- %a" p annotated_expression ae
and matching ppf (m:matching) = match m with and matching : type a . (formatter -> a -> unit) -> formatter -> a matching -> unit =
fun f ppf m -> match m with
| Match_tuple (lst, b) -> | Match_tuple (lst, b) ->
fprintf ppf "let (%a) = %a" (list_sep (fun ppf -> fprintf ppf "%s")) lst block b fprintf ppf "let (%a) = %a" (list_sep (fun ppf -> fprintf ppf "%s")) lst f b
| Match_bool {match_true ; match_false} -> | Match_bool {match_true ; match_false} ->
fprintf ppf "| True -> %a @.| False -> %a" block match_true block match_false fprintf ppf "| True -> %a @.| False -> %a" f match_true f match_false
| Match_list {match_nil ; match_cons = (hd, tl, match_cons)} -> | Match_list {match_nil ; match_cons = (hd, tl, match_cons)} ->
fprintf ppf "| Nil -> %a @.| %s :: %s -> %a" block match_nil hd tl block match_cons fprintf ppf "| Nil -> %a @.| %s :: %s -> %a" f match_nil hd tl f match_cons
| Match_option {match_none ; match_some = (some, match_some)} -> | Match_option {match_none ; match_some = (some, match_some)} ->
fprintf ppf "| None -> %a @.| Some %s -> %a" block match_none some block match_some fprintf ppf "| None -> %a @.| Some %s -> %a" f match_none some f match_some
and instruction ppf (i:instruction) = match i with and instruction ppf (i:instruction) = match i with
| Skip -> fprintf ppf "skip" | Skip -> fprintf ppf "skip"
@ -188,8 +197,8 @@ module PP = struct
| Loop (cond, b) -> fprintf ppf "while (%a) { %a }" annotated_expression cond block b | Loop (cond, b) -> fprintf ppf "while (%a) { %a }" annotated_expression cond block b
| Assignment {name;annotated_expression = ae} -> | Assignment {name;annotated_expression = ae} ->
fprintf ppf "%s := %a" name annotated_expression ae fprintf ppf "%s := %a" name annotated_expression ae
| Matching (ae, m) -> | Matching_instr (ae, m) ->
fprintf ppf "match %a with %a" annotated_expression ae matching m fprintf ppf "match %a with %a" annotated_expression ae (matching block) m
let declaration ppf (d:declaration) = match d with let declaration ppf (d:declaration) = match d with
| Type_declaration {type_name ; type_expression = te} -> | Type_declaration {type_name ; type_expression = te} ->
@ -227,10 +236,10 @@ module Rename = struct
let%bind cond' = rename_annotated_expression r cond in let%bind cond' = rename_annotated_expression r cond in
let%bind body' = rename_block r body in let%bind body' = rename_block r body in
ok (Loop (cond', body')) ok (Loop (cond', body'))
| Matching (ae, m) -> | Matching_instr (ae, m) ->
let%bind ae' = rename_annotated_expression r ae in let%bind ae' = rename_annotated_expression r ae in
let%bind m' = rename_matching r m in let%bind m' = rename_matching rename_block r m in
ok (Matching (ae', m')) ok (Matching_instr (ae', m'))
| Record_patch (v, path, lst) -> | Record_patch (v, path, lst) ->
let aux (x, y) = let aux (x, y) =
let%bind y' = rename_annotated_expression (filter r v) y in let%bind y' = rename_annotated_expression (filter r v) y in
@ -246,29 +255,34 @@ module Rename = struct
and rename_block (r:renamings) (bl:block) : block result = and rename_block (r:renamings) (bl:block) : block result =
bind_map_list (rename_instruction r) bl bind_map_list (rename_instruction r) bl
and rename_matching (r:renamings) (m:matching) : matching result = and rename_matching : type a . (renamings -> a -> a result) -> renamings -> a matching -> a matching result =
fun f r m ->
match m with match m with
| Match_bool { match_true = mt ; match_false = mf } -> | Match_bool { match_true = mt ; match_false = mf } ->
let%bind match_true = rename_block r mt in let%bind match_true = f r mt in
let%bind match_false = rename_block r mf in let%bind match_false = f r mf in
ok (Match_bool {match_true ; match_false}) ok (Match_bool {match_true ; match_false})
| Match_option { match_none = mn ; match_some = (some, ms) } -> | Match_option { match_none = mn ; match_some = (some, ms) } ->
let%bind match_none = rename_block r mn in let%bind match_none = f r mn in
let%bind ms' = rename_block (filter r some) ms in let%bind ms' = f (filter r some) ms in
ok (Match_option {match_none ; match_some = (some, ms')}) ok (Match_option {match_none ; match_some = (some, ms')})
| Match_list { match_nil = mn ; match_cons = (hd, tl, mc) } -> | Match_list { match_nil = mn ; match_cons = (hd, tl, mc) } ->
let%bind match_nil = rename_block r mn in let%bind match_nil = f r mn in
let%bind mc' = rename_block (filters r [hd;tl]) mc in let%bind mc' = f (filters r [hd;tl]) mc in
ok (Match_list {match_nil ; match_cons = (hd, tl, mc')}) ok (Match_list {match_nil ; match_cons = (hd, tl, mc')})
| Match_tuple (lst, body) -> | Match_tuple (lst, body) ->
let%bind body' = rename_block (filters r lst) body in let%bind body' = f (filters r lst) body in
ok (Match_tuple (lst, body')) ok (Match_tuple (lst, body'))
and rename_matching_instruction = fun x -> rename_matching rename_block x
and rename_matching_expr = fun x -> rename_matching rename_expression x
and rename_annotated_expression (r:renamings) (ae:annotated_expression) : annotated_expression result = and rename_annotated_expression (r:renamings) (ae:annotated_expression) : annotated_expression result =
let%bind expression = rename_expression r ae.expression in let%bind expression = rename_expression r ae.expression in
ok {ae with expression} ok {ae with expression}
and rename_expression (r:renamings) (e:expression) : expression result = and rename_expression : renamings -> expression -> expression result = fun r e ->
match e with match e with
| Literal _ as l -> ok l | Literal _ as l -> ok l
| Constant (name, lst) -> | Constant (name, lst) ->
@ -315,6 +329,10 @@ module Rename = struct
| LookUp m -> | LookUp m ->
let%bind m' = bind_map_pair (rename_annotated_expression r) m in let%bind m' = bind_map_pair (rename_annotated_expression r) m in
ok (LookUp m') ok (LookUp m')
| Matching_expr (ae, m) ->
let%bind ae' = rename_annotated_expression r ae in
let%bind m' = rename_matching rename_annotated_expression r m in
ok (Matching_expr (ae', m'))
end end
end end

View File

@ -67,6 +67,8 @@ and expression =
(* Data Structures *) (* Data Structures *)
| Map of (ae * ae) list | Map of (ae * ae) list
| LookUp of (ae * ae) | LookUp of (ae * ae)
(* Advanced *)
| Matching_expr of (ae * matching_expr)
and value = annotated_expression (* todo (for refactoring) *) and value = annotated_expression (* todo (for refactoring) *)
@ -83,25 +85,29 @@ and b = block
and instruction = and instruction =
| Assignment of named_expression | Assignment of named_expression
| Matching of ae * matching | Matching_instr of ae * matching_instr
| Loop of ae * b | Loop of ae * b
| Skip | Skip
| Fail of ae | Fail of ae
and matching = and 'a matching =
| Match_bool of { | Match_bool of {
match_true : b ; match_true : 'a ;
match_false : b ; match_false : 'a ;
} }
| Match_list of { | Match_list of {
match_nil : b ; match_nil : 'a ;
match_cons : name * name * b ; match_cons : name * name * 'a ;
} }
| Match_option of { | Match_option of {
match_none : b ; match_none : 'a ;
match_some : (name * type_value) * b ; match_some : (name * type_value) * 'a ;
} }
| Match_tuple of name list * b | Match_tuple of name list * 'a
and matching_instr = b matching
and matching_expr = ae matching
open! Ligo_helpers.Trace open! Ligo_helpers.Trace
@ -165,6 +171,8 @@ module PP = struct
| Record m -> fprintf ppf "record[%a]" (smap_sep annotated_expression) m | Record m -> fprintf ppf "record[%a]" (smap_sep annotated_expression) m
| Map m -> fprintf ppf "map[%a]" (list_sep assoc_annotated_expression) m | Map m -> fprintf ppf "map[%a]" (list_sep assoc_annotated_expression) m
| LookUp (ds, i) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression i | LookUp (ds, i) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression i
| Matching_expr (ae, m) ->
fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m
and assoc_annotated_expression ppf : (ae * ae) -> unit = fun (a, b) -> and assoc_annotated_expression ppf : (ae * ae) -> unit = fun (a, b) ->
fprintf ppf "%a -> %a" annotated_expression a annotated_expression b fprintf ppf "%a -> %a" annotated_expression a annotated_expression b
@ -183,15 +191,15 @@ module PP = struct
and single_record_patch ppf ((s, ae) : string * ae) = and single_record_patch ppf ((s, ae) : string * ae) =
fprintf ppf "%s <- %a" s annotated_expression ae fprintf ppf "%s <- %a" s annotated_expression ae
and matching ppf (m:matching) = match m with and matching : type a . (formatter -> a -> unit) -> _ -> a matching -> unit = fun f ppf m -> match m with
| Match_tuple (lst, b) -> | Match_tuple (lst, b) ->
fprintf ppf "let (%a) = %a" (list_sep (fun ppf -> fprintf ppf "%s")) lst block b fprintf ppf "let (%a) = %a" (list_sep (fun ppf -> fprintf ppf "%s")) lst f b
| Match_bool {match_true ; match_false} -> | Match_bool {match_true ; match_false} ->
fprintf ppf "| True -> %a @.| False -> %a" block match_true block match_false fprintf ppf "| True -> %a @.| False -> %a" f match_true f match_false
| Match_list {match_nil ; match_cons = (hd, tl, match_cons)} -> | Match_list {match_nil ; match_cons = (hd, tl, match_cons)} ->
fprintf ppf "| Nil -> %a @.| %s :: %s -> %a" block match_nil hd tl block match_cons fprintf ppf "| Nil -> %a @.| %s :: %s -> %a" f match_nil hd tl f match_cons
| Match_option {match_none ; match_some = (some, match_some)} -> | Match_option {match_none ; match_some = (some, match_some)} ->
fprintf ppf "| None -> %a @.| Some %s -> %a" block match_none (fst some) block match_some fprintf ppf "| None -> %a @.| Some %s -> %a" f match_none (fst some) f match_some
and instruction ppf (i:instruction) = match i with and instruction ppf (i:instruction) = match i with
| Skip -> fprintf ppf "skip" | Skip -> fprintf ppf "skip"
@ -199,8 +207,8 @@ module PP = struct
| Loop (cond, b) -> fprintf ppf "while (%a) { %a }" annotated_expression cond block b | Loop (cond, b) -> fprintf ppf "while (%a) { %a }" annotated_expression cond block b
| Assignment {name;annotated_expression = ae} -> | Assignment {name;annotated_expression = ae} ->
fprintf ppf "%s := %a" name annotated_expression ae fprintf ppf "%s := %a" name annotated_expression ae
| Matching (ae, m) -> | Matching_instr (ae, m) ->
fprintf ppf "match %a with %a" annotated_expression ae matching m fprintf ppf "match %a with %a" annotated_expression ae (matching block) m
let declaration ppf (d:declaration) = let declaration ppf (d:declaration) =
match d with match d with

View File

@ -15,3 +15,10 @@ function match_option (const o : option(int)) : int is
| Some(s) -> result := s | Some(s) -> result := s
end end
end with result end with result
function match_expr_bool (const i : int) : int is
begin skip end with
case i = 2 of
| True -> 42
| False -> 0
end

View File

@ -345,7 +345,7 @@ and instruction =
and single_instr = and single_instr =
Cond of conditional reg Cond of conditional reg
| Case of case_instr reg | Case_instr of case_instr reg
| Assign of assignment reg | Assign of assignment reg
| Loop of loop | Loop of loop
| ProcCall of fun_call | ProcCall of fun_call
@ -430,18 +430,35 @@ and case_instr = {
expr : expr; expr : expr;
kwd_of : kwd_of; kwd_of : kwd_of;
lead_vbar : vbar option; lead_vbar : vbar option;
cases : cases; cases_instr : cases_instr;
kwd_end : kwd_end kwd_end : kwd_end
} }
and cases = (case reg, vbar) nsepseq reg and cases_instr = (case_clause_instr reg, vbar) nsepseq reg
and case = { and case_clause_instr = {
pattern : pattern; pattern : pattern;
arrow : arrow; arrow : arrow;
instr : instruction instr : instruction
} }
and case_expr = {
kwd_case : kwd_case;
expr : expr;
kwd_of : kwd_of;
lead_vbar : vbar option;
cases_expr: cases_expr;
kwd_end : kwd_end
}
and cases_expr = (case_clause_expr reg, vbar) nsepseq reg
and case_clause_expr = {
pattern : pattern;
arrow : arrow;
expr : expr;
}
and assignment = { and assignment = {
lhs : lhs; lhs : lhs;
assign : assign; assign : assign;
@ -498,7 +515,8 @@ and for_collect = {
(* Expressions *) (* Expressions *)
and expr = and expr =
ELogic of logic_expr | ECase of case_expr reg
| ELogic of logic_expr
| EArith of arith_expr | EArith of arith_expr
| EString of string_expr | EString of string_expr
| EList of list_expr | EList of list_expr
@ -683,7 +701,7 @@ let type_expr_to_region = function
| TAlias {region; _} -> region | TAlias {region; _} -> region
let rec expr_to_region = function let rec expr_to_region = function
ELogic e -> logic_expr_to_region e | ELogic e -> logic_expr_to_region e
| EArith e -> arith_expr_to_region e | EArith e -> arith_expr_to_region e
| EString e -> string_expr_to_region e | EString e -> string_expr_to_region e
| EList e -> list_expr_to_region e | EList e -> list_expr_to_region e
@ -697,6 +715,7 @@ let rec expr_to_region = function
| ECall {region; _} | ECall {region; _}
| EBytes {region; _} | EBytes {region; _}
| EUnit region | EUnit region
| ECase {region;_}
| EPar {region; _} -> region | EPar {region; _} -> region
and tuple_expr_to_region = function and tuple_expr_to_region = function
@ -761,7 +780,7 @@ let path_to_region = function
let instr_to_region = function let instr_to_region = function
Single Cond {region; _} Single Cond {region; _}
| Single Case {region; _} | Single Case_instr {region; _}
| Single Assign {region; _} | Single Assign {region; _}
| Single Loop While {region; _} | Single Loop While {region; _}
| Single Loop For ForInt {region; _} | Single Loop For ForInt {region; _}
@ -1087,7 +1106,7 @@ and print_instruction = function
and print_single_instr = function and print_single_instr = function
Cond {value; _} -> print_conditional value Cond {value; _} -> print_conditional value
| Case {value; _} -> print_case_instr value | Case_instr {value; _} -> print_case_instr value
| Assign assign -> print_assignment assign | Assign assign -> print_assignment assign
| Loop loop -> print_loop loop | Loop loop -> print_loop loop
| ProcCall fun_call -> print_fun_call fun_call | ProcCall fun_call -> print_fun_call fun_call
@ -1126,22 +1145,22 @@ and print_if_clause = function
and print_case_instr (node : case_instr) = and print_case_instr (node : case_instr) =
let {kwd_case; expr; kwd_of; let {kwd_case; expr; kwd_of;
lead_vbar; cases; kwd_end} = node in lead_vbar; cases_instr; kwd_end} = node in
print_token kwd_case "case"; print_token kwd_case "case";
print_expr expr; print_expr expr;
print_token kwd_of "of"; print_token kwd_of "of";
print_token_opt lead_vbar "|"; print_token_opt lead_vbar "|";
print_cases cases; print_cases_instr cases_instr;
print_token kwd_end "end" print_token kwd_end "end"
and print_token_opt = function and print_token_opt = function
None -> fun _ -> () None -> fun _ -> ()
| Some region -> print_token region | Some region -> print_token region
and print_cases {value; _} = and print_cases_instr {value; _} =
print_nsepseq "|" print_case value print_nsepseq "|" print_case_clause_instr value
and print_case {value; _} = and print_case_clause_instr {value; _} =
let {pattern; arrow; instr} = value in let {pattern; arrow; instr} = value in
print_pattern pattern; print_pattern pattern;
print_token arrow "->"; print_token arrow "->";
@ -1218,7 +1237,8 @@ and print_bind_to = function
| None -> () | None -> ()
and print_expr = function and print_expr = function
ELogic e -> print_logic_expr e ECase {value;_} -> print_case_expr value
| ELogic e -> print_logic_expr e
| EArith e -> print_arith_expr e | EArith e -> print_arith_expr e
| EString e -> print_string_expr e | EString e -> print_string_expr e
| EList e -> print_list_expr e | EList e -> print_list_expr e
@ -1234,6 +1254,25 @@ and print_expr = function
| ETuple e -> print_tuple_expr e | ETuple e -> print_tuple_expr e
| EPar e -> print_par_expr e | EPar e -> print_par_expr e
and print_case_expr (node : case_expr) =
let {kwd_case; expr; kwd_of;
lead_vbar; cases_expr; kwd_end} = node in
print_token kwd_case "case";
print_expr expr;
print_token kwd_of "of";
print_token_opt lead_vbar "|";
print_cases_expr cases_expr;
print_token kwd_end "end"
and print_cases_expr {value; _} =
print_nsepseq "|" print_case_clause_expr value
and print_case_clause_expr {value; _} =
let {pattern; arrow; expr} = value in
print_pattern pattern;
print_token arrow "->";
print_expr expr
and print_map_expr = function and print_map_expr = function
MapLookUp {value; _} -> print_map_lookup value MapLookUp {value; _} -> print_map_lookup value
| MapInj inj -> print_injection "map" print_binding inj | MapInj inj -> print_injection "map" print_binding inj

View File

@ -329,7 +329,7 @@ and instruction =
and single_instr = and single_instr =
Cond of conditional reg Cond of conditional reg
| Case of case_instr reg | Case_instr of case_instr reg
| Assign of assignment reg | Assign of assignment reg
| Loop of loop | Loop of loop
| ProcCall of fun_call | ProcCall of fun_call
@ -414,18 +414,35 @@ and case_instr = {
expr : expr; expr : expr;
kwd_of : kwd_of; kwd_of : kwd_of;
lead_vbar : vbar option; lead_vbar : vbar option;
cases : cases; cases_instr : cases_instr;
kwd_end : kwd_end kwd_end : kwd_end
} }
and cases = (case reg, vbar) nsepseq reg and cases_instr = (case_clause_instr reg, vbar) nsepseq reg
and case = { and case_clause_instr = {
pattern : pattern; pattern : pattern;
arrow : arrow; arrow : arrow;
instr : instruction instr : instruction
} }
and case_expr = {
kwd_case : kwd_case;
expr : expr;
kwd_of : kwd_of;
lead_vbar : vbar option;
cases_expr: cases_expr;
kwd_end : kwd_end
}
and cases_expr = (case_clause_expr reg, vbar) nsepseq reg
and case_clause_expr = {
pattern : pattern;
arrow : arrow;
expr : expr;
}
and assignment = { and assignment = {
lhs : lhs; lhs : lhs;
assign : assign; assign : assign;
@ -482,7 +499,8 @@ and for_collect = {
(* Expressions *) (* Expressions *)
and expr = and expr =
ELogic of logic_expr ECase of case_expr reg
| ELogic of logic_expr
| EArith of arith_expr | EArith of arith_expr
| EString of string_expr | EString of string_expr
| EList of list_expr | EList of list_expr

View File

@ -483,7 +483,7 @@ instruction:
single_instr: single_instr:
conditional { Cond $1 } conditional { Cond $1 }
| case_instr { Case $1 } | case_instr { Case_instr $1 }
| assignment { Assign $1 } | assignment { Assign $1 }
| loop { Loop $1 } | loop { Loop $1 }
| proc_call { ProcCall $1 } | proc_call { ProcCall $1 }
@ -672,23 +672,23 @@ if_clause:
ClauseBlock {value; region}} ClauseBlock {value; region}}
case_instr: case_instr:
Case expr Of option(VBAR) cases End { Case expr Of option(VBAR) cases_instr End {
let region = cover $1 $6 in let region = cover $1 $6 in
let value = { let value = {
kwd_case = $1; kwd_case = $1;
expr = $2; expr = $2;
kwd_of = $3; kwd_of = $3;
lead_vbar = $4; lead_vbar = $4;
cases = $5; cases_instr = $5;
kwd_end = $6} kwd_end = $6}
in {region; value}} in {region; value}}
cases: cases_instr:
nsepseq(case,VBAR) { nsepseq(case_clause_instr,VBAR) {
let region = nsepseq_to_region (fun x -> x.region) $1 let region = nsepseq_to_region (fun x -> x.region) $1
in {region; value = $1}} in {region; value = $1}}
case: case_clause_instr:
pattern ARROW instruction { pattern ARROW instruction {
let region = cover (pattern_to_region $1) (instr_to_region $3) let region = cover (pattern_to_region $1) (instr_to_region $3)
and value = {pattern = $1; arrow = $2; instr = $3} and value = {pattern = $1; arrow = $2; instr = $3}
@ -764,7 +764,34 @@ interactive_expr:
expr EOF { $1 } expr EOF { $1 }
expr: expr:
expr Or conj_expr { case_expr { $1 }
| disj_expr { $1 }
case_expr:
Case expr Of option(VBAR) cases_expr End {
let region = cover $1 $6 in
let value = {
kwd_case = $1;
expr = $2;
kwd_of = $3;
lead_vbar = $4;
cases_expr = $5;
kwd_end = $6}
in ECase {region; value}}
cases_expr:
nsepseq(case_clause_expr,VBAR) {
let region = nsepseq_to_region (fun x -> x.region) $1
in {region; value = $1}}
case_clause_expr:
pattern ARROW expr {
let region = cover (pattern_to_region $1) (expr_to_region $3)
and value = {pattern = $1; arrow = $2; expr = $3}
in {region; value}}
disj_expr:
disj_expr Or conj_expr {
let start = expr_to_region $1 let start = expr_to_region $1
and stop = expr_to_region $3 in and stop = expr_to_region $3 in
let region = cover start stop let region = cover start stop

View File

@ -70,6 +70,7 @@ and expression' =
| Var of var_name | Var of var_name
| Empty_map of (type_value * type_value) | Empty_map of (type_value * type_value)
| Make_None of type_value | Make_None of type_value
| E_Cond of expression * expression * expression
and expression = expression' * type_value * environment (* Environment in which the expressions are evaluated *) and expression = expression' * type_value * environment (* Environment in which the expressions are evaluated *)
@ -77,7 +78,7 @@ and assignment = var_name * expression
and statement' = and statement' =
| Assignment of assignment | Assignment of assignment
| Cond of expression * block * block | I_Cond of expression * block * block
| If_None of expression * block * (var_name * block) | If_None of expression * block * (var_name * block)
| While of expression * block | While of expression * block
@ -179,6 +180,7 @@ module PP = struct
| Function_expression c -> function_ ppf c | Function_expression c -> function_ ppf c
| Empty_map _ -> fprintf ppf "map[]" | Empty_map _ -> fprintf ppf "map[]"
| Make_None _ -> fprintf ppf "none" | Make_None _ -> fprintf ppf "none"
| E_Cond (c, a, b) -> fprintf ppf "%a ? %a : %a" expression c expression a expression b
and function_ ppf ({binder ; input ; output ; body ; result}:anon_function_content) = and function_ ppf ({binder ; input ; output ; body ; result}:anon_function_content) =
fprintf ppf "fun (%s:%a) : %a %a return %a" fprintf ppf "fun (%s:%a) : %a %a return %a"
@ -192,7 +194,7 @@ module PP = struct
and statement ppf ((s, _) : statement) = match s with and statement ppf ((s, _) : statement) = match s with
| Assignment ass -> assignment ppf ass | Assignment ass -> assignment ppf ass
| Cond (expr, i, e) -> fprintf ppf "if (%a) %a %a" expression expr block i block e | I_Cond (expr, i, e) -> fprintf ppf "if (%a) %a %a" expression expr block i block e
| If_None (expr, none, (name, some)) -> fprintf ppf "if (%a) %a %s.%a" expression expr block none name block some | If_None (expr, none, (name, some)) -> fprintf ppf "if (%a) %a %s.%a" expression expr block none name block some
| While (e, b) -> fprintf ppf "while (%a) %a" expression e block b | While (e, b) -> fprintf ppf "while (%a) %a" expression e block b
@ -823,7 +825,18 @@ module Translate_program = struct
] in ] in
ok code ok code
| _ -> simple_fail "expected function code" | _ -> simple_fail "expected function code"
) in )
| E_Cond (c, a, b) -> (
let%bind c' = translate_expression c in
let%bind a' = translate_expression a in
let%bind b' = translate_expression b in
let%bind code = ok (seq [
c' ; i_unpair ;
i_if a' b' ;
]) in
ok code
)
in
let%bind () = let%bind () =
let%bind (Ex_ty schema_ty) = Environment.to_ty env in let%bind (Ex_ty schema_ty) = Environment.to_ty env in
@ -874,7 +887,7 @@ module Translate_program = struct
add ; add ;
]; ];
]) ])
| Cond (expr, a, b) -> | I_Cond (expr, a, b) ->
let%bind expr = translate_expression expr in let%bind expr = translate_expression expr in
let%bind a = translate_regular_block a in let%bind a = translate_regular_block a in
let%bind b = translate_regular_block b in let%bind b = translate_regular_block b in
@ -1195,7 +1208,7 @@ module Combinators = struct
let statement s' e : statement = let statement s' e : statement =
match s' with match s' with
| Cond _ -> s', id_environment_wrap e | I_Cond _ -> s', id_environment_wrap e
| If_None _ -> s', id_environment_wrap e | If_None _ -> s', id_environment_wrap e
| While _ -> s', id_environment_wrap e | While _ -> s', id_environment_wrap e
| Assignment (name, (_, t, _)) -> s', environment_wrap e (Environment.add (name, t) e) | Assignment (name, (_, t, _)) -> s', environment_wrap e (Environment.add (name, t) e)

View File

@ -160,6 +160,18 @@ let rec simpl_expression (t:Raw.expr) : ae result =
| ELogic l -> simpl_logic_expression l | ELogic l -> simpl_logic_expression l
| EList _ -> simple_fail "list: not supported yet" | EList _ -> simple_fail "list: not supported yet"
| ESet _ -> simple_fail "set: not supported yet" | ESet _ -> simple_fail "set: not supported yet"
| ECase c ->
let%bind e = simpl_expression c.value.expr in
let%bind lst =
let aux (x:Raw.case_clause_expr) =
let%bind expr = simpl_expression x.expr in
ok (x.pattern, expr) in
bind_list
@@ List.map aux
@@ List.map get_value
@@ npseq_to_list c.value.cases_expr.value in
let%bind cases = simpl_cases lst in
ok @@ ae @@ Matching_expr (e, cases)
| EMap (MapInj mi) -> | EMap (MapInj mi) ->
let%bind lst = let%bind lst =
let lst = List.map get_value @@ pseq_to_list mi.value.elements in let lst = List.map get_value @@ pseq_to_list mi.value.elements in
@ -369,7 +381,7 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
let%bind match_false = match c.ifnot with let%bind match_false = match c.ifnot with
| ClauseInstr i -> let%bind i = simpl_instruction i in ok [i] | ClauseInstr i -> let%bind i = simpl_instruction i in ok [i]
| ClauseBlock b -> simpl_statements @@ fst b.value.inside in | ClauseBlock b -> simpl_statements @@ fst b.value.inside in
ok @@ Matching (expr, (Match_bool {match_true; match_false})) ok @@ Matching_instr (expr, (Match_bool {match_true; match_false}))
| Assign a -> | Assign a ->
let a = a.value in let a = a.value in
let%bind name = match a.lhs with let%bind name = match a.lhs with
@ -381,18 +393,18 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
| _ -> simple_fail "no weird assignments yet" | _ -> simple_fail "no weird assignments yet"
in in
ok @@ Assignment {name ; annotated_expression} ok @@ Assignment {name ; annotated_expression}
| Case c -> | Case_instr c ->
let c = c.value in let c = c.value in
let%bind expr = simpl_expression c.expr in let%bind expr = simpl_expression c.expr in
let%bind cases = let%bind cases =
let aux (x : Raw.case Raw.reg) = let aux (x : Raw.case_clause_instr Raw.reg) =
let%bind i = simpl_instruction_block x.value.instr in let%bind i = simpl_instruction_block x.value.instr in
ok (x.value.pattern, i) in ok (x.value.pattern, i) in
bind_list bind_list
@@ List.map aux @@ List.map aux
@@ npseq_to_list c.cases.value in @@ npseq_to_list c.cases_instr.value in
let%bind m = simpl_cases cases in let%bind m = simpl_cases cases in
ok @@ Matching (expr, m) ok @@ Matching_instr (expr, m)
| RecordPatch r -> | RecordPatch r ->
let r = r.value in let r = r.value in
let%bind record = match r.path with let%bind record = match r.path with
@ -409,7 +421,7 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
| MapRemove _ -> simple_fail "no map remove yet" | MapRemove _ -> simple_fail "no map remove yet"
| SetRemove _ -> simple_fail "no set remove yet" | SetRemove _ -> simple_fail "no set remove yet"
and simpl_cases : (Raw.pattern * block) list -> matching result = fun t -> and simpl_cases : type a . (Raw.pattern * a) list -> a matching result = fun t ->
let open Raw in let open Raw in
let get_var (t:Raw.pattern) = match t with let get_var (t:Raw.pattern) = match t with
| PVar v -> ok v.value | PVar v -> ok v.value

View File

@ -239,6 +239,21 @@ let matching () : unit result =
@@ [0 ; 2 ; 42 ; 163 ; -1] in @@ [0 ; 2 ; 42 ; 163 ; -1] in
ok () ok ()
in in
let%bind _expr_bool =
let aux n =
let open AST_Typed.Combinators in
let input = a_int n in
let%bind result = easy_run_typed "match_expr_bool" program input in
let%bind result' =
trace (simple_error "bad result") @@
get_a_int result in
Assert.assert_equal_int (if n = 2 then 42 else 0) result'
in
let%bind _ = bind_list
@@ List.map aux
@@ [0 ; 2 ; 42 ; 163 ; -1] in
ok ()
in
let%bind _option = let%bind _option =
let aux n = let aux n =
let open AST_Typed.Combinators in let open AST_Typed.Combinators in

View File

@ -74,14 +74,14 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement op
let%bind (_, t, _) as expression = translate_annotated_expression env annotated_expression in let%bind (_, t, _) as expression = translate_annotated_expression env annotated_expression in
let env' = Environment.add (name, t) env in let env' = Environment.add (name, t) env in
return ~env' (Assignment (name, expression)) return ~env' (Assignment (name, expression))
| Matching (expr, m) -> ( | Matching_instr (expr, m) -> (
let%bind expr' = translate_annotated_expression env expr in let%bind expr' = translate_annotated_expression env expr in
let env' = Environment.extend env in let env' = Environment.extend env in
match m with match m with
| Match_bool {match_true ; match_false} -> ( | Match_bool {match_true ; match_false} -> (
let%bind true_branch = translate_block env' match_true in let%bind true_branch = translate_block env' match_true in
let%bind false_branch = translate_block env' match_false in let%bind false_branch = translate_block env' match_false in
return (Cond (expr', true_branch, false_branch)) return (I_Cond (expr', true_branch, false_branch))
) )
| Match_option {match_none ; match_some = ((name, t), sm)} -> ( | Match_option {match_none ; match_some = ((name, t), sm)} -> (
let%bind none_branch = translate_block env' match_none in let%bind none_branch = translate_block env' match_none in
@ -235,6 +235,15 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
| LookUp dsi -> | LookUp dsi ->
let%bind (ds', i') = bind_map_pair f dsi in let%bind (ds', i') = bind_map_pair f dsi in
return (Predicate ("GET", [i' ; ds']), tv) return (Predicate ("GET", [i' ; ds']), tv)
| Matching_expr (expr, m) -> (
let%bind expr' = translate_annotated_expression env expr in
match m with
| AST.Match_bool {match_true ; match_false} ->
let%bind (t, f) = bind_map_pair (translate_annotated_expression env) (match_true, match_false) in
return (E_Cond (expr', t, f), tv)
| AST.Match_list _ | AST.Match_option _ | AST.Match_tuple (_, _) ->
simple_fail "only match bool exprs are translated yet"
)
and translate_lambda_shallow env l tv = and translate_lambda_shallow env l tv =
let { binder ; input_type ; output_type ; body ; result } : AST.lambda = l in let { binder ; input_type ; output_type ; body ; result } : AST.lambda = l in

View File

@ -162,39 +162,40 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc
let e' = Environment.add e name annotated_expression.type_annotation in let e' = Environment.add e name annotated_expression.type_annotation in
ok (e', O.Assignment {name;annotated_expression}) ok (e', O.Assignment {name;annotated_expression})
) )
| Matching (ex, m) -> | Matching_instr (ex, m) ->
let%bind ex' = type_annotated_expression e ex in let%bind ex' = type_annotated_expression e ex in
let%bind m' = type_match e ex'.type_annotation m in let%bind m' = type_match type_block e ex'.type_annotation m in
ok (e, O.Matching (ex', m')) ok (e, O.Matching_instr (ex', m'))
| Record_patch _ -> simple_fail "no record_patch yet" | Record_patch _ -> simple_fail "no record_patch yet"
and type_match (e:environment) (t:O.type_value) : I.matching -> O.matching result = function and type_match : type i o . (environment -> i -> o result) -> environment -> O.type_value -> i I.matching -> o O.matching result =
fun f e t i -> match i with
| Match_bool {match_true ; match_false} -> | Match_bool {match_true ; match_false} ->
let%bind _ = let%bind _ =
trace_strong (simple_error "Matching bool on not-a-bool") trace_strong (simple_error "Matching bool on not-a-bool")
@@ get_t_bool t in @@ get_t_bool t in
let%bind match_true = type_block e match_true in let%bind match_true = f e match_true in
let%bind match_false = type_block e match_false in let%bind match_false = f e match_false in
ok (O.Match_bool {match_true ; match_false}) ok (O.Match_bool {match_true ; match_false})
| Match_option {match_none ; match_some} -> | Match_option {match_none ; match_some} ->
let%bind t_opt = let%bind t_opt =
trace_strong (simple_error "Matching option on not-an-option") trace_strong (simple_error "Matching option on not-an-option")
@@ get_t_option t in @@ get_t_option t in
let%bind match_none = type_block e match_none in let%bind match_none = f e match_none in
let (n, b) = match_some in let (n, b) = match_some in
let n' = n, t_opt in let n' = n, t_opt in
let e' = Environment.add e n t_opt in let e' = Environment.add e n t_opt in
let%bind b' = type_block e' b in let%bind b' = f e' b in
ok (O.Match_option {match_none ; match_some = (n', b')}) ok (O.Match_option {match_none ; match_some = (n', b')})
| Match_list {match_nil ; match_cons} -> | Match_list {match_nil ; match_cons} ->
let%bind t_list = let%bind t_list =
trace_strong (simple_error "Matching list on not-an-list") trace_strong (simple_error "Matching list on not-an-list")
@@ get_t_list t in @@ get_t_list t in
let%bind match_nil = type_block e match_nil in let%bind match_nil = f e match_nil in
let (hd, tl, b) = match_cons in let (hd, tl, b) = match_cons in
let e' = Environment.add e hd t_list in let e' = Environment.add e hd t_list in
let e' = Environment.add e' tl t in let e' = Environment.add e' tl t in
let%bind b' = type_block e' b in let%bind b' = f e' b in
ok (O.Match_list {match_nil ; match_cons = (hd, tl, b')}) ok (O.Match_list {match_nil ; match_cons = (hd, tl, b')})
| Match_tuple (lst, b) -> | Match_tuple (lst, b) ->
let%bind t_tuple = let%bind t_tuple =
@ -205,7 +206,7 @@ and type_match (e:environment) (t:O.type_value) : I.matching -> O.matching resul
@@ (fun () -> List.combine lst t_tuple) in @@ (fun () -> List.combine lst t_tuple) in
let aux prev (name, tv) = Environment.add prev name tv in let aux prev (name, tv) = Environment.add prev name tv in
let e' = List.fold_left aux e lst' in let e' = List.fold_left aux e lst' in
let%bind b' = type_block e' b in let%bind b' = f e' b in
ok (O.Match_tuple (lst, b')) ok (O.Match_tuple (lst, b'))
and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result = and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result =
@ -383,7 +384,17 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
let dst_opt = make_t_option dst in let dst_opt = make_t_option dst in
let%bind type_annotation = check dst_opt in let%bind type_annotation = check dst_opt in
ok O.{expression = LookUp (ds, ind) ; type_annotation} ok O.{expression = LookUp (ds, ind) ; type_annotation}
(* Advanced *)
| Matching_expr (ex, m) -> (
let%bind ex' = type_annotated_expression e ex in
let%bind m' = type_match type_annotated_expression e ex'.type_annotation m in
let%bind type_annotation = match m' with
| Match_bool {match_true ; match_false} ->
let%bind _ = O.assert_type_value_eq (match_true.type_annotation, match_false.type_annotation) in
ok match_true.type_annotation
| _ -> simple_fail "can only type match_bool expressions yet" in
ok O.{expression = Matching_expr (ex', m') ; type_annotation}
)
and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value option) : (string * O.type_value) result = and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value option) : (string * O.type_value) result =
(* Constant poorman's polymorphism *) (* Constant poorman's polymorphism *)
@ -476,6 +487,10 @@ let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_ex
| LookUp dsi -> | LookUp dsi ->
let%bind dsi' = bind_map_pair untype_annotated_expression dsi in let%bind dsi' = bind_map_pair untype_annotated_expression dsi in
return (LookUp dsi') return (LookUp dsi')
| Matching_expr (ae, m) ->
let%bind ae' = untype_annotated_expression ae in
let%bind m' = untype_matching untype_annotated_expression m in
return (Matching_expr (ae', m'))
and untype_block (b:O.block) : (I.block) result = and untype_block (b:O.block) : (I.block) result =
bind_list @@ List.map untype_instruction b bind_list @@ List.map untype_instruction b
@ -494,28 +509,28 @@ and untype_instruction (i:O.instruction) : (I.instruction) result =
| Assignment a -> | Assignment a ->
let%bind annotated_expression = untype_annotated_expression a.annotated_expression in let%bind annotated_expression = untype_annotated_expression a.annotated_expression in
ok @@ Assignment {name = a.name ; annotated_expression} ok @@ Assignment {name = a.name ; annotated_expression}
| Matching (e, m) -> | Matching_instr (e, m) ->
let%bind e' = untype_annotated_expression e in let%bind e' = untype_annotated_expression e in
let%bind m' = untype_matching m in let%bind m' = untype_matching untype_block m in
ok @@ Matching (e', m') ok @@ Matching_instr (e', m')
and untype_matching (m:O.matching) : (I.matching) result = and untype_matching : type o i . (o -> i result) -> o O.matching -> (i I.matching) result = fun f m ->
let open I in let open I in
match m with match m with
| Match_bool {match_true ; match_false} -> | Match_bool {match_true ; match_false} ->
let%bind match_true = untype_block match_true in let%bind match_true = f match_true in
let%bind match_false = untype_block match_false in let%bind match_false = f match_false in
ok @@ Match_bool {match_true ; match_false} ok @@ Match_bool {match_true ; match_false}
| Match_tuple (lst, b) -> | Match_tuple (lst, b) ->
let%bind b = untype_block b in let%bind b = f b in
ok @@ Match_tuple (lst, b) ok @@ Match_tuple (lst, b)
| Match_option {match_none ; match_some = (v, some)} -> | Match_option {match_none ; match_some = (v, some)} ->
let%bind match_none = untype_block match_none in let%bind match_none = f match_none in
let%bind some = untype_block some in let%bind some = f some in
let match_some = fst v, some in let match_some = fst v, some in
ok @@ Match_option {match_none ; match_some} ok @@ Match_option {match_none ; match_some}
| Match_list {match_nil ; match_cons = (hd, tl, cons)} -> | Match_list {match_nil ; match_cons = (hd, tl, cons)} ->
let%bind match_nil = untype_block match_nil in let%bind match_nil = f match_nil in
let%bind cons = untype_block cons in let%bind cons = f cons in
let match_cons = hd, tl, cons in let match_cons = hd, tl, cons in
ok @@ Match_list {match_nil ; match_cons} ok @@ Match_list {match_nil ; match_cons}