diff --git a/spectec/src/il2al/animate.ml b/spectec/src/il2al/animate.ml index f240de433f..71f4c88746 100644 --- a/spectec/src/il2al/animate.ml +++ b/spectec/src/il2al/animate.ml @@ -8,7 +8,7 @@ by performing dataflow analysis. open Util open Source open Il.Ast -open Il.Free +open Free (* Helpers *) @@ -49,71 +49,6 @@ let remove_or rule = match rule.it with { rule with it = RuleD (id', binds, mixop, args, prems') } ) premss' -(* my_free_??? are equivalent to free_??? in Il.Free module, except - 1. i in e^(i free_varid id - | BoolE _ | NatE _ | TextE _ -> empty - | UnE (_, e1) | LenE e1 | TheE e1 | MixE (_, e1) | SubE (e1, _, _) - | CallE (_, e1) | DotE (e1, _) | CaseE (_, e1) -> - f e1 - | BinE (_, e1, e2) | CmpE (_, e1, e2) | IdxE (e1, e2) | CompE (e1, e2) | CatE (e1, e2) -> - free_list f [e1; e2] - | SliceE (e1, e2, e3) -> free_list f [e1; e2; e3] - | OptE eo -> free_opt f eo - | TupE es | ListE es -> free_list f es - | UpdE (e1, p, e2) | ExtE (e1, p, e2) -> - union (free_list f [e1; e2]) (fp p) - | StrE efs -> free_list fef efs - | IterE (e1, iter) -> - let free1 = f e1 in - let bound, free2 = fi iter in - diff (union free1 free2) bound - -and my_free_expfield ignore_listN (_, e) = my_free_exp ignore_listN e - -and my_free_path ignore_listN p = - let f = my_free_exp ignore_listN in - let fp = my_free_path ignore_listN in - match p.it with - | RootP -> empty - | IdxP (p1, e) -> union (fp p1) (f e) - | SliceP (p1, e1, e2) -> - union (fp p1) (union (f e1) (f e2)) - | DotP (p1, _) -> fp p1 - -and my_free_iterexp ignore_listN (iter, _) = - let f = my_free_exp ignore_listN in - match iter with - | ListN (e, None) -> empty, if ignore_listN then empty else f e - | ListN (e, Some id) -> free_varid id, if ignore_listN then empty else f e - | _ -> empty, empty - -let rec my_free_prem ignore_listN prem = - let f = my_free_exp ignore_listN in - let fp = my_free_prem ignore_listN in - let fi = my_free_iterexp ignore_listN in - match prem.it with - | RulePr (_id, _op, e) -> f e - | IfPr e -> f e - | LetPr (e1, e2, _ids) -> union (f e1) (f e2) - | ElsePr -> empty - | IterPr (prem', iter) -> - let free1 = fp prem' in - let bound, free2 = fi iter in - diff (union free1 free2) bound - (* Helper for handling free-var set *) let subset x y = Set.subset x.varid y.varid @@ -126,13 +61,13 @@ let unwrap (_, p, _) = p (* Check if a given premise is tight: all free variables in the premise is known *) let is_tight env (tag, prem, _) = match tag with - | Condition -> subset (my_free_prem false prem) env + | Condition -> subset (free_prem false prem) env | _ -> false (* Check if a given premise is an assignment: all free variables except to-be-assigned are known *) let is_assign env (tag, prem, _) = match tag with - | Assign frees -> subset (diff (my_free_prem false prem) {empty with varid = (Set.of_list frees)}) env + | Assign frees -> subset (diff (free_prem false prem) {empty with varid = (Set.of_list frees)}) env | _ -> false let best' = ref (-1, []) @@ -157,7 +92,7 @@ and select_assign prems acc env = ( match prems with None | _ -> let assigns' = List.map unwrap assigns in - let new_env = assigns' |> List.map (my_free_prem false) |> List.fold_left union env in + let new_env = assigns' |> List.map (free_prem false) |> List.fold_left union env in select_tight non_assigns (acc @ assigns') new_env ) @@ -193,7 +128,7 @@ let rec index_of acc xs x = match xs with | [] -> None | h :: t -> if h = x then Some acc else index_of (acc + 1) t x -let free_exp_list e = (my_free_exp false e).varid |> Set.elements +let free_exp_list e = (free_exp false e).varid |> Set.elements let rec powset = function | [] -> [ [] ] @@ -277,7 +212,7 @@ let rec rows_of_prem vars p_tot_num i p = match p.it with | _ -> [ Condition, p, [i] ] let build_matrix prems known_vars = - let all_vars = prems |> List.map (my_free_prem false) |> List.fold_left union empty in + let all_vars = prems |> List.map (free_prem false) |> List.fold_left union empty in let unknown_vars = (diff all_vars known_vars).varid |> Set.elements in let prem_num = List.length prems in @@ -330,7 +265,7 @@ let animate_rule r = match r.it with match (mixop, args.it) with (* c |- e : t *) | ([ [] ; [Turnstile] ; [Colon] ; []] , TupE ([c; e; _t])) -> - let new_prems = animate_prems (union (my_free_exp false c) (my_free_exp false e)) prems in + let new_prems = animate_prems (union (free_exp false c) (free_exp false e)) prems in RuleD(id, binds, mixop, args, new_prems) $ r.at (* lhs* ~> rhs* *) | ([ [] ; [Star ; SqArrow] ; [Star]] , TupE ([lhs; _rhs])) @@ -338,7 +273,7 @@ let animate_rule r = match r.it with | ([ [] ; [SqArrow] ; [Star]] , TupE ([lhs; _rhs])) (* lhs ~> rhs *) | ([ [] ; [SqArrow] ; []] , TupE ([lhs; _rhs])) -> - let new_prems = animate_prems (my_free_exp true lhs) prems in + let new_prems = animate_prems (free_exp true lhs) prems in RuleD(id, binds, mixop, args, new_prems) $ r.at | _ -> r ) @@ -346,7 +281,7 @@ let animate_rule r = match r.it with (* Animate clause *) let animate_clause c = match c.it with | DefD (binds, e1, e2, prems) -> - let new_prems = animate_prems (my_free_exp false e1) prems in + let new_prems = animate_prems (free_exp false e1) prems in DefD (binds, e1, e2, new_prems) $ c.at (* Animate defs *) diff --git a/spectec/src/il2al/dune b/spectec/src/il2al/dune index 29a41db6b2..7e740d563a 100644 --- a/spectec/src/il2al/dune +++ b/spectec/src/il2al/dune @@ -6,5 +6,6 @@ il2il translate transpile + free ) ) diff --git a/spectec/src/il2al/free.ml b/spectec/src/il2al/free.ml new file mode 100644 index 0000000000..7110d23e06 --- /dev/null +++ b/spectec/src/il2al/free.ml @@ -0,0 +1,70 @@ +(* +free_??? are equivalent to free_??? in Il.Free module, except +1. i in e^(i free_varid id + | BoolE _ | NatE _ | TextE _ -> empty + | UnE (_, e1) | LenE e1 | TheE e1 | MixE (_, e1) | SubE (e1, _, _) + | CallE (_, e1) | DotE (e1, _) | CaseE (_, e1) -> + f e1 + | BinE (_, e1, e2) | CmpE (_, e1, e2) | IdxE (e1, e2) | CompE (e1, e2) | CatE (e1, e2) -> + free_list f [e1; e2] + | SliceE (e1, e2, e3) -> free_list f [e1; e2; e3] + | OptE eo -> free_opt f eo + | TupE es | ListE es -> free_list f es + | UpdE (e1, p, e2) | ExtE (e1, p, e2) -> + union (free_list f [e1; e2]) (fp p) + | StrE efs -> free_list fef efs + | IterE (e1, iter) -> + let free1 = f e1 in + let bound, free2 = fi iter in + diff (union free1 free2) bound + +and free_expfield ignore_listN (_, e) = free_exp ignore_listN e + +and free_path ignore_listN p = + let f = free_exp ignore_listN in + let fp = free_path ignore_listN in + match p.it with + | RootP -> empty + | IdxP (p1, e) -> union (fp p1) (f e) + | SliceP (p1, e1, e2) -> + union (fp p1) (union (f e1) (f e2)) + | DotP (p1, _) -> fp p1 + +and free_iterexp ignore_listN (iter, _) = + let f = free_exp ignore_listN in + match iter with + | ListN (e, None) -> empty, if ignore_listN then empty else f e + | ListN (e, Some id) -> free_varid id, if ignore_listN then empty else f e + | _ -> empty, empty + +let rec free_prem ignore_listN prem = + let f = free_exp ignore_listN in + let fp = free_prem ignore_listN in + let fi = free_iterexp ignore_listN in + match prem.it with + | RulePr (_id, _op, e) -> f e + | IfPr e -> f e + | LetPr (e1, e2, _ids) -> union (f e1) (f e2) + | ElsePr -> empty + | IterPr (prem', iter) -> + let free1 = fp prem' in + let bound, free2 = fi iter in + diff (union free1 free2) bound diff --git a/spectec/src/il2al/il2il.ml b/spectec/src/il2al/il2il.ml index 10249fbe31..d74a7da308 100644 --- a/spectec/src/il2al/il2il.ml +++ b/spectec/src/il2al/il2il.ml @@ -16,11 +16,13 @@ let take_prefix n str = else String.sub str 0 n + (** Walker-based transformer **) let rec transform_expr f e = let new_ = transform_expr f in - { e with it = match (f e).it with + let it = + match (f e).it with | VarE _ | BoolE _ | NatE _ @@ -45,9 +47,12 @@ let rec transform_expr f e = | ListE es -> ListE ((List.map new_) es) | CatE (e1, e2) -> CatE (new_ e1, new_ e2) | CaseE (atom, e1) -> CaseE (atom, new_ e1) - | SubE (e1, _t1, t2) -> SubE (new_ e1, _t1, t2) } + | SubE (e1, _t1, t2) -> SubE (new_ e1, _t1, t2) + in { e with it } + (** Change right_assoc cat into left_assoc cat **) + let to_left_assoc_cat = let rec rotate_ccw e = begin match e.it with @@ -61,7 +66,9 @@ let to_left_assoc_cat = end in transform_expr rotate_ccw + (** Change left_assoc cat into right_assoc cat **) + let to_right_assoc_cat = let rec rotate_cw e = begin match e.it with @@ -99,98 +106,99 @@ let to_iter e iterexp = IterE (e, iterexp) let is_unified_id id = String.split_on_char '_' id |> Util.Lib.List.last |> String.starts_with ~prefix:unified_prefix let rec overlap e1 e2 = if eq_exp e1 e2 then e1 else - ( match e1.it, e2.it with - | VarE id, _ - | IterE ({ it = VarE id; _}, _) , _ - when is_unified_id id.it -> e1.it - | UnE (unop1, e1), UnE (unop2, e2) when unop1 = unop2 -> + let it = + match e1.it, e2.it with + | VarE id, _ + | IterE ({ it = VarE id; _}, _) , _ + when is_unified_id id.it -> e1.it + | UnE (unop1, e1), UnE (unop2, e2) when unop1 = unop2 -> UnE (unop1, overlap e1 e2) - | BinE (binop1, e1, e1'), BinE (binop2, e2, e2') when binop1 = binop2 -> + | BinE (binop1, e1, e1'), BinE (binop2, e2, e2') when binop1 = binop2 -> BinE (binop1, overlap e1 e2, overlap e1' e2') - | CmpE (cmpop1, e1, e1'), CmpE (cmpop2, e2, e2') when cmpop1 = cmpop2 -> + | CmpE (cmpop1, e1, e1'), CmpE (cmpop2, e2, e2') when cmpop1 = cmpop2 -> CmpE (cmpop1, overlap e1 e2, overlap e1' e2') - | IdxE (e1, e1'), IdxE (e2, e2') -> + | IdxE (e1, e1'), IdxE (e2, e2') -> IdxE (overlap e1 e2, overlap e1' e2') - | SliceE (e1, e1', e1''), SliceE (e2, e2', e2'') -> + | SliceE (e1, e1', e1''), SliceE (e2, e2', e2'') -> SliceE (overlap e1 e2, overlap e1' e2', overlap e1'' e2'') - | UpdE (e1, path1, e1'), UpdE (e2, path2, e2') when eq_path path1 path2 -> + | UpdE (e1, path1, e1'), UpdE (e2, path2, e2') when eq_path path1 path2 -> UpdE (overlap e1 e2, path1, overlap e1' e2') - | ExtE (e1, path1, e1'), ExtE (e2, path2, e2') when eq_path path1 path2 -> + | ExtE (e1, path1, e1'), ExtE (e2, path2, e2') when eq_path path1 path2 -> ExtE (overlap e1 e2, path1, overlap e1' e2') - | StrE efs1, StrE efs2 when List.map fst efs1 = List.map fst efs2 -> + | StrE efs1, StrE efs2 when List.map fst efs1 = List.map fst efs2 -> StrE (List.map2 (fun (a1, e1) (_, e2) -> (a1, overlap e1 e2)) efs1 efs2) - | DotE (e1, atom1), DotE (e2, atom2) when atom1 = atom2 -> + | DotE (e1, atom1), DotE (e2, atom2) when atom1 = atom2 -> DotE (overlap e1 e2, atom1) - | CompE (e1, e1'), CompE (e2, e2') -> + | CompE (e1, e1'), CompE (e2, e2') -> CompE (overlap e1 e2, overlap e1' e2') - | LenE e1, LenE e2 -> + | LenE e1, LenE e2 -> LenE (overlap e1 e2) - | TupE es1, TupE es2 when List.length es1 = List.length es2 -> + | TupE es1, TupE es2 when List.length es1 = List.length es2 -> TupE (List.map2 overlap es1 es2) - | MixE (mixop1, e1), MixE (mixop2, e2) when mixop1 = mixop2 -> + | MixE (mixop1, e1), MixE (mixop2, e2) when mixop1 = mixop2 -> MixE (mixop1, overlap e1 e2) - | CallE (id1, e1), CallE (id2, e2) when eq_id id1 id2-> + | CallE (id1, e1), CallE (id2, e2) when eq_id id1 id2-> CallE (id1, overlap e1 e2) - | IterE (e1, itere1), IterE (e2, itere2) when eq_iterexp itere1 itere2 -> + | IterE (e1, itere1), IterE (e2, itere2) when eq_iterexp itere1 itere2 -> IterE (overlap e1 e2, itere1) - | OptE (Some e1), OptE (Some e2) -> + | OptE (Some e1), OptE (Some e2) -> OptE (Some (overlap e1 e2)) - | TheE e1, TheE e2 -> + | TheE e1, TheE e2 -> TheE (overlap e1 e2) - | ListE es1, ListE es2 when List.length es1 = List.length es2 -> + | ListE es1, ListE es2 when List.length es1 = List.length es2 -> ListE (List.map2 overlap es1 es2) - | CatE (e1, e1'), CatE (e2, e2') -> + | CatE (e1, e1'), CatE (e2, e2') -> CatE (overlap e1 e2, overlap e1' e2') - | CaseE (atom1, e1), CaseE (atom2, e2) when atom1 = atom2 -> + | CaseE (atom1, e1), CaseE (atom2, e2) when atom1 = atom2 -> CaseE (atom1, overlap e1 e2) - | SubE (e1, typ1, typ1'), SubE (e2, typ2, typ2') when eq_typ typ1 typ2 && eq_typ typ1' typ2' -> + | SubE (e1, typ1, typ1'), SubE (e2, typ2, typ2') when eq_typ typ1 typ2 && eq_typ typ1' typ2' -> SubE (overlap e1 e2, typ1, typ1') - | _ -> - let ty = e1.note in - let id = gen_new_unified ty in - match ty.it with - | IterT (ty, iter) -> to_iter (VarE id $$ no_region % ty) (iter, [id]) - | _ -> VarE id - ) $$ (e1.at % e1.note) + | _ -> + let ty = e1.note in + let id = gen_new_unified ty in + match ty.it with + | IterT (ty, iter) -> to_iter (VarE id $$ no_region % ty) (iter, [id]) + | _ -> VarE id + in { e1 with it } let pairwise_concat (a,b) (c,d) = (a@c, b@d) -let rec collect_unified template e = if eq_exp template e then [], [] else match template.it, e.it with - | VarE id, _ - | IterE ({ it = VarE id; _}, _) , _ - when is_unified_id id.it -> - [ IfPr (CmpE (EqOp, template, e) $$ no_region % (BoolT $ no_region)) $ no_region ], - [id, template.note, []] - (* one e *) - | UnE (_, e1), UnE (_, e2) - | DotE (e1, _), DotE (e2, _) - | LenE e1, LenE e2 - | MixE (_, e1), MixE (_, e2) - | CallE (_, e1), CallE (_, e2) - | IterE (e1, _), IterE (e2, _) - | OptE (Some e1), OptE (Some e2) - | TheE e1, TheE e2 - | CaseE (_, e1), CaseE (_, e2) - | SubE (e1, _, _), SubE (e2, _, _) -> collect_unified e1 e2 - (* two e *) - | BinE (_, e1, e1'), BinE (_, e2, e2') - | CmpE (_, e1, e1'), CmpE (_, e2, e2') - | IdxE (e1, e1'), IdxE (e2, e2') - | UpdE (e1, _, e1'), UpdE (e2, _, e2') - | ExtE (e1, _, e1'), ExtE (e2, _, e2') - | CompE (e1, e1'), CompE (e2, e2') - | CatE (e1, e1'), CatE (e2, e2') -> pairwise_concat (collect_unified e1 e2) (collect_unified e1' e2') - (* others *) - | SliceE (e1, e1', e1''), SliceE (e2, e2', e2'') -> - pairwise_concat (pairwise_concat (collect_unified e1 e2) (collect_unified e1' e2')) (collect_unified e1'' e2'') - | StrE efs1, StrE efs2 -> - List.fold_left2 (fun acc (_, e1) (_, e2) -> pairwise_concat acc (collect_unified e1 e2)) ([], []) efs1 efs2 - | TupE es1, TupE es2 - | ListE es1, ListE es2 -> - List.fold_left2 (fun acc e1 e2 -> pairwise_concat acc (collect_unified e1 e2)) ([], []) es1 es2 - | _ -> failwith "Impossible collect_unified" +let rec collect_unified template e = if eq_exp template e then [], [] else + match template.it, e.it with + | VarE id, _ + | IterE ({ it = VarE id; _}, _) , _ + when is_unified_id id.it -> + [ IfPr (CmpE (EqOp, template, e) $$ no_region % (BoolT $ no_region)) $ no_region ], + [id, template.note, []] + | UnE (_, e1), UnE (_, e2) + | DotE (e1, _), DotE (e2, _) + | LenE e1, LenE e2 + | MixE (_, e1), MixE (_, e2) + | CallE (_, e1), CallE (_, e2) + | IterE (e1, _), IterE (e2, _) + | OptE (Some e1), OptE (Some e2) + | TheE e1, TheE e2 + | CaseE (_, e1), CaseE (_, e2) + | SubE (e1, _, _), SubE (e2, _, _) -> collect_unified e1 e2 + | BinE (_, e1, e1'), BinE (_, e2, e2') + | CmpE (_, e1, e1'), CmpE (_, e2, e2') + | IdxE (e1, e1'), IdxE (e2, e2') + | UpdE (e1, _, e1'), UpdE (e2, _, e2') + | ExtE (e1, _, e1'), ExtE (e2, _, e2') + | CompE (e1, e1'), CompE (e2, e2') + | CatE (e1, e1'), CatE (e2, e2') -> pairwise_concat (collect_unified e1 e2) (collect_unified e1' e2') + | SliceE (e1, e1', e1''), SliceE (e2, e2', e2'') -> + pairwise_concat (pairwise_concat (collect_unified e1 e2) (collect_unified e1' e2')) (collect_unified e1'' e2'') + | StrE efs1, StrE efs2 -> + List.fold_left2 (fun acc (_, e1) (_, e2) -> pairwise_concat acc (collect_unified e1 e2)) ([], []) efs1 efs2 + | TupE es1, TupE es2 + | ListE es1, ListE es2 -> + List.fold_left2 (fun acc e1 e2 -> pairwise_concat acc (collect_unified e1 e2)) ([], []) es1 es2 + | _ -> failwith "Impossible collect_unified" + (** If prems include a otherwise premise, make it first prem **) + let prioritize_else prems = let other, non_others = List.partition (fun p -> p.it = ElsePr) prems in other @ non_others