+ | Fold (`Left, base_pattern, names, rec_pattern) ->
+ let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
+ let meta_names =
+ List.filter ((<>) acc_name) (meta_names_of rec_pattern)
+ in
+ (match meta_names with
+ | [] -> assert false (* as above *)
+ | (name :: _) as names ->
+ let rec instantiate_fold_left acc env' =
+ prerr_endline "instantiate_fold_left";
+ match lookup_value ~env:env' name with
+ | ListValue (_ :: _) ->
+ instantiate_fold_left
+ (let acc_binding = acc_name, (TermType, TermValue acc) in
+ aux (acc_binding :: head_names names env') rec_pattern)
+ (tail_names names env')
+ | ListValue [] -> acc
+ | _ -> assert false
+ in
+ instantiate_fold_left (aux env base_pattern) env)
+ | Fold (`Right, base_pattern, names, rec_pattern) ->
+ let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
+ let meta_names =
+ List.filter ((<>) acc_name) (meta_names_of rec_pattern)
+ in
+ (match meta_names with
+ | [] -> assert false (* as above *)
+ | (name :: _) as names ->
+ let rec instantiate_fold_right env' =
+ prerr_endline "instantiate_fold_right";
+ match lookup_value ~env:env' name with
+ | ListValue (_ :: _) ->
+ let acc = instantiate_fold_right (tail_names names env') in
+ let acc_binding = acc_name, (TermType, TermValue acc) in
+ aux (acc_binding :: head_names names env') rec_pattern
+ | ListValue [] -> aux env base_pattern
+ | _ -> assert false
+ in
+ instantiate_fold_right env)