From b06433952ec8e3dc840de8cb0ba9bf3883d3fa44 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 20 Nov 2025 09:48:26 +0100 Subject: [PATCH 1/3] [spectec] Implement IterPr in IL evaluator --- spectec/doc/example/output/NanoWasm.pdf | Bin 245571 -> 245571 bytes spectec/src/il/eval.ml | 137 +++++++++++++++++++++--- 2 files changed, 123 insertions(+), 14 deletions(-) diff --git a/spectec/doc/example/output/NanoWasm.pdf b/spectec/doc/example/output/NanoWasm.pdf index 3401b402bf0e00a21ab9bde6998f8a7301d274b4..417c33dd13ac6598e1b8d4f765eeb29297610908 100644 GIT binary patch delta 366 zcmX^7kMHn5z75Gj^lzHnf1dipI4yOCOh_% zcFx(qt>u%?ezjtG@WNEnv5qP2s}q;k8_w(#>^E*&hflom&BSg;!?uXO5-~?-z4^BG zeP6#s()BvI|1e0YHCqX{TM07)G1GP{VP>&KT1Ey2 zmL{f#=Gq2^>IMetnq2z6`6(`mC8-J;E>=bcMy7^_P$k=|wlWv7Ia@lqS-3hnJGmHH kIvN7yE!|w5-3;9vO$-do-AoN#>=bMWDcP>ShgpOf0IepG`v3p{ delta 366 zcmX^7kMHn5z75Gj^;w4vc-S87p6}!?Efzj$?TMXY+Z_3u0}u1X@++RbcIZ-0PR@G! z<&rGdCf9L(R8-uGwvg#J+nfVO0m#=&%zA2@^Re5dK z6Z0Fhj%(-7J^MsE0o%QD1 z-uHgzC6cb!%{{jH_Vcr?%3pni)ccgC%Pdq9mA^E9djDUgl;s(}^W@I>TI-1YbZb%9 zo|+!iq~&90emXP5{dm&;bf%wad_6joi@$!$HQO(x(rhK%ZY9hJ#7x_*gqg(_X&D$9 z8kiWGnrj;vsv8)nYjWxP=BKzMmZU0ZxL6q(7?~OxLX~W<+R9wS=4{|*XlCZ*WMFA( lX=Y$x>1yt3=;&%_V(e^eZei(YZfK`qLrBSX{XNVg%mC;Mja&c# diff --git a/spectec/src/il/eval.ml b/spectec/src/il/eval.ml index be9321624c..2689034f9c 100644 --- a/spectec/src/il/eval.ml +++ b/spectec/src/il/eval.ml @@ -474,34 +474,143 @@ and reduce_exp_call env id args at = function reduce_exp_call env id args at clauses' | None -> reduce_exp_call env id args at clauses' | Some s -> - match reduce_prems env Subst.(subst_list subst_prem s prems) with + match reduce_prems env s prems with | None -> None | Some false -> reduce_exp_call env id args at clauses' | Some true -> Some (reduce_exp env (Subst.subst_exp s e)) -and reduce_prems env = function +and reduce_prems env s = function | [] -> Some true | prem::prems -> - match reduce_prem env prem with - | Some true -> reduce_prems env prems - | other -> other + match reduce_prem env (Subst.subst_prem s prem) with + | `True s' -> reduce_prems env (Subst.union s s') prems + | `False -> Some false + | `None -> None -and reduce_prem env prem : bool option = +and reduce_prem env prem : [`True of Subst.t | `False | `None] = match prem.it with - | RulePr _ -> None + | RulePr _ -> `None | IfPr e -> (match (reduce_exp env e).it with - | BoolE b -> Some b - | _ -> None + | BoolE b -> if b then `True Subst.empty else `False + | _ -> `None ) - | ElsePr -> Some true + | ElsePr -> `True Subst.empty | LetPr (e1, e2, _ids) -> (match match_exp env Subst.empty e2 e1 with - | Some _ -> Some true (* TODO(2, rossberg): need to keep substitution? *) - | None -> None - | exception Irred -> None + | Some s -> `True s + | None -> `None + | exception Irred -> `None ) - | IterPr (_prem, _iter) -> None (* TODO(3, rossberg): reduce? *) + | IterPr (prem1, iterexp) -> + let iter', xes' = reduce_iterexp env iterexp in + (* Distinguish between let-defined variables, which flow outwards, + * and others, which are assumed to flow inwards. *) + let rec is_let_bound prem (x, _) = + match prem.it with + | LetPr (_, _, xs) -> List.mem x.it xs + | IterPr (premI, iterexpI) -> + let _iter1', xes1' = reduce_iterexp env iterexpI in + let xes1_out, _ = List.partition (is_let_bound premI) xes1' in + List.exists (fun (_, e1) -> Free.(Set.mem x.it (free_exp e1).varid)) xes1_out + | _ -> false + in + let xes_out, xes_in = List.partition (is_let_bound prem) xes' in + let xs_out, es_out = List.split xes_out in + let xs_in, es_in = List.split xes_in in + if not (List.for_all is_head_normal_exp es_in) || iter' <= List1 && es_in = [] then + (* We don't know the number of iterations (yet): can't do anything. *) + `None + else + (match iter' with + | Opt -> + let eos_in = List.map as_opt_exp es_in in + if List.for_all Option.is_none eos_in then + (* Iterating over empty option: nothing to do. *) + `True Subst.empty + else if List.for_all Option.is_some eos_in then + (* All iteration variables are non-empty: reduce body. *) + let es1_in = List.map Option.get eos_in in + (* s substitutes in-bound iteration variables with corresponding + * values. *) + let s = List.fold_left2 Subst.add_varid Subst.empty xs_in es1_in in + match reduce_prem env (Subst.subst_prem s prem1) with + | (`None | `False) as r -> r + | `True s' -> + (* Body is true: now reverse-match out-bound iteration values + * against iteration sources. *) + match + List.fold_left (fun s_opt (xI, eI) -> + let* s = s_opt in + let tI = match eI.note.it with IterT (tI, _) -> tI | _ -> assert false in + match_exp' env s (OptE (Some (Subst.subst_exp s' (VarE xI $$ xI.at % tI))) $> eI) eI + ) (Some Subst.empty) xes_out + with + | Some s'' -> `True s'' + | None -> `None + else + (* Inconsistent arity of iteration values: can't perform mapping. + * (This is a stuck computation, i.e., undefined.) *) + `None + | List | List1 -> + (* Unspecified iteration count: get length from (first) iteration value + * and start over; es'/es_in is in hnf, so got to be a list. *) + let n = List.length (as_list_exp (List.hd es_in)) in + if iter' = List || n >= 1 then + let en = NumE (`Nat (Z.of_int n)) $$ prem.at % (NumT `NatT $ prem.at) in + reduce_prem env (IterPr (prem1, (ListN (en, None), xes')) $> prem) + else + (* List is empty although it is List1: inconsistency. + * (This is a stuck computation, i.e., undefined.) *) + `None + | ListN ({it = NumE (`Nat n'); _}, xo) -> + (* Iterationen values es'/es_in are in hnf, so got to be lists. *) + let ess_in = List.map as_list_exp es_in in + let ns = List.map List.length ess_in in + let n = Z.to_int n' in + if List.for_all ((=) n) ns then + (* All in-bound lists have the expected length: reduce body, + * once for each tuple of values from the iterated lists. *) + let rs = List.init n (fun i -> + let esI_in = List.map (fun es -> List.nth es i) ess_in in + (* s substitutes in-bound iteration variables with corresponding + * values for this respective iteration. *) + let s = List.fold_left2 Subst.add_varid Subst.empty xs_in esI_in in + (* Add iteration counter variable if used. *) + let s' = + Option.fold xo ~none:s ~some:(fun x -> + let en = NumE (`Nat (Z.of_int i)) $$ x.at % (NumT `NatT $ x.at) in + Subst.add_varid s x en + ) + in + reduce_prem env (Subst.subst_prem s' prem1) + ) + in + if List.mem `None rs then `None else + if List.mem `False rs then `False else + (* Body was true in every iteration: now reverse-match out-bound + * iteration variables against iteration sources. *) + let ss = List.map (function `True s -> s | _ -> assert false) rs in + (* Aggregate the out-lists for each out-bound variable. *) + let es_out' = + List.map2 (fun xI eI -> + let tI = match eI.note.it with IterT (tI, _) -> tI | _ -> assert false in + let esI = List.map (fun sJ -> + Subst.subst_exp sJ (VarE xI $$ xI.at % tI) + ) ss + in ListE esI $> eI + ) xs_out es_out + in + (* Reverse-match out-bound list values against iteration sources. *) + match match_list match_exp env Subst.empty es_out' es_out with + | Some s' -> `True s' + | None -> `None + else + (* Inconsistent list lengths: can't perform mapping. + * (This is a stuck computation, i.e., undefined.) *) + `None + | ListN _ -> `None + ) (* Matching *) From f6840abe323dbe4c0cc0b46816695985624d9c55 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 20 Nov 2025 09:57:45 +0100 Subject: [PATCH 2/3] Comment tweaks --- spectec/src/il/eval.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/spectec/src/il/eval.ml b/spectec/src/il/eval.ml index 2689034f9c..b5c58d7c09 100644 --- a/spectec/src/il/eval.ml +++ b/spectec/src/il/eval.ml @@ -524,9 +524,10 @@ and reduce_prem env prem : [`True of Subst.t | `False | `None] = else (match iter' with | Opt -> + (* Iterationen values es'/es_in are in hnf, so got to be options. *) let eos_in = List.map as_opt_exp es_in in if List.for_all Option.is_none eos_in then - (* Iterating over empty option: nothing to do. *) + (* Iterating over empty options: nothing to do. *) `True Subst.empty else if List.for_all Option.is_some eos_in then (* All iteration variables are non-empty: reduce body. *) From f08307f5b6750b7b32ac229338b4db207bd46aca Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 20 Nov 2025 09:58:46 +0100 Subject: [PATCH 3/3] More comment tweaks --- spectec/src/il/eval.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/spectec/src/il/eval.ml b/spectec/src/il/eval.ml index b5c58d7c09..a2cc93fad0 100644 --- a/spectec/src/il/eval.ml +++ b/spectec/src/il/eval.ml @@ -524,7 +524,7 @@ and reduce_prem env prem : [`True of Subst.t | `False | `None] = else (match iter' with | Opt -> - (* Iterationen values es'/es_in are in hnf, so got to be options. *) + (* Iterationen values es_in are in hnf, so got to be options. *) let eos_in = List.map as_opt_exp es_in in if List.for_all Option.is_none eos_in then (* Iterating over empty options: nothing to do. *) @@ -555,7 +555,7 @@ and reduce_prem env prem : [`True of Subst.t | `False | `None] = `None | List | List1 -> (* Unspecified iteration count: get length from (first) iteration value - * and start over; es'/es_in is in hnf, so got to be a list. *) + * and start over; es_in are in hnf, so got to be lists. *) let n = List.length (as_list_exp (List.hd es_in)) in if iter' = List || n >= 1 then let en = NumE (`Nat (Z.of_int n)) $$ prem.at % (NumT `NatT $ prem.at) in @@ -565,7 +565,7 @@ and reduce_prem env prem : [`True of Subst.t | `False | `None] = * (This is a stuck computation, i.e., undefined.) *) `None | ListN ({it = NumE (`Nat n'); _}, xo) -> - (* Iterationen values es'/es_in are in hnf, so got to be lists. *) + (* Iterationen values es_in are in hnf, so got to be lists. *) let ess_in = List.map as_list_exp es_in in let ns = List.map List.length ess_in in let n = Z.to_int n' in