From 1d3be683da2a1a4f5cd054977bb5c718cfff83fa Mon Sep 17 00:00:00 2001 From: DJ Date: Mon, 19 Aug 2024 20:47:32 +0900 Subject: [PATCH] Handle block context for throw_ref --- spectec/src/backend-prose/print.ml | 51 +++++++++----------- spectec/src/il2al/preprocess.ml | 37 ++++++++++++++- spectec/src/il2al/translate.ml | 75 +++++++++++++++++++++--------- spectec/src/il2al/transpile.ml | 1 + 4 files changed, 112 insertions(+), 52 deletions(-) diff --git a/spectec/src/backend-prose/print.ml b/spectec/src/backend-prose/print.ml index aa0ca2f526..a651ddb8d4 100644 --- a/spectec/src/backend-prose/print.ml +++ b/spectec/src/backend-prose/print.ml @@ -270,39 +270,30 @@ let rec string_of_instr' depth instr = let open Al.Ast in match instr.it with - | IfI (e, il, []) -> - sprintf "%s If %s, then:%s" (make_index depth) (string_of_expr e) - (string_of_instrs' (depth + 1) il) - | IfI (e, il1, [ { it = IfI (inner_e, inner_il1, []); _ } ]) -> - let if_index = make_index depth in - let else_if_index = make_index depth in - sprintf "%s If %s, then:%s\n%s Else if %s, then:%s" - if_index - (string_of_expr e) - (string_of_instrs' (depth + 1) il1) - (repeat indent depth ^ else_if_index) - (string_of_expr inner_e) - (string_of_instrs' (depth + 1) inner_il1) - | IfI (e, il1, [ { it = IfI (inner_e, inner_il1, inner_il2); _ } ]) -> - let if_index = make_index depth in - let else_if_index = make_index depth in - let else_index = make_index depth in - sprintf "%s If %s, then:%s\n%s Else if %s, then:%s\n%s Else:%s" - if_index - (string_of_expr e) - (string_of_instrs' (depth + 1) il1) - (repeat indent depth ^ else_if_index) - (string_of_expr inner_e) - (string_of_instrs' (depth + 1) inner_il1) - (repeat indent depth ^ else_index) - (string_of_instrs' (depth + 1) inner_il2) | IfI (e, il1, il2) -> let if_index = make_index depth in - let else_index = make_index depth in - sprintf "%s If %s, then:%s\n%s Else:%s" if_index (string_of_expr e) + let if_prose = sprintf "%s If %s, then:%s" if_index (string_of_expr e) (string_of_instrs' (depth + 1) il1) - (repeat indent depth ^ else_index) - (string_of_instrs' (depth + 1) il2) + in + + let rec collect_clause il = + match il with + | [ {it = IfI (c, il1, il2); _} ] -> (Some c, il1) :: collect_clause il2 + | _ -> [(None, il)] + in + let else_clauses = collect_clause il2 |> List.filter (fun (_, x) -> x <> []) in + let else_proses = List.map (fun (cond_opt, il)-> + let else_index = make_index depth in + match cond_opt with + | None -> sprintf "%s Else:%s" + (repeat indent depth ^ else_index) + (string_of_instrs' (depth + 1) il) + | Some e -> sprintf "%s Else if %s, then:%s" + (repeat indent depth ^ else_index) (string_of_expr e) + (string_of_instrs' (depth + 1) il) + ) else_clauses in + + String.concat "\n" (if_prose :: else_proses) | OtherwiseI il -> sprintf "%s Otherwise:%s" (make_index depth) (string_of_instrs' (depth + 1) il) diff --git a/spectec/src/il2al/preprocess.ml b/spectec/src/il2al/preprocess.ml index b90915fb30..733291279f 100644 --- a/spectec/src/il2al/preprocess.ml +++ b/spectec/src/il2al/preprocess.ml @@ -60,6 +60,35 @@ let remove_or def = DecD (id, params, typ, List.concat_map remove_or_clause clauses) $ def.at | _ -> def +(* HARDCODE: Remove a reduction rule for the block context, specifically, for THROW_REF *) +let is_block_context_exp e = + match e.it with + (* instr* =/= [] *) + | CmpE (NeOp, e1, e2) -> + begin match e1.it, e2.it with + | IterE (var, (List, _)), ListE [] + | ListE [], IterE (var, (List, _)) -> + begin match var.it with + | VarE id -> id.it = "instr" + | _ -> false + end + | _ -> false + end + | _ -> false +let is_block_context_prem prem = + match prem.it with + | IfPr e -> is_block_context_exp e + | _ -> false +let is_block_context_rule rule = + match rule.it with + | RuleD (_, _, _, _, [prem]) -> is_block_context_prem prem + | _ -> false +let remove_block_context def = + match def.it with + | RelD (id, mixop, typ, rules) -> + RelD (id, mixop, typ, Util.Lib.List.filter_not is_block_context_rule rules) $ def.at + | _ -> def + (* Pre-process a premise *) let rec preprocess_prem prem = @@ -128,7 +157,13 @@ let preprocess_clause (clause: clause) : clause = DefD (binds, args, exp, List.concat_map preprocess_prem prems) $ clause.at let rec preprocess_def (def: def) : def = - match (remove_or def).it with + let def' = + def + |> remove_or + |> remove_block_context + in + + match def'.it with | RelD (id, mixop, typ, rules) -> RelD (id, mixop, typ, List.map preprocess_rule rules) $ def.at | DecD (id, params, typ, clauses) -> diff --git a/spectec/src/il2al/translate.ml b/spectec/src/il2al/translate.ml index 887f560bb8..9f098da63b 100644 --- a/spectec/src/il2al/translate.ml +++ b/spectec/src/il2al/translate.ml @@ -120,6 +120,13 @@ let rec insert_instrs target il = h @ [ ifI (cond, insert_instrs (Transpile.insert_nop target) il' , []) ] | _ -> il @ target +(* Insert `target` at the else-branch of innermost if instruction *) +let rec insert_instrs_to_else target il = + match Util.Lib.List.split_last_opt il with + | Some (h, { it = IfI (cond, il1, il2); _ }) -> + h @ [ ifI (cond, il1, insert_instrs_to_else target il2) ] + | _ -> il @ target + let has_branch = List.exists (fun i -> match i.it with | IfI _ @@ -793,11 +800,11 @@ and handle_special_lhs lhs rhs free_ids = | _ when (Il.Print.string_of_typ rhs.note) = "inputT" -> [] | _ when (Il.Print.string_of_typ rhs.note) = "stateT" -> [] | _ when (Il.Print.string_of_typ rhs.note) = "unusedT" -> [] + | _ when (Il.Print.string_of_typ rhs.note) = "contextT" -> [] | TupE [e; _stack] when (Il.Print.string_of_typ rhs.note) = "stackT" -> let args = args_of_call rhs in let pop_num = List.hd args |> arg2expr in insert_pop e pop_num - | _ when (Il.Print.string_of_typ rhs.note) = "contextT" -> [] (* Handle inverse function call *) | CallE _ -> handle_call_lhs lhs rhs free_ids (* Handle iterator *) @@ -1200,50 +1207,76 @@ let rec translate_rgroup' rgroup = let pops, rgroup' = extract_pops rgroup in let subgroups = group_by_context rgroup' in - let blocks = List.map (fun (ctxt, subgroup) -> - let popped_vars = List.concat_map (fun p -> - match p.it with - | Il.LetPr (_, _, ids) -> ids - | _ -> assert false - ) pops in - let u_group = Il2il.unify_ctxt popped_vars subgroup in - - match ctxt with + let blocks = List.map (fun (k, subgroup) -> + match k with (* Normal case *) | None -> - let winstr = extract_winstr (List.hd u_group) in + let winstr = extract_winstr (List.hd subgroup) in let inner_pop_instrs = translate_context_winstr winstr in - let blocks = List.map translate_reduction u_group in + let blocks = List.map translate_reduction subgroup in let instrs = match blocks with | [b1; b2] when not (has_branch b1 || has_branch b2) -> [ eitherI (b1, b2) ] (* Either case *) | _ -> Transpile.merge_blocks blocks in - inner_pop_instrs @ instrs + k, inner_pop_instrs @ instrs (* Context case *) | Some ctxt -> + let popped_vars = List.concat_map (fun p -> + match p.it with + | Il.LetPr (_, _, ids) -> ids + | _ -> assert false + ) pops in + let u_group = Il2il.unify_ctxt popped_vars subgroup in let atom = case_of_case ctxt |> List.hd |> List.hd in let cond = ContextKindE atom $$ atom.at % boolT in - let valTs = listT valT in - let e_vals = iterE (subE ("val", "val") ~note:valT, [ "val" ], List) ~note:valTs in - let instr_popall = popallI e_vals in - let instr_push = pushI e_vals in let head_instrs, middle_instr = translate_context ctxt in let body_instrs = List.map (translate_reduction ~context_opt:(Some middle_instr)) u_group |> List.mapi (fun i instrs -> if i = 0 then instrs else [otherwiseI instrs]) |> Transpile.merge_blocks in - [ - instr_popall; + k, [ ifI ( cond, - head_instrs @ [instr_push] @ body_instrs, + head_instrs @ body_instrs, [] ) ] ) subgroups in - translate_prems pops (Transpile.merge_blocks blocks) + let normal_block_opt, ctxt_blocks = + match List.hd blocks with + | (Some _, _) -> None, blocks + | (None, b) -> Some b, List.tl blocks + in + + let ctxt_block = match ctxt_blocks with + | [] -> [] + | _ -> + let valTs = listT valT in + let e_vals = iterE (subE ("val", "val") ~note:valT, [ "val" ], List) ~note:valTs in + let instr_popall = popallI e_vals in + let instr_push = pushI e_vals in + + instr_popall :: + List.fold_right (fun instrs acc -> + assert (List.length instrs = 1); + let if_instr = List.hd instrs in + match if_instr.it with + | IfI (c, instrs1, []) -> [{if_instr with it = IfI (c, instr_push :: instrs1, acc)}] + | _ -> assert false + ) (List.map snd ctxt_blocks) [] + in + + let body_instrs = + match normal_block_opt, ctxt_block with + | None, b -> b + | Some b1, b2 -> + (* Assert: b1 must have the else-less IfI as inner most instruction *) + insert_instrs_to_else b2 b1 + in + + translate_prems pops body_instrs (* Main translation for reduction rules * `rgroup` -> `Al.Algo` *) diff --git a/spectec/src/il2al/transpile.ml b/spectec/src/il2al/transpile.ml index 85c1415e65..e37f90e3b1 100644 --- a/spectec/src/il2al/transpile.ml +++ b/spectec/src/il2al/transpile.ml @@ -203,6 +203,7 @@ let swap_if instr = match instr.it with | IfI (c, il, []) -> ifI (c, il, []) ~at:at | IfI (c, [], il) -> ifI (neg c, il, []) ~at:at + | IfI (_, _, il2) when (match il2 with | [{it = IfI _; _}] -> true | _ -> false) -> instr | IfI (c, il1, il2) when count_instrs il1 > count_instrs il2 -> ifI (neg c, il2, il1) ~at:at | _ -> instr